c launch: /data/cnf/sc2014/app/UCG-20-5p1.cnf.bz2
c host: atom06
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/UCG-20-5p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UCG-20-5p1.cnf.bz2
c no embedded options
c found 'p cnf 224986 1204430' header
c read 224986 variables, 1204430 clauses, 2908691 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 213583 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  213583  1192277         0       0      0     0    0     0   53   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 6240 at-most-one constraints of average size 5.8
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6240 out of 6240 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 51700 variables
c [simpleprobe-1] all 173286 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 203 variables
c [simpleprobe-1] 9287 variables remain 5% (163796 retained 95%)
c [simpleprobe-1] removed 203 variables, found 14830 hbrs, 20 units
c [unhide-1] limit 57932 based on 926913 irredundant clauses
c [unhide-1-1] 17 units, 836 failed, 10768 tauts, 0 hbrs, 8216 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 171574 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 47540 not tried 28% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 65901 = 38% variables out of 171574 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 769054 negative 99.2% of 774975 except 5921 0.8%
c [phase-count-1] 623698 positive 80.5% of 774975 except 151277 19.5%
c [phase-count-1] less non-negative clauses 5921 than limit 77400 (10.0%)
c [phase-count-1] non-pos/non-neg = 151277/5921 = 25.55 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 105673 negative 100%
c [sort-queue-1] sorted 105673 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 105673 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 72469 variables 40.7% (105673 remain 49%)
c [simplification-1] removed 417302 irredundant clauses 35.0% (774975 remain 65%)
c [simplification-1] maximum reduction of 41% = max (41%, 35%)
c [simplification-1] large reduction 41% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    4.5  105672   774975         4       2      1  8106    0     1   49   0%      0    1    0    0 25376%
c i    4.5  104996   774975         5       2      1  8106    0     1   49   0%      0    1    0    0 25278%
c i    4.5  104977   774975        27      22      2  8106    0     2   49   3%      0    2    1    0 24303%
c i    4.6  104961   774975        43      30      4  8109    0     4   50   1%      0    4    1    0 23417%
c i    4.6  104633   774975        44      30      4  8109    0     4   50   1%      0    4    1    0 23326%
c i    4.6  104586   774975        58      41      5  8110    0     4   50   2%      0    4    1    0 22713%
c i    4.6  103762   774975        60      41      5  8111    0     4   50   2%      0    4    1    0 22547%
c i    4.6  103754   774975        76      47      5  8120    0     4   50   2%      0    4    1    0 21573%
c i    4.6  103745   774975        90      52      6  8124    0     4   50   2%      0    4    1    0 21043%
c i    4.6  103735   774975        93      54      6  8124    0     4   50   2%      0    4    1    0 20872%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 2001 variables
c [simpleprobe-2] 8933 schedulable variables 9%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 9866 variables remain 10% (93806 retained 90%)
c [simpleprobe-2] removed 0 variables, found 1563 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 89314 literals 43%
c [treelook-1] scheduling used 678113 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 320801 steps
c [treelook-1] 89304 literals remain 43%
c [treelook-1] 86529 variables remain to probed next time 83%
c [treelook-1] removed 4 variables, found 2252 hbrs
c [basicprobe-1] limit 6092600 based on 761575 irredundant clauses
c [basicprobe-1-0] 31220 probes remain 36% after last round
c [basicprobe-1-0] 46 units = 46 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 16927 variables, found 15219 hbrs
c [unhide-2] limit 50000 with penalty 1 = 0 + 1
c [unhide-2-2] 14 units, 1950 failed, 5919 tauts, 0 hbrs, 976 literals
c [elim-2] 41152 variables 48% will be scheduled this time
c [elim-2] scheduled 41152 variables 48%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 12239 not tried 14% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 146 = 0% variables out of 41152 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 587021 negative 99.0% of 592945 except 5924 1.0%
c [phase-count-2] 472089 positive 79.6% of 592945 except 120856 20.4%
c [phase-count-2] less non-negative clauses 5924 than limit 59200 (10.0%)
c [phase-count-2] non-pos/non-neg = 120856/5924 = 20.40 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 18024 negative 100%
c [sort-queue-2] sorted 84721 enqueued variables after 93 conflicts
c [score-dist-2] active 0 (0%), one 2374 (3%), zero 82347 (97%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 19003 variables 18.3% (84721 remain 40%)
c [simplification-2] removed 182030 irredundant clauses 23.5% (592945 remain 50%)
c [simplification-2] maximum reduction of 23% = max (18%, 23%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1030 (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.3   84720   592945       128      67      8 15007    0     6   40   2%      0    6    2    0 20079%
c i    7.4   84639   592945       193     120     16 15009    0     8   40   3%      0    8    3    0 18803%
c i    7.4   84634   592945       210     132     17 15012    0     8   40   3%      0    8    3    0 18073%
c i    7.5   84474   592945       229     144     19 15016    0     9   40   3%      0    9    3    0 17210%
c i    7.5   84425   592945       280     175     30 15023    0    10   40   3%      0   10    3    0 15678%
c i    7.5   84063   592945       282     176     30 15023    0    10   40   3%      0   10    3    0 15591%
c i    7.5   84061   592945       321     211     31 15025    0    11   40   5%      0   10    5    0 16343%
c i    7.5   83876   592945       329     216     32 15026    0    11   40   5%      0   10    5    0 15949%
c i    7.5   83660   592945       330     216     32 15026    0    11   40   5%      0   10    5    0 15887%
c i    7.6   83644   592945       427     269     47 15051    1    12   40   5%      0   12    5    0 12614%
c i    7.8   83634   592945       683     480     58 15079    1    16   40   7%      1   16    7    0 9600%
c i    7.8   83588   592945       744     514     69 15093    1    16   40   7%      1   16    6    0 8081%
c i    7.8   83583   592945       764     525     70 15095    1    17   40   7%      1   17    7    0 8189%
c i    7.8   83571   592945       770     526     73 15096    1    17   40   7%      1   17    6    0 8035%
c i    7.8   83460   592945       801     548     75 15102    1    18   40   7%      1   18    7    0 7968%
c i    7.8   83214   592945       802     548     75 15102    1    18   40   7%      1   18    7    0 7937%
c i    7.8   83211   592945       803     548     75 15102    1    18   40   7%      1   18    7    0 7906%
c 
c [simplification-3] limit of 117 binary hit after 117 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3353 at-most-one constraints of average size 4.4
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3353 out of 3353 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 1899 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 69149 literals 42%
c [treelook-2] scheduling used 501528 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 393959 steps
c [treelook-2] 69143 literals remain 42%
c [treelook-2] 59797 variables remain to probed next time 72%
c [decomp-7] removed 1 variables
c [treelook-2] removed 2 variables, found 1591 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 17 units, 959 failed, 15325 tauts, 0 hbrs, 691 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 81624 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 16086 not tried 20% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1700 = 2% variables out of 81624 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 545297 negative 99.0% of 550870 except 5573 1.0%
c [phase-count-3] 438328 positive 79.6% of 550870 except 112542 20.4%
c [phase-count-3] less non-negative clauses 5573 than limit 55000 (10.0%)
c [phase-count-3] non-pos/non-neg = 112542/5573 = 20.19 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 6048 negative 100%
c [sort-queue-3] sorted 79924 enqueued variables after 807 conflicts
c [score-dist-3] active 0 (0%), one 13444 (17%), zero 66480 (83%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 3274 variables 3.9% (79924 remain 37%)
c [simplification-3] removed 42075 irredundant clauses 7.1% (550870 remain 46%)
c [simplification-3] maximum reduction of 7% = max (4%, 7%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 1067 (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   79923   550870       891     586     73 12656    1    23   38   6%      1   23    8    0 7821%
c i   10.2   79872   550870      1052     717     82 12673    2    25   38   7%      1   25    9    0 7277%
c 
c [simplification-4] limit 1067 conflicts (hard 11000) hit after 1067 conflicts
c [decomp-8] removed 52 variables
c [basicprobe-2] limit 4404648 based on 550581 irredundant clauses
c [basicprobe-2-0] 28633 probes remain 37% after last round
c [basicprobe-2-0] 40 units = 40 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 2654 variables, found 10582 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 1 units, 1216 failed, 3409 tauts, 0 hbrs, 1967 literals
c [elim-4] 11519 variables 15% will be scheduled this time
c [elim-4] scheduled 11519 variables 15%
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] eliminated 4 variables 0% in round 1 in 24538758 steps
c [elim-4-1] backward subsumption/strengthening limit 24538700
c [elim-4-1-1] backward checking 47 touched variables 0%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 1 and strengthened 0 clauses in 103857 steps
c [elim-4-1] rescheduled 3 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 1211 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 4 = 0% variables out of 11519 scheduled
c [elim-4] 4 < 1/100 * 11519 = 115 considered unsuccessful
c [phase-count-4] 510322 negative 98.9% of 515895 except 5573 1.1%
c [phase-count-4] 407662 positive 79.0% of 515895 except 108233 21.0%
c [phase-count-4] less non-negative clauses 5573 than limit 51500 (10.0%)
c [phase-count-4] non-pos/non-neg = 108233/5573 = 19.42 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 5877 negative 100%
c [sort-queue-4] sorted 76013 enqueued variables after 1067 conflicts
c [score-dist-4] active 0 (0%), one 14400 (19%), zero 61613 (81%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 3859 variables 4.8% (76013 remain 36%)
c [simplification-4] removed 34975 irredundant clauses 6.3% (515895 remain 43%)
c [simplification-4] maximum reduction of 6% = max (5%, 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 13067 (soft 3067 + delta 10000)
c [simplification-4] new conflict limit 3067 (hard 13067)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   11.6   76012   515895      1087     737     82 17647    2    27   36   7%      1   27   10    0 7403%
c i   11.6   76008   515895      1119     763     86 17648    2    28   36   7%      1   28    9    0 7082%
c i   11.6   75982   515895      1125     767     85 17650    2    28   36   7%      1   28    9    0 6975%
c i   11.7   75934   515895      1170     801     88 17656    2    28   36   7%      1   28    9    0 6462%
c i   11.7   75930   515895      1257     873     93 17664    2    29   36   7%      1   29    8    0 5483%
c i   11.8   75920   515895      1346     951     99 17667    2    31   36   8%      1   31   11    0 6180%
c i   11.8   75899   515895      1378     971    103 17671    2    31   36   8%      1   31   10    0 5651%
c i   11.8   75894   515895      1424    1010    108 17672    2    32   36   8%      1   32    9    0 5114%
c i   11.9   75874   515895      1473    1041    116 17681    2    33   36   7%      1   33    8    0 4548%
c i   11.9   75873   515895      1524    1080    121 17687    3    34   36   7%      1   34    8    0 4565%
c i   11.9   75866   515895      1564    1106    127 17692    3    34   36   7%      1   34    8    0 4144%
c i   11.9   75865   515895      1609    1134    137 17697    3    35   36   7%      1   34    7    0 3775%
c i   12.0   75859   515895      1650    1170    138 17700    3    35   36   7%      1   35    7    0 3752%
c i   12.0   75851   515895      1698    1212    137 17703    3    36   36   7%      1   36    8    0 3796%
c i   12.0   75850   515895      1701    1213    137 17704    3    36   36   7%      1   36    8    0 3788%
c i   12.0   75668   515895      1714    1222    139 17705    3    37   36   7%      1   36    8    0 3696%
c i   12.0   75606   515895      1726    1233    139 17705    3    37   36   7%      1   36    7    0 3612%
c i   12.1   75567   515895      1852    1328    148 17721    3    39   36   7%      1   38    8    0 3550%
c i   12.1   75558   515895      1853    1328    148 17721    3    39   36   7%      1   38    8    0 3537%
c i   12.2   75557   515895      1925    1383    156 17728    3    41   36   7%      1   40    9    0 3680%
c i   12.2   75506   515895      1944    1395    160 17729    3    41   36   7%      1   40    8    0 3613%
c i   12.2   75505   515895      1956    1400    162 17732    3    41   36   7%      1   40    8    0 3490%
c i   12.2   75377   515895      2030    1448    175 17744    3    41   36   7%      1   41    7    0 2977%
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.2   75375   515895      2063    1473    177 17746    3    41   36   7%      1   40    7    0 2916%
c i   12.4   75374   515895      2263    1655    184 17754    3    44   36   8%      1   43    8    0 2970%
c i   12.4   75366   515895      2293    1679    187 17755    3    44   36   8%      1   43    8    0 2861%
c i   12.5   75365   515895      2419    1776    197 17770    3    46   36   8%      1   45    7    0 2588%
c i   12.5   75358   515895      2431    1786    197 17771    3    46   36   8%      1   45    7    0 2533%
c i   12.5   75353   515895      2445    1799    197 17771    4    46   36   8%      1   45    7    0 2589%
c i   12.5   75344   515895      2462    1814    198 17771    4    47   36   8%      1   46    7    0 2604%
c i   12.6   75343   515895      2727    2029    217 17796    4    51   36   8%      1   50    9    0 2871%
c i   12.7   75342   515895      2904    2180    229 17804    4    54   36   8%      1   52   10    0 2755%
c i   12.8   75331   515895      2940    2206    233 17808    4    55   36   8%      1   54   10    0 2673%
c i   12.8   75325   515895      2947    2211    233 17809    4    55   36   8%      1   54    9    0 2619%
c i   12.8   75319   515895      3018    2274    239 17810    4    56   37   8%      1   55   10    0 2768%
c i   12.8   75315   515895      3085    2335    240 17813    5    57   37   8%      1   56   15    0 3692%
c 
c [simplification-5] limit 3082 conflicts (hard 13067) hit after 3085 conflicts
c [quatres-1] found 37785 quaternary clauses 46% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 75315 free variables schedulable
c [ternres-1] 44 ternary resolvents (0 bin, 44 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 217 xors of average arity 2.2
c [gauss-1] connected 486 occurrences of 358 variables (average 1.4)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 173 variables
c [unhide-5] limit 146838 with penalty 0 = 0 + 0
c [unhide-5-5] 7 units, 370 failed, 11137 tauts, 0 hbrs, 3424 literals
c [transred-1] limit 734192 with penalty 0 = 0 + 0
c [transred-1] removed 112 transitive binary clauses
c [transred-1] found 5 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 74382 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 7331 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 4 clauses out of 140 (3%) of length 10
c [cce-1-1] eliminated 31 clauses out of 662 (5%) of length 9
c [cce-1-1] eliminated 53 clauses out of 625 (8%) of length 8
c [cce-1-1] eliminated 86 clauses out of 849 (10%) of length 7
c [cce-1-1] eliminated 3111 clauses out of 4541 (69%) of length 6
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 3285 large clauses in 30000018 steps
c [cce-1-1] allowing another 15000009 steps for small clauses
c [cce-1-1] scheduling 255646 clauses = 239462 binary + 16184 ternary
c [cce-1-1] tried to eliminate 788 small clauses 0%
c [cce-1-1] eliminated 321 binary clauses 0%
c [cce-1-1] eliminated 21 ternary clauses 0%
c [cce-1-1] eliminated 342 small clauses 0%
c [cce-1-1] eliminated 342 small clauses in 30000006 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3627 covered clauses in round 1
c [cce-1] eliminated 3627 covered clauses in TOTAL during 1 rounds
c [cce-1] 3627 < 1/100 * 485711 = 4857 considered unsuccessful
c [bca-1] limit of 10000000 steps and 964668 added (scaled 2)
c [bca-1] 138867 out of 148766 literals actually usable 93%
c [bca-1] added 183 blocked clauses in 441451 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 4074 pos 5.5% + 70308 neg 94.5% = 74382 sched 100.0% ret 0
c [sweep-1-1] 1070313 steps 12 queries 22182.00 avg class size
c [sweep-1-1] 90 decisions 8 SAT calls 55.38 avg env size
c [sweep-1-1] 74359 variables remain 100% (23 retained 0%)
c [decomp-10] removed 14 variables
c [sweep-1-1] removed 14 vars (0 failed, 3 eqs, 8 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 14 vars in TOTAL (1 rounds, 11 queries)
c [phase-count-5] 479500 negative 99.5% of 482049 except 2549 0.5%
c [phase-count-5] 386129 positive 80.1% of 482049 except 95920 19.9%
c [phase-count-5] less non-negative clauses 2549 than limit 48200 (10.0%)
c [phase-count-5] non-pos/non-neg = 95920/2549 = 37.63 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 4965 negative 100%
c [sort-queue-5] sorted 74368 enqueued variables after 3085 conflicts
c [score-dist-5] active 0 (0%), one 18338 (25%), zero 56030 (75%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 947 variables 1.3% (74368 remain 35%)
c [simplification-5] removed 33846 irredundant clauses 6.6% (482049 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 15085 (soft 5085 + delta 10000)
c [simplification-5] new conflict limit 5085 (hard 15085)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   15.7   74367   482049      3171    2374    302 25331    5    60   36   8%      1   58   15    0 3591%
c i   15.7   74360   482049      3208    2405    303 25334    5    60   36   8%      1   59   15    0 3397%
c i   15.8   74309   482049      3277    2456    309 25344    5    61   36   8%      1   60   13    0 2891%
c i   15.8   74300   482049      3291    2467    311 25344    5    61   36   8%      1   60   12    0 2781%
c i   15.8   74288   482049      3321    2490    313 25348    5    61   36   8%      1   60   11    0 2586%
c i   15.9   73800   482049      3360    2523    316 25350    5    62   36   8%      1   60   11    0 2445%
c i   16.0   73797   482049      3452    2598    322 25358    5    64   36   8%      1   62    9    0 2064%
c i   16.0   73791   482049      3589    2718    326 25364    6    65   36   8%      1   63   13    0 2619%
c i   16.1   73784   482049      3700    2812    335 25370    6    66   36   9%      1   64   12    0 2335%
c i   16.1   73783   482049      3715    2825    336 25370    6    66   36   9%      1   64   11    0 2277%
c i   16.1   73775   482049      3793    2893    338 25374    6    67   36   9%      1   65   12    1 2291%
c i   16.2   73774   482049      3851    2935    343 25382    6    70   36   8%      1   68   11    1 2173%
c i   16.3   73767   482049      4006    3062    354 25392    6    72   36   9%      1   69   14    1 2537%
c i   16.4   73766   482049      4346    3351    378 25409    7    73   36   9%      1   70   11    1 1783%
c i   16.5   73761   482049      4402    3395    380 25411    7    73   36   9%      1   71   12    1 1946%
c i   16.5   73760   482049      4497    3471    386 25422    7    75   36   9%      1   72   12    1 1813%
c i   16.6   73749   482049      4586    3546    391 25429    7    76   36   9%      1   73   12    1 1760%
c i   16.6   73747   482049      4769    3708    397 25437    7    78   36   9%      1   74   13    1 1899%
c i   16.8   73737   482049      5038    3946    407 25444    8    80   36  10%      1   77   17    1 2180%
c 
c [simplification-6] limit 5085 conflicts (hard 15085) hit after 5085 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 73733 free variables schedulable
c [ternres-2] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-2] 42639 variables remain 58% (31094 retained 42%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2438 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] 2438 out of 2438 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 667 variables
c [simpleprobe-3] 6049 schedulable variables 8%
c [simpleprobe-3] limit 2236012 penalty 1 = 1 + 0
c [simpleprobe-3] 6666 variables remain 9% (67035 retained 91%)
c [simpleprobe-3] removed 0 variables, found 3212 hbrs, 0 units
c [unhide-6] limit 223601 with penalty 0 = 0 + 0
c [unhide-6-6] 3 units, 589 failed, 2899 tauts, 0 hbrs, 5671 literals
c [transred-2] limit 1118006 with penalty 0 = 0 + 0
c [transred-2] removed 182 transitive binary clauses
c [transred-2] found 14 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 72947 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 1146 blocked clauses
c [block-2] 1146 < 1/100 * 477241 = 4772 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 72947 variables 100%
c [elim-5] limit of 11180061 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 21159 not tried 29% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1081 = 1% variables out of 72947 scheduled
c [bca-2] limit of 10000000 steps and 931783 added (scaled 2)
c [bca-2] 132568 out of 143734 literals actually usable 92%
c [bca-2] added 155 blocked clauses in 419717 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 4543 pos 6.3% + 67309 neg 93.7% = 71852 sched 100.0% ret 14
c [sweep-2-1] 1186580 steps 9 queries 15757.11 avg class size
c [sweep-2-1] 130 decisions 7 SAT calls 95.14 avg env size
c [sweep-2-1] 71836 variables remain 100% (23 retained 0%)
c [decomp-13] removed 15 variables
c [sweep-2-1] removed 15 vars (0 failed, 1 eqs, 2 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 15 vars in TOTAL (1 rounds, 8 queries)
c [phase-count-6] 463050 negative 99.5% of 465453 except 2403 0.5%
c [phase-count-6] 370903 positive 79.7% of 465453 except 94550 20.3%
c [phase-count-6] less non-negative clauses 2403 than limit 46500 (10.0%)
c [phase-count-6] non-pos/non-neg = 94550/2403 = 39.35 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 3416 negative 100%
c [sort-queue-6] sorted 71851 enqueued variables after 5085 conflicts
c [score-dist-6] active 0 (0%), one 22253 (31%), zero 49598 (69%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 1882 variables 2.6% (71851 remain 34%)
c [simplification-6] removed 16596 irredundant clauses 3.4% (465453 remain 39%)
c [simplification-6] maximum reduction of 3% = max (3%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 5000
c [simplification-6] penalized conflict interval 5000 = 1 * 5000
c [simplification-6] hard conflict limit 20085 (soft 10085 + delta 10000)
c [simplification-6] new conflict limit 10085 (hard 20085)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   19.7   71850   465453      5172    2939    377 26485    8    84   35   9%      1   81   13    1 1644%
c i   19.7   71849   465453      5222    2983    377 26487    8    84   35   9%      1   81   13    1 1651%
c i   19.7   71848   465453      5223    2983    377 26487    8    84   35   9%      1   81   13    1 1645%
c i   19.7   71846   465453      5246    3004    377 26488    8    84   35  10%      1   80   13    1 1586%
c i   20.0   71844   465453      5735    3415    403 26524    8    86   35  10%      2   82   10    1 1133%
c i   20.0   71841   465453      5757    3428    408 26527    8    86   35  10%      2   82    9    1 1068%
c i   20.0   71832   465453      5779    3448    408 26527    8    86   35  10%      2   81   10    1 1136%
c i   20.1   71824   465453      5835    3492    411 26534    8    86   35  10%      2   82   10    1 1110%
c i   20.1   71820   465453      5851    3504    412 26536    8    86   35  10%      2   81   10    1 1102%
c i   20.4   71816   465453      6607    4157    452 26577    9    88   35  10%      4   83   11    1 1125%
c i   20.5   71814   465453      6664    4205    457 26579    9    88   35  10%      4   83   11    1 1107%
c i   20.6   71813   465453      7028    4531    473 26598   10    89   35  11%      4   83   15    1 1354%
c i   20.7   71812   465453      7166    4649    483 26604   10    91   35  11%      3   85   15    1 1282%
c i   20.9   71809   465453      7503    4917    505 26630   10    95   35  11%      3   88   17    1 1365%
c i   21.0   71798   465453      7689    5055    523 26653   10    96   35  11%      3   89   12    1  993%
c i   21.1   71679   465453      7784    5134    527 26664   10    97   35  11%      3   90   11    1  861%
c i   21.1   71671   465453      7785    5134    527 26664   10    97   35  11%      3   90   11    1  858%
c i   21.1   71670   465453      7818    5158    529 26670   10    97   35  11%      3   90   11    1  839%
c i   21.2   71666   465453      7832    5170    529 26671   10    98   35  10%      3   91   10    1  836%
c i   21.2   71313   465453      7862    5192    531 26675   10    98   35  10%      2   91   10    1  783%
c i   21.2   70935   465453      7900    5217    535 26683   10    98   35  10%      2   91    9    1  739%
c i   21.4   70928   465453      8083    5379    541 26695   10   100   35  10%      2   93    9    1  740%
c i   21.5   70913   465453      8353    5615    547 26712   11   102   36  11%      2   94   16    1 1197%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   21.5   70793   465453      8367    5623    549 26715   11   101   36  11%      2   94   16    1 1147%
c i   21.7   70787   465453      8659    5857    569 26747   11   104   36  11%      2   96   13    1  921%
c i   21.7   70785   465453      8675    5869    570 26749   11   104   36  11%      2   96   13    1  897%
c i   21.8   70772   465453      8718    5902    573 26755   11   105   36  10%      2   97   11    1  809%
c i   21.8   70760   465453      8759    5934    578 26758   11   106   36  10%      2   98   11    1  769%
c i   21.9   70748   465453      8796    5968    580 26758   11   107   36  10%      2   99   15    1 1033%
c i   21.9   70743   465453      8800    5970    580 26759   11   107   36  10%      2   99   15    1 1022%
c i   21.9   70736   465453      8882    6039    584 26763   11   107   36  11%      2   99   16    1 1082%
c i   22.0   70735   465453      9091    6223    599 26767   11   108   36  11%      2   99   14    2  945%
c i   22.2   70721   465453      9488    6571    617 26791   12   109   36  11%      2   99   13    2  846%
c i   22.4   70715   465453      9907    6929    636 26820   13   110   36  11%      2  100   19    2 1139%
c 
c [simplification-7] limit 10107 conflicts (hard 20085) hit after 10107 conflicts
c [quatres-2] found 38927 quaternary clauses 50% in total
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [quatres-2-2] added 25 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 40859 schedulable variables 57%
c [ternres-3] 42 ternary resolvents (0 bin, 42 trn)
c [ternres-3] 9160 variables remain 13% (61546 retained 87%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 38 xors of average arity 2.4
c [gauss-2] connected 92 occurrences of 79 variables (average 1.2)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 84 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 45221 literals 32%
c [treelook-3] scheduling used 300629 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 396481 steps
c [treelook-3] 45203 literals remain 32%
c [treelook-3] 37073 variables remain to probed next time 52%
c [treelook-3] removed 6 variables, found 3193 hbrs
c [unhide-7] limit 420815 with penalty 0 = 0 + 0
c [unhide-7-7] 3 units, 197 failed, 8804 tauts, 0 hbrs, 7821 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 377 transitive binary clauses
c [transred-3] found 19 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 3 clauses out of 737 (0%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 3 large clauses in 15000004 steps
c [cce-2-1] allowing another 7500002 steps for small clauses
c [cce-2-1] scheduling 236389 clauses = 220057 binary + 16332 ternary
c [cce-2-1] tried to eliminate 381 small clauses 0%
c [cce-2-1] eliminated 133 binary clauses 0%
c [cce-2-1] eliminated 6 ternary clauses 0%
c [cce-2-1] eliminated 139 small clauses 0%
c [cce-2-1] eliminated 3569 small clauses in 15000003 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 3572 covered clauses in round 1
c [cce-2] eliminated 3572 covered clauses in TOTAL during 1 rounds
c [cce-2] 3572 < 1/100 * 448814 = 4488 considered unsuccessful
c [elim-6] 20769 variables 30% will be scheduled this time
c [elim-6] scheduled 20769 variables 30%
c [elim-6] limit of 42081507 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 7 variables 0% in round 1 in 29141578 steps
c [elim-6-1] backward subsumption/strengthening limit 12939929
c [elim-6-1-1] backward checking 224 touched variables 0%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 3 and strengthened 1 clauses in 144949 steps
c [elim-6-1] rescheduled 13 variables 0% by backward subsumption
c [elim-6-2] eliminated 2 variables 0% in round 2 in 4926 steps
c [elim-6-2] backward subsumption/strengthening limit 4900
c [elim-6-2-1] backward checking 18 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 4901 steps
c [elim-6-2] fully rescheduled 70270 variables 100%
c [elim-6] incomplete 16704 not tried 24% in round 3
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 465 = 2% variables out of 20769 scheduled
c [elim-6] 465 < 1/100 * 20769 = 207 considered unsuccessful
c [bca-3] limit of 10000000 steps and 888681 added (scaled 2)
c [bca-3] 123542 out of 139630 literals actually usable 88%
c [bca-3] added 91 blocked clauses in 380792 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 4542 pos 6.5% + 65251 neg 93.5% = 69793 sched 100.0% ret 21
c [sweep-3-1] 1024207 steps 22 queries 11776.09 avg class size
c [sweep-3-1] 465 decisions 20 SAT calls 65.50 avg env size
c [sweep-3-1] 69621 variables remain 100% (193 retained 0%)
c [decomp-16] removed 191 variables
c [sweep-3-1] removed 191 vars (0 failed, 1 eqs, 7 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 191 vars in TOTAL (1 rounds, 21 queries)
c [phase-count-7] 441287 negative 99.5% of 443682 except 2395 0.5%
c [phase-count-7] 352880 positive 79.5% of 443682 except 90802 20.5%
c [phase-count-7] less non-negative clauses 2395 than limit 44300 (10.0%)
c [phase-count-7] non-pos/non-neg = 90802/2395 = 37.91 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 1389 negative 100%
c [sort-queue-7] sorted 69623 enqueued variables after 10107 conflicts
c [score-dist-7] active 0 (0%), one 29416 (42%), zero 40207 (58%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 1083 variables 1.5% (69623 remain 33%)
c [simplification-7] removed 21771 irredundant clauses 4.7% (443682 remain 37%)
c [simplification-7] maximum reduction of 5% = max (2%, 5%)
c [simplification-7] large reduction 5% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 22107 (soft 12107 + delta 10000)
c [simplification-7] new conflict limit 12107 (hard 22107)
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.3   69622   443682     10155    6602    611 28166   13   115   36  12%      2  104   23    2 1269%
c i   26.4   69616   443682     10253    6688    615 28172   13   115   36  12%      2  105   22    2 1186%
c i   26.5   69609   443682     10307    6731    618 28178   13   116   36  12%      2  105   19    2 1051%
c i   26.7   69608   443682     10708    7075    641 28200   14   117   36  12%      2  106   17    2  864%
c i   26.7   69605   443682     10718    7084    641 28200   14   117   36  12%      2  106   16    2  853%
c i   26.7   69603   443682     10738    7100    642 28202   14   117   36  12%      2  106   17    2  862%
c i   26.8   69600   443682     10836    7190    647 28204   14   118   36  12%      2  107   17    2  850%
c i   26.9   69481   443682     11018    7331    658 28223   14   121   36  11%      2  109   14    2  698%
c i   27.0   69396   443681     11091    7383    664 28236   14   121   36  11%      2  109   13    2  662%
c i   27.1   69383   443681     11193    7463    671 28250   14   122   36  11%      2  109   12    2  611%
c i   27.1   69357   443681     11198    7466    671 28251   14   122   36  11%      2  109   12    2  614%
c i   27.1   69348   443681     11270    7525    677 28256   14   123   36  11%      2  111   11    2  552%
c i   27.2   69337   443681     11314    7560    678 28263   13   123   36  11%      2  110   11    2  535%
c i   27.2   69333   443681     11329    7567    681 28266   13   123   36  11%      2  110   11    2  523%
c i   27.3   69309   443681     11410    7632    690 28271   13   122   36  11%      1  109    9    2  450%
c i   27.3   69299   443681     11422    7641    690 28273   13   122   36  11%      1  109    9    2  439%
c i   27.3   69162   443681     11437    7652    691 28275   13   121   36  11%      1  109    9    2  422%
c i   27.3   68967   443681     11481    7684    696 28278   13   122   36  11%      1  109    9    2  453%
c i   27.3   68964   443681     11506    7699    699 28281   13   122   36  11%      1  109    9    2  431%
c i   27.4   68961   443681     11568    7748    703 28287   13   122   36  11%      1  110    9    2  419%
c i   27.4   68956   443681     11598    7771    706 28290   13   122   36  11%      1  109    8    2  401%
c i   27.5   68937   443681     11649    7816    710 28291   13   122   36  11%      1  109    8    2  410%
c i   27.5   68926   443681     11654    7820    710 28291   13   121   36  11%      1  109    8    2  407%
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   27.5   68820   443681     11717    7862    720 28299   13   121   36  11%      1  108    7    2  352%
c i   27.5   68819   443681     11765    7887    732 28306   13   120   36  11%      1  107    7    2  321%
c i   27.6   68625   443681     11775    7894    733 28307   13   120   36  11%      1  107    6    2  318%
c i   27.6   68616   443681     11816    7927    739 28308   13   120   36  11%      1  107    6    2  305%
c i   27.6   68560   443681     11861    7957    744 28315   13   119   36  10%      1  106    6    2  283%
c i   27.7   68543   443681     12066    8125    764 28324   13   119   36  11%      1  106   13    2  641%
c 
c [simplification-8] limit 12113 conflicts (hard 22107) hit after 12113 conflicts
c [quatres-3] found 37752 quaternary clauses 51% in total
c [quatres-3-2] added 2 single-self-subsuming ternary resolvents
c [quatres-3-2] added 113 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 8872 schedulable variables 13%
c [ternres-4] 48 ternary resolvents (0 bin, 48 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 1117 variables
c [basicprobe-3] limit 12936373 penalty 0 = 0 + 0
c [basicprobe-3-0] 24324 probes remain 36% after last round
c [basicprobe-3-0] 129 units = 129 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 1544 variables, found 29123 hbrs
c [bate-1] eliminated 30 asymmetric tautologies during probing
c [unhide-8] limit 517454 with penalty 0 = 0 + 0
c [unhide-8-8] 9 units, 793 failed, 5000 tauts, 0 hbrs, 11267 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 281 transitive binary clauses
c [transred-4] found 6 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 66021 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 278 blocked clauses
c [block-3] 278 < 1/100 * 425770 = 4257 considered unsuccessful
c [bca-4] limit of 10000000 steps and 832664 added (scaled 2)
c [bca-4] 112281 out of 131968 literals actually usable 85%
c [bca-4] added 121 blocked clauses in 328416 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 5041 pos 7.7% + 60760 neg 92.3% = 65801 sched 99.7% ret 182
c [sweep-4-1] 1009476 steps 16 queries 16515.31 avg class size
c [sweep-4-1] 103 decisions 15 SAT calls 40.67 avg env size
c [sweep-4-1] 65744 variables remain 100% (239 retained 0%)
c [decomp-18] removed 161 variables
c [sweep-4-1] removed 161 vars (0 failed, 0 eqs, 2 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 161 vars in TOTAL (1 rounds, 15 queries)
c [phase-count-8] 413195 negative 99.4% of 415590 except 2395 0.6%
c [phase-count-8] 328925 positive 79.1% of 415590 except 86665 20.9%
c [phase-count-8] less non-negative clauses 2395 than limit 41500 (10.0%)
c [phase-count-8] non-pos/non-neg = 86665/2395 = 36.19 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 517 negative 100%
c [sort-queue-8] sorted 65822 enqueued variables after 12113 conflicts
c [score-dist-8] active 0 (0%), one 35203 (53%), zero 30619 (47%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 2718 variables 4.0% (65822 remain 31%)
c [simplification-8] removed 28091 irredundant clauses 6.3% (415590 remain 35%)
c [simplification-8] maximum reduction of 6% = max (4%, 6%)
c [simplification-8] large reduction 6% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 24113 (soft 14113 + delta 10000)
c [simplification-8] new conflict limit 14113 (hard 24113)
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.8   65821   415590     12124    8206    842 48274   13   120   35  11%      1  106   12    2  569%
c i   30.2   65798   415590     12650    8666    863 48308   13   122   35  10%      2  107   12    2  557%
c i   30.3   65793   415590     12753    8755    870 48311   13   123   35  10%      2  108   14    2  622%
c i   30.3   65791   415590     12759    8760    870 48311   13   123   35  10%      2  108   14    2  612%
c i   30.3   65790   415590     12823    8807    872 48317   13   122   35  11%      2  107   17    2  782%
c i   30.3   65787   415590     12825    8808    872 48317   13   122   35  11%      2  107   17    2  777%
c i   30.3   65783   415590     12861    8841    873 48318   13   122   35  11%      2  107   17    2  747%
c i   30.4   65779   415590     12937    8902    879 48326   13   122   35  11%      2  107   14    2  644%
c i   30.4   65776   415590     13006    8968    881 48326   13   122   35  11%      2  107   18    2  810%
c i   30.5   65770   415590     13041    8999    883 48326   13   121   35  11%      2  106   18    2  802%
c i   30.5   65726   415590     13126    9073    884 48333   13   122   35  11%      1  107   18    2  796%
c i   30.5   65725   415590     13127    9073    884 48333   13   122   35  11%      1  107   18    2  793%
c i   30.5   65724   415590     13129    9073    885 48333   13   122   35  11%      1  106   18    2  787%
c i   30.6   65715   415590     13230    9162    891 48336   13   122   35  11%      1  106   15    2  653%
c i   30.6   65709   415590     13231    9162    891 48336   13   122   35  11%      1  106   15    2  650%
c i   30.6   65583   415590     13261    9182    896 48340   13   121   35  11%      1  106   14    2  603%
c i   30.7   65580   415590     13357    9267    899 48347   14   123   35  11%      1  108   18    2  759%
c i   30.7   65577   415590     13443    9345    901 48348   14   123   35  11%      1  107   21    2  881%
c i   30.7   65500   415590     13467    9363    902 48352   14   123   35  11%      1  107   21    2  879%
c i   30.8   65489   415590     13527    9395    912 48368   14   122   35  11%      1  106   17    2  728%
c i   30.8   65481   415590     13535    9395    915 48372   14   122   35  11%      1  106   17    2  707%
c i   30.8   65474   415590     13536    9395    915 48372   14   122   35  11%      1  106   17    2  704%
c i   31.0   65469   415590     13726    9559    925 48385   14   126   35  11%      1  109   15    2  620%
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   31.0   65462   415590     13769    9591    927 48393   14   125   35  11%      1  109   13    2  549%
c i   31.0   65440   415590     13770    9591    927 48393   14   125   35  11%      1  109   13    2  547%
c i   31.2   65437   415590     13948    9735    943 48408   14   128   35  11%      1  111   12    2  491%
c i   31.2   65430   415590     13982    9761    947 48410   14   128   35  11%      1  112   12    2  473%
c i   31.2   65429   415590     14021    9793    951 48412   13   128   35  11%      1  111   11    2  429%
c i   31.3   65422   415590     14066    9829    954 48416   13   129   35  10%      1  112   10    2  401%
c i   31.3   65418   415590     14075    9832    956 48419   13   129   35  10%      1  112   10    2  389%
c i   31.3   65412   415590     14093    9845    957 48419   13   129   35  10%      1  112    9    2  383%
c i   31.3   65404   415590     14096    9847    957 48419   13   129   35  10%      1  112   10    2  394%
c i   31.4   65395   415590     14160    9902    962 48421   13   129   35  10%      1  112   12    2  496%
c 
c [simplification-9] limit 14169 conflicts (hard 24113) hit after 14170 conflicts
c [quatres-4] found 36042 quaternary clauses 52% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-2] added 16 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 65393 free variables schedulable
c [ternres-5] 32 ternary resolvents (0 bin, 32 trn)
c [ternres-5] 32514 variables remain 50% (32879 retained 50%)
c [decomp-19] removed 569 variables
c [unhide-9] limit 612590 with penalty 0 = 0 + 0
c [unhide-9-9] 12 units, 103 failed, 7634 tauts, 0 hbrs, 6931 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 280 transitive binary clauses
c [transred-5] found 6 units
c [elim-7] 15785 variables 24% will be scheduled this time
c [elim-7] scheduled 15785 variables 24%
c [elim-7] limit of 30629544 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 8 variables 0% in round 1 in 23547094 steps
c [elim-7-1] backward subsumption/strengthening limit 7082450
c [elim-7-1-1] backward checking 378 touched variables 1%
c [elim-7-1-1] incomplete backward checking 312 remain 83%
c [elim-7-1] subsumed 0 and strengthened 162 clauses in 7082504 steps
c [elim-7] incomplete 178 not tried 0% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 8 = 0% variables out of 15785 scheduled
c [elim-7] 8 < 1/100 * 15785 = 157 considered unsuccessful
c [bca-5] limit of 10000000 steps and 802409 added (scaled 2)
c [bca-5] 107689 out of 130048 literals actually usable 83%
c [bca-5] added 75 blocked clauses in 304843 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 4768 pos 7.4% + 60016 neg 92.6% = 64784 sched 99.6% ret 239
c [sweep-5-1] 10052434 steps 149 queries 3312.34 avg class size
c [sweep-5-1] 2125 decisions 124 SAT calls 90.28 avg env size
c [sweep-5-1] 61290 variables remain 95% (3561 retained 5%)
c [decomp-20] removed 339 variables
c [sweep-5-1] removed 339 vars (0 failed, 28 eqs, 57 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 339 vars in TOTAL (1 rounds, 148 queries)
c [phase-count-9] 395424 negative 99.4% of 397816 except 2392 0.6%
c [phase-count-9] 313076 positive 78.7% of 397816 except 84740 21.3%
c [phase-count-9] less non-negative clauses 2392 than limit 39700 (10.0%)
c [phase-count-9] non-pos/non-neg = 84740/2392 = 35.43 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 307 negative 100%
c [sort-queue-9] sorted 64684 enqueued variables after 14170 conflicts
c [score-dist-9] active 0 (0%), one 39034 (60%), zero 25650 (40%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 709 variables 1.1% (64684 remain 30%)
c [simplification-9] removed 17774 irredundant clauses 4.3% (397816 remain 33%)
c [simplification-9] maximum reduction of 4% = max (1%, 4%)
c [simplification-9] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-9] new conflict interval 9000
c [simplification-9] penalized conflict interval 9000 = 1 * 9000
c [simplification-9] hard conflict limit 33170 (soft 23170 + delta 10000)
c [simplification-9] new conflict limit 23170 (hard 33170)
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.8   64683   397816     14209    9909    960 55413   13   129   35  10%      1  112   11    2  462%
c i   33.9   64678   397816     14298    9981    967 55420   13   129   35  10%      1  112   11    2  435%
c i   34.3   64667   397816     14655   10272    989 55455   14   134   36  10%      1  116   14    3  538%
c i   34.3   64661   397816     14656   10272    989 55455   14   134   36  10%      1  116   14    3  536%
c i   34.5   64660   397816     14962   10544   1001 55465   14   133   36  10%      2  115   15    3  579%
c i   34.5   64659   397816     15016   10596   1001 55466   14   133   36  11%      1  114   18    3  664%
c i   34.7   64658   397816     15255   10804   1014 55479   14   134   36  11%      1  115   19    3  699%
c i   34.8   64654   397816     15340   10880   1020 55481   14   136   36  10%      1  117   17    3  626%
c i   34.8   64653   397816     15347   10886   1020 55481   14   136   36  10%      1  117   17    3  613%
c i   34.8   64561   397816     15368   10902   1021 55484   14   136   36  10%      1  117   16    3  572%
c i   34.8   64560   397816     15380   10909   1023 55486   14   135   36  10%      1  116   15    3  549%
c i   34.8   64559   397816     15390   10914   1026 55487   14   135   36  10%      1  116   14    3  531%
c i   34.9   64558   397816     15619   11100   1038 55508   14   135   36  10%      1  116   16    3  571%
c i   35.1   64557   397816     15819   11273   1052 55518   14   137   36  11%      1  117   18    3  623%
c i   35.2   64552   397816     15919   11352   1062 55525   15   139   36  10%      1  119   18    3  636%
c i   35.3   64543   397816     15938   11366   1064 55527   14   139   36  10%      1  119   17    3  612%
c i   35.3   64495   397816     15951   11372   1067 55530   14   139   36  10%      1  118   17    3  589%
c i   35.3   64407   397816     15958   11375   1068 55532   14   138   36  10%      1  118   16    3  577%
c i   35.3   64406   397816     15985   11395   1068 55538   14   138   36  10%      1  118   15    3  541%
c i   35.3   64397   397816     16010   11415   1069 55541   14   138   36  10%      1  117   15    3  513%
c i   35.3   64293   397816     16047   11438   1072 55548   14   137   36  10%      1  117   14    3  478%
c i   35.3   64283   397816     16081   11456   1078 55554   14   137   36  10%      1  116   13    3  448%
c i   35.4   64045   397816     16094   11465   1078 55557   14   136   36  10%      1  116   12    3  433%
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   35.4   64044   397816     16138   11492   1080 55568   14   136   36  10%      1  115   11    3  384%
c i   35.5   64039   397816     16281   11586   1106 55586   14   134   36  10%      1  114    9    3  302%
c i   35.6   64034   397816     16350   11639   1116 55590   14   135   36  10%      1  114    8    3  294%
c i   35.6   64031   397816     16359   11642   1117 55594   14   134   36  10%      1  114    8    3  287%
c i   35.6   64001   397816     16383   11658   1120 55597   14   134   36  10%      1  113    8    3  272%
c i   35.6   63921   397816     16411   11680   1124 55598   14   134   36  10%      1  113    8    3  283%
c i   35.6   63916   397816     16435   11697   1124 55602   14   134   36  10%      1  114    8    3  274%
c i   35.6   63833   397816     16441   11700   1126 55602   14   134   36  10%      1  113    8    3  281%
c i   35.7   63826   397816     16540   11768   1138 55617   13   134   36  10%      1  113    7    3  237%
c i   35.7   63821   397816     16576   11789   1142 55626   13   134   36  10%      1  113    7    3  229%
c i   35.8   63761   397816     16631   11831   1147 55632   13   135   36  10%      1  114    7    3  238%
c i   35.8   63757   397816     16648   11841   1148 55637   13   135   36  10%      1  113    7    3  229%
c i   35.8   63755   397816     16691   11871   1152 55643   13   134   36  10%      1  113    6    3  215%
c i   35.8   63751   397816     16692   11871   1152 55643   13   134   36  10%      1  113    6    3  214%
c i   35.9   63749   397816     16727   11893   1154 55652   13   134   36  10%      1  112    6    3  201%
c i   35.9   63733   397816     16787   11933   1166 55659   13   133   36  10%      1  111    6    3  203%
c i   35.9   63724   397816     16806   11946   1171 55659   13   133   36  10%      1  111    6    3  197%
c i   35.9   63663   397816     16821   11957   1173 55660   13   132   36  10%      1  111    6    3  191%
c i   36.0   63631   397816     16857   11984   1177 55664   13   133   36  10%      1  111    5    3  187%
c i   36.0   63588   397816     16899   12008   1181 55677   13   133   36  10%      1  111    5    3  180%
c i   36.1   63545   397816     17013   12088   1200 55690   12   132   36   9%      1  110    5    3  173%
c i   36.2   63510   397816     17086   12133   1214 55703   12   131   36   9%      0  109    5    3  172%
c i   36.2   63509   397816     17087   12133   1214 55703   12   131   36   9%      0  109    5    3  171%
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   36.4   63483   397816     17299   12289   1243 55725   12   134   36   9%      1  111    6    3  204%
c i   36.5   63471   397816     17481   12406   1269 55759   12   133   36   9%      1  110    6    3  212%
c i   36.5   63464   397816     17527   12440   1271 55767   12   133   36   9%      1  110    6    3  214%
c i   36.5   63372   397816     17542   12447   1273 55771   12   132   36   9%      1  110    6    3  206%
c i   36.7   63364   397816     17729   12587   1292 55796   11   134   36   9%      1  110    7    3  242%
c i   36.8   63078   397816     17850   12671   1310 55814   11   135   36   8%      1  112    7    3  248%
c i   36.8   63072   397816     17858   12677   1310 55815   11   135   36   8%      1  112    7    3  242%
c i   36.9   63071   397816     17947   12750   1317 55823   11   134   36   8%      1  110    7    3  254%
c i   36.9   63067   397816     17992   12782   1322 55830   11   133   36   8%      1  109    7    3  238%
c i   37.0   63065   397816     18081   12844   1331 55847   11   131   36   8%      1  108    6    3  210%
c i   37.0   63056   397816     18109   12868   1332 55849   11   131   36   8%      1  107    6    3  210%
c i   37.0   63050   397816     18110   12868   1332 55849   11   131   36   8%      1  107    6    3  209%
c i   37.0   62924   397816     18111   12868   1332 55849   11   131   36   8%      1  107    6    3  209%
c i   37.0   62896   397816     18163   12905   1340 55855   11   130   36   8%      1  107    6    3  195%
c i   37.1   62893   397816     18272   12988   1347 55869   11   129   36   8%      1  105    7    3  220%
c i   37.1   62890   397816     18309   13013   1351 55876   11   129   36   8%      1  105    6    3  217%
c i   37.1   62888   397816     18319   13018   1352 55879   11   129   36   8%      1  105    6    3  211%
c i   37.2   62887   397816     18375   13056   1357 55889   11   129   36   8%      0  105    8    3  276%
c i   37.2   62882   397816     18425   13095   1359 55897   11   128   36   8%      0  104    8    3  253%
c i   37.3   62879   397816     18503   13155   1362 55909   11   129   36   8%      0  105    8    3  275%
c i   37.4   62869   397816     18628   13248   1373 55922   11   130   36   8%      0  105    8    3  261%
c i   37.4   62841   397816     18634   13251   1375 55922   11   130   36   8%      0  105    8    3  257%
c i   37.4   62840   397816     18714   13312   1380 55933   11   129   36   8%      0  104    7    3  248%
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.5   62839   397816     18752   13339   1381 55937   11   129   36   8%      0  104    9    3  286%
c i   37.5   62838   397816     18789   13368   1385 55940   11   129   36   8%      0  104    9    3  308%
c i   37.5   62837   397816     18835   13406   1387 55945   11   129   36   8%      0  104    9    3  307%
c i   37.6   62836   397816     18938   13483   1397 55958   11   128   36   8%      0  103   10    3  329%
c i   37.6   62835   397816     18986   13521   1400 55963   11   128   36   8%      0  103    9    3  304%
c i   37.6   62830   397816     18990   13524   1400 55963   11   128   36   8%      0  103    9    3  301%
c i   37.6   62826   397816     18993   13526   1400 55963   11   128   36   8%      0  103    9    3  302%
c i   37.7   62825   397816     19055   13570   1409 55970   11   128   36   8%      0  103    8    3  281%
c i   38.2   62818   397816     19740   14095   1476 56050   10   134   36   8%      3  108   10    3  336%
c i   38.3   62812   397816     19751   14098   1478 56055   10   134   36   8%      3  108   10    3  325%
c i   38.4   62811   397816     19940   14271   1488 56059   11   138   36   8%      3  111   15    3  488%
c i   38.4   62474   397816     19941   14271   1488 56059   11   138   36   8%      3  111   15    3  486%
c i   38.5   62459   397816     19977   14301   1490 56062   11   140   36   8%      2  113   21    3  659%
c i   38.6   62449   397816     20080   14374   1498 56081   11   140   36   8%      2  113   19    3  581%
c i   38.6   62440   397816     20132   14417   1504 56083   11   141   36   8%      2  114   18    3  558%
c i   38.8   62437   397816     20314   14584   1511 56090   12   142   36   9%      2  115   23    3  701%
c i   39.0   62432   397816     20672   14896   1526 56106   13   143   36   9%      2  115   22    3  650%
c i   39.1   62431   397816     20840   15037   1538 56118   13   142   36   9%      2  114   20    3  570%
c i   39.1   62427   397816     20850   15044   1539 56119   13   142   36   9%      2  114   19    3  559%
c i   39.1   62415   397816     20851   15044   1539 56119   13   142   36   9%      2  114   19    3  556%
c i   39.1   62414   397816     20852   15044   1539 56119   13   142   36   9%      2  114   19    3  554%
c i   39.2   62413   397816     20979   15154   1546 56121   14   142   36  10%      2  114   24    3  683%
c i   39.4   62405   397816     21178   15320   1562 56136   14   145   36  10%      2  116   20    4  557%
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   39.4   62397   397816     21179   15320   1562 56136   14   145   36  10%      2  116   20    4  555%
c i   39.7   62396   397816     21493   15592   1574 56152   15   147   36  10%      2  118   23    4  632%
c i   39.8   62393   397816     21634   15697   1584 56167   15   146   36  10%      2  116   30    4  802%
c i   39.8   62392   397816     21635   15697   1584 56167   15   146   36  10%      2  116   29    4  799%
c i   39.8   62391   397816     21668   15725   1586 56167   15   146   36  11%      2  116   29    4  786%
c i   39.9   62385   397816     21791   15834   1589 56173   16   145   36  11%      1  115   29    4  779%
c i   39.9   62383   397816     21879   15905   1599 56179   16   144   36  11%      1  114   23    4  611%
c i   40.0   62368   397816     21972   15992   1600 56180   16   145   36  11%      1  115   23    4  599%
c 
c [simplification-10] limit of 280 iterations hit after 280 iterations
c [quatres-5] found 30173 quaternary clauses 50% in total
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [quatres-5-2] added 1 quaternary resolvents
c [ternres-6] limit 4920183 with penalty 0 = 0 + 0
c [ternres-6] 31013 schedulable variables 48%
c [ternres-6] 62 ternary resolvents (1 bin, 61 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 307511 penalty 3 = 3 + 0
c [card-4] found 1572 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 307511 for elimination
c [card-4] 1572 out of 1572 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 321 xors of average arity 2.1
c [gauss-3] connected 688 occurrences of 379 variables (average 1.8)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [decomp-21] removed 529 variables
c [gauss-3] exported 2 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 3 variables
c [unhide-10] limit 984036 with penalty 0 = 0 + 0
c [unhide-10-10] 36 units, 670 failed, 5648 tauts, 0 hbrs, 24405 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 248 transitive binary clauses
c [transred-6] found 11 units
c [cce-3] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 4 clauses out of 549 (1%) of length 7
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 4 large clauses in 7500003 steps
c [cce-3-1] allowing another 3750001 steps for small clauses
c [cce-3-1] scheduling 296191 clauses = 190576 binary + 105615 ternary
c [cce-3-1] tried to eliminate 141 small clauses 0%
c [cce-3-1] eliminated 33 binary clauses 0%
c [cce-3-1] eliminated 21 ternary clauses 0%
c [cce-3-1] eliminated 54 small clauses 0%
c [cce-3-1] eliminated 9214 small clauses in 7500004 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 9218 covered clauses in round 1
c [cce-3] eliminated 9218 covered clauses in TOTAL during 1 rounds
c [bca-6] limit of 10000000 steps and 744950 added (scaled 2)
c [bca-6] 90190 out of 121394 literals actually usable 74%
c [bca-6] added 78 blocked clauses in 239388 steps
c [sweep-6] limit 1476055 penalty 0 = 0 + 0
c [sweep-6-1] 4546 pos 7.9% + 53007 neg 92.1% = 57553 sched 94.8% ret 3143
c [sweep-6-1] 1621902 steps 23 queries 12759.78 avg class size
c [sweep-6-1] 168 decisions 21 SAT calls 52.86 avg env size
c [sweep-6-1] 57462 variables remain 95% (3208 retained 5%)
c [decomp-23] removed 268 variables
c [sweep-6-1] removed 268 vars (0 failed, 3 eqs, 4 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 268 vars in TOTAL (1 rounds, 22 queries)
c [sort-queue-10] sorted 60428 enqueued variables after 21972 conflicts
c [score-dist-10] active 0 (0%), one 44669 (74%), zero 15759 (26%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 1940 variables 3.1% (60428 remain 28%)
c [simplification-10] removed 26848 irredundant clauses 6.7% (370968 remain 31%)
c [simplification-10] maximum reduction of 7% = max (3%, 7%)
c [simplification-10] forced so keeping old conflict interval 9000
c [simplification-10] conflict limit remains at 23284 (hard 33170)
c [simplification-10] new iteration 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   42.1   60427   370968     21994   15846   1565 48064   16   145   36  11%      1  115   22    4  576%
c i   42.2   60423   370968     22096   15933   1569 48073   16   148   37  11%      1  117   18    4  477%
c i   42.3   60418   370968     22175   15991   1575 48084   16   147   37  11%      1  117   16    4  421%
c i   42.3   60412   370968     22185   15998   1575 48084   16   147   37  11%      1  117   19    4  504%
c i   42.4   60410   370968     22293   16091   1579 48091   16   147   37  11%      1  117   22    4  562%
c i   42.4   60407   370968     22300   16096   1579 48092   16   147   37  11%      1  116   21    4  550%
c i   42.5   60398   370968     22380   16160   1581 48097   17   147   37  11%      1  116   27    4  699%
c i   42.5   60397   370968     22421   16197   1582 48098   17   149   37  11%      1  118   29    4  730%
c i   42.6   60396   370968     22476   16248   1582 48099   17   148   37  12%      1  117   32    4  809%
c i   42.6   60391   370968     22564   16323   1585 48108   17   148   37  11%      1  117   27    4  670%
c i   42.7   60372   370968     22635   16381   1589 48115   17   149   37  11%      1  118   24    4  595%
c i   42.9   60369   370968     22900   16615   1602 48122   17   150   37  12%      1  118   26    4  632%
c i   43.0   60366   370968     23011   16719   1605 48122   18   151   37  12%      1  119   24    4  579%
c i   43.0   60363   370968     23012   16719   1605 48122   18   151   37  12%      1  119   24    4  577%
c i   43.1   60362   370968     23034   16739   1606 48122   18   152   37  12%      1  120   24    4  578%
c i   43.1   60354   370968     23133   16815   1613 48133   17   153   37  11%      1  121   20    4  482%
c 
c [simplification-11] limit 23296 conflicts (hard 33170) hit after 23296 conflicts
c [quatres-6] found 32733 quaternary clauses 53% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [ternres-7] limit 5255803 with penalty 0 = 0 + 0
c [ternres-7] all 60345 free variables schedulable
c [ternres-7] 21 ternary resolvents (0 bin, 21 trn)
c [ternres-7] 14974 variables remain 25% (45371 retained 75%)
c [decomp-24] removed 104 variables
c [simpleprobe-4] 5022 schedulable variables 8%
c [simpleprobe-4] limit 5255803 penalty 2 = 2 + 0
c [decomp-25] removed 82 variables
c [simpleprobe-4] 3748 variables remain 6% (56494 retained 94%)
c [simpleprobe-4] removed 82 variables, found 7697 hbrs, 27 units
c [unhide-11] limit 1051160 with penalty 0 = 0 + 0
c [unhide-11-11] 15 units, 147 failed, 5951 tauts, 0 hbrs, 15677 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 396 transitive binary clauses
c [transred-7] found 9 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 59960 variables 100%
c [block-4] limit of 13139508 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 277 blocked clauses
c [block-4] 277 < 1/100 * 364144 = 3641 considered unsuccessful
c [bca-7] limit of 10000000 steps and 724495 added (scaled 2)
c [bca-7] 88428 out of 119882 literals actually usable 74%
c [bca-7] added 24 blocked clauses in 234451 steps
c [sweep-7] limit 1576741 penalty 0 = 0 + 0
c [sweep-7-1] 4374 pos 7.7% + 52419 neg 92.3% = 56793 sched 94.7% ret 3147
c [sweep-7-1] 1652953 steps 36 queries 8435.28 avg class size
c [sweep-7-1] 184 decisions 30 SAT calls 50.47 avg env size
c [sweep-7-1] 56535 variables remain 94% (3405 retained 6%)
c [decomp-26] removed 111 variables
c [sweep-7-1] removed 111 vars (0 failed, 6 eqs, 11 impls)
c [sweep-7] removed 111 vars in TOTAL (1 rounds, 35 queries)
c [sort-queue-11] sorted 59829 enqueued variables after 23296 conflicts
c [score-dist-11] active 0 (0%), one 44630 (75%), zero 15199 (25%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 516 variables 0.9% (59829 remain 28%)
c [simplification-11] removed 9540 irredundant clauses 2.6% (361428 remain 30%)
c [simplification-11] maximum reduction of 3% = max (1%, 3%)
c [simplification-11] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-11] new conflict interval 14000
c [simplification-11] penalized conflict interval 14000 = 1 * 14000
c [simplification-11] hard conflict limit 47296 (soft 37296 + delta 10000)
c [simplification-11] new conflict limit 37296 (hard 47296)
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.3   59828   361428     23415   16981   1698 56496   17   152   37  11%      1  119   15    4  356%
c i   45.4   59774   361428     23460   17019   1700 56500   17   151   37  11%      1  118   13    4  323%
c i   45.4   59773   361428     23472   17029   1700 56501   17   151   37  11%      1  118   13    4  317%
c i   45.4   59764   361428     23473   17029   1700 56501   17   151   37  11%      1  118   13    4  316%
c i   45.4   59754   361428     23474   17029   1700 56501   17   151   37  11%      1  118   13    4  314%
c i   45.4   59748   361428     23484   17034   1702 56503   17   150   37  11%      1  118   13    4  305%
c i   45.5   59722   361428     23646   17177   1709 56507   17   149   38  12%      1  116   19    4  454%
c i   45.6   59717   361428     23755   17266   1715 56512   18   150   38  12%      1  117   21    4  497%
c i   45.8   59716   361428     23903   17388   1722 56527   18   151   38  12%      1  117   20    4  469%
c i   45.9   59708   361428     24025   17496   1724 56537   17   151   38  12%      1  117   17    4  403%
c i   45.9   59707   361428     24041   17507   1726 56538   17   151   38  12%      1  117   17    4  386%
c i   46.0   59699   361428     24113   17569   1730 56542   17   152   38  11%      1  118   17    4  400%
c i   46.0   59694   361428     24119   17572   1730 56544   17   152   38  11%      1  118   17    4  392%
c i   46.0   59693   361428     24127   17572   1732 56547   17   151   38  11%      1  117   16    4  383%
c i   46.2   59645   361428     24254   17678   1743 56554   17   153   38  11%      1  119   18    4  406%
c i   46.2   59642   361428     24255   17678   1743 56554   17   153   38  11%      1  119   17    4  404%
c i   46.2   59635   361428     24256   17678   1743 56554   17   153   38  11%      1  119   17    4  402%
c i   46.2   59629   361428     24303   17721   1745 56554   17   153   38  11%      1  119   19    4  428%
c i   46.2   59625   361428     24304   17721   1745 56554   17   153   38  11%      1  119   19    4  427%
c i   46.2   59624   361428     24305   17721   1745 56554   17   153   38  11%      1  119   18    4  425%
c i   46.3   59619   361428     24462   17866   1748 56558   18   153   38  12%      1  118   20    4  450%
c i   46.4   59615   361428     24623   18017   1751 56562   18   152   38  12%      1  117   24    4  551%
c i   46.4   59608   361428     24626   18017   1751 56564   18   152   38  12%      1  117   24    4  544%
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   46.4   59570   361428     24644   18029   1752 56568   18   151   38  12%      1  116   23    4  522%
c i   46.4   59562   361428     24645   18029   1752 56568   18   151   38  12%      1  116   23    4  520%
c i   46.4   59553   361428     24656   18034   1752 56573   18   151   38  12%      1  116   22    4  504%
c i   46.5   59548   361428     24685   18057   1754 56576   18   152   38  12%      1  117   21    4  462%
c i   46.5   59544   361428     24697   18066   1755 56577   18   152   38  12%      1  117   20    4  450%
c i   46.5   59531   361428     24707   18072   1755 56580   18   152   38  12%      1  117   20    4  453%
c i   46.5   59525   361428     24743   18106   1755 56581   18   152   38  12%      1  117   20    4  444%
c i   46.6   59506   361428     24834   18186   1760 56585   18   154   38  12%      1  118   26    5  582%
c i   46.7   59499   361428     24940   18279   1763 56592   18   156   38  12%      1  120   22    5  494%
c i   46.8   59491   361428     24971   18304   1765 56595   18   156   38  12%      0  120   22    5  487%
c i   47.0   59489   361428     25292   18581   1785 56609   18   158   38  12%      1  122   20    5  430%
c i   47.1   59482   361428     25336   18620   1787 56609   18   160   38  12%      1  124   21    5  462%
c i   47.3   59475   361428     25504   18776   1792 56612   19   164   38  11%      1  127   21    5  446%
c i   47.4   59464   361428     25663   18907   1799 56627   18   163   38  11%      1  126   19    5  406%
c i   47.5   59460   361428     25710   18950   1801 56628   18   163   38  11%      1  126   19    5  403%
c i   47.5   59454   361428     25711   18950   1801 56628   18   163   38  11%      1  126   19    5  401%
c i   47.5   59448   361428     25771   19006   1801 56630   18   163   38  11%      1  126   19    5  401%
c i   47.5   59447   361428     25792   19024   1801 56631   18   164   38  11%      1  127   19    5  399%
c i   47.6   59323   361428     25905   19125   1806 56636   19   165   38  11%      1  128   22    5  458%
c i   47.8   59317   361428     26126   19325   1811 56644   19   162   38  12%      1  124   21    5  431%
c i   47.8   59307   361428     26127   19325   1811 56644   19   162   38  12%      1  124   21    5  430%
c i   47.8   59297   361428     26128   19325   1811 56644   19   162   38  12%      1  124   21    5  428%
c i   47.8   59288   361428     26129   19325   1811 56644   19   162   38  12%      1  124   20    5  426%
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   47.8   59284   361428     26130   19325   1811 56644   19   162   38  12%      1  124   20    5  425%
c i   47.9   59275   361428     26208   19395   1814 56646   19   164   38  12%      1  126   25    5  520%
c i   47.9   59271   361428     26209   19395   1814 56646   19   164   38  12%      1  126   25    5  518%
c i   48.0   59268   361428     26303   19476   1819 56652   19   165   38  12%      1  127   26    5  541%
c i   48.1   59266   361428     26351   19514   1822 56658   19   165   38  12%      1  127   24    5  495%
c i   48.2   59265   361428     26479   19621   1828 56669   20   166   38  12%      1  128   26    5  527%
c i   48.3   59261   361428     26521   19652   1830 56676   20   167   38  12%      1  128   25    5  516%
c i   48.3   59212   361428     26532   19657   1831 56680   20   166   38  12%      1  128   25    5  497%
c i   48.3   59211   361428     26533   19657   1831 56680   20   166   38  12%      1  128   24    5  496%
c i   48.3   59206   361428     26566   19687   1831 56680   20   167   38  12%      1  128   27    5  554%
c i   48.4   59205   361428     26708   19816   1835 56687   20   164   38  12%      1  125   24    5  479%
c i   48.9   59204   361428     27156   20202   1857 56715   20   165   38  12%      2  126   24    5  475%
c i   49.0   59187   361428     27228   20263   1860 56721   20   167   38  12%      1  127   26    5  497%
c i   49.1   59180   361428     27337   20356   1862 56729   21   170   38  12%      1  130   28    5  544%
c i   49.2   59173   361428     27379   20397   1862 56729   21   172   38  12%      1  131   31    5  594%
c i   49.2   59167   361428     27399   20410   1862 56730   21   172   38  12%      1  132   33    5  630%
c i   49.2   59158   361428     27400   20410   1862 56730   21   172   38  12%      1  132   33    5  628%
c i   49.4   59145   361428     27607   20587   1870 56743   21   173   38  12%      1  133   26    5  500%
c i   49.4   59142   361428     27608   20587   1870 56743   21   173   38  12%      1  133   26    5  499%
c i   49.4   59137   361428     27611   20589   1870 56743   21   173   38  12%      1  133   26    5  499%
c i   49.4   59136   361428     27621   20597   1870 56744   21   173   38  12%      1  133   27    5  505%
c i   49.4   59121   361428     27622   20597   1870 56744   21   173   38  12%      1  133   27    5  503%
c i   49.5   59104   361428     27699   20667   1872 56746   21   174   38  12%      1  133   26    5  481%
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   49.5   59103   361428     27703   20670   1872 56746   21   174   38  12%      1  133   26    5  482%
c i   49.5   59091   361428     27717   20679   1872 56750   21   173   38  12%      1  133   25    5  463%
c i   49.6   59087   361428     27780   20734   1873 56756   21   173   38  12%      1  132   23    5  430%
c i   49.7   59076   361428     27898   20832   1875 56764   21   173   38  12%      1  131   26    5  482%
c i   49.7   59065   361428     27899   20832   1875 56764   21   173   38  12%      1  131   26    5  480%
c i   49.8   59064   361428     27967   20889   1879 56768   22   176   38  12%      1  134   31    5  568%
c i   49.8   59056   361428     27987   20906   1879 56770   22   175   38  12%      1  134   30    5  549%
c i   49.8   59054   361428     27988   20906   1879 56770   22   175   38  12%      1  134   30    5  547%
c i   49.8   59053   361428     28011   20928   1879 56770   22   175   38  13%      1  134   32    5  583%
c i   49.9   59015   361428     28082   20990   1883 56774   22   176   38  13%      1  134   30    5  544%
c i   50.0   59010   361428     28189   21084   1886 56780   22   176   38  13%      1  135   29    5  532%
c i   50.0   59007   361428     28190   21084   1886 56780   22   176   38  13%      1  134   29    5  530%
c i   50.1   59003   361428     28305   21193   1891 56780   22   176   38  13%      1  134   26    6  473%
c i   50.2   59002   361428     28387   21267   1892 56782   22   176   38  13%      1  134   25    6  450%
c i   50.3   58997   361428     28453   21328   1893 56784   22   178   38  12%      1  135   25    6  454%
c i   50.5   58996   361428     28688   21540   1899 56794   23   180   38  13%      1  138   29    6  518%
c i   50.7   58994   361428     28903   21728   1909 56806   23   181   38  13%      1  138   29    6  503%
c i   50.7   58986   361428     28909   21731   1909 56808   23   181   38  13%      1  138   29    6  503%
c i   50.8   58980   361428     28985   21795   1914 56814   23   180   38  13%      1  137   26    6  456%
c i   50.8   58968   361428     28986   21795   1914 56814   23   180   38  13%      1  137   26    6  454%
c i   50.8   58964   361428     29009   21817   1914 56814   23   180   38  13%      1  136   27    6  471%
c i   50.9   58963   361428     29064   21865   1917 56816   23   180   38  13%      1  137   27    6  477%
c i   50.9   58954   361428     29065   21865   1917 56816   23   180   38  13%      1  137   27    6  475%
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   51.0   58937   361428     29275   22048   1926 56823   23   182   38  13%      1  138   24    6  412%
c i   51.0   58935   361428     29276   22048   1926 56823   23   182   38  13%      1  138   24    6  410%
c i   51.3   58928   361428     29499   22250   1936 56831   23   182   38  12%      1  137   20    6  345%
c i   51.3   58927   361428     29510   22258   1936 56831   23   182   38  12%      1  137   20    6  339%
c i   51.4   58923   361428     29636   22372   1940 56834   23   184   38  12%      1  139   25    6  421%
c i   51.5   58922   361428     29662   22395   1940 56835   23   184   38  12%      1  140   25    6  415%
c i   51.5   58918   361428     29664   22396   1940 56835   23   184   38  12%      1  140   25    6  422%
c i   51.5   58909   361428     29666   22397   1940 56835   23   184   38  12%      1  140   25    6  419%
c i   51.5   58898   361428     29694   22421   1940 56837   23   184   38  12%      1  140   26    6  435%
c i   51.7   58897   361428     29842   22550   1947 56847   23   184   38  12%      1  139   24    6  402%
c i   51.8   58873   361428     29881   22586   1947 56848   23   184   38  12%      1  139   25    6  414%
c i   51.8   58871   361428     29882   22586   1947 56848   23   184   38  12%      1  139   25    6  412%
c i   51.9   58867   361428     29984   22677   1949 56853   23   185   39  13%      1  139   29    6  480%
c i   52.0   58859   361428     30056   22736   1952 56860   23   186   39  13%      1  140   29    6  472%
c i   52.2   58848   361428     30279   22937   1960 56869   23   186   39  13%      1  140   24    6  397%
c i   52.3   58824   361428     30386   23027   1964 56880   23   186   39  13%      1  140   24    6  391%
c i   52.8   58823   361428     30919   23513   1982 56900   24   186   39  13%      2  138   27    6  433%
c i   52.8   58818   361428     30921   23514   1982 56900   24   186   39  13%      2  138   27    6  430%
c i   53.0   58807   361428     31066   23650   1983 56903   24   189   39  13%      2  141   36    6  571%
c i   53.1   58806   361428     31124   23705   1983 56904   24   188   39  13%      2  140   33    6  514%
c i   53.1   58805   361428     31170   23747   1983 56905   24   188   40  13%      2  140   31    6  489%
c i   53.1   58804   361428     31186   23760   1984 56905   25   188   40  13%      2  140   33    6  510%
c i   53.7   58800   361428     31749   24257   2008 56935   25   192   40  13%      3  143   28    7  430%
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   53.9   58789   361428     31926   24421   2011 56939   25   194   41  13%      2  144   32    7  485%
c i   53.9   58785   361428     31938   24429   2012 56940   25   194   41  13%      2  144   32    7  473%
c i   53.9   58783   361428     31939   24429   2012 56940   25   194   41  13%      2  144   31    7  471%
c i   53.9   58770   361428     31940   24429   2012 56940   25   194   41  13%      2  144   31    7  469%
c i   54.0   58760   361428     31989   24472   2014 56943   25   194   41  13%      2  144   29    7  438%
c i   54.0   58759   361428     31995   24476   2015 56943   25   194   41  13%      2  144   29    7  433%
c i   54.1   58754   361428     32131   24593   2022 56952   26   194   41  13%      2  144   33    7  490%
c i   54.4   58753   361428     32456   24870   2031 56958   28   189   41  15%      2  138   45    7  643%
c i   54.6   58752   361428     32628   25025   2037 56964   28   188   41  15%      2  137   44    7  620%
c i   54.6   58687   361428     32629   25025   2037 56964   28   188   41  15%      2  137   44    7  618%
c i   54.6   58684   361428     32665   25057   2040 56964   28   188   41  15%      2  137   41    7  583%
c i   54.7   58681   361428     32691   25081   2039 56965   28   188   41  15%      2  137   38    7  542%
c i   54.7   58664   361428     32742   25126   2041 56967   28   188   41  15%      2  137   35    7  499%
c i   55.4   58653   361428     33366   25685   2057 56994   29   186   41  15%      3  134   37    7  503%
c i   55.5   58652   361428     33479   25774   2069 57003   28   185   41  15%      3  132   29    7  395%
c i   56.0   58644   361428     33941   26179   2087 57024   29   190   42  15%      3  136   34    8  447%
c i   56.2   58643   361428     34125   26341   2094 57032   29   192   42  15%      3  138   34    8  440%
c i   56.5   58631   361428     34415   26604   2100 57041   30   192   42  15%      2  137   34    8  441%
c i   56.7   58624   361428     34588   26764   2102 57041   30   189   42  16%      2  134   33    8  422%
c i   56.7   58621   361428     34626   26799   2103 57042   30   189   44  16%      2  134   32    8  414%
c i   56.9   58620   361428     34796   26953   2113 57044   29   189   44  16%      2  134   29    8  368%
c i   57.0   58619   361428     34872   27016   2116 57047   30   190   44  16%      2  134   33    8  417%
c i   57.0   58612   361428     34875   27018   2116 57047   30   190   44  16%      2  134   33    8  412%
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   57.3   58611   361428     35195   27314   2121 57057   31   193   44  16%      2  136   39    8  485%
c i   57.9   58607   361428     35685   27755   2142 57067   31   187   44  16%      2  130   29    8  357%
c i   58.0   58606   361428     35755   27820   2143 57069   31   190   44  16%      2  133   30    8  360%
c i   58.0   58599   361428     35798   27852   2145 57076   31   190   44  16%      2  132   27    8  324%
c i   58.5   58598   361428     36145   28163   2158 57089   32   193   45  16%      2  135   44    8  515%
c i   58.5   58588   361428     36177   28193   2158 57090   32   194   45  16%      2  136   46    8  541%
c i   58.5   58586   361428     36185   28198   2158 57092   32   194   45  16%      2  136   45    8  528%
c i   58.6   58572   361428     36285   28293   2158 57094   32   193   45  17%      2  134   44    9  512%
c i   58.6   58568   361428     36288   28294   2159 57094   32   192   45  17%      2  134   43    9  507%
c i   58.7   58563   361428     36307   28311   2159 57094   32   192   45  17%      2  133   43    9  498%
c i   58.7   58555   361428     36312   28312   2159 57097   32   192   45  17%      2  133   42    9  489%
c i   58.7   58548   361428     36318   28314   2160 57099   32   191   45  17%      2  133   41    9  478%
c i   58.7   58530   361428     36326   28321   2160 57099   32   191   45  17%      2  132   40    9  466%
c i   59.0   58527   361428     36666   28641   2166 57108   33   191   46  17%      2  132   48    9  553%
c i   59.0   58517   361428     36668   28642   2166 57108   33   191   46  17%      2  132   49    9  558%
c i   59.1   58510   361428     36694   28666   2166 57108   33   191   46  17%      2  131   46    9  524%
c i   59.2   58509   361428     36785   28745   2168 57114   33   190   46  17%      2  130   39    9  452%
c i   59.2   58502   361428     36824   28780   2169 57116   33   190   46  17%      1  130   37    9  426%
c i   59.3   58471   361428     36901   28845   2171 57119   33   190   46  18%      1  130   46    9  520%
c i   59.7   58462   361428     37221   29133   2179 57133   33   191   46  17%      1  131   37    9  414%
c i   59.9   58447   361428     37365   29267   2183 57133   35   193   46  18%      1  132   52    9  577%
c i   59.9   58443   361428     37367   29268   2183 57133   35   193   46  18%      1  132   52    9  575%
c i   60.1   58441   361428     37531   29413   2187 57139   35   193   46  18%      1  132   51    9  556%
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   60.1   58435   361428     37532   29413   2187 57139   35   193   46  18%      1  132   51    9  554%
c 
c [simplification-12] limit 37627 conflicts (hard 47296) hit after 37627 conflicts
c [ternres-8] limit 9455639 with penalty 0 = 0 + 0
c [ternres-8] 14514 schedulable variables 24%
c [ternres-8] 19 ternary resolvents (0 bin, 19 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] extracted 325 xors of average arity 2.3
c [gauss-4] connected 763 occurrences of 602 variables (average 1.3)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [decomp-27] removed 217 variables
c [gauss-4] exported 0 unary, 2 binary and 0 ternary equations
c [treelook-4] limit 945563 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 95421 literals 82%
c [treelook-4] scheduling used 945570 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 945563 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 949794 steps
c [treelook-4] 95405 literals remain 82%
c [treelook-4] 27405 variables remain to probed next time 47%
c [treelook-4] removed 5 variables, found 6603 hbrs
c [unhide-12] limit 1891127 with penalty 0 = 0 + 0
c [unhide-12-12] 31 units, 434 failed, 6606 tauts, 0 hbrs, 80352 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 399 transitive binary clauses
c [transred-8] found 5 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 236390990 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 30 clauses out of 1204 (2%) of length 6
c [cce-4-1] eliminated 14352 clauses out of 20778 (69%) of length 5
c [cce-4-1] eliminated 9359 clauses out of 27877 (34%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 23741 large clauses in 236390990 steps
c [cce-4-1] allowing another 118195495 steps for small clauses
c [cce-4-1] scheduling 196471 clauses = 178239 binary + 18232 ternary
c [cce-4-1] tried to eliminate 9606 small clauses 5%
c [cce-4-1] eliminated 2493 binary clauses 1%
c [cce-4-1] eliminated 475 ternary clauses 3%
c [cce-4-1] eliminated 2968 small clauses 2%
c [cce-4-1] eliminated 8055 small clauses in 236390991 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 31796 covered clauses in round 1
c [cce-4] eliminated 31796 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 57525 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 945563960 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 16243 variables 28% in round 1 in 27928300 steps
c [elim-8-1] backward subsumption/strengthening limit 27928300
c [elim-8-1-1] backward checking 34184 touched variables 59%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 98 and strengthened 534 clauses in 5074858 steps
c [elim-8-1] rescheduled 1478 variables 3% by backward subsumption
c [elim-8-2] eliminated 114 variables 0% in round 2 in 2921898 steps
c [elim-8-2] backward subsumption/strengthening limit 2921800
c [elim-8-2-1] backward checking 1098 touched variables 2%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 94 and strengthened 65 clauses in 1062633 steps
c [elim-8-2] rescheduled 427 variables 1% by backward subsumption
c [elim-8-3] eliminated 26 variables 0% in round 3 in 2407658 steps
c [elim-8-3] backward subsumption/strengthening limit 2407600
c [elim-8-3-1] backward checking 234 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 11 and strengthened 6 clauses in 427407 steps
c [elim-8] incomplete 35 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 16449 = 29% variables out of 57525 scheduled
c [bca-8] limit of 10000000 steps and 558467 added (scaled 2)
c [bca-8] 70003 out of 82154 literals actually usable 85%
c [bca-8] added 153 blocked clauses in 168020 steps
c [sweep-8] limit 2836691 penalty 0 = 0 + 0
c [sweep-8-1] 3638 pos 9.4% + 35003 neg 90.6% = 38641 sched 94.1% ret 2435
c [sweep-8-1] 2862136 steps 65 queries 5519.68 avg class size
c [sweep-8-1] 568 decisions 51 SAT calls 57.84 avg env size
c [sweep-8-1] 38236 variables remain 93% (2840 retained 7%)
c [decomp-30] removed 70 variables
c [sweep-8-1] removed 70 vars (0 failed, 13 eqs, 21 impls)
c [sweep-8] removed 70 vars in TOTAL (1 rounds, 64 queries)
c [sort-queue-12] sorted 41006 enqueued variables after 37627 conflicts
c [score-dist-12] active 0 (0%), one 31040 (76%), zero 9966 (24%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 17423 variables 29.8% (41006 remain 19%)
c [simplification-12] removed 82832 irredundant clauses 22.9% (278596 remain 23%)
c [simplification-12] maximum reduction of 30% = max (30%, 23%)
c [simplification-12] large reduction 30% >= 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 49627 (soft 39627 + delta 10000)
c [simplification-12] new conflict limit 39627 (hard 49627)
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.7   41005   278596     37672    5279   1870 43199   35   192   27  18%      1  131   40    9  437%
c i   71.1   41004   278596     38636    6106   1928 43249   30   178   27  17%      5  115   10    9  108%
c i   71.2   41002   278596     38746    6207   1931 43252   29   179   27  16%      5  115   11    9  115%
c i   71.2   40997   278596     38902    6330   1944 43269   29   177   27  16%      4  113   11    9  117%
c 
c [simplification-13] limit 39627 conflicts (hard 49627) hit after 39627 conflicts
c [quatres-7] found 26436 quaternary clauses 70% in total
c [quatres-7-1] removed 9 duplicate quaternary clauses
c [quatres-7-2] added 6 single-self-subsuming ternary resolvents
c [quatres-7-2] added 38 quaternary resolvents
c [ternres-9] limit 9752784 with penalty 0 = 0 + 0
c [ternres-9] all 40997 free variables schedulable
c [ternres-9] 2057 ternary resolvents (6 bin, 2051 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-5] limit 2000000 penalty 0 = 0 + 0
c [gauss-5] extracted 61 xors of average arity 2.9
c [gauss-5] connected 179 occurrences of 168 variables (average 1.1)
c [gauss-5] limit 2000000 penalty 0 = 0 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-31] removed 3 variables
c [basicprobe-4] limit 48763923 penalty 0 = 0 + 0
c [basicprobe-4-0] 10547 probes remain 26% after last round
c [basicprobe-4-0] 720 units = 635 failed (88%) + 85 lifted (12%)
c [basicprobe-4-0] removed 1026 variables, found 95832 hbrs
c [bate-2] eliminated 854 asymmetric tautologies during probing
c [unhide-13] limit 1950556 with penalty 0 = 0 + 0
c [unhide-13-14] 64 units, 457 failed, 18668 tauts, 0 hbrs, 8176 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 459 transitive binary clauses
c [transred-9] found 3 units
c [cce-5] limit of 48763923 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 25
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 24
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 23
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 22
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 21
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 20
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 19
c [cce-5-1] eliminated 2 clauses out of 5 (40%) of length 18
c [cce-5-1] eliminated 6 clauses out of 6 (100%) of length 17
c [cce-5-1] eliminated 3 clauses out of 7 (43%) of length 16
c [cce-5-1] eliminated 7 clauses out of 8 (88%) of length 15
c [cce-5-1] eliminated 7 clauses out of 10 (70%) of length 14
c [cce-5-1] eliminated 9 clauses out of 10 (90%) of length 13
c [cce-5-1] eliminated 6 clauses out of 10 (60%) of length 12
c [cce-5-1] eliminated 10 clauses out of 11 (91%) of length 11
c [cce-5-1] eliminated 6 clauses out of 11 (55%) of length 10
c [cce-5-1] eliminated 9 clauses out of 10 (90%) of length 9
c [cce-5-1] eliminated 6 clauses out of 12 (50%) of length 8
c [cce-5-1] eliminated 10 clauses out of 34 (29%) of length 7
c [cce-5-1] eliminated 45 clauses out of 953 (5%) of length 6
c [cce-5-1] eliminated 208 clauses out of 6959 (3%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 356 large clauses in 48763937 steps
c [cce-5-1] allowing another 24381968 steps for small clauses
c [cce-5-1] scheduling 139301 clauses = 124942 binary + 14359 ternary
c [cce-5-1] tried to eliminate 2617 small clauses 2%
c [cce-5-1] eliminated 745 binary clauses 1%
c [cce-5-1] eliminated 101 ternary clauses 1%
c [cce-5-1] eliminated 846 small clauses 1%
c [cce-5-1] eliminated 4503 small clauses in 48763923 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 4859 covered clauses in round 1
c [cce-5] eliminated 4859 covered clauses in TOTAL during 1 rounds
c [bca-9] limit of 10000000 steps and 510888 added (scaled 2)
c [bca-9] 63987 out of 78670 literals actually usable 81%
c [bca-9] added 50 blocked clauses in 152598 steps
c [sweep-9] limit 2925835 penalty 0 = 0 + 0
c [sweep-9-1] 4325 pos 11.7% + 32548 neg 88.3% = 36873 sched 93.7% ret 2461
c [sweep-9-1] 2992584 steps 88 queries 4550.84 avg class size
c [sweep-9-1] 1120 decisions 84 SAT calls 53.92 avg env size
c [sweep-9-1] 35932 variables remain 92% (3326 retained 8%)
c [decomp-32] removed 240 variables
c [sweep-9-1] removed 240 vars (0 failed, 6 eqs, 8 impls)
c [sweep-9] removed 240 vars in TOTAL (1 rounds, 87 queries)
c [sort-queue-13] sorted 39094 enqueued variables after 39627 conflicts
c [score-dist-13] active 0 (0%), one 30502 (78%), zero 8592 (22%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 1903 variables 4.6% (39094 remain 18%)
c [simplification-13] removed 24697 irredundant clauses 8.9% (253899 remain 21%)
c [simplification-13] maximum reduction of 9% = max (5%, 9%)
c [simplification-13] large reduction 9% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 51627 (soft 41627 + delta 10000)
c [simplification-13] new conflict limit 41627 (hard 51627)
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   75.7   39093   253899     40063    7269   3861 114568   24   185   28  13%      8  119   10    9  106%
c i   75.9   39091   253899     40476    7641   3873 114583   23   182   28  12%      6  116   11    9  119%
c i   76.0   39087   253899     40714    7828   3892 114600   22   181   28  12%      5  114   11    9  118%
c i   76.0   39085   253899     40742    7850   3893 114601   22   182   28  12%      5  115   12    9  125%
c i   76.0   39084   253899     40756    7860   3893 114603   22   181   28  12%      5  114   11    9  122%
c i   76.0   39083   253899     40757    7860   3893 114603   22   181   28  12%      5  114   11    9  121%
c i   76.0   39079   253899     40789    7884   3897 114606   22   180   28  12%      5  113   11    9  116%
c i   76.2   39078   253899     41134    8196   3911 114617   21   179   28  12%      4  111   12    9  124%
c i   76.2   39048   253899     41264    8311   3917 114620   21   179   28  12%      3  111   18    9  193%
c i   76.2   39047   253899     41265    8311   3917 114620   21   179   28  12%      3  111   18    9  192%
c i   76.2   39045   253899     41266    8311   3917 114620   21   179   28  12%      3  111   18    9  192%
c i   76.2   39044   253899     41279    8320   3920 114620   21   178   28  12%      3  110   17    9  184%
c i   76.3   39034   253899     41346    8378   3921 114622   21   178   28  12%      3  110   16    9  177%
c i   76.3   39033   253899     41347    8378   3921 114622   21   178   28  12%      3  110   16    9  176%
c 
c [simplification-14] limit 41667 conflicts (hard 51627) hit after 41667 conflicts
c [quatres-8] found 23795 quaternary clauses 69% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 6 single-self-subsuming ternary resolvents
c [quatres-8-2] added 7 quaternary resolvents
c [ternres-10] limit 10052512 with penalty 0 = 0 + 0
c [ternres-10] all 39032 free variables schedulable
c [ternres-10] 716 ternary resolvents (1 bin, 715 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-33] removed 81 variables
c [unhide-14] limit 2010502 with penalty 0 = 0 + 0
c [unhide-14-16] 13 units, 206 failed, 9248 tauts, 0 hbrs, 10308 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 341 transitive binary clauses
c [cce-6] limit of 50262564 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 26 clauses out of 6549 (0%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 26 large clauses in 50262572 steps
c [cce-6-1] allowing another 25131286 steps for small clauses
c [cce-6-1] scheduling 133975 clauses = 119927 binary + 14048 ternary
c [cce-6-1] tried to eliminate 2686 small clauses 2%
c [cce-6-1] eliminated 675 binary clauses 1%
c [cce-6-1] eliminated 95 ternary clauses 1%
c [cce-6-1] eliminated 770 small clauses 1%
c [cce-6-1] eliminated 1357 small clauses in 50262569 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 1383 covered clauses in round 1
c [cce-6] eliminated 1383 covered clauses in TOTAL during 1 rounds
c [cce-6] 1383 < 1/100 * 247466 = 2474 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 38686 variables 100%
c [elim-9] limit of 100525129 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1701 variables 4% in round 1 in 21304308 steps
c [elim-9-1] backward subsumption/strengthening limit 21304300
c [elim-9-1-1] backward checking 8261 touched variables 21%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 55 and strengthened 261 clauses in 2163984 steps
c [elim-9-1] rescheduled 707 variables 2% by backward subsumption
c [elim-9-2] eliminated 53 variables 0% in round 2 in 1698548 steps
c [elim-9-2] backward subsumption/strengthening limit 1698500
c [elim-9-2-1] backward checking 508 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 21 and strengthened 20 clauses in 226977 steps
c [elim-9-2] rescheduled 82 variables 0% by backward subsumption
c [elim-9-3] eliminated 10 variables 0% in round 3 in 82481 steps
c [elim-9-3] backward subsumption/strengthening limit 82400
c [elim-9-3-1] backward checking 66 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 1 and strengthened 9 clauses in 82401 steps
c [elim-9] incomplete 20 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 1769 = 5% variables out of 38686 scheduled
c [bca-10] limit of 10000000 steps and 485489 added (scaled 2)
c [bca-10] 58428 out of 73836 literals actually usable 79%
c [bca-10] added 115 blocked clauses in 140854 steps
c [sweep-10] limit 3015753 penalty 0 = 0 + 0
c [sweep-10-1] 3428 pos 10.2% + 30329 neg 89.8% = 33757 sched 91.4% ret 3160
c [sweep-10-1] 3026233 steps 75 queries 4169.52 avg class size
c [sweep-10-1] 1019 decisions 69 SAT calls 52.25 avg env size
c [sweep-10-1] 32926 variables remain 89% (3980 retained 11%)
c [decomp-34] removed 26 variables
c [sweep-10-1] removed 26 vars (0 failed, 5 eqs, 12 impls)
c [sweep-10] 26 < 1/1000 * 36917 = 36 considered unsuccessful
c [sweep-10] removed 26 vars in TOTAL (1 rounds, 74 queries)
c [sort-queue-14] sorted 36891 enqueued variables after 41667 conflicts
c [score-dist-14] active 0 (0%), one 29160 (79%), zero 7731 (21%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 2141 variables 5.5% (36891 remain 17%)
c [simplification-14] removed 11829 irredundant clauses 4.7% (242070 remain 20%)
c [simplification-14] maximum reduction of 5% = max (5%, 5%)
c [simplification-14] large reduction 5% >= 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 53667 (soft 43667 + delta 10000)
c [simplification-14] new conflict limit 43667 (hard 53667)
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   80.3   36890   242070     42438    8654   3846 101049   19   170   27  11%      7  101   15    9  161%
c i   80.4   36888   242070     42510    8719   3848 101053   19   169   27  11%      6   99   16    9  173%
c i   80.4   36887   242070     42647    8841   3852 101061   19   169   27  11%      6   99   17    9  177%
c i   80.8   36886   242070     43371    9495   3877 101090   19   162   28  12%      5   91   15    9  159%
c i   80.8   36883   242070     43395    9509   3880 101095   19   162   28  12%      5   91   15    9  154%
c i   80.9   36877   242070     43475    9583   3882 101098   19   161   28  12%      5   90   17    9  178%
c i   81.0   36876   242070     43618    9705   3892 101108   18   159   28  12%      4   88   14    9  145%
c 
c [simplification-15] limit 43667 conflicts (hard 53667) hit after 43668 conflicts
c [quatres-9] found 22616 quaternary clauses 67% in total
c [quatres-9-2] added 3 single-self-subsuming ternary resolvents
c [quatres-9-2] added 43 quaternary resolvents
c [ternres-11] limit 10405533 with penalty 0 = 0 + 0
c [ternres-11] all 36875 free variables schedulable
c [ternres-11] 1476 ternary resolvents (0 bin, 1476 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 325172 penalty 4 = 4 + 0
c [card-5] found 1275 at-most-one constraints of average size 3.9
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 325172 for elimination
c [card-5] 1275 out of 1275 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-6] limit 1040553 penalty 1 = 1 + 0
c [gauss-6] extracted 56 xors of average arity 2.6
c [gauss-6] connected 145 occurrences of 81 variables (average 1.8)
c [gauss-6] limit 1040553 penalty 1 = 1 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-35] removed 26 variables
c [simpleprobe-5] 2943 schedulable variables 8%
c [simpleprobe-5] limit 20811066 penalty 1 = 1 + 0
c [decomp-36] removed 472 variables
c [simpleprobe-5] 2322 variables remain 6% (34055 retained 94%)
c [simpleprobe-5] removed 472 variables, found 44792 hbrs, 270 units
c [unhide-15] limit 2081106 with penalty 0 = 0 + 0
c [unhide-15-18] 5 units, 128 failed, 16291 tauts, 0 hbrs, 9612 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 540 transitive binary clauses
c [transred-11] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 36207 variables 100%
c [block-5] limit of 13006916 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 209 blocked clauses
c [block-5] 209 < 1/100 * 234111 = 2341 considered unsuccessful
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 36206 variables 100%
c [elim-10] limit of 208110666 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 536 variables 1% in round 1 in 19722893 steps
c [elim-10-1] backward subsumption/strengthening limit 19722800
c [elim-10-1-1] backward checking 3164 touched variables 9%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 15 and strengthened 71 clauses in 772260 steps
c [elim-10-1] rescheduled 214 variables 1% by backward subsumption
c [elim-10-2] eliminated 16 variables 0% in round 2 in 963665 steps
c [elim-10-2] backward subsumption/strengthening limit 963600
c [elim-10-2-1] backward checking 136 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 2 and strengthened 3 clauses in 64754 steps
c [elim-10-2] rescheduled 13 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 6938 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 555 = 2% variables out of 36206 scheduled
c [bca-11] limit of 10000000 steps and 464906 added (scaled 2)
c [bca-11] 54875 out of 71304 literals actually usable 77%
c [bca-11] added 31 blocked clauses in 134309 steps
c [sort-queue-15] sorted 35651 enqueued variables after 43668 conflicts
c [score-dist-15] active 0 (0%), one 28554 (80%), zero 7097 (20%)
c [score-dist-15] max exp 1, different 2 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 1224 variables 3.3% (35651 remain 17%)
c [simplification-15] removed 10128 irredundant clauses 4.2% (231942 remain 19%)
c [simplification-15] maximum reduction of 4% = max (3%, 4%)
c [simplification-15] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-15] new conflict interval 18000
c [simplification-15] penalized conflict interval 18000 = 1 * 18000
c [simplification-15] hard conflict limit 71668 (soft 61668 + delta 10000)
c [simplification-15] new conflict limit 61668 (hard 71668)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   83.5   35650   231942     43838    9654   4618 123884   18   155   28  12%      3   84   16   10  163%
c i   83.5   35647   231942     43930    9732   4622 123890   18   154   28  12%      3   82   15   10  155%
c i   83.6   35646   231942     44108    9896   4627 123894   18   153   28  12%      3   81   14   10  149%
c i   83.6   35645   231942     44116    9901   4629 123894   18   153   28  12%      3   81   14   10  146%
c i   83.7   35641   231942     44265   10039   4632 123898   18   151   28  12%      2   79   18   10  184%
c i   83.8   35639   231942     44465   10203   4640 123910   18   150   28  12%      2   77   15   10  160%
c i   83.9   35637   231942     44631   10360   4644 123912   18   148   28  12%      2   75   22   10  228%
c i   85.0   35636   231942     46644   12177   4726 123976   19   139   28  13%     17   64   19   10  195%
c i   85.1   35632   231942     46753   12276   4728 123981   18   139   28  13%     15   64   18   10  180%
c i   85.2   35631   231942     46872   12376   4735 123986   19   140   28  13%     13   65   20   10  206%
c i   85.2   35626   231942     46902   12401   4737 123988   19   139   28  13%     13   64   19   10  195%
c i   85.2   35622   231942     46940   12427   4743 123990   19   139   28  13%     12   63   18   10  177%
c i   85.4   35616   231942     47259   12701   4756 124010   18   136   29  13%      9   60   16   10  158%
c i   85.4   35576   231942     47363   12794   4758 124013   19   136   29  14%      8   61   23   10  232%
c i   86.0   35573   231942     48240   13580   4789 124050   19   133   29  14%      7   57   17   10  172%
c i   86.2   35572   231942     48609   13907   4796 124065   20   134   29  15%      5   58   23   10  225%
c i   86.2   35571   231942     48705   13992   4800 124068   19   134   29  14%      5   58   21   10  204%
c i   86.7   35563   231942     49358   14543   4828 124104   20   134   30  15%      4   57   22   10  212%
c i   86.9   35560   231942     49639   14797   4837 124112   20   132   30  15%      3   55   20   10  197%
c i   87.2   35553   231942     50139   15254   4858 124124   20   131   31  15%      3   53   24   10  226%
c i   87.3   35550   231942     50326   15418   4862 124136   21   132   31  16%      2   54   29   11  280%
c i   87.8   35549   231942     51111   16137   4881 124167   20   129   31  16%      4   50   20   11  189%
c i   88.2   35547   231942     51852   16790   4912 124191   20   127   31  16%      4   48   23   11  216%
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   88.7   35546   231942     52672   17522   4947 124220   20   128   31  16%      5   48   19   11  173%
c i   88.7   35517   231942     52757   17605   4947 124220   20   127   31  16%      4   47   18   11  167%
c i   88.8   35515   231942     52771   17617   4948 124220   20   127   31  16%      4   47   18   11  162%
c i   89.0   35513   231942     53082   17892   4963 124222   21   128   31  16%      3   48   25   11  231%
c i   90.7   35512   231942     56248   20793   5031 124298   23   127   33  18%     32   45   26   12  226%
c i   90.7   35437   231942     56263   20799   5036 124299   23   127   33  18%     31   44   25   12  214%
c i   90.7   35426   231942     56264   20799   5036 124299   23   127   33  18%     31   44   25   12  213%
c i   90.8   35176   231942     56495   21007   5040 124315   24   126   33  19%     25   44   39   12  331%
c i   90.8   35174   231942     56538   21048   5041 124315   24   125   33  19%     24   43   34   12  289%
c i   91.1   35173   231942     57044   21531   5050 124321   26   129   33  20%     15   47   44   12  368%
c i   92.3   35172   231942     59080   23410   5090 124353   26   126   36  21%     17   41   22   12  179%
c i   92.6   35169   231942     59625   23913   5094 124360   26   123   36  21%     11   39   20   12  160%
c i   92.7   35168   231942     59819   24089   5099 124362   26   122   36  21%      8   37   19   13  152%
c i   93.8   35167   231942     61626   25765   5134 124388   30   127   37  23%     13   42   30   13  226%
c 
c [simplification-16] limit 61679 conflicts (hard 71668) hit after 61679 conflicts
c [quatres-10] found 21532 quaternary clauses 62% in total
c [quatres-10-1] removed 1 duplicate quaternary clauses
c [quatres-10-2] added 9 single-self-subsuming ternary resolvents
c [quatres-10-2] added 16 quaternary resolvents
c [ternres-12] limit 13798229 with penalty 0 = 0 + 0
c [ternres-12] all 35165 free variables schedulable
c [ternres-12] 415 ternary resolvents (0 bin, 415 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-37] removed 529 variables
c [treelook-5] limit 1379822 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 55182 literals 79%
c [treelook-5] scheduling used 853277 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 1379822 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1433380 steps
c [treelook-5] 55101 literals remain 78%
c [treelook-5] 12935 variables remain to probed next time 37%
c [treelook-5] removed 21 variables, found 10420 hbrs
c [unhide-16] limit 2759645 with penalty 0 = 0 + 0
c [unhide-16-20] 7 units, 112 failed, 10367 tauts, 0 hbrs, 104306 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 371 transitive binary clauses
c [transred-12] found 2 units
c [cce-7] limit of 34495574 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 31
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 30
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 29
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 28
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 27
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 26
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 25
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 24
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 23
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 22
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 21
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 20
c [cce-7-1] eliminated 4 clauses out of 9 (44%) of length 19
c [cce-7-1] eliminated 7 clauses out of 9 (78%) of length 18
c [cce-7-1] eliminated 5 clauses out of 10 (50%) of length 17
c [cce-7-1] eliminated 7 clauses out of 10 (70%) of length 16
c [cce-7-1] eliminated 7 clauses out of 15 (47%) of length 15
c [cce-7-1] eliminated 10 clauses out of 15 (67%) of length 14
c [cce-7-1] eliminated 8 clauses out of 14 (57%) of length 13
c [cce-7-1] eliminated 12 clauses out of 19 (63%) of length 12
c [cce-7-1] eliminated 12 clauses out of 20 (60%) of length 11
c [cce-7-1] eliminated 17 clauses out of 29 (59%) of length 10
c [cce-7-1] eliminated 14 clauses out of 25 (56%) of length 9
c [cce-7-1] eliminated 20 clauses out of 30 (67%) of length 8
c [cce-7-1] eliminated 17 clauses out of 47 (36%) of length 7
c [cce-7-1] eliminated 36 clauses out of 929 (4%) of length 6
c [cce-7-1] eliminated 14 clauses out of 6643 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 220 large clauses in 34495576 steps
c [cce-7-1] allowing another 17247788 steps for small clauses
c [cce-7-1] scheduling 180319 clauses = 110924 binary + 69395 ternary
c [cce-7-1] tried to eliminate 1250 small clauses 1%
c [cce-7-1] eliminated 213 binary clauses 0%
c [cce-7-1] eliminated 69 ternary clauses 0%
c [cce-7-1] eliminated 282 small clauses 0%
c [cce-7-1] eliminated 1012 small clauses in 34495583 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1232 covered clauses in round 1
c [cce-7] eliminated 1232 covered clauses in TOTAL during 1 rounds
c [cce-7] 1232 < 1/100 * 222535 = 2225 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 34913 variables 100%
c [elim-11] limit of 275964597 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 384 variables 1% in round 1 in 18022317 steps
c [elim-11-1] backward subsumption/strengthening limit 18022300
c [elim-11-1-1] backward checking 2207 touched variables 6%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 10 and strengthened 70 clauses in 503070 steps
c [elim-11-1] rescheduled 182 variables 1% by backward subsumption
c [elim-11-2] eliminated 13 variables 0% in round 2 in 80829 steps
c [elim-11-2] backward subsumption/strengthening limit 80800
c [elim-11-2-1] backward checking 143 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 6 and strengthened 7 clauses in 59769 steps
c [elim-11-2] rescheduled 25 variables 0% by backward subsumption
c [elim-11-3] eliminated 3 variables 0% in round 3 in 11761 steps
c [elim-11-3] backward subsumption/strengthening limit 11700
c [elim-11-3-1] backward checking 32 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 0 and strengthened 0 clauses in 11701 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 402 = 1% variables out of 34913 scheduled
c [bca-12] limit of 10000000 steps and 442000 added (scaled 2)
c [bca-12] 48301 out of 69024 literals actually usable 70%
c [bca-12] added 29 blocked clauses in 133552 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 20697340 penalty 1 = 1 + 0
c [sweep-11-1] 3031 pos 9.8% + 28044 neg 90.2% = 31075 sched 90.0% ret 3436
c [sweep-11-1] 20706560 steps 509 queries 509.46 avg class size
c [sweep-11-1] 7503 decisions 450 SAT calls 98.07 avg env size
c [sweep-11-1] 22753 variables remain 66% (11681 retained 34%)
c [decomp-39] removed 286 variables
c [sweep-11-1] removed 286 vars (0 failed, 78 eqs, 101 impls)
c [sweep-11] removed 286 vars in TOTAL (1 rounds, 508 queries)
c [sort-queue-16] sorted 34225 enqueued variables after 61679 conflicts
c [score-dist-16] active 0 (0%), one 28040 (82%), zero 6185 (18%)
c [score-dist-16] max exp 1, different 2 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 940 variables 2.7% (34225 remain 16%)
c [simplification-16] removed 12725 irredundant clauses 5.5% (219217 remain 18%)
c [simplification-16] maximum reduction of 5% = max (3%, 5%)
c [simplification-16] large reduction 5% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 73679 (soft 63679 + delta 10000)
c [simplification-16] new conflict limit 63679 (hard 73679)
c 
c [simplification-17] limit 63679 conflicts (hard 73679) hit after 63680 conflicts
c [quatres-11] found 21366 quaternary clauses 61% in total
c [quatres-11-1] removed 4 duplicate quaternary clauses
c [quatres-11-2] added 5 single-self-subsuming ternary resolvents
c [quatres-11-2] added 11 quaternary resolvents
c [ternres-13] limit 14125793 with penalty 0 = 0 + 0
c [ternres-13] all 34225 free variables schedulable
c [ternres-13] 826 ternary resolvents (10 bin, 816 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-40] removed 1 variables
c [basicprobe-5] limit 70628969 penalty 0 = 0 + 0
c [basicprobe-5-0] 3936 probes remain 12% after last round
c [basicprobe-5-0] 771 units = 758 failed (98%) + 13 lifted (2%)
c [basicprobe-5-0] removed 983 variables, found 106367 hbrs
c [bate-3] eliminated 1017 asymmetric tautologies during probing
c [unhide-17] limit 2825158 with penalty 0 = 0 + 0
c [unhide-17-22] 7 units, 271 failed, 25561 tauts, 0 hbrs, 60335 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 471 transitive binary clauses
c [transred-13] found 4 units
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 32970 variables 100%
c [elim-12] limit of 282515878 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 1012 variables 3% in round 1 in 15787809 steps
c [elim-12-1] backward subsumption/strengthening limit 15787800
c [elim-12-1-1] backward checking 5222 touched variables 16%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 24 and strengthened 152 clauses in 1210966 steps
c [elim-12-1] rescheduled 455 variables 1% by backward subsumption
c [elim-12-2] eliminated 37 variables 0% in round 2 in 796879 steps
c [elim-12-2] backward subsumption/strengthening limit 796800
c [elim-12-2-1] backward checking 370 touched variables 1%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 9 and strengthened 36 clauses in 172378 steps
c [elim-12-2] rescheduled 117 variables 0% by backward subsumption
c [elim-12-3] eliminated 6 variables 0% in round 3 in 158585 steps
c [elim-12-3] backward subsumption/strengthening limit 158500
c [elim-12-3-1] backward checking 74 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 1 and strengthened 4 clauses in 68258 steps
c [elim-12] incomplete 19 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 1056 = 3% variables out of 32970 scheduled
c [bca-13] limit of 10000000 steps and 401184 added (scaled 2)
c [bca-13] 43787 out of 63830 literals actually usable 69%
c [bca-13] added 53 blocked clauses in 121734 steps
c [sweep-12] limit 4237738 penalty 0 = 0 + 0
c [sweep-12-1] 2833 pos 13.3% + 18539 neg 86.7% = 21372 sched 67.0% ret 10542
c [sweep-12-1] 4272908 steps 138 queries 1339.00 avg class size
c [sweep-12-1] 2186 decisions 125 SAT calls 87.74 avg env size
c [sweep-12-1] 20403 variables remain 64% (11482 retained 36%)
c [decomp-41] removed 73 variables
c [sweep-12-1] removed 73 vars (0 failed, 18 eqs, 22 impls)
c [sweep-12] removed 73 vars in TOTAL (1 rounds, 137 queries)
c [sort-queue-17] sorted 31841 enqueued variables after 63680 conflicts
c [score-dist-17] active 0 (0%), one 26769 (84%), zero 5072 (16%)
c [score-dist-17] max exp 1, different 2 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 2384 variables 7.0% (31841 remain 15%)
c [simplification-17] removed 19431 irredundant clauses 8.9% (199786 remain 17%)
c [simplification-17] maximum reduction of 9% = max (7%, 9%)
c [simplification-17] large reduction 9% >= 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 75680 (soft 65680 + delta 10000)
c [simplification-17] new conflict limit 65680 (hard 75680)
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  105.0   31840   199786     64366   24014   5341 190491   29   126   37  23%     25   39   27   14  197%
c 
c [simplification-18] limit 65680 conflicts (hard 75680) hit after 65681 conflicts
c [quatres-12] found 19496 quaternary clauses 59% in total
c [quatres-12-1] removed 2 duplicate quaternary clauses
c [quatres-12-2] added 1 single-self-subsuming ternary resolvents
c [quatres-12-2] added 23 quaternary resolvents
c [ternres-14] limit 14423489 with penalty 0 = 0 + 0
c [ternres-14] all 31812 free variables schedulable
c [ternres-14] 729 ternary resolvents (2 bin, 727 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-7] limit 721174 penalty 2 = 2 + 0
c [gauss-7] extracted 26 xors of average arity 3.0
c [gauss-7] connected 77 occurrences of 71 variables (average 1.1)
c [gauss-7] limit 721174 penalty 2 = 2 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-6] 2059 schedulable variables 6%
c [simpleprobe-6] limit 57693959 penalty 0 = 0 + 0
c [decomp-43] removed 314 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 314 variables, found 29108 hbrs, 158 units
c [unhide-18] limit 2884697 with penalty 0 = 0 + 0
c [unhide-18-24] 4 units, 49 failed, 19337 tauts, 0 hbrs, 29916 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 513 transitive binary clauses
c [transred-14] found 1 units
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 31424 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 15056601 steps
c [elim-13-1] backward subsumption/strengthening limit 15056600
c [elim-13-1-1] backward checking 2153 touched variables 7%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 5 and strengthened 15 clauses in 536679 steps
c [elim-13-1] rescheduled 57 variables 0% by backward subsumption
c [elim-13-2] eliminated 4 variables 0% in round 2 in 51229 steps
c [elim-13-2] backward subsumption/strengthening limit 51200
c [elim-13-2-1] backward checking 75 touched variables 0%
c [elim-13-2-1] incomplete backward checking 0 remain 0%
c [elim-13-2] subsumed 4 and strengthened 2 clauses in 51201 steps
c [elim-13-2] rescheduled 19 variables 0% by backward subsumption
c [elim-13-3] eliminated 1 variables 0% in round 3 in 15346 steps
c [elim-13-3] backward subsumption/strengthening limit 15300
c [elim-13-3-1] backward checking 10 touched variables 0%
c [elim-13-3-1] incomplete backward checking 0 remain 0%
c [elim-13-3] subsumed 0 and strengthened 2 clauses in 15301 steps
c [elim-13] incomplete 8 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 297 = 1% variables out of 31424 scheduled
c [elim-13] 297 < 1/100 * 31424 = 314 considered unsuccessful
c [bca-14] limit of 10000000 steps and 387623 added (scaled 2)
c [bca-14] 42161 out of 62256 literals actually usable 68%
c [bca-14] added 25 blocked clauses in 118211 steps
c [sweep-13] limit 4327046 penalty 0 = 0 + 0
c [sweep-13-1] 2538 pos 12.7% + 17499 neg 87.3% = 20037 sched 64.4% ret 11090
c [sweep-13-1] 4338634 steps 52 queries 1957.46 avg class size
c [sweep-13-1] 1331 decisions 49 SAT calls 199.55 avg env size
c [sweep-13-1] 19685 variables remain 63% (11442 retained 37%)
c [decomp-44] removed 34 variables
c [sweep-13-1] removed 34 vars (0 failed, 3 eqs, 6 impls)
c [sweep-13] removed 34 vars in TOTAL (1 rounds, 51 queries)
c [sort-queue-18] sorted 31093 enqueued variables after 65681 conflicts
c [score-dist-18] active 0 (0%), one 26426 (85%), zero 4667 (15%)
c [score-dist-18] max exp 1, different 2 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 719 variables 2.3% (31093 remain 15%)
c [simplification-18] removed 6569 irredundant clauses 3.3% (193217 remain 16%)
c [simplification-18] maximum reduction of 3% = max (2%, 3%)
c [simplification-18] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-18] new conflict interval 23000
c [simplification-18] penalized conflict interval 23000 = 1 * 23000
c [simplification-18] hard conflict limit 100181 (soft 88681 + delta 11500)
c [simplification-18] new conflict limit 88681 (hard 100181)
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  109.4   31092   193217     67196   25019   5634 193882   26   114   37  23%     26   25   18   14  128%
c i  110.2   31091   193217     68559   26262   5661 193898   27   113   37  24%     13   24   29   15  200%
c i  110.5   31090   193217     69275   26892   5680 193922   26   110   37  24%      7   21   23   15  155%
c i  110.6   31088   193217     69396   27004   5684 193924   26   110   37  24%      5   21   22   15  151%
c i  111.0   31080   193217     70179   27731   5695 193946   26   109   37  24%      3   20   23   15  158%
c i  111.4   31068   193217     70973   28476   5701 193961   26   109   37  24%      2   19   35   15  232%
c i  111.5   31067   193217     71055   28543   5708 193968   26   109   37  24%      2   19   30   15  199%
c i  111.7   31064   193217     71530   28971   5721 193985   25   105   37  24%      1   15   20   15  136%
c i  112.9   30980   193217     74008   31238   5770 194024   22    85   37  26%     19   -6   31   15  203%
c i  113.6   30979   193217     75330   32442   5799 194041   23    86   37  27%     10   -4   25   15  162%
c i  113.6   30972   193217     75331   32442   5799 194041   23    86   37  27%     10   -4   25   15  162%
c i  114.2   30969   193217     76407   33445   5821 194057   24    90   37  27%      6   -0   27   15  173%
c i  115.2   30966   193217     78016   34972   5838 194070   25    95   38  27%      9    4   24   16  155%
c i  115.7   30963   193217     78831   35733   5848 194090   26    94   41  27%      5    4   33   16  205%
c i  115.9   30934   193217     79130   36001   5855 194093   27    96   42  28%      3    6   41   16  256%
c i  115.9   30933   193217     79131   36001   5855 194093   27    96   42  28%      3    6   41   16  255%
c i  117.0   30932   193217     80975   37735   5875 194113   29   100   44  29%     11    9   37   16  225%
c i  117.5   30911   193217     81850   38545   5882 194122   29    97   45  30%      5    7   26   17  155%
c i  117.7   30910   193217     82093   38766   5885 194123   29    99   46  29%      3    8   34   17  203%
c i  119.2   30909   193217     84737   41261   5915 194156   26    91   46  28%     21    1   22   17  128%
c 
c [simplification-19] limit 88701 conflicts (hard 100181) hit after 88704 conflicts
c [quatres-13] found 18664 quaternary clauses 54% in total
c [quatres-13-2] added 8 single-self-subsuming ternary resolvents
c [quatres-13-2] added 13 quaternary resolvents
c [ternres-15] limit 18050598 with penalty 0 = 0 + 0
c [ternres-15] all 30909 free variables schedulable
c [ternres-15] 352 ternary resolvents (2 bin, 350 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-45] removed 216 variables
c [treelook-6] limit 1805059 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 48484 literals 79%
c [treelook-6] scheduling used 869230 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 1805059 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 1829330 steps
c [treelook-6] 48403 literals remain 78%
c [treelook-6] 10645 variables remain to probed next time 34%
c [treelook-6] removed 14 variables, found 13042 hbrs
c [unhide-19] limit 3610119 with penalty 0 = 0 + 0
c [unhide-19-26] 2 units, 72 failed, 12423 tauts, 0 hbrs, 176347 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 417 transitive binary clauses
c [transred-15] found 1 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 225632475 steps penalty 2 = 2 + 0
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 29
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 28
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 27
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 26
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 25
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 24
c [cce-8-1] eliminated 1 clauses out of 5 (20%) of length 23
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 22
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 21
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 20
c [cce-8-1] eliminated 2 clauses out of 7 (29%) of length 19
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 18
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 17
c [cce-8-1] eliminated 3 clauses out of 8 (38%) of length 16
c [cce-8-1] eliminated 3 clauses out of 11 (27%) of length 15
c [cce-8-1] eliminated 4 clauses out of 9 (44%) of length 14
c [cce-8-1] eliminated 5 clauses out of 13 (38%) of length 13
c [cce-8-1] eliminated 4 clauses out of 11 (36%) of length 12
c [cce-8-1] eliminated 4 clauses out of 12 (33%) of length 11
c [cce-8-1] eliminated 7 clauses out of 16 (44%) of length 10
c [cce-8-1] eliminated 4 clauses out of 15 (27%) of length 9
c [cce-8-1] eliminated 4 clauses out of 18 (22%) of length 8
c [cce-8-1] eliminated 5 clauses out of 44 (11%) of length 7
c [cce-8-1] eliminated 8 clauses out of 894 (1%) of length 6
c [cce-8-1] eliminated 267 clauses out of 6657 (4%) of length 5
c [cce-8-1] eliminated 5015 clauses out of 16880 (30%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 5355 large clauses in 165997235 steps
c [cce-8-1] allowing another 82998617 steps for small clauses
c [cce-8-1] scheduling 151979 clauses = 100960 binary + 51019 ternary
c [cce-8-1] tried to eliminate 15620 small clauses 10%
c [cce-8-1] eliminated 2240 binary clauses 2%
c [cce-8-1] eliminated 701 ternary clauses 1%
c [cce-8-1] eliminated 2941 small clauses 2%
c [cce-8-1] eliminated 3402 small clauses in 225632478 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 8757 covered clauses in round 1
c [cce-8] eliminated 8757 covered clauses in TOTAL during 1 rounds
c [bca-15] limit of 10000000 steps and 363871 added (scaled 2)
c [bca-15] 39283 out of 61634 literals actually usable 64%
c [bca-15] added 39 blocked clauses in 130273 steps
c [sweep-14] limit 5415179 penalty 0 = 0 + 0
c [sweep-14-1] 2450 pos 12.6% + 17056 neg 87.4% = 19506 sched 63.3% ret 11310
c [sweep-14-1] 5467857 steps 90 queries 1396.16 avg class size
c [sweep-14-1] 1757 decisions 80 SAT calls 149.94 avg env size
c [sweep-14-1] 19013 variables remain 62% (11790 retained 38%)
c [decomp-47] removed 38 variables
c [sweep-14-1] removed 38 vars (0 failed, 15 eqs, 23 impls)
c [sweep-14] removed 38 vars in TOTAL (1 rounds, 89 queries)
c [sort-queue-19] sorted 30778 enqueued variables after 88704 conflicts
c [score-dist-19] active 0 (0%), one 26348 (86%), zero 4430 (14%)
c [score-dist-19] max exp 1, different 2 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 131 variables 0.4% (30778 remain 14%)
c [simplification-19] removed 11983 irredundant clauses 6.2% (181234 remain 15%)
c [simplification-19] maximum reduction of 6% = max (0%, 6%)
c [simplification-19] large reduction 6% >= 5% limit
c [simplification-19] next conflict interval 2000 = 2000/1
c [simplification-19] penalized conflict interval 2000 = 1 * 2000
c [simplification-19] hard conflict limit 100704 (soft 90704 + delta 10000)
c [simplification-19] new conflict limit 90704 (hard 100704)
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 1  131.4   30778   181234     89871   45735   6866 198779   25    96   53  27%     56    5   15   18   84%
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: 1901 basic ate = 1368 trn 72% + 533 lrg 28% in 3 updates
c bcas: 15 count, 1222 added (2772 skipped), 3448609 steps
c bkwd: tried 311284 clauses, 621486 lits, 2.00 lits/clause
c bkwd: checked 15456209 occs, 49.65 occs/clause, 24.87 occs/lit
c bkwd: subsumed 42 binary, 228 ternary, 90 large
c bkwd: strengthened 11 binary, 1 ternary (100% self), 1408 large (0% self)
c blkd: 5 bces, 9241 removed, 6458409 resolutions, 18111850 steps
c blkd: 10269 blocking literals 2%, 59 pure
c bump: 90633 bumped seen, 18031122 lits 198.9 on average
c card: 5 count, 0 units, 0 am1, 21615058 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 66369 subsumed
c card: 14878 at-most-one constraints found, average size 4.88
c card: 14878 at-most-one constraints used 100%, average size 4.88
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: 8 cces, 41332 eliminated, 41234 ate 100%, 98 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: 4113121 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 138 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 47 decompositions, 8302 equivalent 4%
c deco: 1248 decision-only clauses 1%, 57% reduction
c decs: 1786592 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 13 elims, 89813 eliminated 40%, 294 pure 0%
c elms: 34 rounds, 2.6 rounds/bve
c elms: 75853 small 84%, 13607 large 15%
c elms: 173662 tried small, 75861 succeeded 44%, 97801 failed 56%
c elms: 30475 subsumed, 56823 strengthened, 905 blocked
c elms: 12834428 copies, 12629373 resolutions, 4349747 ipos
c elms: 2824371 subchks, 1647943 strchks
c gaus: 7 extractions, 1044 extracted, 2.3 size, 3 max
c gaus: exported 2 units, 2 binary and 0 ternary equations
c gaus: 0 gc, 16525572 steps, 8262786 extr 50%, 12623 elim 0%
c glue: 21.8 orig avg, 21.8 real avg, 3.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 439904 = 101202 simple 23% + 326791 trn 74% + 11911 lrg 3%, 3443 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 90633 clauses, 87.9 length
c lrnd: 7966350 lits = 10617504 orig - 2651154 removed 25%
c lrnd: 47831 uips 53%, 33520 flips 37%
c mins: 81242 mins 90%, 3033 bin 3%, 4804 size 5%
c mins: 22692731 poisoned searches, 5272687 hits, 23% hit rate
c mins: 27085183 used twice searches, 1202806 hits, 4% hit rate
c move: moved 23378, 15330 bin 66%, 8048 trn 34%
c otfs: 371 driving 31%, 809 restarting 69%
c otfs: str 1180, 1068 red 91%, 112 irr 9%
c otfs: str 1180, 0 bin 0%, 131 trn 11%, 1049 lrg 89%
c otfs: sub 5, 4 red 80%, 1 irr 20%
c otfs: sub 5, 0 bin 0%, 1 trn 20%, 4 lrg 80%
c phas: 9 computed, 146216 set, 0 pos (0%), 146216 neg (100%)
c prbs: 5 basic, 18716 probed, 1608 failed, 98 lifted
c prbs: 6 simple, 453054 probed, 475 failed, 415 eqs
c prbs: 6 treelook, 154 probed, 27 failed, 0 lifted
c prom: 0 locked 0% out of 92628 tried
c prps: 264136838 props, 139 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 13 count, 306 quat, 42 self1, 0 self2, 1683 dup
c queu: 19 sorted, 1786592 next (10 steps 0.00)
c queu: 19349623 enq (0 steps 0.00), 18031122 deq 93%
c redc: 4891 clauses 28%, 17771 tried 20%, 223 sat 1%
c redc: 11009 lits 6%, 183244 tried 2%, 223 sat 0%
c redc: 745 times jump level reduced, 25.6 levels on average
c reds: 0 count, 0.0 conflicts per reduce
c reds: 0 memlim 0%, 0 arith 0%
c reds: 0 collected 0%, 0 retired 0%
c rmbd: 39174 removed, 3432 red 9%
c rsts: 6474 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 19 count, 16 confs 84%, 0 vars 0%
c simp: 2 its 11%, 1 bin 5%, 0 trns 0%
c subl: 90633 count (84706 tried 0.9), 2542 sub out of 82419 (3.1%)
c swps: 14 count, 14 rounds, 1270 queries (90.7/round)
c swps: 1133 sat calls, 56 unsat (1.0% success rate)
c swps: 18749 decisions 16.5, 1133 conflicts 1.0
c swps; 2965.0 avg class size, 92.5 avg environment size
c swps: 0 failed, 284 impls, 180 equivs
c swp0: 418 type 0 queries, 121 unsat (28.9%), 396 sat (94.7%)
c swp1: 852 type 1 queries, 587 unsat (68.9%), 694 sat (81.5%)
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: 3755344 calls to obtain time
c tops: 96093 fixed 43%, 541 its, 166.12 confs/it
c trds: 15 transitive reductions, 5387 removed, 87 failed
c trds: 37506 nodes, 88583 edges, 27886865 steps
c trim: 344254 words, 1.3 MB
c trnr: 15 count, 22 bin, 6819 trn, 74990432 steps
c unhd: 19 count, 26 rounds, 54531707 steps
c unhd: 2780 non-trivial sccs of average size 2.2
c unhd: 267 units, 266 bin, 0 trn, 1 lrg
c unhd: 9559 failed, 9479 stamp, 0 lits, 42 bin, 31 trn, 1 lrg
c unhd: 200995 tauts, 13200 bin 7%, 11020 trn 5%, 700 lrg 0%
c unhd: 200995 tauts, 176075 stamp 88%, 132304 red 66%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 566398 str, 266 bin 0%, 3855 trn 1%, 562277 lrg 99%, 549672 red 97%
c vars: 30778 remaining 14% and 194208 removed 86% out of 224986
c vars: 96093 fixed 43%, 89813 eliminated 40%, 8302 equivalent 4%
c vsts: 1980353795 visits, 92% srch, 8% simp, 0% lkhd
c vsts: 7.3 search visits per propagation, 20310.1 per conflict
c wchs: 286619873 pushed, 37470181 enlarged, 204 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all          82725             0             0       3404080        363890         32202
c 
c  0 0         18148  22         0   0<        0   0<  2248283  66    176907  49     12430  39     1.1
c  1 5          5616   7         0   0         0   0    242929   7<    30555   8      2826   9     0.5
c  2 6         12814  15         0   0         0   0    319694   9     45374  12<     4639  14<    1.8
c  3 9         12514  15<        0   0         0   0    207426   6     32369   9      3299  10     2.3
c  4 14         8531  10         0   0         0   0    134031   4     21581   6      2410   7     1.8
c  5 21         6392   8         0   0         0   0     84144   2     17612   5      1888   6     1.4
c  6 30         5182   6         0   0         0   0     77852   2     14885   4      1576   5     1.4
c  7 41         4240   5         0   0         0   0     39268   1      9382   3      1150   4     1.3
c  8 54         3043   4         0   0         0   0     20387   1      5627   2       682   2     1.0
c  9 69         2109   3         0   0         0   0     14819   0      4321   1       525   2     0.7
c 10 86         1964   2         0   0         0   0     10160   0      3176   1       481   1     0.6
c 11 126        1607   2         0   0         0   0      4338   0      1748   0       253   1     0.5
c 12 230         544   1         0   0         0   0       726   0       342   0        42   0     0.3
c 13 534          21   0         0   0         0   0        23   0        11   0         1   0     0.0
c 
c avg                  3.4           0.0           0.0           1.1           1.9           2.4
c std                  3.0           0.0           0.0           1.9           2.5           2.7
c 
c   18.900  14% cce
c   11.974   9% elim
c    9.424   7% probe
c    9.405   7% unhide
c    5.524   4% sweep
c    1.980   2% bca
c    1.775   1% gauss
c    1.672   1% block
c    1.608   1% transred
c    1.286   1% bump
c    1.096   1% decide
c 
c    1.534 < 1% rest (below)
c 
c    0.687   1% ternres
c    0.537   0% quatres
c    0.309   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    4.490   3% preprocessing     6%
c   66.069  50% inprocessing     94%
c ==================================
c   70.559  54% simplifying
c   60.840  46% search
c ==================================
c  131.411 100% all
c 
c         89871 conflicts,         683.9 confs/sec
c          3449 ternaries,          26.1 confs/ternary
c          3793 binaries,           23.7 confs/binary
c           541 iterations,        166.1 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          6474 restarts,           49.3 rests/sec,     13.9 confs/restart
c       1786592 decisions,       13595.5 decis/sec,     19.9 decis/conflict
c     264136838 propagations,  2010010.1 props/sec,    147.8 props/decision
c 
c 131.4 seconds, 78.0 MB
c launch: done
