c launch: /data/cnf/sc2014/app/transport-transport-city-sequential-25nodes-1000size-3degree-100mindistance-3trucks-10packages-2008seed.020-NOTKNOWN.cnf.bz2
c host: atom10
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/transport-transport-city-sequential-25nodes-1000size-3degree-100mindistance-3trucks-10packages-2008seed.020-NOTKNOWN.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/transport-transport-city-sequential-25nodes-1000size-3degree-100mindistance-3trucks-10packages-2008seed.020-NOTKNOWN.cnf.bz2
c no embedded options
c found 'p cnf 241290 1289940' header
c read 241290 variables, 1289940 clauses, 3070540 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=3
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 209710 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] SUM (--score=3)
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  209710  1016580         0       0      0     0    0     0   41   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 6442 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6442 out of 6442 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 40642 variables
c [simpleprobe-1] all 200648 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 204 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 204 variables, found 395 hbrs, 82 units
c [unhide-1] limit 57353 based on 917654 irredundant clauses
c [unhide-1-1] 0 units, 1 failed, 25421 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 200443 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 1985 not tried 1% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 82171 = 41% variables out of 200443 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 828606 negative 100.0% of 828634 except 28 0.0%
c [phase-count-1] 506992 positive 61.2% of 828634 except 321642 38.8%
c [phase-count-1] less non-negative clauses 28 than limit 82800 (10.0%)
c [phase-count-1] non-pos/non-neg = 321642/28 = 11487.21 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 118272 negative 100%
c [sort-queue-1] sorted 118272 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 118272 (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 82438 variables 41.1% (118272 remain 56%)
c [simplification-1] removed 187946 irredundant clauses 18.5% (828634 remain 82%)
c [simplification-1] maximum reduction of 41% = max (41%, 18%)
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.7  118271   828634         3       1      1   386    0     0   37  50%      0    0    0    0 25403%
c i    4.7  118270   828634         4       1      1   386    0     0   37  50%      0    0    0    0 25304%
c i    4.7  118269   828634         5       1      1   386    0     0   37  50%      0    0    0    0 25206%
c i    4.7  118268   828634        16      11      1   386    0     2   37  10%      0    2    3    0 24788%
c i    4.8  118252   828634        79      68      1   386    0     7   38   6%      0    7    6    0 21649%
c i    4.8  118243   828634        95      83      1   386    0     7   38   6%      0    7    6    0 20706%
c i    5.0  118045   828634       208     195      1   386    2    30   39   6%      0   30   20    0 18366%
c i    5.0  118044   828634       209     195      1   386    2    30   39   6%      0   30   20    0 18294%
c i    5.0  118043   828634       210     195      1   386    2    30   39   6%      0   30   20    0 18223%
c i    5.0  118042   828634       270     247      1   387    3    45   39   6%      0   45   30    0 17162%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 234 variables
c [simpleprobe-2] all 118038 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 4 variables
c [simpleprobe-2] 83068 variables remain 70% (34966 retained 30%)
c [simpleprobe-2] removed 4 variables, found 936 hbrs, 4 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 84718 literals 36%
c [treelook-1] scheduling used 300123 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 439585 steps
c [treelook-1] 84710 literals remain 36%
c [treelook-1] 84563 variables remain to probed next time 72%
c [treelook-1] removed 3 variables, found 390 hbrs
c [basicprobe-1] limit 6612880 based on 826610 irredundant clauses
c [basicprobe-1-0] 83854 probes remain 71% after last round
c [basicprobe-1-0] 15 units = 15 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 45 variables, found 596 hbrs
c [unhide-2] limit 51663 based on 826610 irredundant clauses
c [unhide-2-2] 11 units, 15 failed, 6 tauts, 0 hbrs, 2128 literals
c [elim-2] 1983 variables 2% will be scheduled this time
c [elim-2] scheduled 1983 variables 2%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 573 not tried 0% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 0 = 0% variables out of 1983 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 822595 negative 100.0% of 822623 except 28 0.0%
c [phase-count-2] 502287 positive 61.1% of 822623 except 320336 38.9%
c [phase-count-2] less non-negative clauses 28 than limit 82200 (10.0%)
c [phase-count-2] non-pos/non-neg = 320336/28 = 11440.57 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 27889 negative 100%
c [sort-queue-2] sorted 65328 enqueued variables after 270 conflicts
c [score-dist-2] active 52595 (45%), one 0 (0%), zero 65328 (55%)
c [score-dist-2] max exp 513, different 12 (2%)
c [score-dist-2] median active exp 509, avg 508.7
c [simplification-2] removed 119 variables 0.1% (117923 remain 56%)
c [simplification-2] removed 6011 irredundant clauses 0.7% (822623 remain 81%)
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 1043 (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.7  117922   822623       272     248      1  2274    3    45   38   6%      0   45   30    0 17035%
c i    7.7  117921   822623       273     248      1  2274    3    45   38   6%      0   45   30    0 16969%
c i    7.7  117920   822623       274     248      1  2274    3    45   38   6%      0   45   29    0 16903%
c i    7.7  117919   822623       279     251      1  2274    3    45   38   6%      0   45   29    0 16653%
c i    8.2  117918   822623       619     560      3  2277    5    83   39   6%      1   82   25    0 8059%
c i    8.2  117917   822623       621     560      3  2277    5    83   39   6%      1   82   25    0 7999%
c i    8.2  117916   822623       622     560      3  2277    5    83   39   6%      1   82   25    0 7968%
c i    8.2  117915   822623       623     560      3  2277    5    83   39   6%      1   82   25    0 7937%
c i    8.2  117914   822623       624     560      3  2277    5    83   39   6%      1   82   25    0 7906%
c i    8.8  117913   822623       987     863      5  2282    8   104   41   7%      2  103   39    1 7358%
c 
c [simplification-3] limit 1105 conflicts (hard 11000) hit after 1108 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1112 at-most-one constraints of average size 4.1
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 1112 out of 1112 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 12 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 85433 literals 36%
c [treelook-2] scheduling used 301466 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 318378 steps
c [treelook-2] 85430 literals remain 36%
c [treelook-2] 81812 variables remain to probed next time 69%
c [treelook-2] removed 0 variables, found 226 hbrs
c [unhide-3] limit 51407 based on 822525 irredundant clauses
c [unhide-3-3] 0 units, 4 failed, 21035 tauts, 0 hbrs, 17743 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 117901 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 16316 not tried 14% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1696 = 1% variables out of 117901 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 798743 negative 100.0% of 798773 except 30 0.0%
c [phase-count-3] 500866 positive 62.7% of 798773 except 297907 37.3%
c [phase-count-3] less non-negative clauses 30 than limit 79800 (10.0%)
c [phase-count-3] non-pos/non-neg = 297907/30 = 9930.23 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 26792 negative 100%
c [sort-queue-3] sorted 32161 enqueued variables after 1108 conflicts
c [score-dist-3] active 84044 (72%), one 0 (0%), zero 32161 (28%)
c [score-dist-3] max exp 518, different 16 (3%)
c [score-dist-3] median active exp 513, avg 513.0
c [simplification-3] removed 1708 variables 1.4% (116205 remain 55%)
c [simplification-3] removed 23850 irredundant clauses 2.9% (798773 remain 79%)
c [simplification-3] maximum reduction of 3% = max (1%, 3%)
c [simplification-3] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-3] new conflict interval 5000
c [simplification-3] penalized conflict interval 5000 = 1 * 5000
c [simplification-3] hard conflict limit 16108 (soft 6108 + delta 10000)
c [simplification-3] new conflict limit 6108 (hard 16108)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   17.1  116204   798773      1157     802      7  2507   28   134   39  21%      1  133  277    2 14889%
c i   17.1  116203   798773      1163     805      9  2507   29   135   39  21%      1  134  278    2 14712%
c i   17.1  116202   798773      1164     805      9  2507   29   135   39  21%      1  133  277    2 14654%
c i   17.1  116201   798773      1165     805      9  2507   29   135   39  21%      1  133  275    2 14597%
c i   17.1  116200   798773      1167     805      9  2507   29   135   39  21%      1  133  274    2 14541%
c i   17.1  116199   798773      1168     805      9  2507   29   135   39  21%      1  133  273    2 14484%
c i   17.1  116198   798773      1170     806      9  2507   29   135   39  21%      1  133  274    2 14437%
c i   17.1  116197   798773      1171     806      9  2507   29   135   39  21%      1  133  273    2 14381%
c i   17.1  116196   798773      1172     806      9  2507   29   135   39  21%      1  133  272    2 14325%
c i   17.2  116195   798773      1215     831      9  2508   34   141   40  24%      1  140  318    2 14053%
c i   17.2  116194   798773      1225     836      9  2508   35   142   40  25%      1  141  319    2 13802%
c i   17.2  116179   798773      1228     838      9  2508   35   143   40  25%      1  141  318    2 13696%
c i   17.2  116164   798773      1229     838      9  2508   35   143   40  25%      1  141  317    2 13643%
c i   17.2  116153   798773      1230     838      9  2508   35   143   40  25%      1  141  316    2 13590%
c i   17.2  116138   798773      1233     840      9  2508   35   143   40  25%      1  141  315    2 13486%
c i   17.2  116124   798773      1234     840      9  2508   35   143   40  25%      1  141  314    2 13434%
c i   17.2  116113   798773      1274     872      9  2510   37   148   40  25%      1  146  304    2 12215%
c i   17.2  116098   798773      1276     873      9  2510   37   148   40  25%      1  146  302    2 12132%
c i   17.2  116083   798773      1320     908      9  2513   38   152   40  25%      1  151  275    3 10731%
c i   17.2  116072   798773      1340     925      9  2513   39   155   40  25%      1  153  271    3 10319%
c i   17.2  116057   798773      1364     944      9  2513   40   157   40  26%      1  156  273    3 10016%
c i   17.3  116049   798773      1441    1006      9  2513   47   166   40  28%      1  164  304    3 9629%
c i   17.3  116032   798773      1453    1007      9  2513   48   167   40  29%      1  165  310    3 9623%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   17.3  116015   798773      1588    1115     10  2513   59   181   41  33%      1  178  353    4 8781%
c i   17.4  115998   798773      1589    1115     10  2513   59   180   41  33%      1  178  352    4 8747%
c i   17.4  115981   798773      1590    1115     10  2513   59   180   41  33%      1  178  350    4 8713%
c i   17.4  115964   798773      1592    1116     10  2513   59   180   41  33%      1  178  348    4 8650%
c i   17.4  115947   798773      1593    1116     10  2513   59   180   41  33%      1  178  346    4 8616%
c i   17.4  115930   798773      1594    1116     10  2513   59   180   41  33%      1  178  345    4 8582%
c i   17.4  115913   798773      1596    1116     10  2513   59   180   41  33%      1  178  344    4 8549%
c i   17.4  115896   798773      1597    1116     10  2513   59   180   41  33%      1  178  342    4 8516%
c i   17.4  115879   798773      1598    1116     10  2513   59   180   41  33%      1  178  341    4 8483%
c i   17.4  115862   798773      1599    1116     10  2513   59   180   41  33%      1  178  340    4 8450%
c i   17.4  115845   798773      1600    1116     10  2513   59   180   41  33%      1  178  338    4 8417%
c i   17.4  115828   798773      1601    1116     10  2513   59   180   41  33%      1  178  337    4 8384%
c i   17.4  115811   798773      1611    1115     11  2514   59   180   41  33%      1  178  334    4 8231%
c i   17.4  115810   798773      1612    1115     11  2514   59   180   41  33%      1  178  332    4 8199%
c i   17.4  115809   798773      1668    1152     12  2516   61   183   41  33%      1  181  310    4 7315%
c i   17.4  115808   798773      1669    1152     12  2516   61   183   41  33%      1  181  309    4 7286%
c 
c [simplification-4] limit 6332 conflicts (hard 16108) hit after 6332 conflicts
c [decomp-8] removed 409 variables
c [basicprobe-2] limit 12939197 penalty 0 = 0 + 0
c [basicprobe-2-0] 81651 probes remain 71% after last round
c [basicprobe-2-0] 22 units = 22 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 38 variables, found 1069 hbrs
c [unhide-4] limit 129391 with penalty 2 = 0 + 2
c [unhide-4-4] 2 units, 7 failed, 1 tauts, 0 hbrs, 161654 literals
c [elim-4] 573 variables 0% will be scheduled this time
c [elim-4] scheduled 573 variables 0%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1035135800 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 261132350 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 573 scheduled
c [phase-count-4] 794097 negative 100.0% of 794127 except 30 0.0%
c [phase-count-4] 498488 positive 62.8% of 794127 except 295639 37.2%
c [phase-count-4] less non-negative clauses 30 than limit 79400 (10.0%)
c [phase-count-4] non-pos/non-neg = 295639/30 = 9854.63 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 25003 negative 100%
c [sort-queue-4] sorted 28257 enqueued variables after 6332 conflicts
c [score-dist-4] active 87477 (76%), one 0 (0%), zero 28257 (24%)
c [score-dist-4] max exp 525, different 22 (4%)
c [score-dist-4] median active exp 519, avg 519.1
c [simplification-4] removed 62 variables 0.1% (115734 remain 55%)
c [simplification-4] removed 4646 irredundant clauses 0.6% (794127 remain 78%)
c [simplification-4] maximum reduction of 1% = max (0%, 1%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 15000
c [simplification-4] penalized conflict interval 15000 = 1 * 15000
c [simplification-4] hard conflict limit 31332 (soft 21332 + delta 10000)
c [simplification-4] new conflict limit 21332 (hard 31332)
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   40.2  115733   794127      8902    4642     12  3531  588   884   82  66%     92  827  919   66 1402%
c i   40.3  115716   794127      8933    4669     12  3531  585   886   82  66%     89  829  836   66 1275%
c i   40.3  115699   794127      8942    4676     12  3531  584   886   82  66%     89  829  812   66 1238%
c i   40.3  115682   794127      8992    4717     12  3531  578   889   82  65%     84  831  686   66 1046%
c i   41.5  115665   794127      9680    5071     12  3532  607   935   84  65%     43  869  785   73 1079%
c i   41.7  115652   794127      9814    5168     12  3540  598   942   84  63%     37  874  604   73  824%
c i   42.1  115635   794127     10067    5334     12  3542  598   955   84  63%     28  883  615   75  818%
c i   42.8  115618   794127     10483    5549     12  3543  612   974   86  63%     18  897  764   79  963%
c i   42.8  115603   794127     10506    5556     12  3543  613   975   86  63%     17  898  776   80  974%
c i   42.9  115588   794127     10531    5562     12  3543  616   976   86  63%     17  898  799   80  999%
c i   42.9  115573   794127     10532    5562     12  3543  616   976   86  63%     17  898  796   80  995%
c i   45.5  115558   794127     11879    5838     12  3548  725   999   99  73%      9  902  961   99  972%
c i   45.5  115541   794127     11880    5838     12  3548  725   998   99  73%      9  902  957   99  968%
c i   45.5  115524   794127     11881    5838     12  3548  725   998   99  73%      9  902  953   99  964%
c i   45.6  115507   794127     11972    5861     12  3548  729   997   99  73%      8  899  935  100  935%
c i   45.6  115490   794127     11973    5861     12  3548  728   997   99  73%      8  899  931  100  931%
c i   45.6  115473   794127     11974    5861     12  3548  728   996   99  73%      8  899  927  100  928%
c i   45.7  115456   794127     11975    5861     12  3548  728   996   99  73%      8  898  924  100  924%
c i   45.7  115439   794127     11981    5862     12  3548  728   996   99  73%      8  898  918  100  918%
c i   45.7  115422   794127     11982    5862     12  3548  728   996   99  73%      8  898  915  100  914%
c i   45.7  115405   794127     11983    5862     12  3548  728   995   99  73%      8  897  911  100  911%
c i   45.7  115388   794127     11984    5862     12  3548  727   995   99  73%      8  897  907  100  907%
c i   45.7  115371   794127     11985    5862     12  3548  727   995   99  73%      8  897  904  100  904%
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.7  115354   794127     12010    5877     12  3548  726   995   99  73%      8  896  873  100  871%
c i   45.7  115337   794127     12011    5877     12  3548  726   994   99  73%      8  896  869  100  868%
c i   47.8  115320   794127     13182    6107     12  3548  753   965   99  78%      6  851  792  113  700%
c i   48.2  115312   794127     13472    6179     12  3548  749   949   99  79%      3  831  715  116  618%
c i   48.6  115297   794127     13670    6268     12  3549  742   935   99  79%      2  815  656  117  560%
c i   48.6  115281   794127     13681    6273     12  3554  741   934   99  79%      2  814  640  117  546%
c i   48.6  115264   794127     13686    6277     12  3554  741   933   99  79%      2  813  636  117  543%
c i   48.6  115253   794127     13687    6277     12  3554  740   933   99  79%      2  813  634  117  541%
c i   48.6  115236   794127     13720    6280     12  3554  739   930   99  79%      2  810  628  117  534%
c i   48.6  115221   794127     13721    6280     12  3554  739   930   99  79%      2  809  625  117  532%
c i   48.6  115206   794127     13722    6280     12  3554  739   930   99  79%      2  809  623  117  530%
c i   48.6  115191   794127     13723    6280     12  3554  739   930   99  79%      2  809  620  117  528%
c i   48.6  115176   794127     13726    6281     12  3554  738   929   99  79%      2  809  617  117  526%
c i   48.6  115175   794127     13727    6281     12  3554  738   929   99  79%      2  808  615  117  523%
c i   48.7  115164   794127     13728    6281     12  3554  738   929   99  79%      2  808  612  117  521%
c i   48.7  115149   794127     13729    6281     12  3554  738   929   99  79%      2  808  610  117  519%
c i   48.7  115148   794127     13730    6281     12  3554  738   928   99  79%      2  808  608  117  517%
c i   48.7  115147   794127     13734    6284     12  3554  737   928   99  79%      1  807  604  117  514%
c i   48.7  115146   794127     13744    6293     12  3554  737   927   99  79%      1  806  599  118  510%
c i   48.7  115131   794127     13767    6309     14  3554  734   925   99  79%      1  803  564  118  480%
c i   48.7  115116   794127     13768    6309     14  3554  733   924   99  79%      1  803  562  118  478%
c i   48.7  115101   794127     13769    6309     14  3554  733   924   99  79%      1  803  560  118  476%
c i   48.7  115087   794127     13770    6309     14  3554  733   924   99  79%      1  803  557  118  474%
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  115072   794127     13772    6309     14  3554  733   924   99  79%      1  802  555  118  472%
c i   48.7  115071   794127     13773    6309     14  3554  733   923   99  79%      1  802  553  118  470%
c i   48.7  115070   794127     13786    6316     14  3554  732   922   99  79%      1  800  545  118  464%
c i   48.8  115069   794127     13807    6324     14  3555  730   920   99  79%      1  798  530  118  450%
c i   48.8  115068   794127     13810    6326     14  3555  729   919   99  79%      1  798  526  118  447%
c i   48.8  115067   794127     13811    6326     14  3555  729   919   99  79%      1  797  524  118  445%
c i   48.8  115066   794127     13813    6325     14  3555  729   919   99  79%      1  797  522  118  443%
c i   48.8  115065   794127     13832    6333     14  3555  727   917   99  79%      1  795  509  118  433%
c i   48.8  115064   794127     13833    6333     14  3555  727   917   99  79%      1  794  507  118  431%
c i   48.8  115063   794127     13835    6334     14  3555  727   916   99  79%      1  794  504  118  428%
c i   48.8  115062   794127     13836    6334     14  3555  727   916   99  79%      1  794  502  118  426%
c i   48.8  115061   794127     13838    6335     14  3555  726   916   99  79%      1  794  500  118  424%
c i   48.9  115060   794127     13885    6364     15  3555  721   911   99  79%      0  788  461  118  391%
c i   49.1  115059   794127     14044    6415     17  3555  707   895   99  79%     -0  770  416  118  351%
c i   49.4  115058   794127     14247    6571     17  3559  678   875  100  78%     -1  748  238  118  201%
c i   50.0  115043   794127     14636    6687     17  3562  650   837  100  78%     -2  706  347  120  289%
c i   50.1  115030   794127     14685    6710     20  3564  646   833  100  78%     -2  701  331  120  276%
c i   50.5  115013   794127     15095    6951     24  3568  608   804  100  76%     -2  668  260  121  215%
c i   52.5  115012   794127     16475    7116     24  3582  577   727  104  79%      5  578  505  129  393%
c i   52.7  115011   794127     16616    7186     24  3584  569   720  104  79%      3  570  425  129  330%
c i   52.7  115010   794127     16617    7186     24  3584  569   720  104  79%      3  570  424  129  329%
c i   54.2  115009   794127     17657    7443     24  3588  531   666  104  80%      3  508  349  133  262%
c i   54.2  115008   794127     17664    7449     24  3588  530   666  104  80%      3  507  341  133  256%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   54.3  115007   794127     17666    7450     24  3588  530   666  104  80%      3  507  339  133  254%
c i   54.3  115006   794127     17677    7458     24  3588  529   665  104  79%      3  506  331  133  248%
c i   54.3  115005   794127     17678    7458     24  3588  529   665  104  79%      3  506  329  133  247%
c i   55.3  115004   794127     18729    8081     26  3591  466   624  104  75%      3  458  248  135  184%
c i   55.4  114987   794127     18846    8142     26  3591  460   620  104  74%      2  452  250  135  185%
c i   55.4  114970   794127     18934    8184     26  3592  456   616  112  74%      2  448  257  135  190%
c i   56.0  114957   794127     19497    8433     27  3595  441   596  112  74%      0  425  322  137  235%
c i   56.0  114956   794127     19540    8451     28  3595  440   595  112  74%      0  423  327  137  239%
c i   56.1  114943   794127     19544    8454     28  3595  440   595  112  74%      0  423  328  137  239%
c i   56.3  114942   794127     19820    8572     28  3597  438   586  112  75%     -1  412  367  138  265%
c i   56.6  114941   794127     20120    8766     28  3597  425   576  112  74%     -2  401  300  139  216%
c i   56.9  114924   794127     20635    9040     28  3597  405   561  112  72%     -2  383  274  140  196%
c 
c [simplification-5] limit 21653 conflicts (hard 31332) hit after 21656 conflicts
c [quatres-1] found 448 quaternary clauses 4% in total
c [quatres-1-2] added 2 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 33769485 with penalty 0 = 0 + 0
c [ternres-1] all 114918 free variables schedulable
c [ternres-1] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 80874 schedulable variables 70%
c [simpleprobe-3] limit 27015590 penalty 0 = 0 + 0
c [decomp-10] removed 4973 variables
c [simpleprobe-3] 774 variables remain 1% (109171 retained 99%)
c [simpleprobe-3] removed 4973 variables, found 35094 hbrs, 2518 units
c [unhide-5] limit 337694 with penalty 2 = 0 + 2
c [unhide-5-5] 0 units, 2 failed, 16735 tauts, 0 hbrs, 125666 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 15 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 109937 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 675389750 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 2411 blocked clauses
c [block-1] 2411 < 1/100 * 724685 = 7246 considered unsuccessful
c [cce-1] limit of 33769487 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 78 clauses out of 155 (50%) of length 502
c [cce-1-1] eliminated 3 clauses out of 7 (43%) of length 501
c [cce-1-1] eliminated 8 clauses out of 15 (53%) of length 498
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 497
c [cce-1-1] eliminated 3 clauses out of 5 (60%) of length 413
c [cce-1-1] eliminated 4 clauses out of 7 (57%) of length 363
c [cce-1-1] eliminated 5 clauses out of 9 (56%) of length 362
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 342
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 341
c [cce-1-1] eliminated 3 clauses out of 6 (50%) of length 317
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 312
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 311
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 284
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 281
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 262
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 261
c [cce-1-1] eliminated 55 clauses out of 112 (49%) of length 252
c [cce-1-1] eliminated 3 clauses out of 4 (75%) of length 251
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 250
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 249
c [cce-1-1] eliminated 3 clauses out of 7 (43%) of length 248
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 247
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 242
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 234
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 229
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 177
c [cce-1-1] eliminated 4 clauses out of 8 (50%) of length 167
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 164
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 152
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 147
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 141
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 138
c [cce-1-1] eliminated 3 clauses out of 4 (75%) of length 135
c [cce-1-1] eliminated 2 clauses out of 5 (40%) of length 134
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 130
c [cce-1-1] eliminated 3 clauses out of 7 (43%) of length 114
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 113
c [cce-1-1] eliminated 259 clauses out of 653 (40%) of length 102
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 464 large clauses in 33769491 steps
c [cce-1-1] allowing another 16884745 steps for small clauses
c [cce-1-1] scheduling 710078 clauses = 709963 binary + 115 ternary
c [cce-1-1] tried to eliminate 482 small clauses 0%
c [cce-1-1] eliminated 70 binary clauses 0%
c [cce-1-1] eliminated 70 small clauses 0%
c [cce-1-1] eliminated 70 small clauses in 33769494 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 534 covered clauses in round 1
c [cce-1] eliminated 534 covered clauses in TOTAL during 1 rounds
c [cce-1] 534 < 1/100 * 722215 = 7222 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1443862 added (scaled 2)
c [bca-1] 139571 out of 217450 literals actually usable 64%
c [bca-1] added 0 blocked clauses in 291539 steps
c [sweep-1] limit 2026169 penalty 0 = 0 + 0
c [sweep-1-1] 1973 pos 1.8% + 106751 neg 98.2% = 108724 sched 100.0% ret 0
c [sweep-1-1] 2064745 steps 42 queries 17956.29 avg class size
c [sweep-1-1] 743 decisions 40 SAT calls 727.35 avg env size
c [sweep-1-1] 108399 variables remain 100% (325 retained 0%)
c [decomp-11] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 1 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1 vars in TOTAL (1 rounds, 41 queries)
c [phase-count-5] 721651 negative 100.0% of 721681 except 30 0.0%
c [phase-count-5] 464259 positive 64.3% of 721681 except 257422 35.7%
c [phase-count-5] less non-negative clauses 30 than limit 72100 (10.0%)
c [phase-count-5] non-pos/non-neg = 257422/30 = 8580.73 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 23154 negative 100%
c [sort-queue-5] sorted 26586 enqueued variables after 21656 conflicts
c [score-dist-5] active 82137 (76%), one 0 (0%), zero 26586 (24%)
c [score-dist-5] max exp 529, different 24 (5%)
c [score-dist-5] median active exp 520, avg 520.7
c [simplification-5] removed 6195 variables 5.4% (108723 remain 52%)
c [simplification-5] removed 72446 irredundant clauses 9.1% (721681 remain 71%)
c [simplification-5] maximum reduction of 9% = max (5%, 9%)
c [simplification-5] large reduction 9% >= 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 33656 (soft 23656 + delta 10000)
c [simplification-5] new conflict limit 23656 (hard 33656)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   66.3  108722   721681     21666    9548     36 38031  376   533   70  70%      2  349  263  142  185%
c i   66.5  108706   721681     21844    9669     36 38031  367   528   82  69%      1  343  219  142  154%
c i   67.0  108689   721681     22653   10166     36 38031  337   511   84  66%      1  322  220  143  154%
c i   67.0  108672   721681     22654   10166     36 38031  337   511   84  66%      1  322  219  143  154%
c i   67.1  108655   721681     22813   10252     36 38031  332   508   84  65%      0  318  222  143  156%
c i   67.1  108638   721681     22815   10253     36 38031  332   507   84  65%     -0  318  222  143  156%
c i   67.2  108621   721681     22839   10267     36 38031  332   507   84  65%     -0  317  221  143  155%
c i   67.3  108604   721681     23012   10353     36 38031  327   502   84  65%     -1  311  219  143  153%
c i   67.3  108587   721681     23013   10353     36 38031  327   501   84  65%     -1  311  218  143  153%
c i   67.3  108570   721681     23014   10353     36 38031  327   501   84  65%     -1  311  217  143  152%
c i   67.3  108553   721681     23058   10378     36 38031  325   500   84  65%     -1  309  207  143  145%
c i   67.5  108537   721681     23243   10449     36 38031  323   495   84  65%     -2  303  244  143  170%
c i   67.5  108520   721681     23244   10449     36 38031  323   495   84  65%     -2  303  243  143  169%
c i   67.5  108503   721681     23319   10466     36 38031  323   493   84  65%     -2  301  263  143  183%
c i   67.5  108486   721681     23320   10466     36 38031  323   493   84  65%     -2  300  262  143  182%
c i   67.5  108473   721681     23323   10467     36 38031  323   493   84  65%     -2  300  260  143  181%
c i   67.6  108460   721681     23438   10498     36 38031  322   490   84  66%     -2  297  274  144  191%
c i   67.7  108459   721681     23491   10518     36 38031  321   488   84  66%     -2  295  273  144  190%
c i   67.7  108442   721681     23509   10525     36 38031  321   488   84  66%     -3  294  272  144  189%
c i   67.9  108425   721681     23774   10626     36 38031  319   481   84  66%     -3  287  286  144  198%
c i   68.3  108408   721681     24174   10758     36 38031  319   474   84  67%     -3  278  305  146  209%
c i   68.3  108391   721681     24175   10758     36 38031  319   474   84  67%     -3  278  304  146  209%
c i   68.5  108374   721681     24431   10841     36 38031  316   470   84  67%     -3  273  263  146  180%
c 
c [simplification-6] limit 23724 conflicts (hard 33656) hit after 25336 conflicts
c [quatres-2] found 437 quaternary clauses 4% in total
c [ternres-2] limit 7294912 with penalty 0 = 0 + 0
c [ternres-2] all 108368 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 911864 penalty 2 = 2 + 0
c [card-3] found 906 at-most-one constraints of average size 4.4
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 911864 for elimination
c [card-3] 906 out of 906 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 355 variables
c [unhide-6] limit 364745 with penalty 2 = 0 + 2
c [unhide-6-6] 0 units, 3 failed, 328 tauts, 0 hbrs, 261421 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 21 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 108366 variables 100%
c [elim-5] limit of 72949120 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 230 not tried 0% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2014 = 2% variables out of 108366 scheduled
c [sweep-2] limit 2188473 penalty 0 = 0 + 0
c [sweep-2-1] 2067 pos 1.9% + 103966 neg 98.1% = 106033 sched 99.7% ret 319
c [sweep-2-1] 2320972 steps 32 queries 16802.09 avg class size
c [sweep-2-1] 864 decisions 31 SAT calls 1004.87 avg env size
c [sweep-2-1] 105462 variables remain 99% (890 retained 1%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 31 queries)
c [phase-count-6] 714534 negative 100.0% of 714563 except 29 0.0%
c [phase-count-6] 457073 positive 64.0% of 714563 except 257490 36.0%
c [phase-count-6] less non-negative clauses 29 than limit 71400 (10.0%)
c [phase-count-6] non-pos/non-neg = 257490/29 = 8878.97 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 21173 negative 100%
c [sort-queue-6] sorted 24631 enqueued variables after 25336 conflicts
c [score-dist-6] active 81721 (77%), one 0 (0%), zero 24631 (23%)
c [score-dist-6] max exp 529, different 23 (4%)
c [score-dist-6] median active exp 521, avg 521.2
c [simplification-6] removed 2016 variables 1.9% (106352 remain 51%)
c [simplification-6] removed 7118 irredundant clauses 1.0% (714563 remain 70%)
c [simplification-6] maximum reduction of 2% = max (2%, 1%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 21666
c [simplification-6] penalized conflict interval 21666 = 1 * 21666
c [simplification-6] hard conflict limit 57835 (soft 47002 + delta 10833)
c [simplification-6] new conflict limit 47002 (hard 57835)
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   77.9  106351   714563     25454   11031     35 37654  261   517   78  50%      1  316   41  145   28%
c i   77.9  106334   714563     25455   11031     35 37654  261   517   78  50%      1  316   41  145   28%
c i   92.3  106317   714563     32897   13936     63 37688  401   579  106  69%     90  340  185  175  105%
c 
c [simplification-7] limit 47012 conflicts (hard 57835) hit after 47013 conflicts
c [gauss-2] limit 1187388 penalty 1 = 1 + 0
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-3] limit 593694 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 90360 literals 42%
c [treelook-3] scheduling used 593722 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 593694 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 624601 steps
c [treelook-3] 90351 literals remain 42%
c [treelook-3] 74463 variables remain to probed next time 70%
c [treelook-3] removed 0 variables, found 358 hbrs
c [unhide-7] limit 296847 with penalty 3 = 0 + 3
c [unhide-7-7] 0 units, 2 failed, 10764 tauts, 0 hbrs, 520651 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 8 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 106315 variables 100%
c [block-2] limit of 59369443 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 29684721 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 216
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 215
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 127
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 126
c [cce-2-1] eliminated 61 clauses out of 394 (15%) of length 102
c [cce-2-1] eliminated 3 clauses out of 13 (23%) of length 101
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 99
c [cce-2-1] eliminated 3 clauses out of 8 (38%) of length 98
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 97
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 96
c [cce-2-1] eliminated 2 clauses out of 7 (29%) of length 94
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 93
c [cce-2-1] eliminated 3 clauses out of 7 (43%) of length 92
c [cce-2-1] eliminated 3 clauses out of 11 (27%) of length 90
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 89
c [cce-2-1] eliminated 6 clauses out of 12 (50%) of length 86
c [cce-2-1] eliminated 2 clauses out of 3 (67%) of length 84
c [cce-2-1] eliminated 2 clauses out of 5 (40%) of length 82
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 81
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 70
c [cce-2-1] eliminated 2 clauses out of 7 (29%) of length 66
c [cce-2-1] eliminated 4 clauses out of 9 (44%) of length 65
c [cce-2-1] eliminated 1 clauses out of 3 (33%) of length 64
c [cce-2-1] eliminated 9 clauses out of 11 (82%) of length 62
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 61
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 59
c [cce-2-1] eliminated 6 clauses out of 9 (67%) of length 58
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 55
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 53
c [cce-2-1] eliminated 6 clauses out of 10 (60%) of length 50
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 47
c [cce-2-1] eliminated 3 clauses out of 7 (43%) of length 42
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 36
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 35
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 27
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 26
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 25
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 23
c [cce-2-1] eliminated 4 clauses out of 13 (31%) of length 22
c [cce-2-1] eliminated 2 clauses out of 5 (40%) of length 21
c [cce-2-1] eliminated 3 clauses out of 6 (50%) of length 17
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 16
c [cce-2-1] eliminated 471 clauses out of 5813 (8%) of length 14
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 625 large clauses in 29684722 steps
c [cce-2-1] allowing another 14842361 steps for small clauses
c [cce-2-1] scheduling 693829 clauses = 693497 binary + 332 ternary
c [cce-2-1] tried to eliminate 343 small clauses 0%
c [cce-2-1] eliminated 71 binary clauses 0%
c [cce-2-1] eliminated 71 small clauses 0%
c [cce-2-1] eliminated 71 small clauses in 29684773 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 696 covered clauses in round 1
c [cce-2] eliminated 696 covered clauses in TOTAL during 1 rounds
c [cce-2] 696 < 1/100 * 703464 = 7034 considered unsuccessful
c [elim-6] 230 variables 0% will be scheduled this time
c [elim-6] scheduled 230 variables 0%
c [elim-6] limit of 237477773 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 175810247 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 230 scheduled
c [bca-2] limit of 10000000 steps and 1406036 added (scaled 2)
c [bca-2] 132971 out of 212632 literals actually usable 63%
c [bca-2] added 4635 blocked clauses in 299296 steps
c [sweep-3] limit 3562166 penalty 0 = 0 + 0
c [sweep-3-1] 2612 pos 2.5% + 102813 neg 97.5% = 105425 sched 99.2% ret 890
c [sweep-3-1] 3632371 steps 54 queries 11545.78 avg class size
c [sweep-3-1] 1536 decisions 50 SAT calls 824.88 avg env size
c [sweep-3-1] 103642 variables remain 97% (2673 retained 3%)
c [decomp-16] removed 4 variables
c [sweep-3-1] removed 4 vars (0 failed, 3 eqs, 6 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 4 vars in TOTAL (1 rounds, 53 queries)
c [phase-count-7] 702721 negative 100.0% of 702750 except 29 0.0%
c [phase-count-7] 456237 positive 64.9% of 702750 except 246513 35.1%
c [phase-count-7] less non-negative clauses 29 than limit 70200 (10.0%)
c [phase-count-7] non-pos/non-neg = 246513/29 = 8500.45 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 20030 negative 100%
c [sort-queue-7] sorted 24485 enqueued variables after 47013 conflicts
c [score-dist-7] active 81826 (77%), one 0 (0%), zero 24485 (23%)
c [score-dist-7] max exp 531, different 25 (5%)
c [score-dist-7] median active exp 522, avg 522.1
c [simplification-7] removed 6 variables 0.0% (106311 remain 51%)
c [simplification-7] removed 11813 irredundant clauses 1.7% (702750 remain 69%)
c [simplification-7] maximum reduction of 2% = max (0%, 2%)
c [simplification-7] geometric conflict interval increment 7222 = 21666 / 3
c [simplification-7] new conflict interval 28888
c [simplification-7] penalized conflict interval 28888 = 1 * 28888
c [simplification-7] hard conflict limit 90345 (soft 75901 + delta 14444)
c [simplification-7] new conflict limit 75901 (hard 90345)
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  121.3  106310   702750     47020   18595     85 42830  561   817   98  69%    176  504  640  241  265%
c i  137.0  106309   702750     59455   22603    104 42854  473   638  157  74%    137  245  279  292   96%
c i  137.0  106308   702750     59456   22603    104 42854  473   638  157  74%    137  244  278  292   95%
c i  137.0  106307   702750     59457   22603    104 42854  473   638  157  74%    137  244  277  292   95%
c i  137.0  106306   702750     59464   22603    104 42854  472   637  157  74%    135  244  276  292   95%
c i  146.9  106305   702750     68708   24695    113 42907  273   341  165  80%     82  -59  209  288   73%
c i  146.9  106288   702750     68709   24695    113 42907  273   341  165  80%     82  -59  208  288   72%
c i  146.9  106271   702750     68710   24695    113 42907  273   341  165  80%     82  -59  207  288   72%
c i  146.9  106254   702750     68716   24698    113 42907  273   341  165  80%     81  -59  205  288   71%
c i  146.9  106237   702750     68717   24698    113 42907  273   341  165  80%     81  -59  204  288   71%
c i  146.9  106220   702750     68720   24700    113 42907  273   341  165  80%     81  -60  202  288   70%
c i  146.9  106203   702750     68721   24700    113 42907  273   340  165  80%     81  -60  201  288   70%
c i  146.9  106187   702750     68725   24703    113 42907  272   340  165  80%     80  -60  198  288   69%
c i  146.9  106170   702750     68727   24704    113 42907  272   340  165  80%     80  -60  197  288   68%
c i  146.9  106153   702750     68730   24706    113 42907  272   340  165  80%     80  -60  194  288   68%
c i  146.9  106136   702750     68781   24735    113 42908  270   339  165  80%     73  -61  184  288   64%
c i  147.3  106119   702750     69126   24881    114 42911  265   335  170  79%     40  -64  204  287   71%
c i  147.3  106102   702750     69127   24881    114 42911  265   335  170  79%     40  -64  203  287   71%
c i  147.3  106085   702750     69138   24888    114 42911  265   336  170  79%     39  -64  202  287   70%
c i  148.0  106068   702750     69753   25092    114 42925  253   325  170  78%      2  -74  168  286   59%
c i  148.2  106067   702750     70078   25244    115 42928  244   316  170  77%    -10  -82  147  286   52%
c i  148.2  106052   702750     70079   25244    115 42928  244   316  170  77%    -10  -82  147  286   51%
c i  148.2  106038   702750     70081   25245    115 42928  244   316  170  77%    -10  -83  146  286   51%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  148.2  106023   702750     70082   25245    115 42928  244   316  170  77%    -10  -83  145  286   51%
c i  148.2  106012   702750     70085   25247    115 42928  244   316  170  77%    -10  -83  145  286   51%
c i  148.3  106011   702750     70168   25305    115 42929  241   316  170  76%    -13  -83  136  285   48%
c i  148.3  106010   702750     70169   25305    115 42929  241   316  170  76%    -13  -83  135  285   47%
c i  148.3  106009   702750     70171   25305    115 42929  241   316  170  76%    -13  -83  136  285   48%
c i  149.3  106008   702750     71180   25645    122 42948  219   302  170  73%    -28  -95  122  283   43%
c i  149.4  106007   702750     71203   25651    133 42952  218   303  170  72%    -29  -94  114  283   40%
c i  149.4  106006   702750     71217   25661    133 42955  218   304  170  72%    -29  -93  110  283   39%
c i  149.4  106005   702750     71219   25661    133 42956  217   304  170  72%    -29  -93  109  283   39%
c i  149.7  106004   702750     71952   26264    136 42969  194   328  170  59%    -34  -68   86  281   30%
c i  149.8  106003   702750     72099   26389    139 42969  191   333  170  57%    -35  -63   89  280   32%
c i  150.1  106002   702750     72588   26730    139 42975  191   350  170  55%    -38  -46  180  280   64%
c i  150.1  105985   702750     72593   26734    139 42975  191   350  170  54%    -38  -46  178  280   64%
c i  150.1  105968   702750     72599   26739    139 42975  191   350  170  54%    -38  -46  176  280   63%
c i  151.7  105951   702750     75001   28525    149 42981  147   302  170  49%    -21  -91  100  273   37%
c i  151.8  105950   702750     75069   28573    149 42981  146   301  170  49%    -22  -92  100  273   37%
c i  151.8  105942   702750     75071   28573    150 42981  146   301  170  49%    -22  -92   99  273   36%
c 
c [simplification-8] limit 76042 conflicts (hard 90345) hit after 79991 conflicts
c [quatres-3] found 506 quaternary clauses 5% in total
c [ternres-3] limit 9069029 with penalty 1 = 1 + 0
c [ternres-3] all 105942 free variables schedulable
c [ternres-3] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-3] fully completed ternary resolution
c [decomp-17] removed 373 variables
c [basicprobe-3] limit 90690298 penalty 0 = 0 + 0
c [basicprobe-3-0] 73693 probes remain 70% after last round
c [basicprobe-3-0] 123 units = 123 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 202 variables, found 1059 hbrs
c [unhide-8] limit 453451 with penalty 3 = 0 + 3
c [unhide-8-8] 0 units, 17 failed, 168 tauts, 0 hbrs, 1030833 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 17 transitive binary clauses
c [bca-3] limit of 10000000 steps and 1397547 added (scaled 2)
c [bca-3] 127947 out of 211460 literals actually usable 61%
c [bca-3] added 566 blocked clauses in 294776 steps
c [sweep-4] limit 5441417 penalty 0 = 0 + 0
c [sweep-4-1] 4360 pos 4.2% + 98709 neg 95.8% = 103069 sched 97.5% ret 2660
c [sweep-4-1] 5507046 steps 72 queries 10101.72 avg class size
c [sweep-4-1] 1848 decisions 68 SAT calls 717.44 avg env size
c [sweep-4-1] 98577 variables remain 93% (7127 retained 7%)
c [decomp-18] removed 28 variables
c [sweep-4-1] removed 28 vars (0 failed, 3 eqs, 9 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 28 vars in TOTAL (1 rounds, 71 queries)
c [phase-count-8] 697096 negative 100.0% of 697125 except 29 0.0%
c [phase-count-8] 453089 positive 65.0% of 697125 except 244036 35.0%
c [phase-count-8] less non-negative clauses 29 than limit 69700 (10.0%)
c [phase-count-8] non-pos/non-neg = 244036/29 = 8415.03 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 17515 negative 100%
c [sort-queue-8] sorted 24172 enqueued variables after 79991 conflicts
c [score-dist-8] active 81529 (77%), one 0 (0%), zero 24172 (23%)
c [score-dist-8] max exp 532, different 26 (5%)
c [score-dist-8] median active exp 524, avg 524.3
c [simplification-8] removed 241 variables 0.2% (105701 remain 50%)
c [simplification-8] removed 5625 irredundant clauses 0.8% (697125 remain 69%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 14444 = 28888 / 2
c [simplification-8] new conflict interval 43332
c [simplification-8] penalized conflict interval 43332 = 1 * 43332
c [simplification-8] hard conflict limit 144989 (soft 123323 + delta 21666)
c [simplification-8] new conflict limit 123323 (hard 144989)
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  169.1  105700   697125     80730   33003    144 44383  153   409  210  37%     29   17  237  261   91%
c 1  211.1  105691   697125    101574   42504    145 44391  340   444  247  76%    235   25  215  272   79%
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: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 3 count, 5201 added (4327 skipped), 885611 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, 2411 removed, 4056198 resolutions, 10891615 steps
c blkd: 155 blocking literals 0%, 1213 pure
c bump: 100535 bumped seen, 249939047 lits 2486.1 on average
c card: 3 count, 0 units, 0 am1, 24186016 steps
c card: 16 rescheduled, 0 eliminated, 0 resolved, 3540 subsumed
c card: 8460 at-most-one constraints found, average size 3.32
c card: 8460 at-most-one constraints used 100%, average size 3.32
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, 1230 eliminated, 1230 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: 4360480 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 49 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 18 decompositions, 115 equivalent 0%
c deco: 60551 decision-only clauses 60%, 81% reduction
c decs: 4903250 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 87094 eliminated 36%, 41355 pure 47%
c elms: 6 rounds, 1.0 rounds/bve
c elms: 41681 small 48%, 2845 large 3%
c elms: 123910 tried small, 41681 succeeded 34%, 82229 failed 66%
c elms: 5264 subsumed, 330 strengthened, 2 blocked
c elms: 4353992 copies, 4694233 resolutions, 1327173 ipos
c elms: 40849159 subchks, 23124272 strchks
c gaus: 2 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 6375422 steps, 3187711 extr 50%, 0 elim 0%
c glue: 384.8 orig avg, 384.8 real avg, 10.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 40244 = 36425 simple 91% + 2926 trn 7% + 893 lrg 2%, 6 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 100535 clauses, 709.5 length
c lrnd: 71328581 lits = 226276760 orig - 154948179 removed 68%
c lrnd: 43503 uips 43%, 46805 flips 47%
c mins: 32715 mins 35%, 142 bin 0%, 447 size 0%
c mins: 23563371 poisoned searches, 11108940 hits, 47% hit rate
c mins: 27896403 used twice searches, 1029413 hits, 4% hit rate
c move: moved 219, 198 bin 90%, 21 trn 10%
c otfs: 1080 driving 13%, 7418 restarting 87%
c otfs: str 8498, 8498 red 100%, 0 irr 0%
c otfs: str 8498, 0 bin 0%, 4 trn 0%, 8494 lrg 100%
c otfs: sub 42, 42 red 100%, 0 irr 0%
c otfs: sub 42, 0 bin 0%, 0 trn 0%, 42 lrg 100%
c phas: 8 computed, 279828 set, 0 pos (0%), 279828 neg (100%)
c prbs: 3 basic, 3441 probed, 160 failed, 0 lifted
c prbs: 3 simple, 707550 probed, 2604 failed, 78 eqs
c prbs: 3 treelook, 20 probed, 3 failed, 0 lifted
c prom: 0 locked 0% out of 96099 tried
c prps: 604297874 props, 119 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 3 count, 2 quat, 0 self1, 0 self2, 0 dup
c queu: 8 sorted, 4903250 next (18508 steps 0.00)
c queu: 250524229 enq (920232044 steps 3.67), 249939047 deq 100%
c redc: 1280 clauses 52%, 2453 tried 2%, 3 sat 0%
c redc: 5179 lits 17%, 30824 tried 0%, 3 sat 0%
c redc: 391 times jump level reduced, 238.4 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: 103 removed, 39 red 38%
c rsts: 5226 restarts 98%, 83 skipped 2%
c rsts: 83 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 8 count, 7 confs 88%, 0 vars 0%
c simp: 1 its 12%, 0 bin 0%, 0 trns 0%
c subl: 100535 count (127564 tried 1.3), 56305 sub out of 99815 (56.4%)
c swps: 4 count, 4 rounds, 196 queries (49.0/round)
c swps: 189 sat calls, 0 unsat (0.2% success rate)
c swps: 4991 decisions 26.4, 41 conflicts 0.2
c swps; 13482.8 avg class size, 795.1 avg environment size
c swps: 0 failed, 18 impls, 7 equivs
c swp0: 63 type 0 queries, 2 unsat (3.2%), 63 sat (100.0%)
c swp1: 133 type 1 queries, 29 unsat (21.8%), 126 sat (94.7%)
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: 10007903 calls to obtain time
c tops: 48390 fixed 20%, 207 its, 490.70 confs/it
c trds: 4 transitive reductions, 61 removed, 0 failed
c trds: 1011 nodes, 3664 edges, 8020560 steps
c trim: 1438285 words, 5.5 MB
c trnr: 3 count, 0 bin, 2 trn, 5370606 steps
c unhd: 8 count, 8 rounds, 29199201 steps
c unhd: 4 non-trivial sccs of average size 2.0
c unhd: 13 units, 13 bin, 0 trn, 0 lrg
c unhd: 51 failed, 38 stamp, 0 lits, 0 bin, 3 trn, 0 lrg
c unhd: 74458 tauts, 37 bin 0%, 3 trn 0%, 197 lrg 0%
c unhd: 74458 tauts, 74221 stamp 100%, 540 red 1%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 2120096 str, 13 bin 0%, 3 trn 0%, 2120080 lrg 100%, 2119740 red 100%
c vars: 105691 remaining 44% and 135599 removed 56% out of 241290
c vars: 48390 fixed 20%, 87094 eliminated 36%, 115 equivalent 0%
c vsts: 2607581572 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 4.3 search visits per propagation, 24863.7 per conflict
c wchs: 114170032 pushed, 28770494 enlarged, 75 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all          99817             0             0       4984313       1192713         72645
c 
c  0 0          2316   2         0   0<        0   0<  1176602  24    142544  12      3157   4     0.4
c  1 5          1010   1         0   0         0   0    422732   8     72849   6      1490   2     0.2
c  2 6          2806   3         0   0         0   0    653980  13    124714  10      3550   5     1.1
c  3 9          3697   4         0   0         0   0    707003  14    152273  13      4097   6     2.4
c  4 14         3538   4         0   0         0   0    486697  10<   118990  10      4163   6     3.8
c  5 21         3393   3         0   0         0   0    314721   6    101812   9<     4242   6     5.2
c  6 30         2995   3         0   0         0   0    199386   4     72820   6      4319   6     7.8
c  7 41         3310   3         0   0         0   0    213973   4     72370   6      6086   8    12.0
c  8 54         3224   3         0   0         0   0    147602   3     63272   5      5930   8<   17.6
c  9 69         3656   4         0   0         0   0    106625   2     46272   4      6603   9    27.8
c 10 86         4028   4<        0   0         0   0    177095   4     82006   7     14497  20    27.0
c 11 126        5137   5         0   0         0   0    204443   4     75043   6      9719  13     6.0
c 12 230       28385  28         0   0         0   0     98522   2     37632   3      3394   5    26.2
c 13 534       32258  32         0   0         0   0     74531   1     30056   3      1384   2    40.3
c 14 1526         64   0         0   0         0   0       401   0        60   0        14   0     0.3
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                 10.1           0.0           0.0           3.7           5.1           7.5
c std                  3.7           0.0           0.0           3.5           3.7           3.4
c 
c   62.178  29% bump
c   18.066   9% elim
c   14.251   7% unhide
c    8.437   4% probe
c    4.448   2% block
c    3.186   2% decide
c    3.071   1% sweep
c    1.629   1% cce
c 
c    2.346 < 1% rest (below)
c 
c    1.042   0% bca
c    0.798   0% gauss
c    0.215   0% card
c    0.183   0% transred
c    0.097   0% ternres
c    0.011   0% quatres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    4.646   2% preprocessing     8%
c   53.678  25% inprocessing     92%
c ==================================
c   58.324  28% simplifying
c  152.731  72% search
c ==================================
c  211.065 100% all
c 
c        101574 conflicts,         481.2 confs/sec
c           150 ternaries,         677.2 confs/ternary
c           351 binaries,          289.4 confs/binary
c           207 iterations,        490.7 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          5226 restarts,           24.8 rests/sec,     19.4 confs/restart
c       4903250 decisions,       23231.0 decis/sec,     48.3 decis/conflict
c     604297874 propagations,  2863089.6 props/sec,    123.2 props/decision
c 
c 211.1 seconds, 247.0 MB
c launch: done
