c launch: /data/cnf/sc2014/app/grid-strips-grid-y-3.035-NOTKNOWN.cnf.bz2
c host: atom06
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/grid-strips-grid-y-3.035-NOTKNOWN.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/grid-strips-grid-y-3.035-NOTKNOWN.cnf.bz2
c no embedded options
c found 'p cnf 257380 2139615' header
c read 257380 variables, 2139615 clauses, 5163755 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --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 199865 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [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  199865  1689184         0       0      0     0    0     0   60   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 12 at-most-one constraints of average size 15.7
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 12 out of 12 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 3292 at-most-one constraints, 866 used 26%
c [card-1] exported 4772 binary clauses, 5.5 per/constraint
c [decomp-1] removed 65363 variables
c [simpleprobe-1] all 192017 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 2073 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 2073 variables, found 1288 hbrs, 2005 units
c [unhide-1] limit 99299 based on 1588793 irredundant clauses
c [unhide-1-1] 14 units, 6 failed, 76798 tauts, 0 hbrs, 14 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 189928 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 13261 not tried 7% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 4927 = 3% variables out of 189928 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 1489225 negative 100.0% of 1489324 except 99 0.0%
c [phase-count-1] 847794 positive 56.9% of 1489324 except 641530 43.1%
c [phase-count-1] less non-negative clauses 99 than limit 148900 (10.0%)
c [phase-count-1] non-pos/non-neg = 641530/99 = 6480.10 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 185001 negative 100%
c [sort-queue-1] sorted 185001 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 185001 (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 7599 variables 3.9% (185001 remain 93%)
c [simplification-1] removed 199860 irredundant clauses 11.8% (1489324 remain 88%)
c [simplification-1] maximum reduction of 12% = max (4%, 12%)
c [simplification-1] large reduction 12% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    8.6  185000  1489324         1       0      0  1929    0     0   58   0%      0    0    0    0    0%
c i    8.6  184979  1489324         2       0      0  1929    0     0   58   0%      0    0    0    0    0%
c i    9.5  184089  1489324       284     202     36  1935    5    12   61  39%      1   12   48    0 15719%
c i    9.9  184070  1489324       380     279     44  1939    5    16   62  31%      1   16   38    0 11761%
c i   10.1  184069  1489324       423     311     46  1941    5    17   62  31%      1   17   35    0 10442%
c i   13.7  184068  1489324       961     760     63  1943    8    22   69  35%      2   22   31    1 5602%
c 
c [simplification-2] limit 1020 conflicts (hard 11000) hit after 1022 conflicts
c [decomp-3] removed 958 variables
c [simpleprobe-2] all 184043 free variables schedulable
c [simpleprobe-2] limit 3867803 penalty 0 = 0 + 0
c [decomp-4] removed 16 variables
c [simpleprobe-2] 133989 variables remain 73% (50038 retained 27%)
c [simpleprobe-2] removed 16 variables, found 1269 hbrs, 16 units
c [treelook-1] limit 370405 based on 1481620 irredundant clauses
c [treelook-1] scheduled 149395 literals 41%
c [treelook-1] scheduling used 376671 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 370405 based on 1481620 irredundant clauses
c [treelook-1] used 816615 steps
c [treelook-1] 149392 literals remain 41%
c [treelook-1] 149364 variables remain to probed next time 81%
c [treelook-1] removed 0 variables, found 810 hbrs
c [basicprobe-1] limit 11852960 based on 1481620 irredundant clauses
c [basicprobe-1-0] 167123 probes remain 91% after last round
c [basicprobe-1-0] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 5 variables, found 107 hbrs
c [unhide-2] limit 92601 based on 1481620 irredundant clauses
c [unhide-2-2] 8 units, 3 failed, 394 tauts, 0 hbrs, 127004 literals
c [elim-2] 13260 variables 7% will be scheduled this time
c [elim-2] scheduled 13260 variables 7%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 10706 not tried 6% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 0 = 0% variables out of 13260 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 1480681 negative 100.0% of 1480778 except 97 0.0%
c [phase-count-2] 842924 positive 56.9% of 1480778 except 637854 43.1%
c [phase-count-2] less non-negative clauses 97 than limit 148000 (10.0%)
c [phase-count-2] non-pos/non-neg = 637854/97 = 6575.81 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 39 negative 100%
c [sort-queue-2] sorted 24687 enqueued variables after 1022 conflicts
c [score-dist-2] active 159294 (87%), one 0 (0%), zero 24687 (13%)
c [score-dist-2] max exp 519, different 17 (3%)
c [score-dist-2] median active exp 514, avg 514.2
c [simplification-2] removed 70 variables 0.0% (183981 remain 92%)
c [simplification-2] removed 8546 irredundant clauses 0.6% (1480778 remain 88%)
c [simplification-2] maximum reduction of 1% = max (0%, 1%)
c [simplification-2] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-2] new conflict interval 10000
c [simplification-2] penalized conflict interval 10000 = 1 * 10000
c [simplification-2] hard conflict limit 21022 (soft 11022 + delta 10000)
c [simplification-2] new conflict limit 11022 (hard 21022)
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.8  183980  1480778      1063     849     65  3554    8    23   71  35%      2   23   27    1 4776%
c i   20.5  183979  1480778      1195     961     70  3555    9    27   72  33%      2   27   30    1 4696%
c i   23.4  183958  1480778      1640    1320     90  3563   13    57   75  22%      3   56   47    1 4995%
c i   24.0  183940  1480778      1710    1379     90  3565   13    57   75  22%      2   57   42    1 4368%
c i   54.0  183938  1480778      4628    2929    142  3630  143   248  121  58%     30  241  215   12 1771%
c i   58.6  183937  1480778      5092    3256    158  3632  143   260  135  55%     20  251  152   13 1162%
c i   74.0  183918  1480778      6175    4147    276  3638  122   225  194  54%     13  213   46   14  340%
c i   84.8  183917  1480778      7347    4884    291  3652  123   233  210  53%     11  217  120   16  770%
c 
c [simplification-3] limit of 114 binary hit after 114 binaries
c [card-2] limit 2399118 penalty 1 = 1 + 0
c [card-2] found 33 at-most-one constraints of average size 45.3
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 2399118 for elimination
c [card-2] 33 out of 33 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 5585 at-most-one constraints, 360 used 6%
c [card-2] exported 3676 binary clauses, 10.2 per/constraint
c [decomp-6] removed 79 variables
c [unhide-3] limit 119955 with penalty 4 = 0 + 4
c [unhide-3-3] 22 units, 6 failed, 32906 tauts, 0 hbrs, 3260245 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 183876 variables 100%
c [elim-3] limit of 191929505 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 232 variables 0% in round 1 in 191410490 steps
c [elim-3-1] backward subsumption/strengthening limit 519015
c [elim-3-1-1] backward checking 2541 touched variables 1%
c [elim-3-1-1] incomplete backward checking 2501 remain 98%
c [elim-3-1] subsumed 0 and strengthened 0 clauses in 519021 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 232 = 0% variables out of 183876 scheduled
c [elim-3] 232 < 1/100 * 183876 = 1838 considered unsuccessful
c [sort-queue-3] sorted 3244 enqueued variables after 7352 conflicts
c [score-dist-3] active 180400 (98%), one 0 (0%), zero 3244 (2%)
c [score-dist-3] max exp 525, different 19 (4%)
c [score-dist-3] median active exp 522, avg 521.1
c [simplification-3] removed 273 variables 0.1% (183644 remain 92%)
c [simplification-3] removed 37585 irredundant clauses 2.5% (1443193 remain 85%)
c [simplification-3] maximum reduction of 3% = max (0%, 3%)
c [simplification-3] forced so keeping old conflict interval 10000
c [simplification-3] conflict limit remains at 11022 (hard 21022)
c [simplification-3] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  134.2  183643  1443193      8562    4277    324  7324  103   195  164  53%     10  176   42   16  261%
c i  136.6  183642  1443193      8729    4397    328  7355  100   192  187  52%      9  171   40   16  245%
c i  136.7  183641  1443193      8742    4405    328  7359  100   191  187  52%      8  171   39   16  239%
c 
c [simplification-4] limit 11022 conflicts (hard 21022) hit after 11023 conflicts
c [decomp-7] removed 6 variables
c [treelook-2] limit 725985 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 177045 literals 48%
c [treelook-2] scheduling used 728929 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 725985 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 879515 steps
c [treelook-2] 177038 literals remain 48%
c [treelook-2] 148241 variables remain to probed next time 81%
c [treelook-2] removed 4 variables, found 1502 hbrs
c [unhide-4] limit 181496 with penalty 4 = 0 + 4
c [unhide-4-4] 0 units, 3 failed, 947 tauts, 0 hbrs, 4452332 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 183613 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 1451970620 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 642 blocked clauses
c [block-1] 642 < 1/100 * 1443099 = 14430 considered unsuccessful
c [cce-1] limit of 72598531 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 141 clauses out of 481 (29%) of length 541
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 141 large clauses in 72598533 steps
c [cce-1-1] allowing another 36299266 steps for small clauses
c [cce-1-1] scheduling 1409597 clauses = 1409091 binary + 506 ternary
c [cce-1-1] tried to eliminate 347 small clauses 0%
c [cce-1-1] eliminated 144 binary clauses 0%
c [cce-1-1] eliminated 144 small clauses 0%
c [cce-1-1] eliminated 144 small clauses in 72598533 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 285 covered clauses in round 1
c [cce-1] eliminated 285 covered clauses in TOTAL during 1 rounds
c [cce-1] 285 < 1/100 * 1442268 = 14422 considered unsuccessful
c [bca-1] limit of 10000000 steps and 2884466 added (scaled 2)
c [bca-1] 204827 out of 367228 literals actually usable 56%
c [bca-1] added 8390 blocked clauses in 492654 steps
c [sweep-1] limit 4355911 penalty 0 = 0 + 0
c [sweep-1-1] 362 pos 0.2% + 183251 neg 99.8% = 183613 sched 100.0% ret 0
c [sweep-1-1] 4448727 steps 14 queries 16132.57 avg class size
c [sweep-1-1] 520 decisions 12 SAT calls 11282.58 avg env size
c [sweep-1-1] 183478 variables remain 100% (135 retained 0%)
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 0 vars in TOTAL (1 rounds, 13 queries)
c [sort-queue-4] sorted 3106 enqueued variables after 11023 conflicts
c [score-dist-4] active 180507 (98%), one 0 (0%), zero 3106 (2%)
c [score-dist-4] max exp 527, different 21 (4%)
c [score-dist-4] median active exp 523, avg 522.5
c [simplification-4] removed 27 variables 0.0% (183613 remain 92%)
c [simplification-4] removed 1210 irredundant clauses 0.1% (1441983 remain 85%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 30000
c [simplification-4] penalized conflict interval 30000 = 1 * 30000
c [simplification-4] hard conflict limit 56023 (soft 41023 + delta 15000)
c [simplification-4] new conflict limit 41023 (hard 56023)
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  208.6  183612  1441983     11136    6330    395 15075   77   150  364  51%     22  125   38   17  219%
c i  208.6  183610  1441983     11145    6337    395 15076   77   150  364  51%     22  125   38   17  219%
c i  209.5  183608  1441983     11282    6466    397 15076   75   149  364  50%     19  123   32   17  184%
c i  209.6  183593  1441983     11283    6466    397 15076   75   149  364  50%     19  123   32   17  183%
c i  209.6  183592  1441983     11284    6466    397 15076   75   149  364  50%     19  123   31   17  182%
c i  209.8  183577  1441983     11300    6480    397 15077   75   149  364  50%     19  123   32   17  185%
c i  218.4  183563  1441983     11782    6933    402 15077   70   139  365  50%     12  113   28   17  161%
c i  224.7  183562  1441983     12013    7157    404 15077   68   134  365  50%     10  107   28   17  161%
c i  244.6  183551  1441983     13233    8307    440 15078   60   126  441  48%      9   98   48   18  272%
c i  244.9  183536  1441983     13261    8328    440 15078   61   128  441  47%      9   99   57   18  321%
c 
c [simplification-5] limit of 27 iterations hit after 27 iterations
c [quatres-1] found 631 quaternary clauses 2% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 84865225 with penalty 0 = 0 + 0
c [ternres-1] all 183536 free variables schedulable
c [ternres-1] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 3394609 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 [decomp-10] removed 2 variables
c [basicprobe-2] limit 84865226 penalty 0 = 0 + 0
c [basicprobe-2-0] 166390 probes remain 91% after last round
c [basicprobe-2-0] 64 units = 64 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 98 variables, found 1524 hbrs
c [unhide-5] limit 106081 with penalty 5 = 0 + 5
c [unhide-5-5] 1 units, 8 failed, 27449 tauts, 0 hbrs, 4725328 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 44 transitive binary clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 183430 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 3394609070 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 1534 variables 1% in round 1 in 418704570 steps
c [elim-4-1] backward subsumption/strengthening limit 418704500
c [elim-4-1-1] backward checking 29555 touched variables 16%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 121512089 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 1534 = 1% variables out of 183430 scheduled
c [elim-4] 1534 < 1/100 * 183430 = 1834 considered unsuccessful
c [bca-2] limit of 10000000 steps and 2822245 added (scaled 2)
c [bca-2] 277398 out of 363794 literals actually usable 76%
c [bca-2] added 6462 blocked clauses in 866336 steps
c [sweep-2] limit 5091913 penalty 0 = 0 + 0
c [sweep-2-1] 401 pos 0.2% + 181364 neg 99.8% = 181765 sched 99.9% ret 131
c [sweep-2-1] 5361090 steps 16 queries 21492.94 avg class size
c [sweep-2-1] 567 decisions 13 SAT calls 581.23 avg env size
c [sweep-2-1] 181672 variables remain 100% (224 retained 0%)
c [decomp-11] removed 4 variables
c [sweep-2-1] removed 4 vars (0 failed, 2 eqs, 5 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 4 vars in TOTAL (1 rounds, 15 queries)
c [sort-queue-5] sorted 3051 enqueued variables after 13261 conflicts
c [score-dist-5] active 178841 (98%), one 0 (0%), zero 3051 (2%)
c [score-dist-5] max exp 527, different 20 (4%)
c [score-dist-5] median active exp 524, avg 523.2
c [simplification-5] removed 1644 variables 0.9% (181892 remain 91%)
c [simplification-5] removed 33212 irredundant clauses 2.3% (1408771 remain 83%)
c [simplification-5] maximum reduction of 2% = max (1%, 2%)
c [simplification-5] forced so keeping old conflict interval 30000
c [simplification-5] conflict limit remains at 41044 (hard 56023)
c [simplification-5] 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  289.7  181891  1408771     13280    2112    441 22946   61   129   62  47%      9  100   58   18  328%
c i  289.7  181890  1408771     13281    2112    441 22946   61   129   62  47%      9  100   58   18  327%
c i  289.7  181889  1408771     13285    2112    441 22947   61   129   62  47%      9  100   59   18  331%
c i  289.7  181874  1408771     13286    2112    441 22947   61   129   62  47%      9  100   59   18  329%
c i  289.8  181859  1408771     13288    2113    441 22947   61   129   62  47%      9  100   58   18  327%
c i  289.8  181858  1408771     13293    2115    441 22949   61   129   62  47%      9  101   58   18  324%
c i  289.8  181843  1408771     13298    2118    441 22949   61   130   62  47%      9  101   58   18  328%
c i  289.9  181828  1408771     13300    2119    441 22949   61   130   62  47%      9  101   58   18  327%
c i  289.9  181814  1408771     13301    2119    441 22949   61   130   62  47%      9  101   58   18  326%
c i  289.9  181799  1408771     13307    2123    441 22950   61   130   62  47%      9  101   57   18  321%
c i  290.0  181798  1408771     13323    2131    442 22953   61   130   63  47%      8  102   60   18  334%
c i  290.0  181797  1408771     13324    2131    442 22953   61   130   63  47%      8  102   59   18  332%
c i  290.0  181796  1408771     13327    2132    442 22954   61   130   63  46%      8  102   59   18  329%
c i  290.0  181781  1408771     13329    2132    442 22955   61   130   63  46%      8  102   58   18  326%
c i  290.0  181765  1408771     13330    2132    442 22955   61   130   63  46%      8  102   58   18  325%
c i  290.0  181750  1408771     13331    2132    442 22955   61   130   63  46%      8  102   58   18  324%
c i  290.0  181735  1408771     13332    2132    442 22955   61   130   63  46%      8  102   57   18  322%
c i  290.1  181720  1408771     13334    2133    442 22955   61   130   63  46%      8  102   57   18  320%
c i  290.1  181705  1408771     13342    2138    442 22957   61   130   63  46%      8  102   57   18  320%
c i  290.1  181690  1408771     13345    2138    442 22957   61   131   63  46%      8  102   58   18  324%
c i  290.1  181689  1408771     13346    2138    442 22957   61   130   63  46%      8  102   58   18  323%
c i  290.2  181675  1408771     13353    2143    442 22958   60   131   63  46%      8  102   57   18  317%
c i  290.2  181674  1408771     13369    2155    442 22961   60   131   63  46%      8  102   55   18  310%
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  290.3  181659  1408771     13370    2155    442 22961   60   131   63  46%      8  102   55   18  309%
c i  290.4  181643  1408771     13406    2178    445 22966   60   132   63  46%      8  104   56   18  314%
c i  290.5  181628  1408771     13419    2183    446 22972   60   133   63  45%      7  104   56   18  312%
c i  290.7  181613  1408771     13482    2229    449 22972   60   135   63  45%      7  106   56   18  313%
c i  291.0  181612  1408771     13560    2276    460 22973   61   141   63  44%      6  112   72   18  399%
c i  291.0  181611  1408771     13561    2276    460 22973   61   141   63  44%      6  112   72   18  397%
c i  291.1  181590  1408771     13569    2281    460 22974   61   141   63  44%      6  112   70   18  390%
c i  291.5  181589  1408771     13658    2343    463 22978   63   146   63  43%      6  116   86   18  471%
c i  291.5  181588  1408771     13671    2355    463 22978   63   146   63  43%      5  117   84   18  460%
c i  291.5  181574  1408771     13676    2359    463 22978   62   146   63  43%      5  117   82   18  453%
c i  291.6  181553  1408771     13680    2361    463 22978   63   146   63  43%      5  117   82   18  453%
c i  291.6  181552  1408771     13692    2371    463 22978   63   147   63  43%      5  117   83   18  457%
c i  291.7  181551  1408771     13702    2375    463 22979   63   147   63  43%      5  118   85   18  467%
c i  291.7  181530  1408771     13713    2383    463 22980   63   148   63  43%      5  118   87   18  478%
c i  291.8  181529  1408771     13729    2389    464 22980   63   149   63  42%      5  120   87   18  478%
c i  291.9  181519  1408771     13755    2401    466 22980   64   151   63  42%      5  121   99   18  540%
c i  292.0  181498  1408771     13767    2408    466 22980   64   151   63  43%      5  122  103   18  559%
c i  292.1  181497  1408771     13781    2421    466 22980   65   152   63  43%      5  122  105   18  570%
c i  292.6  181496  1408771     13872    2462    471 22981   67   156   63  43%      4  126  130   19  699%
c i  292.6  181476  1408771     13873    2462    471 22981   67   156   63  43%      4  126  130   19  696%
c i  292.6  181475  1408771     13875    2463    471 22981   67   156   63  43%      4  126  129   19  691%
c i  292.8  181454  1408771     13914    2490    475 22981   68   157   63  43%      4  128  122   19  655%
c i  292.8  181453  1408771     13915    2490    475 22981   68   157   63  43%      4  128  122   19  652%
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  292.8  181432  1408771     13917    2491    475 22981   68   157   63  43%      4  128  121   19  648%
c i  292.8  181431  1408771     13926    2497    476 22981   68   158   63  43%      4  128  119   19  640%
c i  292.9  181411  1408771     13930    2499    476 22981   68   158   63  43%      4  128  118   19  635%
c i  292.9  181390  1408771     13934    2499    477 22981   68   158   63  43%      4  128  118   19  631%
c i  293.0  181389  1408771     13967    2518    478 22982   68   158   64  43%      4  129  117   19  626%
c i  293.2  181388  1408771     13984    2531    478 22982   68   159   64  43%      4  129  116   19  617%
c i  294.5  180724  1408771     14282    2733    495 22988   70   165   65  43%      3  135  105   19  552%
c i  294.6  180723  1408771     14289    2738    495 22988   70   165   65  42%      3  135  104   19  546%
c i  295.1  180720  1408771     14386    2805    497 22993   71   166   66  43%      2  136  101   19  523%
c i  295.1  180719  1408771     14389    2807    497 22993   71   166   66  43%      2  136  100   19  519%
c i  295.1  180718  1408771     14395    2809    498 22993   71   166   66  43%      2  135   99   19  517%
c i  295.1  180717  1408771     14398    2810    498 22993   71   166   66  43%      2  135   99   19  515%
c i  295.2  180707  1408771     14399    2810    498 22993   71   166   66  43%      2  135   99   19  513%
c i  295.2  180706  1408771     14400    2810    498 22993   71   166   66  43%      2  135   98   19  511%
c i  295.2  180705  1408771     14410    2816    498 22993   71   166   66  43%      2  135   98   19  509%
c i  295.3  180704  1408771     14412    2817    498 22993   71   166   66  43%      2  135   97   19  506%
c i  295.3  180703  1408771     14415    2819    498 22993   71   166   66  43%      2  135   97   19  503%
c i  295.3  180702  1408771     14420    2823    498 22993   71   166   66  43%      2  135   96   19  499%
c i  295.4  180701  1408771     14428    2827    498 22993   71   166   66  43%      2  135   97   19  501%
c i  295.4  180693  1408771     14429    2827    498 22993   71   166   66  43%      2  135   96   19  500%
c i  295.4  180692  1408771     14431    2827    498 22993   71   166   66  43%      2  135   96   19  499%
c i  295.4  180684  1408771     14432    2827    498 22993   71   166   66  43%      2  135   96   19  497%
c i  295.4  180683  1408771     14434    2828    498 22993   71   166   66  43%      2  135   95   19  493%
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  295.4  180682  1408771     14436    2829    498 22993   71   166   66  43%      2  135   95   19  491%
c i  295.4  180681  1408771     14439    2830    498 22993   71   166   66  43%      2  135   94   19  489%
c i  295.5  180680  1408771     14441    2831    498 22993   71   166   66  43%      2  135   94   19  486%
c i  295.5  180679  1408771     14442    2831    498 22993   71   166   66  43%      2  135   93   19  484%
c i  295.5  180678  1408771     14446    2834    498 22993   71   166   66  43%      2  135   92   19  480%
c i  295.9  180677  1408771     14504    2877    499 22993   71   166   66  43%      2  135   90   19  465%
c i  295.9  180676  1408771     14511    2881    499 22993   71   166   67  43%      2  135   89   19  462%
c i  297.8  180675  1408771     14857    3148    509 23002   71   167   72  42%      1  136   75   20  382%
c i  299.0  180674  1408771     15066    3296    513 23005   71   167   74  43%      1  135   75   20  379%
c i  299.0  180673  1408771     15067    3296    513 23005   71   167   74  43%      1  135   74   20  377%
c i  299.0  180672  1408771     15068    3296    513 23005   71   167   74  43%      1  135   74   20  376%
c i  299.0  180671  1408771     15069    3296    513 23005   71   167   74  43%      1  135   74   20  374%
c i  300.1  180670  1408771     15246    3427    533 23005   69   167   79  42%      1  135   56   20  285%
c i  300.7  180668  1408771     15313    3480    533 23006   69   167   84  42%      1  134   56   20  282%
c i  301.1  180667  1408771     15390    3536    534 23007   69   167   84  41%      0  135   62   20  313%
c i  302.7  180666  1408771     15681    3745    537 23007   70   167   86  42%      0  133   67   20  335%
c i  302.7  180665  1408771     15684    3746    537 23007   70   167   86  42%      0  133   67   20  334%
c i  302.7  180664  1408771     15686    3747    537 23007   70   167   86  42%      0  133   67   20  332%
c i  302.7  180662  1408771     15687    3747    537 23007   70   166   86  42%      0  133   67   20  331%
c i  304.7  180661  1408771     15940    3899    540 23007   71   165   94  43%      0  131   82   20  401%
c i  304.8  180660  1408771     15948    3905    540 23007   71   165   94  43%      0  131   81   20  396%
c i  306.5  180659  1408771     16249    4141    546 23008   70   163   95  43%      0  129   72   21  348%
c i  330.2  180658  1408771     19812    6706    640 23095   76   178  133  43%     37  136  105   24  449%
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  330.3  180652  1408771     19837    6724    640 23096   76   178  133  43%     36  137  103   24  439%
c i  330.8  180638  1408771     19945    6817    642 23096   75   178  133  42%     32  137   87   24  368%
c i  334.6  180637  1408771     20810    7279    645 23099   85   184  133  46%     16  141  141   25  566%
c i  334.6  180636  1408771     20812    7280    645 23099   85   184  133  46%     16  141  140   25  562%
c i  338.7  180635  1408771     21679    7714    671 23108   97   196  134  50%      9  151  179   26  675%
c i  343.7  180633  1408771     22806    8170    673 23111  123   219  150  56%      8  171  182   29  617%
c i  351.3  180628  1408771     24575    8863    677 23115  152   243  152  63%     13  190  219   34  642%
c i  352.0  180619  1408771     24719    8888    677 23116  155   244  152  64%     11  191  226   35  653%
c 
c [simplification-6] limit of 127 iterations hit after 127 iterations
c [ternres-2] limit 28363046 with penalty 0 = 0 + 0
c [ternres-2] all 180618 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 3545380 penalty 2 = 2 + 0
c [card-3] found 112 at-most-one constraints of average size 25.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 3545380 for elimination
c [card-3] 112 out of 112 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] generated 998 at-most-one constraints, 969 used 97%
c [card-3] exported 7138 binary clauses, 7.4 per/constraint
c [decomp-12] removed 1298 variables
c [simpleprobe-3] 131508 schedulable variables 73%
c [simpleprobe-3] limit 113452184 penalty 0 = 0 + 0
c [decomp-13] removed 7060 variables
c [simpleprobe-3] 1175 variables remain 1% (172359 retained 99%)
c [simpleprobe-3] removed 7060 variables, found 103260 hbrs, 3086 units
c [unhide-6] limit 709076 with penalty 3 = 0 + 3
c [unhide-6-6] 1 units, 4 failed, 2117 tauts, 0 hbrs, 2244204 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 33 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 173511 variables 100%
c [block-2] limit of 141815231 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 70907615 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 71 clauses out of 250 (28%) of length 541
c [cce-2-1] eliminated 26 clauses out of 65 (40%) of length 540
c [cce-2-1] eliminated 6 clauses out of 21 (29%) of length 539
c [cce-2-1] eliminated 1 clauses out of 4 (25%) of length 538
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 536
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 534
c [cce-2-1] eliminated 22 clauses out of 22 (100%) of length 531
c [cce-2-1] eliminated 9 clauses out of 9 (100%) of length 530
c [cce-2-1] eliminated 4 clauses out of 5 (80%) of length 529
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 527
c [cce-2-1] eliminated 9 clauses out of 17 (53%) of length 520
c [cce-2-1] eliminated 2 clauses out of 4 (50%) of length 519
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 509
c [cce-2-1] eliminated 7 clauses out of 7 (100%) of length 482
c [cce-2-1] eliminated 3 clauses out of 3 (100%) of length 481
c [cce-2-1] eliminated 4 clauses out of 4 (100%) of length 477
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 476
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 475
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 472
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 465
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 429
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 416
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 415
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 405
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 397
c [cce-2-1] eliminated 4 clauses out of 8 (50%) of length 391
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 390
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 388
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 380
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 376
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 375
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 371
c [cce-2-1] eliminated 3 clauses out of 3 (100%) of length 370
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 369
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 368
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 366
c [cce-2-1] eliminated 4 clauses out of 4 (100%) of length 350
c [cce-2-1] eliminated 3 clauses out of 3 (100%) of length 349
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 345
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 340
c [cce-2-1] eliminated 6 clauses out of 14 (43%) of length 316
c [cce-2-1] eliminated 7 clauses out of 7 (100%) of length 301
c [cce-2-1] eliminated 1 clauses out of 5 (20%) of length 296
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 295
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 294
c [cce-2-1] eliminated 3 clauses out of 5 (60%) of length 291
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 288
c [cce-2-1] eliminated 3 clauses out of 4 (75%) of length 275
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 272
c [cce-2-1] eliminated 4 clauses out of 4 (100%) of length 270
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 268
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 262
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 254
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 250
c [cce-2-1] eliminated 3 clauses out of 3 (100%) of length 195
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 194
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 189
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 181
c [cce-2-1] eliminated 2 clauses out of 3 (67%) of length 176
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 173
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 153
c [cce-2-1] eliminated 1 clauses out of 5 (20%) of length 149
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 248 large clauses in 70908131 steps
c [cce-2-1] allowing another 35454065 steps for small clauses
c [cce-2-1] scheduling 1314266 clauses = 1314123 binary + 143 ternary
c [cce-2-1] tried to eliminate 335 small clauses 0%
c [cce-2-1] eliminated 82 binary clauses 0%
c [cce-2-1] eliminated 82 small clauses 0%
c [cce-2-1] eliminated 82 small clauses in 70907616 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 330 covered clauses in round 1
c [cce-2] eliminated 330 covered clauses in TOTAL during 1 rounds
c [cce-2] 330 < 1/100 * 1346711 = 13467 considered unsuccessful
c [bca-3] limit of 10000000 steps and 2700688 added (scaled 2)
c [bca-3] 206093 out of 347024 literals actually usable 59%
c [bca-3] added 1893 blocked clauses in 509228 steps
c [sweep-3] limit 8508913 penalty 0 = 0 + 0
c [sweep-3-1] 366 pos 0.2% + 172927 neg 99.8% = 173293 sched 99.9% ret 218
c [sweep-3-1] 8640940 steps 32 queries 17619.25 avg class size
c [sweep-3-1] 815 decisions 27 SAT calls 1169.78 avg env size
c [sweep-3-1] 172746 variables remain 100% (763 retained 0%)
c [decomp-14] removed 7 variables
c [sweep-3-1] removed 7 vars (0 failed, 5 eqs, 11 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 7 vars in TOTAL (1 rounds, 31 queries)
c [sort-queue-6] sorted 3042 enqueued variables after 24719 conflicts
c [score-dist-6] active 170462 (98%), one 0 (0%), zero 3042 (2%)
c [score-dist-6] max exp 529, different 20 (4%)
c [score-dist-6] median active exp 525, avg 523.8
c [simplification-6] removed 7114 variables 3.9% (173504 remain 87%)
c [simplification-6] removed 62406 irredundant clauses 4.4% (1346365 remain 80%)
c [simplification-6] maximum reduction of 4% = max (4%, 4%)
c [simplification-6] forced so keeping old conflict interval 30000
c [simplification-6] conflict limit remains at 41370 (hard 56023)
c [simplification-6] new iteration interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  372.4  173503  1346365     24753    8649    663 128969  156   244  136  64%     10  191  222   35  640%
c i  376.5  173502  1346365     25704    9025    670 128972  157   240  151  65%      7  184  149   36  409%
c i  377.9  173501  1346365     25966    9107    671 128973  157   237  151  66%      5  180  147   37  399%
c i  377.9  173500  1346365     25967    9107    671 128973  156   237  151  66%      5  180  147   37  397%
c i  377.9  173499  1346365     25968    9107    671 128973  156   237  151  66%      5  180  146   37  396%
c i  377.9  173498  1346365     25969    9107    671 128973  156   237  151  66%      5  180  145   37  394%
c i  377.9  173497  1346365     25971    9108    671 128973  156   237  151  66%      5  180  145   37  393%
c i  377.9  173496  1346365     25973    9109    671 128973  156   237  151  66%      5  180  144   37  391%
c i  378.0  173495  1346365     25994    9116    671 128973  156   236  151  66%      5  179  144   37  388%
c i  378.0  173494  1346365     25995    9116    671 128973  156   236  151  66%      5  179  143   37  387%
c i  409.1  173493  1346365     32599   11913    759 129007  144   219  155  66%     80  147  139   47  299%
c i  410.8  173455  1346365     33092   12202    807 129019  138   215  155  64%     48  143   89   47  190%
c i  418.6  173445  1346365     34940   13587    859 129037  112   182  155  62%     16  106   56   47  119%
c i  422.4  173444  1346365     35763   14304    889 129046  101   164  155  61%      6   87   44   47   92%
c i  447.6  173438  1346365     39494   17653    970 129065   66   103  278  64%     34   23   46   47   98%
c 
c [simplification-7] limit 41420 conflicts (hard 56023) hit after 41420 conflicts
c [quatres-2] found 759 quaternary clauses 2% in total
c [gauss-2] limit 4322364 penalty 1 = 1 + 0
c [gauss-2] extracted 2 xors of average arity 2.5
c [gauss-2] connected 5 occurrences of 5 variables (average 1.0)
c [gauss-2] limit 4322364 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 5 variables
c [treelook-3] limit 4322364 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 326316 literals 94%
c [treelook-3] scheduling used 3519839 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 4322364 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 4525263 steps
c [treelook-3] 326308 literals remain 94%
c [treelook-3] 139871 variables remain to probed next time 81%
c [treelook-3] removed 0 variables, found 5826 hbrs
c [unhide-7] limit 540295 with penalty 4 = 0 + 4
c [unhide-7-7] 1 units, 2 failed, 13976 tauts, 0 hbrs, 3539501 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 4 transitive binary clauses
c [bca-4] limit of 10000000 steps and 2672512 added (scaled 2)
c [bca-4] 199238 out of 346860 literals actually usable 57%
c [bca-4] added 0 blocked clauses in 495321 steps
c [sweep-4] limit 12967092 penalty 0 = 0 + 0
c [sweep-4-1] 295 pos 0.2% + 172375 neg 99.8% = 172670 sched 99.6% ret 759
c [sweep-4-1] 13306766 steps 39 queries 8905.87 avg class size
c [sweep-4-1] 1257 decisions 39 SAT calls 5733.00 avg env size
c [sweep-4-1] 168737 variables remain 97% (4692 retained 3%)
c [decomp-17] removed 2 variables
c [sweep-4-1] removed 2 vars (0 failed, 1 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 2 vars in TOTAL (1 rounds, 38 queries)
c [sort-queue-7] sorted 3038 enqueued variables after 41420 conflicts
c [score-dist-7] active 170389 (98%), one 0 (0%), zero 3038 (2%)
c [score-dist-7] max exp 531, different 22 (4%)
c [score-dist-7] median active exp 525, avg 524.5
c [simplification-7] removed 11 variables 0.0% (173427 remain 87%)
c [simplification-7] removed 14549 irredundant clauses 1.1% (1331816 remain 79%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 15000 = 30000 / 2
c [simplification-7] new conflict interval 45000
c [simplification-7] penalized conflict interval 45000 = 1 * 45000
c [simplification-7] hard conflict limit 108920 (soft 86420 + delta 22500)
c [simplification-7] new conflict limit 86420 (hard 108920)
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  476.1  173426  1331816     41526   19176   1006 134986   68   101  349  67%     14   20   62   48  130%
c i  486.6  173425  1331816     43245   20464   1029 134998   70   104  375  67%      8   23   73   48  151%
c i  503.4  173418  1331816     45700   22392   1046 135001   71    99  375  71%     15   17   51   49  103%
c i  503.4  173413  1331816     45701   22392   1046 135001   71    99  375  71%     15   17   51   49  103%
c i  526.4  173407  1331816     49087   25219   1077 135012   64    88  375  73%     27    5   48   50   97%
c i  526.5  173406  1331816     49094   25221   1080 135012   64    88  375  73%     27    6   47   50   96%
c i  526.5  173405  1331816     49095   25221   1080 135012   64    88  375  73%     27    6   47   50   95%
c i  526.5  173404  1331816     49098   25223   1080 135012   64    88  375  73%     27    6   47   50   94%
c i  526.5  173403  1331816     49113   25225   1084 135019   64    88  375  72%     27    6   45   50   90%
c i  526.6  173402  1331816     49116   25225   1085 135020   64    88  375  72%     26    6   44   50   89%
c i  526.6  173401  1331816     49118   25225   1086 135020   64    88  375  72%     26    6   44   50   88%
c i  532.6  173400  1331816     49835   25812   1130 135057   60    88  375  68%     11    5   37   50   74%
c i  572.4  173399  1331816     54152   29462   1197 135070   59    98  671  60%     40   15   69   50  137%
c i  584.3  173397  1331816     56370   30483   1225 135076   88   136  675  65%     14   51   94   53  179%
c i  585.5  173396  1331816     56542   30596   1229 135077   88   135  675  65%     10   50   90   53  170%
c i  627.0  173394  1331816     62525   33719   1282 135092  104   145  681  71%     63   56   91   57  160%
c i  668.3  173393  1331816     68569   36967   1348 135103  103   138  694  75%     61   44  126   61  207%
c i  709.0  173383  1331816     73987   40234   1375 135105   92   119  789  77%     49   22   74   63  117%
c i  790.8  173382  1331816     82778   47549   1443 135117   69    93 1081  74%     96   -5   47   64   73%
c i  791.0  173381  1331816     82799   47569   1443 135117   69    93 1081  74%     94   -5   46   64   71%
c i  791.1  173380  1331816     82818   47581   1443 135118   69    93 1081  74%     91   -5   46   64   72%
c i  791.1  173379  1331816     82826   47585   1443 135119   69    93 1081  74%     90   -5   46   64   71%
c i  791.1  173378  1331816     82828   47586   1443 135119   69    93 1081  74%     90   -5   46   64   71%
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  791.2  173377  1331816     82835   47590   1444 135120   69    93 1081  74%     89   -5   45   64   71%
c i  804.7  173376  1331816     84730   49190   1525 135132   62    99 1081  63%      8    1   80   64  126%
c i  806.3  173375  1331816     84969   49339   1531 135137   63   102 1081  62%      1    5   85   64  133%
c 
c [simplification-8] limit 86459 conflicts (hard 108920) hit after 87411 conflicts
c [ternres-3] limit 48181065 with penalty 1 = 1 + 0
c [ternres-3] all 173375 free variables schedulable
c [ternres-3] 53 ternary resolvents (0 bin, 53 trn)
c [ternres-3] fully completed ternary resolution
c [decomp-18] removed 56 variables
c [basicprobe-3] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-3-0] 155618 probes remain 90% after last round
c [basicprobe-3-0] 268 units = 268 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 288 variables, found 8178 hbrs
c [unhide-8] limit 602263 with penalty 5 = 0 + 5
c [unhide-8-8] 1 units, 22 failed, 1131 tauts, 0 hbrs, 27765159 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 20 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 173061 variables 100%
c [elim-5] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 269 not tried 0% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1581 = 1% variables out of 173061 scheduled
c [elim-5] 1581 < 1/100 * 173061 = 1730 considered unsuccessful
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 289086390 penalty 0 = 0 + 0
c [sweep-5-1] 243 pos 0.1% + 166618 neg 99.9% = 166861 sched 97.3% ret 4619
c [sweep-5-1] 290215405 steps 637 queries 525.60 avg class size
c [sweep-5-1] 4312 decisions 449 SAT calls 677.86 avg env size
c [sweep-5-1] 19127 variables remain 11% (152270 retained 89%)
c [decomp-19] removed 291 variables
c [sweep-5-1] removed 291 vars (0 failed, 208 eqs, 414 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 291 vars in TOTAL (1 rounds, 636 queries)
c [sort-queue-8] sorted 2727 enqueued variables after 87411 conflicts
c [score-dist-8] active 168462 (98%), one 0 (0%), zero 2727 (2%)
c [score-dist-8] max exp 533, different 22 (4%)
c [score-dist-8] median active exp 528, avg 527.4
c [simplification-8] removed 2186 variables 1.3% (171189 remain 86%)
c [simplification-8] removed 6745 irredundant clauses 0.5% (1325071 remain 78%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 22500 = 45000 / 2
c [simplification-8] new conflict interval 67500
c [simplification-8] penalized conflict interval 67500 = 1 * 67500
c [simplification-8] hard conflict limit 188661 (soft 154911 + delta 33750)
c [simplification-8] new conflict limit 154911 (hard 188661)
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  907.1  171188  1325071     88041   15191   1577 154160   65   108  103  60%      8   10   61   64   96%
c i  919.3  171187  1325071     89647   16340   1589 154165   73   119  138  61%     -7   21   99   65  153%
c i  919.5  171185  1325071     89682   16353   1590 154165   73   120  138  61%     -7   21  103   65  159%
c i  921.8  171170  1325071     90035   16463   1591 154165   79   123  138  64%    -12   25  127   65  196%
c i  929.7  171169  1325071     91033   16859   1594 154168   85   125  138  67%    -15   26  108   66  164%
c i  932.7  171168  1325071     91465   17191   1597 154169   84   126  146  67%    -17   27   92   66  141%
c i  933.9  171167  1325071     91635   17255   1599 154171   86   128  146  67%    -18   29  106   66  160%
c i  934.2  171163  1325071     91692   17289   1599 154172   86   128  146  67%    -19   28  100   66  151%
c i  979.9  171158  1325071     96953   20681   1630 154183   83   122  321  68%     40   20   79   68  117%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 4 count, 16745 added (3241 skipped), 2363539 steps
c bkwd: tried 323283 clauses, 646566 lits, 2.00 lits/clause
c bkwd: checked 117875429 occs, 364.62 occs/clause, 182.31 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, 642 removed, 8208305 resolutions, 22103690 steps
c blkd: 1812 blocking literals 0%, 0 pure
c bump: 96674 bumped seen, 604322198 lits 6251.1 on average
c card: 3 count, 0 units, 15586 am1, 255635169 steps
c card: 34 rescheduled, 314 eliminated, 30370 resolved, 4140 subsumed
c card: 157 at-most-one constraints found, average size 28.72
c card: 157 at-most-one constraints used 100%, average size 28.72
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, 615 eliminated, 615 ate 100%, 0 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 7303370 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 49 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 19 decompositions, 955 equivalent 0%
c deco: 27847 decision-only clauses 29%, 96% reduction
c decs: 1402375 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 5 elims, 8273 eliminated 3%, 0 pure 0%
c elms: 7 rounds, 1.4 rounds/bve
c elms: 4462 small 54%, 3811 large 46%
c elms: 5019 tried small, 4462 succeeded 89%, 557 failed 11%
c elms: 7365 subsumed, 40162 strengthened, 1754 blocked
c elms: 10451481 copies, 12013317 resolutions, 81562 ipos
c elms: 54475507 subchks, 32309117 strchks
c gaus: 2 extractions, 2 extracted, 2.5 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 15437164 steps, 7718582 extr 50%, 7 elim 0%
c glue: 91.7 orig avg, 91.7 real avg, 7.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 138048 = 105817 simple 77% + 24295 trn 18% + 7936 lrg 6%, 49 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 96673 clauses, 3707.4 length
c lrnd: 358406361 lits = 481063471 orig - 122657110 removed 25%
c lrnd: 38340 uips 40%, 50467 flips 52%
c mins: 40655 mins 58%, 547 bin 1%, 1466 size 2%
c mins: 33972930 poisoned searches, 18046030 hits, 53% hit rate
c mins: 42043212 used twice searches, 1251212 hits, 3% hit rate
c move: moved 521, 520 bin 100%, 1 trn 0%
c otfs: 2214 driving 2%, 105371 restarting 98%
c otfs: str 107585, 107582 red 100%, 3 irr 0%
c otfs: str 107585, 0 bin 0%, 9 trn 0%, 107576 lrg 100%
c otfs: sub 8, 8 red 100%, 0 irr 0%
c otfs: sub 8, 0 bin 0%, 0 trn 0%, 8 lrg 100%
c phas: 2 computed, 185040 set, 0 pos (0%), 185040 neg (100%)
c prbs: 3 basic, 2850 probed, 337 failed, 0 lifted
c prbs: 3 simple, 905835 probed, 5107 failed, 211 eqs
c prbs: 3 treelook, 18 probed, 4 failed, 0 lifted
c prom: 0 locked 0% out of 184413 tried
c prps: 2752213291 props, 1878 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c quat: 2 count, 0 quat, 0 self1, 0 self2, 1 dup
c queu: 8 sorted, 1402375 next (11901 steps 0.01)
c queu: 604807474 enq (4878215413 steps 8.07), 604322198 deq 100%
c redc: 2627 clauses 71%, 3718 tried 4%, 8 sat 0%
c redc: 14645 lits 36%, 40962 tried 0%, 8 sat 0%
c redc: 387 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: 9986 removed, 312 red 3%
c rsts: 5149 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: 8 count, 5 confs 62%, 0 vars 0%
c simp: 2 its 25%, 1 bin 12%, 0 trns 0%
c subl: 96673 count (117916 tried 1.2), 26834 sub out of 94089 (28.5%)
c swps: 5 count, 5 rounds, 733 queries (146.6/round)
c swps: 540 sat calls, 25 unsat (0.3% success rate)
c swps: 7471 decisions 13.8, 173 conflicts 0.3
c swps; 2477.1 avg class size, 1300.9 avg environment size
c swps: 0 failed, 430 impls, 216 equivs
c swp0: 243 type 0 queries, 161 unsat (66.3%), 171 sat (70.4%)
c swp1: 490 type 1 queries, 317 unsat (64.7%), 346 sat (70.6%)
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: 2998398 calls to obtain time
c tops: 76994 fixed 30%, 177 its, 557.71 confs/it
c trds: 4 transitive reductions, 101 removed, 0 failed
c trds: 1100 nodes, 4041 edges, 8047058 steps
c trim: 3908775 words, 14.9 MB
c trnr: 3 count, 0 bin, 55 trn, 10643588 steps
c unhd: 8 count, 8 rounds, 49701854 steps
c unhd: 4 non-trivial sccs of average size 2.0
c unhd: 48 units, 48 bin, 0 trn, 0 lrg
c unhd: 54 failed, 48 stamp, 0 lits, 0 bin, 1 trn, 0 lrg
c unhd: 155718 tauts, 26 bin 0%, 3 trn 0%, 179 lrg 0%
c unhd: 155718 tauts, 155510 stamp 100%, 4616 red 3%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 46113787 str, 48 bin 0%, 36 trn 0%, 46113703 lrg 100%, 46113575 red 100%
c vars: 171158 remaining 67% and 86222 removed 33% out of 257380
c vars: 76994 fixed 30%, 8273 eliminated 3%, 955 equivalent 0%
c vsts: 11589044785 visits, 95% srch, 5% simp, 0% lkhd
c vsts: 4.2 search visits per propagation, 111930.7 per conflict
c wchs: 308600211 pushed, 69602323 enlarged, 76 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all          94089             0             0       4765117       1376922        158356
c 
c  0 0          2675   3         0   0<        0   0<  1237284  26    225735  16      3985   3     1.7
c  1 5           692   1         0   0         0   0    269565   6     64700   5      1619   1     1.3
c  2 6          2242   2         0   0         0   0    622816  13    142601  10      5127   3     7.4
c  3 9          4093   4         0   0         0   0    836411  18<   178617  13     12023   8    15.7
c  4 14         4798   5         0   0         0   0    587265  12    145727  11<     8775   6    19.1
c  5 21         5209   6         0   0         0   0    315619   7    108535   8      9948   6    18.4
c  6 30         6438   7         0   0         0   0    274394   6    103983   8     13177   8    49.4
c  7 41         8356   9         0   0         0   0    238521   5    109808   8     23098  15<  101.9
c  8 54         8845   9<        0   0         0   0    114470   2     97560   7     29611  19   152.7
c  9 69        10469  11         0   0         0   0    108301   2     97531   7     29478  19   206.1
c 10 86        17712  19         0   0         0   0    104297   2     78961   6     20132  13   193.9
c 11 126       16516  18         0   0         0   0     38039   1     16745   1       826   1     4.0
c 12 230        5179   6         0   0         0   0     16157   0      5609   0       526   0     2.7
c 13 534         862   1         0   0         0   0      1962   0       808   0        30   0     1.9
c 14 1526          3   0         0   0         0   0        16   0         2   0         1   0     0.0
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                  8.0           0.0           0.0           3.1           4.4           6.9
c std                  3.1           0.0           0.0           2.8           3.2           2.6
c 
c  279.434  28% bump
c   80.082   8% unhide
c   61.623   6% elim
c   29.405   3% probe
c   16.359   2% block
c   11.810   1% sweep
c 
c   13.969 < 1% rest (below)
c 
c    4.339   0% cce
c    3.837   0% bca
c    2.836   0% gauss
c    1.383   0% decide
c    1.255   0% card
c    0.150   0% transred
c    0.148   0% ternres
c    0.020   0% quatres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    8.591   1% preprocessing     4%
c  218.568  22% inprocessing     96%
c ==================================
c  227.158  23% simplifying
c  771.816  77% search
c ==================================
c  998.977 100% all
c 
c         98715 conflicts,          98.8 confs/sec
c          1629 ternaries,          60.6 confs/ternary
c           648 binaries,          152.3 confs/binary
c           177 iterations,        557.7 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          5149 restarts,            5.2 rests/sec,     19.2 confs/restart
c       1402375 decisions,        1403.8 decis/sec,     14.2 decis/conflict
c    2752213291 propagations,  2755031.2 props/sec,   1962.5 props/decision
c 
c 999.0 seconds, 1292.0 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
