c launch: /data/cnf/sc2014/app/UTI-20-5p1.cnf.bz2
c host: atom14
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/UTI-20-5p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UTI-20-5p1.cnf.bz2
c no embedded options
c found 'p cnf 225926 1207249' header
c read 225926 variables, 1207249 clauses, 2914329 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=5
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 214523 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] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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  214523  1195096         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 6247 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] 6247 out of 6247 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 51720 variables
c [simpleprobe-1] all 174206 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 1287 variables
c [simpleprobe-1] 15114 variables remain 9% (157805 retained 91%)
c [simpleprobe-1] removed 1287 variables, found 20918 hbrs, 291 units
c [unhide-1] limit 57511 based on 920186 irredundant clauses
c [unhide-1-1] 0 units, 2275 failed, 9927 tauts, 0 hbrs, 9683 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 171886 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 47285 not tried 28% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 66343 = 39% variables out of 171886 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 762627 negative 99.2% of 768449 except 5822 0.8%
c [phase-count-1] 617596 positive 80.4% of 768449 except 150853 19.6%
c [phase-count-1] less non-negative clauses 5822 than limit 76800 (10.0%)
c [phase-count-1] non-pos/non-neg = 150853/5822 = 25.91 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 105543 negative 100%
c [sort-queue-1] sorted 105543 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 105543 (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 73539 variables 41.1% (105543 remain 49%)
c [simplification-1] removed 426647 irredundant clauses 35.7% (768449 remain 64%)
c [simplification-1] maximum reduction of 41% = max (41%, 36%)
c [simplification-1] large reduction 41% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    4.5  105542   768449         2       1      0 14308    0     0   51   0%      0    0    0    0 25500%
c i    4.6  105539   768449        12       5      2 14311    0     1   52   1%      0    1    0    0 25090%
c i    4.6  105475   768449        13       5      2 14311    0     1   52   1%      0    1    0    0 24993%
c i    4.6  105315   768449        18       8      2 14312    0     1   52   1%      0    1    0    0 24766%
c i    4.6  104993   768449        25      11      3 14314    0     1   52   2%      0    1    0    0 24553%
c i    4.6  104901   768449        32      15      5 14314    0     2   52   1%      0    2    0    0 24344%
c i    4.6  104064   768449        33      15      5 14314    0     2   52   1%      0    2    0    0 24250%
c i    4.7  103947   768449        41      20      6 14314    0     3   53   1%      0    3    0    0 23956%
c i    4.7  103133   768449        48      26      6 14314    0     4   53   1%      0    4    1    0 23903%
c i    4.8  103099   768449        74      45      9 14317    0     5   53   1%      0    5    1    0 23029%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 2601 variables
c [simpleprobe-2] 14227 schedulable variables 14%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 17029 variables remain 17% (85913 retained 83%)
c [simpleprobe-2] removed 0 variables, found 3575 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 54257 literals 26%
c [treelook-1] scheduling used 300395 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 302385 steps
c [treelook-1] 54250 literals remain 26%
c [treelook-1] 53489 variables remain to probed next time 52%
c [treelook-1] removed 2 variables, found 1733 hbrs
c [basicprobe-1] limit 6019504 based on 752438 irredundant clauses
c [basicprobe-1-0] 29737 probes remain 35% after last round
c [basicprobe-1-0] 52 units = 52 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 17621 variables, found 12436 hbrs
c [unhide-2] limit 50000 with penalty 1 = 0 + 1
c [unhide-2-2] 0 units, 4150 failed, 4924 tauts, 0 hbrs, 1063 literals
c [elim-2] 41821 variables 50% will be scheduled this time
c [elim-2] scheduled 41821 variables 50%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 12165 not tried 14% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 353 = 1% variables out of 41821 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 578266 negative 99.0% of 584090 except 5824 1.0%
c [phase-count-2] 467698 positive 80.1% of 584090 except 116392 19.9%
c [phase-count-2] less non-negative clauses 5824 than limit 58400 (10.0%)
c [phase-count-2] non-pos/non-neg = 116392/5824 = 19.98 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 8768 negative 100%
c [sort-queue-2] sorted 81605 enqueued variables after 74 conflicts
c [score-dist-2] active 1965 (2%), one 0 (0%), zero 81605 (98%)
c [score-dist-2] max exp 522, different 22 (4%)
c [score-dist-2] median active exp 515, avg 514.1
c [simplification-2] removed 19490 variables 18.9% (83570 remain 39%)
c [simplification-2] removed 184359 irredundant clauses 24.0% (584090 remain 49%)
c [simplification-2] maximum reduction of 24% = max (19%, 24%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1032 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    7.6   83569   584090       154      91     17 18058    0     6   42   2%      0    6    2    0 19389%
c i    7.6   83553   584090       206     128     22 18067    0     7   42   3%      0    7    2    0 17821%
c i    7.6   83545   584090       224     131     26 18069    0     7   42   3%      0    7    2    0 17179%
c i    7.7   83537   584090       253     143     32 18078    0     8   42   3%      0    8    2    0 16031%
c i    7.7   83456   584090       306     179     37 18088    0     9   42   3%      0    9    3    0 15207%
c i    7.7   83445   584090       342     206     41 18092    0    10   42   3%      0   10    3    0 15017%
c i    7.8   83409   584090       355     213     41 18097    0    10   42   4%      0   10    3    0 14484%
c i    7.8   83127   584090       416     250     46 18115    0    10   42   4%      0   10    3    0 12758%
c i    7.8   82878   584090       437     256     51 18122    0    10   42   4%      0   10    3    0 12105%
c i    7.8   82871   584090       496     306     55 18125    0    11   42   4%      0   11    4    0 11916%
c i    7.8   82702   584090       500     306     56 18127    0    11   42   4%      0   11    4    0 11759%
c i    7.9   82614   584090       533     330     60 18131    0    12   42   4%      0   12    4    0 11182%
c i    7.9   82560   584090       559     342     68 18135    1    12   42   4%      0   12    4    0 10784%
c i    7.9   82548   584090       560     342     68 18135    1    12   42   4%      0   12    4    0 10742%
c i    7.9   82542   584090       577     356     68 18137    1    13   42   4%      0   13    4    0 10672%
c i    7.9   82529   584090       591     362     73 18139    1    13   42   4%      0   13    4    0 10381%
c 
c [simplification-3] limit of 109 binary hit after 109 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4237 at-most-one constraints of average size 4.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4237 out of 4237 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 1740 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 52432 literals 32%
c [treelook-2] scheduling used 325217 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 338408 steps
c [treelook-2] 52423 literals remain 32%
c [treelook-2] 32603 variables remain to probed next time 40%
c [treelook-2] removed 1 variables, found 2018 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 1397 failed, 11737 tauts, 0 hbrs, 419 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 80977 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 15788 not tried 19% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 3005 = 4% variables out of 80977 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 543767 negative 99.0% of 549476 except 5709 1.0%
c [phase-count-3] 440290 positive 80.1% of 549476 except 109186 19.9%
c [phase-count-3] less non-negative clauses 5709 than limit 54900 (10.0%)
c [phase-count-3] non-pos/non-neg = 109186/5709 = 19.13 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 5449 negative 100%
c [sort-queue-3] sorted 67902 enqueued variables after 613 conflicts
c [score-dist-3] active 10070 (13%), one 0 (0%), zero 67902 (87%)
c [score-dist-3] max exp 662, different 153 (23%)
c [score-dist-3] median active exp 624, avg 605.0
c [simplification-3] removed 4497 variables 5.5% (77972 remain 36%)
c [simplification-3] removed 34614 irredundant clauses 5.9% (549476 remain 46%)
c [simplification-3] maximum reduction of 6% = max (5%, 6%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 1044 (hard 11000)
c [simplification-3] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   10.1   77971   549476       614     297     58 15147    1    14   41   4%      0   13    4    0 10093%
c i   10.2   77961   549476       716     367     69 15165    1    15   41   4%      0   15    4    0 8977%
c i   10.2   77949   549476       734     376     73 15169    1    16   41   4%      0   16    4    0 8663%
c i   10.3   77698   549476       758     387     78 15176    1    16   41   4%      0   16    4    0 8238%
c i   10.3   77600   549476       776     390     85 15182    1    16   41   4%      0   16    4    0 7853%
c i   10.3   77589   549476       844     442     91 15190    1    18   41   5%      0   18    7    0 10561%
c i   10.3   77581   549476       906     492     94 15198    1    19   41   6%      0   18    7    0 9630%
c i   10.4   77573   549476       916     495     96 15202    1    19   41   6%      0   19    7    0 9343%
c i   10.4   77562   549476       945     511    100 15210    1    19   41   5%      0   19    6    0 8643%
c i   10.4   77551   549476       956     517    103 15211    1    20   41   5%      0   19    6    0 8379%
c i   10.4   77504   549476       961     521    103 15211    1    20   41   5%      0   19    6    0 8288%
c i   10.4   76755   549476       963     522    103 15211    1    20   41   5%      0   19    6    0 8235%
c i   10.5   76743   549476      1031     565    113 15225    1    20   41   6%      0   20    6    0 7258%
c i   10.5   76734   549476      1050     578    115 15227    1    21   41   6%      0   20    5    0 6965%
c 
c [simplification-4] limit 1052 conflicts (hard 11000) hit after 1052 conflicts
c [decomp-8] removed 1259 variables
c [basicprobe-2] limit 4325856 based on 540732 irredundant clauses
c [basicprobe-2-0] 26267 probes remain 35% after last round
c [basicprobe-2-0] 49 units = 49 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 2503 variables, found 16818 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 3 units, 813 failed, 2955 tauts, 0 hbrs, 1026 literals
c [elim-4] 11868 variables 16% will be scheduled this time
c [elim-4] scheduled 11868 variables 16%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 25406254 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 11868 scheduled
c [phase-count-4] 508755 negative 98.9% of 514477 except 5722 1.1%
c [phase-count-4] 413374 positive 80.3% of 514477 except 101103 19.7%
c [phase-count-4] less non-negative clauses 5722 than limit 51400 (10.0%)
c [phase-count-4] non-pos/non-neg = 101103/5722 = 17.67 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 4795 negative 100%
c [sort-queue-4] sorted 60601 enqueued variables after 1052 conflicts
c [score-dist-4] active 12959 (18%), one 0 (0%), zero 60601 (82%)
c [score-dist-4] max exp 776, different 248 (32%)
c [score-dist-4] median active exp 700, avg 681.1
c [simplification-4] removed 3168 variables 4.1% (73560 remain 34%)
c [simplification-4] removed 34999 irredundant clauses 6.4% (514477 remain 43%)
c [simplification-4] maximum reduction of 6% = max (4%, 6%)
c [simplification-4] large reduction 6% >= 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 13052 (soft 3052 + delta 10000)
c [simplification-4] new conflict limit 3052 (hard 13052)
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.0   73559   514477      1087     582    118 25722    1    21   39   6%      0   21    5    0 6529%
c i   12.0   73511   514477      1090     583    119 25722    1    21   39   6%      0   21    5    0 6467%
c i   12.0   73492   514477      1111     591    122 25731    1    21   39   5%      0   21    5    0 6169%
c i   12.2   73443   514477      1267     687    150 25758    1    24   39   6%      0   24    7    0 6790%
c i   12.2   73346   514477      1290     702    152 25761    1    25   39   6%      0   24    7    0 6501%
c i   12.2   73345   514477      1300     711    152 25761    1    25   39   6%      0   24    7    0 6420%
c i   12.3   73337   514477      1390     772    156 25783    2    26   39   6%      0   25    6    0 5585%
c i   12.3   73222   514477      1418     788    161 25789    2    26   39   6%      0   26    6    0 5252%
c i   12.3   73215   514477      1470     829    167 25793    2    27   39   6%      0   27    6    0 5344%
c i   12.4   73202   514477      1545     888    175 25800    2    30   39   6%      0   30    6    0 5133%
c i   12.4   73180   514477      1546     888    175 25800    2    30   39   6%      0   30    6    0 5113%
c i   12.4   73173   514477      1578     913    178 25803    2    31   39   6%      0   31    6    0 4859%
c i   12.5   73166   514477      1619     943    180 25811    2    32   39   6%      0   32    6    0 4797%
c i   12.5   73075   514477      1661     969    183 25822    2    33   39   5%      0   33    6    0 4385%
c i   12.6   73027   514477      1701     993    186 25833    2    33   39   6%      0   33    6    0 4072%
c i   12.6   73022   514477      1702     993    186 25833    2    33   39   6%      0   33    6    0 4056%
c i   12.6   73017   514477      1703     993    186 25833    2    33   39   6%      0   33    5    0 4040%
c i   12.6   73009   514477      1717    1003    187 25835    2    33   39   6%      0   33    5    0 3944%
c i   12.6   73006   514477      1718    1003    187 25835    2    33   39   6%      0   33    5    0 3929%
c i   12.6   72999   514477      1727    1003    187 25843    2    33   39   6%      0   33    5    0 3812%
c i   12.6   72995   514477      1747    1020    187 25844    2    34   39   5%      0   33    5    0 3732%
c i   12.7   72683   514477      1799    1058    190 25854    2    35   39   5%      0   35    5    0 3650%
c i   12.7   72674   514477      1804    1058    190 25858    2    35   39   5%      0   35    5    0 3589%
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.7   72648   514477      1866    1093    201 25872    2    35   39   5%      0   35    5    0 3228%
c i   12.7   72621   514477      1870    1094    201 25874    2    35   39   5%      0   35    5    0 3190%
c i   12.7   72584   514477      1871    1094    201 25874    2    35   39   5%      0   35    5    0 3177%
c i   12.7   72583   514477      1887    1103    201 25880    2    35   39   5%      0   35    5    0 3092%
c i   12.7   72535   514477      1905    1112    204 25885    2    35   39   5%      0   35    4    0 3039%
c i   12.8   72534   514477      1945    1142    209 25889    2    36   40   5%      0   35    4    0 2996%
c i   12.8   72452   514477      1982    1166    215 25895    2    36   40   5%      0   35    4    0 2940%
c i   12.8   72364   514477      2044    1207    226 25902    2    37   40   5%      0   36    5    0 2929%
c i   12.9   72353   514477      2110    1258    232 25910    2    39   40   5%      0   38    5    0 3153%
c i   12.9   72310   514477      2160    1301    233 25915    2    39   40   5%      0   39    5    0 3063%
c i   13.0   72278   514477      2224    1350    242 25919    2    40   40   5%      0   39    5    0 3024%
c i   13.0   72259   514477      2248    1366    244 25923    2    40   40   5%      0   39    5    0 2931%
c i   13.1   72254   514477      2366    1443    253 25946    2    41   40   6%      0   40    5    0 2840%
c i   13.2   72244   514477      2443    1491    257 25968    2    42   40   6%      0   41    5    0 2737%
c i   13.2   72233   514477      2445    1491    257 25969    2    42   40   6%      0   41    5    0 2718%
c i   13.2   72223   514477      2446    1491    257 25969    2    42   40   6%      0   41    5    0 2707%
c i   13.2   72212   514477      2497    1527    262 25978    2    43   40   6%      0   42    6    0 3011%
c i   13.3   72201   514477      2599    1593    285 25987    2    44   40   6%      0   43    5    0 2680%
c i   13.5   72193   514477      2836    1764    308 26028    3    48   40   6%      1   47    9    0 3553%
c i   13.6   72165   514477      2870    1787    309 26035    3    49   40   6%      1   48    8    0 3362%
c i   13.6   72136   514477      2874    1790    309 26035    3    49   40   6%      1   48    8    0 3333%
c i   13.6   72124   514477      2913    1815    312 26043    3    49   40   6%      1   48    7    0 3046%
c i   13.7   72107   514477      2998    1876    320 26057    3    52   40   6%      1   51    7    0 2818%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   13.7   72098   514477      3031    1898    326 26061    3    53   40   6%      1   51    7    0 2692%
c i   13.7   72097   514477      3032    1898    326 26061    3    53   40   6%      1   51    7    0 2681%
c i   13.8   72096   514477      3042    1904    326 26063    3    53   40   6%      1   52    7    0 2640%
c i   13.8   72095   514477      3100    1948    330 26071    3    54   40   6%      1   53    7    0 2568%
c i   13.8   72092   514477      3119    1962    330 26075    3    54   40   6%      1   53    7    0 2533%
c 
c [simplification-5] limit 3139 conflicts (hard 13052) hit after 3139 conflicts
c [quatres-1] found 32480 quaternary clauses 47% in total
c [quatres-1-2] added 4 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 72072 free variables schedulable
c [ternres-1] 40 ternary resolvents (1 bin, 39 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 641 xors of average arity 2.2
c [gauss-1] connected 1431 occurrences of 883 variables (average 1.6)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 407 variables
c [gauss-1] exported 0 unary, 10 binary and 0 ternary equations
c [unhide-5] limit 165026 with penalty 0 = 0 + 0
c [unhide-5-5] 9 units, 441 failed, 11743 tauts, 0 hbrs, 1950 literals
c [transred-1] limit 825134 with penalty 0 = 0 + 0
c [transred-1] removed 144 transitive binary clauses
c [transred-1] found 2 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 71327 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 5919 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 138 (1%) of length 10
c [cce-1-1] eliminated 3 clauses out of 426 (1%) of length 9
c [cce-1-1] eliminated 18 clauses out of 488 (4%) of length 8
c [cce-1-1] eliminated 37 clauses out of 679 (5%) of length 7
c [cce-1-1] eliminated 2748 clauses out of 4070 (68%) of length 6
c [cce-1-1] eliminated 1889 clauses out of 30467 (6%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 4697 large clauses in 30000000 steps
c [cce-1-1] allowing another 15000000 steps for small clauses
c [cce-1-1] scheduling 398132 clauses = 233874 binary + 164258 ternary
c [cce-1-1] tried to eliminate 330 small clauses 0%
c [cce-1-1] eliminated 73 binary clauses 0%
c [cce-1-1] eliminated 19 ternary clauses 0%
c [cce-1-1] eliminated 92 small clauses 0%
c [cce-1-1] eliminated 92 small clauses in 30000012 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 4789 covered clauses in round 1
c [cce-1] eliminated 4789 covered clauses in TOTAL during 1 rounds
c [cce-1] 4789 < 1/100 * 484336 = 4843 considered unsuccessful
c [bca-1] limit of 10000000 steps and 959594 added (scaled 2)
c [bca-1] 131380 out of 142656 literals actually usable 92%
c [bca-1] added 182 blocked clauses in 381095 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 6637 pos 9.3% + 64690 neg 90.7% = 71327 sched 100.0% ret 0
c [sweep-1-1] 1942679 steps 21 queries 18780.14 avg class size
c [sweep-1-1] 120 decisions 18 SAT calls 40.00 avg env size
c [sweep-1-1] 71222 variables remain 100% (101 retained 0%)
c [decomp-11] removed 103 variables
c [sweep-1-1] removed 103 vars (0 failed, 2 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 103 vars in TOTAL (1 rounds, 20 queries)
c [phase-count-5] 477377 negative 99.6% of 479149 except 1772 0.4%
c [phase-count-5] 390786 positive 81.6% of 479149 except 88363 18.4%
c [phase-count-5] less non-negative clauses 1772 than limit 47900 (10.0%)
c [phase-count-5] non-pos/non-neg = 88363/1772 = 49.87 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 3256 negative 100%
c [sort-queue-5] sorted 47587 enqueued variables after 3139 conflicts
c [score-dist-5] active 23637 (33%), one 3 (0%), zero 47584 (67%)
c [score-dist-5] max exp 825, different 646 (78%)
c [score-dist-5] median active exp 709, avg 593.6
c [simplification-5] removed 848 variables 1.2% (71224 remain 33%)
c [simplification-5] removed 35328 irredundant clauses 6.9% (479149 remain 40%)
c [simplification-5] maximum reduction of 7% = max (1%, 7%)
c [simplification-5] large reduction 7% >= 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 15139 (soft 5139 + delta 10000)
c [simplification-5] new conflict limit 5139 (hard 15139)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   16.8   71223   479149      3140    1937    397 33780    3    54   38   6%      1   53    8    0 2836%
c i   16.8   71209   479149      3152    1944    398 33783    3    55   38   6%      1   53    8    0 2808%
c i   16.9   71205   479149      3275    2036    415 33795    3    55   38   6%      1   54    6    0 2324%
c i   17.0   71202   479149      3307    2051    424 33802    3    56   38   6%      1   55    6    0 2233%
c i   17.0   71194   479149      3315    2055    425 33804    3    56   38   6%      1   55    6    0 2184%
c i   17.0   71150   479149      3317    2056    425 33804    3    56   38   6%      1   55    6    0 2171%
c i   17.1   71143   479149      3403    2114    438 33815    3    58   38   6%      1   56    6    0 2133%
c i   17.2   71123   479149      3557    2235    451 33832    3    58   38   6%      1   57    6    0 1999%
c i   17.2   71115   479149      3609    2269    456 33840    3    59   38   6%      1   57    6    0 2059%
c i   17.4   71109   479149      3746    2381    462 33855    4    62   38   6%      1   60    6    0 1983%
c i   17.4   71101   479149      3807    2432    464 33861    4    62   38   6%      1   60    6    0 1830%
c i   17.6   71092   479149      4085    2652    484 33893    4    67   38   6%      1   64    7    0 1965%
c i   17.7   71089   479149      4132    2689    486 33897    4    68   38   6%      1   66    8    0 2181%
c i   17.7   71088   479149      4159    2705    491 33902    4    69   38   6%      1   67    8    0 2061%
c i   17.8   71064   479149      4288    2796    502 33927    4    69   39   6%      1   67    7    0 1891%
c i   17.8   71058   479149      4340    2831    508 33936    4    69   39   6%      1   67    7    0 1748%
c i   17.9   71054   479149      4436    2907    514 33949    4    72   39   6%      1   69    7    0 1733%
c i   17.9   71051   479149      4483    2942    517 33957    4    73   39   6%      1   70    7    0 1816%
c i   18.0   71039   479149      4505    2957    519 33960    4    73   39   6%      1   70    7    0 1747%
c i   18.1   71034   479149      4607    3031    532 33971    4    75   39   6%      1   72    6    0 1594%
c i   18.1   71033   479149      4615    3037    532 33972    4    75   39   6%      1   72    6    0 1563%
c i   18.2   71024   479149      4692    3093    539 33984    4    76   39   6%      1   73    6    0 1489%
c i   18.2   71015   479149      4722    3116    540 33988    4    77   39   6%      1   74    6    0 1477%
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   18.2   71014   479149      4754    3141    542 33992    4    76   39   6%      1   73    6    0 1437%
c i   18.2   71013   479149      4785    3165    545 33995    4    76   39   6%      1   73    6    0 1367%
c i   18.3   71012   479149      4888    3245    554 34008    4    77   39   6%      1   74    6    0 1462%
c 
c [simplification-6] limit 5146 conflicts (hard 15139) hit after 5146 conflicts
c [quatres-2] found 33662 quaternary clauses 51% in total
c [quatres-2-2] added 1 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 70941 free variables schedulable
c [ternres-2] 4 ternary resolvents (1 bin, 3 trn)
c [ternres-2] 45083 variables remain 64% (25858 retained 36%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2285 at-most-one constraints of average size 4.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2285 out of 2285 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 220 xors of average arity 2.7
c [gauss-2] connected 602 occurrences of 508 variables (average 1.2)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [decomp-12] removed 43 variables
c [gauss-2] exported 1 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 11237 schedulable variables 16%
c [simpleprobe-3] limit 2599482 penalty 1 = 1 + 0
c [decomp-14] removed 144 variables
c [simpleprobe-3] 14347 variables remain 20% (56407 retained 80%)
c [simpleprobe-3] removed 144 variables, found 5477 hbrs, 42 units
c [unhide-6] limit 259948 with penalty 0 = 0 + 0
c [unhide-6-6] 7 units, 614 failed, 2688 tauts, 0 hbrs, 2479 literals
c [transred-2] limit 1299741 with penalty 0 = 0 + 0
c [transred-2] removed 179 transitive binary clauses
c [transred-2] found 3 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 69949 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 1265 blocked clauses
c [block-2] 1265 < 1/100 * 475085 = 4750 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 69908 variables 100%
c [elim-5] limit of 12997413 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 17285 not tried 25% in round 1
c [gc-37] reconnected 36762 binary clauses (produced 0 empty 3 units)
c [gc-37] reconnected 714 ternary clauses  (produced 0 empty 1 units 0 binary)
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 3549 = 5% variables out of 69908 scheduled
c [bca-2] limit of 10000000 steps and 921401 added (scaled 2)
c [bca-2] 121927 out of 132720 literals actually usable 92%
c [bca-2] added 128 blocked clauses in 356679 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 6628 pos 10.0% + 59644 neg 90.0% = 66272 sched 99.9% ret 87
c [sweep-2-1] 1005962 steps 18 queries 14885.11 avg class size
c [sweep-2-1] 203 decisions 15 SAT calls 123.87 avg env size
c [sweep-2-1] 66203 variables remain 100% (156 retained 0%)
c [decomp-15] removed 8 variables
c [sweep-2-1] removed 8 vars (0 failed, 2 eqs, 4 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 8 vars in TOTAL (1 rounds, 17 queries)
c [phase-count-6] 459263 negative 99.8% of 460384 except 1121 0.2%
c [phase-count-6] 376170 positive 81.7% of 460384 except 84214 18.3%
c [phase-count-6] less non-negative clauses 1121 than limit 46000 (10.0%)
c [phase-count-6] non-pos/non-neg = 84214/1121 = 75.12 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 2308 negative 100%
c [sort-queue-6] sorted 44654 enqueued variables after 5146 conflicts
c [score-dist-6] active 21697 (33%), one 3117 (5%), zero 41537 (63%)
c [score-dist-6] max exp 853, different 659 (77%)
c [score-dist-6] median active exp 718, avg 647.7
c [simplification-6] removed 4590 variables 6.5% (66351 remain 31%)
c [simplification-6] removed 18765 irredundant clauses 3.9% (460384 remain 39%)
c [simplification-6] maximum reduction of 6% = max (6%, 4%)
c [simplification-6] large reduction 6% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 17146 (soft 7146 + delta 10000)
c [simplification-6] new conflict limit 7146 (hard 17146)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   22.0   66350   460384      5581    2735    542 36406    5    84   38   6%      3   80   10    1 1964%
c i   22.0   66340   460384      5616    2761    545 36410    5    84   38   6%      3   80   10    1 1870%
c i   22.1   66334   460384      5659    2790    549 36418    5    84   38   6%      3   80    9    1 1764%
c i   22.1   66322   460384      5663    2791    549 36418    5    84   38   6%      3   80   10    1 1848%
c i   22.1   66315   460384      5701    2820    550 36425    5    85   38   6%      3   81   10    1 1869%
c i   22.1   66309   460384      5751    2860    554 36427    5    86   38   6%      3   82   11    1 1965%
c i   22.1   66244   460384      5769    2873    555 36429    5    85   38   6%      3   81   11    1 1905%
c i   22.2   66242   460384      5827    2920    561 36433    5    86   38   6%      3   82   10    1 1733%
c i   22.3   66235   460384      5927    2992    571 36445    6    88   38   6%      2   84   11    1 1955%
c i   22.3   66232   460384      6040    3071    585 36461    6    89   38   7%      2   85   13    1 2127%
c i   22.4   66225   460384      6171    3176    598 36473    6    87   38   7%      2   83   10    1 1562%
c i   22.4   66219   460384      6254    3242    602 36483    6    88   38   7%      2   84    8    1 1330%
c i   22.4   66198   460384      6278    3262    602 36486    6    88   38   7%      2   84    8    1 1260%
c i   22.4   66195   460384      6332    3300    610 36491    6    88   38   7%      2   84    9    1 1408%
c i   22.4   66190   460384      6333    3300    610 36491    6    88   38   7%      2   84    9    1 1403%
c i   22.4   66189   460384      6334    3300    610 36491    6    88   38   7%      2   84    9    1 1397%
c i   22.5   66188   460384      6353    3315    611 36491    6    88   38   7%      2   83    9    1 1354%
c i   22.5   66174   460384      6422    3379    613 36492    6    88   38   7%      2   83    8    1 1275%
c i   22.6   66172   460384      6584    3510    633 36500    6    88   38   7%      2   83    7    1 1077%
c i   22.8   66162   460384      6845    3720    650 36530    6    92   38   6%      2   87    6    1  937%
c i   22.8   65882   460384      6933    3789    655 36540    6    92   38   7%      2   87    7    1 1023%
c i   22.8   65875   460384      6934    3789    655 36540    6    92   38   7%      2   87    7    1 1019%
c i   22.8   65867   460384      6935    3789    655 36540    6    92   38   7%      2   87    7    1 1015%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   22.8   65860   460384      6938    3789    656 36541    6    92   38   7%      2   87    7    1 1005%
c i   22.9   65858   460384      6945    3793    656 36543    6    92   38   7%      2   87    7    1 1000%
c i   22.9   65856   460384      6946    3793    656 36543    6    92   38   7%      2   87    7    1  996%
c 
c [simplification-7] limit 7202 conflicts (hard 17146) hit after 7202 conflicts
c [quatres-3] found 34427 quaternary clauses 51% in total
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 3 single-self-subsuming ternary resolvents
c [quatres-3-2] added 36 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 41704 schedulable variables 63%
c [ternres-3] 98 ternary resolvents (2 bin, 96 trn)
c [ternres-3] 14695 variables remain 22% (51155 retained 78%)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 74 xors of average arity 2.7
c [gauss-3] connected 203 occurrences of 176 variables (average 1.2)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [decomp-16] removed 42 variables
c [gauss-3] exported 1 unary, 0 binary and 0 ternary equations
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 45747 literals 35%
c [treelook-3] scheduling used 303118 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 334423 steps
c [treelook-3] 45736 literals remain 35%
c [treelook-3] 21290 variables remain to probed next time 32%
c [treelook-3] removed 2 variables, found 1041 hbrs
c [unhide-7] limit 343571 with penalty 0 = 0 + 0
c [unhide-7-7] 16 units, 176 failed, 8068 tauts, 0 hbrs, 4282 literals
c [transred-3] limit 1717858 with penalty 0 = 0 + 0
c [transred-3] removed 240 transitive binary clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 10 clauses out of 600 (2%) of length 7
c [cce-2-1] eliminated 8 clauses out of 1289 (1%) of length 6
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 18 large clauses in 15000007 steps
c [cce-2-1] allowing another 7500003 steps for small clauses
c [cce-2-1] scheduling 359951 clauses = 211640 binary + 148311 ternary
c [cce-2-1] tried to eliminate 238 small clauses 0%
c [cce-2-1] eliminated 56 binary clauses 0%
c [cce-2-1] eliminated 23 ternary clauses 0%
c [cce-2-1] eliminated 79 small clauses 0%
c [cce-2-1] eliminated 1377 small clauses in 15000000 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1395 covered clauses in round 1
c [cce-2] eliminated 1395 covered clauses in TOTAL during 1 rounds
c [cce-2] 1395 < 1/100 * 444847 = 4448 considered unsuccessful
c [elim-6] 16922 variables 26% will be scheduled this time
c [elim-6] scheduled 16922 variables 26%
c [elim-6] limit of 34357168 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 10 variables 0% in round 1 in 27970022 steps
c [elim-6-1] backward subsumption/strengthening limit 6387146
c [elim-6-1-1] backward checking 489 touched variables 1%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 8 and strengthened 1 clauses in 185651 steps
c [elim-6-1] rescheduled 21 variables 0% by backward subsumption
c [elim-6-2] eliminated 1 variables 0% in round 2 in 26960 steps
c [elim-6-2] backward subsumption/strengthening limit 26900
c [elim-6-2-1] backward checking 6 touched variables 0%
c [elim-6-2-1] incomplete backward checking 0 remain 0%
c [elim-6-2] subsumed 0 and strengthened 0 clauses in 26901 steps
c [elim-6-2] fully rescheduled 65657 variables 100%
c [elim-6] incomplete 30817 not tried 47% in round 3
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 349 = 2% variables out of 16922 scheduled
c [elim-6] 349 < 1/100 * 16922 = 169 considered unsuccessful
c [bca-3] limit of 10000000 steps and 884521 added (scaled 2)
c [bca-3] 112220 out of 130654 literals actually usable 86%
c [bca-3] added 56 blocked clauses in 306189 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 8052 pos 12.4% + 57126 neg 87.6% = 65178 sched 99.8% ret 148
c [sweep-3-1] 1052149 steps 11 queries 15920.91 avg class size
c [sweep-3-1] 85 decisions 7 SAT calls 47.86 avg env size
c [sweep-3-1] 65164 variables remain 100% (160 retained 0%)
c [decomp-19] removed 7 variables
c [sweep-3-1] removed 7 vars (0 failed, 3 eqs, 4 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 7 vars in TOTAL (1 rounds, 10 queries)
c [sort-queue-7] sorted 31618 enqueued variables after 7202 conflicts
c [score-dist-7] active 33701 (52%), one 3947 (6%), zero 27671 (42%)
c [score-dist-7] max exp 892, different 760 (85%)
c [score-dist-7] median active exp 740, avg 641.1
c [simplification-7] removed 531 variables 0.8% (65319 remain 30%)
c [simplification-7] removed 18482 irredundant clauses 4.0% (441902 remain 37%)
c [simplification-7] maximum reduction of 4% = max (1%, 4%)
c [simplification-7] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-7] new conflict interval 4000
c [simplification-7] penalized conflict interval 4000 = 1 * 4000
c [simplification-7] hard conflict limit 21202 (soft 11202 + delta 10000)
c [simplification-7] new conflict limit 11202 (hard 21202)
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   65318   441902      7332    4008    768 37284    6    96   37   6%      2   90    8    1 1092%
c i   26.8   65313   441902      7393    4059    771 37288    6    98   37   6%      2   92    8    1 1127%
c i   26.9   65307   441902      7478    4120    782 37299    6    98   37   6%      2   92    8    1 1043%
c i   27.0   65260   441902      7587    4186    797 37325    6   100   37   6%      2   94    7    1  887%
c i   27.0   65258   441902      7591    4188    798 37325    6   100   37   6%      2   93    7    1  877%
c i   27.0   65256   441902      7592    4188    798 37325    6   100   37   6%      2   93    7    1  873%
c i   27.0   65254   441902      7593    4188    798 37325    6   100   37   6%      2   93    7    1  870%
c i   27.0   65247   441902      7609    4199    801 37326    6   100   37   6%      2   93    7    1  866%
c i   27.1   65240   441902      7702    4260    814 37344    6   101   37   6%      2   95    7    1  906%
c i   27.1   65235   441902      7707    4263    814 37345    6   101   37   6%      2   95    7    1  897%
c i   27.2   65230   441902      7865    4385    828 37364    6   103   37   6%      2   96    6    1  823%
c i   27.4   65224   441902      8023    4516    839 37379    6   106   37   6%      1   99    7    1  920%
c i   27.4   65219   441902      8026    4517    839 37380    6   106   37   6%      1   99    7    1  912%
c i   27.4   65169   441902      8077    4553    851 37382    6   106   37   6%      1   99    7    1  871%
c i   27.5   65130   441902      8097    4568    854 37383    6   106   38   6%      1   99    7    1  877%
c i   27.5   65114   441902      8135    4594    859 37388    6   106   38   6%      1   99    7    1  859%
c i   27.6   65110   441902      8244    4674    869 37405    6   106   38   6%      1   99    7    1  891%
c i   27.6   65109   441902      8293    4709    877 37410    6   106   38   6%      1   98    7    1  816%
c i   27.7   65022   441902      8334    4739    881 37414    6   106   38   6%      1   98    6    1  779%
c i   27.8   65015   441902      8588    4921    908 37454    6   105   38   6%      1   97    6    1  707%
c i   27.9   65008   441902      8639    4958    912 37462    6   106   38   6%      1   98    8    1  953%
c i   27.9   64998   441902      8665    4972    917 37464    6   106   38   6%      1   98    9    1 1056%
c i   27.9   64992   441902      8722    5005    923 37480    6   106   38   6%      1   97    8    1  973%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   28.0   64991   441902      8810    5075    929 37486    6   105   38   6%      1   97    8    1  881%
c i   28.4   64985   441902      9154    5345    962 37522    7   111   38   6%      2  103    9    1 1001%
c i   28.4   64978   441902      9164    5352    962 37524    7   111   38   6%      2  102    9    1  983%
c i   28.4   64977   441902      9165    5352    962 37524    7   111   38   6%      2  102    9    1  980%
c i   28.6   64970   441902      9403    5535    979 37553    7   113   38   6%      2  104   13    1 1343%
c i   28.7   64965   441902      9518    5630    986 37561    7   114   38   6%      2  105   12    1 1195%
c i   28.8   64957   441902      9578    5678    991 37567    7   117   38   6%      1  107   11    1 1100%
c i   28.9   64956   441902      9665    5753    994 37574    7   118   38   6%      1  109   10    1  996%
c i   28.9   64943   441902      9670    5756    995 37574    7   118   38   6%      1  109   10    1 1020%
c i   29.0   64939   441902      9703    5773    998 37584    7   118   38   6%      1  108    9    1  945%
c i   29.1   64934   441902      9875    5902   1014 37604    7   117   38   6%      1  107    8    1  768%
c i   29.2   64932   441902      9935    5954   1015 37609    7   117   38   6%      1  107    9    1  913%
c i   29.2   64924   441902      9936    5954   1015 37609    7   117   38   6%      1  107    9    1  909%
c i   29.3   64914   441902     10147    6120   1033 37628    8   119   38   6%      1  109   13    1 1202%
c i   29.4   64909   441902     10192    6150   1038 37636    8   119   38   6%      1  109   11    1 1062%
c i   29.5   64902   441902     10324    6261   1045 37648    8   121   38   6%      1  110   11    1 1027%
c i   29.6   64901   441902     10361    6286   1050 37654    8   124   38   6%      1  113   11    1  977%
c i   29.6   64680   441902     10362    6286   1050 37654    8   124   38   6%      1  113   11    1  974%
c i   29.6   64596   441902     10368    6291   1050 37654    8   124   38   6%      1  113   11    1 1010%
c i   29.6   64591   441902     10395    6304   1054 37662    8   124   38   6%      1  113   10    1  938%
c i   29.6   64585   441902     10399    6307   1054 37662    8   123   38   6%      1  113   10    1  929%
c i   29.6   64579   441902     10435    6336   1057 37664    8   124   38   6%      1  113   10    1  917%
c i   29.7   64578   441902     10516    6404   1063 37670    8   124   38   6%      1  113    9    1  821%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   29.7   64451   441902     10564    6443   1066 37675    8   124   38   6%      1  113    8    1  760%
c i   30.1   64450   441902     11030    6793   1119 37730    8   125   38   6%      2  113    7    1  606%
c i   30.1   64441   441902     11045    6802   1122 37732    8   125   38   6%      2  113    7    1  600%
c i   30.1   64435   441902     11069    6817   1126 37735    8   125   38   6%      2  113    7    1  603%
c i   30.1   64323   441902     11075    6822   1126 37735    8   125   38   6%      2  113    7    1  630%
c i   30.1   64318   441902     11124    6864   1127 37737    8   124   38   6%      2  112    8    1  698%
c i   30.2   64317   441902     11240    6965   1129 37749    8   123   38   6%      2  111    8    1  678%
c 
c [simplification-8] limit 11266 conflicts (hard 21202) hit after 11266 conflicts
c [quatres-4] found 32997 quaternary clauses 51% in total
c [quatres-4-2] added 6 single-self-subsuming ternary resolvents
c [quatres-4-2] added 39 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 14362 schedulable variables 22%
c [ternres-4] 144 ternary resolvents (0 bin, 144 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] extracted 66 xors of average arity 2.8
c [gauss-4] connected 182 occurrences of 154 variables (average 1.2)
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-20] removed 19 variables
c [basicprobe-3] limit 13585117 penalty 0 = 0 + 0
c [basicprobe-3-0] 20991 probes remain 33% after last round
c [basicprobe-3-0] 175 units = 175 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 811 variables, found 53497 hbrs
c [bate-1] eliminated 52 asymmetric tautologies during probing
c [unhide-8] limit 543404 with penalty 0 = 0 + 0
c [unhide-8-8] 16 units, 529 failed, 6969 tauts, 0 hbrs, 5941 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 287 transitive binary clauses
c [transred-4] found 2 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 63004 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 234 blocked clauses
c [block-3] 234 < 1/100 * 426238 = 4262 considered unsuccessful
c [bca-4] limit of 10000000 steps and 844447 added (scaled 2)
c [bca-4] 101893 out of 126002 literals actually usable 81%
c [bca-4] added 32 blocked clauses in 264024 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 8183 pos 13.0% + 54675 neg 87.0% = 62858 sched 99.8% ret 142
c [sweep-4-1] 1036172 steps 16 queries 24548.38 avg class size
c [sweep-4-1] 218 decisions 15 SAT calls 58.47 avg env size
c [sweep-4-1] 62802 variables remain 100% (195 retained 0%)
c [decomp-21] removed 72 variables
c [sweep-4-1] removed 72 vars (0 failed, 0 eqs, 2 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 72 vars in TOTAL (1 rounds, 15 queries)
c [sort-queue-8] sorted 31474 enqueued variables after 11266 conflicts
c [score-dist-8] active 31454 (50%), one 9817 (16%), zero 21657 (34%)
c [score-dist-8] max exp 957, different 828 (86%)
c [score-dist-8] median active exp 694, avg 661.2
c [simplification-8] removed 1384 variables 2.2% (62928 remain 29%)
c [simplification-8] removed 20199 irredundant clauses 4.6% (421703 remain 35%)
c [simplification-8] maximum reduction of 5% = max (2%, 5%)
c [simplification-8] large reduction 5% >= 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 23266 (soft 13266 + delta 10000)
c [simplification-8] new conflict limit 13266 (hard 23266)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   32.6   62927   421703     11376    7018   1305 79208    8   125   38   6%      2  112   10    1  805%
c i   32.7   62920   421703     11500    7122   1315 79215    8   124   38   6%      1  112   10    1  856%
c i   32.7   62912   421703     11521    7133   1319 79220    8   125   38   6%      1  112   10    1  812%
c i   32.8   62884   421703     11545    7155   1320 79220    8   125   38   6%      1  112    9    1  779%
c i   32.8   62831   421703     11620    7205   1331 79228    8   125   38   6%      1  112    9    1  726%
c i   32.8   62709   421703     11642    7218   1332 79235    8   125   38   6%      1  112    8    1  691%
c i   32.8   62704   421703     11674    7245   1333 79236    8   125   38   6%      1  112    9    1  696%
c i   32.8   62703   421703     11682    7250   1333 79237    8   125   38   6%      1  112    9    1  704%
c i   32.8   62656   421703     11704    7265   1333 79242    8   125   38   6%      1  112    9    1  746%
c i   33.0   62605   421703     11913    7407   1367 79269    8   125   38   6%      1  112    8    1  649%
c i   33.0   62597   421703     11950    7437   1369 79272    8   124   38   6%      1  111    8    1  619%
c i   33.0   62589   421703     12016    7497   1371 79275    8   124   38   7%      1  110   11    1  880%
c i   33.0   62587   421703     12036    7507   1375 79279    8   123   38   7%      1  110   11    1  831%
c i   33.1   62584   421703     12162    7616   1379 79289    8   124   38   7%      1  110   10    1  766%
c i   33.1   62582   421703     12194    7642   1379 79293    8   124   38   7%      1  110    9    1  719%
c i   33.2   62581   421703     12258    7695   1380 79302    8   124   38   7%      1  110    9    1  689%
c i   33.2   62578   421703     12260    7696   1380 79302    8   124   38   7%      1  110    9    1  685%
c i   33.2   62575   421703     12261    7696   1380 79302    8   124   38   7%      1  110    9    1  683%
c i   33.2   62573   421703     12271    7704   1381 79302    8   124   38   7%      1  110    9    1  677%
c i   33.2   62564   421703     12277    7708   1382 79302    8   124   38   7%      1  110    9    1  668%
c i   33.2   62560   421703     12304    7730   1384 79304    8   123   38   7%      1  109    9    1  660%
c i   33.2   62552   421703     12325    7748   1385 79305    8   123   38   7%      1  109    8    1  648%
c i   33.2   62551   421703     12326    7748   1385 79305    8   123   38   7%      1  109    8    1  645%
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   33.2   62543   421703     12346    7757   1389 79310    8   123   38   7%      1  109    8    1  636%
c i   33.3   62541   421703     12385    7786   1393 79314    8   123   38   7%      1  109    8    1  613%
c i   33.3   62540   421703     12443    7834   1398 79315    8   123   38   7%      1  108    8    1  596%
c i   33.3   62539   421703     12444    7834   1398 79315    8   123   38   7%      1  108    8    1  593%
c i   33.3   62533   421703     12473    7856   1400 79318    8   123   38   7%      1  108    8    1  581%
c i   33.3   62405   421703     12495    7872   1402 79321    8   122   38   7%      1  108    7    1  560%
c i   33.4   62404   421703     12583    7937   1410 79334    8   122   38   7%      1  107    7    1  533%
c i   33.4   62399   421703     12662    8002   1416 79341    8   122   38   7%      1  108    8    1  602%
c i   33.6   62395   421703     12829    8143   1431 79351    8   123   38   7%      1  108   10    1  754%
c i   33.7   62393   421703     12906    8207   1436 79358    8   123   38   7%      1  108   10    1  738%
c i   33.7   62390   421703     13045    8330   1440 79364    8   122   38   7%      1  107   10    1  685%
c i   33.8   62387   421703     13211    8482   1446 79369    8   124   38   7%      1  109   10    1  736%
c 
c [simplification-9] limit 13304 conflicts (hard 23266) hit after 13304 conflicts
c [quatres-5] found 32009 quaternary clauses 53% in total
c [quatres-5-1] removed 2 duplicate quaternary clauses
c [quatres-5-2] added 2 single-self-subsuming ternary resolvents
c [quatres-5-2] added 5 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 62381 free variables schedulable
c [ternres-5] 51 ternary resolvents (0 bin, 51 trn)
c [ternres-5] 35083 variables remain 56% (27298 retained 44%)
c [decomp-22] removed 661 variables
c [simpleprobe-4] 12993 schedulable variables 21%
c [simpleprobe-4] limit 12386252 penalty 0 = 0 + 0
c [decomp-23] removed 624 variables
c [simpleprobe-4] 18081 variables remain 29% (43562 retained 71%)
c [simpleprobe-4] removed 624 variables, found 32606 hbrs, 240 units
c [unhide-9] limit 619312 with penalty 0 = 0 + 0
c [unhide-9-9] 6 units, 117 failed, 8489 tauts, 0 hbrs, 4710 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 332 transitive binary clauses
c [elim-7] 29080 variables 47% will be scheduled this time
c [elim-7] scheduled 29080 variables 47%
c [elim-7] limit of 30965632 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 35 variables 0% in round 1 in 29290641 steps
c [elim-7-1] backward subsumption/strengthening limit 1674991
c [elim-7-1-1] backward checking 514 touched variables 1%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 11 and strengthened 13 clauses in 199898 steps
c [elim-7-1] rescheduled 50 variables 0% by backward subsumption
c [elim-7-2] eliminated 9 variables 0% in round 2 in 24000 steps
c [elim-7-2] backward subsumption/strengthening limit 24000
c [elim-7-2-1] backward checking 49 touched variables 0%
c [elim-7-2-1] incomplete backward checking 0 remain 0%
c [elim-7-2] subsumed 4 and strengthened 3 clauses in 24001 steps
c [elim-7-2] rescheduled 13 variables 0% by backward subsumption
c [elim-7-3] eliminated 1 variables 0% in round 3 in 4968 steps
c [elim-7-3] backward subsumption/strengthening limit 4900
c [elim-7-3-1] backward checking 9 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 1 and strengthened 0 clauses in 4901 steps
c [elim-7] incomplete 2 not tried 0% in round 3
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 48 = 0% variables out of 29080 scheduled
c [elim-7] 48 < 1/100 * 29080 = 290 considered unsuccessful
c [bca-5] limit of 10000000 steps and 805009 added (scaled 2)
c [bca-5] 97037 out of 122822 literals actually usable 79%
c [bca-5] added 20 blocked clauses in 248646 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 8595 pos 14.0% + 52632 neg 86.0% = 61227 sched 99.7% ret 183
c [sweep-5-1] 10000517 steps 175 queries 2499.02 avg class size
c [sweep-5-1] 1744 decisions 146 SAT calls 80.71 avg env size
c [sweep-5-1] 56589 variables remain 92% (4777 retained 8%)
c [decomp-24] removed 152 variables
c [sweep-5-1] removed 152 vars (0 failed, 31 eqs, 69 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 152 vars in TOTAL (1 rounds, 174 queries)
c [sort-queue-9] sorted 44116 enqueued variables after 13304 conflicts
c [score-dist-9] active 17142 (28%), one 23844 (39%), zero 20272 (33%)
c [score-dist-9] max exp 515, different 433 (84%)
c [score-dist-9] median active exp 419, avg 383.4
c [simplification-9] removed 1123 variables 1.8% (61258 remain 29%)
c [simplification-9] removed 20167 irredundant clauses 4.8% (401536 remain 34%)
c [simplification-9] maximum reduction of 5% = max (2%, 5%)
c [simplification-9] large reduction 5% >= 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 25304 (soft 15304 + delta 10000)
c [simplification-9] new conflict limit 15304 (hard 25304)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   37.2   61257   401536     13649    8797   1469 122247    9   124   39   7%      2  108   10    1  695%
c i   37.2   61249   401536     13676    8819   1471 122249    9   124   39   7%      2  108   10    1  684%
c i   37.2   61246   401536     13677    8819   1471 122249    9   124   39   7%      2  108   10    1  682%
c i   37.2   61242   401536     13678    8819   1471 122249    9   124   39   7%      2  108   10    1  679%
c i   37.4   61237   401536     13846    8953   1485 122262    9   125   39   7%      2  109   10    2  643%
c i   37.5   61219   401536     13995    9061   1511 122273    9   127   39   7%      2  110    9    2  587%
c i   37.6   61216   401536     14090    9138   1519 122282    9   127   39   7%      1  110    8    2  551%
c i   37.8   61207   401536     14336    9344   1538 122296    9   132   39   7%      1  114   11    2  673%
c i   37.9   61199   401536     14496    9482   1546 122307    9   133   39   7%      1  116   12    2  737%
c i   38.1   61198   401536     14666    9619   1553 122327    9   134   39   7%      1  116   12    2  729%
c i   38.1   61197   401536     14696    9646   1553 122329    9   135   39   7%      1  117   15    2  891%
c i   38.1   61191   401536     14753    9691   1559 122333    9   135   39   7%      1  117   14    2  830%
c i   38.1   61183   401536     14754    9691   1559 122333    9   135   39   7%      1  117   14    2  827%
c i   38.2   61177   401536     14787    9719   1561 122334    9   136   39   7%      1  118   13    2  781%
c i   38.2   61175   401536     14871    9771   1577 122347    9   135   39   7%      1  117   11    2  653%
c i   38.3   61170   401536     14931    9809   1584 122359    9   135   39   7%      1  117   10    2  597%
c i   38.3   61163   401536     14932    9809   1584 122359    9   135   39   7%      1  117   10    2  594%
c i   38.3   61158   401536     14933    9809   1584 122359    9   135   39   7%      1  117   10    2  592%
c i   38.3   61142   401536     14934    9809   1584 122359    9   135   39   7%      1  117   10    2  590%
c i   38.3   61137   401536     14935    9809   1584 122359    9   135   39   7%      1  117   10    2  587%
c i   38.5   60979   401536     15150    9957   1609 122392    9   136   39   7%      1  117    9    2  519%
c i   38.6   60972   401536     15307   10082   1627 122403    9   136   39   7%      1  117   10    2  573%
c i   38.6   60971   401536     15308   10082   1627 122403    9   136   39   7%      1  117   10    2  570%
c 
c [simplification-10] limit 15384 conflicts (hard 25304) hit after 15384 conflicts
c [quatres-6] found 30223 quaternary clauses 52% in total
c [quatres-6-2] added 1 single-self-subsuming ternary resolvents
c [quatres-6-2] added 8 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] 34264 schedulable variables 56%
c [ternres-6] 57 ternary resolvents (0 bin, 57 trn)
c [ternres-6] 7900 variables remain 13% (53065 retained 87%)
c [card-4] limit 250000 penalty 3 = 3 + 0
c [card-4] found 854 at-most-one constraints of average size 4.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 250000 for elimination
c [card-4] 854 out of 854 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-5] limit 1000000 penalty 1 = 1 + 0
c [gauss-5] extracted 46 xors of average arity 2.7
c [gauss-5] connected 125 occurrences of 117 variables (average 1.1)
c [gauss-5] limit 1000000 penalty 1 = 1 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-25] removed 22 variables
c [treelook-4] limit 354243 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 55853 literals 46%
c [treelook-4] scheduling used 367580 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 354243 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 382635 steps
c [treelook-4] 55825 literals remain 46%
c [treelook-4] 19132 variables remain to probed next time 31%
c [decomp-26] removed 8 variables
c [treelook-4] removed 8 variables, found 2620 hbrs
c [unhide-10] limit 708487 with penalty 0 = 0 + 0
c [unhide-10-10] 9 units, 522 failed, 8998 tauts, 0 hbrs, 7318 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 268 transitive binary clauses
c [transred-6] found 2 units
c [cce-3] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 233 (0%) of length 9
c [cce-3-1] eliminated 4 clauses out of 484 (1%) of length 7
c [cce-3-1] eliminated 1 clauses out of 1289 (0%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 6 large clauses in 7500005 steps
c [cce-3-1] allowing another 3750002 steps for small clauses
c [cce-3-1] scheduling 322611 clauses = 196055 binary + 126556 ternary
c [cce-3-1] tried to eliminate 160 small clauses 0%
c [cce-3-1] eliminated 30 binary clauses 0%
c [cce-3-1] eliminated 24 ternary clauses 0%
c [cce-3-1] eliminated 54 small clauses 0%
c [cce-3-1] eliminated 3819 small clauses in 7500005 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 3825 covered clauses in round 1
c [cce-3] eliminated 3825 covered clauses in TOTAL during 1 rounds
c [cce-3] 3825 < 1/100 * 399297 = 3992 considered unsuccessful
c [bca-6] limit of 10000000 steps and 791653 added (scaled 2)
c [bca-6] 94042 out of 120926 literals actually usable 78%
c [bca-6] added 29 blocked clauses in 240604 steps
c [sweep-6] limit 1062731 penalty 0 = 0 + 0
c [sweep-6-1] 7510 pos 13.4% + 48414 neg 86.6% = 55924 sched 92.5% ret 4538
c [sweep-6-1] 1138931 steps 30 queries 13314.67 avg class size
c [sweep-6-1] 335 decisions 26 SAT calls 74.35 avg env size
c [sweep-6-1] 55744 variables remain 92% (4715 retained 8%)
c [decomp-27] removed 26 variables
c [sweep-6-1] removed 26 vars (0 failed, 4 eqs, 9 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 26 vars in TOTAL (1 rounds, 29 queries)
c [sort-queue-10] sorted 41422 enqueued variables after 15384 conflicts
c [score-dist-10] active 19014 (31%), one 21745 (36%), zero 19677 (33%)
c [score-dist-10] max exp 563, different 498 (88%)
c [score-dist-10] median active exp 455, avg 401.2
c [simplification-10] removed 529 variables 0.9% (60436 remain 28%)
c [simplification-10] removed 6175 irredundant clauses 1.5% (395361 remain 33%)
c [simplification-10] maximum reduction of 2% = max (1%, 2%)
c [simplification-10] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-10] new conflict interval 10666
c [simplification-10] penalized conflict interval 10666 = 1 * 10666
c [simplification-10] hard conflict limit 36050 (soft 26050 + delta 10000)
c [simplification-10] new conflict limit 26050 (hard 36050)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   41.1   60435   395361     15694   10329   1671 115999    9   142   39   7%      2  122   12    2  665%
c i   41.2   60433   395361     15806   10424   1674 116012    9   143   39   7%      2  123   11    2  603%
c i   41.3   60432   395361     15889   10488   1683 116020    9   142   39   7%      1  122    9    2  526%
c i   41.5   60431   395361     16225   10760   1704 116056   10   144   39   7%      2  123   13    2  728%
c i   41.5   60430   395361     16255   10781   1707 116059   10   144   39   7%      2  123   13    2  719%
c i   41.6   60424   395361     16287   10810   1708 116060   10   145   39   7%      2  124   15    2  820%
c i   41.7   60418   395361     16372   10881   1716 116064   10   149   39   7%      2  128   15    2  794%
c i   41.8   60409   395361     16595   11069   1732 116078   10   149   39   7%      2  127   13    2  680%
c i   41.9   60381   395361     16616   11084   1736 116079   10   149   39   7%      1  127   12    2  653%
c i   42.1   60365   395361     16849   11259   1758 116107   10   150   39   7%      2  128   12    2  615%
c i   42.1   60364   395361     16868   11274   1761 116107   10   150   39   7%      1  128   12    2  601%
c i   42.3   60349   395361     17069   11440   1778 116120   10   151   39   7%      1  129   12    2  590%
c i   42.4   60348   395361     17152   11509   1785 116126   10   151   39   7%      1  129   12    2  601%
c i   42.4   60345   395361     17153   11509   1785 116126   10   151   39   7%      1  129   12    2  598%
c i   42.5   60341   395361     17348   11663   1803 116143   10   150   39   7%      1  127   11    2  526%
c i   42.6   60340   395361     17443   11740   1808 116155   10   149   39   7%      1  126   11    2  522%
c i   42.8   60315   395361     17696   11938   1827 116178   10   150   39   7%      1  126   10    2  507%
c i   42.9   60300   395361     17752   11979   1832 116185   10   150   39   7%      1  126   10    2  468%
c i   43.2   60282   395361     18021   12198   1842 116217   10   153   39   7%      1  129   11    2  522%
c i   43.2   60275   395361     18035   12207   1844 116219   10   153   39   7%      1  128   11    2  508%
c i   43.3   60272   395361     18164   12317   1854 116227   10   152   39   7%      1  127   11    2  514%
c i   43.6   60020   395361     18538   12616   1877 116267   11   154   39   7%      2  129   14    2  654%
c i   43.8   60019   395361     18728   12782   1888 116279   11   157   39   7%      2  131   15    2  669%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   44.0   59770   395361     18982   12994   1907 116292   11   156   39   7%      2  130   18    2  776%
c i   44.3   59768   395361     19493   13433   1937 116320   11   153   39   7%      3  125   12    2  492%
c i   44.4   59759   395361     19672   13582   1952 116332   11   154   39   7%      2  127   11    2  478%
c i   44.6   59753   395361     19958   13845   1959 116342   12   152   39   8%      2  124   20    2  813%
c i   44.7   59749   395361     20137   13997   1968 116352   12   151   39   8%      2  122   18    3  707%
c i   44.7   59746   395361     20233   14073   1980 116358   12   151   39   8%      2  122   15    3  587%
c i   44.8   59733   395361     20307   14131   1986 116367   12   150   39   8%      2  121   15    3  573%
c i   44.8   59726   395361     20452   14259   1987 116378   13   148   39   9%      2  119   18    3  683%
c i   44.9   59722   395361     20589   14379   1993 116385   13   147   39   9%      2  118   17    3  662%
c i   45.0   59717   395361     20688   14454   2006 116392   13   149   39   9%      1  120   14    3  550%
c i   45.2   59710   395361     20869   14609   2017 116403   13   150   39   8%      1  120   14    3  511%
c i   45.2   59664   395361     20873   14611   2018 116403   13   150   39   8%      1  120   13    3  510%
c i   45.2   59626   395361     20874   14611   2018 116403   13   150   39   8%      1  120   13    3  508%
c i   45.2   59625   395361     20880   14615   2019 116403   13   150   39   8%      1  120   13    3  502%
c i   45.3   59620   395361     20972   14697   2023 116408   13   150   40   8%      1  121   13    3  498%
c i   45.3   59615   395361     20988   14708   2027 116408   13   150   40   8%      1  121   13    3  479%
c i   45.3   59610   395361     20999   14717   2027 116409   13   150   40   8%      1  121   13    3  478%
c i   45.4   59609   395361     21139   14831   2036 116420   13   152   40   8%      1  122   14    3  526%
c i   45.4   59601   395361     21218   14903   2038 116422   13   152   40   9%      1  122   19    3  701%
c i   45.7   59594   395361     21499   15145   2054 116437   14   157   40   9%      1  126   17    3  616%
c i   45.7   59593   395361     21565   15200   2058 116441   14   157   40   9%      1  126   17    3  618%
c i   45.8   59588   395361     21714   15329   2067 116444   14   159   40   9%      1  128   25    3  854%
c i   45.8   59584   395361     21715   15329   2067 116444   14   159   40   9%      1  128   25    3  851%
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   45.9   59547   395361     21767   15369   2070 116448   14   159   40   9%      1  127   22    3  767%
c i   46.2   59530   395361     22155   15705   2091 116458   15   158   40   9%      2  126   19    3  625%
c i   46.8   59525   395361     22849   16310   2129 116486   15   159   40  10%      4  126   19    3  599%
c i   46.9   59279   395361     22926   16376   2131 116492   15   161   40   9%      3  127   18    3  577%
c i   46.9   59274   395361     22964   16410   2133 116492   15   161   40   9%      3  127   18    3  563%
c i   47.2   59270   395361     23462   16843   2154 116519   16   159   40  10%      3  125   21    3  645%
c i   47.5   59269   395361     23774   17125   2169 116529   16   161   40  10%      3  126   14    3  414%
c i   47.7   59238   395361     24077   17383   2188 116552   16   159   40  10%      3  123   14    3  404%
c i   47.9   59037   395361     24247   17530   2191 116567   16   161   40  10%      2  125   18    3  515%
c i   48.0   59036   395361     24393   17655   2198 116574   16   160   40  10%      2  124   15    3  436%
c i   48.2   59035   395361     24620   17852   2211 116589   16   163   41  10%      2  126   14    4  393%
c i   48.5   59030   395361     24949   18129   2232 116610   16   169   41   9%      2  131   17    4  465%
c i   48.8   59029   395361     25137   18290   2243 116624   16   172   41   9%      2  134   15    4  420%
c i   48.9   59022   395361     25308   18450   2248 116627   16   175   41   9%      2  136   17    4  471%
c i   49.0   59021   395361     25344   18482   2248 116630   16   175   41   9%      2  136   17    4  469%
c i   49.1   59020   395361     25515   18635   2256 116634   16   176   42   9%      2  138   20    4  527%
c i   49.5   59016   395361     25889   18943   2272 116663   16   178   42   9%      2  139   20    4  536%
c i   49.5   59010   395361     25928   18977   2274 116665   16   178   42   9%      2  139   20    4  528%
c 
c [simplification-11] limit 26083 conflicts (hard 36050) hit after 26087 conflicts
c [quatres-7] found 29279 quaternary clauses 51% in total
c [quatres-7-2] added 5 single-self-subsuming ternary resolvents
c [quatres-7-2] added 3 quaternary resolvents
c [ternres-7] limit 5856511 with penalty 0 = 0 + 0
c [ternres-7] 7648 schedulable variables 13%
c [ternres-7] 43 ternary resolvents (0 bin, 43 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-28] removed 1507 variables
c [basicprobe-4] limit 29282558 penalty 0 = 0 + 0
c [basicprobe-4-0] 17989 probes remain 31% after last round
c [basicprobe-4-0] 446 units = 433 failed (97%) + 13 lifted (3%)
c [basicprobe-4-0] removed 897 variables, found 93865 hbrs
c [bate-2] eliminated 74 asymmetric tautologies during probing
c [unhide-11] limit 1171302 with penalty 0 = 0 + 0
c [unhide-11-11] 51 units, 125 failed, 7286 tauts, 0 hbrs, 24519 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 288 transitive binary clauses
c [transred-7] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 57706 variables 100%
c [block-4] limit of 14641279 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 339 blocked clauses
c [block-4] 339 < 1/100 * 364967 = 3649 considered unsuccessful
c [bca-7] limit of 10000000 steps and 725843 added (scaled 2)
c [bca-7] 82188 out of 115356 literals actually usable 71%
c [bca-7] added 12 blocked clauses in 212119 steps
c [sweep-7] limit 1756953 penalty 0 = 0 + 0
c [sweep-7-1] 7770 pos 14.6% + 45514 neg 85.4% = 53284 sched 92.4% ret 4393
c [sweep-7-1] 1771854 steps 43 queries 10709.07 avg class size
c [sweep-7-1] 452 decisions 29 SAT calls 58.86 avg env size
c [sweep-7-1] 52999 variables remain 92% (4678 retained 8%)
c [decomp-29] removed 283 variables
c [sweep-7-1] removed 283 vars (0 failed, 13 eqs, 25 impls)
c [sweep-7] removed 283 vars in TOTAL (1 rounds, 42 queries)
c [sort-queue-11] sorted 24226 enqueued variables after 26087 conflicts
c [score-dist-11] active 33168 (58%), one 9397 (16%), zero 14829 (26%)
c [score-dist-11] max exp 865, different 769 (89%)
c [score-dist-11] median active exp 707, avg 634.2
c [simplification-11] removed 1611 variables 2.7% (57394 remain 27%)
c [simplification-11] removed 33527 irredundant clauses 8.5% (361834 remain 30%)
c [simplification-11] maximum reduction of 8% = max (3%, 8%)
c [simplification-11] large reduction 8% >= 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 38087 (soft 28087 + delta 10000)
c [simplification-11] new conflict limit 28087 (hard 38087)
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   52.9   57393   361834     26158   18919   2266 194732   17   180   43   9%      2  140   19    4  488%
c i   53.2   57387   361834     26476   19187   2290 194748   17   184   44   9%      2  143   16    4  420%
c i   53.3   57386   361834     26500   19204   2293 194751   17   183   44   9%      2  142   15    4  392%
c i   53.4   57385   361834     26613   19307   2296 194757   17   185   44   9%      2  144   17    4  425%
c i   53.5   57384   361834     26724   19401   2298 194769   17   186   44   9%      1  145   17    4  428%
c i   53.7   57372   361834     26899   19548   2302 194785   16   188   44   9%      1  146   14    4  347%
c i   53.7   57369   361834     26971   19607   2307 194787   16   186   44   9%      1  144   13    4  336%
c i   54.0   57365   361834     27280   19876   2323 194804   16   188   44   9%      1  146   17    4  409%
c i   54.1   57361   361834     27322   19914   2325 194805   16   188   44   9%      1  145   15    4  381%
c i   54.1   57360   361834     27323   19914   2325 194805   16   188   44   9%      1  145   15    4  380%
c i   54.1   57359   361834     27366   19951   2328 194807   16   187   44   9%      1  144   15    4  369%
c i   54.1   57351   361834     27367   19951   2328 194807   16   187   44   9%      1  144   15    4  367%
c i   54.7   57350   361834     28036   20549   2346 194824   17   190   44   9%      3  146   21    4  496%
c i   54.7   57345   361834     28099   20604   2347 194828   17   190   44   9%      3  146   21    4  489%
c 
c [simplification-12] limit 28107 conflicts (hard 38087) hit after 28107 conflicts
c [quatres-8] found 28605 quaternary clauses 51% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 2 single-self-subsuming ternary resolvents
c [quatres-8-2] added 1 quaternary resolvents
c [ternres-8] limit 6319394 with penalty 0 = 0 + 0
c [ternres-8] all 57345 free variables schedulable
c [ternres-8] 41 ternary resolvents (1 bin, 40 trn)
c [ternres-8] 14427 variables remain 25% (42918 retained 75%)
c [decomp-30] removed 71 variables
c [simpleprobe-5] 17045 schedulable variables 30%
c [simpleprobe-5] limit 25277577 penalty 0 = 0 + 0
c [decomp-31] removed 1855 variables
c [simpleprobe-5] 6668 variables remain 12% (48800 retained 88%)
c [simpleprobe-5] removed 1855 variables, found 40320 hbrs, 783 units
c [unhide-12] limit 1263878 with penalty 0 = 0 + 0
c [unhide-12-12] 16 units, 425 failed, 24623 tauts, 0 hbrs, 21018 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 317 transitive binary clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 55216 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 631939440 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 3706 variables 7% in round 1 in 29369063 steps
c [elim-8-1] backward subsumption/strengthening limit 29369000
c [elim-8-1-1] backward checking 11719 touched variables 21%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 87 and strengthened 348 clauses in 2683816 steps
c [elim-8-1] rescheduled 1059 variables 2% by backward subsumption
c [elim-8-2] eliminated 124 variables 0% in round 2 in 929746 steps
c [elim-8-2] backward subsumption/strengthening limit 929700
c [elim-8-2-1] backward checking 999 touched variables 2%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 80 and strengthened 65 clauses in 383855 steps
c [elim-8-2] rescheduled 238 variables 0% by backward subsumption
c [elim-8-3] eliminated 33 variables 0% in round 3 in 206757 steps
c [elim-8-3] backward subsumption/strengthening limit 206700
c [elim-8-3-1] backward checking 244 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 20 and strengthened 26 clauses in 181287 steps
c [elim-8] incomplete 101 not tried 0% in round 3
c [gc-82] reconnected 192716 binary clauses (produced 0 empty 5 units)
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 3893 = 7% variables out of 55216 scheduled
c [bca-8] limit of 10000000 steps and 671659 added (scaled 2)
c [bca-8] 75264 out of 102648 literals actually usable 73%
c [bca-8] added 56 blocked clauses in 192218 steps
c [sweep-8] limit 1895818 penalty 0 = 0 + 0
c [sweep-8-1] 7578 pos 15.9% + 40148 neg 84.1% = 47726 sched 93.0% ret 3597
c [sweep-8-1] 1926832 steps 43 queries 5949.23 avg class size
c [sweep-8-1] 521 decisions 35 SAT calls 89.23 avg env size
c [sweep-8-1] 47224 variables remain 92% (4066 retained 8%)
c [decomp-32] removed 52 variables
c [sweep-8-1] removed 52 vars (0 failed, 9 eqs, 14 impls)
c [sweep-8] removed 52 vars in TOTAL (1 rounds, 42 queries)
c [sort-queue-12] sorted 20755 enqueued variables after 28107 conflicts
c [score-dist-12] active 30516 (60%), one 8978 (18%), zero 11777 (23%)
c [score-dist-12] max exp 899, different 809 (90%)
c [score-dist-12] median active exp 694, avg 641.8
c [simplification-12] removed 6074 variables 10.6% (51271 remain 24%)
c [simplification-12] removed 26645 irredundant clauses 7.4% (335189 remain 28%)
c [simplification-12] maximum reduction of 11% = max (11%, 7%)
c [simplification-12] large reduction 11% >= 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 40107 (soft 30107 + delta 10000)
c [simplification-12] new conflict limit 30107 (hard 40107)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   58.4   51270   335189     28275   13731   2028 175618   17   191   38   9%      3  146   18    4  429%
c i   59.1   51268   335189     29119   14484   2073 175649   17   190   38   9%      5  144   13    4  304%
c i   59.5   51219   335189     29556   14869   2094 175667   17   192   38   9%      4  144   15    5  343%
c 
c [simplification-13] limit 30107 conflicts (hard 40107) hit after 30107 conflicts
c [quatres-9] found 26628 quaternary clauses 51% in total
c [quatres-9-1] removed 2 duplicate quaternary clauses
c [quatres-9-2] added 21 quaternary resolvents
c [ternres-9] limit 6739160 with penalty 0 = 0 + 0
c [ternres-9] 12831 schedulable variables 25%
c [ternres-9] 380 ternary resolvents (3 bin, 377 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-6] limit 500000 penalty 2 = 2 + 0
c [gauss-6] extracted 10 xors of average arity 3.0
c [gauss-6] connected 30 occurrences of 30 variables (average 1.0)
c [gauss-6] limit 500000 penalty 2 = 2 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-33] removed 2 variables
c [treelook-5] limit 673916 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 65611 literals 64%
c [treelook-5] scheduling used 674100 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 673916 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 691498 steps
c [treelook-5] 65598 literals remain 64%
c [treelook-5] 14823 variables remain to probed next time 29%
c [treelook-5] removed 0 variables, found 4912 hbrs
c [unhide-13] limit 1347832 with penalty 0 = 0 + 0
c [unhide-13-13] 7 units, 25 failed, 4202 tauts, 0 hbrs, 8763 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 367 transitive binary clauses
c [transred-9] found 2 units
c [bca-9] limit of 10000000 steps and 662423 added (scaled 2)
c [bca-9] 73226 out of 102326 literals actually usable 72%
c [bca-9] added 9 blocked clauses in 186516 steps
c [sweep-9] limit 2021748 penalty 0 = 0 + 0
c [sweep-9-1] 7404 pos 15.7% + 39730 neg 84.3% = 47134 sched 92.1% ret 4028
c [sweep-9-1] 2031714 steps 39 queries 5398.97 avg class size
c [sweep-9-1] 481 decisions 32 SAT calls 82.03 avg env size
c [sweep-9-1] 46756 variables remain 91% (4403 retained 9%)
c [decomp-35] removed 39 variables
c [sweep-9-1] removed 39 vars (0 failed, 6 eqs, 16 impls)
c [sweep-9] 39 < 1/1000 * 51162 = 51 considered unsuccessful
c [sweep-9] removed 39 vars in TOTAL (1 rounds, 38 queries)
c [sort-queue-13] sorted 20485 enqueued variables after 30107 conflicts
c [score-dist-13] active 30638 (60%), one 9292 (18%), zero 11193 (22%)
c [score-dist-13] max exp 926, different 807 (87%)
c [score-dist-13] median active exp 817, avg 701.8
c [simplification-13] removed 93 variables 0.2% (51123 remain 24%)
c [simplification-13] removed 4452 irredundant clauses 1.3% (330737 remain 28%)
c [simplification-13] maximum reduction of 1% = max (0%, 1%)
c [simplification-13] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-13] new conflict interval 20666
c [simplification-13] penalized conflict interval 20666 = 1 * 20666
c [simplification-13] hard conflict limit 61106 (soft 50773 + delta 10333)
c [simplification-13] new conflict limit 50773 (hard 61106)
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   61.6   51122   330737     30140   15370   2459 181781   17   189   38   9%      4  140   17    5  375%
c i   61.7   51115   330737     30283   15497   2463 181785   17   188   39   9%      4  139   17    5  366%
c i   61.8   51111   330737     30529   15717   2475 181792   17   184   39   9%      3  134   19    5  399%
c i   61.9   51110   330737     30592   15770   2481 181793   17   182   39   9%      3  133   16    5  346%
c i   62.4   51108   330737     31360   16453   2513 181826   17   182   39   9%      5  131   19    5  387%
c i   62.8   51107   330737     31985   17002   2540 181853   17   182   39   9%      5  129   19    5  392%
c i   63.2   51103   330737     32779   17689   2563 181882   17   176   39  10%      5  122   19    5  372%
c i   63.2   51102   330737     32815   17718   2566 181884   17   176   39  10%      5  122   18    5  347%
c i   63.3   51100   330737     32939   17833   2569 181887   17   173   39  10%      5  119   17    5  336%
c i   63.4   51099   330737     33195   18057   2578 181902   17   173   39  10%      4  118   17    5  333%
c i   63.4   51094   330737     33217   18078   2578 181902   17   172   39  10%      4  118   17    5  334%
c i   64.4   51091   330737     34402   19138   2632 181950   17   174   39  10%      8  117   13    5  234%
c i   64.5   51083   330737     34482   19209   2637 181952   17   174   39  10%      7  117   19    5  357%
c i   64.7   51070   330737     34712   19413   2642 181966   17   176   39  10%      6  118   18    5  335%
c i   64.9   51069   330737     35112   19771   2660 181980   17   171   39  10%      5  113   19    6  335%
c i   64.9   51066   330737     35127   19784   2660 181981   17   171   39  10%      5  112   18    6  329%
c i   65.0   51065   330737     35398   20027   2673 181985   17   170   39  10%      4  111   16    6  287%
c i   65.1   51064   330737     35576   20190   2678 181992   17   170   39  10%      3  111   18    6  320%
c i   65.2   51063   330737     35604   20217   2678 181992   17   171   39  10%      3  112   18    6  314%
c i   65.4   51062   330737     35912   20486   2693 182009   17   172   39  10%      3  113   16    6  282%
c i   65.5   51059   330737     35948   20518   2695 182009   17   172   39  10%      3  112   19    6  335%
c i   65.8   51058   330737     36344   20857   2712 182031   17   173   39  10%      2  113   17    6  289%
c i   66.3   51052   330737     36878   21334   2735 182051   17   175   39  10%      3  114   16    6  273%
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   66.3   51037   330737     36957   21403   2740 182054   17   175   39  10%      3  114   17    6  294%
c i   66.3   51033   330737     37041   21462   2748 182065   17   173   39  10%      2  112   19    6  315%
c i   66.4   51029   330737     37077   21495   2749 182066   17   173   39  10%      2  111   18    6  304%
c i   66.5   51021   330737     37194   21601   2755 182069   17   175   39  10%      2  113   20    6  345%
c i   66.8   51018   330737     37564   21926   2775 182085   17   179   40  10%      2  117   20    6  331%
c i   67.2   51017   330737     37918   22241   2788 182105   17   178   40  10%      2  115   17    6  275%
c i   67.6   51013   330737     38396   22648   2818 182136   17   179   40   9%      2  116   14    6  223%
c i   67.6   51010   330737     38461   22704   2820 182138   17   179   40   9%      2  116   16    6  263%
c i   67.9   51006   330737     38804   23006   2835 182147   17   180   40   9%      2  115   20    6  321%
c i   68.3   51002   330737     39295   23445   2854 182162   17   180   41  10%      2  114   18    6  291%
c i   68.3   50996   330737     39369   23513   2855 182164   17   178   41  10%      2  112   18    6  288%
c i   68.4   50993   330737     39456   23582   2862 182168   17   177   41  10%      2  112   15    6  243%
c i   68.4   50858   330737     39467   23592   2862 182168   17   177   41  10%      2  112   15    6  246%
c i   68.5   50833   330737     39713   23808   2874 182181   17   176   41  10%      2  110   16    6  261%
c i   68.9   50775   330737     40085   24138   2895 182192   17   179   41  10%      2  112   18    6  277%
c i   68.9   50774   330737     40122   24168   2897 182196   17   179   41  10%      2  113   17    6  261%
c i   69.1   50773   330737     40342   24352   2907 182212   17   177   42  10%      1  110   19    6  296%
c i   69.4   50772   330737     40674   24648   2920 182219   18   177   42  10%      1  110   20    7  312%
c i   69.5   50771   330737     40877   24830   2928 182229   18   179   42  10%      1  111   19    7  290%
c i   69.7   50765   330737     41055   24983   2935 182237   18   179   42  10%      1  111   17    7  256%
c i   69.7   50761   330737     41139   25054   2940 182239   17   177   42  10%      1  109   15    7  227%
c i   69.9   50758   330737     41291   25181   2951 182249   17   176   42  10%      1  108   13    7  193%
c i   70.0   50750   330737     41467   25339   2959 182255   17   176   42  10%      1  108   13    7  196%
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   70.2   50746   330737     41675   25522   2970 182264   17   178   42  10%      1  108   18    7  276%
c i   70.3   50743   330737     41770   25610   2973 182267   17   177   42  10%      1  107   17    7  258%
c i   70.5   50742   330737     42214   26018   2983 182276   18   176   42  10%      1  106   27    7  391%
c i   70.6   50741   330737     42225   26027   2984 182276   18   176   42  10%      1  105   26    7  378%
c i   70.7   50740   330737     42471   26234   2994 182284   19   174   42  11%      1  104   24    7  343%
c i   70.7   50733   330737     42472   26234   2994 182284   19   174   42  11%      1  104   23    7  341%
c i   70.7   50732   330737     42473   26234   2994 182284   19   174   42  11%      1  104   23    7  340%
c i   70.7   50728   330737     42474   26234   2994 182284   19   174   42  11%      1  104   23    7  339%
c i   70.7   50718   330737     42491   26248   2994 182285   19   174   42  11%      1  103   23    7  329%
c i   70.8   50717   330737     42597   26338   3001 182289   18   173   42  11%      1  102   20    7  285%
c i   71.0   50713   330737     42813   26532   3008 182294   18   171   42  11%      1   99   19    7  275%
c i   71.0   50710   330737     42843   26558   3008 182296   18   171   42  11%      1  100   18    7  254%
c i   71.2   50707   330737     43042   26736   3014 182308   18   172   42  11%      1  101   17    7  251%
c i   71.7   50706   330737     43608   27236   3038 182336   18   171   42  11%      2   98   20    7  276%
c i   71.9   50705   330737     43763   27376   3041 182343   19   171   42  11%      2   99   22    7  312%
c i   71.9   50704   330737     43790   27400   3042 182344   19   171   42  11%      2   98   24    7  339%
c i   72.0   50703   330737     43909   27504   3051 182348   19   171   42  11%      1   98   24    7  331%
c i   72.1   50700   330737     44057   27632   3058 182356   19   171   42  11%      1   98   19    7  264%
c i   72.3   50699   330737     44234   27787   3067 182366   19   171   42  11%      1   98   15    7  213%
c i   72.3   50696   330737     44264   27815   3067 182367   19   171   42  11%      1   98   16    7  220%
c i   72.6   50693   330737     44552   28071   3073 182383   19   173   42  11%      1  100   18    7  250%
c i   72.7   50692   330737     44624   28132   3076 182389   19   174   42  11%      1  101   19    7  264%
c i   72.7   50294   330737     44629   28135   3076 182390   19   174   42  11%      1  101   19    7  261%
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   50293   330737     44815   28301   3083 182402   19   176   42  11%      1  102   18    7  246%
c i   72.9   50292   330737     44874   28347   3089 182406   19   176   42  11%      1  102   19    7  260%
c i   72.9   50192   330737     44929   28392   3093 182408   19   175   42  11%      1  101   18    7  243%
c i   73.2   50191   330737     45253   28677   3102 182421   18   180   42  10%      1  105   16    7  221%
c i   73.2   50162   330737     45256   28678   3102 182422   18   180   42  10%      1  105   16    7  219%
c i   73.5   50157   330737     45576   28937   3137 182442   18   178   43  10%      1  103   12    7  163%
c i   75.1   50135   330737     47431   30590   3224 182508   19   181   44  11%     15  103   22    8  279%
c i   75.1   50128   330737     47433   30591   3224 182508   19   181   44  11%     14  103   21    8  277%
c i   75.4   50116   330737     47758   30884   3235 182521   20   183   44  11%     11  104   25    8  324%
c i   75.4   50113   330737     47760   30884   3236 182521   20   183   44  11%     11  104   25    8  322%
c i   75.8   50098   330737     48398   31453   3252 182540   20   180   44  11%      8  100   23    8  288%
c i   75.8   50096   330737     48399   31453   3252 182540   20   180   44  11%      8  100   23    8  287%
c i   75.8   50094   330737     48400   31453   3252 182540   20   180   44  11%      8  100   23    8  286%
c i   76.1   50087   330737     48873   31879   3277 182546   20   177   45  11%      6   97   21    8  266%
c i   76.2   50086   330737     49030   32008   3286 182555   20   176   45  11%      5   95   21    8  261%
c i   76.5   50085   330737     49400   32337   3301 182569   20   175   46  12%      4   94   20    8  248%
c i   76.5   50083   330737     49402   32337   3301 182569   20   175   46  12%      4   94   20    8  247%
c i   76.6   50078   330737     49427   32361   3301 182569   20   175   46  11%      4   94   19    8  237%
c i   76.6   50075   330737     49461   32389   3303 182570   20   176   46  11%      3   95   18    8  223%
c i   76.7   50074   330737     49576   32493   3305 182573   20   176   46  11%      3   95   20    8  240%
c i   76.7   50073   330737     49589   32503   3306 182573   20   176   46  11%      3   94   19    8  233%
c i   77.1   50072   330737     49974   32834   3325 182597   20   174   47  12%      2   92   21    8  249%
c 
c [simplification-14] limit 50843 conflicts (hard 61106) hit after 50847 conflicts
c [quatres-10] found 26454 quaternary clauses 49% in total
c [quatres-10-1] removed 1 duplicate quaternary clauses
c [quatres-10-2] added 5 single-self-subsuming ternary resolvents
c [quatres-10-2] added 7 quaternary resolvents
c [ternres-10] limit 10734179 with penalty 0 = 0 + 0
c [ternres-10] all 50069 free variables schedulable
c [ternres-10] 433 ternary resolvents (0 bin, 433 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-36] removed 1172 variables
c [basicprobe-5] limit 53670897 penalty 0 = 0 + 0
c [basicprobe-5-0] 12350 probes remain 25% after last round
c [basicprobe-5-0] 727 units = 725 failed (100%) + 2 lifted (0%)
c [basicprobe-5-0] removed 1200 variables, found 161906 hbrs
c [bate-3] eliminated 222 asymmetric tautologies during probing
c [unhide-14] limit 2146835 with penalty 0 = 0 + 0
c [unhide-14-14] 9 units, 346 failed, 24431 tauts, 0 hbrs, 60989 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 387 transitive binary clauses
c [transred-10] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 67088621 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 41
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 40
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 39
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 38
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 37
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 36
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 35
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 34
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 33
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 32
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 31
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 30
c [cce-4-1] eliminated 3 clauses out of 4 (75%) of length 29
c [cce-4-1] eliminated 3 clauses out of 6 (50%) of length 28
c [cce-4-1] eliminated 5 clauses out of 6 (83%) of length 27
c [cce-4-1] eliminated 4 clauses out of 7 (57%) of length 26
c [cce-4-1] eliminated 7 clauses out of 8 (88%) of length 25
c [cce-4-1] eliminated 5 clauses out of 8 (62%) of length 24
c [cce-4-1] eliminated 7 clauses out of 8 (88%) of length 23
c [cce-4-1] eliminated 5 clauses out of 9 (56%) of length 22
c [cce-4-1] eliminated 9 clauses out of 10 (90%) of length 21
c [cce-4-1] eliminated 6 clauses out of 10 (60%) of length 20
c [cce-4-1] eliminated 9 clauses out of 10 (90%) of length 19
c [cce-4-1] eliminated 6 clauses out of 11 (55%) of length 18
c [cce-4-1] eliminated 10 clauses out of 11 (91%) of length 17
c [cce-4-1] eliminated 7 clauses out of 12 (58%) of length 16
c [cce-4-1] eliminated 12 clauses out of 13 (92%) of length 15
c [cce-4-1] eliminated 9 clauses out of 14 (64%) of length 14
c [cce-4-1] eliminated 12 clauses out of 14 (86%) of length 13
c [cce-4-1] eliminated 11 clauses out of 16 (69%) of length 12
c [cce-4-1] eliminated 11 clauses out of 14 (79%) of length 11
c [cce-4-1] eliminated 12 clauses out of 48 (25%) of length 10
c [cce-4-1] eliminated 11 clauses out of 128 (9%) of length 9
c [cce-4-1] eliminated 9 clauses out of 262 (3%) of length 8
c [cce-4-1] eliminated 15 clauses out of 370 (4%) of length 7
c [cce-4-1] eliminated 20 clauses out of 1108 (2%) of length 6
c [cce-4-1] eliminated 9992 clauses out of 15491 (65%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 10218 large clauses in 67088621 steps
c [cce-4-1] allowing another 33544310 steps for small clauses
c [cce-4-1] scheduling 246296 clauses = 160404 binary + 85892 ternary
c [cce-4-1] tried to eliminate 2540 small clauses 1%
c [cce-4-1] eliminated 546 binary clauses 0%
c [cce-4-1] eliminated 183 ternary clauses 0%
c [cce-4-1] eliminated 729 small clauses 0%
c [cce-4-1] eliminated 2835 small clauses in 67088628 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 13053 covered clauses in round 1
c [cce-4] eliminated 13053 covered clauses in TOTAL during 1 rounds
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 48445 variables 100%
c [elim-9] limit of 107341795 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 7482 variables 15% in round 1 in 24947137 steps
c [elim-9-1] backward subsumption/strengthening limit 24947100
c [elim-9-1-1] backward checking 20648 touched variables 43%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 77 and strengthened 247 clauses in 3109090 steps
c [elim-9-1] rescheduled 746 variables 2% by backward subsumption
c [elim-9-2] eliminated 86 variables 0% in round 2 in 467436 steps
c [elim-9-2] backward subsumption/strengthening limit 467400
c [elim-9-2-1] backward checking 751 touched variables 2%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 45 and strengthened 58 clauses in 455581 steps
c [elim-9-2] rescheduled 180 variables 0% by backward subsumption
c [elim-9-3] eliminated 14 variables 0% in round 3 in 154217 steps
c [elim-9-3] backward subsumption/strengthening limit 154200
c [elim-9-3-1] backward checking 111 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 7 and strengthened 16 clauses in 154201 steps
c [elim-9] incomplete 43 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 7597 = 16% variables out of 48445 scheduled
c [bca-10] limit of 10000000 steps and 551060 added (scaled 2)
c [bca-10] 64012 out of 81698 literals actually usable 78%
c [bca-10] added 163 blocked clauses in 158054 steps
c [sort-queue-14] sorted 17801 enqueued variables after 50847 conflicts
c [score-dist-14] active 23047 (56%), one 10127 (25%), zero 7674 (19%)
c [score-dist-14] max exp 858, different 762 (89%)
c [score-dist-14] median active exp 727, avg 663.2
c [simplification-14] removed 9221 variables 18.4% (40848 remain 19%)
c [simplification-14] removed 55588 irredundant clauses 16.8% (275149 remain 23%)
c [simplification-14] maximum reduction of 18% = max (18%, 17%)
c [simplification-14] large reduction 18% >= 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 62847 (soft 52847 + delta 10000)
c [simplification-14] new conflict limit 52847 (hard 62847)
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   85.4   40847   275149     51502    8604   3336 257079   19   174   33  11%     11   90   11    8  126%
c i   85.7   40845   275149     52216    9221   3364 257115   17   184   33   9%      7   99    8    8   98%
c i   85.7   40844   275149     52351    9340   3373 257117   17   183   33   9%      6   98    8    8   96%
c i   85.7   40841   275149     52469    9447   3373 257119   17   185   33   9%      6   99   10    8  122%
c 
c [simplification-15] limit 52847 conflicts (hard 62847) hit after 52847 conflicts
c [quatres-11] found 28849 quaternary clauses 72% in total
c [quatres-11-1] removed 11 duplicate quaternary clauses
c [quatres-11-2] added 5 single-self-subsuming ternary resolvents
c [quatres-11-2] added 44 quaternary resolvents
c [ternres-11] limit 11004565 with penalty 0 = 0 + 0
c [ternres-11] all 40841 free variables schedulable
c [ternres-11] 682 ternary resolvents (5 bin, 677 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 343892 penalty 4 = 4 + 0
c [card-5] found 754 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 343892 for elimination
c [card-5] 754 out of 754 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-37] removed 75 variables
c [simpleprobe-6] 5722 schedulable variables 14%
c [simpleprobe-6] limit 44018260 penalty 0 = 0 + 0
c [decomp-38] removed 779 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 779 variables, found 39832 hbrs, 503 units
c [unhide-15] limit 2200913 with penalty 0 = 0 + 0
c [unhide-15-16] 3 units, 34 failed, 24494 tauts, 0 hbrs, 5417 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 354 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 39969 variables 100%
c [block-5] limit of 13755706 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 132 blocked clauses
c [block-5] 132 < 1/100 * 263464 = 2634 considered unsuccessful
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 39969 variables 100%
c [elim-10] limit of 220091300 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 680 variables 2% in round 1 in 22554282 steps
c [elim-10-1] backward subsumption/strengthening limit 22554200
c [elim-10-1-1] backward checking 3372 touched variables 8%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 40 and strengthened 73 clauses in 843999 steps
c [elim-10-1] rescheduled 275 variables 1% by backward subsumption
c [elim-10-2] eliminated 30 variables 0% in round 2 in 387966 steps
c [elim-10-2] backward subsumption/strengthening limit 387900
c [elim-10-2-1] backward checking 255 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 27 and strengthened 19 clauses in 181097 steps
c [elim-10-2] rescheduled 78 variables 0% by backward subsumption
c [elim-10-3] eliminated 11 variables 0% in round 3 in 130305 steps
c [elim-10-3] backward subsumption/strengthening limit 130300
c [elim-10-3-1] backward checking 70 touched variables 0%
c [elim-10-3-1] fully completed backward checking in 1 rounds
c [elim-10-3] subsumed 4 and strengthened 5 clauses in 82032 steps
c [elim-10] incomplete 24 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 722 = 2% variables out of 39969 scheduled
c [bca-11] limit of 10000000 steps and 522515 added (scaled 2)
c [bca-11] 59251 out of 78496 literals actually usable 75%
c [bca-11] added 23 blocked clauses in 145659 steps
c [sweep-10] limit 1650684 penalty 1 = 1 + 0
c [sweep-10-1] 6223 pos 17.0% + 30316 neg 83.0% = 36539 sched 93.1% ret 2708
c [sweep-10-1] 1659284 steps 44 queries 4618.30 avg class size
c [sweep-10-1] 584 decisions 37 SAT calls 104.62 avg env size
c [sweep-10-1] 36128 variables remain 92% (3115 retained 8%)
c [decomp-39] removed 30 variables
c [sweep-10-1] removed 30 vars (0 failed, 6 eqs, 10 impls)
c [sweep-10] 30 < 1/1000 * 39247 = 39 considered unsuccessful
c [sweep-10] removed 30 vars in TOTAL (1 rounds, 43 queries)
c [sort-queue-15] sorted 16315 enqueued variables after 52847 conflicts
c [score-dist-15] active 22902 (58%), one 9616 (25%), zero 6699 (17%)
c [score-dist-15] max exp 887, different 792 (89%)
c [score-dist-15] median active exp 746, avg 626.2
c [simplification-15] removed 1624 variables 4.0% (39217 remain 18%)
c [simplification-15] removed 14407 irredundant clauses 5.2% (260742 remain 22%)
c [simplification-15] maximum reduction of 5% = max (4%, 5%)
c [simplification-15] large reduction 5% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 64847 (soft 54847 + delta 10000)
c [simplification-15] new conflict limit 54847 (hard 64847)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   89.2   39216   260742     52849    9537   3741 258848   16   180   32   9%      4   93   11    8  134%
c i   89.5   39215   260742     53230    9883   3762 258857   16   176   33   9%      3   89   10    8  116%
c i   89.5   39214   260742     53244    9893   3762 258860   16   175   33   9%      3   88   10    8  112%
c i   89.6   39212   260742     53580   10200   3769 258867   15   175   33   9%      2   87   11    9  129%
c i   89.9   39211   260742     54234   10769   3794 258889   15   169   33   9%      3   81   14    9  160%
c i   89.9   39210   260742     54245   10776   3794 258892   15   168   33   9%      3   80   13    9  157%
c i   90.0   39209   260742     54334   10861   3797 258892   15   168   33   9%      3   80   15    9  170%
c 
c [simplification-16] limit 54847 conflicts (hard 64847) hit after 54847 conflicts
c [quatres-12] found 27624 quaternary clauses 70% in total
c [quatres-12-2] added 5 single-self-subsuming ternary resolvents
c [quatres-12-2] added 20 quaternary resolvents
c [ternres-12] limit 11290444 with penalty 0 = 0 + 0
c [ternres-12] all 39208 free variables schedulable
c [ternres-12] 413 ternary resolvents (3 bin, 410 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-40] removed 13 variables
c [unhide-16] limit 2258088 with penalty 0 = 0 + 0
c [unhide-16-18] 8 units, 25 failed, 9307 tauts, 0 hbrs, 8263 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 297 transitive binary clauses
c [cce-5] limit of 14113055 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 51
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 50
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 49
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 48
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 47
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 46
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 45
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 44
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 43
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 42
c [cce-5-1] eliminated 3 clauses out of 3 (100%) of length 41
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 40
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 39
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 38
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 37
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 36
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 35
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 34
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 33
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 32
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 31
c [cce-5-1] eliminated 1 clauses out of 5 (20%) of length 30
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 29
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 28
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 27
c [cce-5-1] eliminated 1 clauses out of 4 (25%) of length 26
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 25
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 24
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 23
c [cce-5-1] eliminated 1 clauses out of 6 (17%) of length 22
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 21
c [cce-5-1] eliminated 1 clauses out of 4 (25%) of length 20
c [cce-5-1] eliminated 4 clauses out of 7 (57%) of length 19
c [cce-5-1] eliminated 2 clauses out of 6 (33%) of length 18
c [cce-5-1] eliminated 4 clauses out of 7 (57%) of length 17
c [cce-5-1] eliminated 2 clauses out of 7 (29%) of length 16
c [cce-5-1] eliminated 4 clauses out of 7 (57%) of length 15
c [cce-5-1] eliminated 2 clauses out of 7 (29%) of length 14
c [cce-5-1] eliminated 4 clauses out of 9 (44%) of length 13
c [cce-5-1] eliminated 2 clauses out of 7 (29%) of length 12
c [cce-5-1] eliminated 4 clauses out of 9 (44%) of length 11
c [cce-5-1] eliminated 2 clauses out of 6 (33%) of length 10
c [cce-5-1] eliminated 4 clauses out of 9 (44%) of length 9
c [cce-5-1] eliminated 2 clauses out of 11 (18%) of length 8
c [cce-5-1] eliminated 8 clauses out of 23 (35%) of length 7
c [cce-5-1] eliminated 18 clauses out of 941 (2%) of length 6
c [cce-5-1] eliminated 3 clauses out of 6069 (0%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 116 large clauses in 14113055 steps
c [cce-5-1] allowing another 7056527 steps for small clauses
c [cce-5-1] scheduling 206863 clauses = 129905 binary + 76958 ternary
c [cce-5-1] tried to eliminate 593 small clauses 0%
c [cce-5-1] eliminated 99 binary clauses 0%
c [cce-5-1] eliminated 49 ternary clauses 0%
c [cce-5-1] eliminated 148 small clauses 0%
c [cce-5-1] eliminated 213 small clauses in 14113059 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 329 covered clauses in round 1
c [cce-5] eliminated 329 covered clauses in TOTAL during 1 rounds
c [cce-5] 329 < 1/100 * 258002 = 2580 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 39171 variables 100%
c [elim-11] limit of 225808888 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 245 variables 1% in round 1 in 21600091 steps
c [elim-11-1] backward subsumption/strengthening limit 21600000
c [elim-11-1-1] backward checking 1668 touched variables 4%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 18 and strengthened 19 clauses in 477211 steps
c [elim-11-1] rescheduled 98 variables 0% by backward subsumption
c [elim-11-2] eliminated 7 variables 0% in round 2 in 53170 steps
c [elim-11-2] backward subsumption/strengthening limit 53100
c [elim-11-2-1] backward checking 167 touched variables 0%
c [elim-11-2-1] incomplete backward checking 52 remain 31%
c [elim-11-2] subsumed 0 and strengthened 0 clauses in 53136 steps
c [elim-11-2] fully rescheduled 38919 variables 99%
c [elim-11-3] eliminated 43 variables 0% in round 3 in 21545804 steps
c [elim-11-3] backward subsumption/strengthening limit 21545800
c [elim-11-3-1] backward checking 419 touched variables 1%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 4 and strengthened 8 clauses in 167895 steps
c [elim-11] incomplete 22 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 295 = 1% variables out of 39171 scheduled
c [elim-11] 295 < 1/100 * 39171 = 391 considered unsuccessful
c [bca-12] limit of 10000000 steps and 514455 added (scaled 2)
c [bca-12] 57188 out of 77754 literals actually usable 74%
c [bca-12] added 26 blocked clauses in 141019 steps
c [sort-queue-16] sorted 16336 enqueued variables after 54847 conflicts
c [score-dist-16] active 22540 (58%), one 9747 (25%), zero 6589 (17%)
c [score-dist-16] max exp 909, different 783 (86%)
c [score-dist-16] median active exp 721, avg 661.2
c [simplification-16] removed 332 variables 0.8% (38876 remain 18%)
c [simplification-16] removed 3942 irredundant clauses 1.5% (256800 remain 21%)
c [simplification-16] maximum reduction of 2% = max (1%, 2%)
c [simplification-16] geometric conflict interval increment 6888 = 20666 / 3
c [simplification-16] new conflict interval 27554
c [simplification-16] penalized conflict interval 27554 = 1 * 27554
c [simplification-16] hard conflict limit 96178 (soft 82401 + delta 13777)
c [simplification-16] new conflict limit 82401 (hard 96178)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   93.4   38875   256800     55269   11432   4068 248950   14   168   33   8%      5   79   12    9  142%
c i   93.7   38873   256800     55593   11721   4079 248957   14   166   33   8%      4   77   13    9  150%
c i   93.7   38871   256800     55595   11722   4079 248957   14   166   33   8%      4   77   13    9  150%
c i   94.1   38869   256800     56521   12532   4122 248991   14   162   33   9%      5   71   14    9  166%
c i   94.1   38863   256800     56527   12536   4123 248991   14   161   33   9%      5   71   14    9  162%
c i   94.2   38862   256800     56687   12680   4127 248996   14   161   33   9%      4   71   14    9  155%
c i   94.6   38861   256800     57232   13161   4158 249020   14   160   33   9%      3   69   14    9  162%
c i   94.8   38836   256800     57721   13611   4177 249029   14   159   34   9%      3   67   16    9  179%
c i   95.2   38834   256800     58318   14149   4197 249052   14   157   34   9%      3   64   13    9  147%
c i   95.6   38829   256800     59050   14779   4238 249083   14   157   34   9%      4   64   14    9  158%
c i   95.8   38826   256800     59390   15088   4251 249089   14   158   34   9%      3   64   15    9  173%
c i   95.9   38800   256800     59740   15404   4266 249097   14   153   34   9%      2   59   14    9  158%
c i   96.2   38799   256800     60361   15969   4282 249110   14   151   34   9%      3   57   15    9  162%
c i   96.3   38797   256800     60526   16123   4287 249114   14   150   34   9%      2   56   14    9  154%
c i   96.3   38795   256800     60528   16124   4287 249114   14   150   34  10%      2   55   14    9  155%
c i   96.8   38794   256800     61559   17055   4321 249145   15   146   35  10%      5   51   17    9  186%
c i   96.9   38791   256800     61704   17168   4328 249155   15   147   35  10%      4   52   15    9  166%
c i   97.1   38790   256800     62249   17675   4340 249170   14   143   35  10%      3   47   14    9  155%
c i   97.4   38789   256800     62748   18130   4356 249186   15   146   35  10%      3   49   18    9  195%
c i   97.4   38781   256800     62749   18130   4356 249186   15   146   35  10%      3   49   18    9  194%
c i   97.5   38773   256800     62830   18203   4356 249189   15   146   35  10%      2   49   19    9  200%
c i   97.8   38755   256800     63379   18701   4378 249203   16   146   35  11%      2   49   20    9  215%
c i   99.1   38753   256800     65640   20764   4440 249256   17   149   36  11%     19   51   17   10  176%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   99.3   38752   256800     66015   21103   4454 249265   17   149   36  11%     13   50   17   10  173%
c i   99.5   38751   256800     66332   21390   4467 249275   17   148   36  11%     10   49   15   10  151%
c i   99.5   38750   256800     66375   21425   4471 249277   17   149   36  11%      9   50   15   10  155%
c i  100.0   38749   256800     67106   22078   4494 249302   17   151   36  11%      6   51   15   10  152%
c i  100.4   38734   256800     67862   22738   4525 249334   17   149   37  11%      5   49   19   10  187%
c i  100.5   38733   256800     67956   22823   4528 249336   17   151   37  11%      4   50   18   10  180%
c i  100.6   38732   256800     68036   22893   4531 249337   17   150   37  11%      4   50   17   10  176%
c i  101.0   38730   256800     68581   23378   4556 249356   17   153   37  11%      3   52   18   10  177%
c i  101.2   38726   256800     68991   23758   4560 249365   18   152   37  12%      2   51   26   10  254%
c i  101.2   38724   256800     69088   23845   4566 249365   18   151   37  12%      2   50   23   10  229%
c i  101.8   38564   256800     70024   24683   4611 249397   18   152   38  12%      4   50   24   10  233%
c i  102.2   38562   256800     70680   25269   4631 249417   19   149   38  13%      3   46   31   10  297%
c i  102.8   38560   256800     71550   26058   4657 249440   20   150   39  13%      4   47   21   11  199%
c i  103.0   38557   256800     71793   26277   4665 249449   19   153   39  13%      3   50   19   11  181%
c i  103.8   38554   256800     73052   27457   4691 249481   19   153   39  13%      7   49   22   11  202%
c i  104.2   38540   256800     73885   28203   4723 249508   19   150   39  13%      5   45   19   11  173%
c i  104.5   38536   256800     74247   28516   4733 249513   20   148   39  13%      4   43   22   11  200%
c i  104.5   38518   256800     74248   28516   4733 249513   20   148   39  13%      4   43   22   11  199%
c i  105.0   38360   256800     75007   29203   4765 249527   19   151   39  13%      3   45   18   11  162%
c i  105.5   38353   256800     75827   29955   4788 249545   20   152   39  13%      4   46   22   11  202%
c i  105.8   38352   256800     76302   30369   4810 249559   20   153   39  13%      3   47   21   11  192%
c i  105.8   38326   256800     76384   30442   4810 249564   20   152   39  13%      2   46   21   11  186%
c i  106.2   38323   256800     76860   30886   4830 249574   20   155   40  13%      2   48   20   11  178%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  106.7   38315   256800     77553   31521   4854 249582   20   160   41  12%      2   52   19   11  170%
c i  106.8   38314   256800     77767   31716   4859 249586   20   159   41  12%      1   52   19   11  167%
c i  106.9   38313   256800     77911   31851   4864 249588   20   160   41  12%      1   53   18   11  157%
c i  107.3   38312   256800     78687   32549   4892 249606   21   158   41  13%      2   50   29   12  252%
c i  107.4   38310   256800     78815   32666   4895 249608   21   157   41  13%      2   48   25   12  216%
c i  107.4   38282   256800     78842   32690   4896 249608   21   156   41  13%      2   48   24   12  212%
c i  107.7   38281   256800     79220   33046   4906 249613   21   159   41  13%      1   50   21   12  179%
c i  108.0   38280   256800     79810   33587   4916 249626   22   157   41  14%      1   48   29   12  246%
c i  108.0   38279   256800     79834   33606   4917 249628   22   158   41  14%      1   49   28   12  235%
c i  109.0   38275   256800     81819   35406   4962 249667   23   165   43  14%     14   55   22   12  179%
c i  109.2   38271   256800     82101   35653   4974 249674   23   164   43  14%     11   54   24   12  196%
c 
c [simplification-17] limit 82432 conflicts (hard 96178) hit after 82433 conflicts
c [quatres-13] found 27509 quaternary clauses 65% in total
c [quatres-13-1] removed 1 duplicate quaternary clauses
c [quatres-13-2] added 4 single-self-subsuming ternary resolvents
c [quatres-13-2] added 9 quaternary resolvents
c [ternres-13] limit 15491619 with penalty 0 = 0 + 0
c [ternres-13] all 38271 free variables schedulable
c [ternres-13] 292 ternary resolvents (2 bin, 290 trn)
c [ternres-13] fully completed ternary resolution
c [gauss-7] limit 387290 penalty 3 = 3 + 0
c [gauss-7] extracted 14 xors of average arity 2.8
c [gauss-7] connected 39 occurrences of 36 variables (average 1.1)
c [gauss-7] limit 387290 penalty 3 = 3 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-41] removed 67 variables
c [treelook-6] limit 774580 penalty 1 = 1 + 0 boost 1
c [treelook-6] scheduled 54681 literals 72%
c [treelook-6] scheduling used 801181 steps
c [treelook-6] not fully scheduled
c [treelook-6] limit 774580 penalty 1 = 1 + 0 boost 1
c [treelook-6] used 808668 steps
c [treelook-6] 54429 literals remain 71%
c [treelook-6] 8687 variables remain to probed next time 23%
c [treelook-6] removed 91 variables, found 2802 hbrs
c [unhide-17] limit 3098323 with penalty 0 = 0 + 0
c [unhide-17-20] 7 units, 59 failed, 8122 tauts, 0 hbrs, 113626 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 318 transitive binary clauses
c [bca-13] limit of 10000000 steps and 487512 added (scaled 2)
c [bca-13] 45320 out of 76038 literals actually usable 60%
c [bca-13] added 17 blocked clauses in 137447 steps
c [sort-queue-17] sorted 18186 enqueued variables after 82433 conflicts
c [score-dist-17] active 19832 (52%), one 12366 (33%), zero 5820 (15%)
c [score-dist-17] max exp 635, different 562 (88%)
c [score-dist-17] median active exp 511, avg 465.2
c [simplification-17] removed 253 variables 0.7% (38018 remain 18%)
c [simplification-17] removed 13478 irredundant clauses 5.2% (243322 remain 20%)
c [simplification-17] maximum reduction of 5% = max (1%, 5%)
c [simplification-17] large reduction 5% >= 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 94433 (soft 84433 + delta 10000)
c [simplification-17] new conflict limit 84433 (hard 94433)
c 
c [simplification-18] limit 84433 conflicts (hard 94433) hit after 84433 conflicts
c [quatres-14] found 27574 quaternary clauses 64% in total
c [quatres-14-1] removed 3 duplicate quaternary clauses
c [quatres-14-2] added 2 single-self-subsuming ternary resolvents
c [ternres-14] limit 15717514 with penalty 0 = 0 + 0
c [ternres-14] all 38018 free variables schedulable
c [ternres-14] 114 ternary resolvents (1 bin, 113 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-43] removed 40 variables
c [basicprobe-6] limit 78587574 penalty 0 = 0 + 0
c [basicprobe-6-0] 3417 probes remain 9% after last round
c [basicprobe-6-0] 838 units = 801 failed (96%) + 37 lifted (4%)
c [basicprobe-6-0] removed 1093 variables, found 227000 hbrs
c [bate-4] eliminated 511 asymmetric tautologies during probing
c [unhide-18] limit 3143502 with penalty 0 = 0 + 0
c [unhide-18-22] 1 units, 52 failed, 29090 tauts, 0 hbrs, 61390 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 210 transitive binary clauses
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 36831 variables 100%
c [elim-12] limit of 157175149 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 993 variables 3% in round 1 in 18679545 steps
c [elim-12-1] backward subsumption/strengthening limit 18679500
c [elim-12-1-1] backward checking 5180 touched variables 14%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 45 and strengthened 134 clauses in 1142480 steps
c [elim-12-1] rescheduled 481 variables 1% by backward subsumption
c [elim-12-2] eliminated 40 variables 0% in round 2 in 292278 steps
c [elim-12-2] backward subsumption/strengthening limit 292200
c [elim-12-2-1] backward checking 373 touched variables 1%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 15 and strengthened 22 clauses in 171585 steps
c [elim-12-2] rescheduled 94 variables 0% by backward subsumption
c [elim-12-3] eliminated 6 variables 0% in round 3 in 212837 steps
c [elim-12-3] backward subsumption/strengthening limit 212800
c [elim-12-3-1] backward checking 67 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 3 and strengthened 10 clauses in 116209 steps
c [elim-12] incomplete 39 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 1042 = 3% variables out of 36831 scheduled
c [bca-14] limit of 10000000 steps and 456384 added (scaled 2)
c [bca-14] 42939 out of 71580 literals actually usable 60%
c [bca-14] added 22 blocked clauses in 126232 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 11788135 penalty 2 = 2 + 0
c [sweep-11-1] 6017 pos 18.1% + 27211 neg 81.9% = 33228 sched 92.8% ret 2561
c [sweep-11-1] 11810238 steps 318 queries 688.24 avg class size
c [sweep-11-1] 6533 decisions 298 SAT calls 119.27 avg env size
c [sweep-11-1] 25699 variables remain 72% (10075 retained 28%)
c [decomp-44] removed 134 variables
c [sweep-11-1] removed 134 vars (0 failed, 21 eqs, 45 impls)
c [sweep-11] removed 134 vars in TOTAL (1 rounds, 317 queries)
c [sort-queue-18] sorted 15593 enqueued variables after 84433 conflicts
c [score-dist-18] active 20062 (56%), one 10726 (30%), zero 4867 (14%)
c [score-dist-18] max exp 699, different 622 (89%)
c [score-dist-18] median active exp 600, avg 545.7
c [simplification-18] removed 2363 variables 6.2% (35655 remain 17%)
c [simplification-18] removed 15899 irredundant clauses 6.5% (227423 remain 19%)
c [simplification-18] maximum reduction of 7% = max (6%, 7%)
c [simplification-18] large reduction 7% >= 5% limit
c [simplification-18] next conflict interval 2000 = 2000/1
c [simplification-18] penalized conflict interval 2000 = 1 * 2000
c [simplification-18] hard conflict limit 96433 (soft 86433 + delta 10000)
c [simplification-18] new conflict limit 86433 (hard 96433)
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  120.2   35654   227423     84945   31214   4772 373142   26   174   44  15%     26   61   22   13  167%
c 
c [simplification-19] limit 86433 conflicts (hard 96433) hit after 86433 conflicts
c [quatres-15] found 24968 quaternary clauses 63% in total
c [quatres-15-1] removed 3 duplicate quaternary clauses
c [quatres-15-2] added 3 single-self-subsuming ternary resolvents
c [quatres-15-2] added 17 quaternary resolvents
c [ternres-15] limit 15923367 with penalty 0 = 0 + 0
c [ternres-15] all 35653 free variables schedulable
c [ternres-15] 496 ternary resolvents (1 bin, 495 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-45] removed 5 variables
c [simpleprobe-7] all 35650 free variables schedulable
c [simpleprobe-7] limit 63693469 penalty 0 = 0 + 0
c [decomp-46] removed 155 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 155 variables, found 41358 hbrs, 107 units
c [unhide-19] limit 3184673 with penalty 0 = 0 + 0
c [unhide-19-24] 1 units, 11 failed, 28835 tauts, 0 hbrs, 35652 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 281 transitive binary clauses
c [cce-6] limit of 9952104 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 23
c [cce-6-1] eliminated 1 clauses out of 5 (20%) of length 22
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 21
c [cce-6-1] eliminated 1 clauses out of 6 (17%) of length 20
c [cce-6-1] eliminated 2 clauses out of 6 (33%) of length 19
c [cce-6-1] eliminated 1 clauses out of 6 (17%) of length 18
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 17
c [cce-6-1] eliminated 2 clauses out of 7 (29%) of length 16
c [cce-6-1] eliminated 4 clauses out of 8 (50%) of length 15
c [cce-6-1] eliminated 2 clauses out of 6 (33%) of length 14
c [cce-6-1] eliminated 4 clauses out of 10 (40%) of length 13
c [cce-6-1] eliminated 2 clauses out of 8 (25%) of length 12
c [cce-6-1] eliminated 5 clauses out of 12 (42%) of length 11
c [cce-6-1] eliminated 3 clauses out of 7 (43%) of length 10
c [cce-6-1] eliminated 6 clauses out of 12 (50%) of length 9
c [cce-6-1] eliminated 4 clauses out of 19 (21%) of length 8
c [cce-6-1] eliminated 6 clauses out of 24 (25%) of length 7
c [cce-6-1] eliminated 15 clauses out of 878 (2%) of length 6
c [cce-6-1] eliminated 18 clauses out of 5716 (0%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 83 large clauses in 9952104 steps
c [cce-6-1] allowing another 4976052 steps for small clauses
c [cce-6-1] scheduling 179009 clauses = 117039 binary + 61970 ternary
c [cce-6-1] tried to eliminate 536 small clauses 0%
c [cce-6-1] eliminated 84 binary clauses 0%
c [cce-6-1] eliminated 23 ternary clauses 0%
c [cce-6-1] eliminated 107 small clauses 0%
c [cce-6-1] eliminated 160 small clauses in 9952116 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 243 covered clauses in round 1
c [cce-6] eliminated 243 covered clauses in TOTAL during 1 rounds
c [cce-6] 243 < 1/100 * 224375 = 2243 considered unsuccessful
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 35485 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 292 variables 1% in round 1 in 18270156 steps
c [elim-13-1] backward subsumption/strengthening limit 18270100
c [elim-13-1-1] backward checking 1915 touched variables 5%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 14 and strengthened 29 clauses in 587541 steps
c [elim-13-1] rescheduled 105 variables 0% by backward subsumption
c [elim-13-2] eliminated 7 variables 0% in round 2 in 143097 steps
c [elim-13-2] backward subsumption/strengthening limit 143000
c [elim-13-2-1] backward checking 91 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 4 and strengthened 3 clauses in 78393 steps
c [elim-13-2] rescheduled 20 variables 0% by backward subsumption
c [elim-13-3] eliminated 2 variables 0% in round 3 in 19419 steps
c [elim-13-3] backward subsumption/strengthening limit 19400
c [elim-13-3-1] backward checking 38 touched variables 0%
c [elim-13-3-1] incomplete backward checking 0 remain 0%
c [elim-13-3] subsumed 2 and strengthened 0 clauses in 19401 steps
c [elim-13] incomplete 5 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 301 = 1% variables out of 35485 scheduled
c [elim-13] 301 < 1/100 * 35485 = 354 considered unsuccessful
c [bca-15] limit of 10000000 steps and 447015 added (scaled 2)
c [bca-15] 41652 out of 70370 literals actually usable 59%
c [bca-15] added 14 blocked clauses in 123848 steps
c [sort-queue-19] sorted 14611 enqueued variables after 86433 conflicts
c [score-dist-19] active 20573 (58%), one 9968 (28%), zero 4643 (13%)
c [score-dist-19] max exp 725, different 690 (95%)
c [score-dist-19] median active exp 622, avg 534.6
c [simplification-19] removed 469 variables 1.3% (35184 remain 16%)
c [simplification-19] removed 4359 irredundant clauses 1.9% (223064 remain 19%)
c [simplification-19] maximum reduction of 2% = max (1%, 2%)
c [simplification-19] geometric conflict interval increment 9184 = 27554 / 3
c [simplification-19] new conflict interval 36738
c [simplification-19] penalized conflict interval 36738 = 1 * 36738
c [simplification-19] hard conflict limit 141540 (soft 123171 + delta 18369)
c [simplification-19] new conflict limit 123171 (hard 141540)
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  126.1   35183   223064     89806   34389   5139 372737   23   160   43  15%     54   43   28   14  205%
c i  126.3   35182   223064     90447   34975   5153 372748   23   157   43  15%     28   40   23   14  169%
c i  128.5   35181   223064     95746   39830   5260 372831   25   151   44  16%     58   31   28   15  189%
c i  129.0   35179   223064     96947   40918   5291 372850   25   152   44  16%     19   31   23   15  154%
c i  131.7   35178   223064    102760   46229   5422 372919   25   160   48  16%     63   36   21   16  136%
c i  131.8   35177   223064    102970   46405   5427 372927   25   158   48  16%     49   34   20   16  130%
c i  132.0   35145   223064    103559   46948   5443 372931   26   161   48  16%     24   36   35   16  224%
c i  132.0   34946   223064    103578   46964   5443 372932   26   160   48  16%     24   36   33   16  210%
c i  132.2   34768   223064    104006   47354   5453 372938   26   163   48  16%     13   39   25   16  157%
c i  132.7   34764   223064    104850   48130   5472 372947   27   166   50  16%      3   41   33   16  206%
c i  133.4   34763   223064    106362   49515   5489 372960   27   160   50  17%      2   34   31   16  190%
c i  133.7   34731   223064    106953   50058   5503 372965   28   161   50  17%     -2   35   30   16  183%
c i  133.7   34730   223064    106972   50075   5503 372965   28   161   50  17%     -2   35   29   16  177%
c i  134.6   34729   223064    109165   52085   5543 372984   28   158   51  18%      9   30   30   17  175%
c i  137.1   34728   223064    114725   57059   5644 373073   30   145   55  20%     57   16   23   18  125%
c i  137.2   34699   223064    115188   57494   5646 373074   28   165   55  17%     32   36   21   18  116%
c i  137.8   34683   223064    116138   58383   5667 373088   29   167   55  17%      9   37   28   18  153%
c -  141.0   34664   223064    122663   25669   5769 373150   31   163   36  19%     69   30   32   19  163%
c 
c [simplification-20] limit 123171 conflicts (hard 141540) hit after 123171 conflicts
c [quatres-16] found 24675 quaternary clauses 61% in total
c [quatres-16-1] removed 1 duplicate quaternary clauses
c [quatres-16-2] added 4 single-self-subsuming ternary resolvents
c [quatres-16-2] added 9 quaternary resolvents
c [ternres-16] limit 19678908 with penalty 0 = 0 + 0
c [ternres-16] all 34664 free variables schedulable
c [ternres-16] 341 ternary resolvents (0 bin, 341 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-47] removed 526 variables
c [treelook-7] limit 1967890 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 50426 literals 73%
c [treelook-7] scheduling used 934192 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 1967890 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 1972026 steps
c [treelook-7] 50175 literals remain 72%
c [treelook-7] 7508 variables remain to probed next time 22%
c [decomp-48] removed 10 variables
c [treelook-7] removed 34 variables, found 9459 hbrs
c [unhide-20] limit 3935781 with penalty 0 = 0 + 0
c [unhide-20-26] 1 units, 34 failed, 15274 tauts, 0 hbrs, 29918 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 254 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 34582 variables 100%
c [block-6] limit of 12299317 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 38 blocked clauses
c [block-6] 38 < 1/100 * 214345 = 2143 considered unsuccessful
c [bca-16] limit of 10000000 steps and 429490 added (scaled 2)
c [bca-16] 42697 out of 69164 literals actually usable 62%
c [bca-16] added 7 blocked clauses in 119980 steps
c [sweep-12] limit 2951836 penalty 1 = 1 + 0
c [sweep-12-1] 4456 pos 17.9% + 20407 neg 82.1% = 24863 sched 71.9% ret 9718
c [sweep-12-1] 2976507 steps 85 queries 1460.92 avg class size
c [sweep-12-1] 1409 decisions 75 SAT calls 114.60 avg env size
c [sweep-12-1] 24107 variables remain 70% (10469 retained 30%)
c [decomp-49] removed 74 variables
c [sweep-12-1] removed 74 vars (0 failed, 10 eqs, 16 impls)
c [sweep-12] removed 74 vars in TOTAL (1 rounds, 84 queries)
c [sort-queue-20] sorted 13354 enqueued variables after 123171 conflicts
c [score-dist-20] active 21153 (61%), one 9350 (27%), zero 4004 (12%)
c [score-dist-20] max exp 859, different 767 (89%)
c [score-dist-20] median active exp 745, avg 654.1
c [simplification-20] removed 157 variables 0.5% (34507 remain 16%)
c [simplification-20] removed 8891 irredundant clauses 4.0% (214173 remain 18%)
c [simplification-20] maximum reduction of 4% = max (0%, 4%)
c [simplification-20] geometric conflict interval increment 7347 = 36738 / 5
c [simplification-20] new conflict interval 44085
c [simplification-20] penalized conflict interval 44085 = 1 * 44085
c [simplification-20] hard conflict limit 189298 (soft 167256 + delta 22042)
c [simplification-20] new conflict limit 167256 (hard 189298)
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  144.0   34506   214173    124798   27199   6051 367996   28   151   38  19%     99   17   30   20  152%
c i  145.4   34505   214173    128854   30969   6099 368037   26   170   40  15%     28   35   22   20  112%
c i  145.8   34496   214173    129976   31997   6109 368047   27   161   40  17%      2   26   28   20  141%
c i  146.7   34495   214173    132780   34521   6150 368057   25   138   42  18%      8    2   22   20  111%
c i  146.8   34494   214173    133145   34855   6153 368057   25   140   43  18%      0    4   28   20  138%
c i  149.2   34464   214173    138615   39920   6241 368110   30   145   46  21%     47    8   35   21  168%
c i  150.0   34462   214173    140643   41751   6281 368136   29   154   47  19%      4   17   28   21  130%
c i  150.4   34461   214173    141706   42733   6291 368148   29   170   48  17%     -7   33   27   21  126%
c i  153.8   34460   214173    150600   50897   6397 368222   27   168   54  16%     95   28   32   22  148%
c i  156.2   34459   214173    157075   56685   6476 368281   28   132   54  21%     55   -9   34   23  150%
c i  157.4   34452   214173    159814   59244   6505 368303   30   144   59  21%      3    3   43   23  189%
c i  157.5   34450   214173    159980   59391   6506 368304   31   146   59  21%     -2    4   42   23  183%
c i  158.8   34449   214173    162993   62157   6542 368319   30   143   61  21%      3    2   24   23  104%
c 
c [simplification-21] limit 167256 conflicts (hard 189298) hit after 167257 conflicts
c [quatres-17] found 24974 quaternary clauses 57% in total
c [quatres-17-1] removed 2 duplicate quaternary clauses
c [quatres-17-2] added 5 single-self-subsuming ternary resolvents
c [quatres-17-2] added 4 quaternary resolvents
c [ternres-17] limit 23358178 with penalty 0 = 0 + 0
c [ternres-17] all 34448 free variables schedulable
c [ternres-17] 90 ternary resolvents (0 bin, 90 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 729943 penalty 4 = 4 + 0
c [card-6] found 1139 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 729943 for elimination
c [card-6] 1139 out of 1139 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-50] removed 155 variables
c [basicprobe-7] limit 116790894 penalty 0 = 0 + 0
c [basicprobe-7-0] 4263 sched 13%, 433 failed, 8 lifted, 109260 hbrs
c [decomp-51] removed 657 variables
c [basicprobe-7-1] 5214 probes remain 16% after last round
c [basicprobe-7-1] 525 units = 517 failed (98%) + 8 lifted (2%)
c [basicprobe-7-1] removed 842 variables, found 160631 hbrs
c [bate-5] eliminated 286 asymmetric tautologies during probing
c [unhide-21] limit 2335817 with penalty 1 = 0 + 1
c [unhide-21-28] 1 units, 3 failed, 31613 tauts, 0 hbrs, 473369 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 175 transitive binary clauses
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 33508 variables 100%
c [elim-14] limit of 233581788 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 840 variables 3% in round 1 in 16968017 steps
c [elim-14-1] backward subsumption/strengthening limit 16968000
c [elim-14-1-1] backward checking 4240 touched variables 13%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 21 and strengthened 60 clauses in 973641 steps
c [elim-14-1] rescheduled 231 variables 1% by backward subsumption
c [elim-14-2] eliminated 13 variables 0% in round 2 in 260981 steps
c [elim-14-2] backward subsumption/strengthening limit 260900
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 12 and strengthened 8 clauses in 157698 steps
c [elim-14-2] rescheduled 38 variables 0% by backward subsumption
c [elim-14-3] eliminated 4 variables 0% in round 3 in 56367 steps
c [elim-14-3] backward subsumption/strengthening limit 56300
c [elim-14-3-1] backward checking 48 touched variables 0%
c [elim-14-3-1] incomplete backward checking 0 remain 0%
c [elim-14-3] subsumed 0 and strengthened 4 clauses in 56301 steps
c [elim-14] incomplete 16 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 857 = 3% variables out of 33508 scheduled
c [bca-17] limit of 10000000 steps and 405276 added (scaled 2)
c [bca-17] 33833 out of 65304 literals actually usable 52%
c [bca-17] added 7 blocked clauses in 131321 steps
c [sweep-13] limit 7007453 penalty 0 = 0 + 0
c [sweep-13-1] 4648 pos 20.3% + 18288 neg 79.7% = 22936 sched 70.2% ret 9715
c [sweep-13-1] 7013083 steps 181 queries 1139.34 avg class size
c [sweep-13-1] 5081 decisions 166 SAT calls 146.43 avg env size
c [sweep-13-1] 20352 variables remain 62% (12298 retained 38%)
c [decomp-52] removed 40 variables
c [sweep-13-1] removed 40 vars (0 failed, 14 eqs, 25 impls)
c [sweep-13] removed 40 vars in TOTAL (1 rounds, 180 queries)
c [sort-queue-21] sorted 14007 enqueued variables after 167257 conflicts
c [score-dist-21] active 18604 (57%), one 10862 (33%), zero 3145 (10%)
c [score-dist-21] max exp 953, different 789 (83%)
c [score-dist-21] median active exp 771, avg 642.7
c [simplification-21] removed 1837 variables 5.3% (32611 remain 15%)
c [simplification-21] removed 12051 irredundant clauses 5.6% (202122 remain 17%)
c [simplification-21] maximum reduction of 6% = max (5%, 6%)
c [simplification-21] large reduction 6% >= 5% limit
c [simplification-21] next conflict interval 2000 = 2000/1
c [simplification-21] penalized conflict interval 2000 = 1 * 2000
c [simplification-21] hard conflict limit 179257 (soft 169257 + delta 10000)
c [simplification-21] new conflict limit 169257 (hard 179257)
c 
c [simplification-22] limit 169257 conflicts (hard 179257) hit after 169258 conflicts
c [quatres-18] found 23804 quaternary clauses 56% in total
c [quatres-18-1] removed 4 duplicate quaternary clauses
c [quatres-18-2] added 1 single-self-subsuming ternary resolvents
c [quatres-18-2] added 20 quaternary resolvents
c [ternres-18] limit 23511283 with penalty 0 = 0 + 0
c [ternres-18] all 32611 free variables schedulable
c [ternres-18] 298 ternary resolvents (0 bin, 298 trn)
c [ternres-18] fully completed ternary resolution
c [gauss-8] limit 293891 penalty 4 = 4 + 0
c [gauss-8] extracted 7 xors of average arity 3.0
c [gauss-8] connected 21 occurrences of 21 variables (average 1.0)
c [gauss-8] limit 293891 penalty 4 = 4 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-8] all 32611 free variables schedulable
c [simpleprobe-8] limit 94045135 penalty 0 = 0 + 0
c [decomp-54] removed 56 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 56 variables, found 36280 hbrs, 11 units
c [unhide-22] limit 4702256 with penalty 0 = 0 + 0
c [unhide-22-30] 2 units, 1 failed, 30945 tauts, 0 hbrs, 192990 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 222 transitive binary clauses
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 32546 variables 100%
c [elim-15] limit of 470225678 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 132 variables 0% in round 1 in 16834475 steps
c [elim-15-1] backward subsumption/strengthening limit 16834400
c [elim-15-1-1] backward checking 1041 touched variables 3%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 9 and strengthened 13 clauses in 323411 steps
c [elim-15-1] rescheduled 57 variables 0% by backward subsumption
c [elim-15-2] eliminated 4 variables 0% in round 2 in 91763 steps
c [elim-15-2] backward subsumption/strengthening limit 91700
c [elim-15-2-1] backward checking 41 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 2 and strengthened 7 clauses in 59730 steps
c [elim-15-2] rescheduled 22 variables 0% by backward subsumption
c [elim-15-3] eliminated 4 variables 0% in round 3 in 33916 steps
c [elim-15-3] backward subsumption/strengthening limit 33900
c [elim-15-3-1] backward checking 37 touched variables 0%
c [elim-15-3-1] incomplete backward checking 0 remain 0%
c [elim-15-3] subsumed 1 and strengthened 4 clauses in 33901 steps
c [elim-15] incomplete 18 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 140 = 0% variables out of 32546 scheduled
c [elim-15] 140 < 1/100 * 32546 = 325 considered unsuccessful
c [bca-18] limit of 10000000 steps and 402143 added (scaled 2)
c [bca-18] 33673 out of 64814 literals actually usable 52%
c [bca-18] added 7 blocked clauses in 127735 steps
c [sweep-14] limit 7053385 penalty 0 = 0 + 0
c [sweep-14-1] 4191 pos 20.8% + 15989 neg 79.2% = 20180 sched 62.3% ret 12226
c [sweep-14-1] 7066709 steps 199 queries 742.16 avg class size
c [sweep-14-1] 4679 decisions 185 SAT calls 123.37 avg env size
c [sweep-14-1] 17794 variables remain 55% (14491 retained 45%)
c [decomp-55] removed 152 variables
c [sweep-14-1] removed 152 vars (0 failed, 13 eqs, 23 impls)
c [sweep-14] removed 152 vars in TOTAL (1 rounds, 198 queries)
c [sort-queue-22] sorted 15757 enqueued variables after 169258 conflicts
c [score-dist-22] active 16497 (51%), one 12772 (40%), zero 2985 (9%)
c [score-dist-22] max exp 506, different 481 (95%)
c [score-dist-22] median active exp 419, avg 365.5
c [simplification-22] removed 357 variables 1.1% (32254 remain 15%)
c [simplification-22] removed 2727 irredundant clauses 1.3% (199395 remain 17%)
c [simplification-22] maximum reduction of 1% = max (1%, 1%)
c [simplification-22] geometric conflict interval increment 22042 = 44085 / 2
c [simplification-22] new conflict interval 66127
c [simplification-22] penalized conflict interval 66127 = 1 * 66127
c [simplification-22] hard conflict limit 268448 (soft 235385 + delta 33063)
c [simplification-22] new conflict limit 235385 (hard 268448)
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 -  181.2   32254   199395    182684   33641   6255 410151   24   149   38  16%    231    5   24   24  101%
c i  183.0   32253   199395    189237   39627   6303 410180   24   140   45  17%    306   -3   28   24  116%
c i  187.0   32250   199395    201990   51137   6424 410234   24   134   52  18%     90   -9   18   24   75%
c i  191.8   32053   199395    216713   64433   6584 410313   25   132   60  19%    116  -10   28   24  115%
c -  194.1   32022   199395    222852   38833   6633 410334   28   143   39  20%    -15    1   36   24  147%
c 
c [simplification-23] limit 235385 conflicts (hard 268448) hit after 235385 conflicts
c [quatres-19] found 23915 quaternary clauses 53% in total
c [quatres-19-1] removed 2 duplicate quaternary clauses
c [quatres-19-2] added 4 single-self-subsuming ternary resolvents
c [quatres-19-2] added 8 quaternary resolvents
c [ternres-19] limit 28018973 with penalty 0 = 0 + 0
c [ternres-19] all 32022 free variables schedulable
c [ternres-19] 148 ternary resolvents (1 bin, 147 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-56] removed 233 variables
c [treelook-8] limit 2801897 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 46219 literals 72%
c [treelook-8] scheduling used 938785 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 2801897 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 2848889 steps
c [treelook-8] 46114 literals remain 72%
c [treelook-8] 6640 variables remain to probed next time 21%
c [decomp-57] removed 2 variables
c [treelook-8] removed 3 variables, found 11267 hbrs
c [unhide-23] limit 5603794 with penalty 0 = 0 + 0
c [unhide-23-33] 0 units, 6 failed, 17188 tauts, 0 hbrs, 254284 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 136 transitive binary clauses
c [cce-7] limit of 8755929 steps penalty 4 = 4 + 0
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 53
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 52
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 51
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 50
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 33
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 32
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 31
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 30
c [cce-7-1] eliminated 5 clauses out of 8 (62%) of length 29
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 28
c [cce-7-1] eliminated 4 clauses out of 5 (80%) of length 27
c [cce-7-1] eliminated 5 clauses out of 9 (56%) of length 26
c [cce-7-1] eliminated 5 clauses out of 9 (56%) of length 25
c [cce-7-1] eliminated 6 clauses out of 10 (60%) of length 24
c [cce-7-1] eliminated 5 clauses out of 8 (62%) of length 23
c [cce-7-1] eliminated 7 clauses out of 11 (64%) of length 22
c [cce-7-1] eliminated 5 clauses out of 8 (62%) of length 21
c [cce-7-1] eliminated 8 clauses out of 13 (62%) of length 20
c [cce-7-1] eliminated 5 clauses out of 10 (50%) of length 19
c [cce-7-1] eliminated 8 clauses out of 16 (50%) of length 18
c [cce-7-1] eliminated 5 clauses out of 11 (45%) of length 17
c [cce-7-1] eliminated 8 clauses out of 13 (62%) of length 16
c [cce-7-1] eliminated 7 clauses out of 12 (58%) of length 15
c [cce-7-1] eliminated 8 clauses out of 15 (53%) of length 14
c [cce-7-1] eliminated 8 clauses out of 17 (47%) of length 13
c [cce-7-1] eliminated 11 clauses out of 18 (61%) of length 12
c [cce-7-1] eliminated 11 clauses out of 22 (50%) of length 11
c [cce-7-1] eliminated 15 clauses out of 24 (62%) of length 10
c [cce-7-1] eliminated 12 clauses out of 29 (41%) of length 9
c [cce-7-1] eliminated 18 clauses out of 34 (53%) of length 8
c [cce-7-1] eliminated 14 clauses out of 38 (37%) of length 7
c [cce-7-1] eliminated 18 clauses out of 854 (2%) of length 6
c [cce-7-1] eliminated 6 clauses out of 5617 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 223 large clauses in 8755933 steps
c [cce-7-1] allowing another 4377966 steps for small clauses
c [cce-7-1] scheduling 119480 clauses = 104617 binary + 14863 ternary
c [cce-7-1] tried to eliminate 784 small clauses 1%
c [cce-7-1] eliminated 186 binary clauses 0%
c [cce-7-1] eliminated 49 ternary clauses 0%
c [cce-7-1] eliminated 235 small clauses 0%
c [cce-7-1] eliminated 235 small clauses in 8755929 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 458 covered clauses in round 1
c [cce-7] eliminated 458 covered clauses in TOTAL during 1 rounds
c [cce-7] 458 < 1/100 * 193067 = 1930 considered unsuccessful
c [bca-19] limit of 10000000 steps and 386123 added (scaled 2)
c [bca-19] 33350 out of 63766 literals actually usable 52%
c [bca-19] added 5 blocked clauses in 122039 steps
c [sweep-15] limit 8405691 penalty 0 = 0 + 0
c [sweep-15-1] 3736 pos 21.3% + 13804 neg 78.7% = 17540 sched 55.0% ret 14342
c [sweep-15-1] 8436484 steps 279 queries 821.24 avg class size
c [sweep-15-1] 4501 decisions 262 SAT calls 85.12 avg env size
c [sweep-15-1] 15159 variables remain 48% (16722 retained 52%)
c [decomp-58] removed 17 variables
c [sweep-15-1] removed 17 vars (0 failed, 17 eqs, 40 impls)
c [sweep-15] 17 < 1/1000 * 31882 = 31 considered unsuccessful
c [sweep-15] removed 17 vars in TOTAL (1 rounds, 278 queries)
c [sort-queue-23] sorted 12637 enqueued variables after 235385 conflicts
c [score-dist-23] active 19228 (60%), one 9887 (31%), zero 2750 (9%)
c [score-dist-23] max exp 885, different 759 (86%)
c [score-dist-23] median active exp 788, avg 686.4
c [simplification-23] removed 157 variables 0.5% (31865 remain 15%)
c [simplification-23] removed 6814 irredundant clauses 3.4% (192581 remain 16%)
c [simplification-23] maximum reduction of 3% = max (0%, 3%)
c [simplification-23] geometric conflict interval increment 16531 = 66127 / 4
c [simplification-23] new conflict interval 82658
c [simplification-23] penalized conflict interval 82658 = 1 * 82658
c [simplification-23] hard conflict limit 359372 (soft 318043 + delta 41329)
c [simplification-23] new conflict limit 318043 (hard 359372)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  207.0   31864   192581    250531   63413   6958 407853   28   142   57  20%    343    0   37   25  149%
c i  208.8   31858   192581    254983   67524   7007 407870   28   187   60  15%   -107   45   26   25  105%
c i  209.8   31845   192581    257734   69968   7029 407878   26   152   60  17%   -130    9   23   25   90%
c -  210.9   31845   192581    260692   40428   7048 407887   27   164   38  17%   -123   19   25   25  100%
c -  224.2   31845   192581    299127   42817   7300 408013   25    93   39  27%    385  -45   34   26  130%
c 
c [simplification-24] limit 318043 conflicts (hard 359372) hit after 318048 conflicts
c [quatres-20] found 24474 quaternary clauses 50% in total
c [quatres-20-1] removed 3 duplicate quaternary clauses
c [quatres-20-2] added 4 single-self-subsuming ternary resolvents
c [quatres-20-2] added 3 quaternary resolvents
c [ternres-20] limit 33738522 with penalty 0 = 0 + 0
c [ternres-20] all 31845 free variables schedulable
c [ternres-20] 73 ternary resolvents (0 bin, 73 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-59] removed 24 variables
c [basicprobe-8] limit 168692612 penalty 0 = 0 + 0
c [basicprobe-8-0] 5571 sched 18%, 85 failed, 1 lifted, 46312 hbrs
c [decomp-60] removed 173 variables
c [basicprobe-8-1] 10253 sched 32%, 48 failed, 1 lifted, 25927 hbrs
c [decomp-61] removed 127 variables
c [basicprobe-8-2] 9945 probes remain 32% after last round
c [basicprobe-8-2] 135 units = 133 failed (99%) + 2 lifted (1%)
c [basicprobe-8-2] removed 300 variables, found 72371 hbrs
c [bate-6] eliminated 188 asymmetric tautologies during probing
c [unhide-24] limit 6747704 with penalty 0 = 0 + 0
c [unhide-24-36] 0 units, 0 failed, 32396 tauts, 0 hbrs, 470605 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 167 transitive binary clauses
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 31541 variables 100%
c [elim-16] limit of 337385225 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 274 variables 1% in round 1 in 16053615 steps
c [elim-16-1] backward subsumption/strengthening limit 16053600
c [elim-16-1-1] backward checking 1691 touched variables 5%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 3 and strengthened 18 clauses in 436287 steps
c [elim-16-1] rescheduled 65 variables 0% by backward subsumption
c [elim-16-2] eliminated 6 variables 0% in round 2 in 65253 steps
c [elim-16-2] backward subsumption/strengthening limit 65200
c [elim-16-2-1] backward checking 90 touched variables 0%
c [elim-16-2-1] incomplete backward checking 0 remain 0%
c [elim-16-2] subsumed 1 and strengthened 3 clauses in 65201 steps
c [elim-16-2] rescheduled 15 variables 0% by backward subsumption
c [elim-16-3] eliminated 1 variables 0% in round 3 in 32481 steps
c [elim-16-3] backward subsumption/strengthening limit 32400
c [elim-16-3-1] backward checking 12 touched variables 0%
c [elim-16-3-1] incomplete backward checking 0 remain 0%
c [elim-16-3] subsumed 0 and strengthened 2 clauses in 32401 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 281 = 1% variables out of 31541 scheduled
c [elim-16] 281 < 1/100 * 31541 = 315 considered unsuccessful
c [bca-20] limit of 10000000 steps and 377661 added (scaled 2)
c [bca-20] 31819 out of 62522 literals actually usable 51%
c [bca-20] added 3 blocked clauses in 124878 steps
c [sort-queue-24] sorted 15897 enqueued variables after 318048 conflicts
c [score-dist-24] active 15363 (49%), one 13439 (43%), zero 2458 (8%)
c [score-dist-24] max exp 553, different 473 (85%)
c [score-dist-24] median active exp 362, avg 350.7
c [simplification-24] removed 585 variables 1.8% (31260 remain 15%)
c [simplification-24] removed 4204 irredundant clauses 2.2% (188377 remain 16%)
c [simplification-24] maximum reduction of 2% = max (2%, 2%)
c [simplification-24] geometric conflict interval increment 27552 = 82658 / 3
c [simplification-24] new conflict interval 110210
c [simplification-24] penalized conflict interval 110210 = 1 * 110210
c [simplification-24] hard conflict limit 483363 (soft 428258 + delta 55105)
c [simplification-24] new conflict limit 428258 (hard 483363)
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  242.9   31259   188377    322446   59812   7045 421257   25   139   55  18%    576   -2   20   26   76%
c -  249.8   31258   188377    341811   44335   7173 421334   30   146   39  20%    -74    2   33   27  124%
c -  263.5   31258   188377    380525   46464   7394 421433   27   145   39  19%    416    6   32   27  117%
c i  272.6   31257   188377    405542   69447   7546 421510   33   130   63  25%    609   -7   40   28  141%
c -  278.2   31257   188377    420118   48332   7606 421547   31   108   59  28%   -364  -25   23   28   83%
c 
c [simplification-25] limit 428258 conflicts (hard 483363) hit after 440065 conflicts
c [quatres-21] found 25021 quaternary clauses 47% in total
c [quatres-21-1] removed 4 duplicate quaternary clauses
c [quatres-21-2] added 9 single-self-subsuming ternary resolvents
c [quatres-21-2] added 50 quaternary resolvents
c [ternres-21] limit 42486025 with penalty 0 = 0 + 0
c [ternres-21] all 31257 free variables schedulable
c [ternres-21] 224 ternary resolvents (1 bin, 223 trn)
c [ternres-21] fully completed ternary resolution
c [decomp-62] removed 5 variables
c [simpleprobe-9] all 31255 free variables schedulable
c [simpleprobe-9] limit 169944102 penalty 0 = 0 + 0
c [decomp-63] removed 34 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 34 variables, found 27945 hbrs, 3 units
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 281 transitive binary clauses
c [bca-21] limit of 10000000 steps and 377267 added (scaled 2)
c [bca-21] 31109 out of 62444 literals actually usable 50%
c [bca-21] added 2 blocked clauses in 133786 steps
c [sweep-16] limit 6372903 penalty 1 = 1 + 0
c [sweep-16-1] 3425 pos 23.1% + 11410 neg 76.9% = 14835 sched 47.5% ret 16386
c [sweep-16-1] 6402782 steps 95 queries 835.16 avg class size
c [sweep-16-1] 3092 decisions 84 SAT calls 191.98 avg env size
c [sweep-16-1] 14100 variables remain 45% (17121 retained 55%)
c [decomp-64] removed 10 variables
c [sweep-16-1] removed 10 vars (0 failed, 11 eqs, 14 impls)
c [sweep-16] 10 < 1/1000 * 31221 = 31 considered unsuccessful
c [sweep-16] removed 10 vars in TOTAL (1 rounds, 94 queries)
c [sort-queue-25] sorted 15679 enqueued variables after 440065 conflicts
c [score-dist-25] active 15532 (50%), one 13305 (43%), zero 2374 (8%)
c [score-dist-25] max exp 582, different 428 (73%)
c [score-dist-25] median active exp 540, avg 460.1
c [simplification-25] removed 46 variables 0.1% (31211 remain 15%)
c [simplification-25] removed 213 irredundant clauses 0.1% (188164 remain 16%)
c [simplification-25] maximum reduction of 0% = max (0%, 0%)
c [simplification-25] full geometric conflict interval increment 110210
c [simplification-25] new conflict interval 220420
c [simplification-25] penalized conflict interval 220420 = 1 * 220420
c [simplification-25] hard conflict limit 770695 (soft 660485 + delta 110210)
c [simplification-25] new conflict limit 660485 (hard 770695)
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 -  294.2   31211   188164    460528   51062   8052 449399   29   111   41  26%    275  -19   28   28  100%
c i  298.0   31210   188164    471607   61235   8103 449423   29   122   52  24%    391   -9   36   28  127%
c -  308.2   31210   188164    500374   53042   8216 449479   26   122   41  21%    -60   -6   23   28   84%
c i  312.9   31209   188164    514096   65696   8274 449500   25   105   55  24%    145  -23   15   28   55%
c -  324.0   31209   188164    540489   53637   8393 449554   30   100   41  30%    -15  -24   24   29   82%
c -  339.8   31209   188164    582570   55965   8552 449639   39   125   62  31%    477    2   50   29  171%
c i  349.3   31208   188164    608587   79619   8647 449689   31   138   89  22%    657   17   31   29  106%
c -  356.6   31165   188164    624615   57272   8718 449714   36   134   43  27%   -438   11   27   31   87%
c i  371.7   31164   188164    663136   92254   8858 449781   38   127   77  30%    212   -3   56   32  173%
c i  371.7   31163   188164    663187   92278   8862 449788   38   126   77  30%    171   -4   49   32  151%
c -  373.7   31110   188164    667840   59012   8878 449797   35   129   43  27%   -530   -1   33   32  101%
c i  383.2   31109   188164    695039   83765   8987 449829   36   123   66  29%     -8   -4   56   32  175%
c -  389.7   31090   188164    711855   62146   9036 449843   29   116   44  25%   -165   -4   31   31   98%
c i  392.6   31089   188164    719783   69341   9060 449857   32   111   54  29%    -30   -7   33   31  105%
c 
c [simplification-26] limit 660485 conflicts (hard 770695) hit after 742437 conflicts
c [quatres-22] found 25981 quaternary clauses 43% in total
c [quatres-22-2] added 12 single-self-subsuming ternary resolvents
c [quatres-22-2] added 16 quaternary resolvents
c [ternres-22] limit 66073856 with penalty 0 = 0 + 0
c [ternres-22] all 31089 free variables schedulable
c [ternres-22] 157 ternary resolvents (0 bin, 157 trn)
c [ternres-22] fully completed ternary resolution
c [decomp-65] removed 129 variables
c [treelook-9] limit 6607385 penalty 0 = 0 + 0 boost 1
c [treelook-9] scheduled 45218 literals 73%
c [treelook-9] scheduling used 1036117 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 6607385 penalty 0 = 0 + 0 boost 1
c [treelook-9] used 6624861 steps
c [treelook-9] 45016 literals remain 72%
c [treelook-9] 6251 variables remain to probed next time 20%
c [treelook-9] removed 0 variables, found 12924 hbrs
c [unhide-25] limit 3303692 with penalty 2 = 1 + 1
c [unhide-25-38] 0 units, 5 failed, 30116 tauts, 0 hbrs, 711081 literals
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 241 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 30828 variables 100%
c [block-7] limit of 41296160 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 29 blocked clauses
c [block-7] 29 < 1/100 * 186649 = 1866 considered unsuccessful
c [bca-22] limit of 10000000 steps and 368838 added (scaled 2)
c [bca-22] 28965 out of 61654 literals actually usable 47%
c [bca-22] added 3 blocked clauses in 151891 steps
c [sort-queue-26] sorted 13635 enqueued variables after 742437 conflicts
c [score-dist-26] active 17191 (56%), one 11537 (37%), zero 2098 (7%)
c [score-dist-26] max exp 838, different 701 (84%)
c [score-dist-26] median active exp 717, avg 632.4
c [simplification-26] removed 263 variables 0.8% (30826 remain 14%)
c [simplification-26] removed 4200 irredundant clauses 2.2% (183964 remain 15%)
c [simplification-26] maximum reduction of 2% = max (1%, 2%)
c [simplification-26] geometric conflict interval increment 73473 = 220420 / 3
c [simplification-26] new conflict interval 293893
c [simplification-26] penalized conflict interval 293893 = 1 * 293893
c [simplification-26] hard conflict limit 1183276 (soft 1036330 + delta 146946)
c [simplification-26] new conflict limit 1036330 (hard 1183276)
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 -  411.6   30826   183964    754533   61853   9307 429606   34   122   42  28%    173    4   38   32  117%
c i  415.5   30825   183964    765806   72120   9330 429616   34   110   57  31%    307   -7   45   32  141%
c i  420.0   30821   183964    777081   82397   9369 429629   33   107   66  31%   -195  -10   47   32  145%
c i  420.1   30759   183964    777236   82538   9369 429629   34   109   66  31%   -216   -8   50   32  154%
c i  424.1   30758   183964    786599   91152   9388 429635   34   113   75  30%   -187   -3   37   32  115%
c -  428.5   30758   183964    798589   64196   9403 429649   29   135   43  22%   -108   18   28   32   88%
c 1  432.5   30758   183964    810217   74788   9440 429665   28   172   59  16%     76   54   16   31   51%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s SATISFIABLE
c
c bate: 1333 basic ate = 1184 trn 89% + 149 lrg 11% in 6 updates
c bcas: 22 count, 823 added (2595 skipped), 4131979 steps
c bkwd: tried 319647 clauses, 638270 lits, 2.00 lits/clause
c bkwd: checked 8493054 occs, 26.57 occs/clause, 13.31 occs/lit
c bkwd: subsumed 48 binary, 342 ternary, 175 large
c bkwd: strengthened 8 binary, 6 ternary (100% self), 1204 large (0% self)
c blkd: 7 bces, 7956 removed, 7646126 resolutions, 21481757 steps
c blkd: 8291 blocking literals 2%, 77 pure
c bump: 808307 bumped seen, 208119415 lits 257.5 on average
c card: 6 count, 0 units, 0 am1, 98277762 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 67607 subsumed
c card: 15516 at-most-one constraints found, average size 4.96
c card: 15516 at-most-one constraints used 100%, average size 4.96
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, 16805 eliminated, 16786 ate 100%, 19 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 4121578 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 183 gcs, 0 rescored clauses, 425 rescored vars
c dcps: 66 decompositions, 8659 equivalent 4%
c deco: 10012 decision-only clauses 1%, 58% reduction
c decs: 6448663 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 16 elims, 88779 eliminated 39%, 38 pure 0%
c elms: 48 rounds, 3.0 rounds/bve
c elms: 75449 small 85%, 13215 large 15%
c elms: 212132 tried small, 75454 succeeded 36%, 136678 failed 64%
c elms: 38009 subsumed, 54860 strengthened, 669 blocked
c elms: 16805686 copies, 15965124 resolutions, 5894566 ipos
c elms: 3720462 subchks, 2460522 strchks
c gaus: 8 extractions, 1078 extracted, 2.4 size, 3 max
c gaus: exported 2 units, 10 binary and 0 ternary equations
c gaus: 0 gc, 20364540 steps, 10182270 extr 50%, 18322 elim 0%
c glue: 27.6 orig avg, 27.6 real avg, 4.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1146665 = 248311 simple 22% + 881481 trn 77% + 16873 lrg 1%, 5533 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 808307 clauses, 126.9 length
c lrnd: 102607301 lits = 153643917 orig - 51036616 removed 33%
c lrnd: 340168 uips 42%, 390089 flips 48%
c mins: 779970 mins 97%, 5007 bin 1%, 12337 size 2%
c mins: 418927827 poisoned searches, 66180086 hits, 16% hit rate
c mins: 499544573 used twice searches, 14045219 hits, 3% hit rate
c move: moved 14783, 8032 bin 54%, 6751 trn 46%
c otfs: 2967 driving 24%, 9411 restarting 76%
c otfs: str 12378, 12261 red 99%, 117 irr 1%
c otfs: str 12378, 0 bin 0%, 149 trn 1%, 12229 lrg 99%
c otfs: sub 28, 28 red 100%, 0 irr 0%
c otfs: sub 28, 0 bin 0%, 0 trn 0%, 28 lrg 100%
c phas: 6 computed, 130119 set, 0 pos (0%), 130119 neg (100%)
c prbs: 8 basic, 73461 probed, 2885 failed, 62 lifted
c prbs: 9 simple, 805472 probed, 1980 failed, 1659 eqs
c prbs: 9 treelook, 666 probed, 16 failed, 0 lifted
c prom: 249800 locked 12% out of 2101073 tried
c prps: 916473639 props, 134 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 22 count, 325 quat, 82 self1, 1 self2, 1353 dup
c queu: 26 sorted, 6448663 next (819310 steps 0.13)
c queu: 216837694 enq (228571942 steps 1.05), 208119415 deq 96%
c redc: 24630 clauses 35%, 71185 tried 9%, 325 sat 0%
c redc: 66620 lits 8%, 874612 tried 1%, 325 sat 0%
c redc: 3081 times jump level reduced, 16.1 levels on average
c reds: 17 count, 47659.8 conflicts per reduce
c reds: 0 memlim 0%, 17 arith 100%
c reds: 493098 collected 83%, 104059 retired 17%
c rmbd: 44838 removed, 7322 red 16%
c rsts: 19437 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 26 count, 24 confs 92%, 0 vars 0%
c simp: 1 its 4%, 1 bin 4%, 0 trns 0%
c subl: 808307 count (744464 tried 0.9), 56280 sub out of 791845 (7.1%)
c swps: 16 count, 16 rounds, 1581 queries (98.8/round)
c swps: 1430 sat calls, 26 unsat (0.7% success rate)
c swps: 30038 decisions 21.0, 1057 conflicts 0.7
c swps; 2658.1 avg class size, 110.9 avg environment size
c swps: 0 failed, 319 impls, 162 equivs
c swp0: 522 type 0 queries, 131 unsat (25.1%), 504 sat (96.6%)
c swp1: 1059 type 1 queries, 558 unsat (52.7%), 915 sat (86.4%)
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: 14515829 calls to obtain time
c tops: 97730 fixed 43%, 544 its, 1489.37 confs/it
c trds: 22 transitive reductions, 5745 removed, 13 failed
c trds: 31518 nodes, 87797 edges, 41875293 steps
c trim: 2321295 words, 8.9 MB
c trnr: 22 count, 22 bin, 4597 trn, 130236830 steps
c unhd: 25 count, 38 rounds, 90909088 steps
c unhd: 2740 non-trivial sccs of average size 2.1
c unhd: 173 units, 171 bin, 2 trn, 0 lrg
c unhd: 12185 failed, 11982 stamp, 0 lits, 167 bin, 19 trn, 0 lrg
c unhd: 394420 tauts, 11922 bin 3%, 11034 trn 3%, 1199 lrg 0%
c unhd: 394420 tauts, 370265 stamp 94%, 323170 red 82%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 2510755 str, 171 bin 0%, 4760 trn 0%, 2505824 lrg 100%, 2490077 red 99%
c vars: 30758 remaining 14% and 195168 removed 86% out of 225926
c vars: 97730 fixed 43%, 88779 eliminated 39%, 8659 equivalent 4%
c vsts: 7531670984 visits, 95% srch, 5% simp, 0% lkhd
c vsts: 8.2 search visits per propagation, 8803.6 per conflict
c wchs: 1333366728 pushed, 50826684 enlarged, 276 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         792170        493098        104059      51466695       7542149        384816
c 
c  0 0         65849   8     16120   3         0   0  29168508  57   3038785  40     84909  22     2.0
c  1 5         26633   3     12489   3      4562   4   4620733   9<   688419   9     26470   7     0.8
c  2 6         76506  10     45112   9     10760  10   6881359  13   1187677  16<    58436  15     2.3
c  3 9        113033  14     77220  16     13846  13   5097420  10   1045341  14     66029  17<    3.9
c  4 14       124405  16     88328  18     15610  15   2749710   5    643085   9     51502  13     4.4
c  5 21       117500  15<    83515  17<    15225  15<  1507473   3    399323   5     36065   9     4.9
c  6 30        99365  13     68950  14     13504  13    717034   1    245407   3     26041   7     5.2
c  7 41        71905   9     47806  10     10557  10    367254   1    143484   2     16631   4     4.1
c  8 54        44462   6     28039   6      7829   8    177386   0     76672   1      9530   2     2.6
c  9 69        24201   3     14629   3      4990   5    104305   0     40018   1      4909   1     1.5
c 10 86        15651   2      8244   2      3647   4     51846   0     21880   0      2985   1     0.9
c 11 126       10329   1      2271   0      2831   3     20331   0     10205   0      1078   0     0.8
c 12 230        2331   0       375   0       698   1      3336   0      1853   0       231   0     0.3
c 
c avg                  4.5           4.7           5.2           1.2           1.9           3.0
c std                  2.6           2.2           2.5           1.7           2.1           2.4
c 
c   32.461   8% bump
c   32.062   7% probe
c   19.605   5% unhide
c   15.498   4% elim
c    7.594   2% sweep
c    5.364   1% cce
c    3.789   1% decide
c    3.078   1% bca
c    2.485   1% transred
c    2.317   1% gauss
c 
c    5.860 < 1% rest (below)
c 
c    2.316   1% block
c    1.169   0% rescore
c    1.103   0% quatres
c    0.955   0% ternres
c    0.317   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    4.528   1% preprocessing     4%
c   97.937  23% inprocessing     96%
c ==================================
c  102.464  24% simplifying
c  330.046  76% search
c ==================================
c  432.526 100% all
c 
c        810217 conflicts,        1873.2 confs/sec
c          8880 ternaries,          91.2 confs/ternary
c          6799 binaries,          119.2 confs/binary
c           544 iterations,       1489.4 confs/iteration
c 
c            17 reductions,          0.0 redus/sec,  47659.8 confs/reduction
c         19437 restarts,           44.9 rests/sec,     41.7 confs/restart
c       6448663 decisions,       14909.3 decis/sec,      8.0 decis/conflict
c     916473639 propagations,  2118884.5 props/sec,    142.1 props/decision
c 
c 432.5 seconds, 114.9 MB
c launch: done
