c launch: /data/cnf/sc2014/app/dated-10-17-u.cnf.bz2
c host: atom26
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 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 fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/dated-10-17-u.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/dated-10-17-u.cnf.bz2
c no embedded options
c found 'p cnf 229544 1070757' header
c read 229544 variables, 1070757 clauses, 2471122 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 --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 219948 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 
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  219948  1051601         0       0      0     0    0     0   53   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 8728 at-most-one constraints of average size 5.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 8728 out of 8728 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 108248 variables
c [simpleprobe-1] all 121296 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 81213 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 81213 variables, found 15936 hbrs, 1687 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 2 units, 833 failed, 14136 tauts, 0 hbrs, 1203 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 38854 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 13368 variables 34% in round 1 in 18985445 steps
c [elim-1-1] backward subsumption/strengthening limit 1014555
c [elim-1-1-1] backward checking 23632 touched variables 61%
c [elim-1-1-1] incomplete backward checking 18135 remain 77%
c [elim-1-1] subsumed 90 and strengthened 273 clauses in 1014589 steps
c [elim-1] incomplete 684 not tried 2% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 13502 = 35% variables out of 38854 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 200172 negative 99.1% of 202008 except 1836 0.9%
c [phase-count-1] 173023 positive 85.7% of 202008 except 28985 14.3%
c [phase-count-1] less non-negative clauses 1836 than limit 20200 (10.0%)
c [phase-count-1] non-pos/non-neg = 28985/1836 = 15.79 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 25352 negative 100%
c [sort-queue-1] sorted 25352 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 25352 (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 151707 variables 85.7% (25352 remain 12%)
c [simplification-1] removed 849593 irredundant clauses 80.8% (202008 remain 19%)
c [simplification-1] maximum reduction of 86% = max (86%, 81%)
c [simplification-1] large reduction 86% >= 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    2.4   25351   202008         1       0      0  9216    0     0   18   0%      0    0    0    0    0%
c i    2.4   25247   202008        23      14      2  9216    0     0   18  39%      0    0    0    0 24444%
c i    2.4   25246   202008       200     161     10  9222    0     1   18  31%      0    1    4    0 17662%
c i    2.5   25242   202008       246     197     12  9226    0     2   18  30%      0    2    5    0 16413%
c i    2.6   25240   202008       499     420     18  9240    1     5   18  27%      1    5   13    0 14122%
c i    2.6   25236   202008       558     468     22  9244    2     6   18  27%      1    6   12    0 12115%
c i    2.7   25231   202008       654     556     24  9246    2     7   18  26%      1    7   12    0 10378%
c i    2.7   25226   202008       730     617     25  9252    2     7   18  28%      1    7   12    0 9028%
c i    2.7   25223   202008       778     649     28  9253    2     8   19  29%      1    8   17    0 10456%
c i    2.8   25222   202008       812     678     29  9256    3     9   19  30%      1    9   19    0 10566%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 156 variables
c [simpleprobe-2] all 25196 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 577 variables
c [simpleprobe-2] 17669 variables remain 72% (6950 retained 28%)
c [simpleprobe-2] removed 577 variables, found 2699 hbrs, 178 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 32209 literals 65%
c [treelook-1] scheduling used 300037 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 390324 steps
c [treelook-1] 32186 literals remain 65%
c [treelook-1] 23974 variables remain to probed next time 97%
c [treelook-1] removed 9 variables, found 3179 hbrs
c [basicprobe-1] limit 1551224 based on 193903 irredundant clauses
c [basicprobe-1-0] 2825 probes remain 11% after last round
c [basicprobe-1-0] 15 units = 15 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 37 variables, found 7066 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 7 units, 571 failed, 6221 tauts, 0 hbrs, 3491 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 23822 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 902 variables 4% in round 1 in 15623873 steps
c [elim-2-1] backward subsumption/strengthening limit 4376127
c [elim-2-1-1] backward checking 4102 touched variables 17%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 43 and strengthened 68 clauses in 838294 steps
c [elim-2-1] rescheduled 247 variables 1% by backward subsumption
c [elim-2-2] eliminated 43 variables 0% in round 2 in 143909 steps
c [elim-2-2] backward subsumption/strengthening limit 143900
c [elim-2-2-1] backward checking 210 touched variables 1%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 18 and strengthened 16 clauses in 72651 steps
c [elim-2-2] rescheduled 70 variables 0% by backward subsumption
c [elim-2-3] eliminated 14 variables 0% in round 3 in 39210 steps
c [elim-2-3] backward subsumption/strengthening limit 39200
c [elim-2-3-1] backward checking 80 touched variables 0%
c [elim-2-3-1] incomplete backward checking 0 remain 0%
c [elim-2-3] subsumed 12 and strengthened 2 clauses in 39201 steps
c [elim-2] incomplete 27 not tried 0% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 1033 = 4% variables out of 23822 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 179829 negative 99.1% of 181442 except 1613 0.9%
c [phase-count-2] 151811 positive 83.7% of 181442 except 29631 16.3%
c [phase-count-2] less non-negative clauses 1613 than limit 18100 (10.0%)
c [phase-count-2] non-pos/non-neg = 29631/1613 = 18.37 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 351 negative 100%
c [sort-queue-2] sorted 22789 enqueued variables after 812 conflicts
c [score-dist-2] active 0 (0%), one 8297 (36%), zero 14492 (64%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 2431 variables 9.6% (22789 remain 10%)
c [simplification-2] removed 20566 irredundant clauses 10.2% (181442 remain 17%)
c [simplification-2] maximum reduction of 10% = max (10%, 10%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1010 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    4.0   22788   181442       997     776     25 11010    3    12   17  30%      1   12   20    0 8488%
c 
c [simplification-3] limit 1010 conflicts (hard 11000) hit after 1012 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4966 at-most-one constraints of average size 3.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4966 out of 4966 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 31 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 31981 literals 70%
c [treelook-2] scheduling used 300006 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 363396 steps
c [treelook-2] 31965 literals remain 70%
c [treelook-2] 22079 variables remain to probed next time 97%
c [treelook-2] removed 7 variables, found 3331 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 1 units, 304 failed, 8574 tauts, 0 hbrs, 1121 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 22440 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 473 variables 2% in round 1 in 14203266 steps
c [elim-3-1] backward subsumption/strengthening limit 5796734
c [elim-3-1-1] backward checking 2507 touched variables 11%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 41 and strengthened 28 clauses in 506603 steps
c [elim-3-1] rescheduled 147 variables 1% by backward subsumption
c [elim-3-2] eliminated 23 variables 0% in round 2 in 94727 steps
c [elim-3-2] backward subsumption/strengthening limit 94700
c [elim-3-2-1] backward checking 118 touched variables 1%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 10 and strengthened 1 clauses in 43029 steps
c [elim-3-2] rescheduled 25 variables 0% by backward subsumption
c [elim-3-3] eliminated 4 variables 0% in round 3 in 18846 steps
c [elim-3-3] backward subsumption/strengthening limit 18800
c [elim-3-3-1] backward checking 20 touched variables 0%
c [elim-3-3-1] incomplete backward checking 0 remain 0%
c [elim-3-3] subsumed 4 and strengthened 0 clauses in 18801 steps
c [elim-3] incomplete 8 not tried 0% in round 3
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 540 = 2% variables out of 22440 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 166631 negative 99.1% of 168144 except 1513 0.9%
c [phase-count-3] 142731 positive 84.9% of 168144 except 25413 15.1%
c [phase-count-3] less non-negative clauses 1513 than limit 16800 (10.0%)
c [phase-count-3] non-pos/non-neg = 25413/1513 = 16.80 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 298 negative 100%
c [sort-queue-3] sorted 21900 enqueued variables after 1012 conflicts
c [score-dist-3] active 0 (0%), one 8978 (41%), zero 12922 (59%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 888 variables 3.9% (21900 remain 10%)
c [simplification-3] removed 13298 irredundant clauses 7.3% (168144 remain 16%)
c [simplification-3] maximum reduction of 7% = max (4%, 7%)
c [simplification-3] large reduction 7% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13012 (soft 3012 + delta 10000)
c [simplification-3] new conflict limit 3012 (hard 13012)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    5.0   21899   168144      1274    1016     31 12224    4    16   17  27%      1   16   17    0 5711%
c i    5.0   21640   168144      1275    1016     31 12224    4    16   17  27%      1   16   17    0 5689%
c i    5.0   21636   168144      1276    1016     31 12224    4    16   17  27%      1   16   17    0 5667%
c i    5.1   20833   168144      1418    1144     35 12228    5    17   17  28%      1   17   18    0 5243%
c i    5.1   20829   168144      1437    1160     36 12229    5    17   17  27%      1   17   17    0 4987%
c i    5.1   20828   168144      1438    1160     36 12229    5    17   17  27%      1   17   17    0 4968%
c i    5.2   20825   168144      1629    1322     46 12242    5    19   17  26%      1   19   13    0 3432%
c i    5.2   20824   168144      1743    1419     50 12250    5    19   17  27%      1   19   11    0 2894%
c i    5.2   20818   168144      1753    1428     50 12250    5    19   17  27%      1   19   11    0 2860%
c i    5.2   20817   168144      1755    1429     50 12250    5    19   17  27%      1   19   11    0 2838%
c i    5.3   20296   168144      1902    1549     54 12257    5    19   17  27%      1   19   11    0 2746%
c i    5.3   20295   168144      1903    1549     54 12257    5    19   17  27%      1   19   11    0 2735%
c i    5.4   20290   168144      2025    1651     60 12264    5    20   17  27%      1   19   10    0 2367%
c i    5.5   16114   168144      2295    1889     68 12267    6    23   17  27%      1   23   16    1 3132%
c i    5.5   16113   168144      2299    1891     69 12267    6    23   17  27%      1   23   15    1 3089%
c i    5.5   16109   168144      2302    1893     69 12267    6    23   17  27%      1   23   15    1 3058%
c i    5.5   16108   168144      2372    1958     71 12268    6    24   17  26%      1   24   15    1 2872%
c i    5.6   16103   168144      2507    2077     72 12276    7    25   17  26%      1   25   14    1 2640%
c i    5.6   16092   168144      2546    2111     74 12277    7    26   17  26%      1   26   15    1 2696%
c i    5.7   16071   168144      2656    2213     77 12278    7    27   17  26%      1   26   14    1 2512%
c i    5.7   16066   168144      2673    2223     80 12279    7    27   17  26%      1   26   14    1 2388%
c i    5.7   16065   168144      2676    2225     80 12279    7    27   17  26%      1   26   14    1 2384%
c 
c [simplification-4] limit 3066 conflicts (hard 13012) hit after 3066 conflicts
c [decomp-8] removed 6673 variables
c [basicprobe-2] limit 2977094 penalty 0 = 0 + 0
c [basicprobe-2-0] 1512 probes remain 10% after last round
c [basicprobe-2-0] 55 units = 52 failed (95%) + 3 lifted (5%)
c [basicprobe-2-0] removed 654 variables, found 9355 hbrs
c [unhide-4] limit 119083 with penalty 0 = 0 + 0
c [unhide-4-4] 14 units, 319 failed, 2140 tauts, 0 hbrs, 4431 literals
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 14146 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 2638 variables 19% in round 1 in 6997682 steps
c [elim-4-1] backward subsumption/strengthening limit 6997600
c [elim-4-1-1] backward checking 5688 touched variables 40%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 63 and strengthened 60 clauses in 742569 steps
c [elim-4-1] rescheduled 281 variables 2% by backward subsumption
c [elim-4-2] eliminated 60 variables 0% in round 2 in 141119 steps
c [elim-4-2] backward subsumption/strengthening limit 141100
c [elim-4-2-1] backward checking 230 touched variables 2%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 25 and strengthened 8 clauses in 65713 steps
c [elim-4-2] rescheduled 67 variables 0% by backward subsumption
c [elim-4-3] eliminated 21 variables 0% in round 3 in 35338 steps
c [elim-4-3] backward subsumption/strengthening limit 35300
c [elim-4-3-1] backward checking 69 touched variables 0%
c [elim-4-3-1] incomplete backward checking 0 remain 0%
c [elim-4-3] subsumed 11 and strengthened 3 clauses in 35301 steps
c [elim-4] incomplete 34 not tried 0% in round 3
c [gc-21] reconnected 9216 binary clauses (produced 0 empty 1 units)
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 2834 = 20% variables out of 14146 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 11312 enqueued variables after 3066 conflicts
c [score-dist-4] active 0 (0%), one 6196 (55%), zero 5116 (45%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 4750 variables 29.6% (11312 remain 5%)
c [simplification-4] removed 81930 irredundant clauses 48.7% (86214 remain 8%)
c [simplification-4] maximum reduction of 49% = max (30%, 49%)
c [simplification-4] large reduction 49% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 15066 (soft 5066 + delta 10000)
c [simplification-4] new conflict limit 5066 (hard 15066)
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    6.5   11311    86214      3171    1446     50  7462    8    31   12  25%      2   30   16    1 2327%
c i    6.5   10674    86214      3179    1449     50  7463    8    31   12  25%      2   30   16    1 2313%
c i    6.5   10671    86214      3180    1449     50  7463    8    31   12  25%      2   30   16    1 2304%
c i    6.5   10595    86214      3321    1576     53  7467    8    32   12  25%      2   31   15    1 2076%
c i    6.6   10592    86214      3757    1993     59  7471    9    36   12  25%      3   35   16    1 1968%
c i    6.8   10588    86214      4151    2370     61  7477   10    39   12  25%      3   38   18    1 1982%
c i    6.8   10586    86214      4257    2471     62  7478   10    41   12  25%      3   39   19    1 1979%
c i    6.8   10584    86214      4258    2471     62  7478   10    41   12  25%      3   39   19    1 1972%
c i    6.9   10583    86214      4475    2675     65  7480   11    43   12  25%      2   41   19    1 1858%
c i    6.9   10580    86214      4487    2685     65  7481   11    43   12  25%      2   41   18    1 1805%
c i    6.9   10579    86214      4554    2744     66  7482   11    43   12  25%      2   41   18    1 1734%
c i    6.9   10572    86214      4658    2843     67  7484   11    43   12  25%      2   42   20    1 1891%
c i    6.9   10571    86214      4667    2851     67  7484   11    43   12  25%      2   41   20    1 1837%
c i    7.0   10567    86214      4811    2989     68  7485   11    44   12  25%      2   43   19    1 1742%
c i    7.0   10564    86214      4855    3026     69  7486   11    44   12  25%      2   43   18    1 1644%
c i    7.0   10563    86214      4976    3142     70  7488   11    45   12  26%      2   43   18    1 1566%
c 
c [simplification-5] limit 5088 conflicts (hard 15066) hit after 5088 conflicts
c [quatres-1] found 4160 quaternary clauses 71% in total
c [quatres-1-1] removed 2 duplicate quaternary clauses
c [quatres-1-1] added 2 double-self-subsuming ternary resolvents
c [quatres-1-2] added 7 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 10562 free variables schedulable
c [ternres-1] 131 ternary resolvents (0 bin, 131 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 691 xors of average arity 2.3
c [gauss-1] connected 1572 occurrences of 560 variables (average 2.8)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 153 variables
c [gauss-1] exported 0 unary, 3 binary and 0 ternary equations
c [simpleprobe-3] 7320 schedulable variables 70%
c [simpleprobe-3] limit 3385492 penalty 0 = 0 + 0
c [decomp-11] removed 621 variables
c [simpleprobe-3] 958 variables remain 10% (8830 retained 90%)
c [simpleprobe-3] removed 621 variables, found 7621 hbrs, 141 units
c [unhide-5] limit 169274 with penalty 0 = 0 + 0
c [unhide-5-5] 3 units, 101 failed, 4259 tauts, 0 hbrs, 2847 literals
c [transred-1] limit 846373 with penalty 0 = 0 + 0
c [transred-1] removed 592 transitive binary clauses
c [transred-1] found 16 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 9630 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 276 blocked clauses
c [block-1] 276 < 1/100 * 67551 = 675 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 8
c [cce-1-1] eliminated 2 clauses out of 35 (6%) of length 7
c [cce-1-1] eliminated 21 clauses out of 275 (8%) of length 6
c [cce-1-1] eliminated 147 clauses out of 824 (18%) of length 5
c [cce-1-1] eliminated 1426 clauses out of 3617 (39%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 1597 large clauses in 14961784 steps
c [cce-1-1] allowing another 7480892 steps for small clauses
c [cce-1-1] scheduling 50440 clauses = 36793 binary + 13647 ternary
c [cce-1-1] tried to eliminate 2816 small clauses 6%
c [cce-1-1] eliminated 1019 binary clauses 3%
c [cce-1-1] eliminated 115 ternary clauses 1%
c [cce-1-1] eliminated 1134 small clauses 2%
c [cce-1-1] eliminated 1134 small clauses in 30000002 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2731 covered clauses in round 1
c [cce-1] eliminated 2731 covered clauses in TOTAL during 1 rounds
c [elim-5] no untried remaining variables left
c [elim-5] scheduled 9620 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 1011 variables 11% in round 1 in 4449449 steps
c [elim-5-1] backward subsumption/strengthening limit 4449400
c [elim-5-1-1] backward checking 3188 touched variables 33%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 16 and strengthened 36 clauses in 458869 steps
c [elim-5-1] rescheduled 120 variables 1% by backward subsumption
c [elim-5-2] eliminated 28 variables 0% in round 2 in 43710 steps
c [elim-5-2] backward subsumption/strengthening limit 43700
c [elim-5-2-1] backward checking 109 touched variables 1%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 11 and strengthened 5 clauses in 26262 steps
c [elim-5-2] rescheduled 35 variables 0% by backward subsumption
c [elim-5-3] eliminated 9 variables 0% in round 3 in 12101 steps
c [elim-5-3] backward subsumption/strengthening limit 12100
c [elim-5-3-1] backward checking 33 touched variables 0%
c [elim-5-3-1] incomplete backward checking 0 remain 0%
c [elim-5-3] subsumed 0 and strengthened 0 clauses in 12101 steps
c [elim-5] fully completed in 3 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 1051 = 11% variables out of 9620 scheduled
c [bca-1] limit of 10000000 steps and 121734 added (scaled 2)
c [bca-1] 14286 out of 17140 literals actually usable 83%
c [bca-1] added 6 blocked clauses in 31902 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1452 pos 16.9% + 7117 neg 83.1% = 8569 sched 100.0% ret 0
c [sweep-1-1] 1030685 steps 23 queries 809.35 avg class size
c [sweep-1-1] 248 decisions 18 SAT calls 58.39 avg env size
c [sweep-1-1] 8310 variables remain 97% (243 retained 3%)
c [decomp-12] removed 26 variables
c [sweep-1-1] removed 26 vars (0 failed, 7 eqs, 5 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 26 vars in TOTAL (1 rounds, 22 queries)
c [sort-queue-5] sorted 8543 enqueued variables after 5088 conflicts
c [score-dist-5] active 0 (0%), one 5322 (62%), zero 3221 (38%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 2019 variables 19.1% (8543 remain 4%)
c [simplification-5] removed 25799 irredundant clauses 29.9% (60415 remain 6%)
c [simplification-5] maximum reduction of 30% = max (19%, 30%)
c [simplification-5] large reduction 30% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 17088 (soft 7088 + delta 10000)
c [simplification-5] new conflict limit 7088 (hard 17088)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    8.6    8542    60415      5166    2544    223 12581   12    47   11  25%      2   45   19    1 1572%
c i    8.6    8539    60415      5301    2675    224 12582   12    47   11  26%      2   45   19    1 1517%
c i    8.7    8536    60415      5489    2853    226 12585   12    48   11  25%      2   46   17    1 1360%
c i    8.7    8519    60415      5788    3141    231 12586   13    50   11  25%      2   48   19    1 1360%
c i    8.8    8516    60415      6051    3395    231 12587   13    52   11  26%      2   50   22    1 1523%
c i    8.8    8514    60415      6094    3431    232 12587   13    52   11  26%      2   50   20    1 1393%
c i    8.8    8510    60415      6096    3432    232 12587   13    52   11  26%      2   50   20    1 1384%
c i    8.9    8493    60415      6451    3772    235 12590   14    54   12  26%      2   51   18    2 1161%
c i    8.9    8492    60415      6490    3809    235 12590   14    54   12  26%      2   51   18    2 1158%
c i    8.9    8491    60415      6491    3809    235 12590   14    54   12  26%      2   51   18    2 1153%
c i    9.0    8488    60415      6619    3922    237 12591   14    54   12  26%      2   51   18    2 1108%
c i    9.0    8484    60415      6621    3922    238 12591   14    54   12  26%      2   51   18    2 1100%
c i    9.0    8483    60415      6626    3926    238 12591   14    54   12  26%      2   51   17    2 1083%
c i    9.0    8478    60415      6789    4083    238 12594   14    54   12  26%      2   51   16    2 1001%
c 
c [simplification-6] limit 7110 conflicts (hard 17088) hit after 7110 conflicts
c [quatres-2] found 2510 quaternary clauses 62% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-2] added 2 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 8477 free variables schedulable
c [ternres-2] 109 ternary resolvents (0 bin, 109 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2184 at-most-one constraints of average size 3.5
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2184 out of 2184 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 130 xors of average arity 2.7
c [gauss-2] connected 346 occurrences of 131 variables (average 2.6)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 12 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 16866 literals 100%
c [treelook-3] scheduling used 215825 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 302128 steps
c [treelook-3] 16801 literals remain 99%
c [treelook-3] 8303 variables remain to probed next time 98%
c [decomp-14] removed 5 variables
c [treelook-3] removed 27 variables, found 2659 hbrs
c [unhide-6] limit 208568 with penalty 0 = 0 + 0
c [unhide-6-6] 16 units, 159 failed, 3790 tauts, 0 hbrs, 6965 literals
c [transred-2] limit 1042841 with penalty 0 = 0 + 0
c [transred-2] removed 649 transitive binary clauses
c [transred-2] found 19 units
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 3 (33%) of length 10
c [cce-2-1] eliminated 1 clauses out of 5 (20%) of length 9
c [cce-2-1] eliminated 2 clauses out of 52 (4%) of length 7
c [cce-2-1] eliminated 5 clauses out of 246 (2%) of length 6
c [cce-2-1] eliminated 38 clauses out of 783 (5%) of length 5
c [cce-2-1] eliminated 322 clauses out of 2406 (13%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 369 large clauses in 11927789 steps
c [cce-2-1] allowing another 5963894 steps for small clauses
c [cce-2-1] scheduling 41353 clauses = 32514 binary + 8839 ternary
c [cce-2-1] tried to eliminate 3616 small clauses 9%
c [cce-2-1] eliminated 1372 binary clauses 4%
c [cce-2-1] eliminated 132 ternary clauses 1%
c [cce-2-1] eliminated 1504 small clauses 4%
c [cce-2-1] eliminated 3432 small clauses in 30000004 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 3801 covered clauses in round 1
c [cce-2] eliminated 3801 covered clauses in TOTAL during 1 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 8269 variables 100%
c [elim-6] limit of 20856825 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 419 variables 5% in round 1 in 3854690 steps
c [elim-6-1] backward subsumption/strengthening limit 3854600
c [elim-6-1-1] backward checking 1966 touched variables 24%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 6 and strengthened 23 clauses in 308633 steps
c [elim-6-1] rescheduled 75 variables 1% by backward subsumption
c [elim-6-2] eliminated 10 variables 0% in round 2 in 28300 steps
c [elim-6-2] backward subsumption/strengthening limit 28300
c [elim-6-2-1] backward checking 51 touched variables 1%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 4 and strengthened 3 clauses in 16728 steps
c [elim-6-2] rescheduled 14 variables 0% by backward subsumption
c [elim-6-3] eliminated 1 variables 0% in round 3 in 7636 steps
c [elim-6-3] backward subsumption/strengthening limit 7600
c [elim-6-3-1] backward checking 11 touched variables 0%
c [elim-6-3-1] incomplete backward checking 0 remain 0%
c [elim-6-3] subsumed 1 and strengthened 0 clauses in 7601 steps
c [elim-6] incomplete 2 not tried 0% in round 3
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 435 = 5% variables out of 8269 scheduled
c [bca-2] limit of 10000000 steps and 108987 added (scaled 2)
c [bca-2] 12618 out of 15670 literals actually usable 81%
c [bca-2] added 21 blocked clauses in 29518 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1356 pos 17.8% + 6247 neg 82.2% = 7603 sched 97.1% ret 231
c [sweep-2-1] 1006162 steps 14 queries 1238.93 avg class size
c [sweep-2-1] 231 decisions 12 SAT calls 126.00 avg env size
c [sweep-2-1] 7550 variables remain 97% (265 retained 3%)
c [decomp-15] removed 27 variables
c [sweep-2-1] removed 27 vars (0 failed, 4 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 27 vars in TOTAL (1 rounds, 13 queries)
c [sort-queue-6] sorted 7807 enqueued variables after 7110 conflicts
c [score-dist-6] active 0 (0%), one 5022 (64%), zero 2785 (36%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 670 variables 7.9% (7807 remain 4%)
c [simplification-6] removed 6424 irredundant clauses 10.6% (53991 remain 5%)
c [simplification-6] maximum reduction of 11% = max (8%, 11%)
c [simplification-6] large reduction 11% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 19110 (soft 9110 + delta 10000)
c [simplification-6] new conflict limit 9110 (hard 19110)
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   10.5    7806    53991      7275    3870    360 10860   14    55   12  26%      3   52   17    2  957%
c i   10.6    7803    53991      7648    4234    363 10860   16    58   12  27%      3   54   26    2 1350%
c i   10.7    7802    53991      8038    4604    364 10863   16    59   12  27%      3   54   21    2 1033%
c i   10.7    7799    53991      8058    4623    364 10863   16    59   12  27%      3   54   20    2 1019%
c i   10.7    7798    53991      8180    4739    366 10863   16    58   12  27%      2   54   19    2  918%
c i   10.7    7795    53991      8252    4809    367 10863   16    59   12  27%      2   54   18    2  879%
c i   10.7    7794    53991      8259    4813    367 10863   16    59   12  27%      2   54   18    2  864%
c i   10.7    7793    53991      8260    4813    367 10863   16    59   12  27%      2   54   18    2  860%
c i   10.8    7771    53991      8675    5218    367 10864   16    60   12  27%      3   55   18    2  821%
c 
c [simplification-7] limit 9121 conflicts (hard 19110) hit after 9121 conflicts
c [quatres-3] found 2104 quaternary clauses 56% in total
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 7769 free variables schedulable
c [ternres-3] 196 ternary resolvents (0 bin, 196 trn)
c [ternres-3] fully completed ternary resolution
c [decomp-16] removed 44 variables
c [basicprobe-3] limit 6124518 penalty 0 = 0 + 0
c [basicprobe-3-0] 903 probes remain 12% after last round
c [basicprobe-3-0] 143 units = 135 failed (94%) + 8 lifted (6%)
c [basicprobe-3-0] removed 156 variables, found 14921 hbrs
c [bate-1] eliminated 31 asymmetric tautologies during probing
c [unhide-7] limit 244980 with penalty 0 = 0 + 0
c [unhide-7-7] 2 units, 77 failed, 2294 tauts, 0 hbrs, 3302 literals
c [transred-3] limit 1224903 with penalty 0 = 0 + 0
c [transred-3] removed 681 transitive binary clauses
c [transred-3] found 17 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 6921 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 151 blocked clauses
c [block-2] 151 < 1/100 * 49123 = 491 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 10
c [cce-3-1] eliminated 1 clauses out of 33 (3%) of length 7
c [cce-3-1] eliminated 6 clauses out of 184 (3%) of length 6
c [cce-3-1] eliminated 37 clauses out of 526 (7%) of length 5
c [cce-3-1] eliminated 141 clauses out of 1578 (9%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 186 large clauses in 8080423 steps
c [cce-3-1] allowing another 4040211 steps for small clauses
c [cce-3-1] scheduling 31455 clauses = 24547 binary + 6908 ternary
c [cce-3-1] tried to eliminate 3893 small clauses 12%
c [cce-3-1] eliminated 1338 binary clauses 5%
c [cce-3-1] eliminated 154 ternary clauses 2%
c [cce-3-1] eliminated 1492 small clauses 5%
c [cce-3-1] eliminated 1492 small clauses in 30000003 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1678 covered clauses in round 1
c [cce-3] eliminated 1678 covered clauses in TOTAL during 1 rounds
c [elim-7] no untried remaining variables left
c [elim-7] scheduled 6913 variables 100%
c [elim-7] limit of 24498075 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 890 variables 13% in round 1 in 2835608 steps
c [elim-7-1] backward subsumption/strengthening limit 2835600
c [elim-7-1-1] backward checking 2666 touched variables 39%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 5 and strengthened 16 clauses in 343987 steps
c [elim-7-1] rescheduled 60 variables 1% by backward subsumption
c [elim-7-2] eliminated 3 variables 0% in round 2 in 28158 steps
c [elim-7-2] backward subsumption/strengthening limit 28100
c [elim-7-2-1] backward checking 31 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 4 clauses in 15082 steps
c [elim-7-2] rescheduled 9 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 3896 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 895 = 13% variables out of 6913 scheduled
c [bca-3] limit of 10000000 steps and 80911 added (scaled 2)
c [bca-3] 9482 out of 12038 literals actually usable 79%
c [bca-3] added 16 blocked clauses in 22877 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 962 pos 16.6% + 4823 neg 83.4% = 5785 sched 96.1% ret 233
c [sweep-3-1] 1001503 steps 35 queries 274.91 avg class size
c [sweep-3-1] 273 decisions 31 SAT calls 93.94 avg env size
c [sweep-3-1] 5078 variables remain 85% (915 retained 15%)
c [decomp-17] removed 42 variables
c [sweep-3-1] removed 42 vars (0 failed, 6 eqs, 9 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 42 vars in TOTAL (1 rounds, 34 queries)
c [sort-queue-7] sorted 5976 enqueued variables after 9121 conflicts
c [score-dist-7] active 0 (0%), one 3916 (66%), zero 2060 (34%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 1793 variables 23.1% (5976 remain 3%)
c [simplification-7] removed 14071 irredundant clauses 26.1% (39920 remain 4%)
c [simplification-7] maximum reduction of 26% = max (23%, 26%)
c [simplification-7] large reduction 26% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 21121 (soft 11121 + delta 10000)
c [simplification-7] new conflict limit 11121 (hard 21121)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   12.4    5975    39920      9275    3535    412 19321   17    62   11  28%      4   57   21    2  909%
c i   12.5    5971    39920      9402    3654    414 19323   17    62   11  28%      3   56   18    2  777%
c i   12.5    5970    39920      9471    3720    415 19324   17    62   11  28%      3   56   18    2  765%
c i   12.5    5966    39920      9713    3953    416 19326   17    62   11  28%      3   56   22    2  883%
c i   12.6    5962    39920      9904    4135    416 19326   18    63   11  28%      3   57   22    3  893%
c i   12.6    5961    39920     10170    4391    419 19329   18    63   11  28%      2   57   20    3  793%
c i   12.6    5960    39920     10171    4391    419 19329   18    63   11  28%      2   57   20    3  790%
c i   12.6    5957    39920     10174    4390    419 19329   18    63   11  28%      2   57   20    3  787%
c i   12.6    5956    39920     10205    4419    420 19329   18    63   11  28%      2   57   19    3  737%
c i   12.7    5955    39920     10552    4753    422 19332   18    62   11  28%      2   56   18    3  667%
c i   12.8    5951    39920     10824    5012    426 19335   18    63   11  28%      2   56   20    3  716%
c i   12.8    5948    39920     11046    5226    430 19337   18    63   11  29%      2   56   20    3  725%
c 
c [simplification-8] limit 11134 conflicts (hard 21121) hit after 11134 conflicts
c [quatres-4] found 1560 quaternary clauses 54% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-2] added 6 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 5948 free variables schedulable
c [ternres-4] 139 ternary resolvents (0 bin, 139 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 51 xors of average arity 2.6
c [gauss-3] connected 132 occurrences of 57 variables (average 2.3)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-18] removed 4 variables
c [simpleprobe-4] 554 schedulable variables 9%
c [simpleprobe-4] limit 5486103 penalty 0 = 0 + 0
c [decomp-19] removed 152 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 152 variables, found 2402 hbrs, 42 units
c [unhide-8] limit 274305 with penalty 0 = 0 + 0
c [unhide-8-8] 4 units, 69 failed, 4198 tauts, 0 hbrs, 4520 literals
c [transred-4] limit 1371525 with penalty 0 = 0 + 0
c [transred-4] removed 858 transitive binary clauses
c [transred-4] found 26 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 11
c [cce-4-1] eliminated 1 clauses out of 26 (4%) of length 8
c [cce-4-1] eliminated 3 clauses out of 47 (6%) of length 7
c [cce-4-1] eliminated 5 clauses out of 193 (3%) of length 6
c [cce-4-1] eliminated 25 clauses out of 538 (5%) of length 5
c [cce-4-1] eliminated 151 clauses out of 1415 (11%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 186 large clauses in 7253458 steps
c [cce-4-1] allowing another 3626729 steps for small clauses
c [cce-4-1] scheduling 28932 clauses = 20501 binary + 8431 ternary
c [cce-4-1] tried to eliminate 28932 small clauses 100%
c [cce-4-1] eliminated 6248 binary clauses 30%
c [cce-4-1] eliminated 1066 ternary clauses 13%
c [cce-4-1] eliminated 7314 small clauses 25%
c [cce-4-1] eliminated 8243 small clauses in 182835469 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 8429 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 2386126 steps for small clauses
c [cce-4-2] scheduling 21618 clauses = 14253 binary + 7365 ternary
c [cce-4-2] tried to eliminate 21618 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 8429 covered clauses in TOTAL during 2 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 5695 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 548610380 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 697 variables 12% in round 1 in 1977171 steps
c [elim-8-1] backward subsumption/strengthening limit 1977100
c [elim-8-1-1] backward checking 2553 touched variables 45%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 4 and strengthened 10 clauses in 262033 steps
c [elim-8-1] rescheduled 59 variables 1% by backward subsumption
c [elim-8-2] eliminated 5 variables 0% in round 2 in 26843 steps
c [elim-8-2] backward subsumption/strengthening limit 26800
c [elim-8-2-1] backward checking 35 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 4 and strengthened 6 clauses in 16066 steps
c [elim-8-2] rescheduled 15 variables 0% by backward subsumption
c [elim-8-3] eliminated 7 variables 0% in round 3 in 4676 steps
c [elim-8-3] backward subsumption/strengthening limit 4600
c [elim-8-3-1] backward checking 17 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 0 and strengthened 0 clauses in 4601 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 709 = 12% variables out of 5695 scheduled
c [bca-4] limit of 10000000 steps and 57763 added (scaled 2)
c [bca-4] 7704 out of 9974 literals actually usable 77%
c [bca-4] added 8 blocked clauses in 19156 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 694 pos 16.5% + 3523 neg 83.5% = 4217 sched 84.6% ret 769
c [sweep-4-1] 1000079 steps 37 queries 267.65 avg class size
c [sweep-4-1] 543 decisions 35 SAT calls 100.37 avg env size
c [sweep-4-1] 3076 variables remain 62% (1896 retained 38%)
c [decomp-20] removed 21 variables
c [sweep-4-1] removed 21 vars (0 failed, 3 eqs, 4 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 21 vars in TOTAL (1 rounds, 36 queries)
c [sort-queue-8] sorted 4965 enqueued variables after 11134 conflicts
c [score-dist-8] active 0 (0%), one 3378 (68%), zero 1587 (32%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 983 variables 16.5% (4965 remain 2%)
c [simplification-8] removed 11410 irredundant clauses 28.6% (28510 remain 3%)
c [simplification-8] maximum reduction of 29% = max (17%, 29%)
c [simplification-8] large reduction 29% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 23134 (soft 13134 + delta 10000)
c [simplification-8] new conflict limit 13134 (hard 23134)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   19.5    4964    28510     11142    3215    939 18062   18    63   10  29%      2   56   20    3  712%
c i   19.5    4962    28510     11145    3217    939 18062   18    63   10  29%      2   56   20    3  704%
c i   19.5    4956    28510     11146    3217    939 18062   18    63   10  29%      2   56   20    3  701%
c i   19.5    4954    28510     11257    3322    939 18064   18    63   10  29%      2   56   20    3  687%
c i   19.5    4953    28510     11374    3430    939 18064   18    63   10  29%      2   56   20    3  710%
c i   19.5    4952    28510     11572    3618    942 18066   18    62   10  29%      2   55   18    3  602%
c i   19.6    4951    28510     11666    3701    943 18067   18    62   10  29%      1   54   17    3  594%
c i   19.6    4950    28510     11711    3743    944 18068   18    62   10  29%      1   54   17    3  592%
c i   19.7    4949    28510     12515    4513    951 18072   18    60   10  30%      4   52   15    3  494%
c i   19.8    4948    28510     13067    5052    953 18072   18    60   11  30%      4   51   19    3  595%
c 
c [simplification-9] limit 13147 conflicts (hard 23134) hit after 13148 conflicts
c [quatres-5] found 1345 quaternary clauses 49% in total
c [quatres-5-2] added 2 single-self-subsuming ternary resolvents
c [quatres-5-2] added 9 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 4948 free variables schedulable
c [ternres-5] 27 ternary resolvents (0 bin, 27 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-21] removed 29 variables
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 9842 literals 100%
c [treelook-4] scheduling used 143209 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 335350 steps
c [treelook-4] 9812 literals remain 100%
c [treelook-4] 4866 variables remain to probed next time 99%
c [treelook-4] removed 8 variables, found 3346 hbrs
c [unhide-9] limit 299603 with penalty 0 = 0 + 0
c [unhide-9-10] 8 units, 39 failed, 3035 tauts, 0 hbrs, 3568 literals
c [transred-5] limit 1498017 with penalty 0 = 0 + 0
c [transred-5] removed 606 transitive binary clauses
c [transred-5] found 29 units
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 27
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 25
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 23
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 20
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 16
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 13
c [cce-5-1] eliminated 1 clauses out of 4 (25%) of length 12
c [cce-5-1] eliminated 2 clauses out of 5 (40%) of length 11
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 10
c [cce-5-1] eliminated 2 clauses out of 12 (17%) of length 9
c [cce-5-1] eliminated 6 clauses out of 41 (15%) of length 8
c [cce-5-1] eliminated 3 clauses out of 55 (5%) of length 7
c [cce-5-1] eliminated 19 clauses out of 201 (9%) of length 6
c [cce-5-1] eliminated 47 clauses out of 530 (9%) of length 5
c [cce-5-1] eliminated 175 clauses out of 1222 (14%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 265 large clauses in 6229393 steps
c [cce-5-1] allowing another 3114696 steps for small clauses
c [cce-5-1] scheduling 18725 clauses = 13400 binary + 5325 ternary
c [cce-5-1] tried to eliminate 5295 small clauses 28%
c [cce-5-1] eliminated 351 binary clauses 3%
c [cce-5-1] eliminated 251 ternary clauses 5%
c [cce-5-1] eliminated 602 small clauses 3%
c [cce-5-1] eliminated 914 small clauses in 30000008 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1179 covered clauses in round 1
c [cce-5] eliminated 1179 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 4854 variables 100%
c [elim-9] limit of 29960350 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 204 variables 4% in round 1 in 1769396 steps
c [elim-9-1] backward subsumption/strengthening limit 1769300
c [elim-9-1-1] backward checking 1185 touched variables 24%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 6 clauses in 129303 steps
c [elim-9-1] rescheduled 28 variables 1% by backward subsumption
c [elim-9-2] eliminated 3 variables 0% in round 2 in 11161 steps
c [elim-9-2] backward subsumption/strengthening limit 11100
c [elim-9-2-1] backward checking 24 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 8295 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 207 = 4% variables out of 4854 scheduled
c [bca-5] limit of 10000000 steps and 53809 added (scaled 2)
c [bca-5] 6902 out of 9296 literals actually usable 74%
c [bca-5] added 11 blocked clauses in 19134 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 605 pos 21.1% + 2267 neg 78.9% = 2872 sched 61.8% ret 1775
c [sweep-5-1] 10006173 steps 517 queries 21.33 avg class size
c [sweep-5-1] 3299 decisions 417 SAT calls 44.57 avg env size
c [sweep-5-1] 88 variables remain 2% (4376 retained 98%)
c [decomp-23] removed 312 variables
c [sweep-5-1] removed 312 vars (0 failed, 114 eqs, 142 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 312 vars in TOTAL (1 rounds, 516 queries)
c [sort-queue-9] sorted 4335 enqueued variables after 13148 conflicts
c [score-dist-9] active 0 (0%), one 2992 (69%), zero 1343 (31%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 613 variables 12.4% (4335 remain 2%)
c [simplification-9] removed 3250 irredundant clauses 11.4% (25260 remain 2%)
c [simplification-9] maximum reduction of 12% = max (12%, 11%)
c [simplification-9] large reduction 12% >= 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 25148 (soft 15148 + delta 10000)
c [simplification-9] new conflict limit 15148 (hard 25148)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   21.3    4334    25260     13943    5558    685 20846   18    57   11  31%      6   48   17    3  487%
c i   21.3    4333    25260     13947    5561    685 20846   18    57   11  31%      6   48   17    3  483%
c i   21.4    4330    25260     14132    5742    687 20847   18    58   11  31%      5   48   19    3  537%
c i   21.4    4329    25260     14250    5856    687 20847   18    57   11  31%      5   48   18    3  510%
c i   21.4    4328    25260     14482    6077    691 20851   18    57   11  31%      4   47   17    4  475%
c i   21.5    4322    25260     14756    6343    691 20852   18    58   11  31%      3   48   19    4  525%
c 
c [simplification-10] limit 15150 conflicts (hard 25148) hit after 15150 conflicts
c [quatres-6] found 1013 quaternary clauses 46% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 1 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 4308 free variables schedulable
c [ternres-6] 48 ternary resolvents (1 bin, 47 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 250000 penalty 3 = 3 + 0
c [card-4] found 691 at-most-one constraints of average size 3.4
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 250000 for elimination
c [card-4] 691 out of 691 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-24] removed 38 variables
c [basicprobe-4] limit 8056352 penalty 0 = 0 + 0
c [basicprobe-4-0] 119 probes remain 3% after last round
c [basicprobe-4-0] 243 units = 214 failed (88%) + 29 lifted (12%)
c [basicprobe-4-0] removed 304 variables, found 16379 hbrs
c [bate-2] eliminated 42 asymmetric tautologies during probing
c [unhide-10] limit 322254 with penalty 0 = 0 + 0
c [unhide-10-12] 3 units, 207 failed, 4672 tauts, 0 hbrs, 3322 literals
c [transred-6] limit 1611270 with penalty 0 = 0 + 0
c [transred-6] removed 682 transitive binary clauses
c [transred-6] found 19 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 3836 variables 100%
c [block-3] limit of 12500000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 187 blocked clauses
c [block-3] 187 < 1/100 * 21740 = 217 considered unsuccessful
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 20
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 19
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 18
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 16
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 11
c [cce-6-1] eliminated 2 clauses out of 24 (8%) of length 7
c [cce-6-1] eliminated 2 clauses out of 91 (2%) of length 6
c [cce-6-1] eliminated 17 clauses out of 296 (6%) of length 5
c [cce-6-1] eliminated 39 clauses out of 767 (5%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 66 large clauses in 3015795 steps
c [cce-6-1] allowing another 1507897 steps for small clauses
c [cce-6-1] scheduling 15032 clauses = 11584 binary + 3448 ternary
c [cce-6-1] tried to eliminate 6607 small clauses 44%
c [cce-6-1] eliminated 645 binary clauses 6%
c [cce-6-1] eliminated 124 ternary clauses 4%
c [cce-6-1] eliminated 769 small clauses 5%
c [cce-6-1] eliminated 769 small clauses in 30000000 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 835 covered clauses in round 1
c [cce-6] eliminated 835 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 3820 variables 100%
c [elim-10] limit of 32225410 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 452 variables 12% in round 1 in 1304409 steps
c [elim-10-1] backward subsumption/strengthening limit 1304400
c [elim-10-1-1] backward checking 1594 touched variables 42%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 3 and strengthened 3 clauses in 169443 steps
c [elim-10-1] rescheduled 23 variables 1% by backward subsumption
c [elim-10-2] eliminated 2 variables 0% in round 2 in 8614 steps
c [elim-10-2] backward subsumption/strengthening limit 8600
c [elim-10-2-1] backward checking 16 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 2 and strengthened 0 clauses in 6528 steps
c [elim-10-2] rescheduled 5 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 1407 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 456 = 12% variables out of 3820 scheduled
c [bca-6] limit of 10000000 steps and 40177 added (scaled 2)
c [bca-6] 4887 out of 6730 literals actually usable 73%
c [bca-6] added 15 blocked clauses in 13859 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 12 pos 29.3% + 29 neg 70.7% = 41 sched 1.2% ret 3323
c [sweep-6-1] 532012 steps 27 queries 6.44 avg class size
c [sweep-6-1] 243 decisions 24 SAT calls 30.12 avg env size
c [sweep-6-1] fully completed sweeping round
c [decomp-25] removed 7 variables
c [sweep-6-1] removed 7 vars (0 failed, 1 eqs, 2 impls)
c [sweep-6-2] 545 pos 16.2% + 2812 neg 83.8% = 3357 sched 100.0% ret 0
c [sweep-6-2] 477398 steps 28 queries 155.21 avg class size
c [sweep-6-2] 444 decisions 26 SAT calls 71.27 avg env size
c [sweep-6-2] 2398 variables remain 72% (955 retained 28%)
c [decomp-26] removed 7 variables
c [sweep-6-2] removed 7 vars (0 failed, 3 eqs, 5 impls)
c [sweep-6] removed 14 vars in TOTAL (2 rounds, 53 queries)
c [sort-queue-10] sorted 3350 enqueued variables after 15150 conflicts
c [score-dist-10] active 0 (0%), one 2454 (73%), zero 896 (27%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 958 variables 22.2% (3350 remain 2%)
c [simplification-10] removed 5505 irredundant clauses 21.8% (19755 remain 2%)
c [simplification-10] maximum reduction of 22% = max (22%, 22%)
c [simplification-10] large reduction 22% >= 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 27150 (soft 17150 + delta 10000)
c [simplification-10] new conflict limit 17150 (hard 27150)
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   23.0    3349    19755     15415    3752    383 20098   18    57   10  31%      4   46   16    4  414%
c i   23.1    3348    19755     16031    4340    388 20100   18    56   10  32%      4   45   16    4  419%
c i   23.2    3347    19755     17051    5320    400 20103   17    54   10  32%      7   43   14    4  357%
c 
c [simplification-11] limit 17150 conflicts (hard 27150) hit after 17151 conflicts
c [quatres-7] found 985 quaternary clauses 48% in total
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] all 3347 free variables schedulable
c [ternres-7] 57 ternary resolvents (0 bin, 57 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-4] limit 500000 penalty 2 = 2 + 0
c [gauss-4] extracted 17 xors of average arity 2.5
c [gauss-4] connected 43 occurrences of 17 variables (average 2.5)
c [gauss-4] limit 500000 penalty 2 = 2 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-27] removed 4 variables
c [simpleprobe-5] all 3343 free variables schedulable
c [simpleprobe-5] limit 6787843 penalty 0 = 0 + 0
c [decomp-28] removed 26 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 26 variables, found 2443 hbrs, 17 units
c [unhide-11] limit 339392 with penalty 0 = 0 + 0
c [unhide-11-14] 0 units, 3 failed, 2640 tauts, 0 hbrs, 2670 literals
c [transred-7] limit 1696960 with penalty 0 = 0 + 0
c [transred-7] removed 850 transitive binary clauses
c [transred-7] found 12 units
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 15
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 13
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 12
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 10
c [cce-7-1] eliminated 2 clauses out of 14 (14%) of length 8
c [cce-7-1] eliminated 5 clauses out of 33 (15%) of length 7
c [cce-7-1] eliminated 3 clauses out of 109 (3%) of length 6
c [cce-7-1] eliminated 14 clauses out of 338 (4%) of length 5
c [cce-7-1] eliminated 78 clauses out of 831 (9%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 106 large clauses in 4044419 steps
c [cce-7-1] allowing another 2022209 steps for small clauses
c [cce-7-1] scheduling 13243 clauses = 10105 binary + 3138 ternary
c [cce-7-1] tried to eliminate 6821 small clauses 52%
c [cce-7-1] eliminated 640 binary clauses 6%
c [cce-7-1] eliminated 136 ternary clauses 4%
c [cce-7-1] eliminated 776 small clauses 6%
c [cce-7-1] eliminated 919 small clauses in 30000000 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1025 covered clauses in round 1
c [cce-7] eliminated 1025 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 3294 variables 100%
c [elim-11] limit of 33939218 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 132 variables 4% in round 1 in 1172508 steps
c [elim-11-1] backward subsumption/strengthening limit 1172500
c [elim-11-1-1] backward checking 733 touched variables 22%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 0 and strengthened 3 clauses in 87216 steps
c [elim-11-1] rescheduled 16 variables 0% by backward subsumption
c [elim-11-2] eliminated 1 variables 0% in round 2 in 5712 steps
c [elim-11-2] backward subsumption/strengthening limit 5700
c [elim-11-2-1] backward checking 9 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 0 clauses in 3179 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 133 = 4% variables out of 3294 scheduled
c [bca-7] limit of 10000000 steps and 36968 added (scaled 2)
c [bca-7] 4339 out of 6324 literals actually usable 69%
c [bca-7] added 8 blocked clauses in 14420 steps
c [sweep-7] limit 1000000 penalty 0 = 0 + 0
c [sweep-7-1] 487 pos 21.7% + 1754 neg 78.3% = 2241 sched 70.9% ret 920
c [sweep-7-1] 1001285 steps 35 queries 105.37 avg class size
c [sweep-7-1] 776 decisions 31 SAT calls 91.03 avg env size
c [sweep-7-1] 1704 variables remain 54% (1454 retained 46%)
c [decomp-29] removed 6 variables
c [sweep-7-1] removed 6 vars (0 failed, 3 eqs, 3 impls)
c [sweep-7] removed 6 vars in TOTAL (1 rounds, 34 queries)
c [sort-queue-11] sorted 3155 enqueued variables after 17151 conflicts
c [score-dist-11] active 0 (0%), one 2366 (75%), zero 789 (25%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 192 variables 5.7% (3155 remain 1%)
c [simplification-11] removed 1573 irredundant clauses 8.0% (18182 remain 2%)
c [simplification-11] maximum reduction of 8% = max (6%, 8%)
c [simplification-11] large reduction 8% >= 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 29151 (soft 19151 + delta 10000)
c [simplification-11] new conflict limit 19151 (hard 29151)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   24.4    3154    18182     17492    5547    452 16492   17    53   10  32%      6   42   16    4  384%
c 
c [simplification-12] limit 19151 conflicts (hard 29151) hit after 19151 conflicts
c [quatres-8] found 920 quaternary clauses 46% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 8 quaternary resolvents
c [ternres-8] limit 4000000 with penalty 0 = 0 + 0
c [ternres-8] all 3154 free variables schedulable
c [ternres-8] 20 ternary resolvents (0 bin, 20 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-30] removed 1 variables
c [treelook-5] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 6290 literals 100%
c [treelook-5] scheduling used 109673 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 314785 steps
c [treelook-5] 6241 literals remain 99%
c [treelook-5] 3106 variables remain to probed next time 99%
c [treelook-5] removed 9 variables, found 2288 hbrs
c [unhide-12] limit 356150 with penalty 0 = 0 + 0
c [unhide-12-16] 1 units, 0 failed, 1731 tauts, 0 hbrs, 5163 literals
c [transred-8] limit 1780752 with penalty 0 = 0 + 0
c [transred-8] removed 602 transitive binary clauses
c [transred-8] found 6 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 11 (9%) of length 8
c [cce-8-1] eliminated 1 clauses out of 31 (3%) of length 7
c [cce-8-1] eliminated 3 clauses out of 321 (1%) of length 5
c [cce-8-1] eliminated 19 clauses out of 791 (2%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 24 large clauses in 3523970 steps
c [cce-8-1] allowing another 1761985 steps for small clauses
c [cce-8-1] scheduling 13786 clauses = 9290 binary + 4496 ternary
c [cce-8-1] tried to eliminate 13786 small clauses 100%
c [cce-8-1] eliminated 380 binary clauses 4%
c [cce-8-1] eliminated 234 ternary clauses 5%
c [cce-8-1] eliminated 614 small clauses 4%
c [cce-8-1] eliminated 663 small clauses in 55513069 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 687 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 1639678 steps for small clauses
c [cce-8-2] scheduling 13172 clauses = 8910 binary + 4262 ternary
c [cce-8-2] tried to eliminate 13172 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 687 covered clauses in TOTAL during 2 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 3137 variables 100%
c [elim-12] limit of 35615051 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 70 variables 2% in round 1 in 1103288 steps
c [elim-12-1] backward subsumption/strengthening limit 1103200
c [elim-12-1-1] backward checking 447 touched variables 14%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 51325 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 70 = 2% variables out of 3137 scheduled
c [bca-8] limit of 10000000 steps and 35202 added (scaled 2)
c [bca-8] 4140 out of 6136 literals actually usable 67%
c [bca-8] added 9 blocked clauses in 15305 steps
c [sweep-8] limit 1000000 penalty 0 = 0 + 0
c [sweep-8-1] 428 pos 25.8% + 1228 neg 74.2% = 1656 sched 54.0% ret 1411
c [sweep-8-1] 1071083 steps 54 queries 92.81 avg class size
c [sweep-8-1] 705 decisions 50 SAT calls 65.42 avg env size
c [sweep-8-1] 1129 variables remain 37% (1925 retained 63%)
c [decomp-32] removed 15 variables
c [sweep-8-1] removed 15 vars (0 failed, 5 eqs, 7 impls)
c [sweep-8] removed 15 vars in TOTAL (1 rounds, 53 queries)
c [sort-queue-12] sorted 3052 enqueued variables after 19151 conflicts
c [score-dist-12] active 0 (0%), one 2350 (77%), zero 702 (23%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 102 variables 3.2% (3052 remain 1%)
c [simplification-12] removed 941 irredundant clauses 5.2% (17241 remain 2%)
c [simplification-12] maximum reduction of 5% = max (3%, 5%)
c [simplification-12] large reduction 5% >= 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 31151 (soft 21151 + delta 10000)
c [simplification-12] new conflict limit 21151 (hard 31151)
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   27.5    3051    17241     21145    8384    562 15326   17    49   10  34%     40   36   16    5  341%
c 
c [simplification-13] limit 21151 conflicts (hard 31151) hit after 21151 conflicts
c [quatres-9] found 919 quaternary clauses 43% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [quatres-9-2] added 2 single-self-subsuming ternary resolvents
c [ternres-9] limit 4000000 with penalty 0 = 0 + 0
c [ternres-9] all 3050 free variables schedulable
c [ternres-9] 12 ternary resolvents (0 bin, 12 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-33] removed 2 variables
c [basicprobe-5] limit 9335069 penalty 0 = 0 + 0
c [basicprobe-5-0] 373 sched 13%, 112 failed, 10 lifted, 4134 hbrs
c [decomp-34] removed 149 variables
c [basicprobe-5-1] 89 probes remain 3% after last round
c [basicprobe-5-1] 184 units = 172 failed (93%) + 12 lifted (7%)
c [basicprobe-5-1] removed 231 variables, found 11289 hbrs
c [bate-3] eliminated 30 asymmetric tautologies during probing
c [unhide-13] limit 373402 with penalty 0 = 0 + 0
c [unhide-13-18] 0 units, 0 failed, 1784 tauts, 0 hbrs, 2549 literals
c [transred-9] limit 1867013 with penalty 0 = 0 + 0
c [transred-9] removed 536 transitive binary clauses
c [cce-9] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 19 (5%) of length 7
c [cce-9-1] eliminated 16 clauses out of 684 (2%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 17 large clauses in 2553452 steps
c [cce-9-1] allowing another 1276726 steps for small clauses
c [cce-9-1] scheduling 11216 clauses = 8979 binary + 2237 ternary
c [cce-9-1] tried to eliminate 8908 small clauses 79%
c [cce-9-1] eliminated 576 binary clauses 6%
c [cce-9-1] eliminated 95 ternary clauses 4%
c [cce-9-1] eliminated 671 small clauses 6%
c [cce-9-1] eliminated 671 small clauses in 30000001 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 688 covered clauses in round 1
c [cce-9] eliminated 688 covered clauses in TOTAL during 1 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 2819 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 163 variables 6% in round 1 in 909768 steps
c [elim-13-1] backward subsumption/strengthening limit 909700
c [elim-13-1-1] backward checking 804 touched variables 29%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 7 clauses in 86218 steps
c [elim-13-1] rescheduled 21 variables 1% by backward subsumption
c [elim-13-2] eliminated 2 variables 0% in round 2 in 10660 steps
c [elim-13-2] backward subsumption/strengthening limit 10600
c [elim-13-2-1] backward checking 5 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 0 and strengthened 8 clauses in 4622 steps
c [elim-13-2] rescheduled 12 variables 0% by backward subsumption
c [elim-13-3] eliminated 1 variables 0% in round 3 in 4588 steps
c [elim-13-3] backward subsumption/strengthening limit 4500
c [elim-13-3-1] backward checking 0 touched variables 0%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 0 and strengthened 0 clauses in 2604 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 166 = 6% variables out of 2819 scheduled
c [bca-9] limit of 10000000 steps and 29877 added (scaled 2)
c [bca-9] 3317 out of 5308 literals actually usable 62%
c [bca-9] added 11 blocked clauses in 15266 steps
c [sweep-9] limit 1000000 penalty 0 = 0 + 0
c [sweep-9-1] 284 pos 27.8% + 737 neg 72.2% = 1021 sched 38.5% ret 1632
c [sweep-9-1] 1011736 steps 83 queries 20.24 avg class size
c [sweep-9-1] 1201 decisions 82 SAT calls 55.22 avg env size
c [sweep-9-1] 538 variables remain 20% (2111 retained 80%)
c [decomp-35] removed 4 variables
c [sweep-9-1] removed 4 vars (0 failed, 1 eqs, 2 impls)
c [sweep-9] removed 4 vars in TOTAL (1 rounds, 82 queries)
c [sort-queue-13] sorted 2649 enqueued variables after 21151 conflicts
c [score-dist-13] active 0 (0%), one 2189 (83%), zero 460 (17%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 401 variables 13.1% (2649 remain 1%)
c [simplification-13] removed 2597 irredundant clauses 15.1% (14644 remain 1%)
c [simplification-13] maximum reduction of 15% = max (13%, 15%)
c [simplification-13] large reduction 15% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 33151 (soft 23151 + delta 10000)
c [simplification-13] new conflict limit 23151 (hard 33151)
c 
c [simplification-14] limit 23151 conflicts (hard 33151) hit after 23151 conflicts
c [quatres-10] found 842 quaternary clauses 40% in total
c [quatres-10-2] added 2 quaternary resolvents
c [ternres-10] limit 4000000 with penalty 0 = 0 + 0
c [ternres-10] all 2649 free variables schedulable
c [ternres-10] 18 ternary resolvents (0 bin, 18 trn)
c [ternres-10] fully completed ternary resolution
c [simpleprobe-6] all 2649 free variables schedulable
c [simpleprobe-6] limit 7790879 penalty 0 = 0 + 0
c [decomp-37] removed 1 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 1 variables, found 1481 hbrs, 1 units
c [transred-10] limit 1947719 with penalty 0 = 0 + 0
c [transred-10] removed 942 transitive binary clauses
c [transred-10] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 2646 variables 100%
c [block-4] limit of 6250000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 2 blocked clauses
c [block-4] 2 < 1/100 * 14624 = 146 considered unsuccessful
c [cce-10] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 2 clauses out of 8 (25%) of length 9
c [cce-10-1] eliminated 2 clauses out of 338 (1%) of length 5
c [cce-10-1] eliminated 7 clauses out of 709 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 11 large clauses in 2871335 steps
c [cce-10-1] allowing another 1435667 steps for small clauses
c [cce-10-1] scheduling 11255 clauses = 8069 binary + 3186 ternary
c [cce-10-1] tried to eliminate 9304 small clauses 83%
c [cce-10-1] eliminated 106 binary clauses 1%
c [cce-10-1] eliminated 45 ternary clauses 1%
c [cce-10-1] eliminated 151 small clauses 1%
c [cce-10-1] eliminated 151 small clauses in 30000000 steps
c [cce-10-1] incomplete small round (ATE)
c [cce-10-1] eliminated 162 covered clauses in round 1
c [cce-10] eliminated 162 covered clauses in TOTAL during 1 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 2646 variables 100%
c [elim-14] limit of 38954398 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 17 variables 1% in round 1 in 880505 steps
c [elim-14-1] backward subsumption/strengthening limit 880500
c [elim-14-1-1] backward checking 128 touched variables 5%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 2 clauses in 15125 steps
c [elim-14-1] rescheduled 19 variables 1% by backward subsumption
c [elim-14-2] eliminated 1 variables 0% in round 2 in 6092 steps
c [elim-14-2] backward subsumption/strengthening limit 6000
c [elim-14-2-1] backward checking 17 touched variables 1%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 0 and strengthened 2 clauses in 4011 steps
c [elim-14-2] rescheduled 9 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 3020 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 18 = 1% variables out of 2646 scheduled
c [elim-14] 18 < 1/100 * 2646 = 26 considered unsuccessful
c [bca-10] limit of 10000000 steps and 29396 added (scaled 2)
c [bca-10] 3206 out of 5258 literals actually usable 61%
c [bca-10] added 3 blocked clauses in 16865 steps
c [sweep-10] limit 1000000 penalty 0 = 0 + 0
c [sweep-10-1] 169 pos 31.8% + 362 neg 68.2% = 531 sched 20.2% ret 2097
c [sweep-10-1] 1131468 steps 89 queries 15.29 avg class size
c [sweep-10-1] 997 decisions 88 SAT calls 36.85 avg env size
c [sweep-10-1] 257 variables remain 10% (2371 retained 90%)
c [sweep-10-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-10] removed 0 vars in TOTAL (1 rounds, 88 queries)
c [sort-queue-14] sorted 2628 enqueued variables after 23151 conflicts
c [score-dist-14] active 0 (0%), one 2185 (83%), zero 443 (17%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 21 variables 0.8% (2628 remain 1%)
c [simplification-14] removed 222 irredundant clauses 1.5% (14422 remain 1%)
c [simplification-14] maximum reduction of 2% = max (1%, 2%)
c [simplification-14] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-14] new conflict interval 6666
c [simplification-14] penalized conflict interval 6666 = 1 * 6666
c [simplification-14] hard conflict limit 39817 (soft 29817 + delta 10000)
c [simplification-14] new conflict limit 29817 (hard 39817)
c 
c [simplification-15] limit 29817 conflicts (hard 39817) hit after 29818 conflicts
c [quatres-11] found 871 quaternary clauses 36% in total
c [ternres-11] limit 4000000 with penalty 0 = 0 + 0
c [ternres-11] all 2628 free variables schedulable
c [ternres-11] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 125000 penalty 4 = 4 + 0
c [card-5] found 314 at-most-one constraints of average size 3.5
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 125000 for elimination
c [card-5] 314 out of 314 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-5] limit 250000 penalty 3 = 3 + 0
c [gauss-5] extracted 3 xors of average arity 3.0
c [gauss-5] connected 9 occurrences of 6 variables (average 1.5)
c [gauss-5] limit 250000 penalty 3 = 3 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-6] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 5246 literals 100%
c [treelook-6] scheduling used 116251 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 306710 steps
c [treelook-6] 5191 literals remain 99%
c [treelook-6] 2598 variables remain to probed next time 99%
c [treelook-6] removed 1 variables, found 1269 hbrs
c [unhide-14] limit 224470 with penalty 1 = 1 + 0
c [unhide-14-19] 0 units, 0 failed, 1426 tauts, 0 hbrs, 11000 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 397 transitive binary clauses
c [cce-11] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 1 clauses out of 2 (50%) of length 15
c [cce-11-1] eliminated 1 clauses out of 15 (7%) of length 8
c [cce-11-1] eliminated 4 clauses out of 337 (1%) of length 5
c [cce-11-1] eliminated 16 clauses out of 700 (2%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 22 large clauses in 2904380 steps
c [cce-11-1] allowing another 1452190 steps for small clauses
c [cce-11-1] scheduling 10059 clauses = 7942 binary + 2117 ternary
c [cce-11-1] tried to eliminate 8998 small clauses 89%
c [cce-11-1] eliminated 106 binary clauses 1%
c [cce-11-1] eliminated 56 ternary clauses 3%
c [cce-11-1] eliminated 162 small clauses 2%
c [cce-11-1] eliminated 162 small clauses in 30000003 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 184 covered clauses in round 1
c [cce-11] eliminated 184 covered clauses in TOTAL during 1 rounds
c [bca-11] limit of 10000000 steps and 29010 added (scaled 2)
c [bca-11] 2968 out of 5256 literals actually usable 56%
c [bca-11] added 4 blocked clauses in 22653 steps
c [sort-queue-15] sorted 2627 enqueued variables after 29818 conflicts
c [score-dist-15] active 0 (0%), one 2220 (85%), zero 407 (15%)
c [score-dist-15] max exp 1, different 2 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 1 variables 0.0% (2627 remain 1%)
c [simplification-15] removed 194 irredundant clauses 1.3% (14228 remain 1%)
c [simplification-15] maximum reduction of 1% = max (0%, 1%)
c [simplification-15] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-15] new conflict interval 16666
c [simplification-15] penalized conflict interval 16666 = 1 * 16666
c [simplification-15] hard conflict limit 56484 (soft 46484 + delta 10000)
c [simplification-15] new conflict limit 46484 (hard 56484)
c 
c [simplification-16] limit 46484 conflicts (hard 56484) hit after 46486 conflicts
c [ternres-12] limit 4000000 with penalty 0 = 0 + 0
c [ternres-12] all 2627 free variables schedulable
c [ternres-12] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-12] fully completed ternary resolution
c [basicprobe-6] limit 16158378 penalty 0 = 0 + 0
c [basicprobe-6-0] 224 sched 9%, 25 failed, 0 lifted, 1046 hbrs
c [decomp-42] removed 29 variables
c [basicprobe-6-1] 685 sched 27%, 22 failed, 0 lifted, 1155 hbrs
c [decomp-43] removed 32 variables
c [basicprobe-6-2] 679 sched 27%, 4 failed, 0 lifted, 1000 hbrs
c [decomp-44] removed 4 variables
c [basicprobe-6-3] 501 probes remain 20% after last round
c [basicprobe-6-3] 52 units = 52 failed (100%) + 0 lifted (0%)
c [basicprobe-6-3] removed 66 variables, found 3264 hbrs
c [bate-4] eliminated 11 asymmetric tautologies during probing
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 437 transitive binary clauses
c [cce-12] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 116 (1%) of length 6
c [cce-12-1] eliminated 1 clauses out of 327 (0%) of length 5
c [cce-12-1] eliminated 3 clauses out of 665 (0%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 5 large clauses in 2471007 steps
c [cce-12-1] allowing another 1235503 steps for small clauses
c [cce-12-1] scheduling 9785 clauses = 7850 binary + 1935 ternary
c [cce-12-1] tried to eliminate 9785 small clauses 100%
c [cce-12-1] eliminated 148 binary clauses 2%
c [cce-12-1] eliminated 10 ternary clauses 1%
c [cce-12-1] eliminated 158 small clauses 2%
c [cce-12-1] eliminated 165 small clauses in 29596366 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 170 covered clauses in round 1
c [cce-12-2] incomplete large round (ATE)
c [cce-12-2] allowing another 201818 steps for small clauses
c [cce-12-2] scheduling 9627 clauses = 7702 binary + 1925 ternary
c [cce-12-2] tried to eliminate 82 small clauses 1%
c [cce-12-2] incomplete small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 170 covered clauses in TOTAL during 2 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 2561 variables 100%
c [elim-15] limit of 32316757 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 48 variables 2% in round 1 in 820263 steps
c [elim-15-1] backward subsumption/strengthening limit 820200
c [elim-15-1-1] backward checking 297 touched variables 12%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 32889 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 48 = 2% variables out of 2561 scheduled
c [bca-12] limit of 10000000 steps and 27750 added (scaled 2)
c [bca-12] 2529 out of 5028 literals actually usable 50%
c [bca-12] added 8 blocked clauses in 36984 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 5000000 penalty 1 = 1 + 0
c [sweep-11-1] 74 pos 29.7% + 175 neg 70.3% = 249 sched 9.9% ret 2264
c [sweep-11-1] 2516377 steps 133 queries 5.49 avg class size
c [sweep-11-1] 1688 decisions 132 SAT calls 43.14 avg env size
c [sweep-11-1] fully completed sweeping round
c [sweep-11-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-11-2] 461 pos 18.3% + 2052 neg 81.7% = 2513 sched 100.0% ret 0
c [sweep-11-2] 2842672 steps 49 queries 98.04 avg class size
c [sweep-11-2] 1550 decisions 48 SAT calls 175.17 avg env size
c [sweep-11-2] 1112 variables remain 44% (1398 retained 56%)
c [decomp-46] removed 3 variables
c [sweep-11-2] removed 3 vars (0 failed, 1 eqs, 0 impls)
c [sweep-11] removed 3 vars in TOTAL (2 rounds, 180 queries)
c [sort-queue-16] sorted 2510 enqueued variables after 46486 conflicts
c [score-dist-16] active 0 (0%), one 2191 (87%), zero 319 (13%)
c [score-dist-16] max exp 1, different 2 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 117 variables 4.5% (2510 remain 1%)
c [simplification-16] removed 648 irredundant clauses 4.6% (13580 remain 1%)
c [simplification-16] maximum reduction of 5% = max (4%, 5%)
c [simplification-16] large reduction 5% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 58486 (soft 48486 + delta 10000)
c [simplification-16] new conflict limit 48486 (hard 58486)
c 
c [simplification-17] limit 48486 conflicts (hard 58486) hit after 48486 conflicts
c [quatres-12] found 925 quaternary clauses 31% in total
c [quatres-12-2] added 7 quaternary resolvents
c [ternres-13] limit 4000000 with penalty 0 = 0 + 0
c [ternres-13] all 2510 free variables schedulable
c [ternres-13] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-13] fully completed ternary resolution
c [simpleprobe-7] all 2510 free variables schedulable
c [simpleprobe-7] limit 13469909 penalty 0 = 0 + 0
c [decomp-48] removed 1 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 1 variables, found 979 hbrs, 0 units
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 641 transitive binary clauses
c [cce-13] boosting limit by 10
c [cce-13] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-13-1] eliminated 1 clauses out of 31 (3%) of length 7
c [cce-13-1] eliminated 4 clauses out of 124 (3%) of length 6
c [cce-13-1] eliminated 1 clauses out of 321 (0%) of length 5
c [cce-13-1] eliminated 9 clauses out of 679 (1%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 15 large clauses in 2634952 steps
c [cce-13-1] allowing another 1317476 steps for small clauses
c [cce-13-1] scheduling 9526 clauses = 7607 binary + 1919 ternary
c [cce-13-1] tried to eliminate 9526 small clauses 100%
c [cce-13-1] eliminated 34 binary clauses 0%
c [cce-13-1] eliminated 25 ternary clauses 1%
c [cce-13-1] eliminated 59 small clauses 1%
c [cce-13-1] eliminated 59 small clauses in 29626916 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] completed small and large (ACCE)
c [cce-13-1] eliminated 74 covered clauses in round 1
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] allowing another 1302406 steps for small clauses
c [cce-13-2] scheduling 9467 clauses = 7573 binary + 1894 ternary
c [cce-13-2] tried to eliminate 9467 small clauses 100%
c [cce-13-2] eliminated 2 binary clauses 0%
c [cce-13-2] eliminated 2 ternary clauses 0%
c [cce-13-2] eliminated 4 small clauses 0%
c [cce-13-2] eliminated 4 small clauses in 29371766 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 4 covered clauses in round 2
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] allowing another 1302252 steps for small clauses
c [cce-13-3] scheduling 9463 clauses = 7571 binary + 1892 ternary
c [cce-13-3] tried to eliminate 9463 small clauses 100%
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 0 covered clauses in round 3
c [cce-13] eliminated 78 covered clauses in TOTAL during 3 rounds
c [cce-13] 78 < 1/100 * 13573 = 135 considered unsuccessful
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 2509 variables 100%
c [elim-16] limit of 67349548 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 7 variables 0% in round 1 in 810459 steps
c [elim-16-1] backward subsumption/strengthening limit 810400
c [elim-16-1-1] backward checking 89 touched variables 4%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 0 and strengthened 2 clauses in 11447 steps
c [elim-16-1] rescheduled 20 variables 1% by backward subsumption
c [elim-16-2] no variable eliminated in round 2 in 9645 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 7 = 0% variables out of 2509 scheduled
c [elim-16] 7 < 1/100 * 2509 = 25 considered unsuccessful
c [bca-13] limit of 10000000 steps and 27540 added (scaled 2)
c [bca-13] 2465 out of 5006 literals actually usable 49%
c [bca-13] added 2 blocked clauses in 39274 steps
c [sweep-12] limit 1010243 penalty 0 = 0 + 0
c [sweep-12-1] 256 pos 23.1% + 852 neg 76.9% = 1108 sched 44.3% ret 1394
c [sweep-12-1] 1169327 steps 9 queries 176.78 avg class size
c [sweep-12-1] 549 decisions 8 SAT calls 189.12 avg env size
c [sweep-12-1] 1072 variables remain 43% (1430 retained 57%)
c [sweep-12-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-12] removed 0 vars in TOTAL (1 rounds, 8 queries)
c [sort-queue-17] sorted 2502 enqueued variables after 48486 conflicts
c [score-dist-17] active 0 (0%), one 2186 (87%), zero 316 (13%)
c [score-dist-17] max exp 1, different 2 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 8 variables 0.3% (2502 remain 1%)
c [simplification-17] removed 90 irredundant clauses 0.7% (13490 remain 1%)
c [simplification-17] maximum reduction of 1% = max (0%, 1%)
c [simplification-17] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-17] new conflict interval 26666
c [simplification-17] penalized conflict interval 26666 = 1 * 26666
c [simplification-17] hard conflict limit 88485 (soft 75152 + delta 13333)
c [simplification-17] new conflict limit 75152 (hard 88485)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   40.9    2501    13490     54326   39728    451 15891   23    51   23  45%    396   24   21   11  191%
c -   43.8    2500    13490     67325   15658    469 15898   23    53   19  44%     77   21   25   13  187%
c 
c [simplification-18] limit 75152 conflicts (hard 88485) hit after 75153 conflicts
c [quatres-13] found 988 quaternary clauses 29% in total
c [ternres-14] limit 5017784 with penalty 0 = 0 + 0
c [ternres-14] all 2500 free variables schedulable
c [ternres-14] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-50] removed 2 variables
c [treelook-7] limit 501778 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 4990 literals 100%
c [treelook-7] scheduling used 129353 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 501778 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 502187 steps
c [treelook-7] 4779 literals remain 96%
c [treelook-7] 2471 variables remain to probed next time 99%
c [treelook-7] removed 0 variables, found 624 hbrs
c [unhide-15] limit 250889 with penalty 2 = 2 + 0
c [unhide-15-20] 0 units, 0 failed, 43 tauts, 0 hbrs, 7096 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 485 transitive binary clauses
c [bca-14] limit of 10000000 steps and 27525 added (scaled 2)
c [bca-14] 2596 out of 5002 literals actually usable 52%
c [bca-14] added 6 blocked clauses in 28929 steps
c [sort-queue-18] sorted 2500 enqueued variables after 75153 conflicts
c [score-dist-18] active 0 (0%), one 2197 (88%), zero 303 (12%)
c [score-dist-18] max exp 1, different 2 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 0 variables 0.0% (2500 remain 1%)
c [simplification-18] removed 8 irredundant clauses 0.1% (13482 remain 1%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] full geometric conflict interval increment 26666
c [simplification-18] new conflict interval 53332
c [simplification-18] penalized conflict interval 53332 = 1 * 53332
c [simplification-18] hard conflict limit 155151 (soft 128485 + delta 26666)
c [simplification-18] new conflict limit 128485 (hard 155151)
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 -   51.6    2500    13482    106747   21410    482 15928   21    42   18  51%    505    2   17   18   94%
c -   56.4    2500    13482    143020   26795    491 15931   18    26   15  68%    726  -10   17   18   98%
c 
c [simplification-19] limit 128485 conflicts (hard 155151) hit after 155151 conflicts
c [ternres-15] limit 9588672 with penalty 0 = 0 + 0
c [ternres-15] all 2500 free variables schedulable
c [ternres-15] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-15] fully completed ternary resolution
c [basicprobe-7] limit 47943361 penalty 0 = 0 + 0
c [basicprobe-7-0] 526 sched 21%, 5 failed, 0 lifted, 1172 hbrs
c [decomp-53] removed 7 variables
c [basicprobe-7-1] 684 sched 28%, 5 failed, 0 lifted, 550 hbrs
c [decomp-54] removed 6 variables
c [basicprobe-7-2] 679 sched 27%, 0 failed, 0 lifted, 76 hbrs
c [basicprobe-7-3] 679 sched 27%, 0 failed, 0 lifted, 50 hbrs
c [basicprobe-7-4] 679 sched 27%, 0 failed, 0 lifted, 20 hbrs
c [basicprobe-7-5] 679 sched 27%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-7-6] 679 sched 27%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-7-7] 47 probes remain 2% after last round
c [basicprobe-7-7] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-7-7] removed 13 variables, found 1881 hbrs
c [bate-5] eliminated 9 asymmetric tautologies during probing
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 456 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 2487 variables 100%
c [block-5] limit of 5992920 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 2 blocked clauses
c [block-5] 2 < 1/100 * 13354 = 133 considered unsuccessful
c [cce-14] limit of 23971680 steps penalty 1 = 1 + 0
c [cce-14-1] eliminated 1 clauses out of 6 (17%) of length 9
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 1 large clauses in 2527335 steps
c [cce-14-1] allowing another 1263667 steps for small clauses
c [cce-14-1] scheduling 10319 clauses = 7592 binary + 2727 ternary
c [cce-14-1] tried to eliminate 8175 small clauses 79%
c [cce-14-1] eliminated 41 binary clauses 1%
c [cce-14-1] eliminated 20 ternary clauses 1%
c [cce-14-1] eliminated 61 small clauses 1%
c [cce-14-1] eliminated 61 small clauses in 23971689 steps
c [cce-14-1] incomplete small round (ATE)
c [cce-14-1] eliminated 62 covered clauses in round 1
c [cce-14] eliminated 62 covered clauses in TOTAL during 1 rounds
c [cce-14] 62 < 1/100 * 13352 = 133 considered unsuccessful
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 2487 variables 100%
c [elim-17] limit of 95886723 steps penalty 1 = 1 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 12 variables 0% in round 1 in 794518 steps
c [elim-17-1] backward subsumption/strengthening limit 794500
c [elim-17-1-1] backward checking 77 touched variables 3%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 10134 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 12 = 0% variables out of 2487 scheduled
c [elim-17] 12 < 1/100 * 2487 = 24 considered unsuccessful
c [bca-15] limit of 10000000 steps and 27128 added (scaled 2)
c [bca-15] 2529 out of 4952 literals actually usable 51%
c [bca-15] added 7 blocked clauses in 43380 steps
c [sweep-13] limit 1438300 penalty 1 = 1 + 0
c [sweep-13-1] 288 pos 27.2% + 771 neg 72.8% = 1059 sched 42.8% ret 1416
c [sweep-13-1] 1615585 steps 31 queries 56.52 avg class size
c [sweep-13-1] 841 decisions 30 SAT calls 99.13 avg env size
c [sweep-13-1] 835 variables remain 34% (1640 retained 66%)
c [sweep-13-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-13] removed 0 vars in TOTAL (1 rounds, 30 queries)
c [sort-queue-19] sorted 2475 enqueued variables after 155151 conflicts
c [score-dist-19] active 0 (0%), one 2204 (89%), zero 271 (11%)
c [score-dist-19] max exp 1, different 2 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 25 variables 1.0% (2475 remain 1%)
c [simplification-19] removed 200 irredundant clauses 1.5% (13282 remain 1%)
c [simplification-19] maximum reduction of 1% = max (1%, 1%)
c [simplification-19] geometric conflict interval increment 26666 = 53332 / 2
c [simplification-19] new conflict interval 79998
c [simplification-19] penalized conflict interval 79998 = 1 * 79998
c [simplification-19] hard conflict limit 275148 (soft 235149 + delta 39999)
c [simplification-19] new conflict limit 235149 (hard 275148)
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 -   63.5    2475    13282    175007   27264    489 15648   17    28   16  60%    841   -5   17   17   97%
c -   68.2    2475    13282    210180   28945    499 15649   11    14   21  79%    917  -14   12   16   72%
c i   70.7    2474    13282    228633   45667    526 15657    9    11   28  79%    943  -14    6   15   43%
c -   74.5    2474    13282    244350   28369    538 15659   24    50   21  48%  -1216   21   25   17  151%
c i   78.0    2473    13282    271797   53056    544 15665   11    13   28  86%   -450  -13   10   16   67%
c 
c [simplification-20] limit 235149 conflicts (hard 275148) hit after 275148 conflicts
c [quatres-14] found 1129 quaternary clauses 20% in total
c [ternres-16] limit 16629286 with penalty 0 = 0 + 0
c [ternres-16] all 2468 free variables schedulable
c [ternres-16] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-6] limit 207866 penalty 4 = 4 + 0
c [gauss-6] extracted 5 xors of average arity 3.0
c [gauss-6] connected 15 occurrences of 12 variables (average 1.2)
c [gauss-6] limit 207866 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-8] all 2468 free variables schedulable
c [simpleprobe-8] limit 66517146 penalty 0 = 0 + 0
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 0 variables, found 800 hbrs, 0 units
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 527 transitive binary clauses
c [bca-16] limit of 10000000 steps and 26971 added (scaled 2)
c [bca-16] 2537 out of 4938 literals actually usable 51%
c [bca-16] added 7 blocked clauses in 40007 steps
c [sort-queue-20] sorted 2468 enqueued variables after 275148 conflicts
c [score-dist-20] active 0 (0%), one 2211 (90%), zero 257 (10%)
c [score-dist-20] max exp 1, different 2 (100%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 0 variables 0.0% (2468 remain 1%)
c [simplification-20] removed 80 irredundant clauses 0.6% (13202 remain 1%)
c [simplification-20] maximum reduction of 1% = max (0%, 1%)
c [simplification-20] geometric conflict interval increment 39999 = 79998 / 2
c [simplification-20] new conflict interval 119997
c [simplification-20] penalized conflict interval 119997 = 1 * 119997
c [simplification-20] hard conflict limit 455143 (soft 395145 + delta 59998)
c [simplification-20] new conflict limit 395145 (hard 455143)
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 -   84.8    2468    13202    303140   26930    524 15820   25    49   20  50%   -314   17   26   18  139%
c -   90.4    2468    13202    342030   32038    536 15824   15    20   21  74%    285  -10   16   17   91%
c -   96.8    2468    13202    376255   30250    551 15827   19    41   21  47%    585    7   21   19  109%
c 
c [simplification-21] limit 395145 conflicts (hard 455143) hit after 411081 conflicts
c [ternres-17] limit 25726129 with penalty 0 = 0 + 0
c [ternres-17] all 2468 free variables schedulable
c [ternres-17] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 803941 penalty 4 = 4 + 0
c [card-6] found 1085 at-most-one constraints of average size 3.3
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 803941 for elimination
c [card-6] 1085 out of 1085 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] generated 235 at-most-one constraints, 229 used 97%
c [card-6] exported 1598 binary clauses, 7.0 per/constraint
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 469 transitive binary clauses
c [bca-17] limit of 10000000 steps and 26975 added (scaled 2)
c [bca-17] 2468 out of 4938 literals actually usable 50%
c [bca-17] added 5 blocked clauses in 67631 steps
c [sort-queue-21] sorted 2468 enqueued variables after 411081 conflicts
c [score-dist-21] active 0 (0%), one 2223 (90%), zero 245 (10%)
c [score-dist-21] max exp 1, different 2 (100%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 0 variables 0.0% (2468 remain 1%)
c [simplification-21] removed 0 irredundant clauses 0.0% (13202 remain 1%)
c [simplification-21] maximum reduction of 0% = max (0%, 0%)
c [simplification-21] full geometric conflict interval increment 119997
c [simplification-21] new conflict interval 239994
c [simplification-21] penalized conflict interval 239994 = 1 * 239994
c [simplification-21] hard conflict limit 771072 (soft 651075 + delta 119997)
c [simplification-21] new conflict limit 651075 (hard 771072)
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 -  103.1    2468    13202    414856   32606    567 16962   20    35   18  56%    781    4   15   18   84%
c -  110.1    2468    13202    451369   32153    578 16964   18    33   18  56%    885    0   15   19   81%
c -  116.6    2468    13202    490978   34189    583 16965   15    29   26  53%    948   -3   18   18   98%
c -  123.3    2468    13202    529138   34319    595 16972   21    39   26  55%    981    5   20   19  103%
c -  130.0    2468    13202    567813   35639    611 16976   19    32   18  60%   1000   -4   13   21   64%
c -  136.1    2468    13202    607788   37626    613 16976   24    40   25  58%   1011    8   34   20  171%
c -  142.6    2468    13202    646248   37386    622 16978   21    37   25  57%   1017    1   21   21  100%
c 
c [simplification-22] limit 651075 conflicts (hard 771072) hit after 663277 conflicts
c [ternres-18] limit 42898605 with penalty 0 = 0 + 0
c [ternres-18] all 2468 free variables schedulable
c [ternres-18] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-18] fully completed ternary resolution
c [treelook-8] limit 2144930 penalty 1 = 1 + 0 boost 1
c [treelook-8] scheduled 4926 literals 100%
c [treelook-8] scheduling used 195335 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 2144930 penalty 1 = 1 + 0 boost 1
c [treelook-8] used 2152042 steps
c [treelook-8] 4748 literals remain 96%
c [treelook-8] 2439 variables remain to probed next time 99%
c [treelook-8] removed 0 variables, found 20184 hbrs
c [unhide-16] limit 1072465 with penalty 3 = 3 + 0
c [unhide-16-22] 0 units, 0 failed, 8386 tauts, 0 hbrs, 36158 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 405 transitive binary clauses
c [cce-15] limit of 53623257 steps penalty 2 = 2 + 0
c [cce-15-1] eliminated 2 clauses out of 681 (0%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 2 large clauses in 2744280 steps
c [cce-15-1] allowing another 1372140 steps for small clauses
c [cce-15-1] scheduling 10181 clauses = 7542 binary + 2639 ternary
c [cce-15-1] tried to eliminate 10181 small clauses 100%
c [cce-15-1] eliminated 59 binary clauses 1%
c [cce-15-1] eliminated 71 ternary clauses 3%
c [cce-15-1] eliminated 130 small clauses 1%
c [cce-15-1] eliminated 130 small clauses in 30859781 steps
c [cce-15-1] completed small round (ACCE)
c [cce-15-1] eliminated 132 covered clauses in round 1
c [cce-15-2] eliminated 4 clauses out of 679 (1%) of length 4
c [cce-15-2] completed large round (ACCE)
c [cce-15-2] eliminated 4 large clauses in 2718810 steps
c [cce-15-2] allowing another 1359405 steps for small clauses
c [cce-15-2] scheduling 10051 clauses = 7483 binary + 2568 ternary
c [cce-15-2] tried to eliminate 7415 small clauses 74%
c [cce-15-2] eliminated 8 binary clauses 0%
c [cce-15-2] eliminated 2 ternary clauses 0%
c [cce-15-2] eliminated 10 small clauses 0%
c [cce-15-2] eliminated 10 small clauses in 22763480 steps
c [cce-15-2] incomplete small round (ACCE)
c [cce-15-2] eliminated 14 covered clauses in round 2
c [cce-15] eliminated 146 covered clauses in TOTAL during 2 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 2468 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 4000000000 steps penalty 2 = 2 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 17 variables 1% in round 1 in 773992 steps
c [elim-18-1] backward subsumption/strengthening limit 773900
c [elim-18-1-1] backward checking 111 touched variables 4%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 0 and strengthened 3 clauses in 12172 steps
c [elim-18-1] rescheduled 6 variables 0% by backward subsumption
c [elim-18-2] eliminated 1 variables 0% in round 2 in 2496 steps
c [elim-18-2] backward subsumption/strengthening limit 2400
c [elim-18-2-1] backward checking 9 touched variables 0%
c [elim-18-2-1] incomplete backward checking 0 remain 0%
c [elim-18-2] subsumed 0 and strengthened 0 clauses in 2401 steps
c [elim-18-2] fully rescheduled 2450 variables 99%
c [elim-18-3] eliminated 1 variables 0% in round 3 in 773217 steps
c [elim-18-3] backward subsumption/strengthening limit 773200
c [elim-18-3-1] backward checking 25 touched variables 1%
c [elim-18-3-1] fully completed backward checking in 1 rounds
c [elim-18-3] subsumed 0 and strengthened 0 clauses in 3895 steps
c [elim-18] fully completed in 3 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 19 = 1% variables out of 2468 scheduled
c [elim-18] 19 < 1/100 * 2468 = 24 considered unsuccessful
c [bca-18] limit of 10000000 steps and 26649 added (scaled 2)
c [bca-18] 2435 out of 4900 literals actually usable 50%
c [bca-18] added 8 blocked clauses in 58491 steps
c [sweep-14] limit 3217395 penalty 2 = 2 + 0
c [sweep-14-1] 226 pos 27.3% + 603 neg 72.7% = 829 sched 33.9% ret 1620
c [sweep-14-1] 3217437 steps 47 queries 27.89 avg class size
c [sweep-14-1] 949 decisions 46 SAT calls 84.46 avg env size
c [sweep-14-1] 553 variables remain 23% (1896 retained 77%)
c [sweep-14-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-14] removed 0 vars in TOTAL (1 rounds, 46 queries)
c [sort-queue-22] sorted 2449 enqueued variables after 663277 conflicts
c [score-dist-22] active 0 (0%), one 2226 (91%), zero 223 (9%)
c [score-dist-22] max exp 1, different 2 (100%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 19 variables 0.8% (2449 remain 1%)
c [simplification-22] removed 164 irredundant clauses 1.2% (13038 remain 1%)
c [simplification-22] maximum reduction of 1% = max (1%, 1%)
c [simplification-22] geometric conflict interval increment 119997 = 239994 / 2
c [simplification-22] new conflict interval 359991
c [simplification-22] penalized conflict interval 359991 = 1 * 359991
c [simplification-22] hard conflict limit 1203263 (soft 1023268 + delta 179995)
c [simplification-22] new conflict limit 1023268 (hard 1203263)
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 -  151.4    2449    13038    686625   39332    665 28306   14    20   18  71%   1020  -11   14   19   78%
c -  158.3    2449    13038    727059   40306    675 28308   18    30   19  60%   1022    5   24   16  151%
c -  165.0    2449    13038    766747   39385    678 28312   22    40   26  56%   1023   13   28   18  159%
c -  172.6    2449    13038    808426   39742    686 28313   19    32   26  61%   1023   -2   20   20   99%
c -  179.5    2449    13038    850983   42382    691 28313   13    18   26  72%   1024  -11   11   18   61%
c -  187.4    2449    13038    892369   40868    704 28316   26    46   20  56%   1024   13   23   20  112%
c -  195.3    2449    13038    937117   42257    712 28317   21    34   21  62%   1024   -1   20   21   93%
c -  202.5    2449    13038    981848   44140    719 28317   16    24   21  69%   1024  -10   13   20   65%
c 
c [simplification-23] limit 1023268 conflicts (hard 1203263) hit after 1023268 conflicts
c [quatres-15] found 1589 quaternary clauses 13% in total
c [quatres-15-1] removed 2 duplicate quaternary clauses
c [quatres-15-2] added 5 single-self-subsuming ternary resolvents
c [quatres-15-2] added 6 quaternary resolvents
c [basicprobe-8] limit 348607196 penalty 0 = 0 + 0
c [basicprobe-8-0] 80 sched 3%, 5 failed, 0 lifted, 209 hbrs
c [decomp-68] removed 8 variables
c [basicprobe-8-1] 678 sched 28%, 16 failed, 0 lifted, 1822 hbrs
c [decomp-69] removed 19 variables
c [basicprobe-8-2] 678 sched 28%, 5 failed, 0 lifted, 293 hbrs
c [decomp-70] removed 5 variables
c [basicprobe-8-3] 675 sched 28%, 0 failed, 0 lifted, 73 hbrs
c [basicprobe-8-4] 675 sched 28%, 0 failed, 0 lifted, 43 hbrs
c [basicprobe-8-5] 675 sched 28%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-8-6] 675 sched 28%, 0 failed, 0 lifted, 22 hbrs
c [basicprobe-8-7] 675 sched 28%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-8-8] 675 sched 28%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-8-8] round limit 8 hit
c [basicprobe-8-8] 26 units = 26 failed (100%) + 0 lifted (0%)
c [basicprobe-8-8] removed 32 variables, found 2498 hbrs
c [bate-6] eliminated 12 asymmetric tautologies during probing
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 485 transitive binary clauses
c [bca-19] limit of 10000000 steps and 26089 added (scaled 2)
c [bca-19] 2243 out of 4836 literals actually usable 46%
c [bca-19] added 3 blocked clauses in 87791 steps
c [sort-queue-23] sorted 2417 enqueued variables after 1023268 conflicts
c [score-dist-23] active 0 (0%), one 2226 (92%), zero 191 (8%)
c [score-dist-23] max exp 1, different 2 (100%)
c [score-dist-23] median active exp 0, avg 0.0
c [simplification-23] removed 32 variables 1.3% (2417 remain 1%)
c [simplification-23] removed 282 irredundant clauses 2.2% (12756 remain 1%)
c [simplification-23] maximum reduction of 2% = max (1%, 2%)
c [simplification-23] geometric conflict interval increment 119997 = 359991 / 3
c [simplification-23] new conflict interval 479988
c [simplification-23] penalized conflict interval 479988 = 1 * 479988
c [simplification-23] hard conflict limit 1743250 (soft 1503256 + delta 239994)
c [simplification-23] new conflict limit 1503256 (hard 1743250)
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 -  212.8    2417    12756   1025561   44743    692 29380   23    42   21  55%   1024   11   34   20  171%
c -  220.4    2417    12756   1069955   45245    697 29381   19    31   22  60%   1024    1   18   19   97%
c i  227.0    2416    12756   1109226   82018    718 29388   19    31   34  62%   1024   -0    6   19   34%
c -  228.5    2399    12756   1115950   45561    721 29388   21    38   21  54% -10954    7   17   19   87%
c -  236.3    2399    12756   1163848   47739    723 29388   14    18   22  78%  -4752  -10   12   18   66%
c -  244.2    2399    12756   1210456   47783    734 29391   19    31   31  61%  -1812    5   25   18  140%
c -  253.5    2399    12756   1258084   47548    746 29392   16    22   31  72%   -347   -9   17   19   88%
c -  262.2    2399    12756   1306564   48823    751 29394   18    27   17  64%    370   -7   15   20   78%
c -  270.2    2399    12756   1355301   50479    757 29397   16    24   23  67%    713   -9   16   19   84%
c -  280.4    2399    12756   1404437   50416    762 29400   24    44   23  56%    877   13   17   19   88%
c -  290.3    2399    12756   1454923   50819    771 29400   19    29   33  64%    956   -4   18   20   90%
c -  300.4    2399    12756   1506308   51802    778 29400   16    20   33  78%    993  -13   14   20   68%
c 
c [simplification-24] limit 1503256 conflicts (hard 1743250) hit after 1538603 conflicts
c [ternres-19] limit 55580202 with penalty 1 = 1 + 0
c [ternres-19] all 2399 free variables schedulable
c [ternres-19] 15 ternary resolvents (0 bin, 15 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-76] removed 23 variables
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 435 transitive binary clauses
c [transred-20] found 1 units
c [cce-16] limit of 277901013 steps penalty 1 = 1 + 0
c [cce-16-1] eliminated 1 clauses out of 2 (50%) of length 21
c [cce-16-1] eliminated 1 clauses out of 1 (100%) of length 15
c [cce-16-1] eliminated 2 clauses out of 121 (2%) of length 6
c [cce-16-1] eliminated 7 clauses out of 643 (1%) of length 4
c [cce-16-1] completed large round (ATE)
c [cce-16-1] eliminated 11 large clauses in 2345487 steps
c [cce-16-1] allowing another 1172743 steps for small clauses
c [cce-16-1] scheduling 9084 clauses = 7409 binary + 1675 ternary
c [cce-16-1] tried to eliminate 9084 small clauses 100%
c [cce-16-1] eliminated 87 binary clauses 1%
c [cce-16-1] eliminated 21 ternary clauses 1%
c [cce-16-1] eliminated 108 small clauses 1%
c [cce-16-1] eliminated 113 small clauses in 27102775 steps
c [cce-16-1] completed small round (ATE)
c [cce-16-1] eliminated 124 covered clauses in round 1
c [cce-16-2] completed large round (ATE)
c [cce-16-2] allowing another 1168513 steps for small clauses
c [cce-16-2] scheduling 8976 clauses = 7322 binary + 1654 ternary
c [cce-16-2] tried to eliminate 8976 small clauses 100%
c [cce-16-2] completed small round (ATE)
c [cce-16-2] eliminated 0 covered clauses in round 2
c [cce-16] eliminated 124 covered clauses in TOTAL during 2 rounds
c [cce-16] 124 < 1/100 * 12611 = 126 considered unsuccessful
c [bca-20] limit of 10000000 steps and 25553 added (scaled 2)
c [bca-20] 2246 out of 4788 literals actually usable 47%
c [bca-20] added 2 blocked clauses in 84594 steps
c [sort-queue-24] sorted 2393 enqueued variables after 1538603 conflicts
c [score-dist-24] active 0 (0%), one 2208 (92%), zero 185 (8%)
c [score-dist-24] max exp 1, different 2 (100%)
c [score-dist-24] median active exp 0, avg 0.0
c [simplification-24] removed 6 variables 0.3% (2393 remain 1%)
c [simplification-24] removed 269 irredundant clauses 2.1% (12487 remain 1%)
c [simplification-24] maximum reduction of 2% = max (0%, 2%)
c [simplification-24] geometric conflict interval increment 159996 = 479988 / 3
c [simplification-24] new conflict interval 639984
c [simplification-24] penalized conflict interval 639984 = 1 * 639984
c [simplification-24] hard conflict limit 2498579 (soft 2178587 + delta 319992)
c [simplification-24] new conflict limit 2178587 (hard 2498579)
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 -  311.6    2393    12487   1560114   52890    808 28023   14    20   21  74%   1010   -9   16   18   89%
c -  321.7    2393    12487   1611661   52322    822 28029   21    36   22  57%   1018    4   14   20   71%
c -  332.2    2393    12487   1664800   53711    835 28031   19    27   31  70%   1021   -6   19   20   97%
c -  343.1    2393    12487   1718548   53621    847 28031   19    33   31  57%   1023   -2   15   21   71%
c -  352.8    2393    12487   1773405   56237    859 28035   22    35   24  61%   1023    6   22   19  119%
c -  364.5    2393    12487   1826832   55527    866 28038   21    32   24  65%   1024   -1   17   20   84%
c -  375.4    2393    12487   1881837   56940    877 28040   20    35   25  57%   1024    2   22   20  108%
c -  387.4    2393    12487   1937651   57389    892 28045   24    42   25  56%   1024    9   17   21   81%
c i  395.3    2392    12487   1979383   94400    952 28068   12    15   35  76%   1024  -16    6   19   32%
c -  400.3    2392    12487   1997416   59638    954 28069   25    42   25  59%  -9465   11   21   19  110%
c -  411.9    2392    12487   2053373   59677    969 28073   25    42   25  58%  -3442    8   25   21  121%
c -  423.8    2392    12487   2111326   60867    973 28076   18    32   25  56%   -821   -1   19   20   96%
c -  436.7    2392    12487   2168894   62064    982 28080   14    19   37  76%    258  -12   13   19   68%
c 
c [simplification-25] limit 2178587 conflicts (hard 2498579) hit after 2178588 conflicts
c [quatres-16] found 1954 quaternary clauses 11% in total
c [quatres-16-1] removed 2 duplicate quaternary clauses
c [quatres-16-2] added 2 single-self-subsuming ternary resolvents
c [quatres-16-2] added 7 quaternary resolvents
c [ternres-20] limit 168472362 with penalty 0 = 0 + 0
c [ternres-20] all 2392 free variables schedulable
c [ternres-20] 10 ternary resolvents (0 bin, 10 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-77] removed 1 variables
c [simpleprobe-9] all 2392 free variables schedulable
c [simpleprobe-9] limit 100000000 penalty 1 = 1 + 0
c [decomp-78] removed 8 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 8 variables, found 1639 hbrs, 5 units
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 644 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 2384 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 7 blocked clauses
c [block-6] 7 < 1/100 * 12412 = 124 considered unsuccessful
c [bca-21] limit of 10000000 steps and 25390 added (scaled 2)
c [bca-21] 2168 out of 4768 literals actually usable 45%
c [bca-21] added 5 blocked clauses in 74048 steps
c [sort-queue-25] sorted 2383 enqueued variables after 2178588 conflicts
c [score-dist-25] active 0 (0%), one 2201 (92%), zero 182 (8%)
c [score-dist-25] max exp 1, different 2 (100%)
c [score-dist-25] median active exp 0, avg 0.0
c [simplification-25] removed 9 variables 0.4% (2383 remain 1%)
c [simplification-25] removed 82 irredundant clauses 0.7% (12405 remain 1%)
c [simplification-25] maximum reduction of 1% = max (0%, 1%)
c [simplification-25] geometric conflict interval increment 319992 = 639984 / 2
c [simplification-25] new conflict interval 959976
c [simplification-25] penalized conflict interval 959976 = 1 * 959976
c [simplification-25] hard conflict limit 3618552 (soft 3138564 + delta 479988)
c [simplification-25] new conflict limit 3138564 (hard 3618552)
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 -  448.0    2383    12405   2228102   62021    924 28756   15    20   22  77%    714   -8   13   18   72%
c -  460.5    2383    12405   2287094   61738    932 28758   24    41   31  57%    898   13   24   19  127%
c i  469.0    2382    12405   2333949  103151    975 28771   13    16   42  78%    962  -12   10   18   53%
c -  474.3    2382    12405   2350663   63420    980 28771   22    37   31  59%  -3385    9   27   19  145%
c -  487.7    2382    12405   2411206   63502    992 28773   24    39   26  60%   -726    5   21   21  100%
c -  500.7    2382    12405   2474948   65526   1000 28774   17    26   26  66%    362   -4   15   19   80%
c -  514.1    2382    12405   2536711   64976   1012 28775   20    35   26  56%    766    4   20   20  101%
c -  528.6    2382    12405   2598731   65965   1020 28776   24    38   38  63%    924    6   31   21  153%
c i  542.9    2381    12405   2661257  122742   1056 28792   21    33   47  64%    985    1    8   21   41%
c -  543.4    2370    12405   2663785   66693   1056 28792   18    28   26  64%  -3573   -5   15   20   74%
c -  557.9    2370    12405   2728554   68074   1072 28796   23    37   26  62%   -850    5   13   20   63%
c -  572.3    2370    12405   2795349   69901   1103 28803   25    42   27  60%    348   12   24   19  121%
c -  588.1    2370    12405   2860463   69542   1116 28809   21    33   21  64%    774   -0   19   21   92%
c -  602.8    2370    12405   2927177   71409   1127 28811   19    29   28  67%    934   -5   20   21   94%
c i  606.8    2369    12405   2950405   91916   1147 28815   12    16   38  77%    961  -15    9   19   44%
c -  617.6    2357    12405   2994676   72037   1154 28815   22    31   28  69%  -1344   -2   18   21   84%
c -  633.1    2357    12405   3063088   74653   1160 28818   19    26   29  72%    190   -4   21   19  107%
c i  635.1    2356    12405   3074029   84474   1168 28823   16    23   36  70%    318   -7    9   19   49%
c i  637.7    2353    12405   3086741   96189   1173 28829   18    29   39  63%  -1173   -0   16   19   87%
c -  649.2    2327    12405   3129148   73906   1179 28829   21    33   28  63%   -232    2   15   20   75%
c 
c [simplification-26] limit 3138564 conflicts (hard 3618552) hit after 3148800 conflicts
c [quatres-17] found 2032 quaternary clauses 11% in total
c [quatres-17-1] removed 1 duplicate quaternary clauses
c [quatres-17-2] added 4 single-self-subsuming ternary resolvents
c [quatres-17-2] added 5 quaternary resolvents
c [ternres-21] limit 200000000 with penalty 0 = 0 + 0
c [ternres-21] all 2327 free variables schedulable
c [ternres-21] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-21] fully completed ternary resolution
c [gauss-7] limit 3125000 penalty 4 = 4 + 0
c [gauss-7] extracted 26 xors of average arity 2.5
c [gauss-7] connected 64 occurrences of 16 variables (average 4.0)
c [gauss-7] limit 3125000 penalty 4 = 4 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-79] removed 2 variables
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 499 transitive binary clauses
c [transred-22] found 1 units
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 2324 variables 100%
c [elim-19] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 46 variables 2% in round 1 in 677670 steps
c [elim-19-1] backward subsumption/strengthening limit 677600
c [elim-19-1-1] backward checking 283 touched variables 12%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 0 and strengthened 1 clauses in 31994 steps
c [elim-19-1] rescheduled 12 variables 1% by backward subsumption
c [elim-19-2] no variable eliminated in round 2 in 6970 steps
c [elim-19] fully completed in 2 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 46 = 2% variables out of 2324 scheduled
c [bca-22] limit of 10000000 steps and 24252 added (scaled 2)
c [bca-22] 1953 out of 4558 literals actually usable 43%
c [bca-22] added 3 blocked clauses in 89458 steps
c [sweep-15] limit 9892212 penalty 3 = 3 + 0
c [sweep-15-1] 205 pos 39.0% + 321 neg 61.0% = 526 sched 23.1% ret 1752
c [sweep-15-1] 9927446 steps 107 queries 11.32 avg class size
c [sweep-15-1] 1946 decisions 106 SAT calls 70.07 avg env size
c [sweep-15-1] 191 variables remain 8% (2087 retained 92%)
c [sweep-15-1] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-15] removed 0 vars in TOTAL (1 rounds, 106 queries)
c [sort-queue-26] sorted 2278 enqueued variables after 3148800 conflicts
c [score-dist-26] active 0 (0%), one 2153 (95%), zero 125 (5%)
c [score-dist-26] max exp 1, different 2 (100%)
c [score-dist-26] median active exp 0, avg 0.0
c [simplification-26] removed 49 variables 2.1% (2278 remain 1%)
c [simplification-26] removed 570 irredundant clauses 4.6% (11835 remain 1%)
c [simplification-26] maximum reduction of 5% = max (2%, 5%)
c [simplification-26] large reduction 5% >= 5% limit
c [simplification-26] next conflict interval 31488 = min (3148800/100, 959976)
c [simplification-26] penalized conflict interval 31488 = 1 * 31488
c [simplification-26] hard conflict limit 3196032 (soft 3180288 + delta 15744)
c [simplification-26] new conflict limit 3180288 (hard 3196032)
c 
c [simplification-27] limit 3180288 conflicts (hard 3196032) hit after 3180289 conflicts
c [quatres-18] found 2339 quaternary clauses 10% in total
c [quatres-18-1] removed 5 duplicate quaternary clauses
c [quatres-18-2] added 3 single-self-subsuming ternary resolvents
c [quatres-18-2] added 2 quaternary resolvents
c [ternres-22] limit 200000000 with penalty 0 = 0 + 0
c [ternres-22] all 2278 free variables schedulable
c [ternres-22] 45 ternary resolvents (0 bin, 45 trn)
c [ternres-22] fully completed ternary resolution
c [unhide-17] limit 1250000 with penalty 4 = 4 + 0
c [unhide-17-23] 0 units, 1 failed, 237 tauts, 0 hbrs, 76543 literals
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 453 transitive binary clauses
c [transred-23] found 1 units
c [cce-17] limit of 333787810 steps penalty 2 = 2 + 0
c [cce-17-1] eliminated 9 clauses out of 658 (1%) of length 4
c [cce-17-1] completed large round (ACCE)
c [cce-17-1] eliminated 9 large clauses in 2477919 steps
c [cce-17-1] allowing another 1238959 steps for small clauses
c [cce-17-1] scheduling 9150 clauses = 7205 binary + 1945 ternary
c [cce-17-1] tried to eliminate 9150 small clauses 100%
c [cce-17-1] eliminated 229 binary clauses 3%
c [cce-17-1] eliminated 54 ternary clauses 3%
c [cce-17-1] eliminated 283 small clauses 3%
c [cce-17-1] eliminated 304 small clauses in 26922608 steps
c [cce-17-1] completed small round (ACCE)
c [cce-17-1] eliminated 313 covered clauses in round 1
c [cce-17-2] eliminated 2 clauses out of 305 (1%) of length 5
c [cce-17-2] eliminated 1 clauses out of 649 (0%) of length 4
c [cce-17-2] completed large round (ACCE)
c [cce-17-2] eliminated 3 large clauses in 2434666 steps
c [cce-17-2] allowing another 1217333 steps for small clauses
c [cce-17-2] scheduling 8867 clauses = 6976 binary + 1891 ternary
c [cce-17-2] tried to eliminate 8867 small clauses 100%
c [cce-17-2] eliminated 12 binary clauses 0%
c [cce-17-2] eliminated 8 ternary clauses 0%
c [cce-17-2] eliminated 20 small clauses 0%
c [cce-17-2] eliminated 20 small clauses in 26368264 steps
c [cce-17-2] completed small round (ACCE)
c [cce-17-2] eliminated 23 covered clauses in round 2
c [cce-17-3] eliminated 1 clauses out of 4 (25%) of length 9
c [cce-17-3] eliminated 1 clauses out of 118 (1%) of length 6
c [cce-17-3] eliminated 1 clauses out of 303 (0%) of length 5
c [cce-17-3] eliminated 18 clauses out of 648 (3%) of length 4
c [cce-17-3] completed large round (ACCE)
c [cce-17-3] eliminated 21 large clauses in 2426403 steps
c [cce-17-3] allowing another 1213201 steps for small clauses
c [cce-17-3] scheduling 8847 clauses = 6964 binary + 1883 ternary
c [cce-17-3] tried to eliminate 8847 small clauses 100%
c [cce-17-3] eliminated 10 binary clauses 0%
c [cce-17-3] eliminated 3 ternary clauses 0%
c [cce-17-3] eliminated 13 small clauses 0%
c [cce-17-3] eliminated 13 small clauses in 26235595 steps
c [cce-17-3] completed small round (ACCE)
c [cce-17-3] eliminated 34 covered clauses in round 3
c [cce-17] eliminated 370 covered clauses in TOTAL during 3 rounds
c [bca-23] limit of 10000000 steps and 23484 added (scaled 2)
c [bca-23] 1913 out of 4554 literals actually usable 42%
c [bca-23] added 0 blocked clauses in 118303 steps
c [sort-queue-27] sorted 2276 enqueued variables after 3180289 conflicts
c [score-dist-27] active 0 (0%), one 2152 (95%), zero 124 (5%)
c [score-dist-27] max exp 1, different 2 (100%)
c [score-dist-27] median active exp 0, avg 0.0
c [simplification-27] removed 2 variables 0.1% (2276 remain 1%)
c [simplification-27] removed 385 irredundant clauses 3.3% (11450 remain 1%)
c [simplification-27] maximum reduction of 3% = max (0%, 3%)
c [simplification-27] geometric conflict interval increment 239994 = 959976 / 4
c [simplification-27] conflict interval soft limit 1000000 reached
c [simplification-27] new conflict interval 1000000
c [simplification-27] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-27] hard conflict limit 4680289 (soft 4180289 + delta 500000)
c [simplification-27] new conflict limit 4180289 (hard 4680289)
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 -  671.6    2276    11450   3200508   70328   1125 25413   25    40   25  63%    601    7   25   21  116%
c -  688.1    2276    11450   3269537   71636   1133 25418   20    31   38  66%    877   -6   17   22   78%
c i  699.8    2275    11450   3324085  120000   1176 25430   11    14   55  79%    960  -15    7   19   36%
c -  705.1    2254    11450   3341874   73562   1178 25430   24    38   38  65%  -1897    7   21   20  105%
c -  722.3    2254    11450   3413088   74246   1208 25437   27    44   27  60%     39   13   25   21  121%
c -  739.3    2254    11450   3483926   75746   1227 25439   22    35   27  63%    690    1   18   22   81%
c -  758.1    2254    11450   3556922   76403   1249 25441   28    44   41  64%    914   13   28   20  139%
c -  776.2    2254    11450   3628084   76514   1259 25445   20    31   36  66%    987   -2   13   21   62%
c -  794.6    2254    11450   3701496   78086   1266 25445   22    34   37  64%   1012    3   30   20  147%
c -  813.9    2254    11450   3775486   78417   1293 25454   21    32   29  68%   1020    1   21   20  105%
c i  832.0    2253    11450   3842218  140059   1306 25459   24    38   51  63%   1023    4    7   22   33%
c -  833.9    2246    11450   3848886   78607   1306 25459   21    31   29  67%  -6394   -3   19   22   88%
c -  853.9    2246    11450   3923742   80288   1328 25466   26    41   29  64%  -1347    8   20   23   87%
c -  873.3    2246    11450   3998293   81307   1342 25469   24    36   29  67%    264    3   20   22   92%
c -  892.8    2246    11450   4072791   81863   1347 25474   21    31   31  69%    780   -2   27   22  122%
c i  899.9    2245    11450   4106280  112453   1362 25481   14    18   44  76%    878  -12    9   20   43%
c -  913.4    2221    11450   4149360   83361   1369 25482   17    24   31  73%  -1224   -7   13   20   63%
c 
c [simplification-28] limit 4180289 conflicts (hard 4680289) hit after 4200890 conflicts
c [quatres-19] found 2516 quaternary clauses 11% in total
c [quatres-19-1] removed 8 duplicate quaternary clauses
c [quatres-19-2] added 6 single-self-subsuming ternary resolvents
c [quatres-19-2] added 9 quaternary resolvents
c [ternres-23] limit 200000000 with penalty 0 = 0 + 0
c [ternres-23] all 2221 free variables schedulable
c [ternres-23] 27 ternary resolvents (0 bin, 27 trn)
c [ternres-23] fully completed ternary resolution
c [card-7] limit 11905699 penalty 4 = 4 + 0
c [card-7] found 1105 at-most-one constraints of average size 3.3
c [card-7] found 19 at-most-two constraints of average size 4.1
c [card-7] using previous limit 11905699 for elimination
c [card-7] 1124 out of 1124 constraints (100%) meet size limits
c [card-7] no units found
c [card-7] generated 3385 at-most-one constraints, 2555 used 75%
c [card-7] exported 9476 binary clauses, 3.7 per/constraint
c [decomp-82] removed 58 variables
c [treelook-9] limit 9524559 penalty 2 = 2 + 0 boost 1
c [treelook-9] scheduled 4426 literals 100%
c [treelook-9] scheduling used 385655 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 9524559 penalty 2 = 2 + 0 boost 1
c [treelook-9] used 9525630 steps
c [treelook-9] 2137 literals remain 49%
c [treelook-9] 1845 variables remain to probed next time 84%
c [treelook-9] removed 28 variables, found 54845 hbrs
c [transred-24] limit 2000000 with penalty 0 = 0 + 0
c [transred-24] removed 1968 transitive binary clauses
c [transred-24] found 1 units
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 2189 variables 100%
c [elim-20] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 68 variables 3% in round 1 in 606601 steps
c [elim-20-1] backward subsumption/strengthening limit 606600
c [elim-20-1-1] backward checking 376 touched variables 17%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 0 and strengthened 1 clauses in 36877 steps
c [elim-20-1] rescheduled 4 variables 0% by backward subsumption
c [elim-20-2] no variable eliminated in round 2 in 1130 steps
c [elim-20] fully completed in 2 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 68 = 3% variables out of 2189 scheduled
c [sort-queue-28] sorted 2121 enqueued variables after 4200890 conflicts
c [score-dist-28] active 0 (0%), one 2054 (97%), zero 67 (3%)
c [score-dist-28] max exp 1, different 2 (100%)
c [score-dist-28] median active exp 0, avg 0.0
c [simplification-28] removed 100 variables 4.5% (2121 remain 1%)
c [simplification-28] removed 732 irredundant clauses 6.4% (10718 remain 1%)
c [simplification-28] maximum reduction of 6% = max (5%, 6%)
c [simplification-28] large reduction 6% >= 5% limit
c [simplification-28] next conflict interval 42008 = min (4200890/100, 1000000)
c [simplification-28] penalized conflict interval 42008 = 1 * 42008
c [simplification-28] hard conflict limit 4263902 (soft 4242898 + delta 21004)
c [simplification-28] new conflict limit 4242898 (hard 4263902)
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 -  937.6    2121    10718   4234638   80302   1317 75334   26    40   29  66%    412    8   22   21  103%
c 
c [simplification-29] limit 4242898 conflicts (hard 4263902) hit after 4243896 conflicts
c [quatres-20] found 2804 quaternary clauses 11% in total
c [quatres-20-1] removed 5 duplicate quaternary clauses
c [quatres-20-2] added 2 single-self-subsuming ternary resolvents
c [quatres-20-2] added 1 quaternary resolvents
c [ternres-24] limit 200000000 with penalty 0 = 0 + 0
c [ternres-24] all 2121 free variables schedulable
c [ternres-24] 24 ternary resolvents (0 bin, 24 trn)
c [ternres-24] fully completed ternary resolution
c [basicprobe-9] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-9-0] 624 sched 30%, 14 failed, 1 lifted, 561 hbrs
c [decomp-85] removed 14 variables
c [basicprobe-9-1] 617 sched 29%, 3 failed, 0 lifted, 50 hbrs
c [decomp-86] removed 5 variables
c [basicprobe-9-2] 615 sched 29%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-9-3] 615 sched 29%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-9-4] 615 sched 29%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-9-5] 615 sched 29%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-9-6] 615 sched 29%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-9-7] 615 sched 29%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-9-7] fully completed probing
c [basicprobe-9-7] 18 units = 17 failed (94%) + 1 lifted (6%)
c [basicprobe-9-7] removed 19 variables, found 625 hbrs
c [bate-7] eliminated 19 asymmetric tautologies during probing
c [transred-25] limit 2000000 with penalty 0 = 0 + 0
c [transred-25] removed 1453 transitive binary clauses
c [cce-18] almost no limit of 4000000000 steps
c [cce-18-1] eliminated 6 clauses out of 650 (1%) of length 4
c [cce-18-1] completed large round (ATE)
c [cce-18-1] eliminated 6 large clauses in 2083156 steps
c [cce-18-1] allowing another 1041578 steps for small clauses
c [cce-18-1] scheduling 8182 clauses = 6745 binary + 1437 ternary
c [cce-18-1] tried to eliminate 8182 small clauses 100%
c [cce-18-1] eliminated 135 binary clauses 2%
c [cce-18-1] eliminated 28 ternary clauses 2%
c [cce-18-1] eliminated 163 small clauses 2%
c [cce-18-1] eliminated 163 small clauses in 22093314 steps
c [cce-18-1] completed small round (ATE)
c [cce-18-1] eliminated 169 covered clauses in round 1
c [cce-18-2] completed large round (ATE)
c [cce-18-2] allowing another 1030719 steps for small clauses
c [cce-18-2] scheduling 8019 clauses = 6610 binary + 1409 ternary
c [cce-18-2] tried to eliminate 8019 small clauses 100%
c [cce-18-2] completed small round (ATE)
c [cce-18-2] eliminated 0 covered clauses in round 2
c [cce-18] eliminated 169 covered clauses in TOTAL during 2 rounds
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 2102 variables 100%
c [elim-21] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-21] rescheduling of touched variables disabled
c [elim-21-1] eliminated 39 variables 2% in round 1 in 584855 steps
c [elim-21-1] backward subsumption/strengthening limit 584800
c [elim-21-1-1] backward checking 299 touched variables 14%
c [elim-21-1-1] fully completed backward checking in 1 rounds
c [elim-21-1] subsumed 0 and strengthened 2 clauses in 30462 steps
c [elim-21-1] rescheduled 14 variables 1% by backward subsumption
c [elim-21-2] no variable eliminated in round 2 in 4796 steps
c [elim-21] fully completed in 2 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 39 = 2% variables out of 2102 scheduled
c [bca-24] limit of 10000000 steps and 21226 added (scaled 2)
c [bca-24] 1600 out of 4128 literals actually usable 39%
c [bca-24] added 2 blocked clauses in 91837 steps
c [sort-queue-29] sorted 2063 enqueued variables after 4243896 conflicts
c [score-dist-29] active 0 (0%), one 2016 (98%), zero 47 (2%)
c [score-dist-29] max exp 1, different 2 (100%)
c [score-dist-29] median active exp 0, avg 0.0
c [simplification-29] removed 58 variables 2.7% (2063 remain 1%)
c [simplification-29] removed 397 irredundant clauses 3.7% (10321 remain 1%)
c [simplification-29] maximum reduction of 4% = max (3%, 4%)
c [simplification-29] geometric conflict interval increment 200000 = 1000000 / 5
c [simplification-29] conflict interval soft limit 1000000 reached
c [simplification-29] new conflict interval 1000000
c [simplification-29] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-29] hard conflict limit 5743896 (soft 5243896 + delta 500000)
c [simplification-29] new conflict limit 5243896 (hard 5743896)
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 -  962.1    2063    10321   4314080   82424   1345 67715   19    25   27  75%    842   -5   20   21   97%
c -  981.6    2063    10321   4390427   83402   1351 67720   22    34   33  64%    967    7   19   19  100%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 154 basic ate = 145 trn 94% + 9 lrg 6% in 7 updates
c bcas: 24 count, 170 added (123 skipped), 1081682 steps
c bkwd: tried 182932 clauses, 365347 lits, 2.00 lits/clause
c bkwd: checked 3909979 occs, 21.37 occs/clause, 10.70 occs/lit
c bkwd: subsumed 40 binary, 184 ternary, 149 large
c bkwd: strengthened 17 binary, 2 ternary (100% self), 583 large (0% self)
c blkd: 6 bces, 625 removed, 523119 resolutions, 1429195 steps
c blkd: 1639 blocking literals 0%, 35 pure
c bump: 4446513 bumped seen, 434407731 lits 97.7 on average
c card: 7 count, 0 units, 11074 am1, 33883313 steps
c card: 83 rescheduled, 765 eliminated, 62861 resolved, 67814 subsumed
c card: 19073 at-most-one constraints found, average size 4.24
c card: 19073 at-most-one constraints used 100%, average size 4.24
c card: 19 at-most-two constraints found, average size 4.05
c card: 19 at-most-two constraints used 100%, average size 4.05
c cces: 18 cces, 19124 eliminated, 17976 ate 94%, 1148 abce 6%
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: 3541879 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 200 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 91 decompositions, 66437 equivalent 29%
c deco: 121 decision-only clauses 0%, 43% reduction
c decs: 8751173 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 21 elims, 21948 eliminated 10%, 139 pure 1%
c elms: 63 rounds, 3.0 rounds/bve
c elms: 20951 small 95%, 823 large 4%
c elms: 60361 tried small, 20951 succeeded 35%, 39410 failed 65%
c elms: 5922 subsumed, 9623 strengthened, 396 blocked
c elms: 3902847 copies, 3560443 resolutions, 1803183 ipos
c elms: 860253 subchks, 523312 strchks
c gaus: 7 extractions, 923 extracted, 2.4 size, 4 max
c gaus: exported 0 units, 3 binary and 0 ternary equations
c gaus: 0 gc, 12226304 steps, 6113152 extr 50%, 34144 elim 0%
c glue: 19.8 orig avg, 19.8 real avg, 4.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 210407 = 36000 simple 17% + 118448 trn 56% + 55959 lrg 27%, 1147 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 4446513 clauses, 48.2 length
c lrnd: 214428749 lits = 315823489 orig - 101394740 removed 32%
c lrnd: 1443561 uips 32%, 2750139 flips 62%
c mins: 4436755 mins 100%, 300 bin 0%, 9333 size 0%
c mins: 446914405 poisoned searches, 72433956 hits, 16% hit rate
c mins: 685704301 used twice searches, 60706875 hits, 9% hit rate
c move: moved 16984, 13713 bin 81%, 3271 trn 19%
c otfs: 9224 driving 24%, 29504 restarting 76%
c otfs: str 38728, 38684 red 100%, 44 irr 0%
c otfs: str 38728, 0 bin 0%, 49 trn 0%, 38679 lrg 100%
c otfs: sub 57, 57 red 100%, 0 irr 0%
c otfs: sub 57, 0 bin 0%, 1 trn 2%, 56 lrg 98%
c phas: 3 computed, 26001 set, 0 pos (0%), 26001 neg (100%)
c prbs: 9 basic, 38039 probed, 693 failed, 53 lifted
c prbs: 9 simple, 362116 probed, 2071 failed, 30481 eqs
c prbs: 9 treelook, 2805 probed, 56 failed, 0 lifted
c prom: 1311423 locked 11% out of 12227908 tried
c prps: 869074692 props, 97 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 20 count, 73 quat, 28 self1, 2 self2, 34 dup
c queu: 29 sorted, 8751173 next (0 steps 0.00)
c queu: 434801018 enq (0 steps 0.00), 434407731 deq 100%
c redc: 26089 clauses 18%, 144318 tried 3%, 2 sat 0%
c redc: 82830 lits 4%, 2232589 tried 1%, 2 sat 0%
c redc: 3082 times jump level reduced, 3.7 levels on average
c reds: 79 count, 56369.6 conflicts per reduce
c reds: 0 memlim 0%, 79 arith 100%
c reds: 3515760 collected 90%, 407626 retired 10%
c rmbd: 3832 removed, 1104 red 29%
c rsts: 50378 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 29 count, 28 confs 97%, 0 vars 0%
c simp: 1 its 3%, 0 bin 0%, 0 trns 0%
c subl: 4446513 count (2915564 tried 0.7), 323450 sub out of 4444190 (7.3%)
c swps: 15 count, 17 rounds, 1301 queries (76.5/round)
c swps: 1184 sat calls, 40 unsat (2.1% success rate)
c swps: 16483 decisions 13.9, 2535 conflicts 2.1
c swps; 72.4 avg class size, 62.4 avg environment size
c swps: 0 failed, 185 impls, 148 equivs
c swp0: 429 type 0 queries, 218 unsat (50.8%), 388 sat (90.4%)
c swp1: 872 type 1 queries, 501 unsat (57.5%), 765 sat (87.7%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 26396103 calls to obtain time
c tops: 139096 fixed 61%, 118 its, 37739.00 confs/it
c trds: 25 transitive reductions, 16752 removed, 149 failed
c trds: 75829 nodes, 203451 edges, 44649291 steps
c trim: 2774267 words, 10.6 MB
c trnr: 24 count, 1 bin, 905 trn, 29749828 steps
c unhd: 17 count, 23 rounds, 10759576 steps
c unhd: 686 non-trivial sccs of average size 2.2
c unhd: 61 units, 58 bin, 3 trn, 0 lrg
c unhd: 2683 failed, 2657 stamp, 0 lits, 14 bin, 2 trn, 0 lrg
c unhd: 69566 tauts, 4899 bin 7%, 943 trn 1%, 360 lrg 1%
c unhd: 69566 tauts, 63364 stamp 91%, 44212 red 64%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 175949 str, 58 bin 0%, 1020 trn 1%, 174871 lrg 99%, 171177 red 97%
c vars: 2063 remaining 1% and 227481 removed 99% out of 229544
c vars: 139096 fixed 61%, 21948 eliminated 10%, 66437 equivalent 29%
c vsts: 41431304008 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 48.5 search visits per propagation, 9251.9 per conflict
c wchs: 15543911443 pushed, 21171042 enlarged, 339 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        4444263       3515760        407626     148612386      37163448       2299483
c 
c  0 0         64359   1     26687   1         0   0  54733539  37   7997649  22    226148  10     1.3
c  1 5         67667   2     45672   1     12509   3  15163445  10   3477684   9    123823   5     0.6
c  2 6        369961   8    288837   8     43036  11  31446034  21<  8123157  22<   446825  19     2.3
c  3 9        984399  22    818459  23     70913  17  26262818  18   8540930  23    660384  29<    5.4
c  4 14      1308646  29<  1079278  31<    89115  22< 14584473  10   5724374  15    497228  22     6.0
c  5 21       921746  21    734858  21     79288  19   4539133   3   2233302   6    231795  10     4.9
c  6 30       438821  10    326324   9     58840  14   1332733   1    731377   2     81974   4     2.7
c  7 41       201719   5    139883   4     36324   9    361685   0    238550   1     22980   1     1.4
c  8 54        72073   2     46873   1     14369   4    113081   0     74047   0      6302   0     0.5
c  9 69        13202   0      8135   0      2763   1     38180   0     14853   0      1278   0     0.1
c 10 86         1437   0       689   0       396   0     13664   0      4133   0       418   0     0.0
c 11 126         230   0        65   0        73   0     23598   0      3391   0       328   0     0.0
c 12 230           3   0         0   0         0   0         3   0         1   0         0   0     0.0
c 
c avg                  4.1           4.1           4.5           1.7           2.3           3.0
c std                  1.5           1.4           1.7           1.6           1.7           1.6
c 
c   22.487   2% cce
c   15.163   2% bump
c   10.906   1% probe
c    5.013   1% decide
c 
c   12.826 < 1% rest (below)
c 
c    3.729   0% elim
c    2.613   0% transred
c    2.582   0% unhide
c    1.837   0% sweep
c    0.665   0% bca
c    0.472   0% card
c    0.378   0% gauss
c    0.219   0% block
c    0.171   0% ternres
c    0.160   0% quatres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    2.351   0% preprocessing     5%
c   46.533   5% inprocessing     95%
c ==================================
c   48.884   5% simplifying
c  950.628  95% search
c ==================================
c  999.516 100% all
c 
c       4453202 conflicts,        4455.4 confs/sec
c          1426 ternaries,        3122.9 confs/ternary
c           561 binaries,         7938.0 confs/binary
c           118 iterations,      37739.0 confs/iteration
c 
c            79 reductions,          0.1 redus/sec,  56369.6 confs/reduction
c         50378 restarts,           50.4 rests/sec,     88.4 confs/restart
c       8751173 decisions,        8755.4 decis/sec,      2.0 decis/conflict
c     869074692 propagations,   869495.4 props/sec,     99.3 props/decision
c 
c 999.5 seconds, 77.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
