c launch: /data/cnf/sc2014/app/partial-10-17-s.cnf.bz2
c host: atom01
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/partial-10-17-s.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/partial-10-17-s.cnf.bz2
c no embedded options
c found 'p cnf 298900 1409628' header
c read 298900 variables, 1409628 clauses, 3261218 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=2
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 287740 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] VMTF (--score=2)
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  287740  1385857         0       0      0     0    0     0   64   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 11220 at-most-one constraints of average size 5.2
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 11220 out of 11220 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 129705 variables
c [simpleprobe-1] all 169195 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 1390 variables
c [simpleprobe-1] 7799 variables remain 5% (160006 retained 95%)
c [simpleprobe-1] removed 1390 variables, found 18529 hbrs, 9 units
c [unhide-1] limit 60588 based on 969417 irredundant clauses
c [unhide-1-1] 1 units, 196 failed, 8012 tauts, 0 hbrs, 9081 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 167330 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 60911 not tried 36% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 62796 = 38% variables out of 167330 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 733852 negative 99.2% of 739575 except 5723 0.8%
c [phase-count-1] 592701 positive 80.1% of 739575 except 146874 19.9%
c [phase-count-1] less non-negative clauses 5723 than limit 73900 (10.0%)
c [phase-count-1] non-pos/non-neg = 146874/5723 = 25.66 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 104534 negative 100%
c [sort-queue-1] sorted 104534 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 104534 (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 136559 variables 56.6% (104534 remain 36%)
c [simplification-1] removed 646282 irredundant clauses 46.6% (739575 remain 53%)
c [simplification-1] maximum reduction of 57% = max (57%, 47%)
c [simplification-1] large reduction 57% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    4.9  104533   739575        89      76      5 10793    0     9   55   6%      0    9    6    0 20444%
c i    4.9  104376   739575        91      77      5 10793    0     9   55   6%      0    9    6    0 20290%
c i    5.0  104335   739575       128     101     10 10796    1    10   55   5%      0   10    6    0 18250%
c i    5.0  104108   739575       164     128     14 10799    1    11   55   5%      0   11    6    0 16515%
c i    5.4  104096   739575       515     434     35 10816    2    19   55   9%      1   19   13    0 11168%
c i    5.5  103863   739575       687     592     44 10820    2    22   55  11%      1   22   15    0 9276%
c i    5.5  103686   739575       699     599     47 10821    2    22   55  11%      1   22   14    0 8975%
c i    5.6  103672   739575       757     650     51 10823    2    23   55  11%      1   23   13    0 7844%
c i    5.6  103661   739575       769     659     51 10825    2    24   55  10%      1   24   13    0 7545%
c i    5.6  103648   739575       772     659     51 10827    2    24   55  10%      1   24   13    0 7461%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 1084 variables
c [simpleprobe-2] 7500 schedulable variables 7%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 7188 variables remain 7% (96262 retained 93%)
c [simpleprobe-2] removed 0 variables, found 1853 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 74090 literals 36%
c [treelook-1] scheduling used 512237 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 347563 steps
c [treelook-1] 74080 literals remain 36%
c [treelook-1] 73844 variables remain to probed next time 71%
c [treelook-1] removed 3 variables, found 1914 hbrs
c [basicprobe-1] limit 5863064 based on 732883 irredundant clauses
c [basicprobe-1-0] 33583 probes remain 35% after last round
c [basicprobe-1-0] 33 units = 33 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 7777 variables, found 14855 hbrs
c [unhide-2] limit 50000 with penalty 1 = 0 + 1
c [unhide-2-2] 0 units, 228 failed, 5149 tauts, 0 hbrs, 14791 literals
c [elim-2] 57304 variables 60% will be scheduled this time
c [elim-2] scheduled 57304 variables 60%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 18828 not tried 20% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 596 = 1% variables out of 57304 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 649770 negative 99.1% of 655493 except 5723 0.9%
c [phase-count-2] 526353 positive 80.3% of 655493 except 129140 19.7%
c [phase-count-2] less non-negative clauses 5723 than limit 65500 (10.0%)
c [phase-count-2] non-pos/non-neg = 129140/5723 = 22.57 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 5348 negative 100%
c [sort-queue-2] sorted 94178 enqueued variables after 772 conflicts
c [score-dist-2] active 0 (0%), one 11238 (12%), zero 82940 (88%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 9301 variables 9.0% (94178 remain 33%)
c [simplification-2] removed 84082 irredundant clauses 11.4% (655493 remain 47%)
c [simplification-2] maximum reduction of 11% = max (9%, 11%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1008 (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    9.0   94177   655493       926     746     66 20830    3    28   51   9%      1   28   10    0 5372%
c i    9.1   94166   655493       998     803     74 20834    3    30   51  10%      1   30   12    0 6095%
c 
c [simplification-3] limit 1008 conflicts (hard 11000) hit after 1008 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4012 at-most-one constraints of average size 4.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4012 out of 4012 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 511 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 71478 literals 38%
c [treelook-2] scheduling used 505389 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 311004 steps
c [treelook-2] 71465 literals remain 38%
c [treelook-2] 62177 variables remain to probed next time 66%
c [treelook-2] removed 5 variables, found 1371 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 142 failed, 11561 tauts, 0 hbrs, 1976 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 93378 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 24899 not tried 27% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 3295 = 4% variables out of 93378 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 628029 negative 99.1% of 633704 except 5675 0.9%
c [phase-count-3] 508842 positive 80.3% of 633704 except 124862 19.7%
c [phase-count-3] less non-negative clauses 5675 than limit 63300 (10.0%)
c [phase-count-3] non-pos/non-neg = 124862/5675 = 22.00 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 4521 negative 100%
c [sort-queue-3] sorted 90083 enqueued variables after 1008 conflicts
c [score-dist-3] active 0 (0%), one 13820 (15%), zero 76263 (85%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 3810 variables 4.1% (90083 remain 31%)
c [simplification-3] removed 21789 irredundant clauses 3.3% (633704 remain 46%)
c [simplification-3] maximum reduction of 4% = max (4%, 3%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 4000
c [simplification-3] penalized conflict interval 4000 = 1 * 4000
c [simplification-3] hard conflict limit 15008 (soft 5008 + delta 10000)
c [simplification-3] new conflict limit 5008 (hard 15008)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   11.7   90082   633704      1062     651     78 18499    3    35   50   9%      1   34   12    0 5751%
c i   12.1   89166   633704      1319     848    112 18522    3    40   50   9%      1   40   11    0 4253%
c i   12.1   89112   633704      1333     859    113 18522    4    41   50   8%      1   41   11    0 4147%
c i   12.1   89110   633704      1337     861    113 18523    4    42   50   8%      1   41   11    0 4122%
c i   12.1   89101   633704      1340     861    114 18524    4    41   50   8%      1   41   11    0 4078%
c i   12.2   89006   633704      1362     878    117 18525    4    42   50   8%      1   41   10    0 3903%
c i   12.2   88928   633704      1382     893    120 18526    4    43   50   8%      1   43   10    0 3908%
c i   12.3   88872   633704      1389     896    120 18529    4    43   50   8%      1   43   10    0 3874%
c i   12.3   88783   633704      1407     908    122 18532    4    44   50   8%      1   43   10    0 3806%
c i   12.4   88673   633704      1476     963    127 18537    4    46   50   8%      1   46   13    0 4391%
c i   12.5   88372   633704      1515     993    130 18540    4    47   50   8%      1   46   13    0 4300%
c i   12.6   88361   633704      1619    1077    142 18543    4    51   50   9%      1   50   16    0 4903%
c i   12.7   88347   633704      1637    1087    145 18547    4    51   50   9%      1   50   15    0 4638%
c i   12.9   88299   633704      1899    1296    171 18568    6    54   50  10%      1   53   19    0 4443%
c i   13.0   88292   633704      1942    1326    173 18577    6    55   50  10%      1   54   17    0 3934%
c i   13.0   88286   633704      1950    1330    175 18578    6    55   50  10%      1   55   16    0 3838%
c i   13.0   88274   633704      1966    1341    178 18579    6    56   50  10%      1   55   15    0 3664%
c i   13.1   88019   633704      1983    1356    178 18580    6    56   50  10%      1   55   15    0 3581%
c i   13.2   87940   633704      2102    1447    191 18593    6    58   50  10%      1   57   13    0 2929%
c 
c [simplification-4] limit of 158 binary hit after 158 binaries
c [decomp-8] removed 2209 variables
c [basicprobe-2] limit 4960648 based on 620081 irredundant clauses
c [basicprobe-2-0] 29016 probes remain 33% after last round
c [basicprobe-2-0] 13 units = 13 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 576 variables, found 15193 hbrs
c [unhide-4] limit 150093 with penalty 0 = 0 + 0
c [unhide-4-4] 2 units, 242 failed, 2777 tauts, 0 hbrs, 2321 literals
c [elim-4] 18703 variables 22% will be scheduled this time
c [elim-4] scheduled 18703 variables 22%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 34540757 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 18703 scheduled
c [phase-count-4] 604127 negative 99.1% of 609802 except 5675 0.9%
c [phase-count-4] 490153 positive 80.4% of 609802 except 119649 19.6%
c [phase-count-4] less non-negative clauses 5675 than limit 60900 (10.0%)
c [phase-count-4] non-pos/non-neg = 119649/5675 = 21.08 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 2164 negative 100%
c [sort-queue-4] sorted 86891 enqueued variables after 2131 conflicts
c [score-dist-4] active 0 (0%), one 23699 (27%), zero 63192 (73%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 1040 variables 1.2% (86891 remain 30%)
c [simplification-4] removed 23902 irredundant clauses 3.8% (609802 remain 44%)
c [simplification-4] maximum reduction of 4% = max (1%, 4%)
c [simplification-4] forced so keeping old conflict interval 4000
c [simplification-4] conflict limit remains at 5015 (hard 15008)
c [simplification-4] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   15.3   86890   609802      2132    1458    191 28970    6    59   49  10%      1   58   12    0 2721%
c i   15.3   86873   609802      2139    1462    191 28972    6    60   49   9%      1   59   12    0 2733%
c i   15.3   86837   609802      2162    1478    194 28975    6    62   49   9%      1   61   13    0 2831%
c i   15.5   86836   609802      2233    1527    204 28984    6    65   49   9%      1   64   12    0 2631%
c i   15.6   86709   609802      2364    1622    224 28997    6    67   49   9%      1   65   10    0 2068%
c i   15.6   86532   609802      2365    1622    224 28997    6    67   49   9%      1   65   10    0 2060%
c i   15.7   86516   609802      2407    1653    228 29002    6    68   49   9%      1   67    9    0 1936%
c i   16.1   86361   609802      2696    1879    259 29027    6    73   49   9%      1   72   12    1 2223%
c i   16.1   86273   609802      2700    1882    259 29027    6    73   49   9%      1   72   12    1 2202%
c i   16.4   86261   609802      2838    1985    275 29045    6    78   49   8%      1   76   10    1 1917%
c i   16.4   86211   609802      2867    2009    276 29048    6    80   49   8%      1   78   12    1 2080%
c i   16.4   86199   609802      2868    2009    276 29048    6    80   49   8%      1   78   12    1 2071%
c i   16.5   86168   609802      2874    2013    277 29048    6    80   49   8%      1   79   11    1 2053%
c i   16.5   86117   609802      2875    2013    277 29048    6    80   49   8%      1   79   11    1 2045%
c i   16.5   86113   609802      2882    2017    278 29049    6    80   49   8%      1   78   11    1 2001%
c i   16.5   86073   609802      2885    2018    278 29050    6    80   49   8%      1   78   11    1 1986%
c i   16.5   86057   609802      2890    2021    279 29050    6    80   49   8%      1   78   11    1 1954%
c i   16.7   86048   609802      2973    2081    285 29063    7    82   49   8%      1   80   12    1 2026%
c i   16.7   85904   609802      2986    2089    286 29066    7    82   49   8%      1   80   11    1 1954%
c i   16.8   85872   609802      3022    2116    289 29071    7    83   49   8%      1   80   11    1 1908%
c i   16.8   85835   609802      3064    2143    292 29080    7    84   49   8%      1   82   10    1 1728%
c i   16.9   85827   609802      3080    2157    292 29080    7    84   49   8%      1   82   10    1 1715%
c i   17.1   85625   609802      3161    2210    304 29095    7    86   49   8%      1   83    9    1 1455%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   17.1   85615   609802      3222    2252    314 29102    7    86   49   8%      1   83    9    1 1475%
c i   17.1   85571   609802      3224    2253    314 29102    7    86   49   8%      1   83    9    1 1466%
c i   17.3   85559   609802      3390    2377    333 29114    7    88   49   8%      1   85   10    1 1562%
c i   17.5   85526   609802      3564    2521    344 29130    7    91   49   8%      1   88   12    1 1808%
c i   17.9   85514   609802      3768    2684    363 29148    8   101   50   7%      1   98   14    1 1985%
c i   17.9   85473   609802      3803    2710    367 29152    8   101   50   8%      1   98   14    1 2007%
c i   17.9   85461   609802      3821    2723    368 29155    8   101   50   8%      1   98   14    1 1931%
c i   18.0   85452   609802      3831    2727    370 29157    8   101   50   8%      1   98   13    1 1876%
c i   18.2   85451   609802      3962    2822    385 29177    8   103   50   7%      1  100   12    1 1566%
c i   18.3   85432   609802      4033    2871    390 29189    8   104   50   7%      1  101   11    1 1535%
c i   18.7   85370   609802      4279    3047    419 29219    8   110   50   7%      1  106   13    1 1631%
c i   19.0   85369   609802      4398    3152    427 29223    8   113   50   7%      1  109   16    1 1968%
c i   19.1   85362   609802      4426    3170    432 29227    8   113   50   7%      1  109   15    1 1850%
c i   19.1   85257   609802      4464    3193    439 29231    8   114   50   7%      1  110   14    1 1690%
c i   19.2   84491   609802      4494    3217    441 29233    8   115   50   7%      1  110   15    1 1831%
c i   19.3   84488   609802      4514    3230    443 29237    9   115   50   7%      1  111   16    1 1870%
c i   19.3   84345   609802      4539    3244    448 29241    9   116   50   7%      1  112   15    1 1779%
c i   19.6   84335   609802      4695    3352    466 29269    8   116   50   7%      1  111   11    1 1252%
c i   19.6   84275   609802      4696    3352    466 29269    8   116   50   7%      1  111   11    1 1247%
c i   19.8   84222   609802      4774    3403    476 29284    8   115   50   7%      1  110    9    1 1034%
c i   19.8   84212   609802      4783    3409    477 29285    8   115   50   7%      1  111    9    1 1016%
c i   19.9   84207   609802      4821    3426    482 29300    8   115   50   7%      1  110    8    1  913%
c i   20.1   84206   609802      4919    3499    496 29310    8   116   50   7%      1  111    7    1  808%
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   20.2   84142   609802      4995    3554    500 29323    8   116   50   7%      1  111    7    1  795%
c 
c [simplification-5] limit 5072 conflicts (hard 15008) hit after 5072 conflicts
c [quatres-1] found 28194 quaternary clauses 35% in total
c [quatres-1-2] added 2 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 84123 free variables schedulable
c [ternres-1] 66 ternary resolvents (0 bin, 66 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 595 xors of average arity 2.2
c [gauss-1] connected 1297 occurrences of 745 variables (average 1.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 466 variables
c [unhide-5] limit 411336 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 187 failed, 10118 tauts, 0 hbrs, 4933 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 141 transitive binary clauses
c [transred-1] found 4 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 83374 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 9654 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 4 clauses out of 57 (7%) of length 10
c [cce-1-1] eliminated 834 clauses out of 2148 (39%) of length 9
c [cce-1-1] eliminated 334 clauses out of 845 (40%) of length 8
c [cce-1-1] eliminated 1 clauses out of 3018 (0%) of length 7
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1173 large clauses in 30000006 steps
c [cce-1-1] allowing another 15000003 steps for small clauses
c [cce-1-1] scheduling 393312 clauses = 271366 binary + 121946 ternary
c [cce-1-1] tried to eliminate 223 small clauses 0%
c [cce-1-1] eliminated 38 binary clauses 0%
c [cce-1-1] eliminated 11 ternary clauses 0%
c [cce-1-1] eliminated 49 small clauses 0%
c [cce-1-1] eliminated 49 small clauses in 30000016 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1222 covered clauses in round 1
c [cce-1] eliminated 1222 covered clauses in TOTAL during 1 rounds
c [cce-1] 1222 < 1/100 * 571345 = 5713 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1140746 added (scaled 2)
c [bca-1] 145590 out of 166750 literals actually usable 87%
c [bca-1] added 206 blocked clauses in 403262 steps
c [sweep-1] limit 1140246 based on 570123 irredundant clauses
c [sweep-1-1] 5752 pos 6.9% + 77622 neg 93.1% = 83374 sched 100.0% ret 0
c [sweep-1-1] 1141531 steps 16 queries 27429.50 avg class size
c [sweep-1-1] 100 decisions 8 SAT calls 161.75 avg env size
c [sweep-1-1] 83339 variables remain 100% (22 retained 0%)
c [decomp-10] removed 21 variables
c [sweep-1-1] removed 21 vars (0 failed, 7 eqs, 14 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 21 vars in TOTAL (1 rounds, 15 queries)
c [phase-count-5] 564400 negative 99.0% of 570055 except 5655 1.0%
c [phase-count-5] 467386 positive 82.0% of 570055 except 102669 18.0%
c [phase-count-5] less non-negative clauses 5655 than limit 57000 (10.0%)
c [phase-count-5] non-pos/non-neg = 102669/5655 = 18.16 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 214 negative 100%
c [sort-queue-5] sorted 83353 enqueued variables after 5072 conflicts
c [score-dist-5] active 0 (0%), one 42312 (51%), zero 41041 (49%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 770 variables 0.9% (83353 remain 29%)
c [simplification-5] removed 39747 irredundant clauses 6.5% (570055 remain 41%)
c [simplification-5] maximum reduction of 7% = max (1%, 7%)
c [simplification-5] large reduction 7% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 17072 (soft 7072 + delta 10000)
c [simplification-5] new conflict limit 7072 (hard 17072)
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   24.0   83352   570055      5120    3603    585 40710    8   119   49   7%      1  114    8    1  867%
c i   24.2   83350   570055      5185    3651    589 40719    8   121   49   7%      1  116    9    1  961%
c i   24.3   83330   570055      5207    3665    593 40722    8   121   49   7%      1  116    9    1  972%
c i   24.4   83256   570055      5224    3676    594 40725    8   121   49   7%      1  116    9    1  977%
c i   24.4   83182   570055      5245    3694    595 40726    8   122   49   7%      1  117   10    1 1064%
c i   24.6   83168   570055      5372    3794    604 40737    9   126   49   7%      1  121   21    1 2082%
c i   24.6   83159   570055      5398    3810    606 40744    9   127   49   7%      1  122   20    1 2029%
c i   24.7   83148   570055      5405    3814    607 40744    9   127   49   7%      1  122   20    1 1987%
c i   25.2   83139   570055      5754    4089    643 40777   10   132   49   8%      1  126   17    1 1528%
c i   25.2   83066   570055      5755    4089    643 40777   10   132   49   8%      1  126   17    1 1522%
c i   25.2   83062   570055      5756    4089    643 40777   10   132   49   8%      1  126   16    1 1516%
c i   25.4   83058   570055      5840    4154    648 40788   10   134   49   7%      1  127   15    1 1333%
c i   25.4   83057   570054      5901    4203    656 40790   10   133   49   7%      1  126   13    1 1183%
c i   25.5   83053   570054      5927    4227    656 40790   10   133   49   8%      1  127   16    1 1418%
c i   26.2   83037   570054      6500    4664    712 40859   10   136   49   8%      3  128   13    1 1081%
c i   26.2   82873   570054      6559    4711    718 40863   10   135   49   8%      3  127   14    1 1104%
c i   26.8   82866   570054      6879    4972    745 40885   11   140   49   8%      3  131   19    1 1455%
c i   26.9   82855   570054      6912    4996    747 40888   11   140   49   8%      2  131   18    1 1337%
c i   26.9   82646   570054      6929    5009    747 40890   11   140   49   8%      2  131   17    1 1290%
c 
c [simplification-6] limit 7093 conflicts (hard 17072) hit after 7093 conflicts
c [quatres-2] found 32059 quaternary clauses 39% in total
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 82637 free variables schedulable
c [ternres-2] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-2] 54485 variables remain 66% (28152 retained 34%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2048 at-most-one constraints of average size 4.4
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2048 out of 2048 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 898 variables
c [simpleprobe-3] 6799 schedulable variables 8%
c [simpleprobe-3] limit 5775363 penalty 1 = 1 + 0
c [decomp-12] removed 35 variables
c [simpleprobe-3] 9434 variables remain 11% (72986 retained 89%)
c [simpleprobe-3] removed 35 variables, found 10108 hbrs, 11 units
c [unhide-6] limit 577536 with penalty 0 = 0 + 0
c [unhide-6-6] 3 units, 238 failed, 5766 tauts, 0 hbrs, 5434 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 184 transitive binary clauses
c [transred-2] found 8 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 81930 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 954 blocked clauses
c [block-2] 954 < 1/100 * 565542 = 5655 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 81930 variables 100%
c [elim-5] limit of 28876818 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 11276 not tried 14% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 3917 = 5% variables out of 81930 scheduled
c [bca-2] limit of 10000000 steps and 1101277 added (scaled 2)
c [bca-2] 138479 out of 156028 literals actually usable 89%
c [bca-2] added 154 blocked clauses in 388952 steps
c [sweep-2] limit 1100674 based on 550337 irredundant clauses
c [sweep-2-1] 5330 pos 6.8% + 72669 neg 93.2% = 77999 sched 100.0% ret 14
c [sweep-2-1] 1277910 steps 14 queries 15567.86 avg class size
c [sweep-2-1] 86 decisions 11 SAT calls 76.09 avg env size
c [sweep-2-1] 77927 variables remain 100% (68 retained 0%)
c [decomp-13] removed 21 variables
c [sweep-2-1] removed 21 vars (0 failed, 3 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 21 vars in TOTAL (1 rounds, 13 queries)
c [phase-count-6] 544936 negative 99.1% of 550156 except 5220 0.9%
c [phase-count-6] 449131 positive 81.6% of 550156 except 101025 18.4%
c [phase-count-6] less non-negative clauses 5220 than limit 55000 (10.0%)
c [phase-count-6] non-pos/non-neg = 101025/5220 = 19.35 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 175 negative 100%
c [sort-queue-6] sorted 77992 enqueued variables after 7093 conflicts
c [score-dist-6] active 0 (0%), one 42012 (54%), zero 35980 (46%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 4645 variables 5.6% (77992 remain 27%)
c [simplification-6] removed 19898 irredundant clauses 3.5% (550156 remain 40%)
c [simplification-6] maximum reduction of 6% = max (6%, 3%)
c [simplification-6] large reduction 6% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 19093 (soft 9093 + delta 10000)
c [simplification-6] new conflict limit 9093 (hard 19093)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   31.2   77991   550156      7262    3761    716 43788   11   141   48   8%      2  132   11    1  836%
c i   31.2   77984   550156      7292    3787    718 43789   11   141   48   8%      2  132   11    1  786%
c i   31.4   77974   550156      7421    3891    730 43798   11   144   48   8%      2  134   12    1  848%
c i   31.4   77967   550156      7430    3896    732 43799   11   143   48   8%      2  134   12    1  830%
c i   31.4   77960   550156      7431    3896    732 43799   11   143   48   8%      2  134   12    1  826%
c i   31.4   77957   550156      7432    3896    732 43799   11   143   48   8%      2  134   12    1  823%
c i   31.4   77956   550156      7433    3896    732 43799   11   143   48   8%      2  134   11    1  820%
c i   31.9   77955   550156      7818    4231    758 43818   12   146   48   8%      2  136   16    1 1101%
c i   31.9   77885   550156      7827    4237    758 43820   12   147   48   8%      2  136   16    1 1096%
c i   32.3   77884   550156      8144    4503    775 43842   12   150   48   8%      2  139   20    2 1260%
c i   32.5   77788   550156      8299    4624    791 43856   12   150   48   8%      2  138   15    2  956%
c i   32.6   77720   550156      8369    4675    801 43864   12   149   48   8%      2  138   14    2  871%
c i   32.9   77107   550156      8659    4937    814 43872   14   158   48   9%      2  145   27    2 1533%
c i   33.3   77100   550156      8874    5110    829 43891   14   162   48   8%      2  150   21    2 1156%
c i   33.3   77093   550156      8900    5133    831 43891   14   165   48   8%      2  152   20    2 1110%
c i   33.5   77077   550156      9015    5211    848 43910   14   165   48   8%      2  152   18    2  975%
c i   33.6   77072   550156      9055    5240    856 43912   14   166   48   8%      2  153   17    2  907%
c 
c [simplification-7] limit 9125 conflicts (hard 19093) hit after 9125 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 50704 schedulable variables 65%
c [ternres-3] 22 ternary resolvents (0 bin, 22 trn)
c [ternres-3] 23953 variables remain 31% (53073 retained 69%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 20 xors of average arity 2.9
c [gauss-2] connected 58 occurrences of 49 variables (average 1.2)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 7 variables
c [treelook-3] limit 360560 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 55190 literals 36%
c [treelook-3] scheduling used 427098 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 360560 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 380025 steps
c [treelook-3] 55177 literals remain 36%
c [treelook-3] 48182 variables remain to probed next time 63%
c [treelook-3] removed 6 variables, found 2454 hbrs
c [unhide-7] limit 721121 with penalty 0 = 0 + 0
c [unhide-7-7] 3 units, 95 failed, 9560 tauts, 0 hbrs, 5704 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 196 transitive binary clauses
c [transred-3] found 6 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 1062 (0%) of length 9
c [cce-2-1] eliminated 2 clauses out of 435 (0%) of length 8
c [cce-2-1] eliminated 1 clauses out of 2186 (0%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 5 large clauses in 15000008 steps
c [cce-2-1] allowing another 7500004 steps for small clauses
c [cce-2-1] scheduling 369433 clauses = 249379 binary + 120054 ternary
c [cce-2-1] tried to eliminate 188 small clauses 0%
c [cce-2-1] eliminated 42 binary clauses 0%
c [cce-2-1] eliminated 17 ternary clauses 0%
c [cce-2-1] eliminated 59 small clauses 0%
c [cce-2-1] eliminated 2377 small clauses in 15000002 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 2382 covered clauses in round 1
c [cce-2] eliminated 2382 covered clauses in TOTAL during 1 rounds
c [cce-2] 2382 < 1/100 * 538274 = 5382 considered unsuccessful
c [elim-6] 11258 variables 15% will be scheduled this time
c [elim-6] scheduled 11258 variables 15%
c [elim-6] limit of 72112181 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 22820748 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 11258 scheduled
c [bca-3] limit of 10000000 steps and 1072034 added (scaled 2)
c [bca-3] 132581 out of 153516 literals actually usable 86%
c [bca-3] added 51 blocked clauses in 365478 steps
c [sweep-3] limit 1081682 penalty 0 = 0 + 0
c [sweep-3-1] 5039 pos 6.6% + 71658 neg 93.4% = 76697 sched 99.9% ret 60
c [sweep-3-1] 1378751 steps 20 queries 20326.55 avg class size
c [sweep-3-1] 192 decisions 13 SAT calls 64.85 avg env size
c [sweep-3-1] 76364 variables remain 100% (152 retained 0%)
c [decomp-16] removed 261 variables
c [sweep-3-1] removed 261 vars (0 failed, 6 eqs, 12 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 261 vars in TOTAL (1 rounds, 19 queries)
c [phase-count-7] 528420 negative 99.0% of 533640 except 5220 1.0%
c [phase-count-7] 436518 positive 81.8% of 533640 except 97122 18.2%
c [phase-count-7] less non-negative clauses 5220 than limit 53300 (10.0%)
c [phase-count-7] non-pos/non-neg = 97122/5220 = 18.61 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 142 negative 100%
c [sort-queue-7] sorted 76496 enqueued variables after 9125 conflicts
c [score-dist-7] active 0 (0%), one 42545 (56%), zero 33951 (44%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 530 variables 0.7% (76496 remain 27%)
c [simplification-7] removed 16516 irredundant clauses 3.0% (533640 remain 39%)
c [simplification-7] maximum reduction of 3% = max (1%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 9000
c [simplification-7] penalized conflict interval 9000 = 1 * 9000
c [simplification-7] hard conflict limit 28125 (soft 18125 + delta 10000)
c [simplification-7] new conflict limit 18125 (hard 28125)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   37.2   76495   533640      9146    5289    895 44550   14   170   48   8%      2  156   15    2  799%
c i   38.0   76489   533640      9897    5918    947 44599   15   168   48   9%      4  153   24    2 1164%
c i   38.9   76456   533640     10612    6540    981 44650   16   176   48   9%      5  159   21    2  925%
c i   38.9   76295   533640     10618    6544    982 44650   16   176   48   9%      5  159   21    2  908%
c i   39.0   76286   533640     10654    6568    989 44654   16   175   48   9%      5  159   19    2  826%
c i   39.3   76278   533640     10810    6703    997 44664   16   181   48   9%      4  164   19    2  822%
c i   39.9   76271   533640     11192    7044   1018 44680   17   190   48   9%      4  171   22    2  903%
c i   40.0   76264   533640     11270    7108   1024 44684   17   191   49   9%      4  172   25    2 1024%
c i   40.1   76260   533640     11342    7164   1032 44687   17   192   49   9%      3  173   22    2  900%
c i   40.2   75976   533640     11369    7188   1032 44688   17   193   49   9%      3  174   23    3  933%
c i   40.2   75975   533640     11431    7235   1038 44694   17   191   49   9%      3  173   25    3  972%
c i   40.6   75973   533640     11643    7426   1044 44701   18   196   49   9%      3  177   28    3 1057%
c i   41.5   75961   533640     12167    7866   1079 44737   19   217   49   9%      3  196   27    3  973%
c i   42.0   75960   533640     12584    8235   1093 44749   21   218   49  10%      3  196   35    3 1160%
c i   42.1   75949   533640     12613    8258   1098 44749   21   219   49  10%      3  197   35    3 1142%
c i   42.1   75933   533640     12631    8273   1099 44750   21   220   49  10%      3  198   34    3 1116%
c i   43.3   75932   533640     13407    8921   1147 44807   22   228   49  10%      5  204   23    3  686%
c i   43.5   75919   533640     13568    9056   1157 44818   22   227   49  10%      4  202   21    3  637%
c i   43.7   75638   533640     13627    9106   1161 44822   22   231   49   9%      4  205   22    3  634%
c i   44.0   75627   533640     13802    9241   1175 44843   22   233   50   9%      4  207   17    3  508%
c i   44.5   75570   533640     14168    9546   1194 44872   23   235   50  10%      3  208   29    4  807%
c i   44.6   75569   533640     14187    9560   1194 44875   23   235   50  10%      3  208   28    4  768%
c i   44.8   75530   533640     14272    9624   1200 44889   23   235   50  10%      3  208   24    4  650%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   45.0   75291   533640     14397    9729   1209 44896   23   237   51  10%      3  209   27    4  732%
c i   45.1   75281   533640     14438    9764   1211 44897   23   239   51  10%      3  211   28    4  752%
c i   45.2   75270   533640     14474    9792   1214 44900   23   238   51  10%      2  210   26    4  704%
c i   45.8   75269   533640     14898   10162   1237 44923   24   239   52  10%      3  210   32    4  824%
c i   46.3   74972   533640     15240   10459   1253 44944   25   247   52  10%      3  217   37    4  912%
c i   46.7   74866   533640     15464   10640   1276 44961   25   250   52  10%      2  219   27    4  662%
c i   46.7   74840   533640     15488   10653   1277 44968   24   250   52  10%      2  218   25    4  613%
c i   46.8   74581   533640     15507   10667   1279 44970   24   249   52  10%      2  218   24    4  596%
c i   47.2   74565   533640     15807   10927   1287 44989   25   247   52  10%      2  214   31    4  739%
c i   48.1   74548   533640     16287   11337   1312 45015   26   259   52  10%      3  225   36    4  812%
c i   48.2   74539   533640     16289   11338   1312 45015   26   259   52  10%      3  225   36    4  814%
c i   48.3   74538   533640     16340   11383   1315 45016   26   261   52  10%      2  227   34    4  771%
c i   49.0   74535   533640     16757   11747   1335 45041   27   272   53  10%      3  236   40    5  843%
c i   49.0   74530   533640     16785   11773   1335 45042   27   272   53  10%      3  236   39    5  821%
c i   50.1   74529   533640     17360   12273   1370 45070   29   282   53  10%      3  244   44    5  873%
c i   50.3   74528   533640     17480   12381   1371 45073   30   281   53  11%      3  243   46    5  907%
c i   51.1   74519   533640     17870   12727   1389 45092   31   295   54  11%      3  255   46    5  859%
c 
c [simplification-8] limit 18131 conflicts (hard 28125) hit after 18132 conflicts
c [quatres-3] found 28538 quaternary clauses 39% in total
c [quatres-3-2] added 2 single-self-subsuming ternary resolvents
c [ternres-4] limit 7193466 with penalty 0 = 0 + 0
c [ternres-4] 23140 schedulable variables 30%
c [ternres-4] 39 ternary resolvents (0 bin, 39 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 3027 variables
c [basicprobe-3] limit 35967334 penalty 0 = 0 + 0
c [basicprobe-3-0] 21017 probes remain 29% after last round
c [basicprobe-3-0] 175 units = 175 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 554 variables, found 109842 hbrs
c [bate-1] eliminated 50 asymmetric tautologies during probing
c [unhide-8] limit 1438693 with penalty 0 = 0 + 0
c [unhide-8-8] 3 units, 579 failed, 15238 tauts, 0 hbrs, 39451 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 135 transitive binary clauses
c [transred-4] found 5 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 72178 variables 100%
c [block-3] limit of 35967334 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 170 blocked clauses
c [block-3] 170 < 1/100 * 513320 = 5133 considered unsuccessful
c [bca-4] limit of 10000000 steps and 1014657 added (scaled 2)
c [bca-4] 115235 out of 144356 literals actually usable 80%
c [bca-4] added 164 blocked clauses in 308027 steps
c [sweep-4] limit 2158040 penalty 0 = 0 + 0
c [sweep-4-1] 4741 pos 6.6% + 67318 neg 93.4% = 72059 sched 99.8% ret 118
c [sweep-4-1] 2380532 steps 18 queries 16308.89 avg class size
c [sweep-4-1] 108 decisions 15 SAT calls 172.20 avg env size
c [sweep-4-1] 71981 variables remain 100% (176 retained 0%)
c [decomp-18] removed 71 variables
c [sweep-4-1] removed 71 vars (0 failed, 5 eqs, 5 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 71 vars in TOTAL (1 rounds, 17 queries)
c [phase-count-8] 501470 negative 99.0% of 506690 except 5220 1.0%
c [phase-count-8] 414853 positive 81.9% of 506690 except 91837 18.1%
c [phase-count-8] less non-negative clauses 5220 than limit 50600 (10.0%)
c [phase-count-8] non-pos/non-neg = 91837/5220 = 17.59 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 81 negative 100%
c [sort-queue-8] sorted 72106 enqueued variables after 18132 conflicts
c [score-dist-8] active 0 (0%), one 44081 (61%), zero 28025 (39%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 2361 variables 3.2% (72106 remain 25%)
c [simplification-8] removed 26950 irredundant clauses 5.1% (506690 remain 37%)
c [simplification-8] maximum reduction of 5% = max (3%, 5%)
c [simplification-8] large reduction 5% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 30132 (soft 20132 + delta 10000)
c [simplification-8] new conflict limit 20132 (hard 30132)
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   56.4   72105   506690     18327   12940   1360 136851   32   300   57  11%      3  258   39    6  694%
c i   56.7   72102   506690     18538   13119   1370 136866   32   297   57  11%      3  255   35    6  622%
c i   57.0   72099   506690     18858   13401   1386 136882   32   287   57  11%      2  244   30    6  524%
c i   57.0   72053   506690     18859   13401   1386 136882   32   287   57  11%      2  243   30    6  522%
c i   57.2   71991   506690     19026   13556   1388 136886   32   280   57  11%      2  236   33    6  570%
c i   57.6   71990   506690     19328   13818   1407 136902   31   279   57  11%      2  234   26    6  443%
c i   57.6   71886   506690     19336   13822   1409 136903   31   279   57  11%      2  234   26    6  437%
c i   57.7   71864   506690     19377   13847   1417 136910   31   277   57  11%      2  232   23    6  388%
c i   57.9   71644   506690     19497   13951   1425 136916   31   275   57  11%      2  229   22    6  364%
c i   58.5   71632   506690     19859   14283   1432 136931   32   282   57  11%      2  235   43    6  693%
c 
c [simplification-9] limit 20143 conflicts (hard 30132) hit after 20143 conflicts
c [quatres-4] found 28931 quaternary clauses 40% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 1 quaternary resolvents
c [ternres-5] limit 7898313 with penalty 0 = 0 + 0
c [ternres-5] all 71632 free variables schedulable
c [ternres-5] 16 ternary resolvents (0 bin, 16 trn)
c [ternres-5] 23381 variables remain 33% (48251 retained 67%)
c [decomp-19] removed 514 variables
c [simpleprobe-4] 9095 schedulable variables 13%
c [simpleprobe-4] limit 31593255 penalty 0 = 0 + 0
c [decomp-20] removed 879 variables
c [simpleprobe-4] 865 variables remain 1% (69848 retained 99%)
c [simpleprobe-4] removed 879 variables, found 39820 hbrs, 261 units
c [unhide-9] limit 1579662 with penalty 0 = 0 + 0
c [unhide-9-9] 3 units, 138 failed, 10073 tauts, 0 hbrs, 14672 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 258 transitive binary clauses
c [transred-5] found 5 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 70315 variables 100%
c [elim-7] limit of 78983138 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 2455 variables 3% in round 1 in 49394474 steps
c [elim-7-1] backward subsumption/strengthening limit 29588664
c [elim-7-1-1] backward checking 9398 touched variables 13%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 1 and strengthened 35 clauses in 2986063 steps
c [elim-7-1] rescheduled 98 variables 0% by backward subsumption
c [elim-7-2] eliminated 9 variables 0% in round 2 in 141501 steps
c [elim-7-2] backward subsumption/strengthening limit 141500
c [elim-7-2-1] backward checking 85 touched variables 0%
c [elim-7-2-1] incomplete backward checking 0 remain 0%
c [elim-7-2] subsumed 1 and strengthened 2 clauses in 141501 steps
c [elim-7-2] rescheduled 10 variables 0% by backward subsumption
c [elim-7-3] eliminated 1 variables 0% in round 3 in 12928 steps
c [elim-7-3] backward subsumption/strengthening limit 12900
c [elim-7-3-1] backward checking 10 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 0 and strengthened 2 clauses in 12901 steps
c [elim-7] incomplete 8 not tried 0% in round 3
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 2469 = 4% variables out of 70315 scheduled
c [bca-5] limit of 10000000 steps and 963967 added (scaled 2)
c [bca-5] 110919 out of 135694 literals actually usable 82%
c [bca-5] added 74 blocked clauses in 300479 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 23694940 penalty 0 = 0 + 0
c [sweep-5-1] 4714 pos 7.0% + 62991 neg 93.0% = 67705 sched 99.8% ret 141
c [sweep-5-1] 23730287 steps 200 queries 2497.74 avg class size
c [sweep-5-1] 2253 decisions 175 SAT calls 119.38 avg env size
c [sweep-5-1] 54539 variables remain 81% (13208 retained 19%)
c [decomp-21] removed 150 variables
c [sweep-5-1] removed 150 vars (0 failed, 28 eqs, 53 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 150 vars in TOTAL (1 rounds, 199 queries)
c [phase-count-9] 476188 negative 99.1% of 480437 except 4249 0.9%
c [phase-count-9] 391626 positive 81.5% of 480437 except 88811 18.5%
c [phase-count-9] less non-negative clauses 4249 than limit 48000 (10.0%)
c [phase-count-9] non-pos/non-neg = 88811/4249 = 20.90 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 76 negative 100%
c [sort-queue-9] sorted 67696 enqueued variables after 20143 conflicts
c [score-dist-9] active 0 (0%), one 42441 (63%), zero 25255 (37%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 3936 variables 5.5% (67696 remain 24%)
c [simplification-9] removed 26253 irredundant clauses 5.2% (480437 remain 35%)
c [simplification-9] maximum reduction of 5% = max (5%, 5%)
c [simplification-9] large reduction 5% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 32143 (soft 22143 + delta 10000)
c [simplification-9] new conflict limit 22143 (hard 32143)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   66.4   67695   480437     21151   10880   1427 182301   31   288   52  11%      9  237   33    7  498%
c i   66.9   67684   480437     21520   11219   1438 182313   31   280   52  11%      7  227   30    7  440%
c i   67.3   67678   480437     21837   11500   1451 182330   31   283   52  11%      5  229   27    7  394%
c i   67.5   67677   480437     21929   11578   1457 182336   30   282   52  11%      5  228   27    7  390%
c 
c [simplification-10] limit 22143 conflicts (hard 32143) hit after 22145 conflicts
c [quatres-5] found 30671 quaternary clauses 42% in total
c [quatres-5-2] added 1 quaternary resolvents
c [ternres-6] limit 8715034 with penalty 0 = 0 + 0
c [ternres-6] 22046 schedulable variables 33%
c [ternres-6] 63 ternary resolvents (0 bin, 63 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 544689 penalty 3 = 3 + 0
c [card-4] found 1392 at-most-one constraints of average size 4.2
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 544689 for elimination
c [card-4] 1392 out of 1392 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 10 xors of average arity 2.9
c [gauss-3] connected 29 occurrences of 29 variables (average 1.0)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 3 variables
c [treelook-4] limit 871503 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 90128 literals 67%
c [treelook-4] scheduling used 872016 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 871503 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 906016 steps
c [treelook-4] 90104 literals remain 67%
c [treelook-4] 41316 variables remain to probed next time 61%
c [treelook-4] removed 8 variables, found 4147 hbrs
c [unhide-10] limit 1743006 with penalty 0 = 0 + 0
c [unhide-10-10] 8 units, 247 failed, 15345 tauts, 0 hbrs, 21564 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 213 transitive binary clauses
c [transred-6] found 5 units
c [cce-3] limit of 10893792 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 10 clauses out of 869 (1%) of length 9
c [cce-3-1] eliminated 7 clauses out of 417 (2%) of length 8
c [cce-3-1] eliminated 4 clauses out of 1679 (0%) of length 7
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 21 large clauses in 10893792 steps
c [cce-3-1] allowing another 5446896 steps for small clauses
c [cce-3-1] scheduling 333499 clauses = 228642 binary + 104857 ternary
c [cce-3-1] tried to eliminate 125 small clauses 0%
c [cce-3-1] eliminated 21 binary clauses 0%
c [cce-3-1] eliminated 3 ternary clauses 0%
c [cce-3-1] eliminated 24 small clauses 0%
c [cce-3-1] eliminated 3337 small clauses in 10893810 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 3358 covered clauses in round 1
c [cce-3] eliminated 3358 covered clauses in TOTAL during 1 rounds
c [cce-3] 3358 < 1/100 * 479686 = 4796 considered unsuccessful
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 67261 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 3486013700 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 237 variables 0% in round 1 in 47159366 steps
c [elim-8-1] backward subsumption/strengthening limit 47159300
c [elim-8-1-1] backward checking 1128 touched variables 2%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 26 and strengthened 22 clauses in 872114 steps
c [elim-8-1] rescheduled 45 variables 0% by backward subsumption
c [elim-8-2] eliminated 6 variables 0% in round 2 in 3376240 steps
c [elim-8-2] backward subsumption/strengthening limit 3376200
c [elim-8-2-1] backward checking 50 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 92749 steps
c [elim-8] fully completed in 2 rounds
c [gc-67] reconnected 167285 binary clauses (produced 0 empty 1 units)
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 250 = 0% variables out of 67261 scheduled
c [elim-8] 250 < 1/100 * 67261 = 672 considered unsuccessful
c [bca-6] limit of 10000000 steps and 951778 added (scaled 2)
c [bca-6] 107369 out of 134024 literals actually usable 80%
c [bca-6] added 114 blocked clauses in 286794 steps
c [sweep-6] limit 2614510 penalty 0 = 0 + 0
c [sweep-6-1] 4365 pos 8.0% + 49880 neg 92.0% = 54245 sched 80.9% ret 12766
c [sweep-6-1] 2633642 steps 28 queries 9182.43 avg class size
c [sweep-6-1] 222 decisions 20 SAT calls 185.05 avg env size
c [sweep-6-1] 54117 variables remain 81% (12894 retained 19%)
c [decomp-24] removed 11 variables
c [sweep-6-1] removed 11 vars (0 failed, 8 eqs, 14 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 11 vars in TOTAL (1 rounds, 27 queries)
c [phase-count-10] 471274 negative 99.1% of 475463 except 4189 0.9%
c [phase-count-10] 386938 positive 81.4% of 475463 except 88525 18.6%
c [phase-count-10] less non-negative clauses 4189 than limit 47500 (10.0%)
c [phase-count-10] non-pos/non-neg = 88525/4189 = 21.13 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 69 negative 100%
c [sort-queue-10] sorted 67000 enqueued variables after 22145 conflicts
c [score-dist-10] active 0 (0%), one 42507 (63%), zero 24493 (37%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 645 variables 1.0% (67000 remain 23%)
c [simplification-10] removed 4974 irredundant clauses 1.0% (475463 remain 34%)
c [simplification-10] maximum reduction of 1% = max (1%, 1%)
c [simplification-10] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-10] new conflict interval 19000
c [simplification-10] penalized conflict interval 19000 = 1 * 19000
c [simplification-10] hard conflict limit 51145 (soft 41145 + delta 10000)
c [simplification-10] new conflict limit 41145 (hard 51145)
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   74.3   66999   475463     23480   12201   1530 169335   31   295   52  11%     12  235   27    7  362%
c i   74.9   66998   475463     23954   12640   1548 169340   32   290   52  11%      9  228   38    8  493%
c i   74.9   66997   475463     24014   12696   1548 169342   32   289   52  11%      8  228   36    8  463%
c i   75.5   66984   475463     24301   12945   1564 169358   32   291   52  11%      6  229   39    8  503%
c i   75.9   66983   475463     24537   13157   1574 169367   32   293   52  11%      5  229   29    8  370%
c i   77.6   66878   475463     25690   14192   1621 169415   32   292   52  11%      8  225   33    8  399%
c i   77.6   66874   475463     25695   14196   1621 169415   32   292   52  11%      8  224   33    8  397%
c i   79.1   66873   475463     26603   15002   1664 169449   32   294   53  11%      7  224   35    9  408%
c i   81.4   66870   475463     28186   16415   1725 169510   33   285   56  12%     13  209   44    9  475%
c i   82.3   66855   475463     28724   16894   1744 169529   36   300   56  12%      9  223   53   10  554%
c i   82.6   66854   475463     28894   17052   1749 169533   36   305   56  12%      7  227   48   10  488%
c i   83.1   66853   475463     29223   17364   1757 169536   37   312   56  12%      6  233   43   10  434%
c i   83.9   66849   475463     29644   17742   1773 169551   38   322   56  12%      4  241   48   10  478%
c i   84.9   66840   475463     30241   18284   1797 169568   37   321   57  11%      4  239   30   10  289%
c i   85.1   66833   475463     30344   18373   1804 169573   36   323   57  11%      3  240   32   10  309%
c i   85.5   66829   475463     30712   18709   1818 169584   36   310   57  12%      3  226   32   10  305%
c i   86.0   66824   475463     31083   19043   1833 169596   35   306   57  12%      2  220   26   11  251%
c i   86.5   66811   475463     31365   19297   1837 169610   35   307   57  11%      2  220   31   11  291%
c i   86.5   66805   475463     31367   19298   1837 169610   35   307   57  11%      2  220   31   11  288%
c i   87.2   66799   475463     31729   19626   1847 169624   36   313   57  12%      2  225   41   11  380%
c i   87.8   66557   475463     32060   19913   1864 169644   36   310   57  12%      2  221   37   11  336%
c i   88.9   66556   475463     32812   20601   1893 169662   36   307   60  12%      3  216   43   11  383%
c i   89.1   66555   475463     32946   20726   1898 169665   36   308   60  12%      3  216   35   11  307%
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   90.0   66554   475463     33399   21142   1909 169686   37   318   61  12%      2  225   47   12  412%
c i   90.0   66545   475463     33400   21142   1909 169686   37   318   61  12%      2  224   47   12  410%
c i   90.8   66544   475463     33758   21455   1919 169707   38   329   61  12%      2  234   46   12  394%
c i   92.6   66543   475463     34909   22479   1974 169753   38   323   62  12%      7  224   42   12  342%
c i   94.2   66542   475463     35778   23280   2004 169778   39   333   63  12%      6  231   43   13  342%
c i   95.1   66541   475463     36387   23821   2022 169809   37   327   63  11%      5  223   23   13  185%
c i   95.3   66536   475463     36500   23926   2025 169813   37   329   63  11%      4  224   29   13  230%
c i   95.6   66535   475463     36631   24036   2034 169820   36   328   63  11%      4  223   26   13  205%
c i   95.7   66530   475463     36713   24105   2039 169824   36   326   63  11%      3  220   26   13  202%
c i   96.5   66529   475463     37229   24547   2059 169842   38   319   64  12%      3  212   48   13  367%
c i   97.1   66528   475463     37664   24932   2073 169859   37   312   64  12%      2  204   39   13  293%
c i   98.1   66527   475463     38215   25419   2096 169879   38   315   65  12%      3  205   48   13  353%
c i   98.6   66526   475463     38525   25679   2111 169894   38   315   67  12%      2  204   37   14  273%
c i   98.8   66522   475463     38618   25762   2113 169898   38   314   67  12%      2  203   43   14  313%
c i   99.8   66521   475463     39315   26399   2139 169925   38   302   67  12%      3  188   35   14  256%
c i  100.3   66508   475463     39562   26627   2145 169935   37   299   67  12%      2  185   31   14  224%
c 
c [simplification-11] limit 41162 conflicts (hard 51145) hit after 41162 conflicts
c [quatres-6] found 29839 quaternary clauses 42% in total
c [quatres-6-2] added 2 single-self-subsuming ternary resolvents
c [ternres-7] limit 15976704 with penalty 0 = 0 + 0
c [ternres-7] all 66508 free variables schedulable
c [ternres-7] 166 ternary resolvents (3 bin, 163 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-25] removed 512 variables
c [basicprobe-4] limit 79883524 penalty 0 = 0 + 0
c [basicprobe-4-0] 17330 probes remain 26% after last round
c [basicprobe-4-0] 417 units = 416 failed (100%) + 1 lifted (0%)
c [basicprobe-4-0] removed 945 variables, found 196388 hbrs
c [bate-2] eliminated 170 asymmetric tautologies during probing
c [unhide-11] limit 1597670 with penalty 1 = 0 + 1
c [unhide-11-11] 7 units, 115 failed, 8347 tauts, 0 hbrs, 169541 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 180 transitive binary clauses
c [transred-7] found 10 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 65310 variables 100%
c [block-4] limit of 39941762 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 325 blocked clauses
c [block-4] 325 < 1/100 * 461225 = 4612 considered unsuccessful
c [bca-7] limit of 10000000 steps and 918295 added (scaled 2)
c [bca-7] 94996 out of 130618 literals actually usable 73%
c [bca-7] added 27 blocked clauses in 263280 steps
c [sweep-7] limit 4793011 penalty 0 = 0 + 0
c [sweep-7-1] 4243 pos 8.0% + 48755 neg 92.0% = 52998 sched 81.2% ret 12310
c [sweep-7-1] 4841782 steps 38 queries 7658.26 avg class size
c [sweep-7-1] 861 decisions 31 SAT calls 243.48 avg env size
c [sweep-7-1] 52606 variables remain 81% (12683 retained 19%)
c [decomp-26] removed 39 variables
c [sweep-7-1] removed 39 vars (0 failed, 6 eqs, 14 impls)
c [sweep-7] 39 < 1/1000 * 65308 = 65 considered unsuccessful
c [sweep-7] removed 39 vars in TOTAL (1 rounds, 37 queries)
c [phase-count-11] 454275 negative 99.1% of 458464 except 4189 0.9%
c [phase-count-11] 373009 positive 81.4% of 458464 except 85455 18.6%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 8 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 65269 enqueued variables after 41162 conflicts
c [score-dist-11] active 0 (0%), one 43504 (67%), zero 21765 (33%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 1239 variables 1.9% (65269 remain 23%)
c [simplification-11] removed 16999 irredundant clauses 3.6% (458464 remain 33%)
c [simplification-11] maximum reduction of 4% = max (2%, 4%)
c [simplification-11] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-11] new conflict interval 23000
c [simplification-11] penalized conflict interval 23000 = 1 * 23000
c [simplification-11] hard conflict limit 75662 (soft 64162 + delta 11500)
c [simplification-11] new conflict limit 64162 (hard 75662)
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  112.2   65268   458464     41842   28130   2359 355270   37   295   77  13%     19  175   41   15  281%
c i  112.3   65267   458464     41921   28190   2369 355278   37   292   77  13%     18  171   36   15  246%
c i  112.7   65179   458464     42226   28472   2379 355284   37   289   77  13%     13  168   36   15  245%
c i  112.8   65178   458464     42301   28539   2381 355286   37   287   77  13%     12  166   38   15  257%
c i  114.2   65177   458464     42988   29179   2397 355305   37   307   77  12%      8  184   42   15  277%
c i  114.4   65168   458464     43164   29340   2403 355308   38   306   77  12%      6  183   41   15  273%
c i  115.3   65125   458464     43721   29828   2430 355330   37   308   77  12%      5  182   37   15  241%
c i  115.8   65124   458464     43964   30047   2438 355339   38   313   77  12%      3  187   47   15  304%
c i  116.7   65123   458464     44467   30487   2459 355364   39   315   77  12%      3  188   51   16  328%
c i  118.0   65036   458464     45191   31138   2481 355389   39   316   77  12%      3  186   43   16  269%
c i  118.1   65035   458464     45220   31165   2482 355389   39   315   77  12%      3  186   42   16  267%
c i  118.4   65034   458464     45352   31290   2483 355392   39   316   77  12%      2  186   42   16  265%
c i  118.5   65033   458464     45418   31349   2485 355394   39   317   77  12%      2  186   43   16  271%
c i  118.6   65031   458464     45449   31374   2488 355396   39   318   77  12%      2  187   42   16  262%
c i  118.7   65030   458464     45501   31421   2490 355396   39   320   77  12%      2  190   49   16  303%
c i  119.1   64957   458464     45700   31598   2496 355399   42   328   77  13%      1  197   68   16  416%
c i  120.6   64956   458464     46522   32350   2520 355417   46   338   77  14%      3  204   64   17  377%
c i  122.3   64955   458464     47404   33164   2542 355434   48   350   77  14%      4  214   49   17  282%
c i  122.7   64954   458464     47603   33343   2550 355439   47   354   77  13%      3  217   46   17  261%
c i  123.6   64953   458464     48124   33822   2566 355450   46   350   77  13%      3  211   40   18  226%
c i  123.8   64952   458464     48225   33914   2569 355451   46   349   77  13%      2  210   42   18  239%
c i  125.3   64951   458464     49039   34661   2596 355477   45   346   77  13%      3  204   40   18  220%
c i  125.9   64950   458464     49321   34919   2605 355489   45   349   77  13%      2  207   36   18  202%
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  126.2   64949   458464     49475   35063   2606 355494   44   352   77  13%      2  210   39   18  216%
c i  127.3   64948   458464     50085   35610   2628 355516   45   350   77  13%      2  206   53   18  289%
c i  127.4   64947   458464     50214   35733   2628 355518   45   348   77  13%      2  203   51   18  276%
c i  128.8   64946   458464     51274   36706   2647 355536   46   356   77  13%      5  208   54   19  285%
c i  129.5   64945   458464     51750   37139   2658 355541   50   371   77  13%      4  221   84   19  437%
c i  130.2   64944   458464     52368   37703   2670 355551   50   361   77  14%      3  209   56   20  286%
c i  130.6   64943   458464     52771   38054   2671 355555   53   356   77  15%      2  203   87   20  432%
c i  130.8   64942   458464     52934   38207   2673 355558   53   366   77  15%      2  212   76   20  377%
c i  131.2   64941   458464     53142   38400   2675 355564   53   372   77  14%      1  218   64   20  319%
c i  131.3   64940   458464     53224   38473   2678 355565   54   373   77  14%      1  218   65   20  321%
c i  131.3   64936   458464     53262   38507   2678 355567   54   372   79  15%      1  218   70   20  343%
c i  134.8   64935   458464     55588   40652   2715 355600   63   419   86  15%     19  256   81   22  366%
c i  135.5   64934   458464     56065   41085   2732 355611   61   416   86  15%     12  250   48   22  217%
c i  135.5   64933   458464     56066   41085   2732 355611   61   415   86  15%     12  250   48   22  216%
c i  136.3   64930   458464     56677   41650   2744 355618   65   430   90  15%      8  262  102   23  443%
c i  136.3   64918   458464     56678   41650   2744 355618   65   430   90  15%      8  262  101   23  442%
c i  136.3   64917   458464     56679   41650   2744 355618   65   429   90  15%      7  262  101   23  440%
c i  137.5   64915   458464     57438   42343   2769 355635   63   426   90  15%      5  256   69   23  296%
c i  137.6   64914   458464     57489   42390   2770 355636   63   428   90  15%      5  257   66   23  283%
c i  137.6   64913   458464     57563   42456   2771 355639   63   426   90  15%      4  255   63   23  270%
c i  138.5   64912   458464     58175   42995   2782 355650   68   432   90  16%      3  259   72   24  299%
c i  142.2   64894   458464     60609   45220   2826 355698   69   433   95  16%     20  251   77   26  297%
c i  143.1   64893   458464     61253   45814   2850 355706   66   424   95  16%     12  239   56   26  216%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  143.4   64892   458464     61476   46017   2853 355714   65   420   95  15%      9  234   50   26  192%
c i  143.9   64891   458464     61769   46286   2858 355716   67   422   95  16%      6  235   80   26  302%
c i  144.0   64890   458464     61808   46322   2860 355716   67   421   95  16%      6  234   73   26  276%
c i  145.1   64889   458464     62498   46938   2882 355740   66   435   95  15%      4  246   57   27  211%
c i  146.2   64888   458464     63221   47605   2903 355755   66   445   95  15%      3  252   59   27  217%
c i  146.3   64887   458464     63309   47680   2908 355759   65   440   95  15%      3  247   51   27  188%
c i  147.5   64886   458464     64060   48377   2920 355771   66   450   99  15%      2  254   68   28  246%
c 
c [simplification-12] limit 64192 conflicts (hard 75662) hit after 64192 conflicts
c [quatres-7] found 28561 quaternary clauses 42% in total
c [quatres-7-2] added 4 single-self-subsuming ternary resolvents
c [quatres-7-2] added 1 quaternary resolvents
c [ternres-8] limit 23920856 with penalty 0 = 0 + 0
c [ternres-8] all 64886 free variables schedulable
c [ternres-8] 22 ternary resolvents (0 bin, 22 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-27] removed 595 variables
c [simpleprobe-5] 799 schedulable variables 1%
c [simpleprobe-5] limit 95683427 penalty 0 = 0 + 0
c [decomp-28] removed 624 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 624 variables, found 23381 hbrs, 272 units
c [unhide-12] limit 1196042 with penalty 2 = 0 + 2
c [unhide-12-12] 7 units, 201 failed, 42978 tauts, 0 hbrs, 354136 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 213 transitive binary clauses
c [transred-8] found 8 units
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 63692 variables 100%
c [elim-9] limit of 239208568 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1219 variables 2% in round 1 in 41957825 steps
c [elim-9-1] backward subsumption/strengthening limit 41957800
c [elim-9-1-1] backward checking 5110 touched variables 8%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 13 and strengthened 30 clauses in 1724352 steps
c [elim-9-1] rescheduled 118 variables 0% by backward subsumption
c [elim-9-2] eliminated 8 variables 0% in round 2 in 99133 steps
c [elim-9-2] backward subsumption/strengthening limit 99100
c [elim-9-2-1] backward checking 77 touched variables 0%
c [elim-9-2-1] incomplete backward checking 0 remain 0%
c [elim-9-2] subsumed 0 and strengthened 2 clauses in 99101 steps
c [elim-9-2] rescheduled 8 variables 0% by backward subsumption
c [elim-9-3] eliminated 1 variables 0% in round 3 in 9843 steps
c [elim-9-3] backward subsumption/strengthening limit 9800
c [elim-9-3-1] backward checking 10 touched variables 0%
c [elim-9-3-1] incomplete backward checking 5 remain 50%
c [elim-9-3] subsumed 0 and strengthened 2 clauses in 9825 steps
c [elim-9] incomplete 8 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 1228 = 2% variables out of 63692 scheduled
c [bca-8] limit of 10000000 steps and 888135 added (scaled 2)
c [bca-8] 88960 out of 124930 literals actually usable 71%
c [bca-8] added 79 blocked clauses in 250581 steps
c [phase-count-12] 439770 negative 99.1% of 443620 except 3850 0.9%
c [phase-count-12] 359833 positive 81.1% of 443620 except 83787 18.9%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 2 negative 100%
c [sort-queue-12] sorted 62464 enqueued variables after 64192 conflicts
c [score-dist-12] active 0 (0%), one 43621 (70%), zero 18843 (30%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 2422 variables 3.7% (62464 remain 22%)
c [simplification-12] removed 14844 irredundant clauses 3.2% (443620 remain 32%)
c [simplification-12] maximum reduction of 4% = max (4%, 3%)
c [simplification-12] geometric conflict interval increment 4600 = 23000 / 5
c [simplification-12] new conflict interval 27600
c [simplification-12] penalized conflict interval 27600 = 1 * 27600
c [simplification-12] hard conflict limit 105592 (soft 91792 + delta 13800)
c [simplification-12] new conflict limit 91792 (hard 105592)
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  154.1   62463   443620     64408   31922   2768 306843   63   438   71  14%      1  241   45   28  163%
c i  155.1   62462   443620     65008   32480   2782 306860   61   441   71  14%      1  242   45   28  160%
c i  156.2   62455   443620     65844   33253   2794 306873   61   434   71  14%      2  232   52   28  183%
c i  157.6   62454   443620     67080   34393   2817 306898   59   426   71  14%      6  220   71   29  246%
c i  157.9   62450   443620     67317   34616   2819 306900   58   422   71  14%      4  215   60   29  208%
c i  158.1   62449   443620     67494   34777   2822 306904   59   416   71  14%      3  209   59   29  206%
c i  158.6   62448   443620     67919   35164   2828 306907   60   408   71  15%      2  199   72   29  247%
c i  160.0   62447   443620     68955   36126   2850 306926   60   405   71  15%      4  193   52   30  177%
c i  160.1   62446   443620     68972   36140   2851 306927   60   405   71  15%      4  192   51   30  171%
c i  160.3   62445   443620     69133   36292   2852 306930   60   408   72  15%      3  195   54   30  181%
c i  161.0   62444   443620     69665   36771   2859 306941   59   400   72  15%      2  186   52   30  174%
c i  161.0   62443   443620     69666   36771   2859 306941   59   400   72  15%      2  186   52   30  174%
c i  162.2   62439   443620     70645   37684   2873 306949   58   394   72  15%      3  178   58   30  191%
c i  163.0   62438   443620     71227   38222   2887 306957   58   403   72  14%      2  185   59   31  194%
c i  163.1   62437   443620     71253   38242   2889 306959   58   404   72  14%      2  185   57   31  187%
c i  163.3   62436   443620     71375   38354   2892 306961   57   400   72  14%      1  181   45   31  149%
c i  163.9   62435   443620     71808   38753   2906 306974   58   405   72  14%      1  186   62   31  201%
c i  164.1   62405   443620     71950   38883   2908 306979   57   399   72  14%      0  179   47   31  153%
c i  164.1   62388   443620     71951   38883   2908 306979   57   399   72  14%      0  179   47   31  153%
c i  167.0   62377   443620     74202   40929   2955 307023   62   402   81  15%     17  175   54   32  170%
c i  169.7   62372   443620     76187   42718   3003 307082   61   406   81  15%     16  174   37   33  113%
c i  171.2   62368   443620     77331   43786   3022 307096   60   417   85  14%      9  182   59   33  178%
c i  172.0   62367   443620     77882   44293   3033 307112   63   425   85  15%      5  189   77   34  228%
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  172.2   62365   443620     78050   44438   3043 307120   62   421   85  15%      4  184   58   34  172%
c i  172.7   62364   443620     78434   44791   3049 307125   60   414   85  14%      2  175   46   34  135%
c i  173.9   62363   443620     79217   45505   3074 307144   62   429   85  15%      2  189   78   34  228%
c i  174.4   62362   443620     79602   45860   3080 307152   62   423   85  15%      1  181   60   34  174%
c i  177.1   62361   443620     81649   47772   3111 307179   60   412   86  15%     14  165   67   35  192%
c i  177.9   62357   443620     82211   48281   3119 307183   66   425   91  16%      8  177  138   36  388%
c i  177.9   62356   443620     82232   48294   3119 307184   67   425   91  16%      7  177  147   36  412%
c i  179.1   62317   443620     83035   49023   3141 307198   66   422   91  16%      4  171   54   36  149%
c i  179.1   62316   443620     83044   49031   3141 307198   66   422   91  16%      4  171   52   36  145%
c i  181.6   62315   443620     84643   50467   3185 307228   68   430   94  16%      9  175   57   37  155%
c i  182.2   62314   443620     85136   50895   3191 307232   70   418   94  17%      5  162   75   37  200%
c i  183.2   62313   443620     85878   51587   3204 307243   69   429   94  16%      3  171   61   38  162%
c i  187.4   62312   443620     88756   54197   3252 307292   73   432   99  17%     24  167   92   39  234%
c i  187.9   62311   443620     89151   54553   3255 307299   75   432   99  17%     16  166  106   40  269%
c i  188.6   62309   443620     89575   54956   3257 307306   75   434  106  17%      9  167   78   40  196%
c i  188.9   62308   443620     89779   55146   3265 307306   73   434  133  17%      7  167   55   40  139%
c i  190.1   62307   443620     90535   55841   3275 307319   75   442  133  17%      3  173   77   40  192%
c i  190.7   62306   443620     90992   56244   3285 307328   73   428  133  17%      1  157   57   40  140%
c i  191.6   62305   443620     91667   56854   3294 307340   73   422  133  17%      0  149   72   41  176%
c 
c [simplification-13] limit 91813 conflicts (hard 105592) hit after 92330 conflicts
c [quatres-8] found 27270 quaternary clauses 41% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 2 single-self-subsuming ternary resolvents
c [quatres-8-2] added 2 quaternary resolvents
c [ternres-9] limit 32183737 with penalty 0 = 0 + 0
c [ternres-9] all 62303 free variables schedulable
c [ternres-9] 273 ternary resolvents (0 bin, 273 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-29] removed 201 variables
c [treelook-5] limit 3218373 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 117951 literals 95%
c [treelook-5] scheduling used 2022665 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 3218373 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 3239645 steps
c [treelook-5] 117827 literals remain 95%
c [treelook-5] 37607 variables remain to probed next time 60%
c [decomp-30] removed 3 variables
c [treelook-5] removed 29 variables, found 9434 hbrs
c [unhide-13] limit 1609186 with penalty 2 = 0 + 2
c [unhide-13-13] 2 units, 47 failed, 6150 tauts, 0 hbrs, 296159 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 209 transitive binary clauses
c [transred-9] found 3 units
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 62141 variables 100%
c [elim-10] limit of 643674746 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 402 variables 1% in round 1 in 40760383 steps
c [elim-10-1] backward subsumption/strengthening limit 40760300
c [elim-10-1-1] backward checking 1961 touched variables 3%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 8 and strengthened 9 clauses in 781466 steps
c [elim-10-1] rescheduled 41 variables 0% by backward subsumption
c [elim-10-2] eliminated 4 variables 0% in round 2 in 1283612 steps
c [elim-10-2] backward subsumption/strengthening limit 1283600
c [elim-10-2-1] backward checking 34 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 8 and strengthened 5 clauses in 83822 steps
c [elim-10-2] rescheduled 10 variables 0% by backward subsumption
c [elim-10-3] eliminated 3 variables 0% in round 3 in 20851 steps
c [elim-10-3] backward subsumption/strengthening limit 20800
c [elim-10-3-1] backward checking 16 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 3 and strengthened 0 clauses in 20801 steps
c [elim-10] incomplete 4 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 411 = 1% variables out of 62141 scheduled
c [elim-10] 411 < 1/100 * 62141 = 621 considered unsuccessful
c [bca-9] limit of 10000000 steps and 873348 added (scaled 2)
c [bca-9] 82618 out of 123462 literals actually usable 67%
c [bca-9] added 21 blocked clauses in 247133 steps
c [sweep-8] limit 4827560 penalty 1 = 1 + 0
c [sweep-8-1] 4615 pos 9.2% + 45444 neg 90.8% = 50059 sched 81.1% ret 11671
c [sweep-8-1] 5121040 steps 50 queries 5458.20 avg class size
c [sweep-8-1] 984 decisions 47 SAT calls 297.00 avg env size
c [sweep-8-1] 48838 variables remain 79% (12882 retained 21%)
c [decomp-31] removed 18 variables
c [sweep-8-1] removed 18 vars (0 failed, 2 eqs, 7 impls)
c [sweep-8] 18 < 1/1000 * 61730 = 61 considered unsuccessful
c [sweep-8] removed 18 vars in TOTAL (1 rounds, 49 queries)
c [phase-count-13] 432288 negative 99.1% of 436102 except 3814 0.9%
c [phase-count-13] 353750 positive 81.1% of 436102 except 82352 18.9%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 61712 enqueued variables after 92330 conflicts
c [score-dist-13] active 0 (0%), one 44018 (71%), zero 17694 (29%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 591 variables 0.9% (61712 remain 21%)
c [simplification-13] removed 7518 irredundant clauses 1.7% (436102 remain 31%)
c [simplification-13] maximum reduction of 2% = max (1%, 2%)
c [simplification-13] geometric conflict interval increment 9200 = 27600 / 3
c [simplification-13] new conflict interval 36800
c [simplification-13] penalized conflict interval 36800 = 1 * 36800
c [simplification-13] hard conflict limit 147530 (soft 129130 + delta 18400)
c [simplification-13] new conflict limit 129130 (hard 147530)
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  201.5   61711   436102     94392   47446   3492 316952   63   388   96  16%     22  110   65   41  159%
c i  203.4   61710   436102     95580   48533   3515 316974   67   414   96  16%     10  134   68   42  162%
c i  203.6   61709   436102     95688   48637   3516 316976   66   414   96  16%      8  134   60   42  144%
c i  204.8   61708   436102     96468   49353   3541 316991   66   429   96  15%      4  147   58   42  138%
c i  204.9   61707   436102     96554   49432   3544 316993   65   429   96  15%      3  147   50   42  119%
c i  207.6   61692   436102     98468   51183   3564 317023   69   424   96  16%     11  137   74   43  173%
c i  207.7   61691   436102     98506   51216   3565 317025   70   430   96  16%     10  143   89   43  206%
c i  207.8   61690   436102     98583   51290   3565 317027   70   427   96  16%      9  141   75   43  174%
c i  209.0   61688   436102     99332   51979   3571 317036   75   442   96  17%      4  154  102   44  232%
c i  210.1   61687   436102    100776   53319   3582 317052   65   373   96  18%      6   82   42   44   96%
c i  210.5   61686   436102    101144   53648   3594 317058   64   365   96  18%      3   74   46   44  105%
c i  212.0   61685   436102    102508   54938   3602 317064   66   373  105  18%      5   80   87   44  196%
c i  212.3   61640   436102    102672   55091   3606 317067   66   381  111  17%      3   88   91   44  205%
c i  212.4   61639   436102    102832   55245   3608 317067   65   376  111  17%      2   83   67   44  151%
c i  212.6   61638   436102    102888   55296   3608 317067   66   375  111  18%      2   82   72   44  162%
c i  213.4   61637   436102    103466   55846   3613 317075   67   383  111  17%     -0   89   72   45  161%
c i  214.1   61636   436102    103850   56201   3619 317082   69   396  111  17%     -1  101   78   45  172%
c i  214.2   61635   436102    103912   56259   3619 317083   69   398  111  17%     -2  103   83   45  184%
c i  215.0   61634   436102    104391   56668   3629 317094   74   411  112  18%     -2  115  132   46  289%
c -  216.7   61634   436102    105867   19915   3650 317104   68   373   51  18%      5   75   51   46  112%
c i  217.5   61633   436102    106464   20480   3660 317110   68   389   55  17%     12   90   56   46  123%
c i  218.1   61632   436102    107455   21431   3666 317117   60   363   57  17%      5   63   30   46   65%
c i  219.1   61631   436102    108459   22386   3674 317131   58   379   59  15%      3   78   37   46   80%
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  221.1   61628   436102    110854   24611   3716 317167   56   383   64  15%     16   79   50   46  109%
c i  224.5   61627   436102    113923   27497   3751 317204   63   409   72  15%     26  100   47   47  101%
c i  224.9   61626   436102    114297   27835   3755 317210   62   409   74  15%     16  101   56   47  119%
c i  226.2   61625   436102    115377   28827   3781 317229   65   415   74  16%      7  105   67   48  141%
c i  227.8   61623   436102    117087   30448   3790 317245   63   409   78  15%      8   96   84   48  174%
c i  228.9   61622   436102    117948   31256   3797 317259   63   420   79  15%      3  106   58   48  121%
c i  229.5   61621   436102    118463   31734   3806 317263   64   414   80  16%      0   99   66   48  136%
c i  232.2   61614   436102    120744   33857   3843 317295   66   453   84  15%     14  134   70   49  143%
c i  233.6   61613   436102    122167   35179   3857 317311   64   421   84  15%      7   99   57   49  117%
c i  233.7   61612   436102    122260   35269   3858 317312   64   426   84  15%      6  104   58   49  118%
c i  235.7   61611   436102    124270   37111   3879 317350   63   395   91  16%     11   70   67   50  136%
c i  237.7   61610   436102    126506   39213   3900 317370   59   376  124  16%     14   49   51   50  102%
c i  238.0   61609   436102    126730   39418   3906 317372   59   380  124  16%     10   53   56   50  112%
c i  238.0   61608   436102    126775   39461   3906 317372   60   383  124  16%      9   56   66   50  133%
c i  238.5   61607   436102    127057   39722   3913 317376   62   396  126  16%      5   69   88   50  177%
c i  239.9   61601   436102    128070   40648   3941 317388   65   413  126  16%      2   84   65   50  130%
c i  240.6   61600   436102    128511   41059   3947 317395   64   411  126  16%     -1   82   65   50  128%
c i  240.8   61599   436102    128695   41228   3953 317398   64   417  126  15%     -2   87   60   50  119%
c i  241.7   61598   436102    129479   41953   3962 317408   65   407  128  16%     -2   76   68   51  134%
c 
c [simplification-14] limit 129130 conflicts (hard 147530) hit after 130602 conflicts
c [quatres-9] found 27272 quaternary clauses 41% in total
c [quatres-9-1] removed 2 duplicate quaternary clauses
c [quatres-9-2] added 1 single-self-subsuming ternary resolvents
c [quatres-9-2] added 2 quaternary resolvents
c [ternres-10] limit 41374708 with penalty 0 = 0 + 0
c [ternres-10] all 61598 free variables schedulable
c [ternres-10] 251 ternary resolvents (0 bin, 251 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 1034367 penalty 3 = 3 + 0
c [gauss-4] extracted 23 xors of average arity 2.9
c [gauss-4] connected 67 occurrences of 63 variables (average 1.1)
c [gauss-4] limit 1034367 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 62 variables
c [basicprobe-5] limit 206873541 penalty 0 = 0 + 0
c [basicprobe-5-0] 11359 probes remain 19% after last round
c [basicprobe-5-0] 1220 units = 1213 failed (99%) + 7 lifted (1%)
c [basicprobe-5-0] removed 1941 variables, found 455443 hbrs
c [bate-3] eliminated 538 asymmetric tautologies during probing
c [unhide-14] limit 2068735 with penalty 2 = 0 + 2
c [unhide-14-14] 10 units, 367 failed, 84361 tauts, 0 hbrs, 504394 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 127 transitive binary clauses
c [transred-10] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 258591926 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 374 (0%) of length 8
c [cce-4-1] eliminated 498 clauses out of 1102 (45%) of length 7
c [cce-4-1] eliminated 2695 clauses out of 5425 (50%) of length 6
c [cce-4-1] eliminated 14172 clauses out of 21255 (67%) of length 5
c [cce-4-1] eliminated 5753 clauses out of 27287 (21%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 23119 large clauses in 258591928 steps
c [cce-4-1] allowing another 129295964 steps for small clauses
c [cce-4-1] scheduling 272954 clauses = 205347 binary + 67607 ternary
c [cce-4-1] tried to eliminate 4706 small clauses 2%
c [cce-4-1] eliminated 1011 binary clauses 0%
c [cce-4-1] eliminated 218 ternary clauses 0%
c [cce-4-1] eliminated 1229 small clauses 0%
c [cce-4-1] eliminated 3545 small clauses in 258591931 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 26664 covered clauses in round 1
c [cce-4] eliminated 26664 covered clauses in TOTAL during 1 rounds
c [bca-10] limit of 10000000 steps and 798141 added (scaled 2)
c [bca-10] 79567 out of 118662 literals actually usable 67%
c [bca-10] added 61 blocked clauses in 214457 steps
c [phase-count-14] 397635 negative 99.8% of 398598 except 963 0.2%
c [phase-count-14] 317712 positive 79.7% of 398598 except 80886 20.3%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 2 negative 100%
c [sort-queue-14] sorted 59330 enqueued variables after 130602 conflicts
c [score-dist-14] active 0 (0%), one 43442 (73%), zero 15888 (27%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 2268 variables 3.7% (59330 remain 21%)
c [simplification-14] removed 37504 irredundant clauses 8.6% (398598 remain 29%)
c [simplification-14] maximum reduction of 9% = max (4%, 9%)
c [simplification-14] large reduction 9% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 142602 (soft 132602 + delta 10000)
c [simplification-14] new conflict limit 132602 (hard 142602)
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  268.7   59329   398598    130844   42923   4276 657870   68   439  120  15%      2  107   58   51  113%
c i  268.8   59328   398598    130907   42980   4277 657871   67   440  120  15%      1  107   52   51  102%
c 
c [simplification-15] limit 132602 conflicts (hard 142602) hit after 132602 conflicts
c [quatres-10] found 23518 quaternary clauses 57% in total
c [quatres-10-2] added 4 single-self-subsuming ternary resolvents
c [quatres-10-2] added 2 quaternary resolvents
c [ternres-11] limit 41869697 with penalty 0 = 0 + 0
c [ternres-11] all 59328 free variables schedulable
c [ternres-11] 55 ternary resolvents (0 bin, 55 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1308428 penalty 4 = 4 + 0
c [card-5] found 1365 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1308428 for elimination
c [card-5] 1365 out of 1365 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-33] removed 163 variables
c [simpleprobe-6] all 59167 free variables schedulable
c [simpleprobe-6] limit 167478788 penalty 0 = 0 + 0
c [decomp-34] removed 786 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 786 variables, found 51130 hbrs, 384 units
c [unhide-15] limit 2093484 with penalty 2 = 0 + 2
c [unhide-15-15] 3 units, 21 failed, 7853 tauts, 0 hbrs, 344257 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 251 transitive binary clauses
c [transred-11] found 4 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 58334 variables 100%
c [block-5] limit of 52337121 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 837 blocked clauses
c [block-5] 837 < 1/100 * 387716 = 3877 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 58301 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 10315 variables 18% in round 1 in 35968875 steps
c [elim-11-1] backward subsumption/strengthening limit 35968800
c [elim-11-1-1] backward checking 26014 touched variables 45%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 39 and strengthened 30 clauses in 4645209 steps
c [elim-11-1] rescheduled 153 variables 0% by backward subsumption
c [elim-11-2] eliminated 6 variables 0% in round 2 in 936314 steps
c [elim-11-2] backward subsumption/strengthening limit 936300
c [elim-11-2-1] backward checking 68 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 2 clauses in 332511 steps
c [elim-11-2] rescheduled 9 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 3878 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 10321 = 18% variables out of 58301 scheduled
c [bca-11] limit of 10000000 steps and 726289 added (scaled 2)
c [bca-11] 77152 out of 95962 literals actually usable 80%
c [bca-11] added 45 blocked clauses in 183530 steps
c [phase-count-15] 361784 negative 99.8% of 362657 except 873 0.2%
c [phase-count-15] 284061 positive 78.3% of 362657 except 78596 21.7%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 47980 enqueued variables after 132602 conflicts
c [score-dist-15] active 0 (0%), one 34723 (72%), zero 13257 (28%)
c [score-dist-15] max exp 1, different 2 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 11348 variables 19.1% (47980 remain 17%)
c [simplification-15] removed 35941 irredundant clauses 9.0% (362657 remain 26%)
c [simplification-15] maximum reduction of 19% = max (19%, 9%)
c [simplification-15] large reduction 19% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 144602 (soft 134602 + delta 10000)
c [simplification-15] new conflict limit 134602 (hard 144602)
c 
c [simplification-16] limit 134602 conflicts (hard 144602) hit after 134604 conflicts
c [quatres-11] found 27549 quaternary clauses 63% in total
c [quatres-11-1] removed 5 duplicate quaternary clauses
c [quatres-11-2] added 1 single-self-subsuming ternary resolvents
c [quatres-11-2] added 1 quaternary resolvents
c [ternres-12] limit 42104028 with penalty 0 = 0 + 0
c [ternres-12] all 47980 free variables schedulable
c [ternres-12] 567 ternary resolvents (0 bin, 567 trn)
c [ternres-12] fully completed ternary resolution
c [treelook-6] limit 4210402 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 85225 literals 89%
c [treelook-6] scheduling used 2162241 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 4210402 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 4247501 steps
c [treelook-6] 85117 literals remain 89%
c [treelook-6] 24763 variables remain to probed next time 52%
c [decomp-36] removed 1 variables
c [treelook-6] removed 14 variables, found 13103 hbrs
c [unhide-16] limit 8420805 with penalty 0 = 0 + 0
c [unhide-16-18] 6 units, 242 failed, 66120 tauts, 0 hbrs, 45520 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 202 transitive binary clauses
c [transred-12] found 1 units
c [cce-5] limit of 52630035 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 12 clauses out of 96 (12%) of length 7
c [cce-5-1] eliminated 245 clauses out of 3307 (7%) of length 6
c [cce-5-1] eliminated 7 clauses out of 8434 (0%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 264 large clauses in 52630047 steps
c [cce-5-1] allowing another 26315023 steps for small clauses
c [cce-5-1] scheduling 231180 clauses = 167071 binary + 64109 ternary
c [cce-5-1] tried to eliminate 824 small clauses 0%
c [cce-5-1] eliminated 182 binary clauses 0%
c [cce-5-1] eliminated 46 ternary clauses 0%
c [cce-5-1] eliminated 228 small clauses 0%
c [cce-5-1] eliminated 835 small clauses in 52630037 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1099 covered clauses in round 1
c [cce-5] eliminated 1099 covered clauses in TOTAL during 1 rounds
c [cce-5] 1099 < 1/100 * 359037 = 3590 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 47779 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 307 variables 1% in round 1 in 33076960 steps
c [elim-12-1] backward subsumption/strengthening limit 33076900
c [elim-12-1-1] backward checking 2101 touched variables 4%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 3 and strengthened 3 clauses in 656512 steps
c [elim-12-1] rescheduled 21 variables 0% by backward subsumption
c [elim-12-2] eliminated 2 variables 0% in round 2 in 18291 steps
c [elim-12-2] backward subsumption/strengthening limit 18200
c [elim-12-2-1] backward checking 24 touched variables 0%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 0 and strengthened 2 clauses in 18201 steps
c [elim-12-2] rescheduled 8 variables 0% by backward subsumption
c [elim-12-3] eliminated 1 variables 0% in round 3 in 8546 steps
c [elim-12-3] backward subsumption/strengthening limit 8500
c [elim-12-3-1] backward checking 10 touched variables 0%
c [elim-12-3-1] incomplete backward checking 0 remain 0%
c [elim-12-3] subsumed 0 and strengthened 2 clauses in 8526 steps
c [elim-12] incomplete 8 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 312 = 1% variables out of 47779 scheduled
c [elim-12] 312 < 1/100 * 47779 = 477 considered unsuccessful
c [bca-12] limit of 10000000 steps and 715528 added (scaled 2)
c [bca-12] 75942 out of 94936 literals actually usable 80%
c [bca-12] added 54 blocked clauses in 181222 steps
c [sweep-9] limit 3157802 penalty 2 = 2 + 0
c [sweep-9-1] 4579 pos 12.0% + 33681 neg 88.0% = 38260 sched 80.6% ret 9207
c [sweep-9-1] 3407682 steps 44 queries 5625.48 avg class size
c [sweep-9-1] 833 decisions 41 SAT calls 186.29 avg env size
c [sweep-9-1] 37025 variables remain 78% (10441 retained 22%)
c [decomp-37] removed 21 variables
c [sweep-9-1] removed 21 vars (0 failed, 2 eqs, 3 impls)
c [sweep-9] 21 < 1/1000 * 47467 = 47 considered unsuccessful
c [sweep-9] removed 21 vars in TOTAL (1 rounds, 43 queries)
c [phase-count-16] 356444 negative 99.8% of 357226 except 782 0.2%
c [phase-count-16] 279487 positive 78.2% of 357226 except 77739 21.8%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-16] sorted 47446 enqueued variables after 134604 conflicts
c [score-dist-16] active 0 (0%), one 34635 (73%), zero 12811 (27%)
c [score-dist-16] max exp 1, different 2 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 534 variables 1.1% (47446 remain 16%)
c [simplification-16] removed 5431 irredundant clauses 1.5% (357226 remain 26%)
c [simplification-16] maximum reduction of 1% = max (1%, 1%)
c [simplification-16] geometric conflict interval increment 18400 = 36800 / 2
c [simplification-16] new conflict interval 55200
c [simplification-16] penalized conflict interval 55200 = 1 * 55200
c [simplification-16] hard conflict limit 217404 (soft 189804 + delta 27600)
c [simplification-16] new conflict limit 189804 (hard 217404)
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  304.7   47445   357226    169209   45412   4606 512476   48   269  150  18%    439  -45   56   48  116%
c i  306.1   47444   357226    171766   47837   4619 512487   45   268  150  17%    -73  -44   51   48  106%
c -  312.1   47444   357226    181871   27949   4663 512516   37   216   65  17%      6  -88   27   47   58%
c 
c [simplification-17] limit 189804 conflicts (hard 217404) hit after 204876 conflicts
c [quatres-12] found 27574 quaternary clauses 63% in total
c [quatres-12-1] removed 4 duplicate quaternary clauses
c [quatres-12-2] added 1 single-self-subsuming ternary resolvents
c [quatres-12-2] added 8 quaternary resolvents
c [ternres-13] limit 51326352 with penalty 0 = 0 + 0
c [ternres-13] all 47444 free variables schedulable
c [ternres-13] 379 ternary resolvents (0 bin, 379 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-38] removed 4 variables
c [basicprobe-6] limit 256631764 penalty 0 = 0 + 0
c [basicprobe-6-0] 691 probes remain 2% after last round
c [basicprobe-6-0] 1028 units = 953 failed (93%) + 75 lifted (7%)
c [basicprobe-6-0] removed 1766 variables, found 513280 hbrs
c [bate-4] eliminated 2041 asymmetric tautologies during probing
c [unhide-17] limit 1283158 with penalty 3 = 0 + 3
c [unhide-17-19] 2 units, 16 failed, 4943 tauts, 0 hbrs, 2815066 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 288 transitive binary clauses
c [bca-13] limit of 10000000 steps and 671183 added (scaled 2)
c [bca-13] 65677 out of 91290 literals actually usable 72%
c [bca-13] added 11 blocked clauses in 192533 steps
c [phase-count-17] 334297 negative 99.8% of 335079 except 782 0.2%
c [phase-count-17] 260017 positive 77.6% of 335079 except 75062 22.4%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-17] sorted 45644 enqueued variables after 204876 conflicts
c [score-dist-17] active 0 (0%), one 34346 (75%), zero 11298 (25%)
c [score-dist-17] max exp 1, different 2 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 1800 variables 3.8% (45644 remain 16%)
c [simplification-17] removed 22147 irredundant clauses 6.2% (335079 remain 24%)
c [simplification-17] maximum reduction of 6% = max (4%, 6%)
c [simplification-17] large reduction 6% >= 5% limit
c [simplification-17] next conflict interval 2048 = min (204876/100, 55200)
c [simplification-17] penalized conflict interval 2048 = 1 * 2048
c [simplification-17] hard conflict limit 216924 (soft 206924 + delta 10000)
c [simplification-17] new conflict limit 206924 (hard 216924)
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  351.1   45643   335079    206134   51224   6066 919089   45   299  227  15%    321   24   57   44  131%
c 
c [simplification-18] limit 206924 conflicts (hard 216924) hit after 206925 conflicts
c [quatres-13] found 24295 quaternary clauses 60% in total
c [quatres-13-1] removed 3 duplicate quaternary clauses
c [quatres-13-2] added 1 single-self-subsuming ternary resolvents
c [quatres-13-2] added 1 quaternary resolvents
c [ternres-14] limit 51678801 with penalty 0 = 0 + 0
c [ternres-14] all 45598 free variables schedulable
c [ternres-14] 131 ternary resolvents (0 bin, 131 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-39] removed 103 variables
c [simpleprobe-7] all 45541 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-40] removed 377 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 377 variables, found 78828 hbrs, 178 units
c [unhide-18] limit 1291970 with penalty 3 = 0 + 3
c [unhide-18-20] 4 units, 43 failed, 122040 tauts, 0 hbrs, 1381064 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 300 transitive binary clauses
c [transred-14] found 2 units
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 45113 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 852 variables 2% in round 1 in 30039462 steps
c [elim-13-1] backward subsumption/strengthening limit 30039400
c [elim-13-1-1] backward checking 4910 touched variables 11%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 11 and strengthened 5 clauses in 1436573 steps
c [elim-13-1] rescheduled 40 variables 0% by backward subsumption
c [elim-13-2] eliminated 3 variables 0% in round 2 in 21262 steps
c [elim-13-2] backward subsumption/strengthening limit 21200
c [elim-13-2-1] backward checking 36 touched variables 0%
c [elim-13-2-1] incomplete backward checking 11 remain 31%
c [elim-13-2] subsumed 3 and strengthened 2 clauses in 21208 steps
c [elim-13-2] rescheduled 13 variables 0% by backward subsumption
c [elim-13-3] eliminated 1 variables 0% in round 3 in 23297 steps
c [elim-13-3] backward subsumption/strengthening limit 23200
c [elim-13-3-1] backward checking 22 touched variables 0%
c [elim-13-3-1] incomplete backward checking 0 remain 0%
c [elim-13-3] subsumed 0 and strengthened 1 clauses in 23201 steps
c [elim-13] incomplete 4 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 856 = 2% variables out of 45113 scheduled
c [bca-14] limit of 10000000 steps and 658216 added (scaled 2)
c [bca-14] 63330 out of 88516 literals actually usable 72%
c [bca-14] added 12 blocked clauses in 175649 steps
c [phase-count-18] 327844 negative 99.8% of 328593 except 749 0.2%
c [phase-count-18] 253856 positive 77.3% of 328593 except 74737 22.7%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-18] sorted 44257 enqueued variables after 206925 conflicts
c [score-dist-18] active 0 (0%), one 33751 (76%), zero 10506 (24%)
c [score-dist-18] max exp 1, different 2 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 1341 variables 2.9% (44257 remain 15%)
c [simplification-18] removed 6486 irredundant clauses 1.9% (328593 remain 24%)
c [simplification-18] maximum reduction of 3% = max (3%, 2%)
c [simplification-18] geometric conflict interval increment 13800 = 55200 / 4
c [simplification-18] new conflict interval 69000
c [simplification-18] penalized conflict interval 69000 = 1 * 69000
c [simplification-18] hard conflict limit 310425 (soft 275925 + delta 34500)
c [simplification-18] new conflict limit 275925 (hard 310425)
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  370.8   44256   328593    216757   47770   5865 772639   50   292  121  17%    -38   12   70   44  158%
c i  377.1   44133   328593    225301   55794   5960 772681   52   314  129  17%    -56   36   62   45  138%
c i  377.4   44132   328593    225684   56151   5963 772684   52   318  129  16%    -91   39   58   45  129%
c -  379.2   44105   328593    229258   28586   5968 772687   41   277   62  15%   -123   -4   30   44   69%
c i  390.3   44104   328593    245588   44245   6069 772727   52   260  107  20%    127   -9   56   45  125%
c i  395.1   44069   328593    251384   49705   6134 772766   58   323  133  18%    -85   52   75   46  163%
c -  403.7   44065   328593    263417   29131   6217 772809   53   327   61  16%     24   48   62   47  132%
c 
c [simplification-19] limit 275925 conflicts (hard 310425) hit after 280861 conflicts
c [quatres-14] found 24515 quaternary clauses 58% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [quatres-14-2] added 1 single-self-subsuming ternary resolvents
c [quatres-14-2] added 4 quaternary resolvents
c [ternres-15] limit 63370604 with penalty 0 = 0 + 0
c [ternres-15] all 44065 free variables schedulable
c [ternres-15] 333 ternary resolvents (1 bin, 332 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 792132 penalty 4 = 4 + 0
c [gauss-5] extracted 9 xors of average arity 3.0
c [gauss-5] connected 27 occurrences of 24 variables (average 1.1)
c [gauss-5] limit 792132 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-41] removed 2 variables
c [treelook-7] limit 6337060 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 78686 literals 89%
c [treelook-7] scheduling used 2490135 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 6337060 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 6353493 steps
c [treelook-7] 78558 literals remain 89%
c [treelook-7] 22273 variables remain to probed next time 51%
c [treelook-7] removed 12 variables, found 31470 hbrs
c [unhide-19] limit 3168530 with penalty 2 = 0 + 2
c [unhide-19-22] 2 units, 37 failed, 45705 tauts, 0 hbrs, 1079846 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 247 transitive binary clauses
c [transred-15] found 1 units
c [cce-6] limit of 39606627 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 50
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 49
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 48
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 47
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 46
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 45
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 44
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 43
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 42
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 41
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 40
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 39
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 38
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 37
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 36
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 35
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 34
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 33
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 32
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 31
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 30
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 29
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 28
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 27
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 26
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 25
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 24
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 23
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 22
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 21
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 20
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 19
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 18
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 17
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 16
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 15
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 14
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 13
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 12
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 11
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 10
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 9
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 8
c [cce-6-1] eliminated 7 clauses out of 82 (9%) of length 7
c [cce-6-1] eliminated 4 clauses out of 3037 (0%) of length 6
c [cce-6-1] eliminated 16 clauses out of 8161 (0%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 111 large clauses in 39606628 steps
c [cce-6-1] allowing another 19803314 steps for small clauses
c [cce-6-1] scheduling 214808 clauses = 159539 binary + 55269 ternary
c [cce-6-1] tried to eliminate 899 small clauses 0%
c [cce-6-1] eliminated 168 binary clauses 0%
c [cce-6-1] eliminated 46 ternary clauses 0%
c [cce-6-1] eliminated 214 small clauses 0%
c [cce-6-1] eliminated 565 small clauses in 39606641 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 676 covered clauses in round 1
c [cce-6] eliminated 676 covered clauses in TOTAL during 1 rounds
c [cce-6] 676 < 1/100 * 324006 = 3240 considered unsuccessful
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 43990 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 184 variables 0% in round 1 in 28961547 steps
c [elim-14-1] backward subsumption/strengthening limit 28961500
c [elim-14-1-1] backward checking 1263 touched variables 3%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 14 and strengthened 3 clauses in 443437 steps
c [elim-14-1] rescheduled 20 variables 0% by backward subsumption
c [elim-14-2] eliminated 3 variables 0% in round 2 in 34712 steps
c [elim-14-2] backward subsumption/strengthening limit 34700
c [elim-14-2-1] backward checking 34 touched variables 0%
c [elim-14-2-1] incomplete backward checking 0 remain 0%
c [elim-14-2] subsumed 4 and strengthened 0 clauses in 34701 steps
c [elim-14-2] rescheduled 7 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 44836 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 187 = 0% variables out of 43990 scheduled
c [elim-14] 187 < 1/100 * 43990 = 439 considered unsuccessful
c [bca-15] limit of 10000000 steps and 647060 added (scaled 2)
c [bca-15] 59589 out of 87608 literals actually usable 68%
c [bca-15] added 13 blocked clauses in 171704 steps
c [phase-count-19] 322312 negative 99.8% of 323012 except 700 0.2%
c [phase-count-19] 249594 positive 77.3% of 323012 except 73418 22.7%
c [phase-count-19] skipping relative phase luck test
c [phase-19] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-19] sorted 43803 enqueued variables after 280861 conflicts
c [score-dist-19] active 0 (0%), one 33973 (78%), zero 9830 (22%)
c [score-dist-19] max exp 1, different 2 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 262 variables 0.6% (43803 remain 15%)
c [simplification-19] removed 5581 irredundant clauses 1.7% (323012 remain 23%)
c [simplification-19] maximum reduction of 2% = max (1%, 2%)
c [simplification-19] geometric conflict interval increment 23000 = 69000 / 3
c [simplification-19] new conflict interval 92000
c [simplification-19] penalized conflict interval 92000 = 1 * 92000
c [simplification-19] hard conflict limit 418861 (soft 372861 + delta 46000)
c [simplification-19] new conflict limit 372861 (hard 418861)
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  431.6   43802   323012    288777   50424   6575 747153   57   287  121  20%    345    9   69   48  144%
c i  433.9   43801   323012    291411   52917   6594 747165   60   306  128  19%   -153   27   77   48  159%
c -  443.0   43730   323012    301868   29053   6661 747200   55   304   59  18%    -54   19   57   50  115%
c i  444.0   43729   323012    303088   30179   6677 747204   58   319   66  18%    -34   33   67   50  134%
c i  446.0   43728   323012    305922   32844   6703 747220   60   329   69  18%   -155   41   68   50  135%
c i  464.8   43727   323012    328677   54101   6879 747311   65   345  111  19%    151   44   89   55  164%
c i  468.1   43715   323012    331888   57096   6900 747324   68   354  117  19%   -136   51   63   55  113%
c -  473.8   43704   323012    340336   29596   6925 747337   47   235   59  20%    -54  -65   52   54   95%
c i  484.2   43703   323012    354689   43523   6957 747369   43   216  144  20%    158  -76   44   53   83%
c i  502.1   43697   323012    376876   64671   7062 747423   54   272  221  20%    149  -11   63   54  118%
c 
c [simplification-20] limit 372861 conflicts (hard 418861) hit after 377339 conflicts
c [quatres-15] found 24973 quaternary clauses 57% in total
c [quatres-15-1] removed 1 duplicate quaternary clauses
c [quatres-15-2] added 2 single-self-subsuming ternary resolvents
c [quatres-15-2] added 5 quaternary resolvents
c [ternres-16] limit 79903827 with penalty 0 = 0 + 0
c [ternres-16] all 43692 free variables schedulable
c [ternres-16] 149 ternary resolvents (0 bin, 149 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-43] removed 132 variables
c [basicprobe-7] limit 399519138 penalty 0 = 0 + 0
c [basicprobe-7-0] 2394 sched 6%, 504 failed, 5 lifted, 120410 hbrs
c [decomp-44] removed 762 variables
c [basicprobe-7-1] 11202 sched 26%, 409 failed, 16 lifted, 234729 hbrs
c [decomp-45] removed 643 variables
c [basicprobe-7-2] 9856 probes remain 23% after last round
c [basicprobe-7-2] 968 units = 947 failed (98%) + 21 lifted (2%)
c [basicprobe-7-2] removed 1508 variables, found 362902 hbrs
c [bate-5] eliminated 906 asymmetric tautologies during probing
c [unhide-20] limit 1997595 with penalty 3 = 0 + 3
c [unhide-20-23] 0 units, 7 failed, 72432 tauts, 0 hbrs, 2102523 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 296 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 42156 variables 100%
c [block-6] limit of 49939892 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 43 blocked clauses
c [block-6] 43 < 1/100 * 307080 = 3070 considered unsuccessful
c [bca-16] limit of 10000000 steps and 614981 added (scaled 2)
c [bca-16] 52780 out of 84314 literals actually usable 63%
c [bca-16] added 10 blocked clauses in 178537 steps
c [sweep-10] limit 2996393 penalty 3 = 3 + 0
c [sweep-10-1] 4555 pos 13.1% + 30212 neg 86.9% = 34767 sched 82.5% ret 7389
c [sweep-10-1] 3001854 steps 52 queries 2129.83 avg class size
c [sweep-10-1] 1301 decisions 51 SAT calls 402.27 avg env size
c [sweep-10-1] 32701 variables remain 78% (9455 retained 22%)
c [decomp-46] removed 1 variables
c [sweep-10-1] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-10] 1 < 1/1000 * 42156 = 42 considered unsuccessful
c [sweep-10] removed 1 vars in TOTAL (1 rounds, 51 queries)
c [sort-queue-20] sorted 42155 enqueued variables after 377339 conflicts
c [score-dist-20] active 0 (0%), one 34025 (81%), zero 8130 (19%)
c [score-dist-20] max exp 1, different 2 (100%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 1537 variables 3.5% (42155 remain 15%)
c [simplification-20] removed 16048 irredundant clauses 5.0% (306964 remain 22%)
c [simplification-20] maximum reduction of 5% = max (4%, 5%)
c [simplification-20] large reduction 5% >= 5% limit
c [simplification-20] next conflict interval 3773 = min (377339/100, 92000)
c [simplification-20] penalized conflict interval 3773 = 1 * 3773
c [simplification-20] hard conflict limit 391112 (soft 381112 + delta 10000)
c [simplification-20] new conflict limit 381112 (hard 391112)
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 -  534.7   42155   306964    378759   31895   7411 870771   64   318   61  20%   -113   34   89   54  164%
c 
c [simplification-21] limit 381112 conflicts (hard 391112) hit after 388753 conflicts
c [quatres-16] found 23815 quaternary clauses 56% in total
c [quatres-16-1] removed 2 duplicate quaternary clauses
c [ternres-17] limit 82116240 with penalty 0 = 0 + 0
c [ternres-17] all 42155 free variables schedulable
c [ternres-17] 113 ternary resolvents (0 bin, 113 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 2566132 penalty 4 = 4 + 0
c [card-6] found 1530 at-most-one constraints of average size 3.8
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 2566132 for elimination
c [card-6] 1530 out of 1530 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-47] removed 1 variables
c [simpleprobe-8] all 42154 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-48] removed 83 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 83 variables, found 45097 hbrs, 19 units
c [unhide-21] limit 8211624 with penalty 1 = 0 + 1
c [unhide-21-26] 2 units, 4 failed, 58490 tauts, 0 hbrs, 475416 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 253 transitive binary clauses
c [transred-17] found 1 units
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 42064 variables 100%
c [elim-15] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 576 variables 1% in round 1 in 26705118 steps
c [elim-15-1] backward subsumption/strengthening limit 26705100
c [elim-15-1-1] backward checking 3303 touched variables 8%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 10 and strengthened 6 clauses in 901676 steps
c [elim-15-1] rescheduled 41 variables 0% by backward subsumption
c [elim-15-2] eliminated 3 variables 0% in round 2 in 51379 steps
c [elim-15-2] backward subsumption/strengthening limit 51300
c [elim-15-2-1] backward checking 35 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 0 and strengthened 0 clauses in 51301 steps
c [elim-15-2] fully rescheduled 41485 variables 99%
c [elim-15-3] eliminated 19 variables 0% in round 3 in 26663315 steps
c [elim-15-3] backward subsumption/strengthening limit 26663300
c [elim-15-3-1] backward checking 131 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 1 and strengthened 2 clauses in 81197 steps
c [elim-15] incomplete 8 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 598 = 1% variables out of 42064 scheduled
c [bca-17] limit of 10000000 steps and 600872 added (scaled 2)
c [bca-17] 54696 out of 82934 literals actually usable 66%
c [bca-17] added 11 blocked clauses in 152997 steps
c [sort-queue-21] sorted 41466 enqueued variables after 388753 conflicts
c [score-dist-21] active 0 (0%), one 33567 (81%), zero 7899 (19%)
c [score-dist-21] max exp 1, different 2 (100%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 689 variables 1.6% (41466 remain 14%)
c [simplification-21] removed 7052 irredundant clauses 2.3% (299912 remain 22%)
c [simplification-21] maximum reduction of 2% = max (2%, 2%)
c [simplification-21] geometric conflict interval increment 30666 = 92000 / 3
c [simplification-21] new conflict interval 122666
c [simplification-21] penalized conflict interval 122666 = 1 * 122666
c [simplification-21] hard conflict limit 572752 (soft 511419 + delta 61333)
c [simplification-21] new conflict limit 511419 (hard 572752)
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 -  575.4   41466   299912    422852   32811   7423 795916   36   274   59  13%    415  -29   68   54  126%
c -  607.6   41466   299912    461941   32570   7650 795995   59   302   58  20%    689  -17   50   60   84%
c -  637.5   41466   299912    501996   36080   7758 796034   66   342   92  19%    842   30   38   60   64%
c i  644.6   41465   299912    511158   44552   7821 796067   68   312  113  22%    866   -4   87   61  144%
c 
c [simplification-22] limit 511419 conflicts (hard 572752) hit after 511419 conflicts
c [ternres-18] limit 102915032 with penalty 0 = 0 + 0
c [ternres-18] all 41435 free variables schedulable
c [ternres-18] 250 ternary resolvents (8 bin, 242 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-49] removed 40 variables
c [treelook-8] limit 10291503 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 74167 literals 90%
c [treelook-8] scheduling used 2448876 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 10291503 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 10292306 steps
c [treelook-8] 73885 literals remain 89%
c [treelook-8] 20476 variables remain to probed next time 49%
c [treelook-8] removed 1 variables, found 6781 hbrs
c [unhide-22] limit 10000000 with penalty 1 = 0 + 1
c [unhide-22-29] 0 units, 10 failed, 32576 tauts, 0 hbrs, 394938 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 151 transitive binary clauses
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 41422 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 82 variables 0% in round 1 in 26539677 steps
c [elim-16-1] backward subsumption/strengthening limit 26539600
c [elim-16-1-1] backward checking 492 touched variables 1%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 2 and strengthened 0 clauses in 202347 steps
c [elim-16-1] rescheduled 4 variables 0% by backward subsumption
c [elim-16-2] no variable eliminated in round 2 in 2879 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 82 = 0% variables out of 41422 scheduled
c [elim-16] 82 < 1/100 * 41422 = 414 considered unsuccessful
c [bca-18] limit of 10000000 steps and 597255 added (scaled 2)
c [bca-18] 52639 out of 82682 literals actually usable 64%
c [bca-18] added 9 blocked clauses in 155534 steps
c [sort-queue-22] sorted 41340 enqueued variables after 511419 conflicts
c [score-dist-22] active 0 (0%), one 33966 (82%), zero 7374 (18%)
c [score-dist-22] max exp 1, different 2 (100%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 95 variables 0.2% (41340 remain 14%)
c [simplification-22] removed 1811 irredundant clauses 0.6% (298101 remain 22%)
c [simplification-22] maximum reduction of 1% = max (0%, 1%)
c [simplification-22] geometric conflict interval increment 61333 = 122666 / 2
c [simplification-22] new conflict interval 183999
c [simplification-22] penalized conflict interval 183999 = 1 * 183999
c [simplification-22] hard conflict limit 787417 (soft 695418 + delta 91999)
c [simplification-22] new conflict limit 695418 (hard 787417)
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  663.6   41339   298101    527518   56959   7953 768355   61   277  106  22%   -760  -43   94   62  153%
c i  668.9   41336   298101    532948   62034   7995 768376   71   361  122  20%   -856   39   47   63   75%
c -  678.2   41314   298101    543800   34068   8037 768385   69   260   58  27%   -643  -60   94   64  148%
c i  682.2   41313   298101    550259   40204   8051 768397   64   298   79  21%   -487  -19   84   63  132%
c -  711.5   41306   298101    585857   35650   8204 768448   72   353   90  20%    -13   46   81   66  123%
c i  741.0   41305   298101    624337   71534   8376 768515   76   362  198  21%    447   53   86   67  128%
c -  744.1   41305   298101    628448   37374   8388 768523   69   342   91  20%   -601   29   60   67   90%
c -  781.1   41305   298101    671997   37087   8605 768609   81   298   59  27%    177  -37   76   74  104%
c 
c [simplification-23] limit 695418 conflicts (hard 787417) hit after 695915 conflicts
c [quatres-17] found 24759 quaternary clauses 53% in total
c [quatres-17-1] removed 2 duplicate quaternary clauses
c [quatres-17-2] added 8 single-self-subsuming ternary resolvents
c [quatres-17-2] added 18 quaternary resolvents
c [ternres-19] limit 134322590 with penalty 0 = 0 + 0
c [ternres-19] all 41305 free variables schedulable
c [ternres-19] 98 ternary resolvents (3 bin, 95 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-51] removed 41 variables
c [basicprobe-8] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 9932 sched 24%, 239 failed, 3 lifted, 95854 hbrs
c [decomp-52] removed 340 variables
c [basicprobe-8-1] 3003 probes remain 7% after last round
c [basicprobe-8-1] 343 units = 337 failed (98%) + 6 lifted (2%)
c [basicprobe-8-1] removed 475 variables, found 123984 hbrs
c [bate-6] eliminated 332 asymmetric tautologies during probing
c [unhide-23] limit 5000000 with penalty 2 = 0 + 2
c [unhide-23-31] 0 units, 1 failed, 37598 tauts, 0 hbrs, 2061798 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 172 transitive binary clauses
c [cce-7] limit of 41975809 steps penalty 4 = 4 + 0
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 41
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 40
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 39
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 38
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 37
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 36
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 35
c [cce-7-1] eliminated 4 clauses out of 5 (80%) of length 34
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 33
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 32
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 31
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 30
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 29
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 28
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 27
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 26
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 25
c [cce-7-1] eliminated 7 clauses out of 7 (100%) of length 24
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 23
c [cce-7-1] eliminated 6 clauses out of 7 (86%) of length 22
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 21
c [cce-7-1] eliminated 6 clauses out of 6 (100%) of length 20
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 19
c [cce-7-1] eliminated 7 clauses out of 9 (78%) of length 18
c [cce-7-1] eliminated 8 clauses out of 12 (67%) of length 17
c [cce-7-1] eliminated 8 clauses out of 11 (73%) of length 16
c [cce-7-1] eliminated 7 clauses out of 12 (58%) of length 15
c [cce-7-1] eliminated 9 clauses out of 13 (69%) of length 14
c [cce-7-1] eliminated 11 clauses out of 14 (79%) of length 13
c [cce-7-1] eliminated 10 clauses out of 15 (67%) of length 12
c [cce-7-1] eliminated 14 clauses out of 16 (88%) of length 11
c [cce-7-1] eliminated 12 clauses out of 19 (63%) of length 10
c [cce-7-1] eliminated 15 clauses out of 21 (71%) of length 9
c [cce-7-1] eliminated 12 clauses out of 19 (63%) of length 8
c [cce-7-1] eliminated 16 clauses out of 95 (17%) of length 7
c [cce-7-1] eliminated 19 clauses out of 3008 (1%) of length 6
c [cce-7-1] eliminated 12 clauses out of 8118 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 244 large clauses in 41975811 steps
c [cce-7-1] allowing another 20987905 steps for small clauses
c [cce-7-1] scheduling 197419 clauses = 150362 binary + 47057 ternary
c [cce-7-1] tried to eliminate 1200 small clauses 1%
c [cce-7-1] eliminated 217 binary clauses 0%
c [cce-7-1] eliminated 41 ternary clauses 0%
c [cce-7-1] eliminated 258 small clauses 0%
c [cce-7-1] eliminated 271 small clauses in 41975813 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 515 covered clauses in round 1
c [cce-7] eliminated 515 covered clauses in TOTAL during 1 rounds
c [cce-7] 515 < 1/100 * 291900 = 2919 considered unsuccessful
c [bca-19] limit of 10000000 steps and 583828 added (scaled 2)
c [bca-19] 47860 out of 81642 literals actually usable 59%
c [bca-19] added 3 blocked clauses in 161064 steps
c [sort-queue-23] sorted 40820 enqueued variables after 695915 conflicts
c [score-dist-23] active 0 (0%), one 34206 (84%), zero 6614 (16%)
c [score-dist-23] max exp 1, different 2 (100%)
c [score-dist-23] median active exp 0, avg 0.0
c [simplification-23] removed 485 variables 1.2% (40820 remain 14%)
c [simplification-23] removed 6716 irredundant clauses 2.3% (291385 remain 21%)
c [simplification-23] maximum reduction of 2% = max (1%, 2%)
c [simplification-23] geometric conflict interval increment 61333 = 183999 / 3
c [simplification-23] new conflict interval 245332
c [simplification-23] penalized conflict interval 245332 = 1 * 245332
c [simplification-23] hard conflict limit 1063913 (soft 941247 + delta 122666)
c [simplification-23] new conflict limit 941247 (hard 1063913)
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 -  842.8   40820   291385    716785   39272   8479 797943   60   284   60  21%    596  -32   31   72   43%
c -  875.5   40820   291385    760387   41155   8602 797991   52   236   62  22%    804  -72   43   70   62%
c -  908.4   40820   291385    802002   41612   8698 798034   55   224   94  25%    908  -72   81   67  122%
c -  943.6   40820   291385    844331   42202   8801 798063   63   207   94  30%    963  -78   80   63  128%
c i  946.4   40819   291385    847605   45173   8809 798068   71   261  108  27%    966  -22  100   64  156%
c -  986.9   40819   291385    889307   40049   8957 798122   68   366   61  19%   -882   46   43   71   60%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 4037 basic ate = 3128 trn 77% + 909 lrg 23% in 6 updates
c bcas: 19 count, 1119 added (1393 skipped), 4581213 steps
c bkwd: tried 340589 clauses, 680978 lits, 2.00 lits/clause
c bkwd: checked 10463653 occs, 30.72 occs/clause, 15.37 occs/lit
c bkwd: subsumed 13 binary, 95 ternary, 39 large
c bkwd: strengthened 1 binary, 0 ternary (0% self), 166 large (0% self)
c blkd: 6 bces, 11983 removed, 9184493 resolutions, 25551706 steps
c blkd: 15711 blocking literals 3%, 36 pure
c bump: 902654 bumped seen, 565291271 lits 626.3 on average
c card: 6 count, 0 units, 0 am1, 128269545 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 44672 subsumed
c card: 21567 at-most-one constraints found, average size 4.78
c card: 21567 at-most-one constraints used 100%, average size 4.78
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: 7 cces, 26998 eliminated, 26834 ate 99%, 164 abce 1%
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: 4670846 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 159 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 52 decompositions, 76442 equivalent 26%
c deco: 41850 decision-only clauses 5%, 70% reduction
c decs: 12948850 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 16 elims, 87339 eliminated 29%, 12 pure 0%
c elms: 41 rounds, 2.6 rounds/bve
c elms: 59615 small 68%, 27676 large 32%
c elms: 186861 tried small, 59615 succeeded 32%, 127246 failed 68%
c elms: 50775 subsumed, 110176 strengthened, 497 blocked
c elms: 21503451 copies, 20928771 resolutions, 5518730 ipos
c elms: 5954572 subchks, 3256005 strchks
c gaus: 5 extractions, 657 extracted, 2.2 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10655160 steps, 5327580 extr 50%, 18652 elim 0%
c glue: 60.6 orig avg, 60.6 real avg, 6.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 2189279 = 268746 simple 12% + 1893603 trn 86% + 26930 lrg 1%, 5419 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 902654 clauses, 483.3 length
c lrnd: 436296009 lits = 497240999 orig - 60944990 removed 12%
c lrnd: 416254 uips 46%, 423675 flips 47%
c mins: 824220 mins 94%, 3699 bin 0%, 10292 size 1%
c mins: 953163406 poisoned searches, 201899260 hits, 21% hit rate
c mins: 1030515362 used twice searches, 21079214 hits, 2% hit rate
c move: moved 21882, 12580 bin 57%, 9302 trn 43%
c otfs: 2254 driving 25%, 6694 restarting 75%
c otfs: str 8948, 8795 red 98%, 153 irr 2%
c otfs: str 8948, 0 bin 0%, 126 trn 1%, 8822 lrg 99%
c otfs: sub 13, 12 red 92%, 1 irr 8%
c otfs: sub 13, 0 bin 0%, 1 trn 8%, 12 lrg 92%
c phas: 19 computed, 117337 set, 9 pos (0%), 117328 neg (100%)
c prbs: 8 basic, 95554 probed, 4087 failed, 110 lifted
c prbs: 8 simple, 862289 probed, 1134 failed, 2735 eqs
c prbs: 8 treelook, 597 probed, 42 failed, 0 lifted
c prom: 115678 locked 13% out of 881890 tried
c prps: 1877568189 props, 136 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 17 count, 47 quat, 31 self1, 0 self2, 764 dup
c queu: 23 sorted, 12948850 next (19 steps 0.00)
c queu: 567054186 enq (567054139 steps 1.00), 565291271 deq 100%
c redc: 11138 clauses 38%, 29375 tried 3%, 162 sat 1%
c redc: 26342 lits 9%, 284001 tried 0%, 162 sat 0%
c redc: 1462 times jump level reduced, 48.9 levels on average
c reds: 19 count, 47615.9 conflicts per reduce
c reds: 0 memlim 0%, 19 arith 100%
c reds: 560695 collected 81%, 135495 retired 19%
c rmbd: 46102 removed, 5668 red 12%
c rsts: 21206 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: 23 count, 21 confs 91%, 0 vars 0%
c simp: 1 its 4%, 1 bin 4%, 0 trns 0%
c subl: 902654 count (1190127 tried 1.3), 41452 sub out of 889377 (4.7%)
c swps: 10 count, 10 rounds, 470 queries (47.0/round)
c swps: 412 sat calls, 19 unsat (0.5% success rate)
c swps: 6940 decisions 16.8, 206 conflicts 0.5
c swps; 6459.1 avg class size, 193.7 avg environment size
c swps: 0 failed, 126 impls, 68 equivs
c swp0: 154 type 0 queries, 34 unsat (22.1%), 145 sat (94.2%)
c swp1: 316 type 1 queries, 197 unsat (62.3%), 257 sat (81.3%)
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: 27703805 calls to obtain time
c tops: 94300 fixed 32%, 367 its, 2465.13 confs/it
c trds: 19 transitive reductions, 4016 removed, 64 failed
c trds: 19638 nodes, 53409 edges, 38035093 steps
c trim: 1152370 words, 4.4 MB
c trnr: 19 count, 15 bin, 2981 trn, 226592470 steps
c unhd: 23 count, 31 rounds, 100739068 steps
c unhd: 732 non-trivial sccs of average size 2.5
c unhd: 68 units, 68 bin, 0 trn, 0 lrg
c unhd: 3403 failed, 3264 stamp, 0 lits, 50 bin, 19 trn, 0 lrg
c unhd: 683192 tauts, 26693 bin 4%, 12086 trn 2%, 887 lrg 0%
c unhd: 683192 tauts, 643526 stamp 94%, 617632 red 90%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 12144585 str, 68 bin 0%, 2778 trn 0%, 12141739 lrg 100%, 12113897 red 100%
c vars: 40819 remaining 14% and 258081 removed 86% out of 298900
c vars: 94300 fixed 32%, 87339 eliminated 29%, 76442 equivalent 26%
c vsts: 17974109613 visits, 94% srch, 6% simp, 0% lkhd
c vsts: 9.6 search visits per propagation, 18729.6 per conflict
c wchs: 2574362938 pushed, 68959239 enlarged, 236 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         889424        560695        135495      69565635       5843891        330145
c 
c  0 0         24631   3      1759   0         0   0  27795048  40    933550  16     30010   9     0.8
c  1 5          7610   1      1326   0      2676   2   4779283   7    236955   4      8420   3     0.2
c  2 6         22876   3      6987   1      6560   5   9481587  14<   627994  11     24904   8     0.9
c  3 9         51529   6     25160   4     10480   8  11180643  16   1065630  18     51759  16     2.8
c  4 14        93654  11     60362  11     14250  11   7311578  11    984043  17<    61090  19     6.6
c  5 21       126373  14     88579  16     16693  12   3986281   6    698714  12     49745  15<   18.2
c  6 30       133475  15<    96902  17     15966  12   2218939   3    451957   8     34603  10    40.2
c  7 41       129670  15     97930  17<    15026  11<  1140961   2    305707   5     23249   7    27.7
c  8 54       105090  12     79438  14     13382  10    671327   1    210580   4     17476   5    36.4
c  9 69        72903   8     53019   9     10957   8    460010   1    144967   2     12753   4    31.2
c 10 86        49949   6     30752   5     10676   8    318941   0     99126   2      8928   3    10.7
c 11 126       30683   3     11589   2      7635   6    158405   0     49999   1      4697   1     3.5
c 12 230       34488   4      6143   1      9120   7     54598   0     30431   1      2294   1     4.6
c 13 534        6490   1       749   0      2074   2      8031   0      4237   0       217   0     1.6
c 14 1526          3   0         0   0         0   0         3   0         1   0         0   0     0.0
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                  6.5           6.6           6.8           2.1           3.8           4.6
c std                  2.7           2.1           3.0           2.2           2.6           2.7
c 
c   82.712   8% probe
c   76.763   8% bump
c   52.906   5% unhide
c   19.801   2% elim
c   15.919   2% cce
c    8.767   1% decide
c    6.388   1% sweep
c    4.745   0% bca
c 
c   10.872 < 1% rest (below)
c 
c    3.366   0% block
c    2.769   0% transred
c    1.724   0% gauss
c    1.624   0% ternres
c    0.919   0% quatres
c    0.470   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    4.750   0% preprocessing     2%
c  206.568  21% inprocessing     98%
c ==================================
c  211.318  21% simplifying
c  787.961  79% search
c ==================================
c  999.285 100% all
c 
c        904702 conflicts,         905.3 confs/sec
c          7410 ternaries,         122.1 confs/ternary
c          5391 binaries,          167.8 confs/binary
c           367 iterations,       2465.1 confs/iteration
c 
c            19 reductions,          0.0 redus/sec,  47615.9 confs/reduction
c         21206 restarts,           21.2 rests/sec,     42.7 confs/restart
c      12948850 decisions,       12958.1 decis/sec,     14.3 decis/conflict
c    1877568189 propagations,  1878911.7 props/sec,    145.0 props/decision
c 
c 999.3 seconds, 298.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
