c launch: /data/cnf/sc2014/app/aaai10-planning-ipc5-TPP-30-step11.cnf.bz2
c host: atom03
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/aaai10-planning-ipc5-TPP-30-step11.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/aaai10-planning-ipc5-TPP-30-step11.cnf.bz2
c no embedded options
c found 'p cnf 314455 2920820' header
c read 314455 variables, 2920820 clauses, 6301180 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 314131 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  314131  2920496         0       0      0     0    0     0   66   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1000000 penalty 1 = 0 + 1
c [card-1] found 26 at-most-one constraints of average size 3.1
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1000000 for elimination
c [card-1] 26 out of 26 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 12 at-most-one constraints, 8 used 67%
c [card-1] exported 8 binary clauses, 1.0 per/constraint
c [decomp-1] removed 1461 variables
c [simpleprobe-1] all 312994 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 10000000 penalty 1 = 0 + 1
c [decomp-2] removed 14099 variables
c [simpleprobe-1] 167806 variables remain 56% (131089 retained 44%)
c [simpleprobe-1] removed 14099 variables, found 17050 hbrs, 178 units
c [unhide-1] limit 169240 based on 2707852 irredundant clauses
c [unhide-1-1] 68 units, 171 failed, 143 tauts, 0 hbrs, 69 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 273951 variables 100%
c [elim-1] limit of 10000000 steps penalty 1 = 0 + 1
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 209962 not tried 77% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 13667 = 5% variables out of 273951 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 2312807 negative 100.0% of 2313455 except 648 0.0%
c [phase-count-1] 1308993 positive 56.6% of 2313455 except 1004462 43.4%
c [phase-count-1] less non-negative clauses 648 than limit 231300 (10.0%)
c [phase-count-1] non-pos/non-neg = 1004462/648 = 1550.10 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 260284 negative 100%
c [sort-queue-1] sorted 260284 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 260284 (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 53430 variables 17.0% (260284 remain 83%)
c [simplification-1] removed 607041 irredundant clauses 20.8% (2313455 remain 79%)
c [simplification-1] maximum reduction of 21% = max (17%, 21%)
c [simplification-1] large reduction 21% >= 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    5.5  260283  2313455         2       1      0 15661    0     0   78   1%      0    0    0    0 25500%
c i    5.6  260168  2313455        12       7      1 15661    0     2   81   1%      0    2    0    0 24976%
c i    6.0  260167  2313455       100      80      2 15670    0     8   81   4%      0    8    4    0 22596%
c i    6.2  259968  2313455       166     140      5 15672    0    12   82   4%      0   12    6    0 19357%
c i    6.4  259965  2313455       208     174      9 15675    1    18   82   3%      0   18    7    0 18007%
c i    6.5  259964  2313455       257     220     10 15676    1    20   82   4%      0   20    8    0 16328%
c i    6.5  259963  2313455       265     227     10 15676    1    20   82   4%      0   20   10    0 17459%
c i    6.5  259962  2313455       266     227     10 15676    1    20   82   4%      0   20   10    0 17391%
c i    6.6  259961  2313455       268     228     10 15676    1    20   82   5%      0   20   11    0 17719%
c i    6.6  259960  2313455       269     228     10 15676    1    20   82   5%      0   20   11    0 17650%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 333 variables
c [simpleprobe-2] 146516 schedulable variables 56%
c [simpleprobe-2] limit 4619086 based on 2309543 irredundant clauses
c [decomp-4] removed 737 variables
c [simpleprobe-2] 82278 variables remain 32% (176936 retained 68%)
c [simpleprobe-2] removed 737 variables, found 14924 hbrs, 91 units
c [treelook-1] limit 575115 based on 2300463 irredundant clauses
c [treelook-1] scheduled 187189 literals 36%
c [treelook-1] scheduling used 575437 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 575115 based on 2300463 irredundant clauses
c [treelook-1] used 601363 steps
c [treelook-1] 187161 literals remain 36%
c [treelook-1] 184635 variables remain to probed next time 71%
c [treelook-1] removed 7 variables, found 2596 hbrs
c [basicprobe-1] limit 18403088 based on 2300386 irredundant clauses
c [basicprobe-1-0] 166259 probes remain 65% after last round
c [basicprobe-1-0] 96 units = 96 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 2038 variables, found 4413 hbrs
c [unhide-2] limit 143774 based on 2300386 irredundant clauses
c [unhide-2-2] 54 units, 34 failed, 431 tauts, 0 hbrs, 475 literals
c [elim-2] 206883 variables 81% will be scheduled this time
c [elim-2] scheduled 206883 variables 81%
c [elim-2] limit of 10000000 steps penalty 1 = 0 + 1
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 172395 not tried 67% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 419 = 0% variables out of 206883 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 2258338 negative 100.0% of 2258985 except 647 0.0%
c [phase-count-2] 1281324 positive 56.7% of 2258985 except 977661 43.3%
c [phase-count-2] less non-negative clauses 647 than limit 225800 (10.0%)
c [phase-count-2] non-pos/non-neg = 977661/647 = 1511.07 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 51814 negative 100%
c [sort-queue-2] sorted 249850 enqueued variables after 269 conflicts
c [score-dist-2] active 6157 (2%), one 0 (0%), zero 249850 (98%)
c [score-dist-2] max exp 513, different 12 (2%)
c [score-dist-2] median active exp 510, avg 509.5
c [simplification-2] removed 3953 variables 1.5% (256007 remain 81%)
c [simplification-2] removed 54470 irredundant clauses 2.4% (2258985 remain 77%)
c [simplification-2] maximum reduction of 2% = max (2%, 2%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1032 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   12.7  256006  2258985       270     218      7 36495    1    20   80   5%      0   20   11    0 17581%
c i   12.7  256005  2258985       271     218      7 36495    1    20   80   5%      0   20   10    0 17513%
c i   12.7  256004  2258985       272     218      7 36495    1    20   80   5%      0   20   10    0 17445%
c i   12.7  256003  2258985       282     226      7 36495    1    20   80   6%      0   20   14    0 18466%
c i   12.7  256002  2258985       285     225      7 36495    1    20   80   6%      0   20   14    0 18475%
c i   12.7  256001  2258985       287     225      8 36495    1    20   80   6%      0   20   14    0 18334%
c i   13.3  256000  2258985       481     409      8 36497    2    32   81   8%      0   32   23    0 14421%
c i   13.3  255999  2258985       483     410      8 36497    2    32   81   8%      0   32   24    0 14724%
c i   13.3  255998  2258985       484     410      8 36497    2    32   81   8%      0   32   24    0 14667%
c i   13.3  255997  2258985       485     410      8 36497    2    32   81   8%      0   32   24    0 14610%
c i   13.3  255996  2258985       486     410      8 36497    2    32   81   8%      0   32   24    0 14553%
c i   13.4  255995  2258985       488     411      8 36497    3    32   81   8%      0   32   25    0 14843%
c i   13.4  255994  2258985       513     430      8 36500    4    34   81  11%      0   34   41    0 16943%
c i   13.4  255888  2258985       514     430      8 36500    4    34   81  11%      0   34   41    0 16877%
c i   13.4  255887  2258985       515     430      8 36500    4    34   81  11%      0   34   41    0 16812%
c i   13.4  255886  2258985       516     430      8 36500    4    34   81  11%      0   34   41    0 16746%
c i   13.4  255885  2258985       532     442      8 36501    4    35   81  12%      0   35   48    0 16998%
c i   13.4  255884  2258985       533     442      8 36501    4    35   81  12%      0   35   47    0 16932%
c i   13.4  255883  2258985       534     442      8 36501    4    35   81  12%      0   35   47    0 16866%
c i   13.4  255882  2258985       535     442      8 36501    4    35   81  12%      0   35   47    0 16800%
c i   13.4  255881  2258985       536     442      8 36501    4    35   81  12%      0   35   47    0 16735%
c i   13.4  255880  2258985       537     442      8 36501    4    35   81  12%      0   35   47    0 16670%
c i   13.5  255879  2258985       547     450      8 36502    5    36   81  13%      0   35   48    0 16417%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   13.5  255878  2258985       548     450      8 36502    5    36   81  13%      0   35   48    0 16353%
c i   13.5  255877  2258985       549     450      8 36502    5    36   81  13%      0   35   48    0 16290%
c i   13.5  255876  2258985       557     454     10 36502    5    36   81  13%      0   36   48    0 16070%
c i   13.9  255875  2258985       721     596     12 36507    9    46   81  19%      0   46   79    1 14071%
c i   13.9  255874  2258985       739     599     13 36516    9    47   81  18%      0   47   74    1 13131%
c i   13.9  255873  2258985       772     629     14 36517    9    48   81  19%      0   48   74    1 12287%
c i   14.6  255872  2258985      1045     835     25 36518   15    57   81  27%      1   57  101    1 9706%
c i   14.6  255871  2258985      1046     835     25 36518   15    57   81  27%      1   57  101    1 9669%
c i   14.6  255870  2258985      1047     835     25 36518   15    57   81  27%      1   57  100    1 9631%
c i   14.6  255869  2258985      1050     837     25 36518   16    57   81  27%      1   57  100    1 9598%
c i   14.6  255868  2258985      1051     837     25 36518   16    57   81  27%      1   57  100    1 9561%
c i   14.6  255867  2258985      1052     837     25 36518   16    57   81  27%      1   57  100    1 9524%
c i   14.6  255866  2258985      1054     838     25 36518   16    57   81  27%      1   57  100    1 9490%
c i   14.6  255865  2258985      1057     838     25 36520   16    57   81  27%      1   57   98    1 9380%
c i   14.6  255864  2258985      1058     838     25 36520   16    57   81  27%      1   57   98    1 9343%
c i   14.6  255863  2258985      1059     838     25 36520   16    57   81  27%      1   57   98    1 9307%
c i   14.6  255862  2258985      1063     841     25 36520   16    57   81  27%      1   57   98    1 9286%
c i   14.6  255861  2258985      1065     842     25 36520   16    57   81  27%      1   57   98    1 9253%
c i   14.6  255860  2258985      1066     842     25 36520   16    57   81  27%      1   57   98    1 9217%
c i   14.6  255859  2258985      1067     842     25 36520   16    57   81  27%      1   57   97    1 9181%
c i   14.6  255858  2258985      1073     842     25 36520   16    57   81  28%      1   57   98    1 9172%
c i   14.6  255857  2258985      1078     845     25 36521   16    58   81  28%      1   57   98    1 9112%
c 
c [simplification-3] limit 1314 conflicts (hard 11000) hit after 1317 conflicts
c [card-2] limit 564746 based on 2258985 irredundant clauses
c [card-2] found 101 at-most-one constraints of average size 3.2
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 564746 for elimination
c [card-2] 101 out of 101 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 161 variables
c [treelook-2] limit 564269 based on 2257076 irredundant clauses
c [treelook-2] scheduled 183924 literals 36%
c [treelook-2] scheduling used 565232 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 564269 based on 2257076 irredundant clauses
c [treelook-2] used 650560 steps
c [treelook-2] 183918 literals remain 36%
c [treelook-2] 171044 variables remain to probed next time 67%
c [treelook-2] removed 0 variables, found 3494 hbrs
c [unhide-3] limit 141067 based on 2257076 irredundant clauses
c [unhide-3-3] 42 units, 34 failed, 5723 tauts, 0 hbrs, 2657 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 255682 variables 100%
c [elim-3] limit of 10000000 steps penalty 1 = 0 + 1
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 203481 not tried 80% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1462 = 1% variables out of 255682 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 2247617 negative 100.0% of 2248233 except 616 0.0%
c [phase-count-3] 1278035 positive 56.8% of 2248233 except 970198 43.2%
c [phase-count-3] less non-negative clauses 616 than limit 224800 (10.0%)
c [phase-count-3] non-pos/non-neg = 970198/616 = 1575.00 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 49732 negative 100%
c [sort-queue-3] sorted 245775 enqueued variables after 1317 conflicts
c [score-dist-3] active 8445 (3%), one 0 (0%), zero 245775 (97%)
c [score-dist-3] max exp 520, different 18 (3%)
c [score-dist-3] median active exp 512, avg 512.3
c [simplification-3] removed 1637 variables 0.6% (254220 remain 81%)
c [simplification-3] removed 10752 irredundant clauses 0.5% (2248233 remain 77%)
c [simplification-3] maximum reduction of 1% = max (1%, 0%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 21317 (soft 11317 + delta 10000)
c [simplification-3] new conflict limit 11317 (hard 21317)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   19.7  254219  2248233      1438    1047     29 39317   25    70   80  36%      1   69  117    2 6675%
c i   20.0  254216  2248233      1569    1152     31 39321   30    75   80  40%      1   74  140    2 6720%
c i   20.0  254215  2248233      1575    1157     31 39321   30    75   80  40%      1   74  140    2 6679%
c i   20.1  254212  2248233      1600    1176     31 39321   30    76   80  40%      1   74  140    2 6512%
c i   20.1  254211  2248233      1601    1176     31 39321   30    76   80  40%      1   74  140    2 6487%
c i   20.1  254210  2248233      1602    1176     31 39321   30    75   80  40%      1   74  139    2 6462%
c i   20.2  254209  2248233      1687    1235     31 39325   33    78   81  42%      1   77  146    2 6187%
c i   20.2  254208  2248233      1688    1235     31 39325   33    78   81  42%      1   77  145    2 6163%
c i   20.2  254207  2248233      1689    1235     31 39325   33    78   81  42%      1   77  145    2 6139%
c i   20.2  254206  2248233      1690    1235     31 39325   33    78   81  42%      1   77  144    2 6115%
c i   20.2  254205  2248233      1691    1235     31 39325   33    78   81  42%      1   77  144    2 6091%
c i   20.9  254204  2248233      2006    1445     34 39325   39    86   81  46%      2   84  113    3 3869%
c i   20.9  254203  2248233      2007    1445     34 39325   39    86   81  46%      2   84  112    3 3854%
c i   20.9  254202  2248233      2008    1445     34 39325   39    86   81  46%      2   84  112    3 3839%
c i   20.9  254201  2248233      2009    1445     34 39325   39    86   81  46%      2   84  111    3 3824%
c i   20.9  254200  2248233      2016    1451     34 39325   39    86   81  46%      2   84  109    3 3742%
c i   21.0  254095  2248233      2109    1518     34 39325   39    88   81  44%      2   86   80    3 2744%
c i   21.0  254094  2248233      2110    1518     34 39325   39    88   81  44%      2   86   80    3 2733%
c i   21.0  254093  2248233      2111    1518     34 39325   39    88   81  44%      2   86   80    3 2723%
c i   21.0  254092  2248233      2128    1534     34 39325   39    88   81  44%      2   87   80    3 2699%
c i   21.0  254091  2248233      2136    1539     36 39325   39    88   81  44%      1   87   77    3 2617%
c i   21.0  254090  2248233      2137    1539     36 39325   39    88   81  44%      1   87   77    3 2607%
c i   21.9  254089  2248233      2525    1876     46 39328   37    95   81  39%      2   93   34    3 1127%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   21.9  254088  2248233      2532    1879     46 39328   37    95   81  39%      2   93   34    3 1109%
c i   22.2  254087  2248233      2633    1964     47 39328   37    97   81  38%      2   94   33    3 1078%
c i   22.2  254086  2248233      2634    1964     47 39328   37    96   81  38%      2   94   33    3 1074%
c i   22.2  254085  2248233      2635    1964     47 39328   37    96   81  38%      2   94   33    3 1070%
c i   22.2  254084  2248233      2636    1964     47 39328   37    96   81  38%      2   94   33    3 1066%
c i   22.2  254083  2248233      2637    1964     47 39328   37    96   81  38%      2   94   33    3 1062%
c i   22.2  253990  2248233      2646    1971     47 39328   37    96   81  38%      2   94   33    3 1063%
c i   25.6  253989  2248233      3643    2845     58 39339   39   116   83  34%      6  112   77    4 2074%
c i   26.1  253988  2248233      3759    2941     60 39341   40   123   83  33%      6  119   85    4 2191%
c i   26.1  253987  2248233      3760    2941     60 39341   40   123   83  33%      6  119   84    4 2182%
c 1   29.1  253986  2248233      4355    3392     66 39346   64   185   85  35%      5  179  156    6 2687%
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: 0 count, 0 added (0 skipped), 0 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: 0 bces, 0 removed, 0 resolutions, 0 steps
c blkd: 0 blocking literals 0%, 0 pure
c bump: 4312 bumped seen, 1391807 lits 322.8 on average
c card: 2 count, 0 units, 8 am1, 3591744 steps
c card: 16 rescheduled, 71 eliminated, 1138 resolved, 228 subsumed
c card: 127 at-most-one constraints found, average size 3.18
c card: 127 at-most-one constraints used 100%, average size 3.18
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: 0 cces, 0 eliminated, 0 ate 0%, 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: 9222000 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 17 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 7 decompositions, 778 equivalent 0%
c deco: 534 decision-only clauses 12%, 58% reduction
c decs: 284281 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 3 elims, 15548 eliminated 5%, 6382 pure 41%
c elms: 3 rounds, 1.0 rounds/bve
c elms: 9100 small 59%, 66 large 0%
c elms: 50823 tried small, 9100 succeeded 18%, 41723 failed 82%
c elms: 631 subsumed, 47 strengthened, 0 blocked
c elms: 2190489 copies, 2175381 resolutions, 1035708 ipos
c elms: 586227 subchks, 679940 strchks
c gaus: 0 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 0 steps, 0 extr 0%, 0 elim 0%
c glue: 90.7 orig avg, 90.7 real avg, 5.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 42477 = 31974 simple 75% + 6121 trn 14% + 4382 lrg 10%, 21 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 4312 clauses, 187.4 length
c lrnd: 808230 lits = 1116381 orig - 308151 removed 28%
c lrnd: 2551 uips 59%, 1362 flips 32%
c mins: 3383 mins 82%, 47 bin 1%, 157 size 4%
c mins: 1051826 poisoned searches, 311782 hits, 30% hit rate
c mins: 1301835 used twice searches, 129411 hits, 10% hit rate
c move: moved 76, 0 bin 0%, 76 trn 100%
c otfs: 43 driving 38%, 70 restarting 62%
c otfs: str 113, 111 red 98%, 2 irr 2%
c otfs: str 113, 0 bin 0%, 5 trn 4%, 108 lrg 96%
c otfs: sub 0, 0 red 0%, 0 irr 0%
c otfs: sub 0, 0 bin 0%, 0 trn 0%, 0 lrg 0%
c phas: 3 computed, 361830 set, 0 pos (0%), 361830 neg (100%)
c prbs: 1 basic, 610 probed, 96 failed, 0 lifted
c prbs: 2 simple, 633629 probed, 269 failed, 12 eqs
c prbs: 2 treelook, 34 probed, 7 failed, 0 lifted
c prom: 0 locked 0% out of 2016 tried
c prps: 75266394 props, 250 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 0 count, 0 quat, 0 self1, 0 self2, 0 dup
c queu: 3 sorted, 284281 next (13069 steps 0.05)
c queu: 2462171 enq (3098154 steps 1.26), 1391807 deq 57%
c redc: 226 clauses 22%, 1048 tried 24%, 2 sat 0%
c redc: 716 lits 6%, 11577 tried 1%, 2 sat 0%
c redc: 33 times jump level reduced, 40.0 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: 5551 removed, 89 red 2%
c rsts: 408 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 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: 3 count, 2 confs 67%, 0 vars 0%
c simp: 1 its 33%, 0 bin 0%, 0 trns 0%
c subl: 4312 count (3920 tried 0.9), 597 sub out of 4081 (14.6%)
c swps: 0 count, 0 rounds, 0 queries (0.0/round)
c swps: 0 sat calls, 0 unsat (0.0% success rate)
c swps: 0 decisions 0.0, 0 conflicts 0.0
c swps; 0.0 avg class size, 0.0 avg environment size
c swps: 0 failed, 0 impls, 0 equivs
c swp0: 0 type 0 queries, 0 unsat (0.0%), 0 sat (0.0%)
c swp1: 0 type 1 queries, 0 unsat (0.0%), 0 sat (0.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: 577313 calls to obtain time
c tops: 44143 fixed 14%, 88 its, 49.49 confs/it
c trds: 0 transitive reductions, 0 removed, 0 failed
c trds: 0 nodes, 0 edges, 0 steps
c trim: 8603 words, 0.0 MB
c trnr: 0 count, 0 bin, 0 trn, 0 steps
c unhd: 3 count, 3 rounds, 28445387 steps
c unhd: 6 non-trivial sccs of average size 2.0
c unhd: 164 units, 163 bin, 1 trn, 0 lrg
c unhd: 239 failed, 236 stamp, 0 lits, 0 bin, 1 trn, 0 lrg
c unhd: 6297 tauts, 91 bin 1%, 154 trn 2%, 9 lrg 0%
c unhd: 6297 tauts, 6043 stamp 96%, 599 red 10%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 3201 str, 163 bin 5%, 450 trn 14%, 2588 lrg 81%, 2485 red 78%
c vars: 253986 remaining 81% and 60469 removed 19% out of 314455
c vars: 44143 fixed 14%, 15548 eliminated 5%, 778 equivalent 0%
c vsts: 173993565 visits, 93% srch, 7% simp, 0% lkhd
c vsts: 2.3 search visits per propagation, 36989.1 per conflict
c wchs: 53178590 pushed, 21122676 enlarged, 27 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all           4081             0             0        115914         33370          1990
c 
c  0 0           874  21         0   0<        0   0<    70246  61     17571  53       262  13     0.0
c  1 5           109   3         0   0         0   0      4913   4      1818   5        27   1     0.0
c  2 6           246   6         0   0         0   0      9217   8      2781   8        86   4     0.0
c  3 9           184   5         0   0         0   0      2917   3<     1403   4<       74   4     0.1
c  4 14          303   7         0   0         0   0      2820   2      1452   4       370  19     0.1
c  5 21          417  10         0   0         0   0      2420   2      1050   3       197  10     0.4
c  6 30          266   7<        0   0         0   0      1615   1       519   2        88   4<    0.2
c  7 41          106   3         0   0         0   0       644   1       259   1        56   3     0.2
c  8 54           55   1         0   0         0   0       329   0       204   1        32   2     0.2
c  9 69           52   1         0   0         0   0      1134   1       136   0        20   1     0.1
c 10 86          166   4         0   0         0   0      1666   1       549   2       108   5     0.3
c 11 126         960  24         0   0         0   0     16708  14      5088  15       562  28     0.8
c 12 230         224   5         0   0         0   0       987   1       432   1       105   5     0.3
c 13 534         119   3         0   0         0   0       298   0       108   0         3   0     0.3
c 
c avg                  5.9           0.0           0.0           2.6           3.0           6.4
c std                  4.5           0.0           0.0           4.1           4.2           4.1
c 
c    5.345  18% probe
c    3.533  12% elim
c    2.798  10% unhide
c 
c    0.286 < 1% rest (below)
c 
c    0.261   1% bump
c    0.159   1% decide
c    0.127   0% card
c    0.000   0% bca
c    0.000   0% block
c    0.000   0% cce
c    0.000   0% gauss
c    0.000   0% locs
c    0.000   0% quatres
c    0.000   0% queuesort
c    0.000   0% rescore
c    0.000   0% sweep
c    0.000   0% ternres
c    0.000   0% transred
c ==================================
c    5.454  19% preprocessing    34%
c   10.383  36% inprocessing     66%
c ==================================
c   15.837  54% simplifying
c   13.253  46% search
c ==================================
c   29.101 100% all
c 
c          4355 conflicts,         149.6 confs/sec
c            70 ternaries,          62.2 confs/ternary
c            73 binaries,           59.7 confs/binary
c            88 iterations,         49.5 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c           408 restarts,           14.0 rests/sec,     10.7 confs/restart
c        284281 decisions,        9768.7 decis/sec,     65.3 decis/conflict
c      75266394 propagations,  2586363.1 props/sec,    264.8 props/decision
c 
c 29.1 seconds, 156.3 MB
c launch: done
