c launch: /data/cnf/sc2014/app/partial-10-17-s.cnf.bz2
c host: atom07
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=6
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] AVG (--score=6)
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       145     119     11 10798    1     9   56   9%      0    9    9    0 18117%
c i    5.1  104290   739575       350     259     40 10818    1    19   56   6%      0   19   10    0 11620%
c i    5.2  104113   739575       397     303     41 10819    1    20   56   7%      0   20   10    0 10821%
c i    5.3  103138   739575       486     378     44 10821    2    23   56   9%      0   22   15    0 11594%
c i    5.6  102656   739575       662     516     62 10828    2    29   56   8%      1   28   12    0 7953%
c i    5.7  102573   739575       679     532     62 10828    2    29   56   8%      1   29   12    0 7822%
c i    6.1  102525   739575       818     642     72 10838    3    38   56   7%      1   38   13    0 6879%
c i    6.2  102512   739575       913     727     77 10839    3    44   56   7%      1   43   13    0 6135%
c i    6.4  102449   739575       968     770     82 10845    3    47   56   6%      1   46   12    0 5697%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 2217 variables
c [simpleprobe-2] 7491 schedulable variables 7%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 8446 variables remain 8% (93871 retained 92%)
c [simpleprobe-2] removed 0 variables, found 1684 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 62179 literals 30%
c [treelook-1] scheduling used 429955 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 419275 steps
c [treelook-1] 62170 literals remain 30%
c [treelook-1] 61104 variables remain to probed next time 60%
c [decomp-5] removed 1 variables
c [treelook-1] removed 5 variables, found 2536 hbrs
c [basicprobe-1] limit 5803008 based on 725376 irredundant clauses
c [basicprobe-1-0] 32789 probes remain 35% after last round
c [basicprobe-1-0] 35 units = 35 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 7601 variables, found 11716 hbrs
c [unhide-2] limit 50000 with penalty 1 = 0 + 1
c [unhide-2-2] 2 units, 240 failed, 5058 tauts, 0 hbrs, 14501 literals
c [elim-2] 57151 variables 61% will be scheduled this time
c [elim-2] scheduled 57151 variables 61%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 18618 not tried 20% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 494 = 1% variables out of 57151 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 645217 negative 99.1% of 650940 except 5723 0.9%
c [phase-count-2] 522578 positive 80.3% of 650940 except 128362 19.7%
c [phase-count-2] less non-negative clauses 5723 than limit 65000 (10.0%)
c [phase-count-2] non-pos/non-neg = 128362/5723 = 22.43 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 3117 negative 100%
c [sort-queue-2] sorted 74012 enqueued variables after 1000 conflicts
c [score-dist-2] active 19543 (21%), one 0 (0%), zero 74012 (79%)
c [score-dist-2] max exp 511, different 10 (2%)
c [score-dist-2] median active exp 510, avg 510.3
c [simplification-2] removed 8846 variables 8.6% (93555 remain 33%)
c [simplification-2] removed 88635 irredundant clauses 12.0% (650940 remain 47%)
c [simplification-2] maximum reduction of 12% = max (9%, 12%)
c [simplification-2] large reduction 12% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
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.5   93554   650940      1012     734     72 16347    3    48   51   6%      1   48   11    0 5253%
c i    9.7   93470   650940      1077     789     76 16352    3    54   53   6%      1   53   13    0 5369%
c i    9.7   93463   650940      1078     789     76 16352    3    54   53   6%      1   53   13    0 5348%
c i    9.9   93422   650940      1136     838     82 16354    3    58   53   6%      1   57   13    0 5362%
c i    9.9   93411   650940      1166     865     82 16356    4    61   53   6%      1   61   14    0 5507%
c i   10.0   93091   650940      1188     883     82 16359    4    64   53   6%      1   63   14    0 5462%
c i   10.0   93083   650940      1189     883     82 16359    4    64   53   6%      1   63   14    0 5441%
c i   10.2   93062   650940      1249     935     84 16364    4    73   53   6%      1   72   23    0 7249%
c i   10.5   93051   650940      1363    1023     91 16374    5    84   53   6%      1   83   28    0 7379%
c i   10.5   93007   650940      1378    1034     91 16377    5    84   53   6%      1   83   27    0 7090%
c 
c [simplification-3] limit of 19 iterations hit after 19 iterations
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3321 at-most-one constraints of average size 4.5
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3321 out of 3321 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 944 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 50825 literals 27%
c [treelook-2] scheduling used 332253 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 341834 steps
c [treelook-2] 50810 literals remain 27%
c [treelook-2] 38648 variables remain to probed next time 42%
c [treelook-2] removed 4 variables, found 2140 hbrs
c [unhide-3] limit 142697 with penalty 0 = 0 + 0
c [unhide-3-3] 1 units, 127 failed, 12006 tauts, 0 hbrs, 1685 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 92355 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 24098 not tried 26% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 3205 = 3% variables out of 92355 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 619828 negative 99.1% of 625456 except 5628 0.9%
c [phase-count-3] 502855 positive 80.4% of 625456 except 122601 19.6%
c [phase-count-3] less non-negative clauses 5628 than limit 62500 (10.0%)
c [phase-count-3] non-pos/non-neg = 122601/5628 = 21.78 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 2211 negative 100%
c [sort-queue-3] sorted 65544 enqueued variables after 1378 conflicts
c [score-dist-3] active 23606 (26%), one 0 (0%), zero 65544 (74%)
c [score-dist-3] max exp 512, different 11 (2%)
c [score-dist-3] median active exp 511, avg 510.9
c [simplification-3] removed 3701 variables 4.0% (89150 remain 31%)
c [simplification-3] removed 25484 irredundant clauses 3.9% (625456 remain 45%)
c [simplification-3] maximum reduction of 4% = max (4%, 4%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 3020 (hard 13000)
c [simplification-3] 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   13.6   89149   625456      1593    1021    101 15143    7   126   52   6%      1  125   39    1 7475%
c i   13.7   89070   625456      1658    1080    102 15145    8   131   52   6%      1  130   40    1 7141%
c i   14.4   89062   625456      1947    1315    116 15174    9   156   52   6%      1  154   26    1 4095%
c i   14.6   88994   625456      2152    1480    133 15192    9   155   52   6%      1  153   21    1 2975%
c i   14.6   88985   625456      2172    1497    134 15193    9   155   52   6%      1  153   20    1 2863%
c i   15.0   88984   625456      2400    1696    147 15197   11   165   52   7%      1  162   41    1 4712%
c i   15.2   88972   625456      2487    1767    151 15205   12   174   52   7%      1  171   39    1 4263%
c i   15.3   88958   625456      2506    1781    152 15208   12   176   52   7%      1  173   37    1 4083%
c i   15.6   88946   625456      2737    1992    161 15214   13   187   52   7%      1  183   33    1 3189%
c i   15.6   88937   625456      2740    1994    161 15214   13   187   52   7%      1  183   33    1 3186%
c i   15.7   88929   625456      2768    2014    162 15219   13   189   52   7%      1  186   31    1 3012%
c i   15.7   88917   625456      2777    2022    162 15219   13   191   52   7%      1  187   31    1 3028%
c 
c [simplification-4] limit of 189 binary hit after 189 binaries
c [decomp-8] removed 242 variables
c [basicprobe-2] limit 7801423 penalty 0 = 0 + 0
c [basicprobe-2-0] 27831 probes remain 32% after last round
c [basicprobe-2-0] 40 units = 40 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 3264 variables, found 18189 hbrs
c [unhide-4] limit 312056 with penalty 0 = 0 + 0
c [unhide-4-4] 1 units, 223 failed, 3233 tauts, 0 hbrs, 4325 literals
c [elim-4] 18468 variables 22% will be scheduled this time
c [elim-4] scheduled 18468 variables 22%
c [elim-4] boosting limit by 20
c [elim-4] limit of 624113860 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 33893953 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 18468 scheduled
c [phase-count-4] 593360 negative 99.1% of 598988 except 5628 0.9%
c [phase-count-4] 482842 positive 80.6% of 598988 except 116146 19.4%
c [phase-count-4] less non-negative clauses 5628 than limit 59800 (10.0%)
c [phase-count-4] non-pos/non-neg = 116146/5628 = 20.64 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 1520 negative 100%
c [sort-queue-4] sorted 53946 enqueued variables after 2992 conflicts
c [score-dist-4] active 31368 (37%), one 0 (0%), zero 53946 (63%)
c [score-dist-4] max exp 513, different 10 (2%)
c [score-dist-4] median active exp 513, avg 512.1
c [simplification-4] removed 3603 variables 4.1% (85314 remain 30%)
c [simplification-4] removed 26468 irredundant clauses 4.2% (598988 remain 43%)
c [simplification-4] maximum reduction of 4% = max (4%, 4%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3024 (hard 13000)
c [simplification-4] new binary interval 1000
c 
c [simplification-5] limit 3024 conflicts (hard 13000) hit after 3024 conflicts
c [quatres-1] found 43427 quaternary clauses 44% in total
c [quatres-1-2] added 1 single-self-subsuming ternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 85314 free variables schedulable
c [ternres-1] 30 ternary resolvents (0 bin, 30 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 46 xors of average arity 2.4
c [gauss-1] connected 112 occurrences of 91 variables (average 1.2)
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 45 variables
c [unhide-5] limit 316820 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 67 failed, 8626 tauts, 0 hbrs, 3258 literals
c [transred-1] limit 1584100 with penalty 0 = 0 + 0
c [transred-1] removed 140 transitive binary clauses
c [transred-1] found 1 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 85115 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 9785 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 4 clauses out of 63 (6%) of length 10
c [cce-1-1] eliminated 784 clauses out of 2076 (38%) of length 9
c [cce-1-1] eliminated 317 clauses out of 809 (39%) of length 8
c [cce-1-1] eliminated 10 clauses out of 2913 (0%) of length 7
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1115 large clauses in 30000007 steps
c [cce-1-1] allowing another 15000003 steps for small clauses
c [cce-1-1] scheduling 391064 clauses = 274631 binary + 116433 ternary
c [cce-1-1] tried to eliminate 293 small clauses 0%
c [cce-1-1] eliminated 65 binary clauses 0%
c [cce-1-1] eliminated 20 ternary clauses 0%
c [cce-1-1] eliminated 85 small clauses 0%
c [cce-1-1] eliminated 85 small clauses in 30000000 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1200 covered clauses in round 1
c [cce-1] eliminated 1200 covered clauses in TOTAL during 1 rounds
c [cce-1] 1200 < 1/100 * 580188 = 5801 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1158476 added (scaled 2)
c [bca-1] 155926 out of 170232 literals actually usable 92%
c [bca-1] added 257 blocked clauses in 460894 steps
c [sweep-1] limit 1157976 based on 578988 irredundant clauses
c [sweep-1-1] 4013 pos 4.7% + 81102 neg 95.3% = 85115 sched 100.0% ret 0
c [sweep-1-1] 1179225 steps 19 queries 24543.63 avg class size
c [sweep-1-1] 143 decisions 17 SAT calls 56.94 avg env size
c [sweep-1-1] 84661 variables remain 99% (434 retained 1%)
c [decomp-10] removed 22 variables
c [sweep-1-1] removed 22 vars (0 failed, 1 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 22 vars in TOTAL (1 rounds, 18 queries)
c [phase-count-5] 573310 negative 99.0% of 578918 except 5608 1.0%
c [phase-count-5] 472867 positive 81.7% of 578918 except 106051 18.3%
c [phase-count-5] less non-negative clauses 5608 than limit 57800 (10.0%)
c [phase-count-5] non-pos/non-neg = 106051/5608 = 18.91 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 1470 negative 100%
c [sort-queue-5] sorted 53664 enqueued variables after 3024 conflicts
c [score-dist-5] active 31429 (37%), one 0 (0%), zero 53664 (63%)
c [score-dist-5] max exp 513, different 10 (2%)
c [score-dist-5] median active exp 513, avg 512.1
c [simplification-5] removed 221 variables 0.3% (85093 remain 30%)
c [simplification-5] removed 20070 irredundant clauses 3.4% (578918 remain 42%)
c [simplification-5] maximum reduction of 3% = max (0%, 3%)
c [simplification-5] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-5] new conflict interval 5000
c [simplification-5] penalized conflict interval 5000 = 1 * 5000
c [simplification-5] hard conflict limit 18024 (soft 8024 + delta 10000)
c [simplification-5] new conflict limit 8024 (hard 18024)
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   22.6   85092   578918      3387    2550    243 37855   18   256   52   7%      3  250   46    2 3049%
c i   22.7   85091   578918      3406    2567    244 37855   18   258   52   7%      3  252   46    2 3007%
c i   22.8   85090   578918      3441    2597    244 37857   19   263   52   7%      3  257   47    2 3048%
c i   23.1   84984   578918      3602    2741    249 37863   19   273   52   7%      3  267   43    2 2604%
c i   23.3   84983   578918      3681    2803    252 37873   20   282   52   7%      2  275   47    2 2746%
c i   23.4   84982   578918      3709    2826    253 37876   20   284   52   7%      2  277   45    2 2639%
c i   23.5   84976   578918      3749    2858    255 37880   21   288   52   7%      2  280   46    2 2628%
c i   24.1   84959   578918      4095    3146    267 37907   24   303   52   8%      2  294   54    2 2630%
c i   24.6   84958   578918      4457    3477    282 37917   26   311   53   8%      3  301   49    2 2130%
c i   24.7   84947   578918      4492    3508    283 37919   26   317   53   8%      2  307   54    2 2318%
c i   24.9   84936   578918      4580    3586    285 37923   27   322   53   8%      2  310   59    2 2430%
c i   25.1   84935   578918      4631    3632    286 37924   29   330   53   9%      2  319   78    3 3049%
c i   25.1   84934   578918      4632    3632    286 37924   29   330   53   9%      2  319   78    3 3037%
c i   25.1   84933   578918      4633    3632    286 37924   29   330   53   9%      2  318   77    3 3025%
c i   25.3   84932   578918      4697    3687    289 37929   30   337   53   9%      2  325   78    3 2966%
c i   25.5   84920   578918      4790    3768    298 37930   31   349   53   9%      2  336   81    3 2948%
c i   28.1   84919   578918      5983    4846    338 37972   41   443   55   9%      8  424   79    4 1986%
c i   28.5   84915   578918      6161    5019    340 37973   45   472   55   9%      7  452  100    4 2339%
c i   29.5   84914   578918      6571    5377    352 37993   46   495   56   9%      6  472   65    5 1402%
c i   29.6   84902   578918      6661    5446    357 38005   46   498   56   9%      5  474   55    5 1175%
c i   30.0   84901   578918      6844    5613    359 38015   48   511   57   9%      5  486   73    5 1483%
c i   30.1   84890   578918      6860    5626    360 38016   48   511   57   9%      5  486   72    5 1445%
c i   30.9   84889   578918      7134    5869    365 38038   51   543   57   9%      4  516   86    5 1621%
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   32.1   84888   578918      7634    6318    385 38052   54   564   58  10%      4  532   82    6 1396%
c i   32.3   84884   578918      7737    6405    386 38057   56   563   58  10%      4  531   91    6 1506%
c i   32.4   84872   578918      7789    6444    390 38060   57   566   58  10%      3  534   99    6 1617%
c 
c [simplification-6] limit 8044 conflicts (hard 18024) hit after 8044 conflicts
c [quatres-2] found 43282 quaternary clauses 45% in total
c [ternres-2] limit 4219259 with penalty 0 = 0 + 0
c [ternres-2] all 84872 free variables schedulable
c [ternres-2] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-2] 54000 variables remain 64% (30872 retained 36%)
c [card-3] limit 527407 penalty 2 = 2 + 0
c [card-3] found 2298 at-most-one constraints of average size 4.4
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 527407 for elimination
c [card-3] 2298 out of 2298 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 232 variables
c [simpleprobe-3] 8031 schedulable variables 9%
c [simpleprobe-3] limit 8438519 penalty 1 = 1 + 0
c [decomp-12] removed 19 variables
c [simpleprobe-3] 8857 variables remain 10% (75985 retained 90%)
c [simpleprobe-3] removed 19 variables, found 13341 hbrs, 12 units
c [unhide-6] limit 843851 with penalty 0 = 0 + 0
c [unhide-6-6] 2 units, 106 failed, 4916 tauts, 0 hbrs, 44600 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 209 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 84658 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 839 blocked clauses
c [block-2] 839 < 1/100 * 576671 = 5766 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 84658 variables 100%
c [elim-5] limit of 42192597 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 4516 not tried 5% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 886 = 1% variables out of 84658 scheduled
c [bca-2] limit of 10000000 steps and 1144906 added (scaled 2)
c [bca-2] 148080 out of 167546 literals actually usable 88%
c [bca-2] added 135 blocked clauses in 429390 steps
c [sweep-2] limit 1265777 penalty 0 = 0 + 0
c [sweep-2-1] 3834 pos 4.6% + 79550 neg 95.4% = 83384 sched 99.5% ret 388
c [sweep-2-1] 1270478 steps 20 queries 21793.85 avg class size
c [sweep-2-1] 155 decisions 14 SAT calls 80.57 avg env size
c [sweep-2-1] 83171 variables remain 99% (521 retained 1%)
c [decomp-13] removed 87 variables
c [sweep-2-1] removed 87 vars (0 failed, 5 eqs, 8 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 87 vars in TOTAL (1 rounds, 19 queries)
c [phase-count-6] 566066 negative 99.0% of 571568 except 5502 1.0%
c [phase-count-6] 466121 positive 81.6% of 571568 except 105447 18.4%
c [phase-count-6] less non-negative clauses 5502 than limit 57100 (10.0%)
c [phase-count-6] non-pos/non-neg = 105447/5502 = 19.17 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 888 negative 100%
c [sort-queue-6] sorted 44189 enqueued variables after 8044 conflicts
c [score-dist-6] active 39496 (47%), one 0 (0%), zero 44189 (53%)
c [score-dist-6] max exp 514, different 11 (2%)
c [score-dist-6] median active exp 514, avg 513.4
c [simplification-6] removed 1187 variables 1.4% (83685 remain 29%)
c [simplification-6] removed 7350 irredundant clauses 1.3% (571568 remain 41%)
c [simplification-6] maximum reduction of 1% = max (1%, 1%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 15000
c [simplification-6] penalized conflict interval 15000 = 1 * 15000
c [simplification-6] hard conflict limit 33044 (soft 23044 + delta 10000)
c [simplification-6] new conflict limit 23044 (hard 33044)
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.8   83684   571568      8192    5430    389 47174   58   575   57  10%      3  539   69    7 1061%
c i   37.9   83683   571568      8213    5445    393 47175   58   577   57  10%      3  541   67    7 1020%
c i   38.2   83638   571568      8333    5545    396 47183   60   590   57  10%      3  553   93    7 1367%
c i   38.3   83631   571568      8351    5560    397 47184   60   591   57  10%      3  554   89    7 1311%
c i   38.4   83567   571568      8383    5588    398 47185   60   596   57  10%      3  558   86    7 1265%
c i   40.4   83556   571568      9482    6585    431 47215   67   630   57  11%      7  583   95    8 1164%
c i   40.8   83544   571568      9639    6732    432 47220   69   644   57  11%      6  595  118    8 1386%
c i   40.9   83538   571568      9688    6771    437 47224   70   651   57  11%      6  602  114    9 1328%
c i   41.3   83209   571568      9840    6892    447 47235   72   655   57  11%      5  605  125    9 1412%
c i   42.1   83198   571568     10165    7181    453 47255   75   674   58  11%      4  621  120    9 1275%
c i   42.5   83197   571568     10312    7323    453 47258   76   688   58  11%      4  634  113   10 1174%
c i   42.5   83196   571568     10313    7323    453 47258   76   688   58  11%      4  634  112   10 1169%
c i   43.0   83185   571568     10520    7493    457 47270   77   688   59  11%      3  632   99   10 1009%
c i   44.3   83184   571568     11064    7983    469 47285   82   714   60  11%      4  652  117   11 1094%
c i   44.4   83183   571568     11091    8005    469 47285   83   716   60  12%      4  654  131   11 1213%
c i   44.7   83182   571568     11244    8137    475 47292   84   725   60  12%      3  661  121   11 1097%
c i   45.1   83175   571568     11418    8292    477 47294   86   724   60  12%      3  659  119   11 1046%
c i   45.3   83174   571568     11476    8344    479 47295   87   727   60  12%      3  661  136   12 1179%
c i   45.6   83092   571568     11652    8498    491 47300   86   728   61  12%      2  660  103   12  886%
c i   45.6   83085   571568     11654    8499    491 47300   86   727   61  12%      2  660  102   12  879%
c i   45.9   83061   571568     11805    8622    495 47310   85   721   62  12%      2  652   83   12  708%
c i   46.0   83060   571568     11892    8699    499 47312   85   716   62  12%      2  646   81   12  686%
c i   46.2   83048   571568     11974    8773    501 47314   87   720   63  12%      2  649  112   12  926%
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   47.4   83047   571568     12463    9207    512 47333   90   736   63  12%      2  660  117   13  915%
c i   47.9   83040   571568     12685    9401    517 47347   92   740   63  12%      2  662  120   13  912%
c i   48.1   83039   571568     12740    9451    519 47349   92   744   63  12%      2  665  117   13  884%
c i   48.4   83038   571568     12895    9586    526 47352   95   751   63  13%      2  671  141   14 1037%
c i   48.6   83037   571568     13007    9685    528 47355   96   742   63  13%      2  661  138   14  995%
c i   49.2   83036   571568     13210    9857    536 47371   96   749   63  13%      2  666  112   14  796%
c i   49.5   83035   571568     13352    9989    539 47372   95   749   64  13%      1  664  100   14  703%
c i   49.5   83002   571568     13357    9989    541 47373   95   749   64  13%      1  664   98   14  691%
c i   49.7   82856   571568     13451   10068    547 47378   95   748   64  13%      1  662   90   14  626%
c i   51.5   82827   571568     14282   10820    554 47409  100   762   64  13%      4  668  129   16  826%
c i   51.8   82822   571568     14378   10906    556 47414  100   769   64  13%      4  673  124   16  783%
c i   53.2   82795   571568     14943   11404    564 47439  103   778   66  13%      4  677  131   17  785%
c i   53.4   82753   571568     15023   11476    565 47440  102   776   66  13%      4  674  117   17  700%
c i   54.6   82743   571568     15592   11982    579 47453  104   762   68  14%      4  655  124   18  705%
c i   57.5   82733   571568     16776   13014    613 47507  103   774   72  13%      8  655   90   19  473%
c i   58.6   82722   571568     17251   13441    623 47529  102   766   74  13%      6  642  102   20  518%
c i   58.9   82717   571568     17355   13537    623 47534  102   767   74  13%      6  642  106   20  536%
c i   60.6   82716   571568     18193   14280    646 47563  104   747   74  14%      6  614  119   21  566%
c i   60.7   82715   571568     18195   14281    646 47563  104   747   74  14%      6  614  119   21  566%
c i   62.9   82714   571568     19168   15140    666 47594  108   759   76  14%      7  617  124   22  554%
c i   65.0   82674   571568     20065   15986    680 47605  109   787   77  14%      7  636  121   24  513%
c i   65.1   82508   571568     20092   16008    680 47606  109   786   77  14%      7  635  124   24  524%
c i   65.3   82500   571568     20188   16092    683 47611  110   787   77  14%      6  636  129   24  542%
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.0   82396   571568     20451   16341    688 47616  110   800   77  14%      5  646  120   24  494%
c i   66.4   82392   571568     20605   16471    690 47619  115   802   77  14%      4  646  179   25  723%
c i   66.4   82382   571568     20612   16477    690 47619  115   801   77  14%      4  645  175   25  707%
c i   66.5   82378   571568     20618   16481    691 47619  115   801   77  14%      4  644  172   25  694%
c i   69.1   82368   571568     21754   17499    711 47652  123   803   77  15%      8  636  138   27  513%
c i   70.5   82367   571568     22304   17996    723 47674  126   827   79  15%      6  654  136   28  486%
c i   70.6   82357   571568     22334   18025    723 47674  125   829   79  15%      6  656  132   28  473%
c i   72.2   82356   571568     22926   18542    744 47702  124   835   79  15%      5  657  131   29  457%
c 
c [simplification-7] limit 23068 conflicts (hard 33044) hit after 23068 conflicts
c [ternres-3] limit 12048136 with penalty 0 = 0 + 0
c [ternres-3] 52413 schedulable variables 63%
c [ternres-3] 76 ternary resolvents (0 bin, 76 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1204813 penalty 1 = 1 + 0
c [gauss-2] extracted 117 xors of average arity 2.1
c [gauss-2] connected 248 occurrences of 131 variables (average 1.9)
c [gauss-2] limit 1204813 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 129 variables
c [treelook-3] limit 1204813 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 121991 literals 74%
c [treelook-3] scheduling used 1204816 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1204813 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 2564779 steps
c [treelook-3] 121971 literals remain 74%
c [treelook-3] 31943 variables remain to probed next time 39%
c [treelook-3] removed 6 variables, found 8863 hbrs
c [unhide-7] limit 1204813 with penalty 1 = 0 + 1
c [unhide-7-7] 5 units, 71 failed, 7263 tauts, 0 hbrs, 204886 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 166 transitive binary clauses
c [transred-3] found 4 units
c [cce-2] limit of 30120341 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 1155 (0%) of length 9
c [cce-2-1] eliminated 1 clauses out of 480 (0%) of length 8
c [cce-2-1] eliminated 567 clauses out of 2396 (24%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 569 large clauses in 30120343 steps
c [cce-2-1] allowing another 15060171 steps for small clauses
c [cce-2-1] scheduling 379513 clauses = 262362 binary + 117151 ternary
c [cce-2-1] tried to eliminate 276 small clauses 0%
c [cce-2-1] eliminated 61 binary clauses 0%
c [cce-2-1] eliminated 8 ternary clauses 0%
c [cce-2-1] eliminated 69 small clauses 0%
c [cce-2-1] eliminated 1626 small clauses in 30120350 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 2195 covered clauses in round 1
c [cce-2] eliminated 2195 covered clauses in TOTAL during 1 rounds
c [cce-2] 2195 < 1/100 * 558682 = 5586 considered unsuccessful
c [elim-6] 4451 variables 5% will be scheduled this time
c [elim-6] scheduled 4451 variables 5%
c [elim-6] limit of 240962730 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 10777877 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 4451 scheduled
c [bca-3] limit of 10000000 steps and 1109348 added (scaled 2)
c [bca-3] 135135 out of 164098 literals actually usable 82%
c [bca-3] added 51 blocked clauses in 387030 steps
c [sweep-3] limit 3614440 penalty 0 = 0 + 0
c [sweep-3-1] 4237 pos 5.2% + 77329 neg 94.8% = 81566 sched 99.4% ret 482
c [sweep-3-1] 3644841 steps 37 queries 15993.43 avg class size
c [sweep-3-1] 432 decisions 33 SAT calls 131.39 avg env size
c [sweep-3-1] 80539 variables remain 98% (1473 retained 2%)
c [decomp-16] removed 40 variables
c [sweep-3-1] removed 40 vars (0 failed, 4 eqs, 10 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 40 vars in TOTAL (1 rounds, 36 queries)
c [phase-count-7] 548465 negative 99.0% of 553967 except 5502 1.0%
c [phase-count-7] 453038 positive 81.8% of 553967 except 100929 18.2%
c [phase-count-7] less non-negative clauses 5502 than limit 55300 (10.0%)
c [phase-count-7] non-pos/non-neg = 100929/5502 = 18.34 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 280 negative 100%
c [sort-queue-7] sorted 35660 enqueued variables after 23068 conflicts
c [score-dist-7] active 46348 (57%), one 0 (0%), zero 35660 (43%)
c [score-dist-7] max exp 516, different 12 (2%)
c [score-dist-7] median active exp 516, avg 515.4
c [simplification-7] removed 340 variables 0.4% (82008 remain 29%)
c [simplification-7] removed 17601 irredundant clauses 3.1% (553967 remain 40%)
c [simplification-7] maximum reduction of 3% = max (0%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 20000
c [simplification-7] penalized conflict interval 20000 = 1 * 20000
c [simplification-7] hard conflict limit 53068 (soft 43068 + delta 10000)
c [simplification-7] new conflict limit 43068 (hard 53068)
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   79.1   82007   553967     23262   18776    797 56391  124   829   91  15%      4  647  128   29  440%
c i   80.2   81999   553967     23730   19182    809 56424  119   821   91  15%      3  635   92   30  312%
c i   81.6   81998   553967     24268   19669    814 56444  122   827   91  15%      3  635  135   30  444%
c i   83.1   81997   553967     24849   20190    831 56462  120   821   91  15%      3  624   91   31  294%
c i   83.9   81985   553967     25205   20523    836 56468  119   811   91  15%      3  611  108   32  344%
c i   84.6   81984   553967     25501   20795    838 56477  118   807   91  15%      2  603  108   32  338%
c i   84.7   81983   553967     25546   20835    839 56477  117   810   91  15%      2  606  107   32  335%
c i   84.7   81975   553967     25547   20835    839 56477  117   809   91  15%      2  606  106   32  333%
c i   85.7   81969   553967     25954   21203    851 56484  117   795   91  15%      2  587  118   32  363%
c i   86.3   81968   553967     26175   21410    852 56489  120   807   91  15%      2  597  147   33  447%
c i   88.0   81942   553967     26845   22015    866 56516  120   805   91  15%      3  589  123   34  365%
c i   88.2   81941   553967     26910   22071    868 56520  121   806   91  15%      3  590  132   34  390%
c i   89.5   81940   553967     27425   22535    883 56541  118   803   91  15%      3  583  110   34  319%
c i   90.2   81939   553967     27671   22754    889 56548  118   804   91  15%      2  581  120   35  348%
c i   92.9   81931   553967     28863   23850    917 56575  119   789   91  15%      7  556  120   36  331%
c i   94.5   81930   553967     29438   24350    935 56603  123   797   91  15%      6  559  149   37  399%
c i   94.7   81929   553967     29498   24405    936 56606  123   795   91  16%      5  557  148   37  396%
c i   96.0   81925   553967     30030   24885    940 56627  128   801   91  16%      4  558  149   38  389%
c i   96.2   81924   553967     30094   24945    941 56627  128   801   91  16%      4  557  139   38  363%
c i   97.9   81875   553967     30716   25513    956 56634  129   817   91  16%      4  568  139   39  353%
c i  102.6   81874   553967     32604   27193    985 56680  137   804   94  17%     15  539  145   42  341%
c i  103.5   81873   553967     32921   27481    990 56687  138   812   94  17%     11  544  149   43  347%
c i  104.3   81872   553967     33192   27715    997 56693  141   816   94  17%      9  546  167   44  383%
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  111.1   81825   553967     35628   29896   1043 56758  148   829  125  18%     22  539  111   48  232%
c i  113.5   81616   553967     36576   30742   1073 56785  147   831  125  18%     12  533  141   49  286%
c i  113.5   81610   553967     36577   30742   1073 56785  147   831  125  18%     12  533  140   49  285%
c i  113.5   81603   553967     36578   30742   1073 56785  147   830  125  18%     12  533  140   49  284%
c i  115.6   81598   553967     37393   31498   1091 56796  145   845  125  17%      8  540  112   50  223%
c i  117.8   81597   553967     38176   32201   1105 56826  145   852  134  17%      6  541  145   51  282%
c i  119.2   81596   553967     38642   32623   1115 56837  143   855  134  17%      4  540  126   52  244%
c i  119.7   81595   553967     38817   32781   1116 56848  143   848  134  17%      3  532  124   52  237%
c i  122.4   81594   553967     39876   33735   1131 56866  148   838  140  18%      6  513  165   54  305%
c i  125.5   81593   553967     41020   34762   1155 56897  145   819  147  18%      7  486  138   55  248%
c i  125.9   81592   553967     41134   34864   1157 56899  146   825  147  18%      6  491  147   56  264%
c i  127.4   81591   553967     41643   35320   1169 56922  147   843  147  17%      4  505  143   56  253%
c i  130.7   81579   553967     42885   36452   1188 56955  139   820  151  17%      7  472  101   57  177%
c i  131.0   81578   553967     42986   36542   1190 56956  139   816  151  17%      6  468  118   58  205%
c 
c [simplification-8] limit 43098 conflicts (hard 53068) hit after 43098 conflicts
c [quatres-3] found 39432 quaternary clauses 44% in total
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [ternres-4] limit 22605272 with penalty 0 = 0 + 0
c [ternres-4] all 81571 free variables schedulable
c [ternres-4] 23 ternary resolvents (0 bin, 23 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 910 variables
c [basicprobe-3] limit 113026360 penalty 0 = 0 + 0
c [basicprobe-3-0] 23076 probes remain 29% after last round
c [basicprobe-3-0] 420 units = 408 failed (97%) + 12 lifted (3%)
c [basicprobe-3-0] removed 1350 variables, found 222627 hbrs
c [bate-1] eliminated 154 asymmetric tautologies during probing
c [unhide-8] limit 1130263 with penalty 2 = 0 + 2
c [unhide-8-8] 2 units, 257 failed, 19862 tauts, 0 hbrs, 458754 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 102 transitive binary clauses
c [transred-4] found 3 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 79419 variables 100%
c [block-3] limit of 113026360 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 110 blocked clauses
c [block-3] 110 < 1/100 * 542802 = 5428 considered unsuccessful
c [bca-4] limit of 10000000 steps and 1080103 added (scaled 2)
c [bca-4] 124616 out of 158838 literals actually usable 78%
c [bca-4] added 56 blocked clauses in 367339 steps
c [sweep-4] limit 6781581 penalty 0 = 0 + 0
c [sweep-4-1] 4610 pos 5.9% + 73554 neg 94.1% = 78164 sched 98.4% ret 1254
c [sweep-4-1] 6803023 steps 76 queries 8408.43 avg class size
c [sweep-4-1] 1352 decisions 53 SAT calls 194.49 avg env size
c [sweep-4-1] 74439 variables remain 94% (4907 retained 6%)
c [decomp-18] removed 305 variables
c [sweep-4-1] removed 305 vars (0 failed, 23 eqs, 45 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 305 vars in TOTAL (1 rounds, 75 queries)
c [phase-count-8] 533133 negative 99.0% of 538634 except 5501 1.0%
c [phase-count-8] 439427 positive 81.6% of 538634 except 99207 18.4%
c [phase-count-8] less non-negative clauses 5501 than limit 53800 (10.0%)
c [phase-count-8] non-pos/non-neg = 99207/5501 = 18.03 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 185 negative 100%
c [sort-queue-8] sorted 30841 enqueued variables after 43098 conflicts
c [score-dist-8] active 48272 (61%), one 0 (0%), zero 30841 (39%)
c [score-dist-8] max exp 517, different 13 (3%)
c [score-dist-8] median active exp 517, avg 516.4
c [simplification-8] removed 2458 variables 3.0% (79113 remain 27%)
c [simplification-8] removed 15333 irredundant clauses 2.8% (538634 remain 39%)
c [simplification-8] maximum reduction of 3% = max (3%, 3%)
c [simplification-8] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-8] new conflict interval 25000
c [simplification-8] penalized conflict interval 25000 = 1 * 25000
c [simplification-8] hard conflict limit 80598 (soft 68098 + delta 12500)
c [simplification-8] new conflict limit 68098 (hard 80598)
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  145.8   79112   538634     43714   37000   1214 252159  142   824  144  17%      5  471  164   59  280%
c i  148.1   79048   538634     44491   37725   1227 252176  139   817  144  17%      4  458  140   59  235%
c i  150.0   79047   538634     45188   38359   1240 252190  142   809  144  18%      3  446  173   61  286%
c i  151.1   79046   538634     45522   38652   1248 252206  147   827  144  18%      2  461  179   61  293%
c i  152.0   79045   538634     45826   38935   1251 252211  148   834  144  18%      2  467  174   62  281%
c i  153.0   79033   538634     46146   39228   1261 252220  148   837  144  18%      1  467  167   62  270%
c i  153.0   79032   538634     46152   39233   1261 252220  148   837  144  18%      1  467  167   62  268%
c i  155.6   79023   538634     47002   40013   1272 252236  149   844  145  18%      3  468  144   63  228%
c i  156.8   79019   538634     47357   40342   1283 252246  148   858  145  17%      2  479  144   64  226%
c i  163.8   79018   538634     49797   42562   1308 252283  156   853  174  18%     21  457  164   67  243%
c i  164.0   79017   538634     49853   42613   1308 252283  157   846  174  19%     19  450  166   67  245%
c i  165.4   79016   538634     50519   43223   1314 252294  153   825  174  19%     11  424  135   68  198%
c i  169.1   79015   538634     52295   44778   1337 252341  159   813  174  20%     13  401  154   71  218%
c i  170.6   79014   538634     52916   45334   1345 252357  157   821  174  19%      8  405  141   72  197%
c i  176.2   79013   538634     55471   47616   1369 252425  164   855  174  19%     22  424  164   75  217%
c i  176.2   79011   538634     55472   47616   1369 252425  164   855  174  19%     22  423  163   75  217%
c i  176.7   79010   538634     55664   47786   1375 252431  164   862  174  19%     17  429  165   76  218%
c i  177.7   79009   538634     56033   48120   1380 252436  166   866  174  19%     12  431  178   76  233%
c i  180.0   79008   538634     57097   49088   1387 252448  171   875  182  20%      7  433  152   78  195%
c i  181.4   79007   538634     57780   49667   1397 252461  168   842  182  20%      4  395  176   79  224%
c i  182.6   78815   538634     58368   50171   1404 252472  172   845  182  20%      3  395  191   80  238%
c i  182.7   78814   538634     58482   50258   1404 252472  172   830  182  21%      2  379  178   80  223%
c -  187.7   78814   538634     60739   11580   1431 252511  171   822   88  21%     17  358  165   83  199%
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  187.7   78813   538634     60780   11616   1431 252511  171   822   91  21%     17  358  172   83  206%
c i  188.0   78812   538634     60899   11727   1433 252512  172   828   92  21%     15  363  181   83  217%
c i  193.1   78811   538634     63536   14064   1470 252572  169   857   98  20%     22  377  164   87  189%
c i  200.7   78810   538634     67836   17939   1517 252647  151   838  108  18%     45  335  153   90  170%
c 
c [simplification-9] limit 68109 conflicts (hard 80598) hit after 68109 conflicts
c [quatres-4] found 36595 quaternary clauses 44% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 1 single-self-subsuming ternary resolvents
c [ternres-5] limit 33045559 with penalty 0 = 0 + 0
c [ternres-5] all 78797 free variables schedulable
c [ternres-5] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-19] removed 324 variables
c [simpleprobe-4] 8597 schedulable variables 11%
c [simpleprobe-4] limit 132182237 penalty 0 = 0 + 0
c [decomp-20] removed 743 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 743 variables, found 42780 hbrs, 272 units
c [unhide-9] limit 3304555 with penalty 1 = 0 + 1
c [unhide-9-10] 5 units, 464 failed, 27823 tauts, 0 hbrs, 248140 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 186 transitive binary clauses
c [transred-5] found 2 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 77719 variables 100%
c [elim-7] limit of 330455593 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 2798 variables 4% in round 1 in 48259622 steps
c [elim-7-1] backward subsumption/strengthening limit 48259600
c [elim-7-1-1] backward checking 9964 touched variables 13%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 1 and strengthened 59 clauses in 3329055 steps
c [elim-7-1] rescheduled 152 variables 0% by backward subsumption
c [elim-7-2] eliminated 18 variables 0% in round 2 in 172986 steps
c [elim-7-2] backward subsumption/strengthening limit 172900
c [elim-7-2-1] backward checking 152 touched variables 0%
c [elim-7-2-1] incomplete backward checking 0 remain 0%
c [elim-7-2] subsumed 0 and strengthened 6 clauses in 172901 steps
c [elim-7-2] rescheduled 7 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 8362 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 2823 = 4% variables out of 77719 scheduled
c [bca-5] limit of 10000000 steps and 1030309 added (scaled 2)
c [bca-5] 126188 out of 149794 literals actually usable 84%
c [bca-5] added 128 blocked clauses in 351718 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 99136670 penalty 0 = 0 + 0
c [sweep-5-1] 4482 pos 6.3% + 66367 neg 93.7% = 70849 sched 94.6% ret 4047
c [sweep-5-1] 99175198 steps 1347 queries 255.58 avg class size
c [sweep-5-1] 13086 decisions 1205 SAT calls 105.43 avg env size
c [sweep-5-1] 32225 variables remain 43% (42113 retained 57%)
c [decomp-21] removed 1396 variables
c [sweep-5-1] removed 1396 vars (0 failed, 150 eqs, 284 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1396 vars in TOTAL (1 rounds, 1346 queries)
c [phase-count-9] 505204 negative 99.0% of 510317 except 5113 1.0%
c [phase-count-9] 415258 positive 81.4% of 510317 except 95059 18.6%
c [phase-count-9] less non-negative clauses 5113 than limit 51000 (10.0%)
c [phase-count-9] non-pos/non-neg = 95059/5113 = 18.59 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 50 negative 100%
c [sort-queue-9] sorted 24231 enqueued variables after 68109 conflicts
c [score-dist-9] active 49269 (67%), one 0 (0%), zero 24231 (33%)
c [score-dist-9] max exp 518, different 13 (3%)
c [score-dist-9] median active exp 518, avg 517.2
c [simplification-9] removed 5297 variables 6.7% (73500 remain 26%)
c [simplification-9] removed 28317 irredundant clauses 5.3% (510317 remain 37%)
c [simplification-9] maximum reduction of 7% = max (7%, 5%)
c [simplification-9] large reduction 7% >= 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 80109 (soft 70109 + delta 10000)
c [simplification-9] new conflict limit 70109 (hard 80109)
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  214.1   73499   510317     68170   12123   1411 325175  151   843   66  18%     31  338  143   90  159%
c i  214.1   73488   510317     68231   12179   1411 325176  150   840   66  18%     29  336  129   90  143%
c i  214.2   73487   510317     68256   12196   1412 325176  150   836   66  18%     28  332  132   90  146%
c 
c [simplification-10] limit 70109 conflicts (hard 80109) hit after 70109 conflicts
c [quatres-5] found 38176 quaternary clauses 47% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [quatres-5-2] added 7 quaternary resolvents
c [ternres-6] limit 33727867 with penalty 0 = 0 + 0
c [ternres-6] all 73487 free variables schedulable
c [ternres-6] 225 ternary resolvents (0 bin, 225 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 2107991 penalty 3 = 3 + 0
c [card-4] found 3519 at-most-one constraints of average size 4.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2107991 for elimination
c [card-4] 3519 out of 3519 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1686393 penalty 2 = 2 + 0
c [gauss-3] extracted 27 xors of average arity 2.9
c [gauss-3] connected 77 occurrences of 74 variables (average 1.0)
c [gauss-3] limit 1686393 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 1 variables
c [treelook-4] limit 3372786 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 128183 literals 87%
c [treelook-4] scheduling used 2034281 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 3372786 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 3634292 steps
c [treelook-4] 128104 literals remain 87%
c [treelook-4] 27588 variables remain to probed next time 38%
c [decomp-23] removed 5 variables
c [treelook-4] removed 23 variables, found 14855 hbrs
c [unhide-10] limit 3372786 with penalty 1 = 0 + 1
c [unhide-10-11] 11 units, 186 failed, 15292 tauts, 0 hbrs, 47393 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 137 transitive binary clauses
c [transred-6] found 2 units
c [cce-3] limit of 42159834 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 5 clauses out of 952 (1%) of length 9
c [cce-3-1] eliminated 4 clauses out of 503 (1%) of length 8
c [cce-3-1] eliminated 728 clauses out of 1533 (47%) of length 7
c [cce-3-1] eliminated 2745 clauses out of 6011 (46%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 3482 large clauses in 42159844 steps
c [cce-3-1] allowing another 21079922 steps for small clauses
c [cce-3-1] scheduling 348252 clauses = 240528 binary + 107724 ternary
c [cce-3-1] tried to eliminate 548 small clauses 0%
c [cce-3-1] eliminated 131 binary clauses 0%
c [cce-3-1] eliminated 33 ternary clauses 0%
c [cce-3-1] eliminated 164 small clauses 0%
c [cce-3-1] eliminated 2907 small clauses in 42159838 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 6389 covered clauses in round 1
c [cce-3] eliminated 6389 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 73094 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 13491146920 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 3429 variables 5% in round 1 in 53089824 steps
c [elim-8-1] backward subsumption/strengthening limit 53089800
c [elim-8-1-1] backward checking 9210 touched variables 13%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 75 and strengthened 548 clauses in 3986532 steps
c [elim-8-1] rescheduled 1263 variables 2% by backward subsumption
c [elim-8-2] eliminated 179 variables 0% in round 2 in 2807914 steps
c [elim-8-2] backward subsumption/strengthening limit 2807900
c [elim-8-2-1] backward checking 1298 touched variables 2%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 690563 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 3612 = 5% variables out of 73094 scheduled
c [bca-6] limit of 10000000 steps and 981339 added (scaled 2)
c [bca-6] 118845 out of 138966 literals actually usable 86%
c [bca-6] added 433 blocked clauses in 327186 steps
c [sweep-6] limit 10118360 penalty 0 = 0 + 0
c [sweep-6-1] 3405 pos 11.1% + 27328 neg 88.9% = 30733 sched 44.2% ret 38749
c [sweep-6-1] 10273485 steps 187 queries 2074.45 avg class size
c [sweep-6-1] 1943 decisions 164 SAT calls 106.40 avg env size
c [sweep-6-1] 29328 variables remain 42% (40066 retained 58%)
c [decomp-24] removed 178 variables
c [sweep-6-1] removed 178 vars (0 failed, 24 eqs, 40 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 178 vars in TOTAL (1 rounds, 186 queries)
c [phase-count-10] 487491 negative 99.5% of 489781 except 2290 0.5%
c [phase-count-10] 395672 positive 80.8% of 489781 except 94109 19.2%
c [phase-count-10] less non-negative clauses 2290 than limit 48900 (10.0%)
c [phase-count-10] non-pos/non-neg = 94109/2290 = 41.10 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 36 negative 100%
c [sort-queue-10] sorted 21477 enqueued variables after 70109 conflicts
c [score-dist-10] active 47827 (69%), one 0 (0%), zero 21477 (31%)
c [score-dist-10] max exp 518, different 13 (3%)
c [score-dist-10] median active exp 518, avg 517.4
c [simplification-10] removed 4183 variables 5.7% (69304 remain 24%)
c [simplification-10] removed 20536 irredundant clauses 4.0% (489781 remain 35%)
c [simplification-10] maximum reduction of 6% = max (6%, 4%)
c [simplification-10] large reduction 6% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 82109 (soft 72109 + delta 10000)
c [simplification-10] new conflict limit 72109 (hard 82109)
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  224.2   69303   489781     70164    9546   1560 305953  140   816   60  17%     14  302  117   91  128%
c i  224.3   69302   489781     70184    9561   1560 305953  142   817   60  17%     14  303  141   91  154%
c i  224.3   69301   489781     70187    9563   1560 305953  142   818   60  17%     14  303  141   91  154%
c i  225.2   69296   489781     70717   10056   1564 305955  142   813   60  18%      7  296  147   92  160%
c 
c [simplification-11] limit 72112 conflicts (hard 82109) hit after 72112 conflicts
c [quatres-6] found 35866 quaternary clauses 48% in total
c [ternres-7] limit 34222053 with penalty 0 = 0 + 0
c [ternres-7] all 69296 free variables schedulable
c [ternres-7] 107 ternary resolvents (0 bin, 107 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-25] removed 9 variables
c [basicprobe-4] limit 171110269 penalty 0 = 0 + 0
c [basicprobe-4-0] 15655 probes remain 23% after last round
c [basicprobe-4-0] 824 units = 809 failed (98%) + 15 lifted (2%)
c [basicprobe-4-0] removed 1455 variables, found 385997 hbrs
c [bate-2] eliminated 308 asymmetric tautologies during probing
c [unhide-11] limit 3422205 with penalty 1 = 0 + 1
c [unhide-11-13] 14 units, 460 failed, 50041 tauts, 0 hbrs, 77251 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 97 transitive binary clauses
c [transred-7] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 67218 variables 100%
c [block-4] limit of 85555134 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 97 blocked clauses
c [block-4] 97 < 1/100 * 472648 = 4726 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 67217 variables 100%
c [elim-9] limit of 684441078 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1154 variables 2% in round 1 in 48398951 steps
c [elim-9-1] backward subsumption/strengthening limit 48398900
c [elim-9-1-1] backward checking 4858 touched variables 7%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 26 and strengthened 89 clauses in 1762946 steps
c [elim-9-1] rescheduled 269 variables 0% by backward subsumption
c [elim-9-2] eliminated 33 variables 0% in round 2 in 291365 steps
c [elim-9-2] backward subsumption/strengthening limit 291300
c [elim-9-2-1] backward checking 257 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 13 and strengthened 1 clauses in 186973 steps
c [elim-9-2] rescheduled 18 variables 0% by backward subsumption
c [elim-9-3] eliminated 1 variables 0% in round 3 in 13628 steps
c [elim-9-3] backward subsumption/strengthening limit 13600
c [elim-9-3-1] backward checking 8 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 0 and strengthened 0 clauses in 13601 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 1189 = 2% variables out of 67217 scheduled
c [bca-7] limit of 10000000 steps and 932652 added (scaled 2)
c [bca-7] 113149 out of 132058 literals actually usable 86%
c [bca-7] added 115 blocked clauses in 308028 steps
c [sweep-7] limit 10266616 penalty 0 = 0 + 0
c [sweep-7-1] 2886 pos 10.1% + 25756 neg 89.9% = 28642 sched 43.4% ret 37386
c [sweep-7-1] 10300635 steps 151 queries 1665.72 avg class size
c [sweep-7-1] 1381 decisions 140 SAT calls 162.09 avg env size
c [sweep-7-1] 27629 variables remain 42% (38350 retained 58%)
c [decomp-26] removed 111 variables
c [sweep-7-1] removed 111 vars (0 failed, 12 eqs, 26 impls)
c [sweep-7] removed 111 vars in TOTAL (1 rounds, 150 queries)
c [phase-count-11] 463337 negative 99.5% of 465523 except 2186 0.5%
c [phase-count-11] 374665 positive 80.5% of 465523 except 90858 19.5%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 19459 enqueued variables after 72112 conflicts
c [score-dist-11] active 46458 (70%), one 0 (0%), zero 19459 (30%)
c [score-dist-11] max exp 518, different 13 (3%)
c [score-dist-11] median active exp 518, avg 517.5
c [simplification-11] removed 3379 variables 4.9% (65917 remain 23%)
c [simplification-11] removed 24258 irredundant clauses 5.0% (465523 remain 34%)
c [simplification-11] maximum reduction of 5% = max (5%, 5%)
c [simplification-11] large reduction 5% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 84112 (soft 74112 + delta 10000)
c [simplification-11] new conflict limit 74112 (hard 84112)
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  240.4   65916   465523     72152    8429   1812 617896  127   733   64  17%      6  211  101   92  110%
c i  241.1   65915   465523     73191    9338   1819 617903  116   631   67  18%      3  107   79   92   87%
c 
c [simplification-12] limit 74112 conflicts (hard 84112) hit after 74112 conflicts
c [ternres-8] limit 34569306 with penalty 0 = 0 + 0
c [ternres-8] all 65915 free variables schedulable
c [ternres-8] 175 ternary resolvents (0 bin, 175 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-27] removed 2 variables
c [simpleprobe-5] all 65915 free variables schedulable
c [simpleprobe-5] limit 138277226 penalty 0 = 0 + 0
c [decomp-28] removed 1310 variables
c [simpleprobe-5] 16 variables remain 0% (64589 retained 100%)
c [simpleprobe-5] removed 1310 variables, found 75787 hbrs, 554 units
c [unhide-12] limit 6913861 with penalty 0 = 0 + 0
c [unhide-12-16] 13 units, 200 failed, 89812 tauts, 0 hbrs, 78146 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 139 transitive binary clauses
c [transred-8] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 864232665 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 1 clauses out of 446 (0%) of length 8
c [cce-4-1] eliminated 10 clauses out of 647 (2%) of length 7
c [cce-4-1] eliminated 618 clauses out of 2998 (21%) of length 6
c [cce-4-1] eliminated 18617 clauses out of 27565 (68%) of length 5
c [cce-4-1] eliminated 16531 clauses out of 28632 (58%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 35777 large clauses in 485293490 steps
c [cce-4-1] allowing another 242646745 steps for small clauses
c [cce-4-1] scheduling 288116 clauses = 209781 binary + 78335 ternary
c [cce-4-1] tried to eliminate 23633 small clauses 8%
c [cce-4-1] eliminated 4675 binary clauses 2%
c [cce-4-1] eliminated 1467 ternary clauses 2%
c [cce-4-1] eliminated 6142 small clauses 2%
c [cce-4-1] eliminated 6826 small clauses in 864232682 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 42603 covered clauses in round 1
c [cce-4] eliminated 42603 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 64262 variables 100%
c [elim-10] limit of 691386133 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 14236 variables 22% in round 1 in 37825519 steps
c [elim-10-1] backward subsumption/strengthening limit 37825500
c [elim-10-1-1] backward checking 30482 touched variables 47%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 14 and strengthened 39 clauses in 4855403 steps
c [elim-10-1] rescheduled 137 variables 0% by backward subsumption
c [elim-10-2] eliminated 8 variables 0% in round 2 in 96411 steps
c [elim-10-2] backward subsumption/strengthening limit 96400
c [elim-10-2-1] backward checking 80 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 0 and strengthened 3 clauses in 96401 steps
c [elim-10-2] rescheduled 11 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 7671 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 14244 = 22% variables out of 64262 scheduled
c [bca-8] limit of 10000000 steps and 751473 added (scaled 2)
c [bca-8] 92458 out of 100038 literals actually usable 92%
c [bca-8] added 184 blocked clauses in 214066 steps
c [sweep-8] limit 10370791 penalty 0 = 0 + 0
c [sweep-8-1] 2781 pos 11.0% + 22471 neg 89.0% = 25252 sched 50.5% ret 24766
c [sweep-8-1] 10391606 steps 297 queries 1652.57 avg class size
c [sweep-8-1] 3227 decisions 269 SAT calls 108.94 avg env size
c [sweep-8-1] 23458 variables remain 47% (26479 retained 53%)
c [decomp-29] removed 144 variables
c [sweep-8-1] removed 144 vars (0 failed, 29 eqs, 49 impls)
c [sweep-8] removed 144 vars in TOTAL (1 rounds, 296 queries)
c [phase-count-12] 374036 negative 99.8% of 374705 except 669 0.2%
c [phase-count-12] 290482 positive 77.5% of 374705 except 84223 22.5%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 14143 enqueued variables after 74112 conflicts
c [score-dist-12] active 35731 (72%), one 0 (0%), zero 14143 (28%)
c [score-dist-12] max exp 518, different 10 (2%)
c [score-dist-12] median active exp 518, avg 517.5
c [simplification-12] removed 16041 variables 24.3% (49874 remain 17%)
c [simplification-12] removed 90818 irredundant clauses 19.5% (374705 remain 27%)
c [simplification-12] maximum reduction of 24% = max (24%, 20%)
c [simplification-12] large reduction 24% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 86112 (soft 76112 + delta 10000)
c [simplification-12] new conflict limit 76112 (hard 86112)
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  274.8   49873   374705     75583    4163   2968 496344  103   601   53  17%     16   73   65   92   71%
c 
c [simplification-13] limit 76112 conflicts (hard 86112) hit after 76112 conflicts
c [quatres-7] found 20528 quaternary clauses 54% in total
c [quatres-7-1] removed 4 duplicate quaternary clauses
c [quatres-7-2] added 10 single-self-subsuming ternary resolvents
c [quatres-7-2] added 11 quaternary resolvents
c [ternres-9] limit 34836250 with penalty 0 = 0 + 0
c [ternres-9] all 49863 free variables schedulable
c [ternres-9] 498 ternary resolvents (1 bin, 497 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-30] removed 11 variables
c [treelook-5] limit 3483625 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 79320 literals 80%
c [treelook-5] scheduling used 1710715 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 3483625 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 3556531 steps
c [treelook-5] 79203 literals remain 79%
c [treelook-5] 15272 variables remain to probed next time 31%
c [treelook-5] removed 29 variables, found 13686 hbrs
c [unhide-13] limit 6967250 with penalty 0 = 0 + 0
c [unhide-13-20] 2 units, 146 failed, 31765 tauts, 0 hbrs, 31136 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 140 transitive binary clauses
c [transred-9] found 4 units
c [cce-5] limit of 174181250 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 12 clauses out of 102 (12%) of length 7
c [cce-5-1] eliminated 370 clauses out of 3476 (11%) of length 6
c [cce-5-1] eliminated 2699 clauses out of 12663 (21%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 3081 large clauses in 174181256 steps
c [cce-5-1] allowing another 87090628 steps for small clauses
c [cce-5-1] scheduling 258307 clauses = 162813 binary + 95494 ternary
c [cce-5-1] tried to eliminate 2757 small clauses 1%
c [cce-5-1] eliminated 552 binary clauses 0%
c [cce-5-1] eliminated 176 ternary clauses 0%
c [cce-5-1] eliminated 728 small clauses 0%
c [cce-5-1] eliminated 1376 small clauses in 174181256 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 4457 covered clauses in round 1
c [cce-5] eliminated 4457 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 49520 variables 100%
c [elim-11] limit of 696725002 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 459 variables 1% in round 1 in 34419274 steps
c [elim-11-1] backward subsumption/strengthening limit 34419200
c [elim-11-1-1] backward checking 2807 touched variables 6%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 4 clauses in 691388 steps
c [elim-11-1] rescheduled 16 variables 0% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 6462 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 459 = 1% variables out of 49520 scheduled
c [elim-11] 459 < 1/100 * 49520 = 495 considered unsuccessful
c [bca-9] limit of 10000000 steps and 728979 added (scaled 2)
c [bca-9] 87455 out of 98124 literals actually usable 89%
c [bca-9] added 253 blocked clauses in 203443 steps
c [sweep-9] limit 10450875 penalty 0 = 0 + 0
c [sweep-9-1] 2513 pos 10.9% + 20592 neg 89.1% = 23105 sched 47.1% ret 25956
c [sweep-9-1] 10453430 steps 253 queries 1677.36 avg class size
c [sweep-9-1] 2866 decisions 236 SAT calls 83.11 avg env size
c [sweep-9-1] 21961 variables remain 45% (27075 retained 55%)
c [decomp-32] removed 90 variables
c [sweep-9-1] removed 90 vars (0 failed, 16 eqs, 28 impls)
c [sweep-9] removed 90 vars in TOTAL (1 rounds, 252 queries)
c [phase-count-13] 363019 negative 99.8% of 363643 except 624 0.2%
c [phase-count-13] 281437 positive 77.4% of 363643 except 82206 22.6%
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 13033 enqueued variables after 76112 conflicts
c [score-dist-13] active 35938 (73%), one 0 (0%), zero 13033 (27%)
c [score-dist-13] max exp 518, different 10 (2%)
c [score-dist-13] median active exp 518, avg 517.6
c [simplification-13] removed 892 variables 1.8% (48971 remain 17%)
c [simplification-13] removed 11062 irredundant clauses 3.0% (363643 remain 26%)
c [simplification-13] maximum reduction of 3% = max (2%, 3%)
c [simplification-13] geometric conflict interval increment 6250 = 25000 / 4
c [simplification-13] new conflict interval 31250
c [simplification-13] penalized conflict interval 31250 = 1 * 31250
c [simplification-13] hard conflict limit 122987 (soft 107362 + delta 15625)
c [simplification-13] new conflict limit 107362 (hard 122987)
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  285.6   48970   363643     77262    5141   3409 472331  102   628   54  16%     10   98  106   92  115%
c i  285.6   48969   363643     77263    5141   3409 472331  102   628   54  16%     10   98  105   92  115%
c i  295.6   48968   363643     92241   18393   3601 472512  100   561   76  18%    190   24  105   93  113%
c i  300.3   48967   363643     99501   24380   3675 472569   94   372   89  25%     64 -155  114   92  123%
c i  300.4   48934   363643     99594   24457   3675 472569   95   376   89  25%     56 -151  129   93  139%
c i  300.4   48933   363643     99595   24457   3675 472569   95   376   89  25%     56 -151  128   93  139%
c i  301.5   48932   363643    100907   25560   3683 472583  100   392   89  25%     -0 -132  132   93  142%
c i  302.8   48919   363643    102683   27149   3708 472599   99   445   94  22%    -13  -76  107   93  115%
c i  302.8   48917   363643    102684   27149   3708 472599   99   445   94  22%    -13  -76  106   93  115%
c i  305.1   48915   363643    105442   29483   3739 472637  102   433  105  24%     -3  -86  114   94  122%
c i  306.0   48852   363643    106182   30166   3744 472644  109   471  105  23%    -15  -47  142   94  151%
c i  307.5   48851   363643    107644   31448   3761 472662  110   485  105  23%    -17  -32  106   95  112%
c i  308.2   48848   363643    108372   32103   3772 472676  114   505  105  23%    -21  -12  111   95  117%
c 
c [simplification-14] limit 107392 conflicts (hard 122987) hit after 111338 conflicts
c [quatres-8] found 20533 quaternary clauses 58% in total
c [quatres-8-2] added 5 quaternary resolvents
c [ternres-10] limit 40890911 with penalty 0 = 0 + 0
c [ternres-10] all 48848 free variables schedulable
c [ternres-10] 256 ternary resolvents (0 bin, 256 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 1022272 penalty 3 = 3 + 0
c [gauss-4] extracted 8 xors of average arity 3.0
c [gauss-4] connected 24 occurrences of 24 variables (average 1.0)
c [gauss-4] limit 1022272 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-33] removed 6 variables
c [basicprobe-5] limit 204454556 penalty 0 = 0 + 0
c [basicprobe-5-0] 4990 probes remain 10% after last round
c [basicprobe-5-0] 680 units = 652 failed (96%) + 28 lifted (4%)
c [basicprobe-5-0] removed 1016 variables, found 551311 hbrs
c [bate-3] eliminated 1284 asymmetric tautologies during probing
c [unhide-14] limit 2044545 with penalty 2 = 0 + 2
c [unhide-14-21] 1 units, 56 failed, 83525 tauts, 0 hbrs, 416905 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 155 transitive binary clauses
c [transred-10] found 2 units
c [cce-6] limit of 204454556 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 57
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 56
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 55
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 54
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 53
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 52
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 51
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 50
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 49
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 48
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 47
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 46
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 45
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 44
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 43
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 42
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 41
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 40
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 39
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 38
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 37
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 36
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 35
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 34
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 33
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 32
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 31
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 30
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 29
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 28
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 27
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 26
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 25
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 24
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 23
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 22
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 21
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 20
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 19
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 18
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 17
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 16
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 15
c [cce-6-1] eliminated 3 clauses out of 3 (100%) 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 4 clauses out of 6 (67%) of length 9
c [cce-6-1] eliminated 3 clauses out of 7 (43%) of length 8
c [cce-6-1] eliminated 3 clauses out of 83 (4%) of length 7
c [cce-6-1] eliminated 2 clauses out of 3047 (0%) of length 6
c [cce-6-1] eliminated 64 clauses out of 9377 (1%) of length 5
c [cce-6-1] eliminated 23 clauses out of 18856 (0%) of length 4
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 226 large clauses in 204454557 steps
c [cce-6-1] allowing another 102227278 steps for small clauses
c [cce-6-1] scheduling 249486 clauses = 161626 binary + 87860 ternary
c [cce-6-1] tried to eliminate 3770 small clauses 2%
c [cce-6-1] eliminated 718 binary clauses 0%
c [cce-6-1] eliminated 200 ternary clauses 0%
c [cce-6-1] eliminated 918 small clauses 0%
c [cce-6-1] eliminated 1616 small clauses in 204454570 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 1842 covered clauses in round 1
c [cce-6] eliminated 1842 covered clauses in TOTAL during 1 rounds
c [cce-6] 1842 < 1/100 * 351724 = 3517 considered unsuccessful
c [bca-10] limit of 10000000 steps and 701070 added (scaled 2)
c [bca-10] 73777 out of 95502 literals actually usable 77%
c [bca-10] added 52 blocked clauses in 199953 steps
c [sweep-10] limit 12267273 penalty 0 = 0 + 0
c [sweep-10-1] 2556 pos 11.9% + 18965 neg 88.1% = 21521 sched 45.1% ret 26229
c [sweep-10-1] 12424718 steps 263 queries 1539.40 avg class size
c [sweep-10-1] 4062 decisions 238 SAT calls 225.26 avg env size
c [sweep-10-1] 20441 variables remain 43% (27283 retained 57%)
c [decomp-34] removed 188 variables
c [sweep-10-1] removed 188 vars (0 failed, 25 eqs, 54 impls)
c [sweep-10] removed 188 vars in TOTAL (1 rounds, 262 queries)
c [phase-count-14] 348881 negative 99.8% of 349505 except 624 0.2%
c [phase-count-14] 268980 positive 77.0% of 349505 except 80525 23.0%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-14] sorted 11403 enqueued variables after 111338 conflicts
c [score-dist-14] active 36159 (76%), one 0 (0%), zero 11403 (24%)
c [score-dist-14] max exp 518, different 10 (2%)
c [score-dist-14] median active exp 518, avg 517.8
c [simplification-14] removed 1286 variables 2.6% (47562 remain 17%)
c [simplification-14] removed 14138 irredundant clauses 3.9% (349505 remain 25%)
c [simplification-14] maximum reduction of 4% = max (3%, 4%)
c [simplification-14] geometric conflict interval increment 6250 = 31250 / 5
c [simplification-14] new conflict interval 37500
c [simplification-14] penalized conflict interval 37500 = 1 * 37500
c [simplification-14] hard conflict limit 167588 (soft 148838 + delta 18750)
c [simplification-14] new conflict limit 148838 (hard 167588)
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  333.3   47561   349505    112321   35568   5091 910055  111   502  135  22%     15  -13  117   96  122%
c i  348.2   47531   349505    129480   49964   5250 910184  108   468  135  23%    199  -27  116   98  118%
c i  350.0   47296   349505    131305   51555   5259 910193  113   469  135  24%      2  -25   86   99   87%
c i  352.6   47271   349505    133336   53329   5276 910215  124   511  168  24%    -29   17  160  100  160%
c -  353.3   47245   349505    133944   19212   5282 910218  122   518   68  24%    -38   23  137  100  136%
c i  354.3   47244   349505    135387   20462   5293 910226  114   516   76  22%    -32   21   84  100   83%
c i  359.2   47242   349505    142006   26383   5323 910265  109   501   87  22%     35    5   94  101   93%
c i  367.5   47238   349505    152612   35542   5362 910321  116   442  120  26%     93  -38  104  100  104%
c i  368.5   47237   349505    153665   36417   5373 910334  121   452  127  27%      3  -27  151  101  150%
c i  372.5   47236   349505    158019   40325   5409 910361  110   437  127  25%     -2  -42   70  101   69%
c i  375.4   47147   349505    160593   42581   5421 910395  125   492  132  25%    -25   13  177  103  172%
c i  378.8   47071   349505    164020   45623   5433 910409  120   492  139  24%    -14   11  130  104  126%
c 
c [simplification-15] limit 148838 conflicts (hard 167588) hit after 167588 conflicts
c [quatres-9] found 18671 quaternary clauses 56% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [quatres-9-2] added 1 quaternary resolvents
c [ternres-11] limit 51778969 with penalty 0 = 0 + 0
c [ternres-11] all 46962 free variables schedulable
c [ternres-11] 420 ternary resolvents (0 bin, 420 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1618092 penalty 4 = 4 + 0
c [card-5] found 1101 at-most-one constraints of average size 4.3
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1618092 for elimination
c [card-5] 1101 out of 1101 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-35] removed 608 variables
c [simpleprobe-6] 16 schedulable variables 0%
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-36] removed 407 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 407 variables, found 79560 hbrs, 174 units
c [unhide-15] limit 2588948 with penalty 2 = 0 + 2
c [unhide-15-23] 7 units, 106 failed, 92109 tauts, 0 hbrs, 1556427 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 254 transitive binary clauses
c [transred-11] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 46429 variables 100%
c [block-5] limit of 64723711 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 235 blocked clauses
c [block-5] 235 < 1/100 * 337451 = 3374 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 46424 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 842 variables 2% in round 1 in 32958171 steps
c [elim-12-1] backward subsumption/strengthening limit 32958100
c [elim-12-1-1] backward checking 4616 touched variables 10%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 7 and strengthened 35 clauses in 1372782 steps
c [elim-12-1] rescheduled 89 variables 0% by backward subsumption
c [elim-12-2] eliminated 1 variables 0% in round 2 in 236251 steps
c [elim-12-2] backward subsumption/strengthening limit 236200
c [elim-12-2-1] backward checking 28 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 0 and strengthened 0 clauses in 69601 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 843 = 2% variables out of 46424 scheduled
c [bca-11] limit of 10000000 steps and 671708 added (scaled 2)
c [bca-11] 68748 out of 91164 literals actually usable 75%
c [bca-11] added 65 blocked clauses in 190175 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 155336900 penalty 0 = 0 + 0
c [sweep-11-1] 2226 pos 11.5% + 17071 neg 88.5% = 19297 sched 42.3% ret 26284
c [sweep-11-1] 155362143 steps 4766 queries 62.84 avg class size
c [sweep-11-1] 37396 decisions 4115 SAT calls 80.48 avg env size
c [sweep-11-1] 2122 variables remain 5% (43246 retained 95%)
c [decomp-37] removed 1351 variables
c [sweep-11-1] removed 1351 vars (0 failed, 661 eqs, 1154 impls)
c [sweep-11] removed 1351 vars in TOTAL (1 rounds, 4765 queries)
c [sort-queue-15] sorted 9830 enqueued variables after 167588 conflicts
c [score-dist-15] active 34400 (78%), one 0 (0%), zero 9830 (22%)
c [score-dist-15] max exp 519, different 11 (2%)
c [score-dist-15] median active exp 519, avg 518.8
c [simplification-15] removed 2732 variables 5.8% (44230 remain 15%)
c [simplification-15] removed 16909 irredundant clauses 4.8% (332596 remain 24%)
c [simplification-15] maximum reduction of 6% = max (6%, 5%)
c [simplification-15] large reduction 6% >= 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 179588 (soft 169588 + delta 10000)
c [simplification-15] new conflict limit 169588 (hard 179588)
c 
c [simplification-16] limit 169588 conflicts (hard 179588) hit after 169590 conflicts
c [quatres-10] found 18595 quaternary clauses 54% in total
c [quatres-10-2] added 8 quaternary resolvents
c [ternres-12] limit 52239761 with penalty 0 = 0 + 0
c [ternres-12] all 44230 free variables schedulable
c [ternres-12] 491 ternary resolvents (0 bin, 491 trn)
c [ternres-12] fully completed ternary resolution
c [treelook-6] limit 5223976 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 69846 literals 79%
c [treelook-6] scheduling used 2115192 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 5223976 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 5227823 steps
c [treelook-6] 69738 literals remain 79%
c [treelook-6] 12870 variables remain to probed next time 29%
c [decomp-39] removed 2 variables
c [treelook-6] removed 15 variables, found 13574 hbrs
c [unhide-16] limit 2611988 with penalty 2 = 0 + 2
c [unhide-16-24] 3 units, 76 failed, 66735 tauts, 0 hbrs, 160428 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 190 transitive binary clauses
c [cce-7] limit of 130599404 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 111
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 110
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 109
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 108
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 107
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 106
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 105
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 104
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 103
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 102
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 101
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 100
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 99
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 98
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 97
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 96
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 95
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 94
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 93
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 92
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 91
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 90
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 89
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 88
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 87
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 86
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 85
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 84
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 83
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 82
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 81
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 80
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 79
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 78
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 77
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 76
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 75
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 74
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 73
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 72
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 71
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 70
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 69
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 68
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 67
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 66
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 65
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 64
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 63
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 62
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 61
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 60
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 59
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 58
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 57
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 56
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 55
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 54
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 53
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 52
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 51
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 50
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 49
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 48
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 47
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 46
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 45
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 44
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 43
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 42
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 41
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 40
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 39
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 38
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 37
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 36
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 35
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 34
c [cce-7-1] eliminated 5 clauses out of 9 (56%) of length 33
c [cce-7-1] eliminated 5 clauses out of 8 (62%) of length 32
c [cce-7-1] eliminated 6 clauses out of 10 (60%) of length 31
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 30
c [cce-7-1] eliminated 7 clauses out of 11 (64%) of length 29
c [cce-7-1] eliminated 6 clauses out of 10 (60%) of length 28
c [cce-7-1] eliminated 8 clauses out of 12 (67%) of length 27
c [cce-7-1] eliminated 6 clauses out of 10 (60%) of length 26
c [cce-7-1] eliminated 8 clauses out of 12 (67%) of length 25
c [cce-7-1] eliminated 6 clauses out of 10 (60%) of length 24
c [cce-7-1] eliminated 8 clauses out of 11 (73%) of length 23
c [cce-7-1] eliminated 6 clauses out of 11 (55%) of length 22
c [cce-7-1] eliminated 8 clauses out of 12 (67%) of length 21
c [cce-7-1] eliminated 6 clauses out of 11 (55%) of length 20
c [cce-7-1] eliminated 10 clauses out of 14 (71%) of length 19
c [cce-7-1] eliminated 7 clauses out of 13 (54%) of length 18
c [cce-7-1] eliminated 12 clauses out of 16 (75%) of length 17
c [cce-7-1] eliminated 8 clauses out of 14 (57%) of length 16
c [cce-7-1] eliminated 12 clauses out of 16 (75%) of length 15
c [cce-7-1] eliminated 8 clauses out of 15 (53%) of length 14
c [cce-7-1] eliminated 14 clauses out of 17 (82%) of length 13
c [cce-7-1] eliminated 9 clauses out of 17 (53%) of length 12
c [cce-7-1] eliminated 14 clauses out of 17 (82%) of length 11
c [cce-7-1] eliminated 8 clauses out of 17 (47%) of length 10
c [cce-7-1] eliminated 15 clauses out of 20 (75%) of length 9
c [cce-7-1] eliminated 10 clauses out of 23 (43%) of length 8
c [cce-7-1] eliminated 16 clauses out of 99 (16%) of length 7
c [cce-7-1] eliminated 12 clauses out of 3034 (0%) of length 6
c [cce-7-1] eliminated 27 clauses out of 9214 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 416 large clauses in 130599406 steps
c [cce-7-1] allowing another 65299703 steps for small clauses
c [cce-7-1] scheduling 234486 clauses = 155034 binary + 79452 ternary
c [cce-7-1] tried to eliminate 2315 small clauses 1%
c [cce-7-1] eliminated 401 binary clauses 0%
c [cce-7-1] eliminated 86 ternary clauses 0%
c [cce-7-1] eliminated 487 small clauses 0%
c [cce-7-1] eliminated 1388 small clauses in 130599414 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1804 covered clauses in round 1
c [cce-7] eliminated 1804 covered clauses in TOTAL during 1 rounds
c [cce-7] 1804 < 1/100 * 332048 = 3320 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 44120 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 287 variables 1% in round 1 in 34486168 steps
c [elim-13-1] backward subsumption/strengthening limit 34486100
c [elim-13-1-1] backward checking 1926 touched variables 4%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 3 and strengthened 0 clauses in 787531 steps
c [elim-13-1] rescheduled 7 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 2960 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 287 = 1% variables out of 44120 scheduled
c [elim-13] 287 < 1/100 * 44120 = 441 considered unsuccessful
c [bca-12] limit of 10000000 steps and 657586 added (scaled 2)
c [bca-12] 62979 out of 87668 literals actually usable 72%
c [bca-12] added 46 blocked clauses in 175673 steps
c [sweep-12] limit 15671928 penalty 0 = 0 + 0
c [sweep-12-1] 264 pos 17.1% + 1276 neg 82.9% = 1540 sched 3.5% ret 42293
c [sweep-12-1] 15723711 steps 1173 queries 22.71 avg class size
c [sweep-12-1] 6005 decisions 870 SAT calls 55.42 avg env size
c [sweep-12-1] 23 variables remain 0% (43810 retained 100%)
c [decomp-40] removed 349 variables
c [sweep-12-1] removed 349 vars (0 failed, 302 eqs, 295 impls)
c [sweep-12] removed 349 vars in TOTAL (1 rounds, 1172 queries)
c [sort-queue-16] sorted 9647 enqueued variables after 169590 conflicts
c [score-dist-16] active 33837 (78%), one 0 (0%), zero 9647 (22%)
c [score-dist-16] max exp 519, different 11 (2%)
c [score-dist-16] median active exp 519, avg 518.8
c [simplification-16] removed 746 variables 1.7% (43484 remain 15%)
c [simplification-16] removed 4890 irredundant clauses 1.5% (327706 remain 24%)
c [simplification-16] maximum reduction of 2% = max (2%, 1%)
c [simplification-16] geometric conflict interval increment 12500 = 37500 / 3
c [simplification-16] new conflict interval 50000
c [simplification-16] penalized conflict interval 50000 = 1 * 50000
c [simplification-16] hard conflict limit 244590 (soft 219590 + delta 25000)
c [simplification-16] new conflict limit 219590 (hard 244590)
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  415.4   43483   327706    169707   37733   5501 809341  124   544  104  23%     21   59  111  106  105%
c i  417.2   43482   327706    171413   39198   5525 809357  124   526  104  24%    -24   41  123  106  116%
c i  417.2   43477   327706    171450   39225   5531 809359  123   525  104  23%    -25   39  110  106  104%
c i  417.2   43470   327706    171469   39234   5533 809359  123   524  104  23%    -25   38  103  106   97%
c i  417.8   43415   327706    171932   39652   5536 809364  127   539  104  24%    -33   53  165  107  155%
c i  418.4   43411   327706    172442   40128   5538 809367  127   553  104  23%    -38   66  123  107  115%
c i  422.3   43409   327706    177679   44164   5548 809376   93   293  120  32%     17 -189   67  104   64%
c i  432.8   43407   327706    188993   54131   5627 809416  122   473  136  26%    106    4  109  106  103%
c i  435.8   43406   327706    191378   56284   5655 809426  135   531  153  25%    -17   61  149  108  138%
c -  436.0   43404   327706    191456   23235   5655 809426  136   534   64  25%    -20   64  152  108  141%
c i  449.6   43403   327706    207008   36864   5735 809473  126   565  102  22%    161   90  118  111  107%
c i  451.9   43400   327706    211827   41494   5739 809474   66   322  118  20%     -7 -150   39  106   37%
c 
c [simplification-17] limit 219590 conflicts (hard 244590) hit after 223752 conflicts
c [quatres-11] found 18151 quaternary clauses 53% in total
c [quatres-11-2] added 7 single-self-subsuming ternary resolvents
c [quatres-11-2] added 9 quaternary resolvents
c [ternres-13] limit 61437387 with penalty 0 = 0 + 0
c [ternres-13] all 43400 free variables schedulable
c [ternres-13] 183 ternary resolvents (0 bin, 183 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-41] removed 86 variables
c [basicprobe-6] limit 307186937 penalty 0 = 0 + 0
c [basicprobe-6-0] 5665 sched 13%, 636 failed, 31 lifted, 289000 hbrs
c [decomp-42] removed 1002 variables
c [basicprobe-6-1] 6759 probes remain 16% after last round
c [basicprobe-6-1] 918 units = 879 failed (96%) + 39 lifted (4%)
c [basicprobe-6-1] removed 1465 variables, found 432697 hbrs
c [bate-4] eliminated 814 asymmetric tautologies during probing
c [unhide-17] limit 1535934 with penalty 3 = 0 + 3
c [unhide-17-25] 1 units, 0 failed, 6934 tauts, 0 hbrs, 803710 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 361 transitive binary clauses
c [bca-13] limit of 10000000 steps and 612339 added (scaled 2)
c [bca-13] 58208 out of 83866 literals actually usable 69%
c [bca-13] added 8 blocked clauses in 177363 steps
c [sweep-13] limit 18431216 penalty 0 = 0 + 0
c [sweep-13-1] 0 pos 0.0% + 5 neg 100.0% = 5 sched 0.0% ret 41927
c [sweep-13-1] 403547 steps 5 queries 2.40 avg class size
c [sweep-13-1] 61 decisions 4 SAT calls 412.75 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-43] removed 1 variables
c [sweep-13-1] removed 1 vars (0 failed, 0 eqs, 3 impls)
c [sweep-13-2] 4001 pos 9.5% + 37930 neg 90.5% = 41931 sched 100.0% ret 0
c [sweep-13-2] 18052487 steps 352 queries 822.61 avg class size
c [sweep-13-2] 10225 decisions 345 SAT calls 353.96 avg env size
c [sweep-13-2] 25680 variables remain 61% (16222 retained 39%)
c [decomp-44] removed 36 variables
c [sweep-13-2] removed 36 vars (0 failed, 6 eqs, 20 impls)
c [sweep-13] 37 < 1/1000 * 41932 = 41 considered unsuccessful
c [sweep-13] removed 37 vars in TOTAL (2 rounds, 355 queries)
c [sort-queue-17] sorted 8456 enqueued variables after 223752 conflicts
c [score-dist-17] active 33439 (80%), one 0 (0%), zero 8456 (20%)
c [score-dist-17] max exp 519, different 11 (2%)
c [score-dist-17] median active exp 519, avg 518.9
c [simplification-17] removed 1505 variables 3.5% (41895 remain 15%)
c [simplification-17] removed 22512 irredundant clauses 6.9% (305194 remain 22%)
c [simplification-17] maximum reduction of 7% = max (3%, 7%)
c [simplification-17] large reduction 7% >= 5% limit
c [simplification-17] next conflict interval 2237 = min (223752/100, 50000)
c [simplification-17] penalized conflict interval 2237 = 1 * 2237
c [simplification-17] hard conflict limit 235989 (soft 225989 + delta 10000)
c [simplification-17] new conflict limit 225989 (hard 235989)
c 
c [simplification-18] limit 225989 conflicts (hard 235989) hit after 225992 conflicts
c [quatres-12] found 16883 quaternary clauses 52% in total
c [quatres-12-1] removed 1 duplicate quaternary clauses
c [ternres-14] limit 62008247 with penalty 0 = 0 + 0
c [ternres-14] all 41895 free variables schedulable
c [ternres-14] 135 ternary resolvents (0 bin, 135 trn)
c [ternres-14] fully completed ternary resolution
c [simpleprobe-7] all 41895 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-46] removed 181 variables
c [simpleprobe-7] 9 variables remain 0% (41705 retained 100%)
c [simpleprobe-7] removed 181 variables, found 85124 hbrs, 90 units
c [unhide-18] limit 1550206 with penalty 3 = 0 + 3
c [unhide-18-26] 0 units, 20 failed, 143316 tauts, 0 hbrs, 342202 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 327 transitive binary clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 41692 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 726 variables 2% in round 1 in 34391534 steps
c [elim-14-1] backward subsumption/strengthening limit 34391500
c [elim-14-1-1] backward checking 4036 touched variables 10%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 5 clauses in 1221544 steps
c [elim-14-1] rescheduled 14 variables 0% by backward subsumption
c [elim-14-2] no variable eliminated in round 2 in 4240 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 726 = 2% variables out of 41692 scheduled
c [bca-14] limit of 10000000 steps and 606241 added (scaled 2)
c [bca-14] 56766 out of 81934 literals actually usable 69%
c [bca-14] added 43 blocked clauses in 169085 steps
c [sort-queue-18] sorted 8150 enqueued variables after 225992 conflicts
c [score-dist-18] active 32816 (80%), one 0 (0%), zero 8150 (20%)
c [score-dist-18] max exp 519, different 11 (2%)
c [score-dist-18] median active exp 519, avg 518.9
c [simplification-18] removed 929 variables 2.2% (40966 remain 14%)
c [simplification-18] removed 2769 irredundant clauses 0.9% (302425 remain 22%)
c [simplification-18] maximum reduction of 2% = max (2%, 1%)
c [simplification-18] geometric conflict interval increment 16666 = 50000 / 3
c [simplification-18] new conflict interval 66666
c [simplification-18] penalized conflict interval 66666 = 1 * 66666
c [simplification-18] hard conflict limit 325991 (soft 292658 + delta 33333)
c [simplification-18] new conflict limit 292658 (hard 325991)
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  503.6   40965   302425    232227   51542   5821 928236  134   559  130  24%    211   95  140  110  127%
c -  511.3   40965   302425    239314   24096   5858 928260  131   552   65  24%      4   79  133  112  118%
c i  520.3   40964   302425    249791   33329   5924 928295  139   544   91  26%    155   63  168  115  146%
c -  545.2   40959   302425    279888   25803   6046 928364  129   437  101  29%    299  -37  139  117  119%
c 
c [simplification-19] limit 292658 conflicts (hard 325991) hit after 292659 conflicts
c [ternres-15] limit 74694689 with penalty 0 = 0 + 0
c [ternres-15] all 40959 free variables schedulable
c [ternres-15] 302 ternary resolvents (7 bin, 295 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 933683 penalty 4 = 4 + 0
c [gauss-5] extracted 6 xors of average arity 3.0
c [gauss-5] connected 18 occurrences of 18 variables (average 1.0)
c [gauss-5] limit 933683 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-7] limit 7469468 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 63279 literals 77%
c [treelook-7] scheduling used 1932589 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 7469468 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 7753951 steps
c [treelook-7] 63128 literals remain 77%
c [treelook-7] 11280 variables remain to probed next time 28%
c [treelook-7] removed 12 variables, found 19807 hbrs
c [unhide-19] limit 7469468 with penalty 1 = 0 + 1
c [unhide-19-29] 0 units, 14 failed, 43972 tauts, 0 hbrs, 422522 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 229 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 933683615 steps penalty 2 = 2 + 0
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 159
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 158
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 157
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 156
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 155
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 154
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 153
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 152
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 151
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 150
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 149
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 148
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 147
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 146
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 145
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 144
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 143
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 142
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 141
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 140
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 139
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 138
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 137
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 136
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 135
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 134
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 133
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 132
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 131
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 130
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 129
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 128
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 127
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 126
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 125
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 124
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 123
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 122
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 121
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 120
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 119
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 118
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 117
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 116
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 115
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 114
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 113
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 112
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 87
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 86
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 85
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 84
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 83
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 82
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 81
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 80
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 79
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 78
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 77
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 76
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 75
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 74
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 73
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 72
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 71
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 70
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 69
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 68
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 67
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 66
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 65
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 64
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 63
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 62
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 61
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 60
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 59
c [cce-8-1] eliminated 2 clauses out of 6 (33%) of length 58
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 57
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 56
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 55
c [cce-8-1] eliminated 2 clauses out of 7 (29%) of length 54
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 53
c [cce-8-1] eliminated 2 clauses out of 6 (33%) of length 52
c [cce-8-1] eliminated 3 clauses out of 7 (43%) of length 51
c [cce-8-1] eliminated 4 clauses out of 8 (50%) of length 50
c [cce-8-1] eliminated 4 clauses out of 8 (50%) of length 49
c [cce-8-1] eliminated 3 clauses out of 8 (38%) of length 48
c [cce-8-1] eliminated 4 clauses out of 8 (50%) of length 47
c [cce-8-1] eliminated 2 clauses out of 7 (29%) of length 46
c [cce-8-1] eliminated 3 clauses out of 8 (38%) of length 45
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 44
c [cce-8-1] eliminated 3 clauses out of 11 (27%) of length 43
c [cce-8-1] eliminated 3 clauses out of 8 (38%) of length 42
c [cce-8-1] eliminated 3 clauses out of 9 (33%) of length 41
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 40
c [cce-8-1] eliminated 3 clauses out of 9 (33%) of length 39
c [cce-8-1] eliminated 3 clauses out of 8 (38%) of length 38
c [cce-8-1] eliminated 3 clauses out of 9 (33%) of length 37
c [cce-8-1] eliminated 5 clauses out of 11 (45%) of length 36
c [cce-8-1] eliminated 7 clauses out of 12 (58%) of length 35
c [cce-8-1] eliminated 5 clauses out of 12 (42%) of length 34
c [cce-8-1] eliminated 6 clauses out of 13 (46%) of length 33
c [cce-8-1] eliminated 6 clauses out of 15 (40%) of length 32
c [cce-8-1] eliminated 8 clauses out of 16 (50%) of length 31
c [cce-8-1] eliminated 7 clauses out of 16 (44%) of length 30
c [cce-8-1] eliminated 8 clauses out of 16 (50%) of length 29
c [cce-8-1] eliminated 10 clauses out of 18 (56%) of length 28
c [cce-8-1] eliminated 10 clauses out of 20 (50%) of length 27
c [cce-8-1] eliminated 10 clauses out of 19 (53%) of length 26
c [cce-8-1] eliminated 10 clauses out of 20 (50%) of length 25
c [cce-8-1] eliminated 9 clauses out of 18 (50%) of length 24
c [cce-8-1] eliminated 10 clauses out of 20 (50%) of length 23
c [cce-8-1] eliminated 9 clauses out of 17 (53%) of length 22
c [cce-8-1] eliminated 11 clauses out of 22 (50%) of length 21
c [cce-8-1] eliminated 11 clauses out of 22 (50%) of length 20
c [cce-8-1] eliminated 12 clauses out of 22 (55%) of length 19
c [cce-8-1] eliminated 10 clauses out of 22 (45%) of length 18
c [cce-8-1] eliminated 13 clauses out of 22 (59%) of length 17
c [cce-8-1] eliminated 11 clauses out of 24 (46%) of length 16
c [cce-8-1] eliminated 13 clauses out of 23 (57%) of length 15
c [cce-8-1] eliminated 12 clauses out of 26 (46%) of length 14
c [cce-8-1] eliminated 14 clauses out of 26 (54%) of length 13
c [cce-8-1] eliminated 15 clauses out of 32 (47%) of length 12
c [cce-8-1] eliminated 17 clauses out of 29 (59%) of length 11
c [cce-8-1] eliminated 16 clauses out of 34 (47%) of length 10
c [cce-8-1] eliminated 20 clauses out of 35 (57%) of length 9
c [cce-8-1] eliminated 22 clauses out of 48 (46%) of length 8
c [cce-8-1] eliminated 30 clauses out of 130 (23%) of length 7
c [cce-8-1] eliminated 29 clauses out of 3060 (1%) of length 6
c [cce-8-1] eliminated 93 clauses out of 8648 (1%) of length 5
c [cce-8-1] eliminated 1797 clauses out of 15973 (11%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 2442 large clauses in 392334194 steps
c [cce-8-1] allowing another 196167097 steps for small clauses
c [cce-8-1] scheduling 201241 clauses = 146344 binary + 54897 ternary
c [cce-8-1] tried to eliminate 33999 small clauses 17%
c [cce-8-1] eliminated 4955 binary clauses 3%
c [cce-8-1] eliminated 1062 ternary clauses 2%
c [cce-8-1] eliminated 6017 small clauses 3%
c [cce-8-1] eliminated 6017 small clauses in 933683621 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 8459 covered clauses in round 1
c [cce-8] eliminated 8459 covered clauses in TOTAL during 1 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 40932 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 384 variables 1% in round 1 in 29854828 steps
c [elim-15-1] backward subsumption/strengthening limit 29854800
c [elim-15-1-1] backward checking 2986 touched variables 7%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 3 and strengthened 11 clauses in 855197 steps
c [elim-15-1] rescheduled 24 variables 0% by backward subsumption
c [elim-15-2] eliminated 2 variables 0% in round 2 in 15484 steps
c [elim-15-2] backward subsumption/strengthening limit 15400
c [elim-15-2-1] backward checking 16 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 1 and strengthened 3 clauses in 15401 steps
c [elim-15-2] rescheduled 8 variables 0% by backward subsumption
c [elim-15-3] no variable eliminated in round 3 in 13853 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 386 = 1% variables out of 40932 scheduled
c [elim-15] 386 < 1/100 * 40932 = 409 considered unsuccessful
c [bca-15] limit of 10000000 steps and 579505 added (scaled 2)
c [bca-15] 57207 out of 81094 literals actually usable 71%
c [bca-15] added 66 blocked clauses in 157508 steps
c [sweep-14] limit 11204203 penalty 1 = 1 + 0
c [sweep-14-1] 3764 pos 15.1% + 21181 neg 84.9% = 24945 sched 61.5% ret 15601
c [sweep-14-1] 11303608 steps 284 queries 1033.31 avg class size
c [sweep-14-1] 4712 decisions 277 SAT calls 172.75 avg env size
c [sweep-14-1] 22630 variables remain 56% (17903 retained 44%)
c [decomp-49] removed 20 variables
c [sweep-14-1] removed 20 vars (0 failed, 6 eqs, 21 impls)
c [sweep-14] 20 < 1/1000 * 40546 = 40 considered unsuccessful
c [sweep-14] removed 20 vars in TOTAL (1 rounds, 283 queries)
c [sort-queue-19] sorted 7877 enqueued variables after 292659 conflicts
c [score-dist-19] active 32649 (81%), one 0 (0%), zero 7877 (19%)
c [score-dist-19] max exp 520, different 12 (2%)
c [score-dist-19] median active exp 520, avg 519.6
c [simplification-19] removed 433 variables 1.1% (40526 remain 14%)
c [simplification-19] removed 13514 irredundant clauses 4.5% (288911 remain 21%)
c [simplification-19] maximum reduction of 4% = max (1%, 4%)
c [simplification-19] geometric conflict interval increment 13333 = 66666 / 5
c [simplification-19] new conflict interval 79999
c [simplification-19] penalized conflict interval 79999 = 1 * 79999
c [simplification-19] hard conflict limit 412657 (soft 372658 + delta 39999)
c [simplification-19] new conflict limit 372658 (hard 412657)
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 -  610.4   40526   288911    324017   26128   7086 891585  134   419   64  32%    654  -58  145  124  117%
c i  640.9   40525   288911    361542   57036   7184 891624  144   526  191  27%    815   80  152  126  121%
c -  646.3   40523   288911    367094   27544   7204 891633  138   463   99  30%   -790   12  179  126  142%
c i  654.1   40522   288911    376835   35799   7238 891655  140   471  129  30%   -546   16  154  128  121%
c -  683.7   40519   288911    408263   27180   7317 891697  154   603   98  26%    -98  127  162  132  123%
c 
c [simplification-20] limit 372658 conflicts (hard 412657) hit after 412660 conflicts
c [quatres-13] found 15907 quaternary clauses 48% in total
c [quatres-13-1] removed 1 duplicate quaternary clauses
c [quatres-13-2] added 4 single-self-subsuming ternary resolvents
c [quatres-13-2] added 1 quaternary resolvents
c [ternres-16] limit 95216388 with penalty 0 = 0 + 0
c [ternres-16] all 40519 free variables schedulable
c [ternres-16] 377 ternary resolvents (5 bin, 372 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-50] removed 7 variables
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 7073 sched 18%, 337 failed, 12 lifted, 142356 hbrs
c [decomp-51] removed 600 variables
c [basicprobe-7-1] 1197 probes remain 3% after last round
c [basicprobe-7-1] 568 units = 542 failed (95%) + 26 lifted (5%)
c [basicprobe-7-1] removed 864 variables, found 229442 hbrs
c [bate-5] eliminated 532 asymmetric tautologies during probing
c [unhide-20] limit 9521638 with penalty 1 = 0 + 1
c [unhide-20-32] 0 units, 0 failed, 88340 tauts, 0 hbrs, 169295 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 254 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 39655 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 74 blocked clauses
c [block-6] 74 < 1/100 * 278114 = 2781 considered unsuccessful
c [bca-16] limit of 10000000 steps and 557526 added (scaled 2)
c [bca-16] 56062 out of 79312 literals actually usable 71%
c [bca-16] added 34 blocked clauses in 151391 steps
c [sort-queue-20] sorted 7090 enqueued variables after 412660 conflicts
c [score-dist-20] active 32565 (82%), one 0 (0%), zero 7090 (18%)
c [score-dist-20] max exp 520, different 12 (2%)
c [score-dist-20] median active exp 520, avg 519.8
c [simplification-20] removed 864 variables 2.1% (39655 remain 14%)
c [simplification-20] removed 10871 irredundant clauses 3.8% (278040 remain 20%)
c [simplification-20] maximum reduction of 4% = max (2%, 4%)
c [simplification-20] geometric conflict interval increment 15999 = 79999 / 5
c [simplification-20] new conflict interval 95998
c [simplification-20] penalized conflict interval 95998 = 1 * 95998
c [simplification-20] hard conflict limit 556657 (soft 508658 + delta 47999)
c [simplification-20] new conflict limit 508658 (hard 556657)
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 -  738.3   39655   278040    452724   28297   7234 931738  148   544   63  27%    455   46  160  137  117%
c -  776.3   39655   278040    497924   29287   7327 931779  143   460   98  31%    738  -36  169  142  119%
c 
c [simplification-21] limit 508658 conflicts (hard 556657) hit after 509619 conflicts
c [quatres-14] found 15416 quaternary clauses 48% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [quatres-14-2] added 1 quaternary resolvents
c [ternres-17] limit 111329481 with penalty 0 = 0 + 0
c [ternres-17] all 39655 free variables schedulable
c [ternres-17] 41 ternary resolvents (5 bin, 36 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 3479046 penalty 4 = 4 + 0
c [card-6] found 2552 at-most-one constraints of average size 4.1
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 3479046 for elimination
c [card-6] 2552 out of 2552 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-52] removed 1 variables
c [simpleprobe-8] 8 schedulable variables 0%
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-53] removed 16 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 16 variables, found 22438 hbrs, 8 units
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 285 transitive binary clauses
c [cce-9] limit of 278323703 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 161
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 160
c [cce-9-1] eliminated 2 clauses out of 10 (20%) of length 33
c [cce-9-1] eliminated 1 clauses out of 9 (11%) of length 32
c [cce-9-1] eliminated 2 clauses out of 11 (18%) of length 31
c [cce-9-1] eliminated 1 clauses out of 11 (9%) of length 30
c [cce-9-1] eliminated 1 clauses out of 15 (7%) of length 20
c [cce-9-1] eliminated 3 clauses out of 11 (27%) of length 19
c [cce-9-1] eliminated 3 clauses out of 19 (16%) of length 18
c [cce-9-1] eliminated 1 clauses out of 12 (8%) of length 17
c [cce-9-1] eliminated 2 clauses out of 20 (10%) of length 16
c [cce-9-1] eliminated 5 clauses out of 17 (29%) of length 15
c [cce-9-1] eliminated 3 clauses out of 22 (14%) of length 14
c [cce-9-1] eliminated 5 clauses out of 18 (28%) of length 13
c [cce-9-1] eliminated 4 clauses out of 26 (15%) of length 12
c [cce-9-1] eliminated 5 clauses out of 20 (25%) of length 11
c [cce-9-1] eliminated 5 clauses out of 21 (24%) of length 10
c [cce-9-1] eliminated 6 clauses out of 25 (24%) of length 9
c [cce-9-1] eliminated 6 clauses out of 30 (20%) of length 8
c [cce-9-1] eliminated 6 clauses out of 114 (5%) of length 7
c [cce-9-1] eliminated 7 clauses out of 3052 (0%) of length 6
c [cce-9-1] eliminated 62 clauses out of 8446 (1%) of length 5
c [cce-9-1] eliminated 35 clauses out of 13766 (0%) of length 4
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 168 large clauses in 278323706 steps
c [cce-9-1] allowing another 139161853 steps for small clauses
c [cce-9-1] scheduling 203139 clauses = 140760 binary + 62379 ternary
c [cce-9-1] tried to eliminate 5900 small clauses 3%
c [cce-9-1] eliminated 885 binary clauses 1%
c [cce-9-1] eliminated 126 ternary clauses 0%
c [cce-9-1] eliminated 1011 small clauses 0%
c [cce-9-1] eliminated 1011 small clauses in 278323714 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 1179 covered clauses in round 1
c [cce-9] eliminated 1179 covered clauses in TOTAL during 1 rounds
c [cce-9] 1179 < 1/100 * 277886 = 2778 considered unsuccessful
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 39638 variables 100%
c [elim-16] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 455 variables 1% in round 1 in 27733072 steps
c [elim-16-1] backward subsumption/strengthening limit 27733000
c [elim-16-1-1] backward checking 3035 touched variables 8%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 0 and strengthened 4 clauses in 776760 steps
c [elim-16-1] rescheduled 10 variables 0% by backward subsumption
c [elim-16-2] eliminated 1 variables 0% in round 2 in 5388 steps
c [elim-16-2] backward subsumption/strengthening limit 5300
c [elim-16-2-1] backward checking 12 touched variables 0%
c [elim-16-2-1] incomplete backward checking 0 remain 0%
c [elim-16-2] subsumed 0 and strengthened 0 clauses in 5301 steps
c [elim-16-2] fully rescheduled 39182 variables 99%
c [elim-16-3] eliminated 5 variables 0% in round 3 in 27983850 steps
c [elim-16-3] backward subsumption/strengthening limit 27983800
c [elim-16-3-1] backward checking 53 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 0 and strengthened 0 clauses in 65890 steps
c [elim-16] fully completed in 3 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 461 = 1% variables out of 39638 scheduled
c [bca-17] limit of 10000000 steps and 554181 added (scaled 2)
c [bca-17] 53967 out of 78356 literals actually usable 69%
c [bca-17] added 48 blocked clauses in 153360 steps
c [sort-queue-21] sorted 6897 enqueued variables after 509619 conflicts
c [score-dist-21] active 32280 (82%), one 0 (0%), zero 6897 (18%)
c [score-dist-21] max exp 520, different 12 (2%)
c [score-dist-21] median active exp 520, avg 519.8
c [simplification-21] removed 478 variables 1.2% (39177 remain 14%)
c [simplification-21] removed 1681 irredundant clauses 0.6% (276359 remain 20%)
c [simplification-21] maximum reduction of 1% = max (1%, 1%)
c [simplification-21] geometric conflict interval increment 47999 = 95998 / 2
c [simplification-21] new conflict interval 143997
c [simplification-21] penalized conflict interval 143997 = 1 * 143997
c [simplification-21] hard conflict limit 725614 (soft 653616 + delta 71998)
c [simplification-21] new conflict limit 653616 (hard 725614)
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 -  820.5   39177   276359    542952   31773   7239 878849  119   416   65  29%    880  -35  174  127  137%
c -  862.6   39177   276359    588211   29940   7351 878889  154   496   96  31%    952   51  163  136  120%
c -  906.4   39177   276359    636742   30973   7437 878930  161   538   97  30%    990   89  172  142  121%
c 
c [simplification-22] limit 653616 conflicts (hard 725614) hit after 653616 conflicts
c [quatres-15] found 15849 quaternary clauses 47% in total
c [ternres-18] limit 134975103 with penalty 0 = 0 + 0
c [ternres-18] all 39177 free variables schedulable
c [ternres-18] 101 ternary resolvents (5 bin, 96 trn)
c [ternres-18] fully completed ternary resolution
c [treelook-8] limit 13497510 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 60006 literals 77%
c [treelook-8] scheduling used 1751457 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 13497510 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 13512272 steps
c [treelook-8] 59799 literals remain 76%
c [treelook-8] 10662 variables remain to probed next time 27%
c [treelook-8] removed 1 variables, found 33729 hbrs
c [unhide-21] limit 2500000 with penalty 3 = 1 + 2
c [unhide-21-34] 0 units, 2 failed, 33171 tauts, 0 hbrs, 1508274 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 207 transitive binary clauses
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 39171 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 20 variables 0% in round 1 in 27834171 steps
c [elim-17-1] backward subsumption/strengthening limit 27834100
c [elim-17-1-1] backward checking 192 touched variables 0%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 93314 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 20 = 0% variables out of 39171 scheduled
c [elim-17] 20 < 1/100 * 39171 = 391 considered unsuccessful
c [bca-18] limit of 10000000 steps and 552359 added (scaled 2)
c [bca-18] 53025 out of 78304 literals actually usable 68%
c [bca-18] added 26 blocked clauses in 159001 steps
c [sweep-15] limit 10123132 penalty 2 = 2 + 0
c [sweep-15-1] 3467 pos 15.6% + 18740 neg 84.4% = 22207 sched 56.7% ret 16944
c [sweep-15-1] 10123500 steps 363 queries 1003.33 avg class size
c [sweep-15-1] 6668 decisions 359 SAT calls 136.89 avg env size
c [sweep-15-1] 19834 variables remain 51% (19314 retained 49%)
c [decomp-56] removed 6 variables
c [sweep-15-1] removed 6 vars (0 failed, 3 eqs, 33 impls)
c [sweep-15] 6 < 1/1000 * 39151 = 39 considered unsuccessful
c [sweep-15] removed 6 vars in TOTAL (1 rounds, 362 queries)
c [sort-queue-22] sorted 6782 enqueued variables after 653616 conflicts
c [score-dist-22] active 32363 (83%), one 0 (0%), zero 6782 (17%)
c [score-dist-22] max exp 521, different 13 (2%)
c [score-dist-22] median active exp 521, avg 520.7
c [simplification-22] removed 32 variables 0.1% (39145 remain 14%)
c [simplification-22] removed 951 irredundant clauses 0.3% (275408 remain 20%)
c [simplification-22] maximum reduction of 0% = max (0%, 0%)
c [simplification-22] full geometric conflict interval increment 143997
c [simplification-22] new conflict interval 287994
c [simplification-22] penalized conflict interval 287994 = 1 * 287994
c [simplification-22] hard conflict limit 1085607 (soft 941610 + delta 143997)
c [simplification-22] new conflict limit 941610 (hard 1085607)
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 -  960.0   39145   275408    684486   33526   7507 878768   62   206   66  30%   1007 -230   44  131   34%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 3092 basic ate = 2971 trn 96% + 121 lrg 4% in 5 updates
c bcas: 18 count, 2000 added (302 skipped), 4582603 steps
c bkwd: tried 449391 clauses, 898587 lits, 2.00 lits/clause
c bkwd: checked 14384998 occs, 32.01 occs/clause, 16.01 occs/lit
c bkwd: subsumed 3 binary, 120 ternary, 21 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 807 large (0% self)
c blkd: 6 bces, 11140 removed, 9237704 resolutions, 25758385 steps
c blkd: 16541 blocking literals 3%, 7 pure
c bump: 723763 bumped seen, 474757640 lits 656.0 on average
c card: 6 count, 0 units, 0 am1, 305683374 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 49915 subsumed
c card: 24011 at-most-one constraints found, average size 4.69
c card: 24011 at-most-one constraints used 100%, average size 4.69
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: 9 cces, 62897 eliminated, 62373 ate 99%, 524 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: 161 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 56 decompositions, 77470 equivalent 26%
c deco: 101573 decision-only clauses 14%, 67% reduction
c decs: 16495359 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 17 elims, 92426 eliminated 31%, 135 pure 0%
c elms: 37 rounds, 2.2 rounds/bve
c elms: 61898 small 67%, 30386 large 33%
c elms: 196949 tried small, 61898 succeeded 31%, 135051 failed 69%
c elms: 55103 subsumed, 115432 strengthened, 1470 blocked
c elms: 22592641 copies, 21960094 resolutions, 5761045 ipos
c elms: 7102858 subchks, 5518057 strchks
c gaus: 5 extractions, 204 extracted, 2.3 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 13701350 steps, 6850675 extr 50%, 1232 elim 0%
c glue: 127.2 orig avg, 127.2 real avg, 8.2 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 2655191 = 339243 simple 13% + 2269534 trn 85% + 46414 lrg 2%, 4559 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 723763 clauses, 449.5 length
c lrnd: 325317743 lits = 418638292 orig - 93320549 removed 22%
c lrnd: 341361 uips 47%, 330609 flips 46%
c mins: 554598 mins 83%, 3026 bin 0%, 7558 size 1%
c mins: 505082660 poisoned searches, 114577898 hits, 23% hit rate
c mins: 563470787 used twice searches, 26046565 hits, 5% hit rate
c move: moved 33450, 23291 bin 70%, 10159 trn 30%
c otfs: 3293 driving 28%, 8639 restarting 72%
c otfs: str 11932, 11766 red 99%, 166 irr 1%
c otfs: str 11932, 0 bin 0%, 105 trn 1%, 11827 lrg 99%
c otfs: sub 21, 21 red 100%, 0 irr 0%
c otfs: sub 21, 0 bin 0%, 1 trn 5%, 20 lrg 95%
c phas: 14 computed, 114292 set, 1 pos (0%), 114291 neg (100%)
c prbs: 7 basic, 85349 probed, 3365 failed, 120 lifted
c prbs: 8 simple, 831662 probed, 1119 failed, 2488 eqs
c prbs: 8 treelook, 578 probed, 46 failed, 0 lifted
c prom: 55529 locked 11% out of 486796 tried
c prps: 1623348781 props, 92 props/dec
c prps: 93% srch, 7% simp, 0% lkhd
c quat: 15 count, 43 quat, 25 self1, 0 self2, 4235 dup
c queu: 22 sorted, 16495359 next (8837 steps 0.00)
c queu: 475687405 enq (4926959943 steps 10.36), 474757640 deq 100%
c redc: 4660 clauses 34%, 13805 tried 2%, 66 sat 0%
c redc: 11456 lits 9%, 120638 tried 0%, 66 sat 0%
c redc: 508 times jump level reduced, 82.1 levels on average
c reds: 14 count, 51728.2 conflicts per reduce
c reds: 0 memlim 0%, 14 arith 100%
c reds: 395925 collected 79%, 103793 retired 21%
c rmbd: 46712 removed, 11945 red 26%
c rsts: 17831 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: 22 count, 20 confs 91%, 0 vars 0%
c simp: 1 its 5%, 1 bin 5%, 0 trns 0%
c subl: 723763 count (880057 tried 1.2), 96892 sub out of 715125 (13.5%)
c swps: 15 count, 16 rounds, 9577 queries (598.6/round)
c swps: 8339 sat calls, 48 unsat (0.3% success rate)
c swps: 93714 decisions 11.2, 2861 conflicts 0.3
c swps; 596.2 avg class size, 106.3 avg environment size
c swps: 0 failed, 2072 impls, 1267 equivs
c swp0: 3188 type 0 queries, 1813 unsat (56.9%), 2700 sat (84.7%)
c swp1: 6389 type 1 queries, 3861 unsat (60.4%), 5610 sat (87.8%)
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: 34438888 calls to obtain time
c tops: 89859 fixed 30%, 223 its, 3247.51 confs/it
c trds: 18 transitive reductions, 3578 removed, 22 failed
c trds: 17778 nodes, 57330 edges, 35610657 steps
c trim: 1410514 words, 5.4 MB
c trnr: 18 count, 23 bin, 3427 trn, 247938211 steps
c unhd: 21 count, 34 rounds, 110794107 steps
c unhd: 1166 non-trivial sccs of average size 2.1
c unhd: 71 units, 71 bin, 0 trn, 0 lrg
c unhd: 3017 failed, 2848 stamp, 0 lits, 77 bin, 12 trn, 0 lrg
c unhd: 841811 tauts, 26679 bin 3%, 8805 trn 1%, 638 lrg 0%
c unhd: 841811 tauts, 805689 stamp 96%, 777858 red 92%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 6602919 str, 71 bin 0%, 2691 trn 0%, 6600157 lrg 100%, 6572947 red 100%
c vars: 39145 remaining 13% and 259755 removed 87% out of 298900
c vars: 89859 fixed 30%, 92426 eliminated 31%, 77470 equivalent 26%
c vsts: 15753226693 visits, 93% srch, 7% simp, 0% lkhd
c vsts: 9.7 search visits per propagation, 20212.7 per conflict
c wchs: 2148452421 pushed, 64897408 enlarged, 239 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         715168        395925        103793      40091857       4404023        271435
c 
c  0 0         11569   2       440   0         0   0   9946490  25    379506   9     13593   5     0.4
c  1 5          2751   0       373   0       755   1   2111705   5    112091   3      3334   1     0.1
c  2 6          8924   1      2079   1      1918   2   4663827  12    294938   7     10117   4     0.6
c  3 9         22331   3      9418   2      3555   3   6226096  16<   591045  13     24916   9     2.0
c  4 14        42060   6     24692   6      5400   5   5552747  14    681500  15     38049  14     3.9
c  5 21        56446   8     36443   9      7261   7   3873215  10    573079  13<    35954  13     6.0
c  6 30        65741   9     44559  11      7938   8   2780403   7    456718  10     32588  12<   11.5
c  7 41        70913  10     49160  12      8245   8   1940767   5    376856   9     27718  10    20.4
c  8 54        72913  10<    51905  13<     8503   8    972354   2    240106   5     20007   7    23.9
c  9 69        68140  10     48552  12      8470   8<   722353   2    200223   5     17548   6    23.0
c 10 86        79486  11     53373  13     13113  13    670943   2    197505   4     18235   7    13.4
c 11 126       95302  13     46221  12     16273  16    416089   1    167298   4     17510   6    15.7
c 12 230       92517  13     24778   6     14973  14    178384   0    112239   3     10559   4    14.7
c 13 534       26051   4      3928   1      7378   7     36456   0     20909   0      1305   0     8.7
c 14 1526         24   0         4   0        11   0        28   0        10   0         2   0     0.1
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                  8.3           8.0           8.8           3.2           5.1           6.1
c std                  3.0           2.5           3.0           2.8           3.1           3.1
c 
c  158.285  16% bump
c   71.865   7% probe
c   67.435   7% cce
c   47.322   5% unhide
c   26.666   3% sweep
c   21.811   2% elim
c   10.407   1% decide
c    4.499   0% bca
c 
c   10.406 < 1% rest (below)
c 
c    3.263   0% block
c    2.408   0% transred
c    1.750   0% gauss
c    1.717   0% ternres
c    0.755   0% quatres
c    0.513   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    4.722   0% preprocessing     2%
c  260.109  26% inprocessing     98%
c ==================================
c  264.831  27% simplifying
c  734.425  73% search
c ==================================
c  999.263 100% all
c 
c        724195 conflicts,         724.7 confs/sec
c          3946 ternaries,         183.5 confs/ternary
c          3694 binaries,          196.0 confs/binary
c           223 iterations,       3247.5 confs/iteration
c 
c            14 reductions,          0.0 redus/sec,  51728.2 confs/reduction
c         17831 restarts,           17.8 rests/sec,     40.6 confs/restart
c      16495359 decisions,       16507.5 decis/sec,     22.8 decis/conflict
c    1623348781 propagations,  1624546.5 props/sec,     98.4 props/decision
c 
c 999.3 seconds, 242.6 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
