c launch: /data/cnf/sc2014/app/grid-strips-grid-y-3.035-NOTKNOWN.cnf.bz2
c host: atom20
c Lingeling SAT Solver
c 
c Version b7ztzud 55d9a3e9649fc56eacf3e72d8e2e2d5c615d5f18
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Fri May  1 11:44:04 CEST 2015
c compiled Fri May  1 11:44:04 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/grid-strips-grid-y-3.035-NOTKNOWN.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/grid-strips-grid-y-3.035-NOTKNOWN.cnf.bz2
c no embedded options
c found 'p cnf 257380 2139615' header
c read 257380 variables, 2139615 clauses, 5163755 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 --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 199865 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  199865  1689184         0       0      0     0    0     0   59   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 12 at-most-one constraints of average size 15.7
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 12 out of 12 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 3292 at-most-one constraints, 866 used 26%
c [card-1] exported 4772 binary clauses, 5.5 per/constraint
c [decomp-1] removed 65363 variables
c [simpleprobe-1] all 192017 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 2073 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 2073 variables, found 1288 hbrs, 2005 units
c [unhide-1] limit 99299 based on 1588793 irredundant clauses
c [unhide-1-1] 14 units, 6 failed, 76798 tauts, 0 hbrs, 14 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 189928 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 13261 not tried 7% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 4927 = 3% variables out of 189928 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 1489225 negative 100.0% of 1489324 except 99 0.0%
c [phase-count-1] 847794 positive 56.9% of 1489324 except 641530 43.1%
c [phase-count-1] less non-negative clauses 99 than limit 148900 (10.0%)
c [phase-count-1] non-pos/non-neg = 641530/99 = 6480.10 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 185001 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 185001 zero 100.00%
c [score-distribution-1] 1 different 0.00% out of total 185001 variables
c [simplification-1] removed 7599 variables 3.9% (185001 remain 93%)
c [simplification-1] removed 199860 irredundant clauses 11.8% (1489324 remain 88%)
c [simplification-1] maximum reduction of 12% = max (4%, 12%)
c [simplification-1] large reduction 12% >= 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    8.5  185000  1489324        62      46     13  1929    0     5   57   2%      0    5    1    0 22143%
c i    8.6  184985  1489324        66      48     14  1929    0     5   57   2%      0    5    1    0 21845%
c i    8.7  184983  1489324       101      79     16  1930    0    13   58   2%      0   13    3    0 21471%
c i    8.8  184072  1489324       135     103     19  1934    0    14   58   2%      0   14    4    0 20585%
c i    8.9  183149  1489324       194     147     24  1937    0    15   58   3%      0   15    6    0 18928%
c i    9.1  183148  1489324       237     184     28  1937    1    21   58   4%      0   21   10    0 18968%
c i    9.2  183133  1489324       276     212     34  1938    1    25   58   4%      0   25   10    0 17225%
c i    9.5  183112  1489324       366     284     47  1941    1    29   59   4%      0   29   10    0 14278%
c i   10.0  183095  1489324       555     443     59  1947    2    41   59   5%      0   41   17    0 12140%
c i   10.6  183071  1489324       718     575     70  1953    4    53   60   7%      1   53   29    0 11920%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 1957 variables
c [simpleprobe-2] all 183044 free variables schedulable
c [simpleprobe-2] limit 2946710 based on 1473355 irredundant clauses
c [decomp-4] removed 190 variables
c [simpleprobe-2] 168222 variables remain 92% (14632 retained 8%)
c [simpleprobe-2] removed 190 variables, found 1660 hbrs, 187 units
c [treelook-1] limit 368033 based on 1472132 irredundant clauses
c [treelook-1] scheduled 149830 literals 41%
c [treelook-1] scheduling used 371303 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 368033 based on 1472132 irredundant clauses
c [treelook-1] used 1100637 steps
c [treelook-1] 149827 literals remain 41%
c [treelook-1] 149797 variables remain to probed next time 82%
c [treelook-1] removed 0 variables, found 2889 hbrs
c [basicprobe-1] limit 11777056 based on 1472132 irredundant clauses
c [basicprobe-1-0] 166027 probes remain 91% after last round
c [basicprobe-1-0] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 9 variables, found 34 hbrs
c [unhide-2] limit 92008 based on 1472132 irredundant clauses
c [unhide-2-2] 7 units, 6 failed, 354 tauts, 0 hbrs, 28943 literals
c [elim-2] 13258 variables 7% will be scheduled this time
c [elim-2] scheduled 13258 variables 7%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 10701 not tried 6% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 0 = 0% variables out of 13258 scheduled
c [elim-2] considered successful since not run to completion yet
c [score-distribution-2] 173323 pos 94.81%, 0 min 0.00%, 9481 zero 5.19%
c [score-distribution-2] 5776 different 3.16% out of total 182804 variables
c [simplification-2] removed 267 variables 0.1% (182804 remain 91%)
c [simplification-2] removed 18001 irredundant clauses 1.2% (1471323 remain 87%)
c [simplification-2] maximum reduction of 1% = max (0%, 1%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1002 (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   15.0  182803  1471323       719     563     72  5891    4    53   58   7%      1   53   29    0 11874%
c i   15.0  182795  1471323       736     578     72  5891    4    55   60   8%      0   55   37    0 13102%
c i   15.3  182794  1471323       849     665     82  5896    5    60   61   9%      1   59   41    0 11469%
c i   15.7  182793  1471323       958     748     87  5898    7    69   61  10%      1   69   49    0 10443%
c 
c [simplification-3] limit 1012 conflicts (hard 11000) hit after 1012 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 21 at-most-one constraints of average size 47.4
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 21 out of 21 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 4894 at-most-one constraints, 894 used 18%
c [card-2] exported 4938 binary clauses, 5.5 per/constraint
c [decomp-6] removed 24 variables
c [unhide-3] limit 91949 based on 1471196 irredundant clauses
c [unhide-3-3] 0 units, 4 failed, 32779 tauts, 0 hbrs, 23952 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 182777 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 49346 not tried 27% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 234 = 0% variables out of 182777 scheduled
c [elim-3] considered successful since not run to completion yet
c [score-distribution-3] 175764 pos 96.29%, 0 min 0.00%, 6779 zero 3.71%
c [score-distribution-3] 5794 different 3.17% out of total 182543 variables
c [simplification-3] removed 250 variables 0.1% (182543 remain 91%)
c [simplification-3] removed 33245 irredundant clauses 2.3% (1438078 remain 85%)
c [simplification-3] maximum reduction of 2% = max (0%, 2%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 6666
c [simplification-3] penalized conflict interval 6666 = 1 * 6666
c [simplification-3] hard conflict limit 17678 (soft 7678 + delta 10000)
c [simplification-3] new conflict limit 7678 (hard 17678)
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.9  182542  1438078      1018     590     90 10810    7    70   58  10%      1   69   41    0 8602%
c i   31.9  182540  1438078      1020     590     90 10811    7    70   58  10%      1   69   41    0 8536%
c i   32.2  182539  1438078      1090     653     92 10812    7    73   60  10%      1   73   36    1 7140%
c i   33.0  182537  1438078      1374     886    120 10816    9   104   61   8%      1  103   34    1 5396%
c i   35.3  182536  1438078      2150    1524    180 10843   10   144   66   7%      4  141   21    1 2568%
c i   35.4  182535  1438078      2205    1569    184 10845   12   150   66   8%      4  147   41    1 4365%
c i   36.0  182531  1438078      2364    1704    191 10848   14   159   67   8%      3  156   46    1 4377%
c i   38.8  182512  1438078      3289    2429    267 10873   24   188   70  13%      6  183   93    2 4918%
c i   39.2  182489  1438078      3433    2550    276 10876   25   193   73  13%      6  188   84    2 4106%
c i   41.2  182474  1438078      3884    2918    302 10890   31   232   76  13%      5  225   79    3 3082%
c i   41.4  182472  1438078      3973    2990    309 10893   31   231   76  13%      4  224   64    3 2485%
c i   43.0  182471  1438078      4467    3422    335 10912   35   250   79  14%      4  241   67    3 2204%
c i   43.1  182470  1438078      4503    3451    338 10912   34   249   79  14%      4  240   61    3 1977%
c 
c [simplification-4] limit of 131 binary hit after 131 binaries
c [decomp-7] removed 79 variables
c [treelook-2] limit 359348 based on 1437393 irredundant clauses
c [treelook-2] scheduled 141310 literals 39%
c [treelook-2] scheduling used 361293 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 359348 based on 1437393 irredundant clauses
c [treelook-2] used 691615 steps
c [treelook-2] 141307 literals remain 39%
c [treelook-2] 131267 variables remain to probed next time 72%
c [treelook-2] removed 0 variables, found 886 hbrs
c [unhide-4] limit 194886 with penalty 2 = 0 + 2
c [unhide-4-4] 13 units, 13 failed, 867 tauts, 0 hbrs, 169845 literals
c [elim-4] 10700 variables 6% will be scheduled this time
c [elim-4] scheduled 10700 variables 6%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1559091920 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 189432458 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 10700 scheduled
c [score-distribution-4] 178449 pos 97.82%, 882 min 0.48%, 3102 zero 1.70%
c [score-distribution-4] 7521 different 4.12% out of total 182433 variables
c [simplification-4] removed 36 variables 0.0% (182433 remain 91%)
c [simplification-4] removed 4493 irredundant clauses 0.3% (1433585 remain 85%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] forced so keeping old conflict interval 6666
c [simplification-4] conflict limit remains at 7683 (hard 17678)
c [simplification-4] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   48.7  182432  1433585      4579    3474    342 10946   34   247   75  14%      4  238   56    3 1813%
c i   49.0  182426  1433585      4644    3531    345 10947   34   247   82  14%      4  238   48    3 1522%
c i   49.3  182406  1433585      4735    3604    349 10949   35   249   83  14%      3  239   54    3 1690%
c i   51.9  182405  1433585      5529    4253    394 10968   41   272   84  15%      5  259   64    4 1600%
c i   53.2  182404  1433585      5943    4616    417 10974   41   268   85  15%      4  254   43    4 1024%
c i   53.8  182403  1433585      6114    4753    431 10981   43   283   85  15%      4  268   70    4 1566%
c i   53.8  182401  1433585      6131    4764    431 10983   44   283   85  15%      4  268   76    5 1683%
c i   53.8  182400  1433585      6132    4764    431 10983   44   283   85  15%      4  268   75    5 1677%
c i   54.0  182398  1433585      6163    4793    431 10983   44   285   86  15%      4  269   80    5 1759%
c i   55.1  182379  1433585      6538    5117    450 10989   49   294   86  17%      3  277   76    5 1496%
c i   55.3  182378  1433585      6579    5153    450 10990   50   293   86  17%      3  276   88    5 1706%
c i   55.8  182357  1433585      6748    5283    466 10998   50   289   86  17%      3  271   64    5 1219%
c i   56.2  182356  1433585      6873    5382    481 11001   49   284   86  17%      3  266   45    5  853%
c i   58.4  182355  1433585      7465    5876    518 11017   50   296   97  17%      4  275   70    6 1203%
c 
c [simplification-5] limit 7693 conflicts (hard 17678) hit after 7693 conflicts
c [quatres-1] found 711 quaternary clauses 2% in total
c [quatres-1-2] added 1 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 32969580 with penalty 0 = 0 + 0
c [ternres-1] all 182336 free variables schedulable
c [ternres-1] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 1 xors of average arity 2.0
c [gauss-1] connected 2 occurrences of 2 variables (average 1.0)
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 4 variables
c [basicprobe-2] limit 32969582 penalty 0 = 0 + 0
c [basicprobe-2-0] 165462 probes remain 91% after last round
c [basicprobe-2-0] 27 units = 27 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 28 variables, found 836 hbrs
c [unhide-5] limit 164847 with penalty 3 = 0 + 3
c [unhide-5-5] 6 units, 3 failed, 30742 tauts, 0 hbrs, 331131 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 36 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 182294 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 659391640 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 646 blocked clauses
c [block-1] 646 < 1/100 * 1401778 = 14017 considered unsuccessful
c [cce-1] limit of 32969582 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 37 clauses out of 405 (9%) of length 541
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 37 large clauses in 32970042 steps
c [cce-1-1] allowing another 16485021 steps for small clauses
c [cce-1-1] scheduling 1368176 clauses = 1368054 binary + 122 ternary
c [cce-1-1] tried to eliminate 85 small clauses 0%
c [cce-1-1] eliminated 29 binary clauses 0%
c [cce-1-1] eliminated 29 small clauses 0%
c [cce-1-1] eliminated 29 small clauses in 32969585 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 66 covered clauses in round 1
c [cce-1] eliminated 66 covered clauses in TOTAL during 1 rounds
c [cce-1] 66 < 1/100 * 1401059 = 14010 considered unsuccessful
c [bca-1] limit of 10000000 steps and 2802486 added (scaled 2)
c [bca-1] 186259 out of 364590 literals actually usable 51%
c [bca-1] added 7050 blocked clauses in 399554 steps
c [sweep-1] limit 2801986 based on 1400993 irredundant clauses
c [sweep-1-1] 380 pos 0.2% + 181914 neg 99.8% = 182294 sched 100.0% ret 0
c [sweep-1-1] 3251739 steps 10 queries 30509.60 avg class size
c [sweep-1-1] 567 decisions 8 SAT calls 3032.50 avg env size
c [sweep-1-1] 182265 variables remain 100% (29 retained 0%)
c [decomp-10] removed 3 variables
c [sweep-1-1] removed 3 vars (0 failed, 1 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 3 vars in TOTAL (1 rounds, 9 queries)
c [score-distribution-5] 178441 pos 97.89%, 788 min 0.43%, 3062 zero 1.68%
c [score-distribution-5] 7255 different 3.98% out of total 182291 variables
c [simplification-5] removed 45 variables 0.0% (182291 remain 91%)
c [simplification-5] removed 32596 irredundant clauses 2.3% (1400989 remain 83%)
c [simplification-5] maximum reduction of 2% = max (0%, 2%)
c [simplification-5] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-5] new conflict interval 13332
c [simplification-5] penalized conflict interval 13332 = 1 * 13332
c [simplification-5] hard conflict limit 31025 (soft 21025 + delta 10000)
c [simplification-5] new conflict limit 21025 (hard 31025)
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   73.7  182290  1400989      7786    6131    549 19091   49   288  108  17%      3  266   42    6  706%
c i   74.5  182289  1400989      7997    6308    567 19098   48   286  109  17%      3  264   40    6  663%
c i   75.2  182288  1400989      8197    6478    577 19105   49   291  109  17%      3  268   45    6  734%
c i   77.0  182287  1400989      8743    6948    599 19117   49   287  109  17%      3  262   54    7  817%
c i   77.3  182286  1400989      8822    7015    601 19118   50   287  109  17%      3  261   60    7  909%
c i   78.7  182271  1400989      9244    7387    626 19121   53   321  109  16%      3  293   82    7 1151%
c i   79.0  182270  1400989      9357    7487    631 19123   52   318  109  16%      3  290   60    7  840%
c i   81.0  182255  1400989      9922    7968    663 19140   50   302  109  17%      3  271   49    7  659%
c i   81.4  182249  1400989     10027    8058    671 19143   51   304  109  17%      3  273   60    7  804%
c i   83.7  182245  1400989     10748    8660    703 19154   54   300  109  18%      4  266   76    8  927%
c i   85.5  182244  1400989     11285    9113    739 19166   57   306  112  19%      4  270   62    9  709%
c i   85.6  182239  1400989     11300    9122    739 19168   57   305  112  19%      4  269   59    9  680%
c i   86.2  182230  1400989     11527    9307    752 19172   54   296  112  18%      4  259   33    9  378%
c i   86.4  182229  1400989     11588    9365    754 19172   54   295  112  18%      3  257   36    9  414%
c i   87.1  182228  1400989     11781    9504    763 19176   58   299  112  19%      3  260   83    9  914%
c i   87.8  182227  1400989     12001    9696    776 19180   58   298  112  19%      3  259   65    9  702%
c i   88.5  182221  1400989     12191    9860    791 19181   58   295  112  20%      2  255   54    9  570%
c i   88.7  182220  1400989     12278    9939    795 19181   57   291  116  20%      2  251   46    9  484%
c i   89.7  182218  1400989     12532   10152    813 19188   55   285  116  19%      2  244   36   10  377%
c i   89.8  182211  1400989     12567   10181    816 19188   55   286  116  19%      2  245   34   10  358%
c i   90.0  182210  1400989     12619   10230    818 19188   55   287  116  19%      2  246   38   10  393%
c i   90.2  182205  1400989     12694   10283    821 19190   55   287  124  19%      2  245   42   10  440%
c i   91.7  182203  1400989     13106   10629    855 19204   53   276  138  19%      2  233   32   10  331%
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   92.4  182202  1400989     13284   10779    864 19207   53   272  140  19%      2  228   41   10  412%
c i   93.0  182201  1400989     13482   10952    876 19208   52   266  140  19%      2  222   35   10  348%
c i   95.7  182151  1400989     14257   11623    909 19216   63   293  160  22%      4  246  107   11  960%
c i   96.5  182135  1400989     14539   11856    928 19221   64   293  160  22%      3  245   95   11  825%
c i   96.5  182133  1400989     14540   11856    928 19221   64   293  160  22%      3  245   94   11  822%
c i  101.7  182128  1400989     15968   13078    985 19239   72   287  161  25%     11  233   80   13  605%
c i  101.8  182119  1400989     15982   13090    985 19239   72   286  161  25%     10  233   79   13  596%
c i  103.8  182118  1400989     16548   13571   1001 19244   72   296  161  24%      8  240   93   14  682%
c i  104.0  182097  1400989     16613   13631   1003 19244   71   292  161  24%      7  236   76   14  554%
c i  104.0  182095  1400989     16614   13631   1003 19244   71   292  161  24%      7  236   76   14  552%
c i  105.9  182056  1400989     17073   14021   1029 19251   70   298  161  23%      6  241   45   14  324%
c i  107.2  182041  1400989     17401   14304   1039 19255   73   306  161  24%      5  247   99   14  681%
c i  107.3  182022  1400989     17406   14308   1039 19255   73   306  161  24%      4  247   97   14  669%
c i  107.4  182017  1400989     17455   14347   1045 19256   73   304  161  24%      4  245   90   15  621%
c i  109.6  182016  1400989     17933   14747   1072 19259   78   301  163  26%      4  241   97   15  634%
c i  111.1  182015  1400989     18322   15079   1091 19264   79   306  163  26%      3  244   96   16  609%
c i  111.9  182013  1400989     18569   15279   1094 19274   80   303  163  26%      3  241   90   16  560%
c i  112.2  182002  1400989     18677   15376   1095 19274   79   299  163  26%      3  236   74   16  461%
c i  114.5  182000  1400989     19191   15826   1116 19278   77   290  163  26%      3  225   55   16  338%
c i  117.4  181975  1400989     19824   16344   1146 19289   82   296  169  28%      4  229   86   17  494%
c i  117.9  181974  1400989     19960   16462   1152 19294   80   299  169  27%      3  231   60   17  348%
c i  117.9  181973  1400989     19961   16462   1152 19294   80   299  169  27%      3  231   60   17  346%
c i  118.1  181968  1400989     20009   16506   1153 19295   79   297  169  27%      3  229   53   17  305%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  120.3  181967  1400989     20623   17020   1176 19307   75   280  176  27%      3  210   45   18  255%
c i  120.4  181965  1400989     20658   17050   1176 19308   77   282  176  27%      3  212   73   18  412%
c i  121.3  181964  1400989     20863   17224   1188 19308   76   280  189  27%      3  210   70   18  392%
c i  121.7  181963  1400989     20964   17290   1198 19308   75   277  189  27%      3  206   63   18  352%
c 
c [simplification-6] limit 21057 conflicts (hard 31025) hit after 21057 conflicts
c [quatres-2] found 982 quaternary clauses 3% in total
c [ternres-2] limit 18016088 with penalty 0 = 0 + 0
c [ternres-2] all 181963 free variables schedulable
c [ternres-2] 36 ternary resolvents (0 bin, 36 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 2252011 penalty 2 = 2 + 0
c [card-3] found 54 at-most-one constraints of average size 46.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 2252011 for elimination
c [card-3] 54 out of 54 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 380 variables
c [simpleprobe-3] 167361 schedulable variables 92%
c [simpleprobe-3] limit 72064353 penalty 0 = 0 + 0
c [decomp-12] removed 4905 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 4905 variables, found 37846 hbrs, 2679 units
c [unhide-6] limit 225201 with penalty 4 = 0 + 4
c [unhide-6-6] 0 units, 5 failed, 1382 tauts, 0 hbrs, 2656982 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 46 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 177004 variables 100%
c [elim-5] limit of 180160883 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 323 not tried 0% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1520 = 1% variables out of 177004 scheduled
c [elim-5] 1520 < 1/100 * 177004 = 1770 considered unsuccessful
c [bca-2] limit of 10000000 steps and 2715693 added (scaled 2)
c [bca-2] 194873 out of 350970 literals actually usable 56%
c [bca-2] added 8102 blocked clauses in 457243 steps
c [sweep-2] limit 5404826 penalty 0 = 0 + 0
c [sweep-2-1] 426 pos 0.2% + 175030 neg 99.8% = 175456 sched 100.0% ret 28
c [sweep-2-1] 5826332 steps 9 queries 54835.22 avg class size
c [sweep-2-1] 337 decisions 8 SAT calls 1016.88 avg env size
c [sweep-2-1] 175433 variables remain 100% (50 retained 0%)
c [decomp-13] removed 1 variables
c [sweep-2-1] removed 1 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 1 vars in TOTAL (1 rounds, 8 queries)
c [score-distribution-6] 169696 pos 96.70%, 2778 min 1.58%, 3009 zero 1.71%
c [score-distribution-6] 15965 different 9.10% out of total 175483 variables
c [simplification-6] removed 6480 variables 3.6% (175483 remain 88%)
c [simplification-6] removed 45161 irredundant clauses 3.2% (1355828 remain 80%)
c [simplification-6] maximum reduction of 4% = max (4%, 3%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 17332
c [simplification-6] penalized conflict interval 17332 = 1 * 17332
c [simplification-6] hard conflict limit 48389 (soft 38389 + delta 10000)
c [simplification-6] new conflict limit 38389 (hard 48389)
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  159.2  175482  1355828     22847    7477   1309 62967   65   267   83  24%     15  191   37   19  195%
c i  160.9  175481  1355828     23373    7915   1339 62982   64   286   88  23%     10  207   68   19  357%
c i  162.7  175479  1355828     23877    8327   1363 62984   64   288   90  22%      7  208   51   19  261%
c i  162.9  175478  1355828     23952    8390   1366 62985   63   294   90  22%      7  214   43   19  222%
c i  167.9  175477  1355828     25360    9629   1432 63002   65   315  102  21%     11  230   71   20  345%
c i  173.7  175458  1355828     26993   11000   1511 63027   67   311  113  21%     13  221   75   22  346%
c i  176.6  175439  1355828     27764   11652   1556 63037   67   322  130  21%      9  229   85   22  383%
c i  180.1  175438  1355828     28539   12323   1594 63048   72   323  144  22%      7  229  103   23  448%
c i  180.3  175437  1355828     28597   12367   1597 63053   72   322  144  22%      6  227   89   23  386%
c i  182.7  175435  1355828     29194   12864   1621 63060   76   332  153  23%      5  235   96   24  402%
c i  185.8  175434  1355828     29971   13522   1664 63073   81   359  153  23%      5  259  129   25  523%
c i  192.1  175418  1355828     31541   14863   1729 63090   85   342  169  25%     11  236   90   26  342%
c i  195.6  175417  1355828     32514   15647   1782 63103  111   375  171  30%      8  265  181   29  623%
c i  195.8  175416  1355828     32581   15706   1783 63103  110   372  171  30%      8  262  152   29  524%
c i  196.0  175406  1355828     32634   15753   1786 63105  111   373  171  30%      7  263  151   29  520%
c i  198.0  175405  1355828     33198   16223   1808 63109  113   372  180  30%      5  260  127   30  423%
c i  199.4  175391  1355828     33563   16508   1827 63116  111   373  190  30%      4  260   88   30  291%
c i  199.7  175390  1355828     33618   16551   1830 63117  110   373  190  30%      3  260   84   30  276%
c i  200.8  175389  1355828     33936   16805   1842 63128  107   369  190  29%      3  254   65   30  214%
c i  201.4  175388  1355828     34066   16915   1849 63132  106   367  190  29%      2  252   70   31  231%
c i  204.2  175365  1355828     34787   17515   1879 63136  104   368  190  28%      3  250   80   31  255%
c i  211.4  175364  1355828     36450   18900   1946 63154  139   416  230  33%     12  291  218   36  610%
c i  213.1  175345  1355828     36891   19267   1966 63161  140   431  232  32%      8  304  150   36  413%
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  217.3  175343  1355828     37869   20116   2006 63173  127   419  250  30%      7  288   57   37  155%
c i  219.4  175320  1355828     38285   20442   2022 63181  141   452  253  31%      5  318  196   38  508%
c 
c [simplification-7] limit 38389 conflicts (hard 48389) hit after 38392 conflicts
c [ternres-3] limit 33171113 with penalty 0 = 0 + 0
c [ternres-3] all 175301 free variables schedulable
c [ternres-3] 158 ternary resolvents (0 bin, 158 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 3317111 penalty 1 = 1 + 0
c [gauss-2] extracted 2 xors of average arity 2.5
c [gauss-2] connected 5 occurrences of 5 variables (average 1.0)
c [gauss-2] limit 3317111 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 3 variables
c [unhide-7] limit 414638 with penalty 4 = 0 + 4
c [unhide-7-7] 7 units, 3 failed, 13554 tauts, 0 hbrs, 2259570 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 18 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 175288 variables 100%
c [block-2] limit of 165855569 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [cce-2] limit of 82927784 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 63 clauses out of 277 (23%) of length 541
c [cce-2-1] eliminated 15 clauses out of 65 (23%) of length 540
c [cce-2-1] eliminated 6 clauses out of 22 (27%) of length 539
c [cce-2-1] eliminated 6 clauses out of 20 (30%) of length 538
c [cce-2-1] eliminated 8 clauses out of 18 (44%) of length 537
c [cce-2-1] eliminated 5 clauses out of 15 (33%) of length 536
c [cce-2-1] eliminated 1 clauses out of 10 (10%) of length 535
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 104 large clauses in 82927784 steps
c [cce-2-1] allowing another 41463892 steps for small clauses
c [cce-2-1] scheduling 1308462 clauses = 1307958 binary + 504 ternary
c [cce-2-1] tried to eliminate 432 small clauses 0%
c [cce-2-1] eliminated 141 binary clauses 0%
c [cce-2-1] eliminated 141 small clauses 0%
c [cce-2-1] eliminated 141 small clauses in 82927861 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 245 covered clauses in round 1
c [cce-2] eliminated 245 covered clauses in TOTAL during 1 rounds
c [cce-2] 245 < 1/100 * 1340746 = 13407 considered unsuccessful
c [bca-3] limit of 10000000 steps and 2689078 added (scaled 2)
c [bca-3] 177298 out of 350578 literals actually usable 51%
c [bca-3] added 0 blocked clauses in 396377 steps
c [sweep-3] limit 9951334 penalty 0 = 0 + 0
c [sweep-3-1] 409 pos 0.2% + 174829 neg 99.8% = 175238 sched 100.0% ret 50
c [sweep-3-1] 10707650 steps 21 queries 19492.95 avg class size
c [sweep-3-1] 1099 decisions 18 SAT calls 7528.28 avg env size
c [sweep-3-1] 175029 variables remain 100% (258 retained 0%)
c [decomp-15] removed 5 variables
c [sweep-3-1] removed 5 vars (0 failed, 2 eqs, 4 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 5 vars in TOTAL (1 rounds, 20 queries)
c [score-distribution-7] 171347 pos 97.75%, 942 min 0.54%, 2994 zero 1.71%
c [score-distribution-7] 11883 different 6.78% out of total 175283 variables
c [simplification-7] removed 18 variables 0.0% (175283 remain 88%)
c [simplification-7] removed 15337 irredundant clauses 1.1% (1340491 remain 79%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-7] new conflict interval 27332
c [simplification-7] penalized conflict interval 27332 = 1 * 27332
c [simplification-7] hard conflict limit 79390 (soft 65724 + delta 13666)
c [simplification-7] new conflict limit 65724 (hard 79390)
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  247.8  175282  1340491     39694   20696   2231 63309  167   483  277  35%      9  342  189   43  444%
c i  249.1  175276  1340491     39902   20852   2234 63309  166   473  277  35%      7  331  169   43  394%
c i  251.9  175275  1340491     40504   21339   2255 63315  162   461  277  35%      5  316  184   44  420%
c i  255.3  175256  1340491     41323   22010   2295 63336  166   471  277  35%      4  322  269   45  593%
c i  258.6  175255  1340491     42060   22576   2329 63343  192   509  280  38%      4  356  270   49  555%
c i  258.6  175254  1340491     42061   22576   2329 63343  192   509  280  38%      4  356  269   49  553%
c i  260.8  175233  1340491     42560   23001   2343 63352  189   503  280  38%      3  348  179   49  362%
c i  260.8  175232  1340491     42561   23001   2343 63352  188   503  280  38%      3  348  178   49  360%
c i  262.9  175231  1340491     43100   23404   2374 63359  193   499  280  39%      2  341  185   51  364%
c i  263.5  175229  1340491     43213   23494   2378 63360  194   499  280  39%      2  341  211   51  413%
c i  265.2  175228  1340491     43704   23898   2396 63365  200   505  280  40%      1  344  276   53  524%
c i  266.8  175094  1340491     44079   24206   2420 63369  192   499  280  38%      1  336  140   53  264%
c i  268.1  175073  1340491     44405   24469   2431 63376  193   491  280  39%      1  327  194   54  361%
c i  268.7  175072  1340491     44506   24556   2437 63377  193   494  280  39%      0  330  195   54  361%
c i  274.1  175049  1340491     45632   25480   2472 63389  199   500  291  40%      5  330  300   57  530%
c i  275.1  175033  1340491     45890   25676   2480 63395  198   506  291  39%      4  334  223   57  391%
c i  278.4  175028  1340491     46698   26346   2514 63399  191   488  296  39%      4  312  203   58  349%
c i  278.6  175027  1340491     46741   26385   2516 63399  190   485  296  39%      3  310  179   58  308%
c i  279.1  175026  1340491     46881   26492   2519 63400  190   486  296  39%      3  309  180   59  308%
c i  279.2  175025  1340491     46906   26505   2520 63400  190   484  296  39%      3  308  170   59  291%
c i  281.9  175024  1340491     47491   26955   2541 63410  185   478  313  39%      2  299  158   59  266%
c i  286.4  174891  1340491     48336   27593   2573 63412  184   460  313  40%      3  277  185   61  305%
c i  287.2  174872  1340491     48531   27749   2585 63413  182   461  315  40%      2  277  166   61  272%
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  291.7  174871  1340491     49534   28555   2625 63421  193   477  341  40%      5  289  170   64  268%
c i  296.7  174870  1340491     50596   29386   2659 63430  203   503  421  40%      6  311  278   66  419%
c i  297.1  174869  1340491     50700   29470   2661 63430  202   504  421  40%      5  311  247   67  372%
c i  299.0  174868  1340491     51194   29845   2687 63434  207   503  461  41%      3  308  205   68  302%
c i  299.1  174867  1340491     51236   29874   2689 63438  206   501  461  41%      3  305  190   68  281%
c i  302.8  174866  1340491     52101   30546   2726 63447  210   520  461  40%      4  320  181   70  259%
c i  303.5  174865  1340491     52227   30649   2729 63451  207   511  467  41%      3  311  144   70  205%
c i  306.4  174864  1340491     52856   31145   2748 63459  220   571  467  39%      2  368  235   72  326%
c i  310.0  174862  1340491     53563   31629   2771 63464  251   591  467  42%      3  384  379   76  499%
c i  314.5  174841  1340491     54429   32245   2809 63467  258   602  467  43%      3  390  306   79  389%
c i  315.3  174840  1340491     54614   32403   2813 63470  254   599  467  42%      3  386  239   79  303%
c i  315.4  174839  1340491     54639   32425   2815 63470  253   596  467  42%      2  383  223   79  282%
c i  315.4  174838  1340491     54640   32425   2815 63470  253   596  467  42%      2  382  222   79  281%
c i  318.4  174837  1340491     55177   32801   2828 63479  275   629  467  44%      2  413  339   82  415%
c i  320.4  174836  1340491     55555   33078   2839 63484  298   657  467  45%      1  438  424   84  503%
c i  320.5  174835  1340491     55575   33095   2839 63485  297   658  467  45%      1  439  404   84  479%
c i  321.2  174834  1340491     55750   33216   2846 63487  298   650  476  46%      1  430  346   85  407%
c i  321.8  174833  1340491     55855   33296   2849 63488  293   638  476  46%      0  417  267   85  314%
c i  338.0  174832  1340491     58915   35557   2934 63510  312   668  534  47%     29  426  183   97  189%
c i  339.4  174831  1340491     59180   35744   2941 63513  318   679  534  47%     22  435  307   98  314%
c i  347.9  174808  1340491     60382   36627   2987 63524  308   627  586  49%     11  376  327  101  324%
c i  347.9  174789  1340491     60383   36627   2987 63524  308   627  586  49%     11  376  326  101  322%
c i  349.0  174788  1340491     60519   36724   2989 63525  302   614  616  49%      9  362  243  101  241%
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  350.1  174786  1340491     60729   36875   3000 63533  292   595  616  49%      7  342  171  101  169%
c i  350.3  174763  1340491     60753   36885   3003 63538  291   592  616  49%      7  339  157  101  155%
c i  351.4  174756  1340491     60853   36954   3007 63543  290   588  616  49%      6  335  180  101  178%
c i  351.4  174732  1340491     60854   36954   3007 63543  290   588  616  49%      6  335  180  101  177%
c 0  351.4  174117  1340491     60854   36954   3007 63543  290   588  616  49%      6  335  180  101  177%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 3 count, 15152 added (37 skipped), 1253174 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 2 bces, 646 removed, 8162118 resolutions, 21966525 steps
c blkd: 637 blocking literals 0%, 0 pure
c bump: 59750 bumped seen, 254425651 lits 4258.2 on average
c card: 3 count, 0 units, 9710 am1, 357299372 steps
c card: 25 rescheduled, 233 eliminated, 26355 resolved, 1896 subsumed
c card: 87 at-most-one constraints found, average size 42.21
c card: 87 at-most-one constraints used 100%, average size 42.21
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: 2 cces, 311 eliminated, 311 ate 100%, 0 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: 7303370 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 44 gcs, 0 rescored clauses, 31 rescored vars
c dcps: 15 decompositions, 810 equivalent 0%
c deco: 6846 decision-only clauses 11%, 88% reduction
c decs: 3392186 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 32996470 push, 32739830 pop (32739830 dec 100%)
c dsch: 858250840 swaps, 0 down, 342546479 up
c elms: 5 elims, 6681 eliminated 3%, 0 pure 0%
c elms: 5 rounds, 1.0 rounds/bve
c elms: 4404 small 66%, 2277 large 34%
c elms: 4951 tried small, 4404 succeeded 89%, 547 failed 11%
c elms: 6776 subsumed, 5975 strengthened, 0 blocked
c elms: 6246760 copies, 7017372 resolutions, 80336 ipos
c elms: 24413889 subchks, 19009585 strchks
c gaus: 2 extractions, 3 extracted, 2.3 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10650538 steps, 5325269 extr 50%, 10 elim 0%
c glue: 146.1 orig avg, 146.1 real avg, 4.8 scaled avg
c glue: 58 maxscaledglue=15 (0%), 1 kept 0%
c hbrs: 45786 = 40794 simple 89% + 1288 trn 3% + 3704 lrg 8%, 15 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 59750 clauses, 2295.7 length
c lrnd: 137166311 lits = 183838106 orig - 46671795 removed 25%
c lrnd: 23565 uips 39%, 27278 flips 46%
c mins: 36332 mins 78%, 555 bin 1%, 2646 size 6%
c mins: 30641461 poisoned searches, 14197283 hits, 46% hit rate
c mins: 34892945 used twice searches, 422960 hits, 1% hit rate
c move: moved 461, 460 bin 100%, 1 trn 0%
c otfs: 1130 driving 3%, 37688 restarting 97%
c otfs: str 38818, 38817 red 100%, 1 irr 0%
c otfs: str 38818, 0 bin 0%, 60 trn 0%, 38758 lrg 100%
c otfs: sub 9, 9 red 100%, 0 irr 0%
c otfs: sub 9, 0 bin 0%, 0 trn 0%, 9 lrg 100%
c phas: 1 computed, 185001 set, 0 pos (0%), 185001 neg (100%)
c prbs: 2 basic, 262 probed, 36 failed, 0 lifted
c prbs: 3 simple, 934145 probed, 4871 failed, 256 eqs
c prbs: 2 treelook, 6 probed, 0 failed, 0 lifted
c prom: 0 locked 0% out of 169465 tried
c prps: 1476932076 props, 433 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 2 count, 1 quat, 0 self1, 0 self2, 0 dup
c redc: 4557 clauses 57%, 8024 tried 13%, 4 sat 0%
c redc: 18308 lits 22%, 82160 tried 0%, 4 sat 0%
c redc: 906 times jump level reduced, 74.7 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: 9987 removed, 309 red 3%
c rsts: 4980 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 7 count, 5 confs 71%, 0 vars 0%
c simp: 1 its 14%, 1 bin 14%, 0 trns 0%
c subl: 59750 count (69536 tried 1.2), 6152 sub out of 55982 (11.0%)
c swps: 3 count, 3 rounds, 37 queries (12.3/round)
c swps: 34 sat calls, 2 unsat (0.8% success rate)
c swps: 2003 decisions 58.9, 26 conflicts 0.8
c swps; 32647.7 avg class size, 4938.4 avg environment size
c swps: 0 failed, 8 impls, 3 equivs
c swp0: 11 type 0 queries, 9 unsat (81.8%), 8 sat (72.7%)
c swp1: 26 type 1 queries, 2 unsat (7.7%), 26 sat (100.0%)
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: 6904210 calls to obtain time
c tops: 75772 fixed 29%, 166 its, 366.59 confs/it
c trds: 3 transitive reductions, 100 removed, 0 failed
c trds: 1181 nodes, 5693 edges, 6019650 steps
c trim: 3095481 words, 11.8 MB
c trnr: 3 count, 0 bin, 196 trn, 11088308 steps
c unhd: 7 count, 7 rounds, 42743733 steps
c unhd: 4 non-trivial sccs of average size 2.0
c unhd: 47 units, 47 bin, 0 trn, 0 lrg
c unhd: 40 failed, 34 stamp, 0 lits, 1 bin, 0 trn, 0 lrg
c unhd: 156476 tauts, 19 bin 0%, 19 trn 0%, 236 lrg 0%
c unhd: 156476 tauts, 156202 stamp 100%, 2623 red 2%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 5470437 str, 47 bin 0%, 47 trn 0%, 5470343 lrg 100%, 5470171 red 100%
c vars: 174117 remaining 68% and 83263 removed 32% out of 257380
c vars: 75772 fixed 29%, 6681 eliminated 3%, 810 equivalent 0%
c vsts: 5206498917 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 3.5 search visits per propagation, 84847.7 per conflict
c wchs: 189467488 pushed, 57092836 enlarged, 66 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all          56040             0             0       1872685        502013         69243
c 
c  0 0          8022  14         0   0<        0   0<   825817  44    167841  33      7726  11    10.4
c  1 5          2439   4         0   0         0   0    185659  10     41120   8      3412   5     6.2
c  2 6          6265  11         0   0         0   0    330807  18<    83263  17      9928  14    23.6
c  3 9          7600  14         0   0         0   0    271462  14     75579  15<    11324  16    45.6
c  4 14         6581  12         0   0         0   0    100101   5     42535   8     10255  15<   59.1
c  5 21         4840   9<        0   0         0   0     48900   3     23391   5      6320   9    51.1
c  6 30         3519   6         0   0         0   0     25606   1     14571   3      4487   6    47.3
c  7 41         2677   5         0   0         0   0     14473   1     13436   3      4773   7    39.8
c  8 54         1994   4         0   0         0   0     13791   1      9187   2      2829   4    31.3
c  9 69         1658   3         0   0         0   0     11814   1      6683   1      2037   3    32.4
c 10 86         1429   3         0   0         0   0      9140   0      6195   1      2023   3    18.8
c 11 126        1669   3         0   0         0   0      7462   0      3217   1       573   1     1.5
c 12 230        2482   4         0   0         0   0     13384   1      6087   1      1260   2     3.4
c 13 534        3621   6         0   0         0   0     11536   1      7013   1      1766   3    10.8
c 14 1526       1187   2         0   0         0   0      2676   0      1895   0       530   1    10.1
c 15 5046         57   0         0   0         0   0        57   0         0   0         0   0     0.1
c 
c avg                  5.1           0.0           0.0           1.8           2.6           4.4
c std                  4.1           0.0           0.0           2.4           3.0           3.3
c 
c   37.615  11% elim
c   35.668  10% bump
c   16.877   5% block
c   15.911   5% unhide
c   14.550   4% decide
c   12.962   4% probe
c    3.329   1% cce
c    2.698   1% sweep
c    1.577   0% card
c 
c    3.524 < 1% rest (below)
c 
c    1.548   0% bca
c    1.402   0% gauss
c    0.230   0% rescore
c    0.200   0% ternres
c    0.118   0% transred
c    0.025   0% quatres
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    8.322   2% preprocessing     8%
c   91.789  26% inprocessing     92%
c ==================================
c  100.110  28% simplifying
c  251.308  72% search
c ==================================
c  351.422 100% all
c 
c         60854 conflicts,         173.2 confs/sec
c          2675 ternaries,          22.7 confs/ternary
c           864 binaries,           70.4 confs/binary
c           166 iterations,        366.6 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          4980 restarts,           14.2 rests/sec,     12.2 confs/restart
c       3392186 decisions,        9652.7 decis/sec,     55.7 decis/conflict
c    1476932076 propagations,  4202729.1 props/sec,    435.4 props/decision
c 
c 351.4 seconds, 616.4 MB
c launch: done
