c launch: /data/cnf/sc2014/app/UR-15-10p0.cnf.bz2
c host: atom03
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 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 fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/UR-15-10p0.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UR-15-10p0.cnf.bz2
c no embedded options
c found 'p cnf 199290 1005792' header
c read 199290 variables, 1005792 clauses, 2392883 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 --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 189041 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 
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  189041   994873         0       0      0     0    0     0   35   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 5557 at-most-one constraints of average size 5.8
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 5557 out of 5557 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 54038 variables
c [simpleprobe-1] all 145252 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 94 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 94 variables, found 12399 hbrs, 1 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 1 units, 555 failed, 7032 tauts, 0 hbrs, 5829 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 144722 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 32474 not tried 22% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 56043 = 39% variables out of 144722 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 601952 negative 99.2% of 606815 except 4863 0.8%
c [phase-count-1] 476134 positive 78.5% of 606815 except 130681 21.5%
c [phase-count-1] less non-negative clauses 4863 than limit 60600 (10.0%)
c [phase-count-1] non-pos/non-neg = 130681/4863 = 26.87 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 88679 negative 100%
c [sort-queue-1] sorted 88679 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 88679 (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 62467 variables 41.3% (88679 remain 47%)
c [simplification-1] removed 388058 irredundant clauses 39.0% (606815 remain 61%)
c [simplification-1] maximum reduction of 41% = max (41%, 39%)
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.8   88678   606815         1       0      0  8499    0     0   38   0%      0    0    0    0    0%
c i    3.9   88672   606815        24      14      5  8502    0     3   38   2%      0    3    1    0 24340%
c i    3.9   88321   606815        33      22      5  8502    0     3   38   2%      0    3    1    0 23793%
c i    4.0   88208   606815       136     103     17  8506    1     8   38  13%      0    8   12    0 20012%
c i    4.0   87147   606815       137     103     17  8506    1     8   38  13%      0    8   12    0 19934%
c i    4.1   87130   606815       258     202     26  8512    1    11   38  12%      0   11   12    0 14656%
c i    4.1   86836   606815       316     247     31  8517    1    12   38  12%      0   12   11    0 12421%
c i    4.1   86774   606815       317     247     31  8517    1    12   38  12%      0   12   11    0 12373%
c i    4.3   86762   606815       442     341     38  8534    2    15   39  10%      0   15   10    0 9252%
c i    4.3   86721   606815       447     343     39  8535    2    15   39  10%      0   15   10    0 9198%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 2619 variables
c [simpleprobe-2] all 86060 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 36 variables
c [simpleprobe-2] 58688 variables remain 68% (27336 retained 32%)
c [simpleprobe-2] removed 36 variables, found 2608 hbrs, 14 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 77753 literals 45%
c [treelook-1] scheduling used 511674 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 379486 steps
c [treelook-1] 77746 literals remain 45%
c [treelook-1] 74751 variables remain to probed next time 87%
c [treelook-1] removed 0 variables, found 2751 hbrs
c [basicprobe-1] limit 4699960 based on 587495 irredundant clauses
c [basicprobe-1-0] 32215 probes remain 39% after last round
c [basicprobe-1-0] 20 units = 20 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 2933 variables, found 19628 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 5 units, 1093 failed, 6931 tauts, 0 hbrs, 1492 literals
c [elim-2] 31393 variables 38% will be scheduled this time
c [elim-2] scheduled 31393 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 8831 not tried 11% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 11 = 0% variables out of 31393 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 545012 negative 99.1% of 549876 except 4864 0.9%
c [phase-count-2] 429569 positive 78.1% of 549876 except 120307 21.9%
c [phase-count-2] less non-negative clauses 4864 than limit 54900 (10.0%)
c [phase-count-2] non-pos/non-neg = 120307/4864 = 24.73 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 6244 negative 100%
c [sort-queue-2] sorted 81990 enqueued variables after 447 conflicts
c [score-dist-2] active 0 (0%), one 11600 (14%), zero 70390 (86%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 4182 variables 4.9% (81990 remain 43%)
c [simplification-2] removed 56939 irredundant clauses 9.4% (549876 remain 55%)
c [simplification-2] maximum reduction of 9% = max (5%, 9%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1033 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    6.7   81989   549876       472     358     40 24694    2    17   36  10%      0   17    9    0 8842%
c i    6.7   81977   549876       473     358     40 24694    2    17   36  10%      0   17    9    0 8808%
c i    6.7   81972   549876       485     369     40 24694    2    17   36  10%      0   17    9    0 8689%
c i    6.8   81969   549876       516     396     41 24695    2    18   36   9%      0   18    9    0 8254%
c i    6.8   81968   549876       586     442     51 24704    2    20   36   9%      0   20   10    0 7974%
c i    6.9   81958   549876       595     449     51 24705    2    20   36   9%      0   20   10    0 7771%
c i    7.0   81841   549876       779     606     64 24710    3    25   36  12%      0   25   19    0 9586%
c i    7.2   81839   549876       920     724     74 24720    3    30   36  11%      1   29   17    0 7403%
c i    7.2   81829   549876       931     731     75 24722    3    30   36  11%      1   29   16    0 7145%
c i    7.2   81210   549876       968     756     80 24727    3    30   36  11%      1   29   15    0 6307%
c i    7.3   81178   549876      1036     810     88 24732    3    33   36  10%      1   33   13    0 5608%
c 
c [simplification-3] limit 1044 conflicts (hard 11000) hit after 1044 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4564 at-most-one constraints of average size 4.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4564 out of 4564 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 946 variables
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 5 units, 445 failed, 9419 tauts, 0 hbrs, 807 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 79862 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 15707 not tried 20% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1115 = 1% variables out of 79862 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 519607 negative 99.1% of 524435 except 4828 0.9%
c [phase-count-3] 410352 positive 78.2% of 524435 except 114083 21.8%
c [phase-count-3] less non-negative clauses 4828 than limit 52400 (10.0%)
c [phase-count-3] non-pos/non-neg = 114083/4828 = 23.63 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 1235 negative 100%
c [sort-queue-3] sorted 78747 enqueued variables after 1044 conflicts
c [score-dist-3] active 0 (0%), one 25563 (32%), zero 53184 (68%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 2421 variables 3.0% (78747 remain 42%)
c [simplification-3] removed 25441 irredundant clauses 4.6% (524435 remain 53%)
c [simplification-3] maximum reduction of 5% = max (3%, 5%)
c [simplification-3] large reduction 5% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13044 (soft 3044 + delta 10000)
c [simplification-3] new conflict limit 3044 (hard 13044)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    9.1   78746   524435      1161     760     95 22689    4    38   35   9%      1   38   12    0 4648%
c i    9.2   78630   524435      1219     812     98 22691    4    39   35   9%      1   39   11    0 4253%
c i    9.3   78622   524435      1249     839     98 22693    4    40   35   9%      1   40   11    0 4116%
c i    9.3   78615   524435      1250     839     98 22693    4    40   35   9%      1   40   11    0 4100%
c i    9.3   78564   524435      1291     872    101 22695    4    41   35  10%      1   41   14    0 4911%
c i    9.4   78563   524435      1339     905    105 22704    4    42   35  10%      1   42   13    0 4354%
c i    9.4   78550   524435      1366     926    107 22707    4    43   35   9%      1   42   12    0 4045%
c i    9.4   78119   524435      1382     940    108 22707    4    43   35   9%      1   42   12    0 3987%
c i    9.5   78102   524435      1417     967    111 22710    4    44   35   9%      1   43   12    0 3964%
c i    9.5   78090   524435      1448     992    114 22712    4    45   35   9%      1   45   12    0 3950%
c i    9.6   78085   524435      1568    1097    120 22718    4    51   35   8%      1   51   11    0 3321%
c i    9.7   78075   524435      1626    1136    123 22732    4    56   35   8%      1   55   10    0 3057%
c i    9.8   78034   524435      1633    1141    123 22733    4    56   35   8%      1   55   10    0 2992%
c i    9.8   77525   524435      1659    1157    127 22738    4    57   35   8%      1   56    9    0 2840%
c i    9.9   77514   524435      1711    1192    131 22748    4    57   35   8%      1   57    9    0 2554%
c i   10.1   77502   524435      1884    1322    146 22772    4    61   35   7%      1   60    7    0 2009%
c 
c [simplification-4] limit of 178 binary hit after 178 binaries
c [decomp-7] removed 1276 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 35438 literals 23%
c [treelook-2] scheduling used 153056 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 165910 steps
c [treelook-2] 35408 literals remain 23%
c [treelook-2] 33766 variables remain to probed next time 44%
c [decomp-8] removed 7 variables
c [treelook-2] removed 17 variables, found 1087 hbrs
c [unhide-4] limit 137500 with penalty 0 = 0 + 0
c [unhide-4-4] 2 units, 687 failed, 3071 tauts, 0 hbrs, 1303 literals
c [elim-4] 8587 variables 11% will be scheduled this time
c [elim-4] scheduled 8587 variables 11%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 17400957 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 8587 scheduled
c [phase-count-4] 506089 negative 99.1% of 510917 except 4828 0.9%
c [phase-count-4] 399524 positive 78.2% of 510917 except 111393 21.8%
c [phase-count-4] less non-negative clauses 4828 than limit 51000 (10.0%)
c [phase-count-4] non-pos/non-neg = 111393/4828 = 23.07 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 447 negative 100%
c [sort-queue-4] sorted 76915 enqueued variables after 1908 conflicts
c [score-dist-4] active 0 (0%), one 31892 (41%), zero 45023 (59%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 577 variables 0.7% (76915 remain 41%)
c [simplification-4] removed 13518 irredundant clauses 2.6% (510917 remain 51%)
c [simplification-4] maximum reduction of 3% = max (1%, 3%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3055 (hard 13044)
c [simplification-4] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   11.6   76914   510917      1942    1360    152 20479    5    66   34   7%      1   65    9    0 2525%
c i   12.0   76898   510917      2313    1677    177 20500    6    79   34   7%      1   77   16    0 3543%
c i   12.1   76884   510917      2391    1742    178 20511    6    80   34   7%      1   79   13    0 2858%
c i   12.2   76880   510917      2406    1753    179 20513    6    80   34   7%      1   79   13    0 2789%
c i   12.3   76875   510917      2555    1871    191 20525    6    83   34   8%      1   81   16    1 3135%
c i   12.3   76872   510917      2626    1929    199 20528    6    83   34   8%      1   81   15    1 2845%
c i   12.4   76860   510917      2677    1972    200 20533    6    84   34   8%      1   82   14    1 2665%
c i   12.5   76851   510917      2835    2089    212 20551    7    89   34   7%      1   87   13    1 2313%
c i   12.8   76738   510917      3017    2226    233 20572    7    92   35   7%      1   90   10    1 1786%
c i   12.8   76668   510917      3025    2232    234 20572    7    92   35   7%      1   90   11    1 1844%
c 
c [simplification-5] limit 3056 conflicts (hard 13044) hit after 3056 conflicts
c [quatres-1] found 29963 quaternary clauses 36% in total
c [quatres-1-2] added 3 single-self-subsuming ternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 76658 free variables schedulable
c [ternres-1] 20 ternary resolvents (2 bin, 18 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 29 xors of average arity 2.7
c [gauss-1] connected 79 occurrences of 51 variables (average 1.5)
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 8 variables
c [basicprobe-2] limit 5397416 penalty 0 = 0 + 0
c [basicprobe-2-0] 29319 probes remain 39% after last round
c [basicprobe-2-0] 31 units = 31 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 588 variables, found 15432 hbrs
c [bate-1] eliminated 21 asymmetric tautologies during probing
c [unhide-5] limit 215896 with penalty 0 = 0 + 0
c [unhide-5-5] 4 units, 248 failed, 9256 tauts, 0 hbrs, 2084 literals
c [transred-1] limit 1079483 with penalty 0 = 0 + 0
c [transred-1] removed 110 transitive binary clauses
c [transred-1] found 4 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 75676 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 9125 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 8 clauses out of 363 (2%) of length 10
c [cce-1-1] eliminated 65 clauses out of 1653 (4%) of length 9
c [cce-1-1] eliminated 20 clauses out of 372 (5%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 93 large clauses in 30000003 steps
c [cce-1-1] allowing another 15000001 steps for small clauses
c [cce-1-1] scheduling 265630 clauses = 249495 binary + 16135 ternary
c [cce-1-1] tried to eliminate 478 small clauses 0%
c [cce-1-1] eliminated 139 binary clauses 0%
c [cce-1-1] eliminated 13 ternary clauses 0%
c [cce-1-1] eliminated 152 small clauses 0%
c [cce-1-1] eliminated 152 small clauses in 30000000 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 245 covered clauses in round 1
c [cce-1] eliminated 245 covered clauses in TOTAL during 1 rounds
c [cce-1] 245 < 1/100 * 486829 = 4868 considered unsuccessful
c [bca-1] limit of 10000000 steps and 973668 added (scaled 2)
c [bca-1] 134227 out of 151354 literals actually usable 89%
c [bca-1] added 158 blocked clauses in 404683 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 4578 pos 6.0% + 71098 neg 94.0% = 75676 sched 100.0% ret 0
c [sweep-1-1] 1263964 steps 8 queries 19928.12 avg class size
c [sweep-1-1] 158 decisions 6 SAT calls 119.17 avg env size
c [sweep-1-1] 75666 variables remain 100% (10 retained 0%)
c [decomp-10] removed 2 variables
c [sweep-1-1] removed 2 vars (0 failed, 1 eqs, 1 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 2 vars in TOTAL (1 rounds, 7 queries)
c [phase-count-5] 481772 negative 99.0% of 486580 except 4808 1.0%
c [phase-count-5] 388417 positive 79.8% of 486580 except 98163 20.2%
c [phase-count-5] less non-negative clauses 4808 than limit 48600 (10.0%)
c [phase-count-5] non-pos/non-neg = 98163/4808 = 20.42 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 200 negative 100%
c [sort-queue-5] sorted 75674 enqueued variables after 3056 conflicts
c [score-dist-5] active 0 (0%), one 37777 (50%), zero 37897 (50%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 984 variables 1.3% (75674 remain 40%)
c [simplification-5] removed 24337 irredundant clauses 4.8% (486580 remain 49%)
c [simplification-5] maximum reduction of 5% = max (1%, 5%)
c [simplification-5] large reduction 5% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 15056 (soft 5056 + delta 10000)
c [simplification-5] new conflict limit 5056 (hard 15056)
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   16.0   75673   486580      3162    2335    314 45050    7    96   35   7%      1   94   10    1 1723%
c i   16.0   75652   486580      3185    2353    316 45052    7    97   35   7%      1   95   11    1 1784%
c i   16.1   75645   486580      3188    2355    316 45052    7    97   35   7%      1   95   11    1 1773%
c i   16.1   75640   486580      3198    2362    317 45052    7    97   35   7%      1   95   11    1 1766%
c i   16.2   75575   486580      3426    2552    336 45067    7    98   35   7%      1   96   10    1 1523%
c i   16.4   75547   486580      3526    2628    343 45078    7   100   35   7%      1   97   12    1 1747%
c i   16.5   75539   486580      3612    2687    349 45098    7   101   35   7%      1   98   10    1 1479%
c i   16.6   75532   486580      3681    2750    353 45099    7   102   35   7%      1   99   11    1 1596%
c i   16.7   75531   486580      3702    2769    353 45099    7   102   35   7%      1   99   11    1 1587%
c i   16.7   75525   486580      3726    2789    354 45099    7   102   35   7%      1   99   12    1 1699%
c i   16.8   75517   486580      3813    2857    367 45103    7   102   35   7%      1   99   11    1 1570%
c i   16.8   75511   486580      3820    2862    368 45103    7   102   35   7%      1   99   11    1 1573%
c i   16.9   75502   486580      3908    2936    374 45110    7   104   35   7%      1  101   12    1 1595%
c i   17.0   75498   486580      3943    2967    374 45113    8   105   35   7%      1  102   11    1 1530%
c i   17.0   75336   486580      3955    2975    374 45116    8   105   35   7%      1  102   11    1 1506%
c i   17.0   75335   486580      3986    2999    376 45120    8   107   35   7%      1  103   11    1 1443%
c i   17.0   75325   486580      3988    3000    376 45120    7   107   35   7%      1  103   10    1 1435%
c i   17.3   75312   486580      4202    3183    383 45133    8   110   35   8%      1  106   17    1 2125%
c i   17.3   75301   486580      4203    3183    383 45133    8   110   35   8%      1  106   17    1 2117%
c i   17.3   75265   486580      4204    3183    383 45133    8   110   35   8%      1  106   17    1 2109%
c i   17.4   75261   486580      4280    3249    387 45136    9   113   35   8%      1  109   22    1 2614%
c i   17.5   75260   486580      4340    3304    390 45137    9   114   35   8%      1  110   20    1 2304%
c i   17.6   75180   486580      4457    3398    396 45153    9   117   35   8%      1  112   18    1 2075%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   17.6   75168   486580      4483    3422    396 45154    9   117   35   8%      1  112   18    1 2020%
c i   17.7   75166   486580      4524    3452    401 45159    9   117   35   8%      1  112   17    1 1881%
c i   17.7   75157   486580      4528    3453    401 45161    9   117   35   8%      1  112   17    1 1854%
c i   18.1   75147   486580      4941    3818    415 45184   10   124   35   8%      2  118   21    1 2001%
c i   18.2   75138   486580      4974    3848    416 45185   10   124   35   8%      2  119   20    1 1884%
c i   18.2   75056   486580      5000    3866    419 45188   10   125   35   8%      2  120   18    1 1777%
c i   18.2   74239   486580      5002    3866    419 45189   10   125   35   8%      2  120   18    1 1764%
c 
c [simplification-6] limit 5093 conflicts (hard 15056) hit after 5094 conflicts
c [quatres-2] found 31030 quaternary clauses 39% in total
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 73987 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] 36961 variables remain 50% (37026 retained 50%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2263 at-most-one constraints of average size 4.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2263 out of 2263 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 1716 variables
c [simpleprobe-3] 50562 schedulable variables 68%
c [simpleprobe-3] limit 7110647 penalty 0 = 0 + 0
c [decomp-12] removed 504 variables
c [simpleprobe-3] 27357 variables remain 37% (46097 retained 63%)
c [simpleprobe-3] removed 504 variables, found 19164 hbrs, 287 units
c [unhide-6] limit 355532 with penalty 0 = 0 + 0
c [unhide-6-6] 10 units, 456 failed, 6514 tauts, 0 hbrs, 4475 literals
c [transred-2] limit 1777661 with penalty 0 = 0 + 0
c [transred-2] removed 165 transitive binary clauses
c [transred-2] found 10 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 72888 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 527 blocked clauses
c [block-2] 527 < 1/100 * 473269 = 4732 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 72887 variables 100%
c [elim-5] limit of 17776618 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 13974 not tried 19% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1466 = 2% variables out of 72887 scheduled
c [bca-2] limit of 10000000 steps and 929821 added (scaled 2)
c [bca-2] 124729 out of 142844 literals actually usable 87%
c [bca-2] added 106 blocked clauses in 375581 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 4290 pos 6.0% + 67123 neg 94.0% = 71413 sched 100.0% ret 8
c [sweep-2-1] 1008018 steps 20 queries 14759.60 avg class size
c [sweep-2-1] 150 decisions 18 SAT calls 46.83 avg env size
c [sweep-2-1] 71198 variables remain 100% (151 retained 0%)
c [decomp-13] removed 80 variables
c [sweep-2-1] removed 80 vars (0 failed, 1 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 80 vars in TOTAL (1 rounds, 19 queries)
c [phase-count-6] 459501 negative 99.0% of 464265 except 4764 1.0%
c [phase-count-6] 369114 positive 79.5% of 464265 except 95151 20.5%
c [phase-count-6] less non-negative clauses 4764 than limit 46400 (10.0%)
c [phase-count-6] non-pos/non-neg = 95151/4764 = 19.97 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 45 negative 100%
c [sort-queue-6] sorted 71341 enqueued variables after 5094 conflicts
c [score-dist-6] active 0 (0%), one 40596 (57%), zero 30745 (43%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 2646 variables 3.6% (71341 remain 38%)
c [simplification-6] removed 22315 irredundant clauses 4.6% (464265 remain 47%)
c [simplification-6] maximum reduction of 5% = max (4%, 5%)
c [simplification-6] large reduction 5% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 17094 (soft 7094 + delta 10000)
c [simplification-6] new conflict limit 7094 (hard 17094)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   21.6   71340   464265      5238    3655    429 57265   10   127   35   8%      2  122   14    1 1310%
c i   21.6   70964   464265      5256    3668    430 57266   10   128   35   8%      2  122   14    1 1262%
c i   21.6   70952   464265      5270    3680    431 57266   10   127   35   8%      2  121   13    1 1224%
c i   21.9   70947   464265      5467    3845    443 57279   11   129   35   8%      2  123   14    1 1281%
c i   22.0   70944   464265      5568    3920    449 57296   11   130   35   8%      2  123   14    1 1209%
c i   22.1   70939   464265      5612    3961    449 57298   11   132   35   8%      1  126   15    1 1264%
c i   22.2   70938   464265      5744    4068    458 57310   11   132   35   8%      1  126   14    1 1190%
c i   22.2   70929   464265      5762    4081    460 57312   11   133   35   8%      1  126   14    1 1202%
c i   22.3   70918   464265      5827    4127    466 57323   11   133   35   8%      1  126   13    1 1129%
c i   22.3   70785   464265      5833    4130    467 57324   11   133   35   8%      1  126   13    1 1107%
c i   22.5   70712   464265      5985    4253    479 57338   11   133   35   8%      1  126   11    1  950%
c i   22.5   70705   464265      5999    4263    481 57339   11   133   35   8%      1  125   11    1  928%
c i   22.5   70633   464265      6034    4294    484 57339   11   133   35   8%      1  126   12    1  948%
c i   22.6   70518   464265      6038    4297    484 57339   11   133   35   8%      1  126   11    1  944%
c i   22.6   70509   464265      6089    4332    489 57346   11   133   35   8%      1  125   11    1  868%
c i   22.8   69955   464265      6203    4424    498 57355   11   133   35   8%      1  125   12    1  980%
c i   22.9   69954   464265      6307    4515    503 57356   12   134   35   9%      1  126   21    1 1603%
c i   22.9   69945   464265      6342    4542    505 57360   12   134   35   9%      1  126   20    1 1498%
c i   22.9   69942   464265      6350    4549    505 57360   12   133   35   9%      1  126   19    1 1489%
c i   22.9   69939   464265      6369    4564    505 57360   12   133   35   9%      1  125   21    1 1598%
c i   22.9   69938   464265      6443    4623    512 57364   12   132   35   9%      1  124   20    1 1466%
c i   23.0   69937   464265      6506    4676    513 57372   12   132   35   9%      1  124   18    1 1318%
c i   23.2   69868   464265      6661    4787    525 57399   12   131   35   9%      1  122   13    1  959%
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   23.2   69848   464265      6683    4804    525 57403   12   131   35   9%      1  122   12    1  904%
c i   23.3   69837   464265      6792    4873    542 57423   11   130   35   9%      1  121   10    1  701%
c i   23.4   69835   464265      6878    4948    545 57428   11   129   35   9%      1  120   11    1  801%
c i   23.5   69826   464265      6926    4986    550 57432   11   131   35   9%      1  122   12    1  876%
c 
c [simplification-7] limit 7098 conflicts (hard 17094) hit after 7098 conflicts
c [quatres-3] found 30836 quaternary clauses 41% in total
c [quatres-3-2] added 4 single-self-subsuming ternary resolvents
c [quatres-3-2] added 24 quaternary resolvents
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 219 xors of average arity 2.2
c [gauss-2] connected 477 occurrences of 249 variables (average 1.9)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 145 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 47211 literals 34%
c [treelook-3] scheduling used 300772 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 448880 steps
c [treelook-3] 47208 literals remain 34%
c [treelook-3] 24913 variables remain to probed next time 36%
c [treelook-3] removed 0 variables, found 3182 hbrs
c [unhide-7] limit 487482 with penalty 0 = 0 + 0
c [unhide-7-7] 2 units, 174 failed, 8152 tauts, 0 hbrs, 6015 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 194 transitive binary clauses
c [transred-3] found 7 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 14 clauses out of 349 (4%) of length 8
c [cce-2-1] eliminated 44 clauses out of 832 (5%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 58 large clauses in 15000002 steps
c [cce-2-1] allowing another 7500001 steps for small clauses
c [cce-2-1] scheduling 245830 clauses = 227280 binary + 18550 ternary
c [cce-2-1] tried to eliminate 256 small clauses 0%
c [cce-2-1] eliminated 69 binary clauses 0%
c [cce-2-1] eliminated 16 ternary clauses 0%
c [cce-2-1] eliminated 85 small clauses 0%
c [cce-2-1] eliminated 1519 small clauses in 15000005 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1577 covered clauses in round 1
c [cce-2] eliminated 1577 covered clauses in TOTAL during 1 rounds
c [cce-2] 1577 < 1/100 * 449142 = 4491 considered unsuccessful
c [elim-6] 13789 variables 20% will be scheduled this time
c [elim-6] scheduled 13789 variables 20%
c [elim-6] limit of 48748291 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 22535737 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 13789 scheduled
c [bca-3] limit of 10000000 steps and 891914 added (scaled 2)
c [bca-3] 116253 out of 139002 literals actually usable 84%
c [bca-3] added 47 blocked clauses in 329057 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 3977 pos 5.7% + 65377 neg 94.3% = 69354 sched 99.8% ret 146
c [sweep-3-1] 1194362 steps 18 queries 14736.67 avg class size
c [sweep-3-1] 258 decisions 16 SAT calls 126.69 avg env size
c [sweep-3-1] 69299 variables remain 100% (201 retained 0%)
c [decomp-16] removed 50 variables
c [sweep-3-1] removed 50 vars (0 failed, 1 eqs, 2 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 50 vars in TOTAL (1 rounds, 17 queries)
c [phase-count-7] 440778 negative 98.9% of 445541 except 4763 1.1%
c [phase-count-7] 355335 positive 79.8% of 445541 except 90206 20.2%
c [phase-count-7] less non-negative clauses 4763 than limit 44500 (10.0%)
c [phase-count-7] non-pos/non-neg = 90206/4763 = 18.94 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 17 negative 100%
c [sort-queue-7] sorted 69450 enqueued variables after 7098 conflicts
c [score-dist-7] active 0 (0%), one 44305 (64%), zero 25145 (36%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 364 variables 0.5% (69450 remain 37%)
c [simplification-7] removed 18724 irredundant clauses 4.0% (445541 remain 45%)
c [simplification-7] maximum reduction of 4% = max (1%, 4%)
c [simplification-7] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-7] new conflict interval 4000
c [simplification-7] penalized conflict interval 4000 = 1 * 4000
c [simplification-7] hard conflict limit 21098 (soft 11098 + delta 10000)
c [simplification-7] new conflict limit 11098 (hard 21098)
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   26.8   69449   445541      7309    5297    582 60300   12   136   35   9%      2  126   12    1  801%
c i   26.8   69445   445541      7352    5336    584 60301   12   136   35   9%      2  126   15    1 1023%
c i   27.0   69422   445541      7528    5486    589 60317   12   141   35   9%      1  131   18    2 1192%
c i   27.0   69416   445541      7530    5487    589 60317   12   141   35   9%      1  130   18    2 1185%
c i   27.1   69413   445541      7665    5605    592 60326   13   142   35   9%      1  131   18    2 1161%
c i   27.3   69273   445541      7800    5724    603 60329   13   144   35   9%      1  133   20    2 1245%
c i   27.3   69074   445541      7801    5724    603 60329   13   144   35   9%      1  133   20    2 1240%
c i   27.3   69043   445541      7846    5764    604 60332   13   144   35   9%      1  133   24    2 1436%
c i   27.5   69042   445541      7995    5878    618 60351   13   145   35   9%      1  134   20    2 1165%
c i   27.6   69036   445541      8019    5899    618 60353   13   146   35   9%      1  135   19    2 1126%
c i   27.8   69032   445541      8280    6126    624 60374   14   148   35   9%      1  137   21    2 1180%
c i   27.8   69024   445541      8293    6137    625 60374   14   149   35   9%      1  137   21    2 1208%
c i   28.3   69020   445541      8689    6479    650 60396   15   160   35   9%      2  147   21    2 1121%
c i   28.3   69014   445541      8694    6481    650 60398   15   159   35   9%      2  147   21    2 1107%
c i   28.6   68982   445541      8938    6689    665 60413   15   163   35   9%      2  150   22    2 1094%
c i   29.0   68979   445541      9310    7011    678 60432   16   162   35  10%      2  148   26    2 1257%
c i   29.2   68974   445541      9441    7125    687 60438   16   165   35  10%      2  151   29    2 1323%
c i   29.3   68834   445541      9525    7201    687 60444   16   165   35  10%      2  150   24    2 1106%
c i   29.3   68833   445541      9540    7213    688 60445   17   165   35  10%      2  151   31    2 1398%
c i   29.4   68827   445541      9623    7288    690 60448   17   169   36  10%      2  154   35    2 1554%
c i   29.5   68826   445541      9664    7324    694 60448   17   168   36  10%      2  154   33    2 1468%
c i   29.7   68825   445541      9812    7450    702 60454   18   168   36  11%      2  153   29    2 1261%
c i   29.8   68821   445541      9951    7576    705 60461   18   167   36  11%      2  151   23    2  972%
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   29.9   68820   445541      9983    7604    707 60462   18   166   36  11%      1  151   22    2  920%
c i   30.6   68819   445541     10645    8194    727 60488   21   168   37  12%      3  151   42    3 1556%
c i   30.7   68802   445541     10710    8243    732 60497   21   170   37  12%      3  153   40    3 1473%
c i   30.7   68679   445541     10785    8310    734 60499   21   169   37  12%      3  152   39    3 1391%
c i   30.8   68678   445541     10827    8347    736 60500   21   171   37  12%      3  153   34    3 1233%
c i   30.9   68677   445541     10895    8407    741 60501   21   171   37  12%      3  154   31    3 1098%
c i   31.1   68676   445541     11062    8551    749 60513   21   175   37  12%      2  157   27    3  932%
c i   31.1   68673   445541     11065    8553    749 60513   21   174   37  12%      2  156   26    3  923%
c i   31.1   68516   445541     11098    8577    753 60517   21   174   37  12%      2  156   24    3  846%
c 
c [simplification-8] limit 11118 conflicts (hard 21098) hit after 11118 conflicts
c [quatres-4] found 30535 quaternary clauses 42% in total
c [quatres-4-2] added 1 single-self-subsuming ternary resolvents
c [ternres-3] limit 2000000 with penalty 1 = 1 + 0
c [ternres-3] 34228 schedulable variables 49%
c [ternres-3] 8 ternary resolvents (0 bin, 8 trn)
c [ternres-3] 15925 variables remain 23% (52565 retained 77%)
c [decomp-17] removed 1037 variables
c [basicprobe-3] limit 18890557 penalty 0 = 0 + 0
c [basicprobe-3-0] 24482 probes remain 36% after last round
c [basicprobe-3-0] 70 units = 70 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 378 variables, found 52330 hbrs
c [bate-2] eliminated 44 asymmetric tautologies during probing
c [unhide-8] limit 755622 with penalty 0 = 0 + 0
c [unhide-8-8] 14 units, 650 failed, 8495 tauts, 0 hbrs, 15115 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 224 transitive binary clauses
c [transred-4] found 4 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 67109 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 216 blocked clauses
c [block-3] 216 < 1/100 * 436563 = 4365 considered unsuccessful
c [bca-4] limit of 10000000 steps and 859841 added (scaled 2)
c [bca-4] 108285 out of 134220 literals actually usable 81%
c [bca-4] added 62 blocked clauses in 301427 steps
c [sweep-4] limit 1133433 penalty 0 = 0 + 0
c [sweep-4-1] 4121 pos 6.2% + 62795 neg 93.8% = 66916 sched 99.7% ret 193
c [sweep-4-1] 1165867 steps 14 queries 11989.29 avg class size
c [sweep-4-1] 116 decisions 12 SAT calls 59.92 avg env size
c [sweep-4-1] 66867 variables remain 100% (227 retained 0%)
c [decomp-18] removed 156 variables
c [sweep-4-1] removed 156 vars (0 failed, 2 eqs, 2 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 156 vars in TOTAL (1 rounds, 13 queries)
c [phase-count-8] 424401 negative 98.9% of 429165 except 4764 1.1%
c [phase-count-8] 341789 positive 79.6% of 429165 except 87376 20.4%
c [phase-count-8] less non-negative clauses 4764 than limit 42900 (10.0%)
c [phase-count-8] non-pos/non-neg = 87376/4764 = 18.34 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 8 negative 100%
c [sort-queue-8] sorted 66953 enqueued variables after 11118 conflicts
c [score-dist-8] active 0 (0%), one 45628 (68%), zero 21325 (32%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 1537 variables 2.2% (66953 remain 35%)
c [simplification-8] removed 16376 irredundant clauses 3.7% (429165 remain 43%)
c [simplification-8] maximum reduction of 4% = max (2%, 4%)
c [simplification-8] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-8] new conflict interval 8000
c [simplification-8] penalized conflict interval 8000 = 1 * 8000
c [simplification-8] hard conflict limit 29118 (soft 19118 + delta 10000)
c [simplification-8] new conflict limit 19118 (hard 29118)
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   34.1   66952   429165     11309    8668    768 101394   21   173   38  12%      2  154   22    3  748%
c i   34.2   66951   429165     11367    8721    768 101398   21   173   38  12%      2  154   22    3  761%
c i   34.2   66946   429165     11389    8738    769 101401   21   172   38  12%      2  153   21    3  713%
c i   34.3   66945   429165     11429    8770    771 101406   21   172   38  12%      2  153   21    3  701%
c i   34.5   66804   429165     11549    8876    778 101412   21   174   38  12%      2  155   23    3  781%
c i   34.5   66803   429165     11584    8906    780 101413   21   174   38  12%      2  155   24    3  792%
c i   34.9   66802   429165     11835    9131    795 101423   21   181   38  12%      2  161   24    3  774%
c i   34.9   66800   429165     11839    9133    795 101424   21   181   38  12%      2  161   24    3  770%
c i   35.6   66797   429165     12448    9674    821 101457   22   182   38  12%      3  161   29    3  888%
c i   35.8   66796   429165     12589    9803    825 101462   22   185   38  12%      3  164   28    3  827%
c i   35.9   66791   429165     12684    9885    831 101467   23   187   38  12%      3  165   30    3  889%
c i   35.9   66786   429165     12704    9901    832 101469   23   187   38  12%      3  165   30    3  891%
c i   36.0   66785   429165     12791    9978    837 101473   23   187   38  12%      2  165   29    3  835%
c i   36.3   66780   429165     13005   10158    853 101487   23   188   38  12%      2  165   27    4  765%
c i   36.3   66778   429165     13033   10185    853 101487   23   189   38  12%      2  166   27    4  769%
c i   36.5   66777   429165     13172   10314    856 101492   24   191   38  12%      2  168   33    4  907%
c i   36.7   66776   429165     13272   10406    857 101496   24   195   38  12%      2  172   37    4 1016%
c i   37.4   66775   429165     13825   10894    878 101522   25   199   38  12%      3  174   33    4  850%
c i   37.5   66774   429165     13912   10972    880 101527   24   199   38  12%      3  174   27    4  700%
c i   37.5   66691   429165     13932   10988    881 101529   24   199   38  12%      3  174   26    4  663%
c i   37.6   66686   429165     14005   11044    884 101535   25   199   39  12%      2  173   27    4  684%
c i   37.7   66476   429165     14096   11128    885 101540   24   199   39  12%      2  173   25    4  623%
c i   37.9   66475   429165     14205   11226    889 101542   24   198   39  12%      2  172   24    4  604%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   37.9   66474   429165     14206   11226    889 101542   24   198   39  12%      2  172   24    4  602%
c i   38.1   66472   429165     14366   11366    893 101549   25   196   39  13%      2  170   32    4  779%
c i   38.2   66471   429165     14498   11487    899 101552   25   198   39  13%      2  172   30    4  724%
c i   38.3   66466   429165     14572   11554    900 101556   26   202   39  13%      2  175   50    4 1192%
c i   39.2   66462   429165     15335   12219    932 101590   28   207   39  14%      4  178   31    5  683%
c i   39.2   66461   429165     15377   12258    932 101592   28   205   39  14%      4  176   29    5  635%
c i   39.3   66458   429165     15474   12335    946 101595   28   205   39  14%      4  175   26    5  565%
c i   39.7   66430   429165     15822   12644    957 101615   29   206   40  14%      3  176   39    5  817%
c i   40.0   66429   429165     16002   12797    971 101624   29   207   40  14%      3  176   36    5  737%
c i   40.2   66428   429165     16164   12944    977 101628   29   204   40  14%      3  173   33    5  675%
c i   40.4   66358   429165     16358   13119    986 101636   29   204   40  14%      2  173   27    5  547%
c i   40.6   66350   429165     16569   13312    989 101645   29   205   40  14%      2  173   28    5  556%
c i   40.9   66349   429165     16754   13490    991 101647   29   207   41  14%      2  174   26    5  507%
c i   41.0   66348   429165     16833   13554    995 101654   28   205   41  14%      2  172   26    5  500%
c i   41.4   66252   429165     17140   13833   1007 101659   29   204   41  14%      2  170   36    5  676%
c i   41.5   66251   429165     17200   13886   1008 101661   29   203   41  14%      2  170   33    5  614%
c i   41.5   66247   429165     17254   13930   1008 101668   29   203   41  14%      2  169   31    5  575%
c i   42.1   66241   429165     17662   14305   1019 101679   29   205   42  14%      2  170   39    6  707%
c i   42.6   66240   429165     18094   14699   1026 101701   30   203   43  15%      2  167   34    6  595%
c i   42.6   66232   429165     18135   14736   1027 101702   30   204   43  15%      2  168   34    6  600%
c i   42.7   66229   429165     18263   14851   1031 101706   30   202   43  15%      2  166   31    6  540%
c i   42.7   66223   429165     18264   14851   1031 101706   30   202   43  15%      2  166   31    6  538%
c i   42.8   66063   429165     18322   14896   1033 101712   30   202   43  15%      2  165   32    6  559%
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   43.0   66061   429165     18456   15022   1037 101713   30   200   43  15%      2  163   31    6  524%
c i   43.0   66050   429165     18503   15063   1037 101714   31   202   43  15%      2  165   43    6  730%
c i   43.8   66049   429165     19081   15585   1048 101736   32   205   44  16%      3  167   40    6  640%
c i   43.8   66048   429165     19104   15601   1048 101742   32   204   44  16%      3  166   37    6  604%
c 
c [simplification-9] limit 19140 conflicts (hard 29118) hit after 19140 conflicts
c [quatres-5] found 26850 quaternary clauses 40% in total
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [ternres-4] limit 6584981 with penalty 0 = 0 + 0
c [ternres-4] 15345 schedulable variables 23%
c [ternres-4] 25 ternary resolvents (1 bin, 24 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-19] removed 1462 variables
c [simpleprobe-4] 25312 schedulable variables 39%
c [simpleprobe-4] limit 26339926 penalty 0 = 0 + 0
c [decomp-20] removed 1035 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 1035 variables, found 42597 hbrs, 313 units
c [unhide-9] limit 1316996 with penalty 0 = 0 + 0
c [unhide-9-9] 5 units, 155 failed, 7235 tauts, 0 hbrs, 34774 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 210 transitive binary clauses
c [transred-5] found 2 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 64290 variables 100%
c [elim-7] limit of 65849816 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 3833 variables 6% in round 1 in 37277560 steps
c [elim-7-1] backward subsumption/strengthening limit 28572256
c [elim-7-1-1] backward checking 11165 touched variables 17%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 19 and strengthened 121 clauses in 3921218 steps
c [elim-7-1] rescheduled 322 variables 1% by backward subsumption
c [elim-7-2] eliminated 43 variables 0% in round 2 in 377788 steps
c [elim-7-2] backward subsumption/strengthening limit 377700
c [elim-7-2-1] backward checking 303 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 223991 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 3888 = 6% variables out of 64290 scheduled
c [bca-5] limit of 10000000 steps and 803554 added (scaled 2)
c [bca-5] 96026 out of 120806 literals actually usable 79%
c [bca-5] added 68 blocked clauses in 266072 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 19754940 penalty 0 = 0 + 0
c [sweep-5-1] 3620 pos 6.0% + 56584 neg 94.0% = 60204 sched 99.7% ret 198
c [sweep-5-1] 19881431 steps 246 queries 1621.89 avg class size
c [sweep-5-1] 2618 decisions 218 SAT calls 94.28 avg env size
c [sweep-5-1] 52291 variables remain 87% (8023 retained 13%)
c [decomp-21] removed 166 variables
c [sweep-5-1] removed 166 vars (0 failed, 35 eqs, 60 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 166 vars in TOTAL (1 rounds, 245 queries)
c [phase-count-9] 396611 negative 99.0% of 400628 except 4017 1.0%
c [phase-count-9] 318468 positive 79.5% of 400628 except 82160 20.5%
c [phase-count-9] less non-negative clauses 4017 than limit 40000 (10.0%)
c [phase-count-9] non-pos/non-neg = 82160/4017 = 20.45 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 6 negative 100%
c [sort-queue-9] sorted 60236 enqueued variables after 19140 conflicts
c [score-dist-9] active 0 (0%), one 42820 (71%), zero 17416 (29%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 5803 variables 8.8% (60236 remain 32%)
c [simplification-9] removed 28537 irredundant clauses 6.6% (400628 remain 40%)
c [simplification-9] maximum reduction of 9% = max (9%, 7%)
c [simplification-9] large reduction 9% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 31140 (soft 21140 + delta 10000)
c [simplification-9] new conflict limit 21140 (hard 31140)
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.9   60235   400628     19300    9850    905 143184   31   204   38  15%      3  165   28    6  448%
c i   49.4   60234   400628     19711   10205    927 143207   30   206   38  15%      3  165   22    6  343%
c i   49.4   60233   400628     19782   10274    928 143207   30   204   38  15%      2  164   20    6  320%
c i   49.5   60193   400628     19815   10300    931 143208   30   204   38  15%      2  164   25    6  387%
c i   49.5   60192   400628     19845   10326    932 143210   30   204   38  15%      2  164   24    6  375%
c i   49.9   60191   400628     20189   10646    942 143221   30   206   38  14%      2  164   22    6  340%
c i   49.9   60190   400628     20203   10657    942 143223   30   205   38  14%      2  164   24    6  370%
c i   50.2   60189   400628     20479   10905    953 143234   29   203   38  14%      2  161   23    7  355%
c i   50.4   60188   400628     20645   11056    960 143240   29   202   38  14%      2  160   22    7  334%
c 
c [simplification-10] limit 21140 conflicts (hard 31140) hit after 21140 conflicts
c [quatres-6] found 27346 quaternary clauses 40% in total
c [ternres-5] limit 7279322 with penalty 0 = 0 + 0
c [ternres-5] all 60185 free variables schedulable
c [ternres-5] 109 ternary resolvents (2 bin, 107 trn)
c [ternres-5] 4948 variables remain 8% (55237 retained 92%)
c [card-4] limit 454957 penalty 3 = 3 + 0
c [card-4] found 1198 at-most-one constraints of average size 3.8
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 454957 for elimination
c [card-4] 1198 out of 1198 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 36 xors of average arity 2.3
c [gauss-3] connected 82 occurrences of 37 variables (average 2.2)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 51 variables
c [unhide-10] limit 1455864 with penalty 0 = 0 + 0
c [unhide-10-10] 21 units, 362 failed, 13059 tauts, 0 hbrs, 20928 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 203 transitive binary clauses
c [transred-6] found 7 units
c [cce-3] limit of 9099152 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 269 (0%) of length 10
c [cce-3-1] eliminated 2 clauses out of 328 (1%) of length 8
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 3 large clauses in 9099152 steps
c [cce-3-1] allowing another 4549576 steps for small clauses
c [cce-3-1] scheduling 310547 clauses = 199690 binary + 110857 ternary
c [cce-3-1] tried to eliminate 145 small clauses 0%
c [cce-3-1] eliminated 23 binary clauses 0%
c [cce-3-1] eliminated 17 ternary clauses 0%
c [cce-3-1] eliminated 40 small clauses 0%
c [cce-3-1] eliminated 2954 small clauses in 9099165 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 2957 covered clauses in round 1
c [cce-3] eliminated 2957 covered clauses in TOTAL during 1 rounds
c [cce-3] 2957 < 1/100 * 399829 = 3998 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 59786 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2911728940 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 351 variables 1% in round 1 in 35974611 steps
c [elim-8-1] backward subsumption/strengthening limit 35974600
c [elim-8-1-1] backward checking 1515 touched variables 3%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 3 and strengthened 11 clauses in 625897 steps
c [elim-8-1] rescheduled 39 variables 0% by backward subsumption
c [elim-8-2] eliminated 4 variables 0% in round 2 in 48777 steps
c [elim-8-2] backward subsumption/strengthening limit 48700
c [elim-8-2-1] backward checking 31 touched variables 0%
c [elim-8-2-1] incomplete backward checking 0 remain 0%
c [elim-8-2] subsumed 0 and strengthened 1 clauses in 48701 steps
c [elim-8-2] rescheduled 5 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 2217 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 358 = 1% variables out of 59786 scheduled
c [elim-8] 358 < 1/100 * 59786 = 597 considered unsuccessful
c [bca-6] limit of 10000000 steps and 792232 added (scaled 2)
c [bca-6] 92234 out of 118858 literals actually usable 78%
c [bca-6] added 56 blocked clauses in 249922 steps
c [sweep-6] limit 2183796 penalty 0 = 0 + 0
c [sweep-6-1] 3956 pos 7.6% + 47793 neg 92.4% = 51749 sched 87.1% ret 7679
c [sweep-6-1] 2201027 steps 26 queries 5828.04 avg class size
c [sweep-6-1] 483 decisions 24 SAT calls 126.46 avg env size
c [sweep-6-1] 51572 variables remain 87% (7856 retained 13%)
c [decomp-23] removed 2 variables
c [sweep-6-1] removed 2 vars (0 failed, 1 eqs, 5 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 2 vars in TOTAL (1 rounds, 25 queries)
c [phase-count-10] 391821 negative 99.0% of 395754 except 3933 1.0%
c [phase-count-10] 313945 positive 79.3% of 395754 except 81809 20.7%
c [phase-count-10] less non-negative clauses 3933 than limit 39500 (10.0%)
c [phase-count-10] non-pos/non-neg = 81809/3933 = 20.80 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 4 negative 100%
c [sort-queue-10] sorted 59426 enqueued variables after 21140 conflicts
c [score-dist-10] active 0 (0%), one 42689 (72%), zero 16737 (28%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 759 variables 1.3% (59426 remain 31%)
c [simplification-10] removed 4874 irredundant clauses 1.2% (395754 remain 40%)
c [simplification-10] maximum reduction of 1% = max (1%, 1%)
c [simplification-10] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-10] new conflict interval 18000
c [simplification-10] penalized conflict interval 18000 = 1 * 18000
c [simplification-10] hard conflict limit 49140 (soft 39140 + delta 10000)
c [simplification-10] new conflict limit 39140 (hard 49140)
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   54.1   59425   395754     21176   10879   1052 131755   28   202   37  14%      3  158   24    7  351%
c i   54.3   59424   395754     21294   10984   1054 131761   28   202   38  14%      2  158   23    7  341%
c i   54.5   59423   395754     21502   11176   1057 131771   27   199   38  14%      2  154   20    7  302%
c i   54.9   59422   395754     21933   11570   1074 131784   27   195   38  14%      2  149   26    7  372%
c i   55.7   59401   395754     22628   12216   1087 131803   27   190   38  14%      4  142   27    7  382%
c i   55.8   59400   395754     22775   12348   1095 131808   27   188   38  14%      3  140   23    7  324%
c i   55.8   59399   395754     22785   12356   1095 131808   27   188   38  14%      3  140   23    7  326%
c i   56.0   59386   395754     22903   12460   1096 131816   27   189   38  14%      3  141   27    7  375%
c i   56.4   59385   395754     23322   12848   1109 131825   27   188   38  15%      3  139   30    7  404%
c i   56.5   59384   395754     23367   12887   1111 131826   27   187   38  15%      3  138   31    7  424%
c i   56.6   59383   395754     23445   12960   1112 131828   27   186   38  15%      3  138   30    7  405%
c i   56.6   59382   395754     23470   12981   1114 131829   27   187   38  15%      3  138   28    7  382%
c i   56.6   59380   395754     23471   12981   1114 131829   27   187   38  15%      3  138   28    7  381%
c i   57.1   59379   395754     23897   13382   1123 131835   27   188   38  14%      3  139   26    7  343%
c i   57.2   59375   395754     23974   13455   1124 131837   27   189   38  14%      2  139   28    7  370%
c i   57.2   59374   395754     23996   13475   1124 131838   27   189   38  14%      2  139   27    8  364%
c i   57.2   59373   395754     24024   13497   1126 131841   27   189   38  14%      2  139   26    8  352%
c i   57.3   59372   395754     24053   13522   1127 131843   27   190   38  14%      2  139   26    8  341%
c i   57.6   59370   395754     24271   13724   1130 131850   28   192   38  14%      2  142   35    8  458%
c i   57.7   59369   395754     24379   13819   1130 131856   28   192   38  14%      2  141   32    8  415%
c i   57.9   59365   395754     24585   14005   1134 131860   29   194   38  15%      2  143   49    8  626%
c i   58.0   59364   395754     24677   14086   1137 131866   30   196   38  15%      2  145   46    8  588%
c i   58.3   59363   395754     24873   14270   1140 131871   29   194   38  15%      1  142   35    8  437%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   58.6   59318   395754     25218   14572   1153 131892   29   191   38  15%      2  138   29    8  362%
c i   58.6   59315   395754     25250   14602   1153 131892   29   191   38  15%      2  138   28    8  353%
c i   58.6   59314   395754     25267   14618   1153 131892   29   191   38  15%      2  138   29    8  362%
c i   59.0   59310   395754     25616   14949   1155 131901   29   190   39  15%      2  136   30    8  371%
c i   59.0   59309   395754     25617   14949   1155 131901   29   190   39  15%      2  136   30    8  370%
c i   59.0   59302   395754     25624   14953   1155 131903   29   190   39  15%      2  136   29    8  362%
c i   59.0   59297   395754     25626   14954   1155 131903   29   190   39  15%      2  136   29    8  359%
c i   59.5   59294   395754     26015   15321   1161 131911   30   188   40  16%      2  133   33    8  401%
c i   59.6   59289   395754     26097   15392   1164 131918   29   187   40  16%      2  132   29    8  353%
c i   59.7   59283   395754     26191   15479   1165 131922   29   187   40  16%      2  132   25    8  301%
c i   60.2   59280   395754     26687   15934   1184 131933   30   190   41  16%      2  134   33    9  390%
c i   60.2   59235   395754     26689   15935   1184 131933   30   190   41  16%      2  134   33    9  387%
c i   60.3   59234   395754     26738   15978   1184 131934   31   190   42  16%      2  134   38    9  442%
c i   61.0   59231   395754     27431   16629   1198 131950   31   191   42  16%      4  134   35    9  391%
c i   61.5   59230   395754     27860   17023   1205 131957   33   198   42  17%      3  140   52    9  564%
c i   61.8   59200   395754     28086   17231   1214 131960   33   199   42  17%      3  141   42    9  459%
c i   61.8   59199   395754     28091   17235   1214 131960   34   199   42  17%      3  141   46    9  497%
c i   62.3   59198   395754     28478   17567   1221 131981   35   196   42  18%      3  137   46    9  482%
c i   63.1   59196   395754     29138   18179   1235 131995   36   197   43  18%      4  137   41   10  413%
c i   63.3   59195   395754     29309   18335   1241 132002   36   200   43  18%      3  139   40   10  409%
c i   63.4   59194   395754     29353   18373   1242 132005   36   200   43  18%      3  139   36   10  368%
c i   63.5   59176   395754     29415   18429   1243 132006   36   201   43  18%      3  140   40   10  400%
c i   65.1   59175   395754     30857   19784   1273 132030   37   199   45  19%     10  134   29   11  278%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   65.2   59174   395754     30893   19817   1273 132031   37   201   45  19%     10  136   33   11  309%
c i   65.6   59173   395754     31239   20142   1277 132039   38   206   45  18%      8  140   37   11  342%
c i   65.7   59172   395754     31332   20227   1279 132041   38   205   45  18%      7  140   38   11  349%
c i   65.7   58986   395754     31341   20235   1279 132041   38   205   45  18%      7  139   37   11  339%
c i   65.9   58985   395754     31493   20378   1284 132043   37   205   45  18%      6  139   34   11  311%
c i   66.0   58984   395754     31592   20469   1287 132044   38   203   45  19%      5  137   37   11  342%
c i   66.6   58983   395754     32155   20982   1296 132058   37   197   46  19%      5  130   33   11  294%
c i   67.0   58982   395754     32494   21304   1301 132064   37   199   47  19%      4  131   39   11  346%
c i   67.6   58981   395754     32912   21686   1311 132066   38   199   47  19%      3  130   53   11  459%
c i   67.9   58980   395754     33150   21903   1314 132069   39   202   47  19%      3  133   47   12  405%
c i   69.4   58979   395754     34392   23049   1343 132093   41   207   48  20%      8  136   49   12  399%
c i   69.5   58978   395754     34442   23098   1343 132093   41   207   48  20%      8  136   49   12  401%
c i   69.8   58977   395754     34678   23303   1348 132095   43   209   49  21%      6  137   66   13  529%
c i   70.0   58976   395754     34883   23493   1350 132099   43   208   49  21%      5  135   50   13  392%
c i   70.2   58975   395754     35044   23632   1357 132102   43   207   49  21%      4  134   51   13  399%
c i   70.3   58974   395754     35120   23702   1357 132105   43   207   49  21%      4  134   44   13  342%
c i   70.3   58954   395754     35121   23702   1357 132105   43   207   49  21%      4  134   43   13  341%
c i   70.3   58952   395754     35122   23702   1357 132105   43   207   49  21%      4  134   43   13  340%
c i   70.8   58946   395754     35450   24016   1358 132112   42   205   50  20%      3  131   36   13  277%
c i   71.1   58945   395754     35690   24241   1360 132114   42   205   50  20%      3  131   37   13  290%
c i   71.7   58944   395754     36142   24666   1369 132123   42   206   50  20%      3  131   41   13  310%
c i   71.7   58943   395754     36143   24666   1369 132123   42   206   50  20%      3  130   41   13  309%
c i   72.1   58941   395754     36427   24925   1374 132132   42   204   50  20%      2  129   38   13  290%
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   72.1   58938   395754     36485   24975   1378 132135   42   207   50  20%      2  131   45   13  339%
c i   72.5   58937   395754     36800   25269   1386 132138   42   203   50  21%      2  126   39   13  294%
c i   72.7   58936   395754     36963   25420   1387 132144   42   203   50  21%      2  126   40   13  300%
c i   72.7   58934   395754     36978   25428   1388 132146   42   203   50  21%      2  126   39   13  292%
c i   73.5   58653   395754     37588   25979   1392 132164   45   206   52  22%      3  128   61   14  437%
c i   73.9   58652   395754     37926   26285   1399 132176   44   203   52  22%      2  124   41   14  294%
c i   74.7   58366   395754     38521   26829   1412 132184   48   210   52  23%      3  131   61   15  420%
c i   74.9   58365   395754     38687   26977   1414 132189   49   210   52  23%      2  130   67   15  452%
c i   75.3   58361   395754     39000   27267   1418 132190   51   211   52  24%      2  130   69   15  456%
c i   75.4   58360   395754     39103   27355   1423 132195   50   212   52  24%      2  131   58   15  383%
c 
c [simplification-11] limit 39205 conflicts (hard 49140) hit after 39206 conflicts
c [ternres-6] limit 13472654 with penalty 0 = 0 + 0
c [ternres-6] 4787 schedulable variables 8%
c [ternres-6] 92 ternary resolvents (0 bin, 92 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-24] removed 1107 variables
c [treelook-4] limit 673632 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 74627 literals 64%
c [treelook-4] scheduling used 673635 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 673632 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 791397 steps
c [treelook-4] 74526 literals remain 64%
c [treelook-4] 18228 variables remain to probed next time 31%
c [treelook-4] removed 62 variables, found 3336 hbrs
c [unhide-11] limit 1347265 with penalty 1 = 0 + 1
c [unhide-11-11] 5 units, 64 failed, 7712 tauts, 0 hbrs, 196010 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 240 transitive binary clauses
c [transred-7] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 58102 variables 100%
c [block-4] limit of 33681636 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 78 blocked clauses
c [block-4] 78 < 1/100 * 373550 = 3735 considered unsuccessful
c [bca-7] limit of 10000000 steps and 745396 added (scaled 2)
c [bca-7] 83539 out of 116204 literals actually usable 72%
c [bca-7] added 26 blocked clauses in 238612 steps
c [sweep-7] limit 4041796 penalty 0 = 0 + 0
c [sweep-7-1] 3494 pos 6.9% + 47282 neg 93.1% = 50776 sched 87.4% ret 7325
c [sweep-7-1] 4070184 steps 57 queries 5039.21 avg class size
c [sweep-7-1] 952 decisions 46 SAT calls 150.61 avg env size
c [sweep-7-1] 50232 variables remain 86% (7868 retained 14%)
c [decomp-26] removed 105 variables
c [sweep-7-1] removed 105 vars (0 failed, 10 eqs, 21 impls)
c [sweep-7] removed 105 vars in TOTAL (1 rounds, 56 queries)
c [phase-count-11] 368308 negative 99.0% of 372206 except 3898 1.0%
c [phase-count-11] 290665 positive 78.1% of 372206 except 81541 21.9%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-11] sorted 57996 enqueued variables after 39206 conflicts
c [score-dist-11] active 0 (0%), one 43681 (75%), zero 14315 (25%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 364 variables 0.6% (57996 remain 31%)
c [simplification-11] removed 23548 irredundant clauses 6.0% (372206 remain 37%)
c [simplification-11] maximum reduction of 6% = max (1%, 6%)
c [simplification-11] large reduction 6% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 51206 (soft 41206 + delta 10000)
c [simplification-11] new conflict limit 41206 (hard 51206)
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   79.4   57995   372206     39720   27562   1506 136704   50   212   59  24%      3  130   48   15  312%
c i   80.0   57994   372206     40195   27984   1520 136713   51   211   59  24%      3  128   57   16  365%
c i   81.2   57993   372206     41122   28836   1529 136729   51   210   59  24%      5  125   62   16  383%
c 
c [simplification-12] limit 41206 conflicts (hard 51206) hit after 41207 conflicts
c [quatres-7] found 27509 quaternary clauses 40% in total
c [quatres-7-1] removed 3 duplicate quaternary clauses
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [quatres-7-2] added 2 quaternary resolvents
c [ternres-7] limit 14102944 with penalty 0 = 0 + 0
c [ternres-7] all 57985 free variables schedulable
c [ternres-7] 120 ternary resolvents (0 bin, 120 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-27] removed 11 variables
c [basicprobe-4] limit 70514723 penalty 0 = 0 + 0
c [basicprobe-4-0] 19294 probes remain 34% after last round
c [basicprobe-4-0] 327 units = 327 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 623 variables, found 148676 hbrs
c [bate-3] eliminated 135 asymmetric tautologies during probing
c [unhide-12] limit 1410294 with penalty 1 = 0 + 1
c [unhide-12-12] 7 units, 328 failed, 21820 tauts, 0 hbrs, 60301 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 176 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 56920 variables 100%
c [elim-9] limit of 141029446 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 770 variables 1% in round 1 in 32703328 steps
c [elim-9-1] backward subsumption/strengthening limit 32703300
c [elim-9-1-1] backward checking 3904 touched variables 7%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 10 and strengthened 155 clauses in 1468302 steps
c [elim-9-1] rescheduled 365 variables 1% by backward subsumption
c [elim-9-2] eliminated 45 variables 0% in round 2 in 357968 steps
c [elim-9-2] backward subsumption/strengthening limit 357900
c [elim-9-2-1] backward checking 328 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 10 and strengthened 2 clauses in 230359 steps
c [elim-9-2] rescheduled 21 variables 0% by backward subsumption
c [elim-9-3] eliminated 1 variables 0% in round 3 in 69855 steps
c [elim-9-3] backward subsumption/strengthening limit 69800
c [elim-9-3-1] backward checking 10 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 1 and strengthened 1 clauses in 69801 steps
c [elim-9] incomplete 9 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 817 = 1% variables out of 56920 scheduled
c [bca-8] limit of 10000000 steps and 721867 added (scaled 2)
c [bca-8] 82108 out of 112208 literals actually usable 73%
c [bca-8] added 68 blocked clauses in 237039 steps
c [sweep-8] limit 4230883 penalty 0 = 0 + 0
c [sweep-8-1] 3750 pos 7.7% + 45060 neg 92.3% = 48810 sched 87.0% ret 7293
c [sweep-8-1] 4289155 steps 59 queries 4532.17 avg class size
c [sweep-8-1] 671 decisions 53 SAT calls 142.28 avg env size
c [sweep-8-1] 48229 variables remain 86% (7865 retained 14%)
c [decomp-28] removed 77 variables
c [sweep-8-1] removed 77 vars (0 failed, 5 eqs, 9 impls)
c [sweep-8] removed 77 vars in TOTAL (1 rounds, 58 queries)
c [phase-count-12] 356671 negative 99.0% of 360398 except 3727 1.0%
c [phase-count-12] 278613 positive 77.3% of 360398 except 81785 22.7%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 56026 enqueued variables after 41207 conflicts
c [score-dist-12] active 0 (0%), one 42687 (76%), zero 13339 (24%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 1959 variables 3.4% (56026 remain 30%)
c [simplification-12] removed 11808 irredundant clauses 3.2% (360398 remain 36%)
c [simplification-12] maximum reduction of 3% = max (3%, 3%)
c [simplification-12] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-12] new conflict interval 23000
c [simplification-12] penalized conflict interval 23000 = 1 * 23000
c [simplification-12] hard conflict limit 75707 (soft 64207 + delta 11500)
c [simplification-12] new conflict limit 64207 (hard 75707)
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   89.4   56025   360398     41995   23840   1603 251133   49   206   53  24%      6  119   52   16  314%
c i   90.0   56024   360398     42416   24228   1611 251138   49   205   53  24%      4  118   44   17  267%
c i   92.4   56019   360398     44322   26012   1640 251175   49   201   53  24%     15  110   39   18  221%
c i   92.9   56018   360398     44657   26305   1641 251181   50   202   53  25%     11  111   54   18  304%
c i   93.3   56017   360398     44962   26591   1647 251185   51   204   53  25%      9  112   60   18  330%
c i   93.8   56016   360398     45356   26958   1653 251195   51   205   53  25%      6  112   56   18  307%
c i   93.8   55990   360398     45357   26958   1653 251195   51   205   53  25%      6  112   56   18  306%
c i   93.9   55989   360398     45420   27015   1653 251198   51   208   53  25%      6  115   58   18  319%
c i   94.2   55988   360398     45714   27284   1656 251204   51   206   53  25%      4  113   59   18  318%
c i   94.5   55987   360398     45894   27437   1656 251209   52   205   53  25%      4  112   61   19  328%
c i   94.6   55225   360398     45948   27488   1656 251210   52   205   53  25%      3  112   59   19  316%
c i   95.2   55221   360398     46441   27949   1662 251222   51   201   53  25%      3  107   44   19  234%
c i   95.4   55220   360398     46592   28080   1666 251227   51   201   53  25%      2  106   50   19  268%
c i   96.4   55219   360398     47293   28718   1683 251240   50   200   53  25%      3  104   46   19  238%
c i   96.7   55218   360398     47477   28893   1685 251241   50   200   53  25%      3  104   41   19  214%
c i   96.9   55217   360398     47659   29063   1688 251243   50   199   53  25%      2  103   44   19  227%
c i   98.0   55216   360398     48478   29816   1700 251261   49   196   54  25%      4   99   50   20  254%
c i   98.0   55215   360398     48479   29816   1700 251261   49   196   54  25%      4   99   50   20  253%
c i   98.1   55212   360398     48548   29877   1701 251261   49   196   54  25%      3   98   53   20  268%
c i   98.7   55211   360398     49037   30323   1707 251278   49   195   54  25%      3   97   40   20  202%
c i   98.8   54963   360398     49114   30395   1707 251279   50   197   54  25%      3   98   51   20  258%
c i   99.0   54962   360398     49206   30471   1709 251281   50   197   54  25%      2   99   55   20  276%
c i   99.0   54959   360398     49263   30521   1710 251282   50   196   54  25%      2   97   50   20  249%
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   99.6   54958   360398     49677   30893   1722 251289   52   200   54  26%      2  100   65   20  321%
c i   99.9   54957   360398     49946   31136   1725 251294   52   197   54  26%      1   97   56   20  273%
c i   99.9   54956   360398     49954   31143   1725 251294   52   197   54  26%      1   97   55   20  267%
c i   99.9   54953   360398     49955   31143   1725 251294   52   196   54  26%      1   97   54   20  266%
c i  100.3   54952   360398     50342   31493   1732 251299   51   199   55  26%      1   99   51   21  248%
c i  100.5   54951   360398     50519   31651   1734 251313   50   196   55  26%      1   96   39   21  190%
c i  100.6   54950   360398     50659   31784   1734 251315   50   197   55  25%      1   96   38   21  186%
c i  100.8   54949   360398     50823   31935   1739 251318   49   196   55  25%      0   95   36   21  175%
c i  100.9   54941   360398     50892   31992   1743 251323   49   195   55  25%      0   94   40   21  192%
c i  101.3   54940   360398     51264   32335   1751 251325   50   198   56  25%      1   97   47   21  226%
c i  101.3   54939   360398     51310   32378   1751 251326   49   198   56  25%      0   97   45   21  214%
c i  101.5   54938   360398     51451   32516   1751 251327   51   203   58  25%      0  101   68   21  322%
c i  102.1   54937   360398     52021   33032   1760 251334   53   209   59  25%      1  107   71   21  330%
c i  103.2   54936   360398     52884   33828   1773 251343   53   208   59  25%      4  104   50   22  230%
c i  103.7   54935   360398     53296   34212   1777 251346   54   205   65  26%      3  100   57   22  257%
c i  103.9   54934   360398     53425   34316   1778 251349   54   204   65  27%      2   99   63   22  285%
c i  104.5   54933   360398     54098   34929   1790 251365   52   200   65  26%      3   94   47   22  211%
c i  104.8   54932   360398     54267   35092   1791 251366   53   204   65  26%      2   98   62   23  273%
c i  104.9   54931   360398     54335   35155   1791 251367   53   204   65  26%      2   98   58   23  255%
c i  104.9   54929   360398     54336   35155   1791 251367   53   204   65  26%      2   98   57   23  254%
c i  105.4   54917   360398     54906   35672   1803 251379   54   210   65  26%      2  103   55   23  239%
c i  106.1   54916   360398     55497   36221   1808 251383   54   208   65  26%      3  100   60   23  260%
c i  106.1   54915   360398     55506   36228   1808 251384   54   208   65  26%      2  100   59   23  253%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  106.9   54803   360398     56177   36838   1817 251393   58   218   65  26%      3  109   83   24  348%
c i  107.8   54802   360398     56881   37480   1822 251408   59   218   70  27%      3  108   57   24  237%
c i  108.4   54801   360398     57378   37936   1824 251412   60   222   70  27%      3  111   62   25  250%
c i  108.5   54800   360398     57451   38007   1824 251412   60   221   70  27%      2  110   59   25  241%
c i  109.2   54799   360398     58026   38518   1830 251420   59   216   71  27%      2  104   52   25  211%
c i  109.4   54798   360398     58176   38647   1834 251425   60   215   71  28%      2  103   63   25  252%
c i  109.5   54797   360398     58345   38801   1837 251434   58   210   71  28%      2   98   44   25  175%
c i  109.8   54796   360398     58615   39034   1847 251446   57   207   71  27%      1   94   38   25  153%
c i  110.5   54794   360398     59183   39553   1859 251451   55   200   71  27%      2   86   44   25  176%
c i  111.5   54793   360398     59921   40234   1861 251454   57   203   72  28%      3   88   71   26  276%
c i  111.7   54792   360398     60069   40374   1863 251456   56   198   72  28%      2   84   48   26  186%
c i  112.4   54791   360398     60563   40831   1870 251461   58   200   72  29%      2   85   63   26  243%
c i  112.9   54790   360398     60997   41197   1882 251471   58   200   72  29%      2   84   55   26  212%
c i  114.4   54789   360398     62271   42320   1896 251492   60   210   72  29%      7   92   58   27  217%
c i  114.4   54758   360398     62281   42326   1898 251493   60   209   72  29%      7   92   56   27  209%
c i  115.9   54610   360398     63477   43378   1923 251512   61   211   74  29%      8   91   53   28  193%
c i  116.2   54609   360398     63603   43493   1923 251512   62   213   74  29%      7   93   72   28  261%
c i  116.8   54608   360398     64022   43875   1925 251518   66   220   74  30%      5  100  103   28  365%
c i  117.0   54607   360398     64183   44015   1927 251519   66   219   74  30%      4   98   85   28  300%
c i  117.1   54601   360398     64250   44076   1927 251521   65   219   74  30%      4   98   77   28  273%
c 
c [simplification-13] limit 64250 conflicts (hard 75707) hit after 64250 conflicts
c [quatres-8] found 27098 quaternary clauses 43% in total
c [quatres-8-2] added 1 single-self-subsuming ternary resolvents
c [ternres-8] limit 21069187 with penalty 0 = 0 + 0
c [ternres-8] all 54601 free variables schedulable
c [ternres-8] 266 ternary resolvents (0 bin, 266 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-29] removed 1509 variables
c [simpleprobe-5] all 54517 free variables schedulable
c [simpleprobe-5] limit 84276751 penalty 0 = 0 + 0
c [decomp-30] removed 652 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 652 variables, found 40082 hbrs, 346 units
c [unhide-13] limit 2106918 with penalty 1 = 0 + 1
c [unhide-13-13] 1 units, 24 failed, 8136 tauts, 0 hbrs, 231935 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 252 transitive binary clauses
c [transred-9] found 3 units
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 53776 variables 100%
c [elim-10] limit of 421383756 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 1047 variables 2% in round 1 in 28739591 steps
c [elim-10-1] backward subsumption/strengthening limit 28739500
c [elim-10-1-1] backward checking 4508 touched variables 8%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 29 and strengthened 31 clauses in 1493215 steps
c [elim-10-1] rescheduled 155 variables 0% by backward subsumption
c [elim-10-2] eliminated 11 variables 0% in round 2 in 145564 steps
c [elim-10-2] backward subsumption/strengthening limit 145500
c [elim-10-2-1] backward checking 125 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 9 and strengthened 0 clauses in 133908 steps
c [elim-10-2] rescheduled 7 variables 0% by backward subsumption
c [elim-10-3] eliminated 1 variables 0% in round 3 in 21480 steps
c [elim-10-3] backward subsumption/strengthening limit 21400
c [elim-10-3-1] backward checking 21 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 0 and strengthened 0 clauses in 21401 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 1059 = 2% variables out of 53776 scheduled
c [bca-9] limit of 10000000 steps and 672027 added (scaled 2)
c [bca-9] 73883 out of 105436 literals actually usable 70%
c [bca-9] added 31 blocked clauses in 211609 steps
c [sweep-9] limit 6320756 penalty 0 = 0 + 0
c [sweep-9-1] 3202 pos 7.0% + 42287 neg 93.0% = 45489 sched 86.3% ret 7228
c [sweep-9-1] 6348449 steps 71 queries 3723.68 avg class size
c [sweep-9-1] 1402 decisions 64 SAT calls 168.30 avg env size
c [sweep-9-1] 44777 variables remain 85% (7930 retained 15%)
c [decomp-31] removed 25 variables
c [sweep-9-1] removed 25 vars (0 failed, 8 eqs, 17 impls)
c [sweep-9] 25 < 1/1000 * 52717 = 52 considered unsuccessful
c [sweep-9] removed 25 vars in TOTAL (1 rounds, 70 queries)
c [phase-count-13] 332033 negative 99.0% of 335514 except 3481 1.0%
c [phase-count-13] 259077 positive 77.2% of 335514 except 76437 22.8%
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 52692 enqueued variables after 64250 conflicts
c [score-dist-13] active 0 (0%), one 41582 (79%), zero 11110 (21%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 1909 variables 3.5% (52692 remain 28%)
c [simplification-13] removed 24884 irredundant clauses 6.9% (335514 remain 34%)
c [simplification-13] maximum reduction of 7% = max (3%, 7%)
c [simplification-13] large reduction 7% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 76250 (soft 66250 + delta 10000)
c [simplification-13] new conflict limit 66250 (hard 76250)
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  123.0   52691   335514     64349   28424   2063 264303   65   220   54  29%      3   99   65   28  231%
c i  123.9   52690   335514     65238   29246   2075 264314   60   212   54  28%      4   90   52   28  182%
c 
c [simplification-14] limit 66250 conflicts (hard 76250) hit after 66251 conflicts
c [quatres-9] found 26781 quaternary clauses 42% in total
c [quatres-9-1] removed 2 duplicate quaternary clauses
c [quatres-9-2] added 5 quaternary resolvents
c [ternres-9] limit 21585421 with penalty 0 = 0 + 0
c [ternres-9] all 52690 free variables schedulable
c [ternres-9] 270 ternary resolvents (0 bin, 270 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 539635 penalty 3 = 3 + 0
c [gauss-4] extracted 12 xors of average arity 3.0
c [gauss-4] connected 36 occurrences of 33 variables (average 1.1)
c [gauss-4] limit 539635 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 3 variables
c [treelook-5] limit 2158542 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 86843 literals 82%
c [treelook-5] scheduling used 1366600 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2158542 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2167839 steps
c [treelook-5] 86803 literals remain 82%
c [treelook-5] 15313 variables remain to probed next time 29%
c [treelook-5] removed 1 variables, found 9911 hbrs
c [unhide-14] limit 4317084 with penalty 0 = 0 + 0
c [unhide-14-15] 9 units, 187 failed, 24858 tauts, 0 hbrs, 108367 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 168 transitive binary clauses
c [transred-10] found 3 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 134908885 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 14
c [cce-4-1] eliminated 1 clauses out of 167 (1%) of length 10
c [cce-4-1] eliminated 2 clauses out of 329 (1%) of length 8
c [cce-4-1] eliminated 19 clauses out of 594 (3%) of length 7
c [cce-4-1] eliminated 2057 clauses out of 4035 (51%) of length 6
c [cce-4-1] eliminated 9053 clauses out of 24589 (37%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 11133 large clauses in 134908893 steps
c [cce-4-1] allowing another 67454446 steps for small clauses
c [cce-4-1] scheduling 196685 clauses = 177355 binary + 19330 ternary
c [cce-4-1] tried to eliminate 3064 small clauses 2%
c [cce-4-1] eliminated 651 binary clauses 0%
c [cce-4-1] eliminated 170 ternary clauses 1%
c [cce-4-1] eliminated 821 small clauses 0%
c [cce-4-1] eliminated 964 small clauses in 134908889 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 12097 covered clauses in round 1
c [cce-4] eliminated 12097 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 52450 variables 100%
c [elim-11] limit of 431708435 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 5967 variables 11% in round 1 in 26439862 steps
c [elim-11-1] backward subsumption/strengthening limit 26439800
c [elim-11-1-1] backward checking 15726 touched variables 30%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 12 and strengthened 20 clauses in 2927322 steps
c [elim-11-1] rescheduled 80 variables 0% by backward subsumption
c [elim-11-2] eliminated 6 variables 0% in round 2 in 50701 steps
c [elim-11-2] backward subsumption/strengthening limit 50700
c [elim-11-2-1] backward checking 57 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 0 and strengthened 5 clauses in 50701 steps
c [elim-11-2] rescheduled 19 variables 0% by backward subsumption
c [elim-11-3] eliminated 1 variables 0% in round 3 in 20323 steps
c [elim-11-3] backward subsumption/strengthening limit 20300
c [elim-11-3-1] backward checking 14 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 0 and strengthened 2 clauses in 20301 steps
c [elim-11] incomplete 8 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 5980 = 11% variables out of 52450 scheduled
c [bca-10] limit of 10000000 steps and 611197 added (scaled 2)
c [bca-10] 73694 out of 92942 literals actually usable 79%
c [bca-10] added 231 blocked clauses in 198695 steps
c [phase-count-14] 304261 negative 99.7% of 305193 except 932 0.3%
c [phase-count-14] 231200 positive 75.8% of 305193 except 73993 24.2%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-14] sorted 46470 enqueued variables after 66251 conflicts
c [score-dist-14] active 0 (0%), one 36322 (78%), zero 10148 (22%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 6220 variables 11.8% (46470 remain 25%)
c [simplification-14] removed 30321 irredundant clauses 9.0% (305193 remain 31%)
c [simplification-14] maximum reduction of 12% = max (12%, 9%)
c [simplification-14] large reduction 12% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 78251 (soft 68251 + delta 10000)
c [simplification-14] new conflict limit 68251 (hard 78251)
c 
c [simplification-15] limit 68251 conflicts (hard 78251) hit after 68252 conflicts
c [quatres-10] found 30120 quaternary clauses 56% in total
c [quatres-10-2] added 1 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1 quaternary resolvents
c [ternres-10] limit 21931670 with penalty 0 = 0 + 0
c [ternres-10] all 46470 free variables schedulable
c [ternres-10] 131 ternary resolvents (0 bin, 131 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 685364 penalty 4 = 4 + 0
c [card-5] found 1769 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 685364 for elimination
c [card-5] 1769 out of 1769 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-34] removed 3 variables
c [basicprobe-5] limit 109658353 penalty 0 = 0 + 0
c [basicprobe-5-0] 11032 probes remain 24% after last round
c [basicprobe-5-0] 472 units = 469 failed (99%) + 3 lifted (1%)
c [basicprobe-5-0] removed 1030 variables, found 242391 hbrs
c [bate-4] eliminated 534 asymmetric tautologies during probing
c [unhide-15] limit 4386334 with penalty 0 = 0 + 0
c [unhide-15-17] 13 units, 149 failed, 38198 tauts, 0 hbrs, 31699 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 173 transitive binary clauses
c [transred-11] found 3 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 45337 variables 100%
c [block-5] limit of 27414588 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 89 blocked clauses
c [block-5] 89 < 1/100 * 292365 = 2923 considered unsuccessful
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 45337 variables 100%
c [elim-12] limit of 438633413 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 560 variables 1% in round 1 in 23549987 steps
c [elim-12-1] backward subsumption/strengthening limit 23549900
c [elim-12-1-1] backward checking 3316 touched variables 7%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 30 and strengthened 45 clauses in 1009024 steps
c [elim-12-1] rescheduled 164 variables 0% by backward subsumption
c [elim-12-2] eliminated 18 variables 0% in round 2 in 201324 steps
c [elim-12-2] backward subsumption/strengthening limit 201300
c [elim-12-2-1] backward checking 143 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 10 and strengthened 7 clauses in 123398 steps
c [elim-12-2] rescheduled 30 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 179154 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 581 = 1% variables out of 45337 scheduled
c [bca-11] limit of 10000000 steps and 581008 added (scaled 2)
c [bca-11] 69704 out of 89514 literals actually usable 78%
c [bca-11] added 67 blocked clauses in 184689 steps
c [sweep-10] limit 3289750 penalty 1 = 1 + 0
c [sweep-10-1] 3514 pos 9.1% + 35175 neg 90.9% = 38689 sched 86.4% ret 6067
c [sweep-10-1] 3328943 steps 77 queries 3222.61 avg class size
c [sweep-10-1] 801 decisions 74 SAT calls 78.09 avg env size
c [sweep-10-1] 37614 variables remain 84% (7135 retained 16%)
c [decomp-35] removed 53 variables
c [sweep-10-1] removed 53 vars (0 failed, 3 eqs, 10 impls)
c [sweep-10] removed 53 vars in TOTAL (1 rounds, 76 queries)
c [phase-count-15] 288983 negative 99.7% of 289845 except 862 0.3%
c [phase-count-15] 216932 positive 74.8% of 289845 except 72913 25.2%
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 44703 enqueued variables after 68252 conflicts
c [score-dist-15] active 0 (0%), one 35860 (80%), zero 8843 (20%)
c [score-dist-15] max exp 1, different 2 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 1767 variables 3.8% (44703 remain 24%)
c [simplification-15] removed 15348 irredundant clauses 5.0% (289845 remain 29%)
c [simplification-15] maximum reduction of 5% = max (4%, 5%)
c [simplification-15] large reduction 5% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 80252 (soft 70252 + delta 10000)
c [simplification-15] new conflict limit 70252 (hard 80252)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  142.5   44702   289845     68981   12341   2557 421584   36   160   38  22%     39   35   13   28   48%
c i  142.9   44701   289845     69835   13114   2572 421607   33   153   38  22%     19   27   27   28   97%
c i  143.0   44700   289845     69905   13180   2573 421607   34   153   38  22%     18   27   30   28  106%
c 
c [simplification-16] limit 70252 conflicts (hard 80252) hit after 70253 conflicts
c [quatres-11] found 29577 quaternary clauses 57% in total
c [quatres-11-2] added 3 single-self-subsuming ternary resolvents
c [quatres-11-2] added 2 quaternary resolvents
c [ternres-11] limit 22227863 with penalty 0 = 0 + 0
c [ternres-11] all 44700 free variables schedulable
c [ternres-11] 282 ternary resolvents (0 bin, 282 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-36] removed 3 variables
c [simpleprobe-6] all 44700 free variables schedulable
c [simpleprobe-6] limit 88911452 penalty 0 = 0 + 0
c [decomp-37] removed 278 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 278 variables, found 54281 hbrs, 147 units
c [unhide-16] limit 4445572 with penalty 0 = 0 + 0
c [unhide-16-19] 7 units, 39 failed, 32510 tauts, 0 hbrs, 49932 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 319 transitive binary clauses
c [cce-5] limit of 27784829 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 10 clauses out of 251 (4%) of length 7
c [cce-5-1] eliminated 41 clauses out of 2354 (2%) of length 6
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 51 large clauses in 27784832 steps
c [cce-5-1] allowing another 13892416 steps for small clauses
c [cce-5-1] scheduling 171198 clauses = 152467 binary + 18731 ternary
c [cce-5-1] tried to eliminate 857 small clauses 1%
c [cce-5-1] eliminated 200 binary clauses 0%
c [cce-5-1] eliminated 39 ternary clauses 0%
c [cce-5-1] eliminated 239 small clauses 0%
c [cce-5-1] eliminated 310 small clauses in 27784829 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 361 covered clauses in round 1
c [cce-5] eliminated 361 covered clauses in TOTAL during 1 rounds
c [cce-5] 361 < 1/100 * 286328 = 2863 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 44379 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 410 variables 1% in round 1 in 22921712 steps
c [elim-13-1] backward subsumption/strengthening limit 22921700
c [elim-13-1-1] backward checking 2014 touched variables 5%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 19 and strengthened 53 clauses in 647796 steps
c [elim-13-1] rescheduled 149 variables 0% by backward subsumption
c [elim-13-2] eliminated 23 variables 0% in round 2 in 164861 steps
c [elim-13-2] backward subsumption/strengthening limit 164800
c [elim-13-2-1] backward checking 162 touched variables 0%
c [elim-13-2-1] incomplete backward checking 0 remain 0%
c [elim-13-2] subsumed 11 and strengthened 2 clauses in 164801 steps
c [elim-13-2] rescheduled 24 variables 0% by backward subsumption
c [elim-13-3] eliminated 4 variables 0% in round 3 in 355622 steps
c [elim-13-3] backward subsumption/strengthening limit 355600
c [elim-13-3-1] backward checking 35 touched variables 0%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 7 and strengthened 3 clauses in 89275 steps
c [elim-13] incomplete 13 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 441 = 1% variables out of 44379 scheduled
c [elim-13] 441 < 1/100 * 44379 = 443 considered unsuccessful
c [bca-12] limit of 10000000 steps and 570120 added (scaled 2)
c [bca-12] 66880 out of 87878 literals actually usable 76%
c [bca-12] added 50 blocked clauses in 174785 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 66683580 penalty 0 = 0 + 0
c [sweep-11-1] 3335 pos 9.0% + 33690 neg 91.0% = 37025 sched 84.3% ret 6913
c [sweep-11-1] 66752327 steps 1243 queries 164.65 avg class size
c [sweep-11-1] 11563 decisions 1141 SAT calls 106.04 avg env size
c [sweep-11-1] 18990 variables remain 43% (24824 retained 57%)
c [decomp-38] removed 527 variables
c [sweep-11-1] removed 527 vars (0 failed, 127 eqs, 215 impls)
c [sweep-11] removed 527 vars in TOTAL (1 rounds, 1242 queries)
c [sort-queue-16] sorted 43411 enqueued variables after 70253 conflicts
c [score-dist-16] active 0 (0%), one 35274 (81%), zero 8137 (19%)
c [score-dist-16] max exp 1, different 2 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 1289 variables 2.9% (43411 remain 23%)
c [simplification-16] removed 6522 irredundant clauses 2.3% (283323 remain 28%)
c [simplification-16] maximum reduction of 3% = max (3%, 2%)
c [simplification-16] geometric conflict interval increment 5750 = 23000 / 4
c [simplification-16] new conflict interval 28750
c [simplification-16] penalized conflict interval 28750 = 1 * 28750
c [simplification-16] hard conflict limit 113378 (soft 99003 + delta 14375)
c [simplification-16] new conflict limit 99003 (hard 113378)
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  152.0   43410   283323     70656   13233   2733 496985   32   158   41  20%     10   31   19   28   69%
c i  152.1   43409   283323     70824   13382   2740 496987   31   156   41  20%      8   30   16   28   57%
c i  155.1   43393   283323     75698   17968   2793 497034   25   124   48  21%     55   -4   13   28   48%
c i  155.6   43392   283323     76715   18900   2822 497049   25   121   50  21%     22   -7   23   28   82%
c i  156.3   43391   283323     77580   19720   2828 497052   28   133   50  21%     10    5   46   28  167%
c i  157.6   43389   283323     79414   21448   2853 497074   27   117   54  23%     11  -10   27   28   96%
c i  157.9   43386   283323     79733   21749   2857 497076   29   123   54  24%      7   -4   41   28  146%
c i  158.6   43385   283323     81374   23258   2878 497094   25   104   57  24%      9  -23   17   28   61%
c i  158.7   43384   283323     81643   23497   2880 497101   25   100   57  25%      6  -28   19   28   67%
c i  160.4   43383   283323     83908   25617   2906 497125   26   124   64  21%     15   -3   38   28  139%
c i  160.8   43381   283323     84436   26124   2909 497127   26   123   64  21%      8   -4   23   28   84%
c i  161.9   43380   283323     85994   27606   2921 497135   25   107   67  23%      8  -20   22   27   82%
c i  161.9   43379   283323     86076   27681   2923 497138   25   107   67  23%      7  -20   22   27   79%
c i  164.2   43378   283323     88703   30163   2939 497152   26   105   70  24%     20  -21   17   27   63%
c i  165.1   43377   283323     89814   31206   2957 497164   29   118   70  25%      8   -8   32   28  116%
c i  165.3   43376   283323     90054   31424   2960 497164   30   119   70  25%      5   -6   34   28  122%
c i  165.5   43375   283323     90323   31682   2961 497165   29   116   73  25%      3   -9   24   28   85%
c i  165.8   43374   283323     90648   31981   2965 497168   30   119   73  25%      0   -7   35   28  127%
c i  166.0   43308   283323     90959   32272   2969 497170   29   116   75  25%     -1  -10   29   28  103%
c i  167.3   43307   283323     92410   33616   2991 497183   31   126   75  25%      4    0   22   28   79%
c i  167.6   43306   283323     92828   33997   2996 497188   32   124   75  26%      1   -2   47   28  169%
c i  167.7   43305   283323     93030   34175   2997 497193   33   125   78  26%     -0   -1   53   28  188%
c i  168.6   43304   283323     94222   35255   3014 497211   32   119   79  27%      2   -7   34   28  122%
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  168.8   43303   283323     94349   35364   3015 497211   34   121   79  28%      1   -5   53   28  189%
c i  169.1   43104   283323     94700   35698   3018 497214   33   124   79  27%     -1   -2   34   28  122%
c i  170.7   43103   283323     96492   37358   3031 497240   33   125   81  26%      8   -1   27   28   97%
c i  171.5   43102   283323     97645   38424   3049 497253   33   118   84  28%      4   -7   44   28  157%
c i  172.3   43101   283323     98580   39306   3057 497266   35   127   84  27%      2    2   48   29  167%
c i  172.5   43100   283323     98787   39499   3058 497267   36   130   84  28%      0    4   53   29  186%
c i  172.5   43098   283323     98788   39499   3058 497267   36   129   84  28%      0    4   53   29  186%
c i  173.0   43097   283323     99264   39966   3059 497267   36   135   84  27%     -1   10   40   29  140%
c i  173.9   43096   283323    100335   40958   3068 497273   33   122   84  27%      1   -4   21   29   74%
c i  174.4   43095   283323    100871   41465   3068 497278   31   111   84  28%     -1  -15   16   29   56%
c i  175.1   43094   283323    101742   42275   3076 497282   35   109   91  32%     -1  -16   81   29  282%
c i  175.8   43093   283323    102467   42962   3080 497286   35   114   91  31%     -1  -11   40   29  139%
c i  176.1   43090   283323    102788   43250   3087 497289   36   116   91  31%     -2   -9   45   29  155%
c i  176.9   43089   283323    103628   44025   3106 497298   37   121   91  30%     -1   -4   33   29  114%
c i  176.9   43048   283323    103629   44025   3106 497298   37   121   91  30%     -1   -4   33   29  113%
c i  176.9   43045   283323    103630   44025   3106 497298   37   121   91  30%     -1   -4   33   29  113%
c i  177.6   43044   283323    104340   44690   3119 497305   36   123   91  29%     -2   -2   31   29  106%
c i  177.8   42735   283323    104516   44844   3119 497305   37   125   91  30%     -2   -0   50   29  170%
c i  178.3   42734   283323    105031   45325   3124 497313   38   129   91  29%     -3    4   51   29  172%
c 
c [simplification-17] limit 99033 conflicts (hard 113378) hit after 106069 conflicts
c [quatres-12] found 26364 quaternary clauses 52% in total
c [quatres-12-2] added 1 single-self-subsuming ternary resolvents
c [quatres-12-2] added 2 quaternary resolvents
c [ternres-12] limit 29671279 with penalty 0 = 0 + 0
c [ternres-12] all 42734 free variables schedulable
c [ternres-12] 225 ternary resolvents (0 bin, 225 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-39] removed 705 variables
c [treelook-6] limit 2967127 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 68468 literals 80%
c [treelook-6] scheduling used 1521799 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 2967127 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 3144592 steps
c [treelook-6] 68436 literals remain 80%
c [treelook-6] 10777 variables remain to probed next time 25%
c [treelook-6] removed 1 variables, found 17414 hbrs
c [unhide-17] limit 1483563 with penalty 2 = 0 + 2
c [unhide-17-20] 3 units, 25 failed, 2688 tauts, 0 hbrs, 858562 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 197 transitive binary clauses
c [transred-13] found 2 units
c [bca-13] limit of 10000000 steps and 547911 added (scaled 2)
c [bca-13] 55865 out of 85290 literals actually usable 66%
c [bca-13] added 9 blocked clauses in 174908 steps
c [sweep-12] limit 8901383 penalty 0 = 0 + 0
c [sweep-12-1] 2097 pos 11.3% + 16406 neg 88.7% = 18503 sched 43.4% ret 24141
c [sweep-12-1] 8956872 steps 157 queries 832.04 avg class size
c [sweep-12-1] 3190 decisions 142 SAT calls 288.06 avg env size
c [sweep-12-1] 17649 variables remain 41% (24988 retained 59%)
c [decomp-41] removed 39 variables
c [sweep-12-1] removed 39 vars (0 failed, 19 eqs, 27 impls)
c [sweep-12] 39 < 1/1000 * 42644 = 42 considered unsuccessful
c [sweep-12] removed 39 vars in TOTAL (1 rounds, 156 queries)
c [sort-queue-17] sorted 42605 enqueued variables after 106069 conflicts
c [score-dist-17] active 0 (0%), one 35568 (83%), zero 7037 (17%)
c [score-dist-17] max exp 1, different 2 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 129 variables 0.3% (42605 remain 23%)
c [simplification-17] removed 9966 irredundant clauses 3.5% (273357 remain 27%)
c [simplification-17] maximum reduction of 4% = max (0%, 4%)
c [simplification-17] geometric conflict interval increment 5750 = 28750 / 5
c [simplification-17] new conflict interval 34500
c [simplification-17] penalized conflict interval 34500 = 1 * 34500
c [simplification-17] hard conflict limit 157819 (soft 140569 + delta 17250)
c [simplification-17] new conflict limit 140569 (hard 157819)
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  184.5   42604   273357    106183   45950   3257 511738   40   135  102  29%      1   10   43   30  146%
c i  184.9   42555   273357    106496   46222   3261 511742   41   141  105  29%     -1   16   61   30  206%
c i  185.2   42554   273357    106750   46437   3262 511744   42   141  105  30%     -2   16   56   30  189%
c i  185.3   42553   273357    106874   46552   3267 511746   41   140  105  29%     -2   15   41   30  136%
c i  185.4   42552   273357    106940   46608   3272 511746   41   142  105  29%     -3   16   40   30  133%
c i  185.4   42476   273357    106946   46612   3272 511746   41   142  105  29%     -3   16   39   30  132%
c i  186.5   42475   273357    108200   47799   3284 511753   39   144  105  27%      2   19   41   30  137%
c i  188.0   42474   273357    109586   49131   3292 511759   39   139  105  28%      4   13   35   30  116%
c i  188.3   42473   273357    109836   49364   3294 511761   38   137  105  28%      2   11   33   30  110%
c i  189.1   42464   273357    110702   50178   3298 511777   38   136  105  27%      1   10   34   30  113%
c i  189.7   42463   273357    111491   50911   3308 511787   36   140  105  25%     -0   14   23   30   78%
c i  192.8   42462   273357    114555   53767   3332 511807   41   147  105  28%     25   20   33   31  106%
c i  195.5   42461   273357    117300   56385   3350 511826   33   101  105  32%     21  -26   33   31  107%
c i  197.1   42456   273357    118784   57766   3375 511836   34   107  105  32%      9  -19   41   31  135%
c i  197.5   42455   273357    119192   58140   3376 511840   36   110  105  33%      4  -16   64   31  208%
c i  199.1   42454   273357    120608   59453   3389 511849   39   119  106  33%      4   -7   43   31  139%
c i  199.8   42453   273357    121271   60041   3398 511855   41   124  106  33%      1   -2   55   31  177%
c -  201.2   42453   273357    122452   25854   3416 511875   44   135   45  32%      1    9   62   32  194%
c i  203.8   42452   273357    125545   28732   3451 511905   40   125   55  32%     41   -2   45   32  140%
c i  204.8   42451   273357    126660   29751   3457 511910   41   124   56  33%     14   -3   55   32  171%
c i  205.6   42450   273357    127631   30614   3468 511919   44   128   56  34%      4    2   63   33  194%
c i  206.9   42449   273357    129144   31999   3488 511933   42   127   58  33%      4   -0   37   33  115%
c i  207.0   42448   273357    129267   32112   3490 511935   41   125   58  33%      2   -1   34   33  104%
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  207.1   42447   273357    129464   32297   3492 511936   41   123   59  34%      0   -3   40   33  123%
c i  207.8   42446   273357    130165   32949   3507 511945   45   134   60  33%     -2    8   61   33  185%
c i  207.8   42425   273357    130166   32949   3507 511945   45   134   60  33%     -2    8   61   33  184%
c i  207.8   42423   273357    130167   32949   3507 511945   45   134   60  33%     -2    8   60   33  183%
c i  207.8   42406   273357    130168   32949   3507 511945   45   134   60  33%     -2    8   60   33  183%
c i  207.8   42403   273357    130169   32949   3507 511945   45   134   60  33%     -2    8   60   33  182%
c i  208.2   42402   273357    130619   33357   3511 511949   45   135   60  33%     -4    8   52   33  156%
c i  208.7   42401   273357    131242   33911   3520 511960   45   136   60  33%     -4    9   50   33  150%
c i  210.4   42400   273357    133189   35701   3539 511981   42   124   63  34%      7   -3   40   33  121%
c i  212.4   42399   273357    135388   37717   3556 511992   43   113   65  38%     12  -13   58   34  173%
c i  212.5   42398   273357    135459   37779   3558 511993   43   114   65  38%     10  -12   61   34  180%
c i  212.6   42397   273357    135532   37848   3558 511993   43   115   65  38%      9  -12   61   34  180%
c i  212.7   42396   273357    135636   37919   3558 511994   45   117   65  38%      7   -9   72   34  212%
c i  213.1   42395   273357    136061   38304   3564 511998   46   125   65  37%      2   -1   61   34  181%
c i  214.4   42394   273357    137565   39649   3585 512015   44   127   68  34%      3    1   25   34   74%
c i  214.5   42386   273357    137687   39759   3585 512022   43   125   68  34%      2   -1   24   34   71%
c i  214.6   42385   273357    137939   40004   3586 512022   43   125   68  34%     -0   -2   33   34   97%
c i  215.8   42384   273357    139191   41149   3590 512028   42   120   73  35%      1   -6   37   34  108%
c i  216.4   42381   273357    139843   41755   3595 512033   41   122   73  34%     -2   -4   37   34  108%
c i  216.8   42380   273357    140297   42168   3597 512035   40   115   73  35%     -4  -11   29   34   84%
c i  216.8   42379   273357    140298   42168   3597 512035   40   115   73  35%     -4  -11   29   34   84%
c i  217.1   42378   273357    140695   42520   3604 512037   42   123   73  34%     -5   -3   52   34  151%
c 
c [simplification-18] limit 140620 conflicts (hard 157819) hit after 142007 conflicts
c [quatres-13] found 25981 quaternary clauses 50% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-2] added 4 single-self-subsuming ternary resolvents
c [ternres-13] limit 37887231 with penalty 0 = 0 + 0
c [ternres-13] all 42284 free variables schedulable
c [ternres-13] 27 ternary resolvents (0 bin, 27 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-42] removed 545 variables
c [basicprobe-6] limit 189436155 penalty 0 = 0 + 0
c [basicprobe-6-0] 5279 probes remain 13% after last round
c [basicprobe-6-0] 753 units = 744 failed (99%) + 9 lifted (1%)
c [basicprobe-6-0] removed 1252 variables, found 328537 hbrs
c [bate-5] eliminated 932 asymmetric tautologies during probing
c [unhide-18] limit 3788723 with penalty 1 = 0 + 1
c [unhide-18-21] 4 units, 82 failed, 68729 tauts, 0 hbrs, 400419 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 219 transitive binary clauses
c [transred-14] found 2 units
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 40754 variables 100%
c [elim-14] limit of 378872310 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 1289 variables 3% in round 1 in 21405031 steps
c [elim-14-1] backward subsumption/strengthening limit 21405000
c [elim-14-1-1] backward checking 5872 touched variables 14%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 19 and strengthened 49 clauses in 1581832 steps
c [elim-14-1] rescheduled 161 variables 0% by backward subsumption
c [elim-14-2] eliminated 18 variables 0% in round 2 in 331767 steps
c [elim-14-2] backward subsumption/strengthening limit 331700
c [elim-14-2-1] backward checking 145 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 1 and strengthened 2 clauses in 127945 steps
c [elim-14-2] rescheduled 11 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 13762 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 1307 = 3% variables out of 40754 scheduled
c [bca-14] limit of 10000000 steps and 510501 added (scaled 2)
c [bca-14] 54468 out of 78896 literals actually usable 69%
c [bca-14] added 35 blocked clauses in 149439 steps
c [sort-queue-18] sorted 39447 enqueued variables after 142007 conflicts
c [score-dist-18] active 0 (0%), one 33844 (86%), zero 5603 (14%)
c [score-dist-18] max exp 1, different 2 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 2837 variables 6.7% (39447 remain 21%)
c [simplification-18] removed 18601 irredundant clauses 6.8% (254756 remain 26%)
c [simplification-18] maximum reduction of 7% = max (7%, 7%)
c [simplification-18] large reduction 7% >= 5% limit
c [simplification-18] next conflict interval 2000 = 2000/1
c [simplification-18] penalized conflict interval 2000 = 1 * 2000
c [simplification-18] hard conflict limit 154007 (soft 144007 + delta 10000)
c [simplification-18] new conflict limit 144007 (hard 154007)
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  231.6   39446   254756    142096   25150   3589 671046   46   135   50  34%      1    9   49   35  142%
c i  232.0   39445   254756    142725   25725   3597 671052   45   132   50  34%     -2    6   37   35  107%
c i  232.9   39444   254756    143788   26668   3606 671061   39   112   50  35%     -1  -15   16   35   46%
c i  233.4   39443   254756    144553   27386   3608 671070   36   105   50  34%     -2  -21   24   34   70%
c i  234.4   39442   254756    145705   28420   3616 671079   36   103   52  35%     -1  -22   21   34   62%
c i  234.4   39441   254756    145740   28453   3616 671079   36   103   52  35%     -1  -23   23   34   68%
c i  234.6   39440   254756    146082   28741   3618 671087   37   110   52  34%     -3  -16   36   35  104%
c i  236.0   39396   254756    147810   30375   3629 671094   38   117   54  32%      5   -8   28   35   81%
c i  236.3   39395   254756    148231   30772   3633 671095   36   110   56  33%      1  -15   23   35   65%
c i  237.4   39394   254756    149612   32047   3640 671104   36   112   56  32%      2  -13   29   35   83%
c i  237.9   39393   254756    150424   32764   3651 671109   36   117   56  31%     -1   -8   39   35  111%
c i  238.4   39392   254756    151076   33381   3655 671112   34   108   58  32%     -3  -17   21   35   62%
c i  240.4   39390   254756    153957   36038   3665 671123   31    86   61  36%     20  -38   25   34   74%
c 
c [simplification-19] limit 144007 conflicts (hard 154007) hit after 154007 conflicts
c [quatres-14] found 27228 quaternary clauses 54% in total
c [ternres-14] limit 40183848 with penalty 0 = 0 + 0
c [ternres-14] all 39390 free variables schedulable
c [ternres-14] 446 ternary resolvents (0 bin, 446 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-5] limit 502298 penalty 4 = 4 + 0
c [gauss-5] extracted 7 xors of average arity 2.7
c [gauss-5] connected 19 occurrences of 19 variables (average 1.0)
c [gauss-5] limit 502298 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-43] removed 26 variables
c [simpleprobe-7] all 39364 free variables schedulable
c [simpleprobe-7] limit 160735393 penalty 0 = 0 + 0
c [decomp-44] removed 118 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 118 variables, found 84250 hbrs, 86 units
c [unhide-19] limit 8036769 with penalty 0 = 0 + 0
c [unhide-19-25] 13 units, 35 failed, 60919 tauts, 0 hbrs, 409777 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 169 transitive binary clauses
c [transred-15] found 2 units
c [cce-6] limit of 25114905 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 77
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 76
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 75
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 74
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 73
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 72
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 71
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 70
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 69
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 67
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 66
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 65
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 64
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 63
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 62
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 61
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 60
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 59
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 58
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 57
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 56
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 55
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 54
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 53
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 52
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 51
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 50
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 49
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 48
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 47
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 46
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 45
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 44
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 43
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 42
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 41
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 40
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 39
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 38
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 37
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 36
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 35
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 34
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 33
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 32
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 31
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 30
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 29
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 28
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 27
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 26
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 25
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 24
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 23
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 22
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 21
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 20
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 19
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 18
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 17
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 16
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 15
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 14
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 13
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 12
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 11
c [cce-6-1] eliminated 3 clauses out of 38 (8%) of length 10
c [cce-6-1] eliminated 3 clauses out of 106 (3%) of length 9
c [cce-6-1] eliminated 3 clauses out of 107 (3%) of length 8
c [cce-6-1] eliminated 3 clauses out of 199 (2%) of length 7
c [cce-6-1] eliminated 16 clauses out of 2409 (1%) of length 6
c [cce-6-1] eliminated 261 clauses out of 11595 (2%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 399 large clauses in 25114909 steps
c [cce-6-1] allowing another 12557454 steps for small clauses
c [cce-6-1] scheduling 192649 clauses = 139852 binary + 52797 ternary
c [cce-6-1] tried to eliminate 955 small clauses 0%
c [cce-6-1] eliminated 189 binary clauses 0%
c [cce-6-1] eliminated 58 ternary clauses 0%
c [cce-6-1] eliminated 247 small clauses 0%
c [cce-6-1] eliminated 391 small clauses in 25114910 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 790 covered clauses in round 1
c [cce-6] eliminated 790 covered clauses in TOTAL during 1 rounds
c [cce-6] 790 < 1/100 * 249673 = 2496 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 39187 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 503 variables 1% in round 1 in 19872648 steps
c [elim-15-1] backward subsumption/strengthening limit 19872600
c [elim-15-1-1] backward checking 2552 touched variables 7%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 6 and strengthened 4 clauses in 607412 steps
c [elim-15-1] rescheduled 30 variables 0% by backward subsumption
c [elim-15-2] eliminated 2 variables 0% in round 2 in 30441 steps
c [elim-15-2] backward subsumption/strengthening limit 30400
c [elim-15-2-1] backward checking 19 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 0 and strengthened 2 clauses in 30401 steps
c [elim-15-2] rescheduled 8 variables 0% by backward subsumption
c [elim-15-3] eliminated 1 variables 0% in round 3 in 7687 steps
c [elim-15-3] backward subsumption/strengthening limit 7600
c [elim-15-3-1] backward checking 10 touched variables 0%
c [elim-15-3-1] incomplete backward checking 0 remain 0%
c [elim-15-3] subsumed 0 and strengthened 2 clauses in 7601 steps
c [elim-15] incomplete 8 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 506 = 1% variables out of 39187 scheduled
c [bca-15] limit of 10000000 steps and 496591 added (scaled 2)
c [bca-15] 52185 out of 77364 literals actually usable 67%
c [bca-15] added 40 blocked clauses in 149839 steps
c [sweep-13] limit 6027577 penalty 1 = 1 + 0
c [sweep-13-1] 1977 pos 12.0% + 14468 neg 88.0% = 16445 sched 42.5% ret 22236
c [sweep-13-1] 6053396 steps 109 queries 1022.06 avg class size
c [sweep-13-1] 1759 decisions 99 SAT calls 142.28 avg env size
c [sweep-13-1] 15857 variables remain 41% (22822 retained 59%)
c [decomp-45] removed 13 variables
c [sweep-13-1] removed 13 vars (0 failed, 10 eqs, 15 impls)
c [sweep-13] 13 < 1/1000 * 38681 = 38 considered unsuccessful
c [sweep-13] removed 13 vars in TOTAL (1 rounds, 108 queries)
c [sort-queue-19] sorted 38668 enqueued variables after 154007 conflicts
c [score-dist-19] active 0 (0%), one 33431 (86%), zero 5237 (14%)
c [score-dist-19] max exp 1, different 2 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 722 variables 1.8% (38668 remain 20%)
c [simplification-19] removed 7000 irredundant clauses 2.7% (247756 remain 25%)
c [simplification-19] maximum reduction of 3% = max (2%, 3%)
c [simplification-19] geometric conflict interval increment 8625 = 34500 / 4
c [simplification-19] new conflict interval 43125
c [simplification-19] penalized conflict interval 43125 = 1 * 43125
c [simplification-19] hard conflict limit 218694 (soft 197132 + delta 21562)
c [simplification-19] new conflict limit 197132 (hard 218694)
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  252.4   38667   247756    157712   34722   3904 676933   27    68   58  40%     32  -53   31   34   92%
c i  252.4   38666   247756    157728   34737   3904 676933   27    68   58  40%     32  -53   30   34   89%
c i  253.5   38665   247756    159075   35976   3914 676942   27    70   58  39%      9  -50   22   34   66%
c i  254.0   38664   247756    159674   36512   3915 676942   30    77   58  39%      2  -42   34   34  100%
c i  254.8   38579   247756    161253   37977   3926 676949   26    68   60  37%      3  -50   19   33   56%
c i  257.3   38578   247756    163998   40587   3940 676955   30    81   65  37%     17  -36   35   33  106%
c i  257.5   38576   247756    164274   40838   3945 676957   29    76   65  38%     11  -40   16   33   47%
c i  257.7   38575   247756    164529   41055   3947 676959   28    74   65  38%      6  -43   16   33   47%
c i  258.5   38574   247756    165421   41910   3950 676962   27    71   67  38%      0  -45   27   33   80%
c i  259.1   38573   247756    166177   42617   3953 676964   28    74   68  38%     -3  -42   31   33   92%
c i  261.2   38572   247756    169447   45659   3973 676981   25    72   71  35%     24  -41   15   33   47%
c i  261.3   38571   247756    169490   45689   3973 676982   26    73   71  35%     22  -40   25   33   76%
c i  261.4   38570   247756    169668   45833   3974 676983   26    76   71  35%     17  -37   36   33  111%
c i  261.7   38569   247756    169920   46051   3975 676983   28    77   71  36%     11  -36   40   33  123%
c i  264.1   38568   247756    172778   48662   4001 677023   28    75   74  38%     18  -37   13   33   41%
c i  264.3   38555   247756    173027   48889   4001 677031   29    81   74  36%     12  -31   33   33  102%
c i  264.8   38554   247756    173596   49435   4005 677033   28    82   74  34%      3  -30   19   32   58%
c i  266.4   38553   247756    175461   51131   4014 677039   31    85   81  37%      6  -25   26   33   80%
c i  266.8   38552   247756    176003   51606   4019 677046   31    82   81  38%     -0  -28   32   33   98%
c i  266.9   38551   247756    176104   51700   4021 677047   31    81   81  38%     -1  -30   25   33   77%
c i  266.9   38550   247756    176105   51700   4021 677047   31    81   81  38%     -1  -30   25   33   77%
c i  267.3   38549   247756    176632   52193   4024 677050   30    76   81  39%     -4  -34   21   32   66%
c i  269.0   38497   247756    178535   54019   4044 677065   28    71   89  40%      5  -38   23   32   70%
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  269.9   38496   247756    179523   54950   4053 677073   27    73   89  37%     -1  -35   20   32   64%
c i  273.2   38495   247756    183324   58413   4074 677088   34    85   89  40%     31  -21   40   32  124%
c i  273.4   38494   247756    183522   58564   4078 677092   34    83   89  41%     23  -23   34   32  105%
c i  274.1   38109   247756    184184   59187   4081 677095   33    82   95  40%      8  -24   38   32  118%
c i  274.2   38108   247756    184227   59226   4081 677096   33    82   95  40%      8  -24   35   32  107%
c i  274.3   38023   247756    184327   59316   4083 677098   33    82   95  40%      6  -24   29   32   89%
c i  274.4   38022   247756    184520   59480   4086 677100   32    81   95  40%      3  -25   24   32   75%
c i  278.1   38021   247756    189469   63951   4120 677119   28    69   97  41%     47  -35   32   32  100%
c i  278.2   38019   247756    189627   64103   4120 677121   28    68   97  41%     38  -36   28   32   88%
c -  279.7   38019   247756    190922   33182   4127 677125   35    85   48  41%      9  -18   54   32  166%
c i  279.8   38018   247756    190994   33245   4127 677126   35    85   56  41%      8  -18   50   32  155%
c i  281.0   37842   247756    192475   34581   4135 677133   34    86   56  39%      1  -17   43   32  134%
c i  287.3   37841   247756    199934   41417   4176 677162   30    74   59  41%     82  -28   22   32   67%
c i  288.9   37840   247756    201659   42948   4190 677170   33    78   60  42%     13  -23   18   33   55%
c i  296.4   37839   247756    210414   50725   4246 677214   27    65   73  42%     96  -32   16   32   51%
c i  297.1   37636   247756    211044   51281   4248 677216   28    64   73  44%     43  -33   21   32   67%
c i  297.2   37239   247756    211244   51459   4252 677219   28    64   73  44%     31  -33   29   32   90%
c i  297.9   36951   247756    212017   52104   4259 677221   26    60   73  44%      4  -37   13   32   42%
c i  298.0   36950   247756    212081   52161   4261 677223   26    59   73  44%      3  -37   11   32   36%
c i  298.7   36948   247756    212867   52816   4274 677234   27    58   73  46%     -9  -38   24   32   75%
c i  298.7   34540   247756    212871   52816   4275 677236   27    58   73  46%     -9  -38   23   32   74%
c i  298.7   34318   247756    212875   52816   4275 677238   27    58   73  46%     -9  -38   23   32   73%
c i  298.7   30465   247756    212876   52816   4275 677238   27    58   73  46%     -9  -38   23   32   73%
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  298.7   28257   247756    212879   52817   4275 677239   27    58   73  46%     -9  -38   23   32   72%
c i  298.7   28193   247756    212880   52817   4275 677239   27    58   73  46%     -9  -38   23   32   72%
c i  298.7   27774   247756    212897   52825   4278 677240   27    58   73  46%     -9  -38   21   32   68%
c i  298.7   26283   247756    212898   52825   4278 677240   27    58   73  46%     -9  -38   21   32   68%
c 0  298.7   25586   247756    212898   52825   4278 677240   27    58   73  46%     -9  -38   21   32   68%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 1666 basic ate = 1100 trn 66% + 566 lrg 34% in 5 updates
c bcas: 15 count, 1054 added (149 skipped), 3646357 steps
c bkwd: tried 334231 clauses, 668206 lits, 2.00 lits/clause
c bkwd: checked 10232747 occs, 30.62 occs/clause, 15.31 occs/lit
c bkwd: subsumed 11 binary, 147 ternary, 38 large
c bkwd: strengthened 1 binary, 2 ternary (100% self), 515 large (0% self)
c blkd: 5 bces, 10035 removed, 6968939 resolutions, 19260649 steps
c blkd: 11404 blocking literals 3%, 2 pure
c bump: 213351 bumped seen, 101784988 lits 477.1 on average
c card: 5 count, 0 units, 0 am1, 113390595 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 77879 subsumed
c card: 15351 at-most-one constraints found, average size 4.91
c card: 15351 at-most-one constraints used 100%, average size 4.91
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: 6 cces, 13321 eliminated, 13274 ate 100%, 47 abce 0%
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: 3398675 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 137 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 45 decompositions, 8903 equivalent 4%
c deco: 7484 decision-only clauses 4%, 66% reduction
c decs: 3050925 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 73545 eliminated 37%, 19 pure 0%
c elms: 38 rounds, 2.5 rounds/bve
c elms: 60349 small 82%, 13175 large 18%
c elms: 152469 tried small, 60349 succeeded 40%, 92120 failed 60%
c elms: 34986 subsumed, 48141 strengthened, 570 blocked
c elms: 16349653 copies, 16374039 resolutions, 4017762 ipos
c elms: 3814651 subchks, 2428183 strchks
c gaus: 5 extractions, 303 extracted, 2.3 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 9084414 steps, 4542207 extr 50%, 2456 elim 0%
c glue: 35.2 orig avg, 35.2 real avg, 4.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1236751 = 255381 simple 21% + 970242 trn 78% + 11128 lrg 1%, 3917 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 213351 clauses, 219.2 length
c lrnd: 46757866 lits = 64945603 orig - 18187737 removed 28%
c lrnd: 99769 uips 47%, 94116 flips 44%
c mins: 196986 mins 93%, 2512 bin 1%, 4421 size 2%
c mins: 127036805 poisoned searches, 28035725 hits, 22% hit rate
c mins: 148650149 used twice searches, 3738807 hits, 3% hit rate
c move: moved 17459, 11059 bin 63%, 6400 trn 37%
c otfs: 562 driving 24%, 1805 restarting 76%
c otfs: str 2367, 2286 red 97%, 81 irr 3%
c otfs: str 2367, 0 bin 0%, 71 trn 3%, 2296 lrg 97%
c otfs: sub 4, 4 red 100%, 0 irr 0%
c otfs: sub 4, 0 bin 0%, 1 trn 25%, 3 lrg 75%
c phas: 15 computed, 96885 set, 0 pos (0%), 96885 neg (100%)
c prbs: 6 basic, 19262 probed, 1661 failed, 12 lifted
c prbs: 7 simple, 925808 probed, 1194 failed, 1335 eqs
c prbs: 6 treelook, 113 probed, 7 failed, 0 lifted
c prom: 17900 locked 4% out of 459638 tried
c prps: 783836155 props, 243 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 14 count, 36 quat, 21 self1, 0 self2, 943 dup
c queu: 19 sorted, 3050925 next (4 steps 0.00)
c queu: 103135707 enq (0 steps 0.00), 101784988 deq 99%
c redc: 5414 clauses 26%, 20440 tried 10%, 135 sat 1%
c redc: 12707 lits 6%, 219276 tried 0%, 135 sat 0%
c redc: 732 times jump level reduced, 26.4 levels on average
c reds: 2 count, 106449.0 conflicts per reduce
c reds: 0 memlim 0%, 2 arith 100%
c reds: 50502 collected 75%, 16856 retired 25%
c rmbd: 41431 removed, 7150 red 17%
c rsts: 8026 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 19 count, 17 confs 89%, 0 vars 0%
c simp: 1 its 5%, 1 bin 5%, 0 trns 0%
c subl: 213351 count (240750 tried 1.1), 11212 sub out of 205986 (5.4%)
c swps: 13 count, 13 rounds, 2092 queries (160.9/round)
c swps: 1913 sat calls, 75 unsat (0.5% success rate)
c swps: 24121 decisions 12.6, 1015 conflicts 0.5
c swps; 1411.1 avg class size, 122.8 avg environment size
c swps: 0 failed, 387 impls, 223 equivs
c swp0: 693 type 0 queries, 233 unsat (33.6%), 650 sat (93.8%)
c swp1: 1399 type 1 queries, 788 unsat (56.3%), 1219 sat (87.1%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 6529398 calls to obtain time
c tops: 91256 fixed 46%, 496 its, 429.23 confs/it
c trds: 15 transitive reductions, 3019 removed, 50 failed
c trds: 14854 nodes, 38550 edges, 28875279 steps
c trim: 710982 words, 2.7 MB
c trnr: 14 count, 5 bin, 2016 trn, 90600833 steps
c unhd: 19 count, 25 rounds, 69709141 steps
c unhd: 706 non-trivial sccs of average size 2.4
c unhd: 131 units, 130 bin, 1 trn, 0 lrg
c unhd: 5758 failed, 5717 stamp, 0 lits, 14 bin, 14 trn, 0 lrg
c unhd: 344734 tauts, 16747 bin 5%, 10633 trn 3%, 790 lrg 0%
c unhd: 344734 tauts, 316564 stamp 92%, 292016 red 85%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 2439824 str, 130 bin 0%, 1943 trn 0%, 2437751 lrg 100%, 2428198 red 100%
c vars: 25586 remaining 13% and 173704 removed 87% out of 199290
c vars: 91256 fixed 46%, 73545 eliminated 37%, 8903 equivalent 4%
c vsts: 5557254762 visits, 94% srch, 6% simp, 0% lkhd
c vsts: 7.0 search visits per propagation, 24495.7 per conflict
c wchs: 672019470 pushed, 48010182 enlarged, 201 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         206022         50502         16856      11263656       1611571        100302
c 
c  0 0         27515  13      2462   5         0   0   6802467  60    756440  47     30656  31     2.2
c  1 5         10922   5      1950   4       731   4    858824   8<   139935   9      8797   9     1.3
c  2 6         27167  13      6846  14      2090  12   1265350  11    208147  13<    14288  14     4.4
c  3 9         27683  13      7819  15      2417  14    752448   7    137412   9     10441  10<    6.6
c  4 14        22909  11<     7020  14      2323  14    514984   5     99437   6      8368   8     7.6
c  5 21        20542  10      6641  13<     1949  12<   353295   3     81566   5      7251   7     8.3
c  6 30        17217   8      5580  11      1726  10    229578   2     57067   4      5372   5     6.9
c  7 41        14492   7      4317   9      1444   9    218123   2     49544   3      5021   5     5.0
c  8 54        11177   5      3392   7      1202   7    117935   1     32829   2      3574   4     4.6
c  9 69         7767   4      2122   4       859   5     60695   1     19099   1      2298   2     3.2
c 10 86         7322   4      1456   3       807   5     55833   0     16569   1      2182   2     2.0
c 11 126        6599   3       602   1       771   5     27057   0      9867   1      1476   1     1.9
c 12 230        4437   2       279   1       510   3      6739   0      3503   0       560   1     2.3
c 13 534         273   0        16   0        27   0       328   0       156   0        18   0     0.3
c 
c avg                  4.4           4.7           5.5           1.3           2.0           3.0
c std                  3.2           2.6           2.9           2.1           2.6           3.0
c 
c   28.795  10% probe
c   17.839   6% unhide
c   14.268   5% elim
c   10.314   3% sweep
c   10.034   3% bump
c    7.864   3% cce
c    2.536   1% bca
c    1.930   1% decide
c    1.885   1% block
c 
c    4.448 < 1% rest (below)
c 
c    1.547   1% transred
c    1.213   0% gauss
c    0.710   0% quatres
c    0.663   0% ternres
c    0.316   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    3.808   1% preprocessing     4%
c   93.168  31% inprocessing     96%
c ==================================
c   96.976  32% simplifying
c  201.739  68% search
c ==================================
c  298.719 100% all
c 
c        212898 conflicts,         712.7 confs/sec
c          3171 ternaries,          67.1 confs/ternary
c          3310 binaries,           64.3 confs/binary
c           496 iterations,        429.2 confs/iteration
c 
c             2 reductions,          0.0 redus/sec, 106449.0 confs/reduction
c          8026 restarts,           26.9 rests/sec,     26.5 confs/restart
c       3050925 decisions,       10213.4 decis/sec,     14.3 decis/conflict
c     783836155 propagations,  2623996.0 props/sec,    256.9 props/decision
c 
c 298.7 seconds, 106.9 MB
c launch: done
