c launch: /data/cnf/sc2014/app/UCG-20-5p1.cnf.bz2
c host: atom24
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/UCG-20-5p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UCG-20-5p1.cnf.bz2
c no embedded options
c found 'p cnf 224986 1204430' header
c read 224986 variables, 1204430 clauses, 2908691 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 213583 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] INC (--score=1)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  213583  1192277         0       0      0     0    0     0   55   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 6240 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] 6240 out of 6240 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 51700 variables
c [simpleprobe-1] all 173286 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 203 variables
c [simpleprobe-1] 9287 variables remain 5% (163796 retained 95%)
c [simpleprobe-1] removed 203 variables, found 14830 hbrs, 20 units
c [unhide-1] limit 57932 based on 926913 irredundant clauses
c [unhide-1-1] 17 units, 836 failed, 10768 tauts, 0 hbrs, 8216 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 171574 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 47540 not tried 28% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 65901 = 38% variables out of 171574 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 769054 negative 99.2% of 774975 except 5921 0.8%
c [phase-count-1] 623698 positive 80.5% of 774975 except 151277 19.5%
c [phase-count-1] less non-negative clauses 5921 than limit 77400 (10.0%)
c [phase-count-1] non-pos/non-neg = 151277/5921 = 25.55 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 105673 negative 100%
c [sort-queue-1] sorted 105673 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 105673 (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 72469 variables 40.7% (105673 remain 49%)
c [simplification-1] removed 417302 irredundant clauses 35.0% (774975 remain 65%)
c [simplification-1] maximum reduction of 41% = max (41%, 35%)
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    4.5  105672   774975         4       2      1  8106    0     1   51   0%      0    1    0    0 25376%
c i    4.5  104996   774975         5       2      1  8106    0     1   51   0%      0    1    0    0 25278%
c i    4.5  104977   774975        12       7      2  8106    0     1   51   1%      0    1    0    0 25048%
c i    4.6  104974   774975       108      79      8  8115    0     2   51   7%      0    2    2    0 21662%
c i    4.8  104958   774975       228     177     19  8125    0     6   52   5%      0    6    3    0 17527%
c i    4.8  104907   774975       264     201     26  8129    0     7   52   5%      0    7    4    0 16146%
c i    5.0  104897   774975       395     307     39  8139    1    10   52   6%      0   10    5    0 13621%
c i    5.3  103935   774975       576     465     49  8147    2    19   52  10%      0   19   19    0 16180%
c i    5.3  102973   774975       601     482     51  8150    2    21   52  11%      0   20   23    0 16302%
c 
c [simplification-2] limit 1013 conflicts (hard 11000) hit after 1013 conflicts
c [decomp-3] removed 3184 variables
c [simpleprobe-2] 8732 schedulable variables 9%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 9633 variables remain 9% (92856 retained 91%)
c [simpleprobe-2] removed 0 variables, found 1661 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 69028 literals 34%
c [treelook-1] scheduling used 533365 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 305247 steps
c [treelook-1] 68980 literals remain 34%
c [treelook-1] 68903 variables remain to probed next time 67%
c [decomp-5] removed 43 variables
c [treelook-1] removed 44 variables, found 2850 hbrs
c [basicprobe-1] limit 5996584 based on 749573 irredundant clauses
c [basicprobe-1-0] 31475 probes remain 36% after last round
c [basicprobe-1-0] 49 units = 49 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 15581 variables, found 19122 hbrs
c [unhide-2] limit 50000 with penalty 1 = 0 + 1
c [unhide-2-2] 26 units, 2538 failed, 6624 tauts, 0 hbrs, 1798 literals
c [elim-2] 40678 variables 48% will be scheduled this time
c [elim-2] scheduled 40678 variables 48%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 12040 not tried 14% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 187 = 0% variables out of 40678 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 583348 negative 99.0% of 589303 except 5955 1.0%
c [phase-count-2] 468593 positive 79.5% of 589303 except 120710 20.5%
c [phase-count-2] less non-negative clauses 5955 than limit 58900 (10.0%)
c [phase-count-2] non-pos/non-neg = 120710/5955 = 20.27 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 8050 negative 100%
c [sort-queue-2] sorted 72638 enqueued variables after 1013 conflicts
c [score-dist-2] active 11774 (14%), one 0 (0%), zero 72638 (86%)
c [score-dist-2] max exp 509, different 9 (2%)
c [score-dist-2] median active exp 504, avg 504.2
c [simplification-2] removed 18191 variables 17.7% (84412 remain 40%)
c [simplification-2] removed 185672 irredundant clauses 24.0% (589303 remain 49%)
c [simplification-2] maximum reduction of 24% = max (18%, 24%)
c [simplification-2] large reduction 24% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13013 (soft 3013 + delta 10000)
c [simplification-2] new conflict limit 3013 (hard 13013)
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    8.8   84411   589303      1505    1164    120 15993   10    55   42  17%      5   54   48    1 7141%
c i    8.9   84398   589303      1538    1190    123 15993   10    56   42  17%      5   55   45    1 6592%
c i    8.9   84387   589303      1539    1190    123 15993   10    56   42  17%      5   55   45    1 6567%
c i    8.9   84377   589303      1540    1190    123 15993   10    56   42  17%      5   55   45    1 6541%
c i    8.9   84364   589303      1541    1190    123 15993   10    55   42  17%      5   55   45    1 6516%
c i    9.2   84351   589303      1828    1430    145 16007   10    64   42  16%      4   64   26    1 3407%
c i    9.2   84298   589303      1834    1433    145 16009   10    65   42  16%      4   64   25    1 3335%
c i    9.2   83992   589303      1874    1466    149 16011   10    70   42  14%      4   69   23    1 3039%
c i    9.7   83600   589303      2049    1609    159 16029   11    89   42  12%      4   88   26    1 3158%
c i    9.8   83592   589303      2084    1642    159 16030   11    94   43  12%      3   93   28    1 3313%
c 
c [simplification-3] limit of 19 iterations hit after 19 iterations
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3738 at-most-one constraints of average size 4.5
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3738 out of 3738 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 1124 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 52256 literals 31%
c [treelook-2] scheduling used 400893 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 373766 steps
c [treelook-2] 52174 literals remain 31%
c [treelook-2] 49430 variables remain to probed next time 59%
c [decomp-7] removed 73 variables
c [treelook-2] removed 73 variables, found 3152 hbrs
c [unhide-3] limit 162415 with penalty 0 = 0 + 0
c [unhide-3-3] 13 units, 796 failed, 15755 tauts, 0 hbrs, 5232 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 82063 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 16152 not tried 20% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2108 = 3% variables out of 82063 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 546017 negative 98.9% of 551880 except 5863 1.1%
c [phase-count-3] 437494 positive 79.3% of 551880 except 114386 20.7%
c [phase-count-3] less non-negative clauses 5863 than limit 55100 (10.0%)
c [phase-count-3] non-pos/non-neg = 114386/5863 = 19.51 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 2133 negative 100%
c [sort-queue-3] sorted 56211 enqueued variables after 2084 conflicts
c [score-dist-3] active 23744 (30%), one 0 (0%), zero 56211 (70%)
c [score-dist-3] max exp 510, different 10 (2%)
c [score-dist-3] median active exp 504, avg 504.2
c [simplification-3] removed 3629 variables 4.3% (79955 remain 37%)
c [simplification-3] removed 37423 irredundant clauses 6.4% (551880 remain 46%)
c [simplification-3] maximum reduction of 6% = max (4%, 6%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 3044 (hard 13013)
c [simplification-3] 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   12.1   79954   551880      2143    1480    155 17035   12   105   40  12%      3  104   42    1 4522%
c i   12.4   79866   551880      2317    1607    161 17047   19   131   41  14%      3  130  114    1 8298%
c i   12.5   79858   551880      2346    1632    162 17048   19   134   41  14%      3  132  111    1 7824%
c i   12.7   79780   551880      2454    1720    164 17060   22   145   41  15%      3  143  120    2 7291%
c i   12.8   79733   551880      2545    1804    164 17062   23   159   41  14%      2  157   93    2 5514%
c i   13.0   79732   551880      2649    1893    166 17065   23   173   41  14%      2  170   81    2 4609%
c 
c [simplification-4] limit 3044 conflicts (hard 13013) hit after 3047 conflicts
c [decomp-8] removed 235 variables
c [basicprobe-2] limit 6694083 penalty 0 = 0 + 0
c [basicprobe-2-0] 27842 probes remain 37% after last round
c [basicprobe-2-0] 72 units = 68 failed (94%) + 4 lifted (6%)
c [basicprobe-2-0] removed 3879 variables, found 16615 hbrs
c [unhide-4] limit 267763 with penalty 0 = 0 + 0
c [unhide-4-4] 6 units, 973 failed, 5131 tauts, 0 hbrs, 10831 literals
c [elim-4] 11263 variables 15% will be scheduled this time
c [elim-4] scheduled 11263 variables 15%
c [elim-4] boosting limit by 20
c [elim-4] limit of 535526680 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 19 variables 0% in round 1 in 23842321 steps
c [elim-4-1] backward subsumption/strengthening limit 23842300
c [elim-4-1-1] backward checking 61 touched variables 0%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 2 and strengthened 0 clauses in 106919 steps
c [elim-4-1] rescheduled 5 variables 0% by backward subsumption
c [elim-4-2] eliminated 2 variables 0% in round 2 in 1153 steps
c [elim-4-2] backward subsumption/strengthening limit 1100
c [elim-4-2-1] backward checking 8 touched variables 0%
c [elim-4-2-1] incomplete backward checking 7 remain 88%
c [elim-4-2] subsumed 1 and strengthened 0 clauses in 1116 steps
c [elim-4-2] rescheduled 2 variables 0% by backward subsumption
c [elim-4-3] no variable eliminated in round 3 in 4696 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 21 = 0% variables out of 11263 scheduled
c [elim-4] 21 < 1/100 * 11263 = 112 considered unsuccessful
c [phase-count-4] 499842 negative 98.8% of 505705 except 5863 1.2%
c [phase-count-4] 398006 positive 78.7% of 505705 except 107699 21.3%
c [phase-count-4] less non-negative clauses 5863 than limit 50500 (10.0%)
c [phase-count-4] non-pos/non-neg = 107699/5863 = 18.37 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 1566 negative 100%
c [sort-queue-4] sorted 44722 enqueued variables after 3047 conflicts
c [score-dist-4] active 29842 (40%), one 0 (0%), zero 44722 (60%)
c [score-dist-4] max exp 510, different 10 (2%)
c [score-dist-4] median active exp 505, avg 505.0
c [simplification-4] removed 5162 variables 6.5% (74564 remain 35%)
c [simplification-4] removed 46175 irredundant clauses 8.4% (505705 remain 42%)
c [simplification-4] maximum reduction of 8% = max (6%, 8%)
c [simplification-4] large reduction 8% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 15047 (soft 5047 + delta 10000)
c [simplification-4] new conflict limit 5047 (hard 15047)
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   15.9   74563   505705      3283    2248    173 25286   57   219   40  26%      4  215  227    4 5397%
c i   16.0   74556   505705      3339    2268    173 25286   61   222   40  27%      4  217  250    4 5558%
c i   16.0   74550   505705      3340    2268    173 25286   61   221   40  27%      4  217  249    4 5537%
c i   16.0   74542   505705      3341    2268    173 25286   61   221   40  27%      3  217  248    4 5515%
c i   16.0   74535   505705      3342    2268    173 25286   61   221   40  27%      3  217  247    4 5494%
c i   16.1   74526   505705      3344    2268    173 25287   60   221   40  27%      3  217  245    4 5451%
c i   16.1   74519   505705      3345    2268    173 25287   60   221   40  27%      3  217  244    4 5430%
c i   16.1   74512   505705      3346    2268    173 25287   60   221   40  27%      3  217  243    4 5409%
c i   16.8   74503   505705      3644    2409    174 25288   76   234   40  32%      3  229  280    6 4863%
c i   17.2   74502   505705      3844    2529    175 25290   83   244   41  34%      3  238  236    6 3672%
c i   17.2   74498   505705      3849    2533    175 25290   83   244   41  34%      3  238  233    6 3624%
c i   17.2   74496   505705      3852    2534    175 25291   83   244   41  34%      3  238  231    6 3591%
c i   17.3   74490   505705      3864    2544    176 25291   83   245   41  34%      3  239  223    6 3467%
c i   17.7   74481   505705      4097    2675    185 25297   92   258   42  36%      3  251  240    7 3285%
c i   17.8   74480   505705      4171    2721    185 25300   96   264   42  36%      2  256  255    8 3339%
c i   17.8   74479   505705      4172    2721    185 25300   96   263   42  36%      2  256  254    8 3326%
c i   18.0   74478   505705      4242    2776    185 25301   97   269   42  36%      2  262  239    8 3053%
c i   18.0   74475   505705      4243    2776    185 25301   97   269   42  36%      2  262  238    8 3041%
c i   18.0   74472   505705      4245    2776    185 25301   98   269   42  36%      2  262  238    8 3043%
c i   19.2   74465   505705      4812    3018    194 25312  135   302   44  45%      3  292  385   11 3467%
c i   19.4   74461   505705      4939    3097    195 25315  141   309   45  46%      3  298  366   12 3133%
c i   19.5   74458   505705      4961    3118    195 25315  142   310   45  46%      3  299  360   12 3058%
c i   19.5   74455   505705      4963    3119    195 25315  142   310   45  46%      3  299  360   12 3050%
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   19.5   74452   505705      4964    3119    195 25315  142   310   45  46%      3  299  358   12 3038%
c i   19.5   74449   505705      4979    3129    195 25315  142   310   45  46%      3  300  351   12 2961%
c i   19.5   74448   505705      4986    3132    195 25315  142   311   45  46%      3  300  352   12 2958%
c i   19.8   74447   505705      5113    3203    197 25315  150   317   45  47%      3  306  361   13 2867%
c i   19.8   74442   505705      5114    3203    197 25315  149   317   45  47%      3  306  359   13 2855%
c i   19.8   74435   505705      5115    3203    197 25315  149   317   45  47%      3  306  358   13 2844%
c i   19.8   74430   505705      5118    3205    197 25315  150   317   45  47%      3  306  358   13 2840%
c i   19.8   74423   505705      5119    3205    197 25315  150   317   45  47%      3  306  356   13 2829%
c i   19.9   74415   505705      5138    3213    197 25315  151   318   45  47%      3  306  361   13 2835%
c i   19.9   74414   505705      5153    3220    197 25315  152   318   45  48%      2  307  361   13 2820%
c i   19.9   74413   505705      5180    3239    197 25315  153   320   45  48%      2  308  360   13 2784%
c 
c [simplification-5] limit 5181 conflicts (hard 15047) hit after 5182 conflicts
c [quatres-1] found 34974 quaternary clauses 44% in total
c [quatres-1-2] added 1 single-self-subsuming ternary resolvents
c [quatres-1-2] added 3 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 74413 free variables schedulable
c [ternres-1] 22 ternary resolvents (0 bin, 22 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 276 xors of average arity 2.2
c [gauss-1] connected 613 occurrences of 287 variables (average 2.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 306 variables
c [unhide-5] limit 543126 with penalty 0 = 0 + 0
c [unhide-5-5] 12 units, 329 failed, 10958 tauts, 0 hbrs, 11704 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 345 transitive binary clauses
c [transred-1] found 24 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 73588 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 7309 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 139 (1%) of length 10
c [cce-1-1] eliminated 2 clauses out of 596 (0%) of length 9
c [cce-1-1] eliminated 68 clauses out of 626 (11%) of length 8
c [cce-1-1] eliminated 147 clauses out of 968 (15%) of length 7
c [cce-1-1] eliminated 3171 clauses out of 4914 (65%) of length 6
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 3389 large clauses in 30000003 steps
c [cce-1-1] allowing another 15000001 steps for small clauses
c [cce-1-1] scheduling 254067 clauses = 237374 binary + 16693 ternary
c [cce-1-1] tried to eliminate 680 small clauses 0%
c [cce-1-1] eliminated 233 binary clauses 0%
c [cce-1-1] eliminated 8 ternary clauses 0%
c [cce-1-1] eliminated 241 small clauses 0%
c [cce-1-1] eliminated 241 small clauses in 30000000 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3630 covered clauses in round 1
c [cce-1] eliminated 3630 covered clauses in TOTAL during 1 rounds
c [cce-1] 3630 < 1/100 * 480197 = 4801 considered unsuccessful
c [bca-1] limit of 10000000 steps and 953634 added (scaled 2)
c [bca-1] 132200 out of 147178 literals actually usable 90%
c [bca-1] added 191 blocked clauses in 389132 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3758 pos 5.1% + 69830 neg 94.9% = 73588 sched 100.0% ret 0
c [sweep-1-1] 1205343 steps 22 queries 16605.55 avg class size
c [sweep-1-1] 262 decisions 18 SAT calls 100.89 avg env size
c [sweep-1-1] 73467 variables remain 100% (121 retained 0%)
c [decomp-10] removed 3 variables
c [sweep-1-1] removed 3 vars (0 failed, 3 eqs, 7 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 3 vars in TOTAL (1 rounds, 21 queries)
c [phase-count-5] 473880 negative 99.4% of 476566 except 2686 0.6%
c [phase-count-5] 379362 positive 79.6% of 476566 except 97204 20.4%
c [phase-count-5] less non-negative clauses 2686 than limit 47600 (10.0%)
c [phase-count-5] non-pos/non-neg = 97204/2686 = 36.19 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 1093 negative 100%
c [sort-queue-5] sorted 39969 enqueued variables after 5182 conflicts
c [score-dist-5] active 33616 (46%), one 0 (0%), zero 39969 (54%)
c [score-dist-5] max exp 512, different 12 (2%)
c [score-dist-5] median active exp 506, avg 506.0
c [simplification-5] removed 828 variables 1.1% (73585 remain 34%)
c [simplification-5] removed 29139 irredundant clauses 5.8% (476566 remain 40%)
c [simplification-5] maximum reduction of 6% = max (1%, 6%)
c [simplification-5] large reduction 6% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 17182 (soft 7182 + delta 10000)
c [simplification-5] new conflict limit 7182 (hard 17182)
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.1   73584   476566      5219    3260    228 34053  155   321   41  48%      2  309  361   13 2748%
c i   23.4   73579   476566      5406    3306    229 34053  168   328   42  51%      2  315  403   14 2812%
c i   23.6   73573   476566      5494    3385    229 34053  168   331   42  51%      2  318  348   15 2381%
c i   23.9   73565   476566      5698    3574    230 34057  163   343   43  47%      2  329  187   15 1272%
c i   23.9   73564   476566      5699    3574    230 34057  163   343   43  47%      2  329  187   15 1267%
c i   23.9   73563   476566      5702    3576    230 34057  163   343   43  47%      2  329  185   15 1254%
c i   23.9   73562   476566      5704    3577    230 34057  163   343   43  47%      2  329  183   15 1244%
c i   23.9   73561   476566      5705    3577    230 34057  163   343   43  47%      2  329  182   15 1240%
c i   23.9   73560   476566      5709    3580    230 34057  163   343   43  47%      2  329  182   15 1234%
c i   23.9   73559   476566      5710    3580    230 34057  162   343   43  47%      2  329  181   15 1230%
c i   25.4   73558   476566      6491    3928    231 34057  196   366   44  54%      4  348  392   19 2095%
c i   25.8   73557   476566      6736    3994    231 34059  209   371   44  56%      4  351  420   20 2087%
c i   25.8   73556   476566      6737    3994    231 34059  209   370   44  56%      4  351  418   20 2079%
c i   26.1   73555   476566      6883    4008    233 34065  216   373   44  58%      3  353  411   21 1960%
c i   26.1   73554   476566      6891    4009    233 34065  216   373   44  58%      3  353  410   21 1950%
c i   26.6   73553   476566      7159    4080    233 34066  227   375   47  60%      3  354  391   22 1739%
c i   26.6   73552   476566      7160    4080    233 34066  226   375   47  60%      3  354  390   22 1733%
c i   26.6   73551   476566      7161    4080    233 34066  226   375   47  60%      3  353  388   22 1726%
c i   26.7   73550   476566      7169    4087    233 34066  226   375   47  60%      3  353  384   23 1704%
c i   26.7   73549   476566      7171    4088    233 34066  226   375   47  60%      3  353  382   23 1696%
c i   26.7   73548   476566      7172    4088    233 34066  226   375   47  60%      3  353  380   23 1690%
c i   26.7   73547   476566      7175    4090    233 34066  226   375   47  60%      3  353  378   23 1680%
c i   26.7   73546   476566      7176    4090    233 34066  226   375   47  60%      3  353  377   23 1674%
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.7   73545   476566      7179    4092    233 34066  226   375   47  60%      3  353  375   23 1664%
c i   26.7   73544   476566      7181    4093    233 34066  226   375   47  60%      3  353  373   23 1657%
c i   26.7   73543   476566      7182    4093    233 34066  226   375   47  60%      3  353  372   23 1650%
c i   26.7   73542   476566      7183    4093    233 34066  226   375   47  60%      3  353  370   23 1644%
c 
c [simplification-6] limit 7310 conflicts (hard 17182) hit after 7310 conflicts
c [quatres-2] found 34773 quaternary clauses 46% in total
c [quatres-2-2] added 1 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 73542 free variables schedulable
c [ternres-2] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-2] 42672 variables remain 58% (30870 retained 42%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2245 at-most-one constraints of average size 4.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2245 out of 2245 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 46 variables
c [simpleprobe-3] 6060 schedulable variables 8%
c [simpleprobe-3] limit 7704632 penalty 1 = 1 + 0
c [decomp-12] removed 53 variables
c [simpleprobe-3] 3976 variables remain 5% (69510 retained 95%)
c [simpleprobe-3] removed 53 variables, found 8043 hbrs, 18 units
c [unhide-6] limit 770463 with penalty 0 = 0 + 0
c [unhide-6-6] 10 units, 530 failed, 4805 tauts, 0 hbrs, 18437 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 372 transitive binary clauses
c [transred-2] found 17 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 72683 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 1120 blocked clauses
c [block-2] 1120 < 1/100 * 475421 = 4754 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 72682 variables 100%
c [elim-5] limit of 38523160 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 1195 not tried 2% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 814 = 1% variables out of 72682 scheduled
c [bca-2] limit of 10000000 steps and 929759 added (scaled 2)
c [bca-2] 130005 out of 143738 literals actually usable 90%
c [bca-2] added 126 blocked clauses in 390424 steps
c [sweep-2] limit 1155694 penalty 0 = 0 + 0
c [sweep-2-1] 3732 pos 5.2% + 68035 neg 94.8% = 71767 sched 99.9% ret 101
c [sweep-2-1] 1183027 steps 22 queries 16987.55 avg class size
c [sweep-2-1] 195 decisions 17 SAT calls 43.82 avg env size
c [sweep-2-1] 71662 variables remain 100% (201 retained 0%)
c [decomp-13] removed 17 variables
c [sweep-2-1] removed 17 vars (0 failed, 5 eqs, 9 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 17 vars in TOTAL (1 rounds, 21 queries)
c [phase-count-6] 461858 negative 99.4% of 464489 except 2631 0.6%
c [phase-count-6] 367696 positive 79.2% of 464489 except 96793 20.8%
c [phase-count-6] less non-negative clauses 2631 than limit 46400 (10.0%)
c [phase-count-6] non-pos/non-neg = 96793/2631 = 36.79 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 963 negative 100%
c [sort-queue-6] sorted 37884 enqueued variables after 7310 conflicts
c [score-dist-6] active 33967 (47%), one 0 (0%), zero 37884 (53%)
c [score-dist-6] max exp 513, different 13 (3%)
c [score-dist-6] median active exp 506, avg 506.2
c [simplification-6] removed 1691 variables 2.3% (71851 remain 34%)
c [simplification-6] removed 12077 irredundant clauses 2.5% (464489 remain 39%)
c [simplification-6] maximum reduction of 3% = max (2%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 5000
c [simplification-6] penalized conflict interval 5000 = 1 * 5000
c [simplification-6] hard conflict limit 22310 (soft 12310 + delta 10000)
c [simplification-6] new conflict limit 12310 (hard 22310)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   30.6   71850   464489      7355    3091    214 37845  227   376   40  60%      3  353  313   23 1352%
c i   30.6   71848   464489      7356    3091    214 37845  227   376   40  60%      3  353  312   23 1347%
c i   30.7   71846   464489      7368    3097    214 37845  227   376   40  61%      3  353  311   23 1343%
c i   30.7   71845   464489      7369    3097    214 37845  227   376   40  61%      3  353  310   23 1338%
c i   30.7   71844   464489      7389    3105    214 37845  228   376   40  61%      3  353  306   23 1316%
c i   30.7   71843   464489      7393    3106    214 37845  228   376   40  61%      3  353  305   23 1311%
c i   30.9   71842   464489      7480    3161    214 37845  228   376   41  60%      2  353  283   24 1202%
c i   30.9   71841   464489      7481    3161    214 37845  228   376   41  60%      2  353  282   24 1197%
c i   30.9   71840   464489      7489    3168    214 37845  228   376   41  60%      2  353  281   24 1191%
c i   30.9   71832   464489      7507    3173    214 37848  227   376   41  60%      2  353  271   24 1150%
c i   32.0   71831   464489      8098    3478    222 37854  237   383   41  62%      3  356  315   26 1212%
c i   33.4   71830   464489      9019    4084    268 37883  221   410   43  54%      6  378  172   28  618%
c i   36.5   71829   464489     10973    4671    269 37883  286   434   47  66%     17  391  307   38  798%
c i   36.5   71828   464489     10974    4671    269 37883  286   434   47  66%     17  390  306   38  795%
c i   36.6   71822   464489     10975    4671    269 37883  286   433   47  66%     17  390  304   38  792%
c i   36.6   71812   464489     10976    4671    269 37883  286   433   47  66%     17  390  303   38  789%
c i   36.6   71805   464489     10977    4671    269 37883  286   433   47  66%     17  390  302   38  786%
c i   36.6   71795   464489     10978    4671    269 37883  286   433   47  66%     17  390  301   38  783%
c i   36.6   71793   464489     10979    4671    269 37883  286   433   47  66%     17  390  300   38  780%
c i   36.8   71778   464489     11104    4785    269 37883  280   439   47  64%     15  395  226   39  587%
c i   36.8   71774   464489     11105    4785    269 37883  280   439   47  64%     15  395  225   39  584%
c i   37.2   71766   464489     11391    5017    272 37909  269   451   47  60%     12  406  144   39  371%
c 
c [simplification-7] limit 12413 conflicts (hard 22310) hit after 12413 conflicts
c [quatres-3] found 35287 quaternary clauses 46% in total
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [ternres-3] limit 6264206 with penalty 0 = 0 + 0
c [ternres-3] 41656 schedulable variables 58%
c [ternres-3] 71 ternary resolvents (2 bin, 69 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 17 xors of average arity 2.8
c [gauss-2] connected 47 occurrences of 41 variables (average 1.1)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 7 variables
c [treelook-3] limit 626420 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 85347 literals 59%
c [treelook-3] scheduling used 626526 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 626420 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 639030 steps
c [treelook-3] 85332 literals remain 59%
c [treelook-3] 39894 variables remain to probed next time 56%
c [treelook-3] removed 3 variables, found 5175 hbrs
c [unhide-7] limit 1252841 with penalty 0 = 0 + 0
c [unhide-7-7] 6 units, 193 failed, 7032 tauts, 0 hbrs, 28793 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 405 transitive binary clauses
c [transred-3] found 7 units
c [cce-2] limit of 15660516 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 6 clauses out of 802 (1%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 6 large clauses in 15660527 steps
c [cce-2-1] allowing another 7830263 steps for small clauses
c [cce-2-1] scheduling 243186 clauses = 226218 binary + 16968 ternary
c [cce-2-1] tried to eliminate 461 small clauses 0%
c [cce-2-1] eliminated 148 binary clauses 0%
c [cce-2-1] eliminated 12 ternary clauses 0%
c [cce-2-1] eliminated 160 small clauses 0%
c [cce-2-1] eliminated 3318 small clauses in 15660524 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 3324 covered clauses in round 1
c [cce-2] eliminated 3324 covered clauses in TOTAL during 1 rounds
c [cce-2] 3324 < 1/100 * 457419 = 4574 considered unsuccessful
c [elim-6] 1193 variables 2% will be scheduled this time
c [elim-6] scheduled 1193 variables 2%
c [elim-6] limit of 125284128 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 3841688 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 1193 scheduled
c [bca-3] limit of 10000000 steps and 908768 added (scaled 2)
c [bca-3] 127131 out of 142888 literals actually usable 89%
c [bca-3] added 90 blocked clauses in 379364 steps
c [sweep-3] limit 1879261 penalty 0 = 0 + 0
c [sweep-3-1] 3604 pos 5.1% + 67654 neg 94.9% = 71258 sched 99.7% ret 185
c [sweep-3-1] 1881244 steps 39 queries 16180.36 avg class size
c [sweep-3-1] 391 decisions 30 SAT calls 56.27 avg env size
c [sweep-3-1] 71085 variables remain 100% (350 retained 0%)
c [decomp-16] removed 17 variables
c [sweep-3-1] removed 17 vars (0 failed, 9 eqs, 20 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 17 vars in TOTAL (1 rounds, 38 queries)
c [phase-count-7] 451315 negative 99.4% of 453944 except 2629 0.6%
c [phase-count-7] 359129 positive 79.1% of 453944 except 94815 20.9%
c [phase-count-7] less non-negative clauses 2629 than limit 45300 (10.0%)
c [phase-count-7] non-pos/non-neg = 94815/2629 = 36.07 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 723 negative 100%
c [sort-queue-7] sorted 35548 enqueued variables after 12413 conflicts
c [score-dist-7] active 35878 (50%), one 0 (0%), zero 35548 (50%)
c [score-dist-7] max exp 514, different 14 (3%)
c [score-dist-7] median active exp 507, avg 506.7
c [simplification-7] removed 338 variables 0.5% (71426 remain 33%)
c [simplification-7] removed 10545 irredundant clauses 2.3% (453944 remain 38%)
c [simplification-7] maximum reduction of 2% = max (0%, 2%)
c [simplification-7] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-7] new conflict interval 11666
c [simplification-7] penalized conflict interval 11666 = 1 * 11666
c [simplification-7] hard conflict limit 34079 (soft 24079 + delta 10000)
c [simplification-7] new conflict limit 24079 (hard 34079)
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.7   71425   453944     12981    5728    359 43018  288   474   47  61%     14  418  375   46  822%
c i   44.7   71412   453944     13478    6156    359 43019  293   461   47  63%     10  402  313   48  657%
c i   44.7   71401   453944     13479    6156    359 43019  293   461   47  63%     10  402  312   48  654%
c i   44.7   71393   453944     13481    6157    359 43019  293   461   47  63%     10  402  310   48  650%
c i   44.7   71381   453944     13485    6160    359 43019  292   461   47  63%     10  402  306   48  641%
c i   44.7   71372   453944     13486    6160    359 43019  292   461   47  63%     10  402  305   48  639%
c i   44.7   71360   453944     13487    6160    359 43019  292   460   47  63%     10  402  303   48  636%
c i   44.7   71347   453944     13488    6160    359 43019  292   460   47  63%     10  402  302   48  634%
c i   44.8   71337   453944     13491    6162    359 43019  292   460   47  63%     10  401  301   48  631%
c i   44.8   71327   453944     13496    6166    359 43019  292   460   47  63%     10  401  295   48  619%
c i   44.8   71320   453944     13497    6166    359 43019  292   460   47  63%     10  401  294   48  617%
c i   44.8   71312   453944     13498    6166    359 43019  291   460   47  63%     10  401  293   48  614%
c i   44.8   71302   453944     13509    6176    359 43019  291   461   47  63%      9  402  286   48  599%
c i   44.9   71295   453944     13550    6213    360 43019  289   462   47  63%      9  402  261   48  548%
c i   45.8   71294   453944     13993    6468    399 43026  280   459   47  61%      7  397  213   49  438%
c i   45.8   71293   453944     13996    6470    399 43026  280   459   47  61%      7  397  211   49  434%
c i   45.8   71292   453944     13998    6471    399 43026  279   459   47  61%      7  397  210   49  431%
c i   45.8   71291   453944     14003    6475    399 43026  279   459   47  61%      7  397  207   49  425%
c i   45.8   71290   453944     14004    6475    399 43026  279   459   47  61%      7  397  206   49  423%
c i   48.6   71289   453944     15531    6989    406 43033  313   485   53  65%     12  414  241   57  425%
c i   48.7   71284   453944     15560    7006    406 43033  313   485   53  64%     12  414  248   57  437%
c i   48.7   71278   453944     15561    7006    406 43033  313   485   53  64%     12  414  247   57  435%
c i   48.7   71273   453944     15562    7006    406 43033  313   485   53  64%     12  414  246   57  434%
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.7   71270   453944     15563    7006    406 43033  313   485   53  64%     12  413  245   57  432%
c i   48.7   71266   453944     15564    7006    406 43033  313   485   53  64%     12  413  244   57  430%
c i   48.7   71262   453944     15565    7006    406 43033  312   485   53  64%     11  413  243   57  429%
c i   48.7   71259   453944     15571    7007    406 43037  312   485   53  64%     11  413  240   57  422%
c i   48.7   71251   453944     15573    7007    406 43037  312   485   53  64%     11  413  240   57  423%
c i   48.8   71211   453944     15595    7019    406 43037  312   485   53  64%     11  413  247   57  435%
c i   49.3   71202   453944     15872    7136    405 43038  316   488   53  65%      9  414  328   58  564%
c i   49.3   71201   453944     15875    7138    405 43038  316   488   53  65%      9  414  327   58  562%
c i   49.3   71200   453944     15876    7138    405 43038  316   488   53  65%      9  414  326   58  560%
c i   49.3   71199   453944     15877    7138    405 43038  316   488   53  65%      9  414  324   58  558%
c i   51.3   71198   453944     16924    7533    406 43054  323   492   53  66%      8  412  234   63  372%
c i   51.4   71125   453944     16966    7563    406 43054  321   492   53  65%      8  412  227   63  360%
c i   52.1   71114   453944     17428    7901    408 43055  319   505   53  63%      6  422  274   65  425%
c i   52.2   71113   453944     17446    7906    408 43055  319   505   53  63%      6  422  276   65  426%
c i   52.2   71112   453944     17462    7918    408 43055  319   505   53  63%      6  421  274   65  424%
c i   52.2   71111   453944     17464    7919    408 43055  319   505   53  63%      6  421  273   65  422%
c i   52.2   71110   453944     17466    7920    408 43055  319   505   53  63%      6  421  272   65  421%
c i   52.3   71109   453944     17472    7923    408 43055  319   504   53  63%      6  421  271   65  420%
c i   52.3   71108   453944     17477    7927    408 43055  319   504   53  63%      6  421  270   65  418%
c i   52.3   71107   453944     17478    7927    408 43055  319   504   53  63%      5  421  269   65  416%
c i   55.6   71106   453944     19105    8557    408 43059  328   474   62  69%     12  381  348   71  487%
c i   55.6   71097   453944     19106    8557    408 43059  328   474   62  69%     12  381  347   71  485%
c i   55.8   71090   453944     19211    8607    409 43059  326   472   62  69%     11  378  322   72  449%
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   55.8   71081   453944     19212    8607    409 43059  326   472   62  69%     11  378  321   72  447%
c i   55.8   71072   453944     19213    8607    409 43059  326   471   62  69%     11  377  319   72  445%
c i   55.8   71067   453944     19228    8610    409 43059  326   471   62  69%     11  377  318   72  443%
c i   55.8   71058   453944     19229    8610    409 43059  326   471   62  69%     11  377  317   72  442%
c i   55.9   71049   453944     19288    8616    409 43059  326   469   62  69%     10  375  317   72  440%
c 
c [simplification-8] limit 24313 conflicts (hard 34079) hit after 24315 conflicts
c [quatres-4] found 34697 quaternary clauses 46% in total
c [ternres-4] limit 12606432 with penalty 0 = 0 + 0
c [ternres-4] all 71040 free variables schedulable
c [ternres-4] 19 ternary resolvents (0 bin, 19 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 416 variables
c [basicprobe-3] limit 63032164 penalty 0 = 0 + 0
c [basicprobe-3-0] 22990 probes remain 34% after last round
c [basicprobe-3-0] 507 units = 507 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 4128 variables, found 109059 hbrs
c [bate-1] eliminated 268 asymmetric tautologies during probing
c [unhide-8] limit 1260643 with penalty 1 = 0 + 1
c [unhide-8-8] 6 units, 905 failed, 16248 tauts, 0 hbrs, 58654 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 308 transitive binary clauses
c [transred-4] found 6 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 66082 variables 100%
c [block-3] limit of 63032164 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 118 blocked clauses
c [block-3] 118 < 1/100 * 424202 = 4242 considered unsuccessful
c [bca-4] limit of 10000000 steps and 830489 added (scaled 2)
c [bca-4] 116041 out of 132158 literals actually usable 88%
c [bca-4] added 83 blocked clauses in 338893 steps
c [sweep-4] limit 3781929 penalty 0 = 0 + 0
c [sweep-4-1] 3019 pos 4.6% + 62784 neg 95.4% = 65803 sched 99.6% ret 275
c [sweep-4-1] 3817715 steps 55 queries 10490.76 avg class size
c [sweep-4-1] 829 decisions 45 SAT calls 89.96 avg env size
c [sweep-4-1] 65175 variables remain 99% (814 retained 1%)
c [decomp-18] removed 261 variables
c [sweep-4-1] removed 261 vars (0 failed, 10 eqs, 18 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 261 vars in TOTAL (1 rounds, 54 queries)
c [phase-count-8] 411495 negative 99.4% of 414124 except 2629 0.6%
c [phase-count-8] 325471 positive 78.6% of 414124 except 88653 21.4%
c [phase-count-8] less non-negative clauses 2629 than limit 41400 (10.0%)
c [phase-count-8] non-pos/non-neg = 88653/2629 = 33.72 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 521 negative 100%
c [sort-queue-8] sorted 29468 enqueued variables after 24315 conflicts
c [score-dist-8] active 36349 (55%), one 0 (0%), zero 29468 (45%)
c [score-dist-8] max exp 516, different 16 (3%)
c [score-dist-8] median active exp 507, avg 507.2
c [simplification-8] removed 5223 variables 7.4% (65817 remain 31%)
c [simplification-8] removed 39820 irredundant clauses 8.8% (414124 remain 35%)
c [simplification-8] maximum reduction of 9% = max (7%, 9%)
c [simplification-8] large reduction 9% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 36315 (soft 26315 + delta 10000)
c [simplification-8] new conflict limit 26315 (hard 36315)
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.8   65816   414124     25081   10455    596 123831  311   379   56  82%     70  257  255   92  278%
c 
c [simplification-9] limit 26315 conflicts (hard 36315) hit after 26316 conflicts
c [ternres-5] limit 13528227 with penalty 0 = 0 + 0
c [ternres-5] all 65814 free variables schedulable
c [ternres-5] 23 ternary resolvents (0 bin, 23 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-19] removed 3 variables
c [simpleprobe-4] 3180 schedulable variables 5%
c [simpleprobe-4] limit 54112908 penalty 0 = 0 + 0
c [decomp-20] removed 1259 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 1259 variables, found 65320 hbrs, 518 units
c [unhide-9] limit 2705645 with penalty 0 = 0 + 0
c [unhide-9-10] 8 units, 267 failed, 39182 tauts, 0 hbrs, 203254 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 340 transitive binary clauses
c [transred-5] found 2 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 64275 variables 100%
c [elim-7] limit of 135282270 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 2055 variables 3% in round 1 in 34080367 steps
c [elim-7-1] backward subsumption/strengthening limit 34080300
c [elim-7-1-1] backward checking 7828 touched variables 12%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 36 and strengthened 153 clauses in 2032597 steps
c [elim-7-1] rescheduled 491 variables 1% by backward subsumption
c [elim-7-2] eliminated 53 variables 0% in round 2 in 373828 steps
c [elim-7-2] backward subsumption/strengthening limit 373800
c [elim-7-2-1] backward checking 453 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 41 and strengthened 21 clauses in 224972 steps
c [elim-7-2] rescheduled 95 variables 0% by backward subsumption
c [elim-7-3] eliminated 14 variables 0% in round 3 in 55872 steps
c [elim-7-3] backward subsumption/strengthening limit 55800
c [elim-7-3-1] backward checking 89 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 0 and strengthened 1 clauses in 55801 steps
c [elim-7] incomplete 4 not tried 0% in round 3
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 2131 = 3% variables out of 64275 scheduled
c [bca-5] limit of 10000000 steps and 770293 added (scaled 2)
c [bca-5] 110387 out of 124290 literals actually usable 89%
c [bca-5] added 142 blocked clauses in 320610 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 40584680 penalty 0 = 0 + 0
c [sweep-5-1] 3180 pos 5.2% + 58280 neg 94.8% = 61460 sched 98.9% ret 684
c [sweep-5-1] 40599489 steps 789 queries 725.21 avg class size
c [sweep-5-1] 5712 decisions 648 SAT calls 58.84 avg env size
c [sweep-5-1] 44201 variables remain 72% (17121 retained 28%)
c [decomp-21] removed 1241 variables
c [sweep-5-1] removed 1241 vars (1 failed, 173 eqs, 264 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1241 vars in TOTAL (1 rounds, 788 queries)
c [phase-count-9] 375137 negative 99.3% of 377740 except 2603 0.7%
c [phase-count-9] 292433 positive 77.4% of 377740 except 85307 22.6%
c [phase-count-9] less non-negative clauses 2603 than limit 37700 (10.0%)
c [phase-count-9] non-pos/non-neg = 85307/2603 = 32.77 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 376 negative 100%
c [sort-queue-9] sorted 21876 enqueued variables after 26316 conflicts
c [score-dist-9] active 39027 (64%), one 0 (0%), zero 21876 (36%)
c [score-dist-9] max exp 516, different 16 (3%)
c [score-dist-9] median active exp 506, avg 506.8
c [simplification-9] removed 4911 variables 7.5% (60903 remain 29%)
c [simplification-9] removed 36384 irredundant clauses 8.8% (377740 remain 32%)
c [simplification-9] maximum reduction of 9% = max (7%, 9%)
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 38316 (soft 28316 + delta 10000)
c [simplification-9] new conflict limit 28316 (hard 38316)
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   82.4   60902   377740     26382    4686    524 170027  308   375   39  82%     24  249  292   96  304%
c 
c [simplification-10] limit 28316 conflicts (hard 38316) hit after 28316 conflicts
c [quatres-5] found 32040 quaternary clauses 50% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-1] added 2 double-self-subsuming ternary resolvents
c [quatres-5-2] added 2 single-self-subsuming ternary resolvents
c [quatres-5-2] added 7 quaternary resolvents
c [ternres-6] limit 14555253 with penalty 0 = 0 + 0
c [ternres-6] all 60902 free variables schedulable
c [ternres-6] 447 ternary resolvents (1 bin, 446 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 909703 penalty 3 = 3 + 0
c [card-4] found 3137 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 909703 for elimination
c [card-4] 3137 out of 3137 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 727762 penalty 2 = 2 + 0
c [gauss-3] extracted 15 xors of average arity 3.0
c [gauss-3] connected 45 occurrences of 42 variables (average 1.1)
c [gauss-3] limit 727762 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 1 variables
c [treelook-4] limit 1455525 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 110047 literals 90%
c [treelook-4] scheduling used 1409393 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1455525 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 1499463 steps
c [treelook-4] 109996 literals remain 90%
c [treelook-4] 31715 variables remain to probed next time 52%
c [treelook-4] removed 9 variables, found 9031 hbrs
c [unhide-10] limit 2911050 with penalty 0 = 0 + 0
c [unhide-10-12] 28 units, 345 failed, 22786 tauts, 0 hbrs, 7280 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 391 transitive binary clauses
c [transred-6] found 2 units
c [cce-3] limit of 18194067 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 2 clauses out of 89 (2%) of length 10
c [cce-3-1] eliminated 1 clauses out of 353 (0%) of length 9
c [cce-3-1] eliminated 3 clauses out of 411 (1%) of length 8
c [cce-3-1] eliminated 13 clauses out of 652 (2%) of length 7
c [cce-3-1] eliminated 83 clauses out of 1473 (6%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 102 large clauses in 18194073 steps
c [cce-3-1] allowing another 9097036 steps for small clauses
c [cce-3-1] scheduling 205939 clauses = 188425 binary + 17514 ternary
c [cce-3-1] tried to eliminate 565 small clauses 0%
c [cce-3-1] eliminated 170 binary clauses 0%
c [cce-3-1] eliminated 31 ternary clauses 0%
c [cce-3-1] eliminated 201 small clauses 0%
c [cce-3-1] eliminated 860 small clauses in 18194072 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 962 covered clauses in round 1
c [cce-3] eliminated 962 covered clauses in TOTAL during 1 rounds
c [cce-3] 962 < 1/100 * 367500 = 3675 considered unsuccessful
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 60547 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 5822101520 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1946 variables 3% in round 1 in 33506804 steps
c [elim-8-1] backward subsumption/strengthening limit 33506800
c [elim-8-1-1] backward checking 7096 touched variables 12%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 33 and strengthened 136 clauses in 2096571 steps
c [elim-8-1] rescheduled 410 variables 1% by backward subsumption
c [elim-8-2] eliminated 51 variables 0% in round 2 in 1357815 steps
c [elim-8-2] backward subsumption/strengthening limit 1357800
c [elim-8-2-1] backward checking 395 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 15 and strengthened 9 clauses in 260935 steps
c [elim-8-2] rescheduled 47 variables 0% by backward subsumption
c [elim-8-3] eliminated 5 variables 0% in round 3 in 31461 steps
c [elim-8-3] backward subsumption/strengthening limit 31400
c [elim-8-3-1] backward checking 29 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 3 and strengthened 2 clauses in 31401 steps
c [elim-8] incomplete 13 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 2012 = 3% variables out of 60547 scheduled
c [bca-6] limit of 10000000 steps and 722146 added (scaled 2)
c [bca-6] 103865 out of 117072 literals actually usable 89%
c [bca-6] added 438 blocked clauses in 300948 steps
c [sweep-6] limit 4366576 penalty 0 = 0 + 0
c [sweep-6-1] 2402 pos 5.6% + 40149 neg 94.4% = 42551 sched 72.7% ret 15984
c [sweep-6-1] 4386212 steps 96 queries 3346.89 avg class size
c [sweep-6-1] 1339 decisions 83 SAT calls 116.40 avg env size
c [sweep-6-1] 41935 variables remain 72% (16594 retained 28%)
c [decomp-24] removed 44 variables
c [sweep-6-1] removed 44 vars (0 failed, 14 eqs, 26 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 44 vars in TOTAL (1 rounds, 95 queries)
c [phase-count-10] 358166 negative 99.3% of 360545 except 2379 0.7%
c [phase-count-10] 277735 positive 77.0% of 360545 except 82810 23.0%
c [phase-count-10] less non-negative clauses 2379 than limit 36000 (10.0%)
c [phase-count-10] non-pos/non-neg = 82810/2379 = 34.81 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 347 negative 100%
c [sort-queue-10] sorted 19722 enqueued variables after 28316 conflicts
c [score-dist-10] active 38769 (66%), one 0 (0%), zero 19722 (34%)
c [score-dist-10] max exp 516, different 16 (3%)
c [score-dist-10] median active exp 506, avg 506.9
c [simplification-10] removed 2411 variables 4.0% (58491 remain 27%)
c [simplification-10] removed 17195 irredundant clauses 4.6% (360545 remain 30%)
c [simplification-10] maximum reduction of 5% = max (4%, 5%)
c [simplification-10] large reduction 5% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 40316 (soft 30316 + delta 10000)
c [simplification-10] new conflict limit 30316 (hard 40316)
c 
c [simplification-11] limit 30316 conflicts (hard 40316) hit after 30316 conflicts
c [quatres-6] found 31778 quaternary clauses 50% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 4 single-self-subsuming ternary resolvents
c [quatres-6-2] added 14 quaternary resolvents
c [ternres-7] limit 15381441 with penalty 0 = 0 + 0
c [ternres-7] all 58491 free variables schedulable
c [ternres-7] 288 ternary resolvents (0 bin, 288 trn)
c [ternres-7] fully completed ternary resolution
c [basicprobe-4] limit 76907209 penalty 0 = 0 + 0
c [basicprobe-4-0] 17172 probes remain 30% after last round
c [basicprobe-4-0] 774 units = 759 failed (98%) + 15 lifted (2%)
c [basicprobe-4-0] removed 1509 variables, found 101476 hbrs
c [bate-2] eliminated 207 asymmetric tautologies during probing
c [unhide-11] limit 3076288 with penalty 0 = 0 + 0
c [unhide-11-14] 34 units, 260 failed, 20560 tauts, 0 hbrs, 7208 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 311 transitive binary clauses
c [transred-7] found 4 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 56652 variables 100%
c [block-4] limit of 38453604 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 111 blocked clauses
c [block-4] 111 < 1/100 * 348204 = 3482 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 56649 variables 100%
c [elim-9] limit of 307628837 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1524 variables 3% in round 1 in 32082260 steps
c [elim-9-1] backward subsumption/strengthening limit 32082200
c [elim-9-1-1] backward checking 5415 touched variables 10%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 75 and strengthened 203 clauses in 1498738 steps
c [elim-9-1] rescheduled 612 variables 1% by backward subsumption
c [elim-9-2] eliminated 71 variables 0% in round 2 in 475359 steps
c [elim-9-2] backward subsumption/strengthening limit 475300
c [elim-9-2-1] backward checking 492 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 21 and strengthened 15 clauses in 225325 steps
c [elim-9-2] rescheduled 84 variables 0% by backward subsumption
c [elim-9-3] eliminated 17 variables 0% in round 3 in 42029 steps
c [elim-9-3] backward subsumption/strengthening limit 42000
c [elim-9-3-1] backward checking 92 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 11 and strengthened 9 clauses in 42001 steps
c [elim-9] incomplete 45 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 1632 = 3% variables out of 56649 scheduled
c [bca-7] limit of 10000000 steps and 681603 added (scaled 2)
c [bca-7] 98215 out of 110036 literals actually usable 89%
c [bca-7] added 151 blocked clauses in 279878 steps
c [sweep-7] limit 4614432 penalty 0 = 0 + 0
c [sweep-7-1] 2440 pos 6.1% + 37329 neg 93.9% = 39769 sched 72.3% ret 15248
c [sweep-7-1] 4632907 steps 110 queries 4650.02 avg class size
c [sweep-7-1] 1131 decisions 95 SAT calls 65.37 avg env size
c [sweep-7-1] 38866 variables remain 71% (16122 retained 29%)
c [decomp-26] removed 142 variables
c [sweep-7-1] removed 142 vars (0 failed, 14 eqs, 26 impls)
c [sweep-7] removed 142 vars in TOTAL (1 rounds, 109 queries)
c [phase-count-11] 337545 negative 99.3% of 339828 except 2283 0.7%
c [phase-count-11] 260307 positive 76.6% of 339828 except 79521 23.4%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 80 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 17606 enqueued variables after 30316 conflicts
c [score-dist-11] active 37269 (68%), one 0 (0%), zero 17606 (32%)
c [score-dist-11] max exp 516, different 16 (3%)
c [score-dist-11] median active exp 506, avg 506.9
c [simplification-11] removed 3616 variables 6.2% (54875 remain 26%)
c [simplification-11] removed 20717 irredundant clauses 5.7% (339828 remain 29%)
c [simplification-11] maximum reduction of 6% = max (6%, 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 42316 (soft 32316 + delta 10000)
c [simplification-11] new conflict limit 32316 (hard 42316)
c 
c [simplification-12] limit 32316 conflicts (hard 42316) hit after 32321 conflicts
c [quatres-7] found 29435 quaternary clauses 51% in total
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [quatres-7-2] added 20 quaternary resolvents
c [ternres-8] limit 16138289 with penalty 0 = 0 + 0
c [ternres-8] all 54875 free variables schedulable
c [ternres-8] 364 ternary resolvents (0 bin, 364 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-27] removed 1 variables
c [simpleprobe-5] all 54874 free variables schedulable
c [simpleprobe-5] limit 64553157 penalty 0 = 0 + 0
c [decomp-28] removed 1545 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 1545 variables, found 54063 hbrs, 736 units
c [unhide-12] limit 3227657 with penalty 0 = 0 + 0
c [unhide-12-16] 10 units, 86 failed, 30686 tauts, 0 hbrs, 16652 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 361 transitive binary clauses
c [transred-8] found 2 units
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 53219 variables 100%
c [elim-10] limit of 322765786 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 1094 variables 2% in round 1 in 29113336 steps
c [elim-10-1] backward subsumption/strengthening limit 29113300
c [elim-10-1-1] backward checking 4620 touched variables 9%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 97 and strengthened 160 clauses in 1737526 steps
c [elim-10-1] rescheduled 532 variables 1% by backward subsumption
c [elim-10-2] eliminated 41 variables 0% in round 2 in 1834066 steps
c [elim-10-2] backward subsumption/strengthening limit 1834000
c [elim-10-2-1] backward checking 339 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 9 and strengthened 4 clauses in 188430 steps
c [elim-10-2] rescheduled 36 variables 0% by backward subsumption
c [elim-10-3] eliminated 3 variables 0% in round 3 in 27417 steps
c [elim-10-3] backward subsumption/strengthening limit 27400
c [elim-10-3-1] backward checking 28 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 5 and strengthened 3 clauses in 27401 steps
c [elim-10] incomplete 20 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 1141 = 2% variables out of 53219 scheduled
c [bca-8] limit of 10000000 steps and 638478 added (scaled 2)
c [bca-8] 92493 out of 104158 literals actually usable 89%
c [bca-8] added 165 blocked clauses in 265509 steps
c [sweep-8] limit 4841486 penalty 0 = 0 + 0
c [sweep-8-1] 2713 pos 7.3% + 34385 neg 92.7% = 37098 sched 71.2% ret 14980
c [sweep-8-1] 4887542 steps 135 queries 2126.76 avg class size
c [sweep-8-1] 1427 decisions 119 SAT calls 80.32 avg env size
c [sweep-8-1] 35765 variables remain 69% (16058 retained 31%)
c [decomp-29] removed 499 variables
c [sweep-8-1] removed 499 vars (0 failed, 19 eqs, 43 impls)
c [sweep-8] removed 499 vars in TOTAL (1 rounds, 134 queries)
c [phase-count-12] 314957 negative 99.3% of 317076 except 2119 0.7%
c [phase-count-12] 239913 positive 75.7% of 317076 except 77163 24.3%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 8 positive 73%, 3 negative 27%
c [sort-queue-12] sorted 14658 enqueued variables after 32321 conflicts
c [score-dist-12] active 36921 (72%), one 0 (0%), zero 14658 (28%)
c [score-dist-12] max exp 516, different 16 (3%)
c [score-dist-12] median active exp 507, avg 507.0
c [simplification-12] removed 3296 variables 6.0% (51579 remain 24%)
c [simplification-12] removed 22752 irredundant clauses 6.7% (317076 remain 27%)
c [simplification-12] maximum reduction of 7% = max (6%, 7%)
c [simplification-12] large reduction 7% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 44321 (soft 34321 + delta 10000)
c [simplification-12] new conflict limit 34321 (hard 44321)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  107.5   51578   317076     32859    3589   1104 223694  316   408   38  78%     77  257  301  116  259%
c i  107.9   51576   317076     33243    3888   1105 223696  303   412   38  73%     50  260  199  116  171%
c 
c [simplification-13] limit 34321 conflicts (hard 44321) hit after 34322 conflicts
c [quatres-8] found 26408 quaternary clauses 49% in total
c [quatres-8-2] added 1 single-self-subsuming ternary resolvents
c [quatres-8-2] added 7 quaternary resolvents
c [ternres-9] limit 16769755 with penalty 0 = 0 + 0
c [ternres-9] all 51469 free variables schedulable
c [ternres-9] 981 ternary resolvents (0 bin, 981 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-30] removed 113 variables
c [treelook-5] limit 1676975 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 92125 literals 90%
c [treelook-5] scheduling used 1298166 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 1676975 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1791692 steps
c [treelook-5] 92080 literals remain 89%
c [treelook-5] 25554 variables remain to probed next time 50%
c [treelook-5] removed 8 variables, found 10136 hbrs
c [unhide-13] limit 3353951 with penalty 0 = 0 + 0
c [unhide-13-18] 5 units, 76 failed, 15877 tauts, 0 hbrs, 40736 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 305 transitive binary clauses
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 51405 variables 100%
c [elim-11] limit of 335395107 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 533 variables 1% in round 1 in 28391113 steps
c [elim-11-1] backward subsumption/strengthening limit 28391100
c [elim-11-1-1] backward checking 2172 touched variables 4%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 31 and strengthened 45 clauses in 761619 steps
c [elim-11-1] rescheduled 163 variables 0% by backward subsumption
c [elim-11-2] eliminated 28 variables 0% in round 2 in 276104 steps
c [elim-11-2] backward subsumption/strengthening limit 276100
c [elim-11-2-1] backward checking 187 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 29 and strengthened 18 clauses in 176077 steps
c [elim-11-2] rescheduled 61 variables 0% by backward subsumption
c [elim-11-3] eliminated 8 variables 0% in round 3 in 136435 steps
c [elim-11-3] backward subsumption/strengthening limit 136400
c [elim-11-3-1] backward checking 61 touched variables 0%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 5 and strengthened 5 clauses in 109279 steps
c [elim-11] incomplete 21 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 573 = 1% variables out of 51405 scheduled
c [bca-9] limit of 10000000 steps and 624251 added (scaled 2)
c [bca-9] 89389 out of 101666 literals actually usable 88%
c [bca-9] added 129 blocked clauses in 253232 steps
c [sweep-9] limit 5030926 penalty 0 = 0 + 0
c [sweep-9-1] 2617 pos 7.5% + 32469 neg 92.5% = 35086 sched 69.0% ret 15746
c [sweep-9-1] 5117172 steps 139 queries 2475.69 avg class size
c [sweep-9-1] 1290 decisions 123 SAT calls 55.59 avg env size
c [sweep-9-1] 33881 variables remain 67% (16905 retained 33%)
c [decomp-32] removed 123 variables
c [sweep-9-1] removed 123 vars (0 failed, 16 eqs, 28 impls)
c [sweep-9] removed 123 vars in TOTAL (1 rounds, 138 queries)
c [phase-count-13] 309183 negative 99.4% of 311169 except 1986 0.6%
c [phase-count-13] 235169 positive 75.6% of 311169 except 76000 24.4%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 3 positive 75%, 1 negative 25%
c [sort-queue-13] sorted 13965 enqueued variables after 34322 conflicts
c [score-dist-13] active 36744 (72%), one 0 (0%), zero 13965 (28%)
c [score-dist-13] max exp 516, different 16 (3%)
c [score-dist-13] median active exp 507, avg 507.1
c [simplification-13] removed 760 variables 1.5% (50709 remain 24%)
c [simplification-13] removed 5907 irredundant clauses 1.9% (311169 remain 26%)
c [simplification-13] maximum reduction of 2% = max (1%, 2%)
c [simplification-13] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-13] new conflict interval 18332
c [simplification-13] penalized conflict interval 18332 = 1 * 18332
c [simplification-13] hard conflict limit 62654 (soft 52654 + delta 10000)
c [simplification-13] new conflict limit 52654 (hard 62654)
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  112.7   50708   311169     34405    4209   1803 217813  316   418   38  76%     17  261  391  120  325%
c i  112.7   50702   311169     34406    4209   1803 217813  316   418   38  76%     17  261  390  120  324%
c i  114.2   50698   311169     35392    4533   1805 217815  335   428   40  78%      6  268  418  125  335%
c i  114.2   50697   311169     35393    4533   1805 217815  335   428   40  78%      6  268  416  125  334%
c i  114.2   50696   311169     35394    4533   1805 217815  335   428   40  78%      6  268  414  125  332%
c i  114.2   50695   311169     35395    4533   1805 217815  335   428   40  78%      6  268  413  125  331%
c i  114.2   50694   311169     35401    4538   1805 217815  335   428   40  78%      6  268  403  125  323%
c i  114.2   50693   311169     35402    4538   1805 217815  335   428   40  78%      6  267  402  125  322%
c i  114.2   50692   311169     35403    4538   1805 217815  334   428   40  78%      6  267  400  125  321%
c i  114.7   50691   311169     35823    4854   1808 217830  322   432   40  75%      2  270  249  125  199%
c i  114.7   50690   311169     35824    4854   1808 217830  322   432   40  75%      2  270  248  125  198%
c i  123.3   50681   311169     40765    6367   1810 217834  384   479   52  80%     50  296  254  146  174%
c i  127.4   50674   311169     43442    7368   1813 217847  396   486   69  81%     19  291  392  157  250%
c i  127.5   50673   311169     43456    7377   1814 217848  396   486   69  81%     19  291  383  157  244%
c i  129.0   50672   311169     44357    7574   1815 217852  388   469   69  83%      5  270  367  159  230%
c i  129.1   50671   311169     44403    7574   1815 217852  388   468   69  83%      5  268  365  160  229%
c i  131.8   50670   311169     46197    8140   1815 217855  390   456   69  85%      6  249  387  166  233%
c i  132.2   50669   311169     46520    8330   1815 217859  379   457   69  83%      1  249  278  166  167%
c i  132.2   50668   311169     46522    8330   1815 217860  379   457   69  83%      1  249  276  166  166%
c i  132.2   50667   311169     46535    8341   1815 217861  378   457   69  83%      1  249  263  166  158%
c i  132.2   50666   311169     46536    8341   1815 217861  378   457   69  83%      1  249  262  166  157%
c i  132.2   50665   311169     46569    8373   1815 217861  375   458   69  82%      1  250  234  166  141%
c i  132.2   50664   311169     46571    8374   1815 217861  375   458   69  82%      1  250  232  166  140%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  132.2   50663   311169     46573    8375   1815 217861  375   458   69  82%      1  249  231  166  139%
c i  132.2   50662   311169     46575    8376   1815 217861  375   458   69  82%      1  249  229  166  138%
c i  132.4   50661   311169     46654    8442   1815 217861  370   459   69  81%     -0  250  210  166  126%
c i  132.9   50660   311169     46964    8659   1815 217861  362   459   69  79%     -3  249  254  167  152%
c i  132.9   50659   311169     46967    8661   1815 217861  362   459   69  79%     -3  249  251  167  151%
c i  132.9   50658   311169     46982    8675   1815 217861  362   459   69  79%     -3  249  250  167  150%
c i  137.1   50657   311169     49599    9613   1815 217861  390   463   69  84%     15  243  428  176  243%
c i  137.1   50656   311169     49627    9635   1815 217861  388   463   69  84%     14  244  401  176  227%
c i  137.1   50655   311169     49628    9635   1815 217861  388   463   69  84%     14  243  399  176  227%
c i  137.1   50654   311169     49629    9635   1815 217861  388   463   69  84%     14  243  398  176  226%
c i  137.1   50653   311169     49634    9639   1815 217861  388   463   69  84%     14  243  392  176  222%
c i  140.5   50652   311169     52144   10299   1820 217870  383   459   70  84%     14  230  353  184  192%
c 
c [simplification-14] limit 52780 conflicts (hard 62654) hit after 52780 conflicts
c [quatres-9] found 25522 quaternary clauses 49% in total
c [quatres-9-2] added 1 quaternary resolvents
c [ternres-10] limit 23614198 with penalty 0 = 0 + 0
c [ternres-10] all 50651 free variables schedulable
c [ternres-10] 352 ternary resolvents (1 bin, 351 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 590354 penalty 3 = 3 + 0
c [gauss-4] extracted 16 xors of average arity 3.0
c [gauss-4] connected 48 occurrences of 45 variables (average 1.1)
c [gauss-4] limit 590354 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-33] removed 2 variables
c [basicprobe-5] limit 118070990 penalty 0 = 0 + 0
c [basicprobe-5-0] 9396 probes remain 19% after last round
c [basicprobe-5-0] 1148 units = 1144 failed (100%) + 4 lifted (0%)
c [basicprobe-5-0] removed 1769 variables, found 146656 hbrs
c [bate-3] eliminated 440 asymmetric tautologies during probing
c [unhide-14] limit 4722839 with penalty 0 = 0 + 0
c [unhide-14-21] 6 units, 253 failed, 33444 tauts, 0 hbrs, 83795 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 297 transitive binary clauses
c [transred-10] found 2 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 147588737 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 4 clauses out of 48 (8%) of length 10
c [cce-4-1] eliminated 1 clauses out of 294 (0%) of length 8
c [cce-4-1] eliminated 9 clauses out of 487 (2%) of length 7
c [cce-4-1] eliminated 38 clauses out of 1382 (3%) of length 6
c [cce-4-1] eliminated 12626 clauses out of 19599 (64%) of length 5
c [cce-4-1] eliminated 6105 clauses out of 24839 (25%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 18783 large clauses in 147588740 steps
c [cce-4-1] allowing another 73794370 steps for small clauses
c [cce-4-1] scheduling 171888 clauses = 155513 binary + 16375 ternary
c [cce-4-1] tried to eliminate 7834 small clauses 5%
c [cce-4-1] eliminated 1864 binary clauses 1%
c [cce-4-1] eliminated 359 ternary clauses 2%
c [cce-4-1] eliminated 2223 small clauses 1%
c [cce-4-1] eliminated 2664 small clauses in 147588740 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 21447 covered clauses in round 1
c [cce-4] eliminated 21447 covered clauses in TOTAL during 1 rounds
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 48726 variables 100%
c [elim-12] limit of 472283961 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 11068 variables 23% in round 1 in 23645675 steps
c [elim-12-1] backward subsumption/strengthening limit 23645600
c [elim-12-1-1] backward checking 27268 touched variables 56%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 69 and strengthened 247 clauses in 4025654 steps
c [elim-12-1] rescheduled 710 variables 1% by backward subsumption
c [elim-12-2] eliminated 59 variables 0% in round 2 in 1813371 steps
c [elim-12-2] backward subsumption/strengthening limit 1813300
c [elim-12-2-1] backward checking 541 touched variables 1%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 15 and strengthened 17 clauses in 505552 steps
c [elim-12-2] rescheduled 84 variables 0% by backward subsumption
c [elim-12-3] eliminated 9 variables 0% in round 3 in 74737 steps
c [elim-12-3] backward subsumption/strengthening limit 74700
c [elim-12-3-1] backward checking 77 touched variables 0%
c [elim-12-3-1] incomplete backward checking 0 remain 0%
c [elim-12-3] subsumed 2 and strengthened 6 clauses in 74701 steps
c [elim-12] incomplete 28 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 11136 = 23% variables out of 48726 scheduled
c [bca-10] limit of 10000000 steps and 497167 added (scaled 2)
c [bca-10] 71059 out of 75182 literals actually usable 95%
c [bca-10] added 151 blocked clauses in 168760 steps
c [sweep-10] limit 7084259 penalty 0 = 0 + 0
c [sweep-10-1] 2444 pos 8.9% + 24923 neg 91.1% = 27367 sched 72.8% ret 10223
c [sweep-10-1] 7090760 steps 260 queries 1399.92 avg class size
c [sweep-10-1] 2652 decisions 235 SAT calls 60.57 avg env size
c [sweep-10-1] 25217 variables remain 67% (12317 retained 33%)
c [decomp-34] removed 199 variables
c [sweep-10-1] removed 199 vars (0 failed, 31 eqs, 45 impls)
c [sweep-10] removed 199 vars in TOTAL (1 rounds, 259 queries)
c [phase-count-14] 246129 negative 99.6% of 247196 except 1067 0.4%
c [phase-count-14] 176998 positive 71.6% of 247196 except 70198 28.4%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 4 positive 15%, 22 negative 85%
c [sort-queue-14] sorted 8684 enqueued variables after 52780 conflicts
c [score-dist-14] active 28707 (77%), one 0 (0%), zero 8684 (23%)
c [score-dist-14] max exp 517, different 17 (3%)
c [score-dist-14] median active exp 507, avg 507.4
c [simplification-14] removed 13260 variables 26.2% (37391 remain 18%)
c [simplification-14] removed 63973 irredundant clauses 20.6% (247196 remain 21%)
c [simplification-14] maximum reduction of 26% = max (26%, 21%)
c [simplification-14] large reduction 26% >= 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 64780 (soft 54780 + delta 10000)
c [simplification-14] new conflict limit 54780 (hard 64780)
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  155.4   37390   247196     53840    1798   2284 257948  312   431   32  72%      6  197   99  184   54%
c 
c [simplification-15] limit 54780 conflicts (hard 64780) hit after 54853 conflicts
c [quatres-10] found 23856 quaternary clauses 70% in total
c [quatres-10-2] added 7 single-self-subsuming ternary resolvents
c [quatres-10-2] added 15 quaternary resolvents
c [ternres-11] limit 23910972 with penalty 0 = 0 + 0
c [ternres-11] all 37378 free variables schedulable
c [ternres-11] 709 ternary resolvents (0 bin, 709 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 747217 penalty 4 = 4 + 0
c [card-5] found 1592 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 747217 for elimination
c [card-5] 1592 out of 1592 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-35] removed 13 variables
c [simpleprobe-6] all 37378 free variables schedulable
c [simpleprobe-6] limit 95643889 penalty 0 = 0 + 0
c [decomp-36] removed 355 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 355 variables, found 61163 hbrs, 207 units
c [unhide-15] limit 4782194 with penalty 0 = 0 + 0
c [unhide-15-25] 2 units, 153 failed, 40666 tauts, 0 hbrs, 15515 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 457 transitive binary clauses
c [transred-11] found 3 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 36923 variables 100%
c [block-5] limit of 29888715 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 145 blocked clauses
c [block-5] 145 < 1/100 * 240141 = 2401 considered unsuccessful
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 36919 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 516 variables 1% in round 1 in 21049174 steps
c [elim-13-1] backward subsumption/strengthening limit 21049100
c [elim-13-1-1] backward checking 3290 touched variables 9%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 26 and strengthened 57 clauses in 886828 steps
c [elim-13-1] rescheduled 205 variables 1% by backward subsumption
c [elim-13-2] eliminated 13 variables 0% in round 2 in 303101 steps
c [elim-13-2] backward subsumption/strengthening limit 303100
c [elim-13-2-1] backward checking 155 touched variables 0%
c [elim-13-2-1] incomplete backward checking 33 remain 21%
c [elim-13-2] subsumed 14 and strengthened 4 clauses in 303140 steps
c [elim-13-2] rescheduled 40 variables 0% by backward subsumption
c [elim-13-3] eliminated 4 variables 0% in round 3 in 903541 steps
c [elim-13-3] backward subsumption/strengthening limit 903500
c [elim-13-3-1] backward checking 71 touched variables 0%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 6 and strengthened 5 clauses in 104841 steps
c [elim-13] incomplete 23 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 533 = 1% variables out of 36919 scheduled
c [bca-11] limit of 10000000 steps and 477713 added (scaled 2)
c [bca-11] 66160 out of 72774 literals actually usable 91%
c [bca-11] added 63 blocked clauses in 157435 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 71732910 penalty 0 = 0 + 0
c [sweep-11-1] 2283 pos 9.3% + 22280 neg 90.7% = 24563 sched 67.5% ret 11823
c [sweep-11-1] 71765158 steps 2936 queries 105.63 avg class size
c [sweep-11-1] 14349 decisions 2531 SAT calls 55.13 avg env size
c [sweep-11-1] 7566 variables remain 21% (28379 retained 79%)
c [decomp-37] removed 1268 variables
c [sweep-11-1] removed 1268 vars (0 failed, 433 eqs, 795 impls)
c [sweep-11] removed 1268 vars in TOTAL (1 rounds, 2935 queries)
c [phase-count-15] 233457 negative 99.6% of 234471 except 1014 0.4%
c [phase-count-15] 166218 positive 70.9% of 234471 except 68253 29.1%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 4 positive 44%, 5 negative 56%
c [sort-queue-15] sorted 6539 enqueued variables after 54853 conflicts
c [score-dist-15] active 28579 (81%), one 0 (0%), zero 6539 (19%)
c [score-dist-15] max exp 517, different 17 (3%)
c [score-dist-15] median active exp 507, avg 507.5
c [simplification-15] removed 2260 variables 6.0% (35118 remain 16%)
c [simplification-15] removed 12725 irredundant clauses 5.1% (234471 remain 20%)
c [simplification-15] maximum reduction of 6% = max (6%, 5%)
c [simplification-15] large reduction 6% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 66853 (soft 56853 + delta 10000)
c [simplification-15] new conflict limit 56853 (hard 66853)
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  163.4   35117   234471     55828    3650   2613 324019  252   404   35  62%      7  164  185  183  101%
c 
c [simplification-16] limit 56853 conflicts (hard 66853) hit after 56856 conflicts
c [quatres-11] found 22329 quaternary clauses 68% in total
c [quatres-11-1] removed 2 duplicate quaternary clauses
c [quatres-11-2] added 5 single-self-subsuming ternary resolvents
c [quatres-11-2] added 8 quaternary resolvents
c [ternres-12] limit 24155260 with penalty 0 = 0 + 0
c [ternres-12] all 35117 free variables schedulable
c [ternres-12] 695 ternary resolvents (1 bin, 694 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-38] removed 5 variables
c [treelook-6] limit 2415526 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 56866 literals 81%
c [treelook-6] scheduling used 1130086 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 2415526 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 2423858 steps
c [treelook-6] 56787 literals remain 81%
c [treelook-6] 12913 variables remain to probed next time 37%
c [decomp-39] removed 1 variables
c [treelook-6] removed 5 variables, found 18886 hbrs
c [unhide-16] limit 4831052 with penalty 0 = 0 + 0
c [unhide-16-28] 11 units, 221 failed, 50819 tauts, 0 hbrs, 57811 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 467 transitive binary clauses
c [cce-5] limit of 30194075 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 10
c [cce-5-1] eliminated 1 clauses out of 6 (17%) of length 8
c [cce-5-1] eliminated 4 clauses out of 14 (29%) of length 7
c [cce-5-1] eliminated 45 clauses out of 1298 (3%) of length 6
c [cce-5-1] eliminated 22 clauses out of 7663 (0%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 73 large clauses in 30194076 steps
c [cce-5-1] allowing another 15097038 steps for small clauses
c [cce-5-1] scheduling 130415 clauses = 115507 binary + 14908 ternary
c [cce-5-1] tried to eliminate 1858 small clauses 1%
c [cce-5-1] eliminated 483 binary clauses 0%
c [cce-5-1] eliminated 88 ternary clauses 1%
c [cce-5-1] eliminated 571 small clauses 0%
c [cce-5-1] eliminated 1018 small clauses in 30194082 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1091 covered clauses in round 1
c [cce-5] eliminated 1091 covered clauses in TOTAL during 1 rounds
c [cce-5] 1091 < 1/100 * 230650 = 2306 considered unsuccessful
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 34935 variables 100%
c [elim-14] limit of 483105212 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 594 variables 2% in round 1 in 20697113 steps
c [elim-14-1] backward subsumption/strengthening limit 20697100
c [elim-14-1-1] backward checking 3480 touched variables 10%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 38 and strengthened 64 clauses in 969360 steps
c [elim-14-1] rescheduled 263 variables 1% by backward subsumption
c [elim-14-2] eliminated 17 variables 0% in round 2 in 276274 steps
c [elim-14-2] backward subsumption/strengthening limit 276200
c [elim-14-2-1] backward checking 151 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 5 and strengthened 9 clauses in 100152 steps
c [elim-14-2] rescheduled 33 variables 0% by backward subsumption
c [elim-14-3] eliminated 3 variables 0% in round 3 in 40868 steps
c [elim-14-3] backward subsumption/strengthening limit 40800
c [elim-14-3-1] backward checking 41 touched variables 0%
c [elim-14-3-1] incomplete backward checking 0 remain 0%
c [elim-14-3] subsumed 0 and strengthened 2 clauses in 40801 steps
c [elim-14] incomplete 8 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 621 = 2% variables out of 34935 scheduled
c [bca-12] limit of 10000000 steps and 455436 added (scaled 2)
c [bca-12] 59410 out of 68630 literals actually usable 87%
c [bca-12] added 62 blocked clauses in 140583 steps
c [sweep-12] limit 7246578 penalty 0 = 0 + 0
c [sweep-12-1] 702 pos 10.2% + 6193 neg 89.8% = 6895 sched 20.1% ret 27419
c [sweep-12-1] 7247040 steps 399 queries 229.39 avg class size
c [sweep-12-1] 2079 decisions 338 SAT calls 56.48 avg env size
c [sweep-12-1] 5918 variables remain 17% (28323 retained 83%)
c [decomp-40] removed 243 variables
c [sweep-12-1] removed 243 vars (0 failed, 68 eqs, 126 impls)
c [sweep-12] removed 243 vars in TOTAL (1 rounds, 398 queries)
c [phase-count-16] 225480 negative 99.6% of 226434 except 954 0.4%
c [phase-count-16] 160290 positive 70.8% of 226434 except 66144 29.2%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 7 positive 78%, 2 negative 22%
c [sort-queue-16] sorted 6225 enqueued variables after 56856 conflicts
c [score-dist-16] active 27846 (82%), one 0 (0%), zero 6225 (18%)
c [score-dist-16] max exp 517, different 17 (3%)
c [score-dist-16] median active exp 507, avg 507.6
c [simplification-16] removed 1046 variables 3.0% (34071 remain 16%)
c [simplification-16] removed 8037 irredundant clauses 3.4% (226434 remain 19%)
c [simplification-16] maximum reduction of 3% = max (3%, 3%)
c [simplification-16] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-16] new conflict interval 23332
c [simplification-16] penalized conflict interval 23332 = 1 * 23332
c [simplification-16] hard conflict limit 91854 (soft 80188 + delta 11666)
c [simplification-16] new conflict limit 80188 (hard 91854)
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.0   34070   226434     56857    3527   2986 286006  249   398   32  63%      0  156  199  184  109%
c i  168.0   34067   226434     56924    3584   2988 286006  247   397   33  62%     -0  155  190  183  104%
c i  168.1   34066   226434     57028    3652   2989 286007  246   397   34  62%     -1  155  189  183  103%
c i  172.8   34064   226434     63765    6151   3007 286045  212   299   41  71%     74   46  131  187   70%
c i  175.2   34063   226434     68623    7079   3008 286050  245   281   47  87%     43   26  244  192  127%
c i  180.1   34062   226434     77312    9408   3023 286079  241   326   59  74%     97   66  240  199  121%
c i  180.9   34059   226434     78854   10290   3028 286088  220   340   60  65%     14   78  215  198  109%
c 
c [simplification-17] limit 80188 conflicts (hard 91854) hit after 80993 conflicts
c [quatres-12] found 21276 quaternary clauses 67% in total
c [quatres-12-1] removed 1 duplicate quaternary clauses
c [quatres-12-2] added 1 single-self-subsuming ternary resolvents
c [quatres-12-2] added 5 quaternary resolvents
c [ternres-13] limit 27452248 with penalty 0 = 0 + 0
c [ternres-13] all 34057 free variables schedulable
c [ternres-13] 410 ternary resolvents (1 bin, 409 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-41] removed 16 variables
c [basicprobe-6] limit 137261240 penalty 0 = 0 + 0
c [basicprobe-6-0] 9485 sched 29%, 797 failed, 71 lifted, 159893 hbrs
c [decomp-42] removed 1577 variables
c [basicprobe-6-1] 9672 probes remain 30% after last round
c [basicprobe-6-1] 905 units = 834 failed (92%) + 71 lifted (8%)
c [basicprobe-6-1] removed 1622 variables, found 166887 hbrs
c [bate-4] eliminated 960 asymmetric tautologies during probing
c [unhide-17] limit 5490449 with penalty 0 = 0 + 0
c [unhide-17-32] 1 units, 72 failed, 58362 tauts, 0 hbrs, 150015 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 425 transitive binary clauses
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 32379 variables 100%
c [elim-15] limit of 549044961 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 1053 variables 3% in round 1 in 17756107 steps
c [elim-15-1] backward subsumption/strengthening limit 17756100
c [elim-15-1-1] backward checking 5101 touched variables 16%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 25 and strengthened 88 clauses in 1120553 steps
c [elim-15-1] rescheduled 315 variables 1% by backward subsumption
c [elim-15-2] eliminated 26 variables 0% in round 2 in 882067 steps
c [elim-15-2] backward subsumption/strengthening limit 882000
c [elim-15-2-1] backward checking 289 touched variables 1%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 15 and strengthened 14 clauses in 195673 steps
c [elim-15-2] rescheduled 72 variables 0% by backward subsumption
c [elim-15-3] eliminated 4 variables 0% in round 3 in 740765 steps
c [elim-15-3] backward subsumption/strengthening limit 740700
c [elim-15-3-1] backward checking 46 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 8 and strengthened 2 clauses in 87451 steps
c [elim-15] incomplete 17 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 1083 = 3% variables out of 32379 scheduled
c [bca-13] limit of 10000000 steps and 404887 added (scaled 2)
c [bca-13] 51950 out of 62594 literals actually usable 83%
c [bca-13] added 45 blocked clauses in 124114 steps
c [sweep-13] limit 8235674 penalty 0 = 0 + 0
c [sweep-13-1] 563 pos 10.8% + 4669 neg 89.2% = 5232 sched 16.7% ret 26064
c [sweep-13-1] 8255455 steps 485 queries 165.69 avg class size
c [sweep-13-1] 2680 decisions 419 SAT calls 56.21 avg env size
c [sweep-13-1] 4093 variables remain 13% (27172 retained 87%)
c [decomp-43] removed 185 variables
c [sweep-13-1] removed 185 vars (0 failed, 67 eqs, 120 impls)
c [sweep-13] removed 185 vars in TOTAL (1 rounds, 484 queries)
c [phase-count-17] 200499 negative 99.5% of 201417 except 918 0.5%
c [phase-count-17] 141214 positive 70.1% of 201417 except 60203 29.9%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 2 positive 50%, 2 negative 50%
c [sort-queue-17] sorted 5033 enqueued variables after 80993 conflicts
c [score-dist-17] active 26078 (84%), one 0 (0%), zero 5033 (16%)
c [score-dist-17] max exp 517, different 17 (3%)
c [score-dist-17] median active exp 508, avg 508.1
c [simplification-17] removed 2946 variables 8.7% (31111 remain 15%)
c [simplification-17] removed 25017 irredundant clauses 11.0% (201417 remain 17%)
c [simplification-17] maximum reduction of 11% = max (9%, 11%)
c [simplification-17] large reduction 11% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 92993 (soft 82993 + delta 10000)
c [simplification-17] new conflict limit 82993 (hard 92993)
c 
c [simplification-18] limit 82993 conflicts (hard 92993) hit after 82999 conflicts
c [quatres-13] found 18766 quaternary clauses 66% in total
c [quatres-13-2] added 3 single-self-subsuming ternary resolvents
c [quatres-13-2] added 26 quaternary resolvents
c [ternres-14] limit 27797686 with penalty 0 = 0 + 0
c [ternres-14] all 31111 free variables schedulable
c [ternres-14] 573 ternary resolvents (1 bin, 572 trn)
c [ternres-14] fully completed ternary resolution
c [simpleprobe-7] all 31111 free variables schedulable
c [simpleprobe-7] limit 111190745 penalty 0 = 0 + 0
c [decomp-45] removed 153 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 153 variables, found 91219 hbrs, 52 units
c [unhide-18] limit 5559537 with penalty 0 = 0 + 0
c [unhide-18-36] 4 units, 32 failed, 86640 tauts, 0 hbrs, 59199 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 502 transitive binary clauses
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 30933 variables 100%
c [elim-16] limit of 555953727 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 328 variables 1% in round 1 in 17801149 steps
c [elim-16-1] backward subsumption/strengthening limit 17801100
c [elim-16-1-1] backward checking 2089 touched variables 7%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 18 and strengthened 55 clauses in 729964 steps
c [elim-16-1] rescheduled 161 variables 1% by backward subsumption
c [elim-16-2] eliminated 13 variables 0% in round 2 in 1064499 steps
c [elim-16-2] backward subsumption/strengthening limit 1064400
c [elim-16-2-1] backward checking 131 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 10 and strengthened 5 clauses in 181080 steps
c [elim-16-2] rescheduled 30 variables 0% by backward subsumption
c [elim-16-3] eliminated 4 variables 0% in round 3 in 193979 steps
c [elim-16-3] backward subsumption/strengthening limit 193900
c [elim-16-3-1] backward checking 26 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 0 and strengthened 2 clauses in 48547 steps
c [elim-16] incomplete 8 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 345 = 1% variables out of 30933 scheduled
c [bca-14] limit of 10000000 steps and 395310 added (scaled 2)
c [bca-14] 50504 out of 61178 literals actually usable 83%
c [bca-14] added 23 blocked clauses in 120260 steps
c [sweep-14] limit 8339305 penalty 0 = 0 + 0
c [sweep-14-1] 387 pos 9.9% + 3522 neg 90.1% = 3909 sched 12.8% ret 26679
c [sweep-14-1] 8341634 steps 542 queries 96.78 avg class size
c [sweep-14-1] 2575 decisions 472 SAT calls 47.44 avg env size
c [sweep-14-1] 2877 variables remain 9% (27697 retained 91%)
c [decomp-46] removed 153 variables
c [sweep-14-1] removed 153 vars (0 failed, 71 eqs, 125 impls)
c [sweep-14] removed 153 vars in TOTAL (1 rounds, 541 queries)
c [phase-count-18] 195649 negative 99.5% of 196554 except 905 0.5%
c [phase-count-18] 137394 positive 69.9% of 196554 except 59160 30.1%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-18] sorted 4615 enqueued variables after 82999 conflicts
c [score-dist-18] active 25820 (85%), one 0 (0%), zero 4615 (15%)
c [score-dist-18] max exp 517, different 17 (3%)
c [score-dist-18] median active exp 508, avg 508.2
c [simplification-18] removed 676 variables 2.2% (30435 remain 14%)
c [simplification-18] removed 4863 irredundant clauses 2.4% (196554 remain 16%)
c [simplification-18] maximum reduction of 2% = max (2%, 2%)
c [simplification-18] geometric conflict interval increment 7777 = 23332 / 3
c [simplification-18] new conflict interval 31109
c [simplification-18] penalized conflict interval 31109 = 1 * 31109
c [simplification-18] hard conflict limit 129662 (soft 114108 + delta 15554)
c [simplification-18] new conflict limit 114108 (hard 129662)
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  197.7   30434   196554     84941    7185   3309 346441  264   336   38  79%     54   67  251  206  122%
c i  204.2   30433   196554     94924   10276   3317 346470  248   322   57  77%    108   45  152  213   71%
c i  206.4   30417   196554     98496   11834   3320 346478  241   315   58  77%     11   36  229  214  107%
c 
c [simplification-19] limit 114108 conflicts (hard 129662) hit after 120868 conflicts
c [quatres-14] found 18590 quaternary clauses 65% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [quatres-14-2] added 1 single-self-subsuming ternary resolvents
c [quatres-14-2] added 12 quaternary resolvents
c [ternres-15] limit 33104043 with penalty 0 = 0 + 0
c [ternres-15] all 30416 free variables schedulable
c [ternres-15] 266 ternary resolvents (2 bin, 264 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 413800 penalty 4 = 4 + 0
c [gauss-5] extracted 22 xors of average arity 2.8
c [gauss-5] connected 61 occurrences of 58 variables (average 1.1)
c [gauss-5] limit 413800 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-47] removed 20 variables
c [treelook-7] limit 3310404 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 49484 literals 81%
c [treelook-7] scheduling used 1095107 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 3310404 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 3321793 steps
c [treelook-7] 49357 literals remain 81%
c [treelook-7] 10826 variables remain to probed next time 36%
c [treelook-7] removed 13 variables, found 3370 hbrs
c [unhide-19] limit 6620808 with penalty 0 = 0 + 0
c [unhide-19-41] 2 units, 21 failed, 37850 tauts, 0 hbrs, 153891 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 445 transitive binary clauses
c [cce-6] limit of 20690027 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) 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 1 (100%) 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 1 (100%) of length 43
c [cce-6-1] eliminated 3 clauses out of 3 (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 3 (67%) of length 40
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 39
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 38
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 37
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 36
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 35
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 34
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 33
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 32
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 31
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 30
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 29
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 28
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 27
c [cce-6-1] eliminated 7 clauses out of 9 (78%) of length 26
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 25
c [cce-6-1] eliminated 9 clauses out of 10 (90%) of length 24
c [cce-6-1] eliminated 6 clauses out of 10 (60%) of length 23
c [cce-6-1] eliminated 7 clauses out of 8 (88%) of length 22
c [cce-6-1] eliminated 8 clauses out of 10 (80%) of length 21
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 20
c [cce-6-1] eliminated 9 clauses out of 10 (90%) of length 19
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 18
c [cce-6-1] eliminated 10 clauses out of 11 (91%) of length 17
c [cce-6-1] eliminated 8 clauses out of 15 (53%) of length 16
c [cce-6-1] eliminated 10 clauses out of 14 (71%) of length 15
c [cce-6-1] eliminated 12 clauses out of 16 (75%) of length 14
c [cce-6-1] eliminated 11 clauses out of 16 (69%) of length 13
c [cce-6-1] eliminated 14 clauses out of 17 (82%) of length 12
c [cce-6-1] eliminated 13 clauses out of 18 (72%) of length 11
c [cce-6-1] eliminated 13 clauses out of 18 (72%) of length 10
c [cce-6-1] eliminated 15 clauses out of 20 (75%) of length 9
c [cce-6-1] eliminated 16 clauses out of 26 (62%) of length 8
c [cce-6-1] eliminated 16 clauses out of 29 (55%) of length 7
c [cce-6-1] eliminated 26 clauses out of 1156 (2%) of length 6
c [cce-6-1] eliminated 28 clauses out of 6942 (0%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 317 large clauses in 20690032 steps
c [cce-6-1] allowing another 10345016 steps for small clauses
c [cce-6-1] scheduling 155511 clauses = 102659 binary + 52852 ternary
c [cce-6-1] tried to eliminate 1135 small clauses 1%
c [cce-6-1] eliminated 155 binary clauses 0%
c [cce-6-1] eliminated 52 ternary clauses 0%
c [cce-6-1] eliminated 207 small clauses 0%
c [cce-6-1] eliminated 227 small clauses in 20690037 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 544 covered clauses in round 1
c [cce-6] eliminated 544 covered clauses in TOTAL during 1 rounds
c [cce-6] 544 < 1/100 * 193992 = 1939 considered unsuccessful
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 30341 variables 100%
c [elim-17] limit of 662080875 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 216 variables 1% in round 1 in 16907469 steps
c [elim-17-1] backward subsumption/strengthening limit 16907400
c [elim-17-1-1] backward checking 1436 touched variables 5%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 12 and strengthened 26 clauses in 388476 steps
c [elim-17-1] rescheduled 103 variables 0% by backward subsumption
c [elim-17-2] eliminated 1 variables 0% in round 2 in 150867 steps
c [elim-17-2] backward subsumption/strengthening limit 150800
c [elim-17-2-1] backward checking 33 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 4 and strengthened 0 clauses in 39707 steps
c [elim-17-2] rescheduled 6 variables 0% by backward subsumption
c [elim-17-3] no variable eliminated in round 3 in 5449 steps
c [elim-17] fully completed in 3 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 217 = 1% variables out of 30341 scheduled
c [elim-17] 217 < 1/100 * 30341 = 303 considered unsuccessful
c [bca-15] limit of 10000000 steps and 387367 added (scaled 2)
c [bca-15] 48413 out of 60250 literals actually usable 80%
c [bca-15] added 18 blocked clauses in 123074 steps
c [sweep-15] limit 9931213 penalty 0 = 0 + 0
c [sweep-15-1] 307 pos 11.1% + 2455 neg 88.9% = 2762 sched 9.2% ret 27362
c [sweep-15-1] 9932297 steps 737 queries 53.45 avg class size
c [sweep-15-1] 4254 decisions 652 SAT calls 51.60 avg env size
c [sweep-15-1] 1487 variables remain 5% (28629 retained 95%)
c [decomp-49] removed 159 variables
c [sweep-15-1] removed 159 vars (0 failed, 86 eqs, 157 impls)
c [sweep-15] removed 159 vars in TOTAL (1 rounds, 736 queries)
c [phase-count-19] 191816 negative 99.5% of 192708 except 892 0.5%
c [phase-count-19] 134850 positive 70.0% of 192708 except 57858 30.0%
c [phase-count-19] skipping relative phase luck test
c [phase-19] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-19] sorted 4358 enqueued variables after 120868 conflicts
c [score-dist-19] active 25607 (85%), one 0 (0%), zero 4358 (15%)
c [score-dist-19] max exp 518, different 18 (3%)
c [score-dist-19] median active exp 508, avg 508.6
c [simplification-19] removed 451 variables 1.5% (29965 remain 14%)
c [simplification-19] removed 3846 irredundant clauses 2.0% (192708 remain 16%)
c [simplification-19] maximum reduction of 2% = max (1%, 2%)
c [simplification-19] geometric conflict interval increment 10369 = 31109 / 3
c [simplification-19] new conflict interval 41478
c [simplification-19] penalized conflict interval 41478 = 1 * 41478
c [simplification-19] hard conflict limit 183085 (soft 162346 + delta 20739)
c [simplification-19] new conflict limit 162346 (hard 183085)
c 
c [simplification-20] limit 162346 conflicts (hard 183085) hit after 162350 conflicts
c [quatres-15] found 18548 quaternary clauses 65% in total
c [quatres-15-1] removed 1 duplicate quaternary clauses
c [quatres-15-2] added 4 quaternary resolvents
c [ternres-16] limit 40760732 with penalty 0 = 0 + 0
c [ternres-16] all 29965 free variables schedulable
c [ternres-16] 129 ternary resolvents (1 bin, 128 trn)
c [ternres-16] fully completed ternary resolution
c [basicprobe-7] limit 203803664 penalty 0 = 0 + 0
c [basicprobe-7-0] 9364 sched 32%, 340 failed, 9 lifted, 46334 hbrs
c [decomp-51] removed 698 variables
c [basicprobe-7-1] 1449 probes remain 5% after last round
c [basicprobe-7-1] 569 units = 553 failed (97%) + 16 lifted (3%)
c [basicprobe-7-1] removed 1095 variables, found 67948 hbrs
c [bate-5] eliminated 175 asymmetric tautologies during probing
c [unhide-20] limit 8152146 with penalty 0 = 0 + 0
c [unhide-20-46] 0 units, 16 failed, 59243 tauts, 0 hbrs, 348634 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 392 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 28856 variables 100%
c [block-6] limit of 25475458 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 129 blocked clauses
c [block-6] 129 < 1/100 * 179384 = 1793 considered unsuccessful
c [bca-16] limit of 10000000 steps and 359948 added (scaled 2)
c [bca-16] 45116 out of 57676 literals actually usable 78%
c [bca-16] added 19 blocked clauses in 121070 steps
c [sweep-16] limit 12228219 penalty 0 = 0 + 0
c [sweep-16-1] 200 pos 15.0% + 1129 neg 85.0% = 1329 sched 4.6% ret 27508
c [sweep-16-1] 10488044 steps 973 queries 20.62 avg class size
c [sweep-16-1] 5219 decisions 841 SAT calls 44.49 avg env size
c [sweep-16-1] fully completed sweeping round
c [decomp-52] removed 193 variables
c [sweep-16-1] removed 193 vars (0 failed, 131 eqs, 205 impls)
c [sweep-16-2] 2909 pos 10.2% + 25735 neg 89.8% = 28644 sched 100.0% ret 0
c [sweep-16-2] 1891158 steps 54 queries 2771.24 avg class size
c [sweep-16-2] 1262 decisions 51 SAT calls 125.63 avg env size
c [sweep-16-2] 27722 variables remain 97% (916 retained 3%)
c [decomp-53] removed 9 variables
c [sweep-16-2] removed 9 vars (0 failed, 3 eqs, 4 impls)
c [sweep-16] removed 202 vars in TOTAL (2 rounds, 1025 queries)
c [phase-count-20] 178032 negative 99.5% of 178909 except 877 0.5%
c [phase-count-20] 124130 positive 69.4% of 178909 except 54779 30.6%
c [phase-count-20] skipping relative phase luck test
c [phase-20] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-20] sorted 3563 enqueued variables after 162350 conflicts
c [score-dist-20] active 25072 (88%), one 0 (0%), zero 3563 (12%)
c [score-dist-20] max exp 519, different 19 (4%)
c [score-dist-20] median active exp 509, avg 509.1
c [simplification-20] removed 1330 variables 4.4% (28635 remain 13%)
c [simplification-20] removed 13799 irredundant clauses 7.2% (178909 remain 15%)
c [simplification-20] maximum reduction of 7% = max (4%, 7%)
c [simplification-20] large reduction 7% >= 5% limit
c [simplification-20] next conflict interval 2000 = 2000/1
c [simplification-20] penalized conflict interval 2000 = 1 * 2000
c [simplification-20] hard conflict limit 174350 (soft 164350 + delta 10000)
c [simplification-20] new conflict limit 164350 (hard 174350)
c 
c [simplification-21] limit 164350 conflicts (hard 174350) hit after 164350 conflicts
c [quatres-16] found 17282 quaternary clauses 64% in total
c [quatres-16-1] removed 1 duplicate quaternary clauses
c [quatres-16-2] added 3 single-self-subsuming ternary resolvents
c [ternres-17] limit 41113381 with penalty 0 = 0 + 0
c [ternres-17] all 28635 free variables schedulable
c [ternres-17] 287 ternary resolvents (3 bin, 284 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 1284793 penalty 4 = 4 + 0
c [card-6] found 1766 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 1284793 for elimination
c [card-6] 1766 out of 1766 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-54] removed 1 variables
c [simpleprobe-8] all 28634 free variables schedulable
c [simpleprobe-8] limit 164453525 penalty 0 = 0 + 0
c [decomp-55] removed 28 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 28 variables, found 55223 hbrs, 10 units
c [unhide-21] limit 8222676 with penalty 0 = 0 + 0
c [unhide-21-52] 0 units, 4 failed, 72787 tauts, 0 hbrs, 170060 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 427 transitive binary clauses
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 28590 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 8000000000 steps penalty 1 = 1 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 680 variables 2% in round 1 in 16169888 steps
c [elim-18-1] backward subsumption/strengthening limit 16169800
c [elim-18-1-1] backward checking 3667 touched variables 13%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 7 and strengthened 36 clauses in 804608 steps
c [elim-18-1] rescheduled 128 variables 0% by backward subsumption
c [elim-18-2] eliminated 8 variables 0% in round 2 in 89377 steps
c [elim-18-2] backward subsumption/strengthening limit 89300
c [elim-18-2-1] backward checking 90 touched variables 0%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 2 and strengthened 0 clauses in 59534 steps
c [elim-18-2] rescheduled 4 variables 0% by backward subsumption
c [elim-18-3] no variable eliminated in round 3 in 4264 steps
c [elim-18] fully completed in 3 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 688 = 2% variables out of 28590 scheduled
c [bca-17] limit of 10000000 steps and 354170 added (scaled 2)
c [bca-17] 43384 out of 55806 literals actually usable 78%
c [bca-17] added 26 blocked clauses in 116073 steps
c [sweep-17] limit 12334014 penalty 0 = 0 + 0
c [sweep-17-1] 2887 pos 10.7% + 24136 neg 89.3% = 27023 sched 96.8% ret 879
c [sweep-17-1] 12348172 steps 444 queries 605.01 avg class size
c [sweep-17-1] 6994 decisions 428 SAT calls 102.60 avg env size
c [sweep-17-1] 19815 variables remain 71% (8057 retained 29%)
c [decomp-56] removed 48 variables
c [sweep-17-1] removed 48 vars (0 failed, 20 eqs, 49 impls)
c [sweep-17] removed 48 vars in TOTAL (1 rounds, 443 queries)
c [phase-count-21] 175103 negative 99.5% of 175966 except 863 0.5%
c [phase-count-21] 122041 positive 69.4% of 175966 except 53925 30.6%
c [phase-count-21] skipping relative phase luck test
c [phase-21] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-21] sorted 3267 enqueued variables after 164350 conflicts
c [score-dist-21] active 24587 (88%), one 0 (0%), zero 3267 (12%)
c [score-dist-21] max exp 519, different 19 (4%)
c [score-dist-21] median active exp 509, avg 509.2
c [simplification-21] removed 781 variables 2.7% (27854 remain 13%)
c [simplification-21] removed 2943 irredundant clauses 1.6% (175966 remain 15%)
c [simplification-21] maximum reduction of 3% = max (3%, 2%)
c [simplification-21] geometric conflict interval increment 10369 = 41478 / 4
c [simplification-21] new conflict interval 51847
c [simplification-21] penalized conflict interval 51847 = 1 * 51847
c [simplification-21] hard conflict limit 242120 (soft 216197 + delta 25923)
c [simplification-21] new conflict limit 216197 (hard 242120)
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  287.1   27853   175966    165026   21092   2966 261275  323   352   59  92%    635   22  271  282   96%
c i  287.1   27852   175966    165032   21097   2966 261275  323   352   59  92%    629   22  268  282   95%
c i  287.7   27850   175966    165709   21272   2966 261276  316   347   59  91%    135   17  282  282  100%
c 
c [simplification-22] limit 216198 conflicts (hard 242120) hit after 216200 conflicts
c [quatres-17] found 17424 quaternary clauses 63% in total
c [quatres-17-2] added 2 single-self-subsuming ternary resolvents
c [quatres-17-2] added 7 quaternary resolvents
c [ternres-18] limit 50616471 with penalty 0 = 0 + 0
c [ternres-18] all 27845 free variables schedulable
c [ternres-18] 301 ternary resolvents (4 bin, 297 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-57] removed 11 variables
c [treelook-8] limit 5061647 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 45525 literals 82%
c [treelook-8] scheduling used 952364 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 5061647 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 5065685 steps
c [treelook-8] 45269 literals remain 81%
c [treelook-8] 9676 variables remain to probed next time 35%
c [treelook-8] removed 20 variables, found 33102 hbrs
c [unhide-22] limit 5061647 with penalty 1 = 0 + 1
c [unhide-22-55] 0 units, 12 failed, 32240 tauts, 0 hbrs, 227835 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 317 transitive binary clauses
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 27810 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 59 variables 0% in round 1 in 16050169 steps
c [elim-19-1] backward subsumption/strengthening limit 16050100
c [elim-19-1-1] backward checking 470 touched variables 2%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 7 and strengthened 11 clauses in 158143 steps
c [elim-19-1] rescheduled 50 variables 0% by backward subsumption
c [elim-19-2] eliminated 2 variables 0% in round 2 in 32042 steps
c [elim-19-2] backward subsumption/strengthening limit 32000
c [elim-19-2-1] backward checking 26 touched variables 0%
c [elim-19-2-1] incomplete backward checking 0 remain 0%
c [elim-19-2] subsumed 2 and strengthened 0 clauses in 32001 steps
c [elim-19-2] rescheduled 4 variables 0% by backward subsumption
c [elim-19-3] no variable eliminated in round 3 in 8719 steps
c [elim-19] fully completed in 3 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 61 = 0% variables out of 27810 scheduled
c [elim-19] 61 < 1/100 * 27810 = 278 considered unsuccessful
c [bca-18] limit of 10000000 steps and 351127 added (scaled 2)
c [bca-18] 42251 out of 55500 literals actually usable 76%
c [bca-18] added 15 blocked clauses in 125683 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 2285 pos 11.6% + 17475 neg 88.4% = 19760 sched 71.2% ret 7989
c [sweep-18-1] 88538735 steps 4358 queries 43.38 avg class size
c [sweep-18-1] 36258 decisions 4157 SAT calls 69.40 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-59] removed 252 variables
c [sweep-18-1] removed 252 vars (0 failed, 213 eqs, 668 impls)
c [sweep-18-2] 2834 pos 10.3% + 24663 neg 89.7% = 27497 sched 100.0% ret 0
c [sweep-18-2] 97077732 steps 4471 queries 46.14 avg class size
c [sweep-18-2] 40722 decisions 4399 SAT calls 73.35 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-60] removed 138 variables
c [sweep-18-2] removed 138 vars (0 failed, 85 eqs, 473 impls)
c [sweep-18-3] 2833 pos 10.4% + 24526 neg 89.6% = 27359 sched 100.0% ret 0
c [sweep-18-3] 98929122 steps 4422 queries 63.69 avg class size
c [sweep-18-3] 39404 decisions 4381 SAT calls 70.18 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-61] removed 71 variables
c [sweep-18-3] removed 71 vars (0 failed, 52 eqs, 363 impls)
c [sweep-18] removed 461 vars in TOTAL (3 rounds, 13248 queries)
c [sort-queue-22] sorted 2714 enqueued variables after 216200 conflicts
c [score-dist-22] active 24574 (90%), one 0 (0%), zero 2714 (10%)
c [score-dist-22] max exp 519, different 19 (4%)
c [score-dist-22] median active exp 509, avg 509.6
c [simplification-22] removed 557 variables 2.0% (27288 remain 13%)
c [simplification-22] removed 3138 irredundant clauses 1.8% (172828 remain 14%)
c [simplification-22] maximum reduction of 2% = max (2%, 2%)
c [simplification-22] geometric conflict interval increment 17282 = 51847 / 3
c [simplification-22] new conflict interval 69129
c [simplification-22] penalized conflict interval 69129 = 1 * 69129
c [simplification-22] hard conflict limit 319893 (soft 285329 + delta 34564)
c [simplification-22] new conflict limit 285329 (hard 319893)
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  385.3   27287   172828    265035   44587   3380 284205  238   286  139  83%    707  -37  219  281   78%
c -  413.5   27287   172828    300267   24207   3405 284217  205   242   43  85%    -82  -61  136  260   52%
c i  415.9   27286   172828    303707   26028   3411 284220  165   224   56  74%    -25  -75  147  253   58%
c 
c [simplification-23] limit 285329 conflicts (hard 319893) hit after 319893 conflicts
c [quatres-18] found 17619 quaternary clauses 61% in total
c [quatres-18-1] removed 1 duplicate quaternary clauses
c [quatres-18-2] added 7 single-self-subsuming ternary resolvents
c [quatres-18-2] added 2 quaternary resolvents
c [ternres-19] limit 69471393 with penalty 0 = 0 + 0
c [ternres-19] all 27286 free variables schedulable
c [ternres-19] 195 ternary resolvents (3 bin, 192 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-62] removed 2 variables
c [basicprobe-8] limit 347356965 penalty 0 = 0 + 0
c [basicprobe-8-0] 1716 sched 6%, 141 failed, 4 lifted, 3317 hbrs
c [decomp-63] removed 188 variables
c [basicprobe-8-1] 8885 sched 33%, 133 failed, 4 lifted, 13422 hbrs
c [decomp-64] removed 370 variables
c [basicprobe-8-2] 8796 sched 33%, 95 failed, 8 lifted, 5593 hbrs
c [decomp-65] removed 120 variables
c [basicprobe-8-3] 8755 sched 33%, 65 failed, 1 lifted, 8040 hbrs
c [decomp-66] removed 78 variables
c [basicprobe-8-4] 6348 probes remain 24% after last round
c [basicprobe-8-4] 464 units = 447 failed (96%) + 17 lifted (4%)
c [basicprobe-8-4] removed 772 variables, found 34166 hbrs
c [bate-6] eliminated 150 asymmetric tautologies during probing
c [unhide-23] limit 13894278 with penalty 0 = 0 + 0
c [unhide-23-64] 0 units, 0 failed, 85552 tauts, 0 hbrs, 390793 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 473 transitive binary clauses
c [cce-7] limit of 21709810 steps penalty 4 = 4 + 0
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 40
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 39
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 38
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 37
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 36
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 35
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 34
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 33
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 32
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 31
c [cce-7-1] eliminated 3 clauses out of 3 (100%) of length 30
c [cce-7-1] eliminated 1 clauses out of 5 (20%) of length 29
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 28
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 27
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 26
c [cce-7-1] eliminated 5 clauses out of 9 (56%) of length 25
c [cce-7-1] eliminated 7 clauses out of 8 (88%) of length 24
c [cce-7-1] eliminated 5 clauses out of 9 (56%) of length 23
c [cce-7-1] eliminated 7 clauses out of 10 (70%) of length 22
c [cce-7-1] eliminated 6 clauses out of 9 (67%) of length 21
c [cce-7-1] eliminated 6 clauses out of 10 (60%) of length 20
c [cce-7-1] eliminated 11 clauses out of 14 (79%) of length 19
c [cce-7-1] eliminated 7 clauses out of 14 (50%) of length 18
c [cce-7-1] eliminated 12 clauses out of 17 (71%) of length 17
c [cce-7-1] eliminated 12 clauses out of 20 (60%) of length 16
c [cce-7-1] eliminated 11 clauses out of 18 (61%) of length 15
c [cce-7-1] eliminated 14 clauses out of 22 (64%) of length 14
c [cce-7-1] eliminated 13 clauses out of 18 (72%) of length 13
c [cce-7-1] eliminated 17 clauses out of 23 (74%) of length 12
c [cce-7-1] eliminated 19 clauses out of 25 (76%) of length 11
c [cce-7-1] eliminated 15 clauses out of 27 (56%) of length 10
c [cce-7-1] eliminated 20 clauses out of 32 (62%) of length 9
c [cce-7-1] eliminated 17 clauses out of 38 (45%) of length 8
c [cce-7-1] eliminated 27 clauses out of 55 (49%) of length 7
c [cce-7-1] eliminated 40 clauses out of 1032 (4%) of length 6
c [cce-7-1] eliminated 158 clauses out of 6167 (3%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 457 large clauses in 21709814 steps
c [cce-7-1] allowing another 10854907 steps for small clauses
c [cce-7-1] scheduling 127658 clauses = 92804 binary + 34854 ternary
c [cce-7-1] tried to eliminate 1779 small clauses 1%
c [cce-7-1] eliminated 306 binary clauses 0%
c [cce-7-1] eliminated 105 ternary clauses 0%
c [cce-7-1] eliminated 411 small clauses 0%
c [cce-7-1] eliminated 411 small clauses in 21709820 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 868 covered clauses in round 1
c [cce-7] eliminated 868 covered clauses in TOTAL during 1 rounds
c [cce-7] 868 < 1/100 * 161309 = 1613 considered unsuccessful
c [bca-19] limit of 10000000 steps and 322350 added (scaled 2)
c [bca-19] 37787 out of 53030 literals actually usable 71%
c [bca-19] added 5 blocked clauses in 112701 steps
c [sweep-19] limit 20841417 penalty 0 = 0 + 0
c [sweep-19-1] 2986 pos 11.3% + 23528 neg 88.7% = 26514 sched 100.0% ret 0
c [sweep-19-1] 20854146 steps 777 queries 301.84 avg class size
c [sweep-19-1] 14622 decisions 770 SAT calls 106.75 avg env size
c [sweep-19-1] 14717 variables remain 56% (11787 retained 44%)
c [decomp-67] removed 18 variables
c [sweep-19-1] removed 18 vars (0 failed, 8 eqs, 45 impls)
c [sweep-19] 18 < 1/1000 * 26514 = 26 considered unsuccessful
c [sweep-19] removed 18 vars in TOTAL (1 rounds, 776 queries)
c [sort-queue-23] sorted 2228 enqueued variables after 319893 conflicts
c [score-dist-23] active 24268 (92%), one 0 (0%), zero 2228 (8%)
c [score-dist-23] max exp 519, different 19 (4%)
c [score-dist-23] median active exp 510, avg 510.0
c [simplification-23] removed 790 variables 2.9% (26496 remain 12%)
c [simplification-23] removed 12473 irredundant clauses 7.2% (160355 remain 13%)
c [simplification-23] maximum reduction of 7% = max (3%, 7%)
c [simplification-23] large reduction 7% >= 5% limit
c [simplification-23] next conflict interval 3198 = min (319893/100, 69129)
c [simplification-23] penalized conflict interval 3198 = 1 * 3198
c [simplification-23] hard conflict limit 333091 (soft 323091 + delta 10000)
c [simplification-23] new conflict limit 323091 (hard 333091)
c 
c [simplification-24] limit 323091 conflicts (hard 333091) hit after 333092 conflicts
c [quatres-19] found 16726 quaternary clauses 62% in total
c [quatres-19-1] removed 5 duplicate quaternary clauses
c [quatres-19-2] added 2 single-self-subsuming ternary resolvents
c [ternres-20] limit 72240157 with penalty 0 = 0 + 0
c [ternres-20] all 26496 free variables schedulable
c [ternres-20] 105 ternary resolvents (1 bin, 104 trn)
c [ternres-20] fully completed ternary resolution
c [simpleprobe-9] all 26496 free variables schedulable
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-69] removed 15 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 15 variables, found 39001 hbrs, 0 units
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 810 transitive binary clauses
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 26481 variables 100%
c [elim-20] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 428 variables 2% in round 1 in 13853290 steps
c [elim-20-1] backward subsumption/strengthening limit 13853200
c [elim-20-1-1] backward checking 2379 touched variables 9%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 3 and strengthened 19 clauses in 429107 steps
c [elim-20-1] rescheduled 75 variables 0% by backward subsumption
c [elim-20-2] eliminated 4 variables 0% in round 2 in 45454 steps
c [elim-20-2] backward subsumption/strengthening limit 45400
c [elim-20-2-1] backward checking 68 touched variables 0%
c [elim-20-2-1] incomplete backward checking 0 remain 0%
c [elim-20-2] subsumed 5 and strengthened 1 clauses in 45401 steps
c [elim-20-2] rescheduled 12 variables 0% by backward subsumption
c [elim-20-3] no variable eliminated in round 3 in 8885 steps
c [elim-20] fully completed in 3 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 432 = 2% variables out of 26481 scheduled
c [bca-20] limit of 10000000 steps and 321183 added (scaled 2)
c [bca-20] 36975 out of 52100 literals actually usable 71%
c [bca-20] added 8 blocked clauses in 110705 steps
c [sort-queue-24] sorted 2164 enqueued variables after 333092 conflicts
c [score-dist-24] active 23885 (92%), one 0 (0%), zero 2164 (8%)
c [score-dist-24] max exp 520, different 20 (4%)
c [score-dist-24] median active exp 510, avg 510.0
c [simplification-24] removed 447 variables 1.7% (26049 remain 12%)
c [simplification-24] removed 499 irredundant clauses 0.3% (159856 remain 13%)
c [simplification-24] maximum reduction of 2% = max (2%, 0%)
c [simplification-24] geometric conflict interval increment 23043 = 69129 / 3
c [simplification-24] new conflict interval 92172
c [simplification-24] penalized conflict interval 92172 = 1 * 92172
c [simplification-24] hard conflict limit 471350 (soft 425264 + delta 46086)
c [simplification-24] new conflict limit 425264 (hard 471350)
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  476.3   26048   159856    349372   39251   3360 228708  110   145   60  76%    195  -96  126  195   64%
c -  494.3   26048   159856    373402   27647   3388 228725   64   106   40  61%    -53  -94   83  155   54%
c -  548.2   26048   159856    445265   28724   3423 228769   61    75   55  80%    664  -92   54  135   40%
c 
c [simplification-25] limit 425264 conflicts (hard 471350) hit after 463475 conflicts
c [quatres-20] found 16886 quaternary clauses 60% in total
c [quatres-20-2] added 1 single-self-subsuming ternary resolvents
c [quatres-20-2] added 1 quaternary resolvents
c [ternres-21] limit 95718946 with penalty 0 = 0 + 0
c [ternres-21] all 26048 free variables schedulable
c [ternres-21] 89 ternary resolvents (1 bin, 88 trn)
c [ternres-21] fully completed ternary resolution
c [gauss-6] limit 1196486 penalty 4 = 4 + 0
c [gauss-6] extracted 59 xors of average arity 3.0
c [gauss-6] connected 177 occurrences of 137 variables (average 1.3)
c [gauss-6] limit 1196486 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-70] removed 1 variables
c [treelook-9] limit 9571894 penalty 0 = 0 + 0 boost 1
c [treelook-9] scheduled 42647 literals 82%
c [treelook-9] scheduling used 875709 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 9571894 penalty 0 = 0 + 0 boost 1
c [treelook-9] used 9661783 steps
c [treelook-9] 41918 literals remain 80%
c [treelook-9] 8677 variables remain to probed next time 33%
c [decomp-71] removed 3 variables
c [treelook-9] removed 13 variables, found 45574 hbrs
c [unhide-24] limit 4785947 with penalty 2 = 1 + 1
c [unhide-24-67] 0 units, 2 failed, 60584 tauts, 0 hbrs, 452899 literals
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 553 transitive binary clauses
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 26030 variables 100%
c [elim-21] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-21] rescheduling of touched variables disabled
c [elim-21-1] eliminated 16 variables 0% in round 1 in 14276554 steps
c [elim-21-1] backward subsumption/strengthening limit 14276500
c [elim-21-1-1] backward checking 134 touched variables 1%
c [elim-21-1-1] fully completed backward checking in 1 rounds
c [elim-21-1] subsumed 0 and strengthened 1 clauses in 48721 steps
c [elim-21-1] rescheduled 4 variables 0% by backward subsumption
c [elim-21-2] no variable eliminated in round 2 in 1369 steps
c [elim-21] fully completed in 2 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 16 = 0% variables out of 26030 scheduled
c [elim-21] 16 < 1/100 * 26030 = 260 considered unsuccessful
c [bca-21] limit of 10000000 steps and 320085 added (scaled 2)
c [bca-21] 36504 out of 52030 literals actually usable 70%
c [bca-21] added 8 blocked clauses in 118020 steps
c [sweep-20] limit 14357842 penalty 1 = 1 + 0
c [sweep-20-1] 1864 pos 12.9% + 12589 neg 87.1% = 14453 sched 55.6% ret 11561
c [sweep-20-1] 14372031 steps 577 queries 197.49 avg class size
c [sweep-20-1] 8517 decisions 571 SAT calls 85.87 avg env size
c [sweep-20-1] 10670 variables remain 41% (15344 retained 59%)
c [decomp-72] removed 6 variables
c [sweep-20-1] removed 6 vars (0 failed, 7 eqs, 28 impls)
c [sweep-20] 6 < 1/1000 * 26014 = 26 considered unsuccessful
c [sweep-20] removed 6 vars in TOTAL (1 rounds, 576 queries)
c [sort-queue-25] sorted 2080 enqueued variables after 463475 conflicts
c [score-dist-25] active 23928 (92%), one 0 (0%), zero 2080 (8%)
c [score-dist-25] max exp 520, different 20 (4%)
c [score-dist-25] median active exp 510, avg 510.5
c [simplification-25] removed 40 variables 0.2% (26008 remain 12%)
c [simplification-25] removed 559 irredundant clauses 0.3% (159297 remain 13%)
c [simplification-25] maximum reduction of 0% = max (0%, 0%)
c [simplification-25] full geometric conflict interval increment 92172
c [simplification-25] new conflict interval 184344
c [simplification-25] penalized conflict interval 184344 = 1 * 184344
c [simplification-25] hard conflict limit 739991 (soft 647819 + delta 92172)
c [simplification-25] new conflict limit 647819 (hard 739991)
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 -  637.1   26008   159297    571446   25543   3518 213322  151   173   37  88%    972  -20  144  181   79%
c 
c [simplification-26] limit 647819 conflicts (hard 739991) hit after 647819 conflicts
c [quatres-21] found 16863 quaternary clauses 60% in total
c [quatres-21-2] added 1 single-self-subsuming ternary resolvents
c [ternres-22] limit 121241142 with penalty 0 = 0 + 0
c [ternres-22] all 26008 free variables schedulable
c [ternres-22] 31 ternary resolvents (1 bin, 30 trn)
c [ternres-22] fully completed ternary resolution
c [basicprobe-9] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-9-0] 6340 sched 24%, 74 failed, 5 lifted, 6112 hbrs
c [decomp-74] removed 93 variables
c [basicprobe-9-1] 8624 sched 33%, 50 failed, 4 lifted, 3154 hbrs
c [decomp-75] removed 57 variables
c [basicprobe-9-2] 8621 sched 33%, 32 failed, 3 lifted, 975 hbrs
c [decomp-76] removed 38 variables
c [basicprobe-9-3] 8616 sched 33%, 18 failed, 0 lifted, 874 hbrs
c [decomp-77] removed 21 variables
c [basicprobe-9-4] 279 probes remain 1% after last round
c [basicprobe-9-4] 195 units = 183 failed (94%) + 12 lifted (6%)
c [basicprobe-9-4] removed 220 variables, found 11508 hbrs
c [bate-7] eliminated 55 asymmetric tautologies during probing
c [unhide-25] limit 20000000 with penalty 0 = 0 + 0
c [unhide-25-80] 0 units, 0 failed, 42452 tauts, 0 hbrs, 278899 literals
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 318 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 25788 variables 100%
c [block-7] limit of 50000000 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 8 blocked clauses
c [block-7] 8 < 1/100 * 155172 = 1551 considered unsuccessful
c [bca-22] limit of 10000000 steps and 311807 added (scaled 2)
c [bca-22] 36158 out of 51578 literals actually usable 70%
c [bca-22] added 9 blocked clauses in 110152 steps
c [sort-queue-26] sorted 1907 enqueued variables after 647819 conflicts
c [score-dist-26] active 23881 (93%), one 0 (0%), zero 1907 (7%)
c [score-dist-26] max exp 521, different 21 (4%)
c [score-dist-26] median active exp 511, avg 510.7
c [simplification-26] removed 220 variables 0.8% (25788 remain 12%)
c [simplification-26] removed 4133 irredundant clauses 2.6% (155164 remain 13%)
c [simplification-26] maximum reduction of 3% = max (1%, 3%)
c [simplification-26] geometric conflict interval increment 46086 = 184344 / 4
c [simplification-26] new conflict interval 230430
c [simplification-26] penalized conflict interval 230430 = 1 * 230430
c [simplification-26] hard conflict limit 993464 (soft 878249 + delta 115215)
c [simplification-26] new conflict limit 878249 (hard 993464)
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 -  864.6   25788   155164    833571   26293   3448 178640  214   237   39  91%   1023  -43  257  264   98%
c 
c [simplification-27] limit 878249 conflicts (hard 993464) hit after 913452 conflicts
c [quatres-22] found 16712 quaternary clauses 60% in total
c [quatres-22-1] removed 1 duplicate quaternary clauses
c [ternres-23] limit 171501717 with penalty 0 = 0 + 0
c [ternres-23] all 25788 free variables schedulable
c [ternres-23] 70 ternary resolvents (0 bin, 70 trn)
c [ternres-23] fully completed ternary resolution
c [decomp-78] removed 2 variables
c [simpleprobe-10] all 25786 free variables schedulable
c [simpleprobe-10] limit 200000000 penalty 0 = 0 + 0
c [decomp-79] removed 5 variables
c [simpleprobe-10] fully completed simple probing
c [simpleprobe-10] removed 5 variables, found 25442 hbrs, 4 units
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 647 transitive binary clauses
c [elim-22] scheduling all variables this time
c [elim-22] scheduled 25781 variables 100%
c [elim-22] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-22] rescheduling of touched variables disabled
c [elim-22-1] eliminated 89 variables 0% in round 1 in 13622702 steps
c [elim-22-1] backward subsumption/strengthening limit 13622700
c [elim-22-1-1] backward checking 580 touched variables 2%
c [elim-22-1-1] fully completed backward checking in 1 rounds
c [elim-22-1] subsumed 2 and strengthened 3 clauses in 149957 steps
c [elim-22-1] rescheduled 13 variables 0% by backward subsumption
c [elim-22-2] no variable eliminated in round 2 in 3753 steps
c [elim-22] fully completed in 2 rounds
c [elim-22] transition to [ all 0 rem 0 ] state
c [elim-22] eliminated 89 = 0% variables out of 25781 scheduled
c [elim-22] 89 < 1/100 * 25781 = 257 considered unsuccessful
c [bca-23] limit of 10000000 steps and 311449 added (scaled 2)
c [bca-23] 36021 out of 51386 literals actually usable 70%
c [bca-23] added 1 blocked clauses in 117506 steps
c [sort-queue-27] sorted 1864 enqueued variables after 913452 conflicts
c [score-dist-27] active 23828 (93%), one 0 (0%), zero 1864 (7%)
c [score-dist-27] max exp 521, different 21 (4%)
c [score-dist-27] median active exp 511, avg 511.1
c [simplification-27] removed 96 variables 0.4% (25692 remain 12%)
c [simplification-27] removed 181 irredundant clauses 0.1% (154983 remain 13%)
c [simplification-27] maximum reduction of 0% = max (0%, 0%)
c [simplification-27] full geometric conflict interval increment 230430
c [simplification-27] new conflict interval 460860
c [simplification-27] penalized conflict interval 460860 = 1 * 460860
c [simplification-27] hard conflict limit 1604742 (soft 1374312 + delta 230430)
c [simplification-27] new conflict limit 1374312 (hard 1604742)
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 2255 basic ate = 2037 trn 90% + 218 lrg 10% in 7 updates
c bcas: 23 count, 1968 added (835 skipped), 4684126 steps
c bkwd: tried 476738 clauses, 952301 lits, 2.00 lits/clause
c bkwd: checked 13813733 occs, 28.98 occs/clause, 14.51 occs/lit
c bkwd: subsumed 53 binary, 444 ternary, 212 large
c bkwd: strengthened 16 binary, 0 ternary (0% self), 1442 large (0% self)
c blkd: 7 bces, 8940 removed, 7452583 resolutions, 20881183 steps
c blkd: 10431 blocking literals 2%, 31 pure
c bump: 998555 bumped seen, 1019254525 lits 1020.7 on average
c card: 6 count, 0 units, 0 am1, 116366166 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 71929 subsumed
c card: 18718 at-most-one constraints found, average size 4.75
c card: 18718 at-most-one constraints used 100%, average size 4.75
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 7 cces, 27141 eliminated, 26998 ate 99%, 143 abce 1%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 4113121 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 220 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 79 decompositions, 9623 equivalent 4%
c deco: 765762 decision-only clauses 77%, 63% reduction
c decs: 5941679 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 22 elims, 91717 eliminated 41%, 53 pure 0%
c elms: 64 rounds, 2.9 rounds/bve
c elms: 77251 small 84%, 14382 large 16%
c elms: 249540 tried small, 77253 succeeded 31%, 172287 failed 69%
c elms: 37312 subsumed, 58701 strengthened, 1157 blocked
c elms: 20752658 copies, 19945839 resolutions, 6942704 ipos
c elms: 5252760 subchks, 3131053 strchks
c gaus: 6 extractions, 405 extracted, 2.4 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 11857412 steps, 5928706 extr 50%, 13509 elim 0%
c glue: 240.3 orig avg, 240.3 real avg, 10.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1381474 = 415965 simple 30% + 907074 trn 66% + 58435 lrg 4%, 4786 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 998555 clauses, 274.2 length
c lrnd: 273795526 lits = 654397942 orig - 380602416 removed 58%
c lrnd: 396576 uips 40%, 541397 flips 54%
c mins: 193762 mins 20%, 1202 bin 0%, 3157 size 0%
c mins: 84943639 poisoned searches, 20843398 hits, 25% hit rate
c mins: 115487251 used twice searches, 11647846 hits, 10% hit rate
c move: moved 19324, 11833 bin 61%, 7491 trn 39%
c otfs: 7654 driving 61%, 4927 restarting 39%
c otfs: str 12581, 12451 red 99%, 130 irr 1%
c otfs: str 12581, 0 bin 0%, 96 trn 1%, 12485 lrg 99%
c otfs: sub 68, 68 red 100%, 0 irr 0%
c otfs: sub 68, 0 bin 0%, 0 trn 0%, 68 lrg 100%
c phas: 21 computed, 121589 set, 108 pos (0%), 121481 neg (100%)
c prbs: 9 basic, 218609 probed, 4544 failed, 139 lifted
c prbs: 10 simple, 998159 probed, 1565 failed, 931 eqs
c prbs: 9 treelook, 1219 probed, 40 failed, 0 lifted
c prom: 8479 locked 0% out of 2354246 tried
c prps: 3031577176 props, 484 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 22 count, 133 quat, 43 self1, 2 self2, 1988 dup
c queu: 27 sorted, 5941679 next (53185 steps 0.01)
c queu: 1020044692 enq (2154039305 steps 2.11), 1019254525 deq 100%
c redc: 1497 clauses 21%, 7290 tried 1%, 27 sat 0%
c redc: 3847 lits 6%, 67202 tried 0%, 27 sat 0%
c redc: 179 times jump level reduced, 42.7 levels on average
c reds: 5 count, 200072.8 conflicts per reduce
c reds: 0 memlim 0%, 5 arith 100%
c reds: 130031 collected 87%, 19705 retired 13%
c rmbd: 52269 removed, 15768 red 30%
c rsts: 7394 restarts 40%, 11059 skipped 60%
c rsts: 11059 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 27 count, 26 confs 96%, 0 vars 0%
c simp: 1 its 4%, 0 bin 0%, 0 trns 0%
c subl: 998555 count (1499414 tried 1.5), 748344 sub out of 994762 (75.2%)
c swps: 20 count, 23 rounds, 22819 queries (992.1/round)
c swps: 21423 sat calls, 197 unsat (0.3% success rate)
c swps: 194163 decisions 9.1, 5845 conflicts 0.3
c swps; 279.8 avg class size, 68.6 avg environment size
c swps: 1 failed, 3644 impls, 1538 equivs
c swp0: 7598 type 0 queries, 3632 unsat (47.8%), 7155 sat (94.2%)
c swp1: 15221 type 1 queries, 8169 unsat (53.7%), 14126 sat (92.8%)
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: 13881199 calls to obtain time
c tops: 97954 fixed 44%, 216 its, 4631.31 confs/it
c trds: 23 transitive reductions, 9668 removed, 69 failed
c trds: 55851 nodes, 173858 edges, 46011349 steps
c trim: 11521505 words, 44.0 MB
c trnr: 23 count, 23 bin, 6405 trn, 144479201 steps
c unhd: 25 count, 80 rounds, 150936589 steps
c unhd: 2931 non-trivial sccs of average size 2.3
c unhd: 207 units, 202 bin, 5 trn, 0 lrg
c unhd: 8920 failed, 8843 stamp, 0 lits, 45 bin, 17 trn, 0 lrg
c unhd: 867051 tauts, 24119 bin 3%, 11155 trn 1%, 502 lrg 0%
c unhd: 867051 tauts, 831275 stamp 96%, 785307 red 91%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 2808141 str, 202 bin 0%, 5208 trn 0%, 2802731 lrg 100%, 2788564 red 99%
c vars: 25692 remaining 11% and 199294 removed 89% out of 224986
c vars: 97954 fixed 44%, 91717 eliminated 41%, 9623 equivalent 4%
c vsts: 20272105180 visits, 93% srch, 7% simp, 0% lkhd
c vsts: 6.6 search visits per propagation, 18846.7 per conflict
c wchs: 1526348313 pushed, 65514125 enlarged, 326 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         994895        130031         19705      77584097      22744070        531728
c 
c  0 0          7391   1        47   0         0   0  30607827  39   4315421  19     44497   8     0.3
c  1 5          1274   0        39   0       193   1   3711473   5    759037   3     10252   2     0.1
c  2 6          3469   0       236   0       268   1   7404153  10   2036280   9     13377   3     0.4
c  3 9          4896   0       756   1       313   2   5864366   8<  1781870   8     30825   6     0.7
c  4 14         7953   1      2389   2       522   3   6411621   8   2421687  11     30364   6     1.6
c  5 21        12299   1      5549   4       657   3   6488830   8   2574362  11<    30832   6     3.9
c  6 30        18014   2      9697   7       868   4   3691484   5   1578165   7     38925   7     4.9
c  7 41        27021   3     16440  13      1033   5   3077374   4   1313531   6     34559   6<    7.2
c  8 54        26527   3     14863  11       908   5   1797879   2    922199   4     41065   8     5.6
c  9 69        26090   3     14516  11<      830   4   1735051   2    976854   4     32042   6     4.9
c 10 86        43197   4     21681  17      1329   7<  2221258   3   1349508   6     72193  14    10.1
c 11 126      246463  25<    21498  17      5506  28   3108128   4   1841419   8     97809  18    60.4
c 12 230      567737  57     22314  17      7278  37   1458661   2    871486   4     54814  10   180.3
c 13 534        2564   0         6   0         0   0      5992   0      2251   0       174   0     2.6
c 
c avg                 10.9           9.1           9.9           3.1           4.9           7.4
c std                  2.1           2.3           2.7           3.5           3.8           3.7
c 
c  204.843  20% bump
c   61.221   6% unhide
c   53.170   5% probe
c   28.814   3% sweep
c   19.237   2% elim
c    9.150   1% cce
c    3.545   0% decide
c 
c   11.564 < 1% rest (below)
c 
c    3.254   0% bca
c    2.467   0% transred
c    2.160   0% block
c    1.394   0% gauss
c    1.152   0% ternres
c    0.785   0% quatres
c    0.352   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    4.493   0% preprocessing     2%
c  189.120  19% inprocessing     98%
c ==================================
c  193.614  19% simplifying
c  805.744  81% search
c ==================================
c  999.362 100% all
c 
c       1000364 conflicts,        1001.0 confs/sec
c           952 ternaries,        1050.8 confs/ternary
c           924 binaries,         1082.6 confs/binary
c           216 iterations,       4631.3 confs/iteration
c 
c             5 reductions,          0.0 redus/sec, 200072.8 confs/reduction
c          7394 restarts,            7.4 rests/sec,    135.3 confs/restart
c       5941679 decisions,        5945.5 decis/sec,      5.9 decis/conflict
c    3031577176 propagations,  3033513.5 props/sec,    510.2 props/decision
c 
c 999.4 seconds, 289.1 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
