c launch: /data/cnf/sc2014/app/dated-10-17-u.cnf.bz2
c host: atom10
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/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 --score=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 [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] INC (--score=1)
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   55   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   19   0%      0    0    0    0    0%
c i    2.4   25247   202008        35      30      1  9216    0     0   19  14%      0    0    0    0 23979%
c i    2.5   25246   202008       151     119     10  9226    0     1   20  20%      0    1    2    0 19718%
c i    2.6   25242   202008       344     245     22  9239    1     2   20  32%      0    2    6    0 16800%
c i    2.6   24242   202008       509     381     31  9249    1     6   20  22%      0    6   13    0 14711%
c i    2.7   22508   202008       617     471     31  9255    2     8   20  26%      1    8   18    0 13852%
c i    2.7   20871   202008       631     482     32  9256    2     8   20  25%      1    8   17    0 13218%
c 
c [simplification-2] limit 1010 conflicts (hard 11000) hit after 1011 conflicts
c [decomp-3] removed 5028 variables
c [simpleprobe-2] all 20324 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 734 variables
c [simpleprobe-2] 10551 variables remain 54% (9039 retained 46%)
c [simpleprobe-2] removed 734 variables, found 4386 hbrs, 198 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 32041 literals 82%
c [treelook-1] scheduling used 300068 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 315311 steps
c [treelook-1] 32024 literals remain 82%
c [treelook-1] 19532 variables remain to probed next time 100%
c [treelook-1] removed 5 variables, found 2582 hbrs
c [basicprobe-1] limit 1313325 penalty 0 = 0 + 0
c [basicprobe-1-0] 2010 probes remain 11% after last round
c [basicprobe-1-0] 40 units = 40 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1451 variables, found 6328 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 19 units, 444 failed, 3049 tauts, 0 hbrs, 2710 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 17399 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 3553 variables 20% in round 1 in 9500856 steps
c [elim-2-1] backward subsumption/strengthening limit 9500800
c [elim-2-1-1] backward checking 7173 touched variables 41%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 73 and strengthened 147 clauses in 983544 steps
c [elim-2-1] rescheduled 402 variables 2% by backward subsumption
c [elim-2-2] eliminated 93 variables 1% in round 2 in 224155 steps
c [elim-2-2] backward subsumption/strengthening limit 224100
c [elim-2-2-1] backward checking 354 touched variables 2%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 35 and strengthened 21 clauses in 101019 steps
c [elim-2-2] rescheduled 115 variables 1% by backward subsumption
c [elim-2-3] eliminated 33 variables 0% in round 3 in 53506 steps
c [elim-2-3] backward subsumption/strengthening limit 53500
c [elim-2-3-1] backward checking 184 touched variables 1%
c [elim-2-3-1] incomplete backward checking 0 remain 0%
c [elim-2-3] subsumed 30 and strengthened 7 clauses in 53501 steps
c [elim-2] incomplete 62 not tried 0% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 3783 = 22% variables out of 17399 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 108277 negative 99.1% of 109232 except 955 0.9%
c [phase-count-2] 90891 positive 83.2% of 109232 except 18341 16.8%
c [phase-count-2] less non-negative clauses 955 than limit 10900 (10.0%)
c [phase-count-2] non-pos/non-neg = 18341/955 = 19.21 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 141 negative 100%
c [sort-queue-2] sorted 8597 enqueued variables after 1011 conflicts
c [score-dist-2] active 5019 (37%), one 0 (0%), zero 8597 (63%)
c [score-dist-2] max exp 509, different 9 (2%)
c [score-dist-2] median active exp 505, avg 504.8
c [simplification-2] removed 7254 variables 34.8% (13616 remain 6%)
c [simplification-2] removed 92776 irredundant clauses 45.9% (109232 remain 10%)
c [simplification-2] maximum reduction of 46% = max (35%, 46%)
c [simplification-2] large reduction 46% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13011 (soft 3011 + delta 10000)
c [simplification-2] new conflict limit 3011 (hard 13011)
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   13615   109232      1302     605     11  7168    7    20   14  33%      3   20   40    0 8601%
c i    4.8   13511   109232      2888    2068     25  7173   15    32   16  47%     13   32   37    1 2977%
c i    4.8   13507   109232      2914    2090     25  7173   15    32   16  48%     12   32   37    1 2946%
c i    4.8   13506   109232      2915    2090     25  7173   15    32   16  48%     12   32   37    1 2934%
c i    4.8   13502   109232      2916    2090     25  7173   15    32   16  48%     12   32   37    1 2923%
c 
c [simplification-3] limit 3031 conflicts (hard 13011) hit after 3031 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4282 at-most-one constraints of average size 3.6
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4282 out of 4282 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 158 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 26421 literals 98%
c [treelook-2] scheduling used 300024 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 316152 steps
c [treelook-2] 26310 literals remain 98%
c [treelook-2] 13399 variables remain to probed next time 100%
c [decomp-7] removed 21 variables
c [treelook-2] removed 64 variables, found 1394 hbrs
c [unhide-3] limit 129052 with penalty 0 = 0 + 0
c [unhide-3-3] 3 units, 193 failed, 8710 tauts, 0 hbrs, 5521 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 13218 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 543 variables 4% in round 1 in 7659988 steps
c [elim-3-1] backward subsumption/strengthening limit 7659900
c [elim-3-1-1] backward checking 2494 touched variables 19%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 28 and strengthened 44 clauses in 454132 steps
c [elim-3-1] rescheduled 157 variables 1% by backward subsumption
c [elim-3-2] eliminated 26 variables 0% in round 2 in 88286 steps
c [elim-3-2] backward subsumption/strengthening limit 88200
c [elim-3-2-1] backward checking 145 touched variables 1%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 16 and strengthened 4 clauses in 39807 steps
c [elim-3-2] rescheduled 44 variables 0% by backward subsumption
c [elim-3-3] eliminated 13 variables 0% in round 3 in 22410 steps
c [elim-3-3] backward subsumption/strengthening limit 22400
c [elim-3-3-1] backward checking 65 touched variables 0%
c [elim-3-3-1] incomplete backward checking 0 remain 0%
c [elim-3-3] subsumed 7 and strengthened 9 clauses in 22401 steps
c [elim-3] incomplete 24 not tried 0% in round 3
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 609 = 5% variables out of 13218 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 93356 negative 99.1% of 94216 except 860 0.9%
c [phase-count-3] 79270 positive 84.1% of 94216 except 14946 15.9%
c [phase-count-3] less non-negative clauses 860 than limit 9400 (10.0%)
c [phase-count-3] non-pos/non-neg = 14946/860 = 17.38 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 30 negative 100%
c [sort-queue-3] sorted 6695 enqueued variables after 3031 conflicts
c [score-dist-3] active 5914 (47%), one 0 (0%), zero 6695 (53%)
c [score-dist-3] max exp 512, different 12 (2%)
c [score-dist-3] median active exp 506, avg 506.3
c [simplification-3] removed 893 variables 6.6% (12609 remain 6%)
c [simplification-3] removed 15016 irredundant clauses 13.7% (94216 remain 9%)
c [simplification-3] maximum reduction of 14% = max (7%, 14%)
c [simplification-3] large reduction 14% >= 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 15031 (soft 5031 + delta 10000)
c [simplification-3] new conflict limit 5031 (hard 15031)
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.4   12608    94216      3052    2172     26  6312   16    34   15  48%     11   33   34    1 2598%
c i    5.4   12605    94216      3062    2178     26  6312   16    34   15  48%     11   33   34    1 2589%
c i    5.4   12592    94216      3070    2183     26  6312   16    34   15  48%     11   33   35    1 2592%
c 
c [simplification-4] limit 5033 conflicts (hard 15031) hit after 5033 conflicts
c [decomp-8] removed 35 variables
c [basicprobe-2] limit 5112716 penalty 0 = 0 + 0
c [basicprobe-2-0] 1155 probes remain 10% after last round
c [basicprobe-2-0] 121 units = 115 failed (95%) + 6 lifted (5%)
c [basicprobe-2-0] removed 810 variables, found 14771 hbrs
c [unhide-4] limit 204508 with penalty 0 = 0 + 0
c [unhide-4-4] 7 units, 290 failed, 2229 tauts, 0 hbrs, 24080 literals
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 11493 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 409017320 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 710 variables 6% in round 1 in 6282030 steps
c [elim-4-1] backward subsumption/strengthening limit 6282000
c [elim-4-1-1] backward checking 2599 touched variables 23%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 31 and strengthened 22 clauses in 430719 steps
c [elim-4-1] rescheduled 141 variables 1% by backward subsumption
c [elim-4-2] eliminated 26 variables 0% in round 2 in 69801 steps
c [elim-4-2] backward subsumption/strengthening limit 69800
c [elim-4-2-1] backward checking 109 touched variables 1%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 16 and strengthened 2 clauses in 31063 steps
c [elim-4-2] rescheduled 37 variables 0% by backward subsumption
c [elim-4-3] eliminated 7 variables 0% in round 3 in 21765 steps
c [elim-4-3] backward subsumption/strengthening limit 21700
c [elim-4-3-1] backward checking 23 touched variables 0%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 0 and strengthened 3 clauses in 16118 steps
c [elim-4] incomplete 11 not tried 0% in round 3
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 774 = 7% variables out of 11493 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 79326 negative 99.1% of 80043 except 717 0.9%
c [phase-count-4] 65881 positive 82.3% of 80043 except 14162 17.7%
c [phase-count-4] less non-negative clauses 717 than limit 8000 (10.0%)
c [phase-count-4] non-pos/non-neg = 14162/717 = 19.75 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 14 negative 100%
c [sort-queue-4] sorted 5243 enqueued variables after 5033 conflicts
c [score-dist-4] active 5476 (51%), one 0 (0%), zero 5243 (49%)
c [score-dist-4] max exp 513, different 13 (3%)
c [score-dist-4] median active exp 507, avg 507.4
c [simplification-4] removed 1871 variables 14.9% (10719 remain 5%)
c [simplification-4] removed 14173 irredundant clauses 15.0% (80043 remain 8%)
c [simplification-4] maximum reduction of 15% = max (15%, 15%)
c [simplification-4] large reduction 15% >= 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 17033 (soft 7033 + delta 10000)
c [simplification-4] new conflict limit 7033 (hard 17033)
c 
c [simplification-5] limit 7033 conflicts (hard 17033) hit after 7034 conflicts
c [quatres-1] found 4320 quaternary clauses 69% in total
c [quatres-1-2] added 3 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 10719 free variables schedulable
c [ternres-1] 202 ternary resolvents (0 bin, 202 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 189 xors of average arity 2.5
c [gauss-1] connected 470 occurrences of 159 variables (average 3.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 25 variables
c [gauss-1] exported 0 unary, 2 binary and 0 ternary equations
c [simpleprobe-3] 5713 schedulable variables 53%
c [simpleprobe-3] limit 5144621 penalty 0 = 0 + 0
c [decomp-11] removed 200 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 200 variables, found 6525 hbrs, 62 units
c [unhide-5] limit 257231 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 46 failed, 4884 tauts, 0 hbrs, 4604 literals
c [transred-1] limit 1286155 with penalty 0 = 0 + 0
c [transred-1] removed 541 transitive binary clauses
c [transred-1] found 16 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 10422 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 320 blocked clauses
c [block-1] 320 < 1/100 * 74877 = 748 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 9
c [cce-1-1] eliminated 2 clauses out of 7 (29%) of length 8
c [cce-1-1] eliminated 5 clauses out of 53 (9%) of length 7
c [cce-1-1] eliminated 40 clauses out of 370 (11%) of length 6
c [cce-1-1] eliminated 181 clauses out of 999 (18%) of length 5
c [cce-1-1] eliminated 1326 clauses out of 3748 (35%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 1555 large clauses in 16015717 steps
c [cce-1-1] allowing another 8007858 steps for small clauses
c [cce-1-1] scheduling 56166 clauses = 38762 binary + 17404 ternary
c [cce-1-1] tried to eliminate 2025 small clauses 4%
c [cce-1-1] eliminated 611 binary clauses 2%
c [cce-1-1] eliminated 99 ternary clauses 1%
c [cce-1-1] eliminated 710 small clauses 1%
c [cce-1-1] eliminated 710 small clauses in 30000004 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2265 covered clauses in round 1
c [cce-1] eliminated 2265 covered clauses in TOTAL during 1 rounds
c [elim-5] no untried remaining variables left
c [elim-5] scheduled 10420 variables 100%
c [elim-5] limit of 25723105 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 556 variables 5% in round 1 in 5273029 steps
c [elim-5-1] backward subsumption/strengthening limit 5273000
c [elim-5-1-1] backward checking 2169 touched variables 21%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 15 and strengthened 29 clauses in 358745 steps
c [elim-5-1] rescheduled 102 variables 1% by backward subsumption
c [elim-5-2] eliminated 19 variables 0% in round 2 in 47720 steps
c [elim-5-2] backward subsumption/strengthening limit 47700
c [elim-5-2-1] backward checking 79 touched variables 1%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 13 and strengthened 4 clauses in 29126 steps
c [elim-5-2] rescheduled 34 variables 0% by backward subsumption
c [elim-5-3] eliminated 1 variables 0% in round 3 in 30246 steps
c [elim-5-3] backward subsumption/strengthening limit 30200
c [elim-5-3-1] backward checking 12 touched variables 0%
c [elim-5-3-1] fully completed backward checking in 1 rounds
c [elim-5-3] subsumed 3 and strengthened 0 clauses in 9946 steps
c [elim-5] incomplete 8 not tried 0% in round 3
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 594 = 6% variables out of 10420 scheduled
c [bca-1] limit of 10000000 steps and 141040 added (scaled 2)
c [bca-1] 17773 out of 19654 literals actually usable 90%
c [bca-1] added 5 blocked clauses in 38736 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1738 pos 17.7% + 8088 neg 82.3% = 9826 sched 100.0% ret 0
c [sweep-1-1] 1014626 steps 22 queries 760.00 avg class size
c [sweep-1-1] 130 decisions 19 SAT calls 45.68 avg env size
c [sweep-1-1] 9509 variables remain 97% (313 retained 3%)
c [decomp-12] removed 12 variables
c [sweep-1-1] removed 12 vars (0 failed, 4 eqs, 4 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 12 vars in TOTAL (1 rounds, 21 queries)
c [phase-count-5] 69685 negative 99.3% of 70193 except 508 0.7%
c [phase-count-5] 58648 positive 83.6% of 70193 except 11545 16.4%
c [phase-count-5] less non-negative clauses 508 than limit 7000 (10.0%)
c [phase-count-5] non-pos/non-neg = 11545/508 = 22.73 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 5 negative 100%
c [sort-queue-5] sorted 4468 enqueued variables after 7034 conflicts
c [score-dist-5] active 5346 (54%), one 0 (0%), zero 4468 (46%)
c [score-dist-5] max exp 514, different 14 (3%)
c [score-dist-5] median active exp 508, avg 507.7
c [simplification-5] removed 905 variables 8.4% (9814 remain 4%)
c [simplification-5] removed 9850 irredundant clauses 12.3% (70193 remain 7%)
c [simplification-5] maximum reduction of 12% = max (8%, 12%)
c [simplification-5] large reduction 12% >= 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 19034 (soft 9034 + delta 10000)
c [simplification-5] new conflict limit 9034 (hard 19034)
c 
c [simplification-6] limit 9034 conflicts (hard 19034) hit after 9034 conflicts
c [quatres-2] found 2625 quaternary clauses 61% in total
c [quatres-2-2] added 3 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 9814 free variables schedulable
c [ternres-2] 87 ternary resolvents (0 bin, 87 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2205 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] 2205 out of 2205 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 63 xors of average arity 3.0
c [gauss-2] connected 189 occurrences of 77 variables (average 2.5)
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 [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 19626 literals 100%
c [treelook-3] scheduling used 261000 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 351658 steps
c [treelook-3] 19608 literals remain 100%
c [treelook-3] 9801 variables remain to probed next time 100%
c [treelook-3] removed 5 variables, found 3505 hbrs
c [unhide-6] limit 306134 with penalty 0 = 0 + 0
c [unhide-6-6] 4 units, 91 failed, 3394 tauts, 0 hbrs, 7511 literals
c [transred-2] limit 1530670 with penalty 0 = 0 + 0
c [transred-2] removed 536 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 9
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 8
c [cce-2-1] eliminated 1 clauses out of 60 (2%) of length 7
c [cce-2-1] eliminated 4 clauses out of 339 (1%) of length 6
c [cce-2-1] eliminated 20 clauses out of 904 (2%) of length 5
c [cce-2-1] eliminated 167 clauses out of 2534 (7%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 194 large clauses in 13233798 steps
c [cce-2-1] allowing another 6616899 steps for small clauses
c [cce-2-1] scheduling 48235 clauses = 36622 binary + 11613 ternary
c [cce-2-1] tried to eliminate 2540 small clauses 5%
c [cce-2-1] eliminated 808 binary clauses 2%
c [cce-2-1] eliminated 103 ternary clauses 1%
c [cce-2-1] eliminated 911 small clauses 2%
c [cce-2-1] eliminated 2023 small clauses in 30000002 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 2217 covered clauses in round 1
c [cce-2] eliminated 2217 covered clauses in TOTAL during 1 rounds
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 9704 variables 100%
c [elim-6] limit of 30613400 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 197 variables 2% in round 1 in 4947010 steps
c [elim-6-1] backward subsumption/strengthening limit 4947000
c [elim-6-1-1] backward checking 1164 touched variables 12%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 10 and strengthened 8 clauses in 202421 steps
c [elim-6-1] rescheduled 55 variables 1% by backward subsumption
c [elim-6-2] eliminated 5 variables 0% in round 2 in 30702 steps
c [elim-6-2] backward subsumption/strengthening limit 30700
c [elim-6-2-1] backward checking 34 touched variables 0%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 6 and strengthened 0 clauses in 11545 steps
c [elim-6-2] rescheduled 9 variables 0% by backward subsumption
c [elim-6-3] eliminated 3 variables 0% in round 3 in 3993 steps
c [elim-6-3] backward subsumption/strengthening limit 3900
c [elim-6-3-1] backward checking 9 touched variables 0%
c [elim-6-3-1] incomplete backward checking 0 remain 0%
c [elim-6-3] subsumed 5 and strengthened 0 clauses in 3901 steps
c [elim-6] incomplete 5 not tried 0% in round 3
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 210 = 2% variables out of 9704 scheduled
c [bca-2] limit of 10000000 steps and 134776 added (scaled 2)
c [bca-2] 17048 out of 18990 literals actually usable 90%
c [bca-2] added 2 blocked clauses in 39076 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1690 pos 18.4% + 7502 neg 81.6% = 9192 sched 96.8% ret 302
c [sweep-2-1] 1000290 steps 28 queries 1019.29 avg class size
c [sweep-2-1] 235 decisions 20 SAT calls 39.60 avg env size
c [sweep-2-1] 8893 variables remain 94% (526 retained 6%)
c [decomp-15] removed 86 variables
c [sweep-2-1] removed 86 vars (0 failed, 7 eqs, 14 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 86 vars in TOTAL (1 rounds, 27 queries)
c [phase-count-6] 65588 negative 99.3% of 66078 except 490 0.7%
c [phase-count-6] 54617 positive 82.7% of 66078 except 11461 17.3%
c [phase-count-6] less non-negative clauses 490 than limit 6600 (10.0%)
c [phase-count-6] non-pos/non-neg = 11461/490 = 23.39 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 5 negative 100%
c [sort-queue-6] sorted 4143 enqueued variables after 9034 conflicts
c [score-dist-6] active 5265 (56%), one 0 (0%), zero 4143 (44%)
c [score-dist-6] max exp 514, different 14 (3%)
c [score-dist-6] median active exp 508, avg 507.9
c [simplification-6] removed 406 variables 4.1% (9408 remain 4%)
c [simplification-6] removed 4115 irredundant clauses 5.9% (66078 remain 6%)
c [simplification-6] maximum reduction of 6% = max (4%, 6%)
c [simplification-6] large reduction 6% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 21034 (soft 11034 + delta 10000)
c [simplification-6] new conflict limit 11034 (hard 21034)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   11.9    9407    66078      9543    4632    366 16407   16    25   16  65%     81   22   20    3  703%
c 
c [simplification-7] limit 11034 conflicts (hard 21034) hit after 11034 conflicts
c [quatres-3] found 2425 quaternary clauses 60% in total
c [quatres-3-2] added 2 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 9401 free variables schedulable
c [ternres-3] 89 ternary resolvents (0 bin, 89 trn)
c [ternres-3] fully completed ternary resolution
c [decomp-16] removed 12 variables
c [basicprobe-3] limit 8790790 penalty 0 = 0 + 0
c [basicprobe-3-0] 887 probes remain 10% after last round
c [basicprobe-3-0] 249 units = 227 failed (91%) + 22 lifted (9%)
c [basicprobe-3-0] removed 390 variables, found 19035 hbrs
c [bate-1] eliminated 76 asymmetric tautologies during probing
c [unhide-7] limit 351631 with penalty 0 = 0 + 0
c [unhide-7-8] 11 units, 420 failed, 5038 tauts, 0 hbrs, 45583 literals
c [transred-3] limit 1758158 with penalty 0 = 0 + 0
c [transred-3] removed 468 transitive binary clauses
c [transred-3] found 11 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 8871 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 163 blocked clauses
c [block-2] 163 < 1/100 * 58998 = 589 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 10
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 9
c [cce-3-1] eliminated 1 clauses out of 4 (25%) of length 8
c [cce-3-1] eliminated 1 clauses out of 38 (3%) of length 7
c [cce-3-1] eliminated 5 clauses out of 277 (2%) of length 6
c [cce-3-1] eliminated 28 clauses out of 776 (4%) of length 5
c [cce-3-1] eliminated 111 clauses out of 2141 (5%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 148 large clauses in 9462467 steps
c [cce-3-1] allowing another 4731233 steps for small clauses
c [cce-3-1] scheduling 41475 clauses = 32021 binary + 9454 ternary
c [cce-3-1] tried to eliminate 3267 small clauses 8%
c [cce-3-1] eliminated 970 binary clauses 3%
c [cce-3-1] eliminated 154 ternary clauses 2%
c [cce-3-1] eliminated 1124 small clauses 3%
c [cce-3-1] eliminated 1124 small clauses in 30000013 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1272 covered clauses in round 1
c [cce-3] eliminated 1272 covered clauses in TOTAL during 1 rounds
c [elim-7] no untried remaining variables left
c [elim-7] scheduled 8865 variables 100%
c [elim-7] limit of 35163161 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 640 variables 7% in round 1 in 4041614 steps
c [elim-7-1] backward subsumption/strengthening limit 4041600
c [elim-7-1-1] backward checking 2675 touched variables 30%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 6 and strengthened 10 clauses in 408227 steps
c [elim-7-1] rescheduled 54 variables 1% by backward subsumption
c [elim-7-2] eliminated 3 variables 0% in round 2 in 26068 steps
c [elim-7-2] backward subsumption/strengthening limit 26000
c [elim-7-2-1] backward checking 18 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 3 clauses in 12893 steps
c [elim-7-2] rescheduled 12 variables 0% by backward subsumption
c [elim-7-3] eliminated 3 variables 0% in round 3 in 4934 steps
c [elim-7-3] backward subsumption/strengthening limit 4900
c [elim-7-3-1] backward checking 10 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 0 and strengthened 1 clauses in 4901 steps
c [elim-7] incomplete 5 not tried 0% in round 3
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 648 = 7% variables out of 8865 scheduled
c [bca-3] limit of 10000000 steps and 112719 added (scaled 2)
c [bca-3] 14745 out of 16436 literals actually usable 90%
c [bca-3] added 6 blocked clauses in 34414 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1451 pos 18.7% + 6327 neg 81.3% = 7778 sched 94.7% ret 439
c [sweep-3-1] 1045962 steps 34 queries 901.09 avg class size
c [sweep-3-1] 306 decisions 24 SAT calls 69.33 avg env size
c [sweep-3-1] 7239 variables remain 89% (897 retained 11%)
c [decomp-17] removed 98 variables
c [sweep-3-1] removed 98 vars (0 failed, 9 eqs, 18 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 98 vars in TOTAL (1 rounds, 33 queries)
c [phase-count-7] 54660 negative 99.3% of 55067 except 407 0.7%
c [phase-count-7] 45280 positive 82.2% of 55067 except 9787 17.8%
c [phase-count-7] less non-negative clauses 407 than limit 5500 (10.0%)
c [phase-count-7] non-pos/non-neg = 9787/407 = 24.05 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 4 negative 100%
c [sort-queue-7] sorted 3402 enqueued variables after 11034 conflicts
c [score-dist-7] active 4717 (58%), one 0 (0%), zero 3402 (42%)
c [score-dist-7] max exp 515, different 15 (3%)
c [score-dist-7] median active exp 508, avg 508.0
c [simplification-7] removed 1282 variables 13.6% (8119 remain 4%)
c [simplification-7] removed 11011 irredundant clauses 16.7% (55067 remain 5%)
c [simplification-7] maximum reduction of 17% = max (14%, 17%)
c [simplification-7] large reduction 17% >= 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 23034 (soft 13034 + delta 10000)
c [simplification-7] new conflict limit 13034 (hard 23034)
c 
c [simplification-8] limit 13034 conflicts (hard 23034) hit after 13035 conflicts
c [quatres-4] found 2113 quaternary clauses 58% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 2 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 8119 free variables schedulable
c [ternres-4] 107 ternary resolvents (1 bin, 106 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 30 xors of average arity 2.9
c [gauss-3] connected 88 occurrences of 49 variables (average 1.8)
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 [simpleprobe-4] all 8119 free variables schedulable
c [simpleprobe-4] limit 7718514 penalty 0 = 0 + 0
c [decomp-19] removed 69 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 69 variables, found 3630 hbrs, 32 units
c [unhide-8] limit 385925 with penalty 0 = 0 + 0
c [unhide-8-10] 3 units, 156 failed, 3979 tauts, 0 hbrs, 8500 literals
c [transred-4] limit 1929628 with penalty 0 = 0 + 0
c [transred-4] removed 662 transitive binary clauses
c [transred-4] found 9 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 2 (50%) of length 10
c [cce-4-1] eliminated 1 clauses out of 6 (17%) of length 9
c [cce-4-1] eliminated 1 clauses out of 14 (7%) of length 8
c [cce-4-1] eliminated 1 clauses out of 58 (2%) of length 7
c [cce-4-1] eliminated 2 clauses out of 323 (1%) of length 6
c [cce-4-1] eliminated 27 clauses out of 836 (3%) of length 5
c [cce-4-1] eliminated 127 clauses out of 2015 (6%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 160 large clauses in 9595188 steps
c [cce-4-1] allowing another 4797594 steps for small clauses
c [cce-4-1] scheduling 40779 clauses = 29062 binary + 11717 ternary
c [cce-4-1] tried to eliminate 39109 small clauses 96%
c [cce-4-1] eliminated 7900 binary clauses 27%
c [cce-4-1] eliminated 1430 ternary clauses 12%
c [cce-4-1] eliminated 9330 small clauses 23%
c [cce-4-1] eliminated 9849 small clauses in 300000008 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 10009 covered clauses in round 1
c [cce-4] eliminated 10009 covered clauses in TOTAL during 1 rounds
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 7968 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 771851460 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 794 variables 10% in round 1 in 2879747 steps
c [elim-8-1] backward subsumption/strengthening limit 2879700
c [elim-8-1-1] backward checking 3237 touched variables 41%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 7 and strengthened 16 clauses in 358858 steps
c [elim-8-1] rescheduled 114 variables 1% by backward subsumption
c [elim-8-2] eliminated 1 variables 0% in round 2 in 49683 steps
c [elim-8-2] backward subsumption/strengthening limit 49600
c [elim-8-2-1] backward checking 12 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 3 and strengthened 0 clauses in 15046 steps
c [elim-8-2] rescheduled 6 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 2831 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 796 = 10% variables out of 7968 scheduled
c [bca-4] limit of 10000000 steps and 84262 added (scaled 2)
c [bca-4] 12875 out of 14346 literals actually usable 90%
c [bca-4] added 7 blocked clauses in 29692 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1178 pos 18.3% + 5242 neg 81.7% = 6420 sched 89.5% ret 752
c [sweep-4-1] 1011608 steps 28 queries 468.82 avg class size
c [sweep-4-1] 662 decisions 26 SAT calls 94.69 avg env size
c [sweep-4-1] 5651 variables remain 79% (1516 retained 21%)
c [decomp-20] removed 6 variables
c [sweep-4-1] removed 6 vars (0 failed, 1 eqs, 4 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 6 vars in TOTAL (1 rounds, 27 queries)
c [phase-count-8] 41531 negative 99.2% of 41846 except 315 0.8%
c [phase-count-8] 35350 positive 84.5% of 41846 except 6496 15.5%
c [phase-count-8] less non-negative clauses 315 than limit 4100 (10.0%)
c [phase-count-8] non-pos/non-neg = 6496/315 = 20.62 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-8] sorted 2970 enqueued variables after 13035 conflicts
c [score-dist-8] active 4196 (59%), one 0 (0%), zero 2970 (41%)
c [score-dist-8] max exp 515, different 15 (3%)
c [score-dist-8] median active exp 508, avg 508.2
c [simplification-8] removed 953 variables 11.7% (7166 remain 3%)
c [simplification-8] removed 13221 irredundant clauses 24.0% (41846 remain 4%)
c [simplification-8] maximum reduction of 24% = max (12%, 24%)
c [simplification-8] large reduction 24% >= 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 25035 (soft 15035 + delta 10000)
c [simplification-8] new conflict limit 15035 (hard 25035)
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.7    7165    41846     14243    4085   1260 26438   23    34   14  69%     52   29   35    4  807%
c 
c [simplification-9] limit 15035 conflicts (hard 25035) hit after 15036 conflicts
c [quatres-5] found 1900 quaternary clauses 53% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 5 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 7163 free variables schedulable
c [ternres-5] 78 ternary resolvents (0 bin, 78 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-21] removed 3 variables
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 14323 literals 100%
c [treelook-4] scheduling used 204055 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 346784 steps
c [treelook-4] 14304 literals remain 100%
c [treelook-4] 7154 variables remain to probed next time 100%
c [treelook-4] removed 3 variables, found 2986 hbrs
c [unhide-9] limit 426683 with penalty 0 = 0 + 0
c [unhide-9-12] 3 units, 5 failed, 2194 tauts, 0 hbrs, 5986 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 521 transitive binary clauses
c [transred-5] found 19 units
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 20
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 19
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 18
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 16
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 14
c [cce-5-1] eliminated 2 clauses out of 9 (22%) 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 11 (18%) of length 11
c [cce-5-1] eliminated 1 clauses out of 8 (12%) of length 10
c [cce-5-1] eliminated 2 clauses out of 21 (10%) of length 9
c [cce-5-1] eliminated 3 clauses out of 29 (10%) of length 8
c [cce-5-1] eliminated 8 clauses out of 107 (7%) of length 7
c [cce-5-1] eliminated 23 clauses out of 399 (6%) of length 6
c [cce-5-1] eliminated 58 clauses out of 825 (7%) of length 5
c [cce-5-1] eliminated 205 clauses out of 1837 (11%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 312 large clauses in 9635460 steps
c [cce-5-1] allowing another 4817730 steps for small clauses
c [cce-5-1] scheduling 28299 clauses = 20311 binary + 7988 ternary
c [cce-5-1] tried to eliminate 4164 small clauses 15%
c [cce-5-1] eliminated 238 binary clauses 1%
c [cce-5-1] eliminated 176 ternary clauses 2%
c [cce-5-1] eliminated 414 small clauses 1%
c [cce-5-1] eliminated 587 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 899 covered clauses in round 1
c [cce-5] eliminated 899 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 7128 variables 100%
c [elim-9] limit of 42668322 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 158 variables 2% in round 1 in 2694535 steps
c [elim-9-1] backward subsumption/strengthening limit 2694500
c [elim-9-1-1] backward checking 1065 touched variables 15%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 1 and strengthened 3 clauses in 130234 steps
c [elim-9-1] rescheduled 20 variables 0% by backward subsumption
c [elim-9-2] eliminated 1 variables 0% in round 2 in 7201 steps
c [elim-9-2] backward subsumption/strengthening limit 7200
c [elim-9-2-1] backward checking 8 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 5684 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 159 = 2% variables out of 7128 scheduled
c [bca-5] limit of 10000000 steps and 81540 added (scaled 2)
c [bca-5] 12204 out of 13940 literals actually usable 88%
c [bca-5] added 16 blocked clauses in 29514 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 1091 pos 19.8% + 4415 neg 80.2% = 5506 sched 79.0% ret 1463
c [sweep-5-1] 10157061 steps 557 queries 38.31 avg class size
c [sweep-5-1] 2955 decisions 526 SAT calls 29.75 avg env size
c [sweep-5-1] 664 variables remain 10% (6108 retained 90%)
c [decomp-23] removed 272 variables
c [sweep-5-1] removed 272 vars (0 failed, 47 eqs, 62 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 272 vars in TOTAL (1 rounds, 556 queries)
c [sort-queue-9] sorted 2566 enqueued variables after 15036 conflicts
c [score-dist-9] active 4131 (62%), one 0 (0%), zero 2566 (38%)
c [score-dist-9] max exp 515, different 15 (3%)
c [score-dist-9] median active exp 508, avg 508.4
c [simplification-9] removed 466 variables 6.5% (6697 remain 3%)
c [simplification-9] removed 2903 irredundant clauses 6.9% (38943 remain 4%)
c [simplification-9] maximum reduction of 7% = max (7%, 7%)
c [simplification-9] large reduction 7% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 27036 (soft 17036 + delta 10000)
c [simplification-9] new conflict limit 17036 (hard 27036)
c 
c [simplification-10] limit 17036 conflicts (hard 27036) hit after 17036 conflicts
c [quatres-6] found 1587 quaternary clauses 53% in total
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 6697 free variables schedulable
c [ternres-6] 42 ternary resolvents (1 bin, 41 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 250000 penalty 3 = 3 + 0
c [card-4] found 790 at-most-one constraints of average size 3.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 250000 for elimination
c [card-4] 790 out of 790 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [basicprobe-4] limit 11536472 penalty 0 = 0 + 0
c [basicprobe-4-0] 132 probes remain 2% after last round
c [basicprobe-4-0] 514 units = 454 failed (88%) + 60 lifted (12%)
c [basicprobe-4-0] removed 714 variables, found 22579 hbrs
c [bate-2] eliminated 78 asymmetric tautologies during probing
c [unhide-10] limit 461458 with penalty 0 = 0 + 0
c [unhide-10-14] 4 units, 46 failed, 5465 tauts, 0 hbrs, 4841 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 706 transitive binary clauses
c [transred-6] found 22 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 5887 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 117 blocked clauses
c [block-3] 117 < 1/100 * 32843 = 328 considered unsuccessful
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 2 clauses out of 16 (12%) of length 8
c [cce-6-1] eliminated 2 clauses out of 42 (5%) of length 7
c [cce-6-1] eliminated 3 clauses out of 166 (2%) of length 6
c [cce-6-1] eliminated 13 clauses out of 462 (3%) of length 5
c [cce-6-1] eliminated 45 clauses out of 1230 (4%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 65 large clauses in 4368960 steps
c [cce-6-1] allowing another 2184480 steps for small clauses
c [cce-6-1] scheduling 23143 clauses = 17858 binary + 5285 ternary
c [cce-6-1] tried to eliminate 5539 small clauses 24%
c [cce-6-1] eliminated 582 binary clauses 3%
c [cce-6-1] eliminated 164 ternary clauses 3%
c [cce-6-1] eliminated 746 small clauses 3%
c [cce-6-1] eliminated 746 small clauses in 30000004 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 811 covered clauses in round 1
c [cce-6] eliminated 811 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 5887 variables 100%
c [elim-10] limit of 46145890 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 783 variables 13% in round 1 in 2066937 steps
c [elim-10-1] backward subsumption/strengthening limit 2066900
c [elim-10-1-1] backward checking 2354 touched variables 40%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 5 and strengthened 7 clauses in 234189 steps
c [elim-10-1] rescheduled 46 variables 1% by backward subsumption
c [elim-10-2] eliminated 3 variables 0% in round 2 in 16183 steps
c [elim-10-2] backward subsumption/strengthening limit 16100
c [elim-10-2-1] backward checking 23 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 1 and strengthened 0 clauses in 11106 steps
c [elim-10-2] rescheduled 3 variables 0% by backward subsumption
c [elim-10-3] eliminated 1 variables 0% in round 3 in 470 steps
c [elim-10-3] backward subsumption/strengthening limit 400
c [elim-10-3-1] backward checking 6 touched variables 0%
c [elim-10-3-1] incomplete backward checking 2 remain 33%
c [elim-10-3] subsumed 0 and strengthened 0 clauses in 403 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 791 = 13% variables out of 5887 scheduled
c [bca-6] limit of 10000000 steps and 61702 added (scaled 2)
c [bca-6] 8934 out of 10194 literals actually usable 88%
c [bca-6] added 15 blocked clauses in 21184 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 170 pos 37.2% + 287 neg 62.8% = 457 sched 9.0% ret 4639
c [sweep-6-1] 1010769 steps 113 queries 24.49 avg class size
c [sweep-6-1] 427 decisions 104 SAT calls 18.80 avg env size
c [sweep-6-1] 228 variables remain 4% (4850 retained 96%)
c [decomp-25] removed 37 variables
c [sweep-6-1] removed 37 vars (0 failed, 10 eqs, 7 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 37 vars in TOTAL (1 rounds, 112 queries)
c [sort-queue-10] sorted 1857 enqueued variables after 17036 conflicts
c [score-dist-10] active 3202 (63%), one 0 (0%), zero 1857 (37%)
c [score-dist-10] max exp 515, different 15 (3%)
c [score-dist-10] median active exp 508, avg 508.5
c [simplification-10] removed 1638 variables 24.5% (5059 remain 2%)
c [simplification-10] removed 8567 irredundant clauses 22.0% (30376 remain 3%)
c [simplification-10] maximum reduction of 24% = max (24%, 22%)
c [simplification-10] large reduction 24% >= 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 29036 (soft 19036 + delta 10000)
c [simplification-10] new conflict limit 19036 (hard 29036)
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   25.8    5058    30376     17205    2620    406 23627   25    35   12  72%     27   28   21    5  387%
c i   26.2    5057    30376     18904    4223    407 23627   26    35   13  75%     12   28   31    6  514%
c 
c [simplification-11] limit 19036 conflicts (hard 29036) hit after 19036 conflicts
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] all 5055 free variables schedulable
c [ternres-7] 47 ternary resolvents (0 bin, 47 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-4] limit 500000 penalty 2 = 2 + 0
c [gauss-4] extracted 14 xors of average arity 3.0
c [gauss-4] connected 42 occurrences of 27 variables (average 1.6)
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-26] removed 1 variables
c [simpleprobe-5] all 5054 free variables schedulable
c [simpleprobe-5] limit 9738661 penalty 0 = 0 + 0
c [decomp-27] removed 51 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 51 variables, found 2844 hbrs, 25 units
c [unhide-11] limit 486933 with penalty 0 = 0 + 0
c [unhide-11-17] 1 units, 14 failed, 3246 tauts, 0 hbrs, 3587 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 796 transitive binary clauses
c [transred-7] found 9 units
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 35
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 34
c [cce-7-1] eliminated 4 clauses out of 5 (80%) of length 29
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 16
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 13
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 12
c [cce-7-1] eliminated 1 clauses out of 6 (17%) of length 10
c [cce-7-1] eliminated 1 clauses out of 12 (8%) of length 9
c [cce-7-1] eliminated 4 clauses out of 20 (20%) of length 8
c [cce-7-1] eliminated 5 clauses out of 54 (9%) of length 7
c [cce-7-1] eliminated 11 clauses out of 213 (5%) of length 6
c [cce-7-1] eliminated 25 clauses out of 513 (5%) of length 5
c [cce-7-1] eliminated 119 clauses out of 1187 (10%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 178 large clauses in 5569755 steps
c [cce-7-1] allowing another 2784877 steps for small clauses
c [cce-7-1] scheduling 22662 clauses = 15788 binary + 6874 ternary
c [cce-7-1] tried to eliminate 5432 small clauses 24%
c [cce-7-1] eliminated 592 binary clauses 4%
c [cce-7-1] eliminated 155 ternary clauses 2%
c [cce-7-1] eliminated 747 small clauses 3%
c [cce-7-1] eliminated 840 small clauses in 30000004 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1018 covered clauses in round 1
c [cce-7] eliminated 1018 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 4978 variables 100%
c [elim-11] limit of 48693307 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 204 variables 4% in round 1 in 1845381 steps
c [elim-11-1] backward subsumption/strengthening limit 1845300
c [elim-11-1-1] backward checking 1057 touched variables 21%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 2 clauses in 124759 steps
c [elim-11-1] rescheduled 16 variables 0% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 6106 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 204 = 4% variables out of 4978 scheduled
c [bca-7] limit of 10000000 steps and 57035 added (scaled 2)
c [bca-7] 8253 out of 9550 literals actually usable 86%
c [bca-7] added 19 blocked clauses in 20828 steps
c [sweep-7] limit 1000000 penalty 0 = 0 + 0
c [sweep-7-1] 57 pos 28.5% + 143 neg 71.5% = 200 sched 4.2% ret 4574
c [sweep-7-1] 942089 steps 134 queries 8.20 avg class size
c [sweep-7-1] 539 decisions 129 SAT calls 18.77 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-28] removed 3 variables
c [sweep-7-1] removed 3 vars (0 failed, 4 eqs, 13 impls)
c [sweep-7-2] 825 pos 17.3% + 3946 neg 82.7% = 4771 sched 100.0% ret 0
c [sweep-7-2] 197021 steps 2 queries 2385.50 avg class size
c [sweep-7-2] 100 decisions 1 SAT calls 295.00 avg env size
c [sweep-7-2] 4771 variables remain 100% (0 retained 0%)
c [sweep-7-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7] 3 < 1/1000 * 4774 = 4 considered unsuccessful
c [sweep-7] removed 3 vars in TOTAL (2 rounds, 134 queries)
c [sort-queue-11] sorted 1711 enqueued variables after 19036 conflicts
c [score-dist-11] active 3060 (64%), one 0 (0%), zero 1711 (36%)
c [score-dist-11] max exp 515, different 15 (3%)
c [score-dist-11] median active exp 509, avg 508.6
c [simplification-11] removed 284 variables 5.6% (4771 remain 2%)
c [simplification-11] removed 2123 irredundant clauses 7.0% (28253 remain 3%)
c [simplification-11] maximum reduction of 7% = max (6%, 7%)
c [simplification-11] large reduction 7% >= 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 31036 (soft 21036 + delta 10000)
c [simplification-11] new conflict limit 21036 (hard 31036)
c 
c [simplification-12] limit 21036 conflicts (hard 31036) hit after 21037 conflicts
c [quatres-7] found 1175 quaternary clauses 54% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-2] added 4 quaternary resolvents
c [ternres-8] limit 4000000 with penalty 0 = 0 + 0
c [ternres-8] all 4771 free variables schedulable
c [ternres-8] 42 ternary resolvents (0 bin, 42 trn)
c [ternres-8] fully completed ternary resolution
c [treelook-5] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 9539 literals 100%
c [treelook-5] scheduling used 146627 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 302201 steps
c [treelook-5] 9484 literals remain 100%
c [treelook-5] 4758 variables remain to probed next time 100%
c [decomp-31] removed 3 variables
c [treelook-5] removed 13 variables, found 2302 hbrs
c [unhide-12] limit 511588 with penalty 0 = 0 + 0
c [unhide-12-20] 3 units, 56 failed, 2152 tauts, 0 hbrs, 5206 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 534 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 1 (100%) of length 15
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 12
c [cce-8-1] eliminated 5 clauses out of 63 (8%) of length 7
c [cce-8-1] eliminated 2 clauses out of 485 (0%) of length 5
c [cce-8-1] eliminated 33 clauses out of 1131 (3%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 42 large clauses in 5445292 steps
c [cce-8-1] allowing another 2722646 steps for small clauses
c [cce-8-1] scheduling 21295 clauses = 14719 binary + 6576 ternary
c [cce-8-1] tried to eliminate 21295 small clauses 100%
c [cce-8-1] eliminated 1263 binary clauses 9%
c [cce-8-1] eliminated 332 ternary clauses 5%
c [cce-8-1] eliminated 1595 small clauses 7%
c [cce-8-1] eliminated 1707 small clauses in 104320311 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] completed small and large (ATE)
c [cce-8-1] eliminated 1749 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 2455218 steps for small clauses
c [cce-8-2] scheduling 19700 clauses = 13456 binary + 6244 ternary
c [cce-8-2] tried to eliminate 19700 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 1749 covered clauses in TOTAL during 2 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 4737 variables 100%
c [elim-12] limit of 51158808 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 180 variables 4% in round 1 in 1703020 steps
c [elim-12-1] backward subsumption/strengthening limit 1703000
c [elim-12-1-1] backward checking 1063 touched variables 22%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 2 and strengthened 0 clauses in 116288 steps
c [elim-12-1] rescheduled 4 variables 0% by backward subsumption
c [elim-12-2] no variable eliminated in round 2 in 1555 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 180 = 4% variables out of 4737 scheduled
c [bca-8] limit of 10000000 steps and 52685 added (scaled 2)
c [bca-8] 7815 out of 9116 literals actually usable 86%
c [bca-8] added 11 blocked clauses in 19986 steps
c [sort-queue-12] sorted 1622 enqueued variables after 21037 conflicts
c [score-dist-12] active 2935 (64%), one 0 (0%), zero 1622 (36%)
c [score-dist-12] max exp 516, different 16 (3%)
c [score-dist-12] median active exp 509, avg 508.8
c [simplification-12] removed 214 variables 4.5% (4557 remain 2%)
c [simplification-12] removed 2178 irredundant clauses 7.7% (26075 remain 2%)
c [simplification-12] maximum reduction of 8% = max (4%, 8%)
c [simplification-12] large reduction 8% >= 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 33037 (soft 23037 + delta 10000)
c [simplification-12] new conflict limit 23037 (hard 33037)
c 
c [simplification-13] limit 23037 conflicts (hard 33037) hit after 23042 conflicts
c [quatres-8] found 1186 quaternary clauses 55% in total
c [ternres-9] limit 4000000 with penalty 0 = 0 + 0
c [ternres-9] all 4557 free variables schedulable
c [ternres-9] 10 ternary resolvents (0 bin, 10 trn)
c [ternres-9] fully completed ternary resolution
c [basicprobe-5] limit 13379702 penalty 0 = 0 + 0
c [basicprobe-5-0] 482 sched 11%, 198 failed, 16 lifted, 7743 hbrs
c [decomp-33] removed 307 variables
c [basicprobe-5-1] 169 probes remain 4% after last round
c [basicprobe-5-1] 363 units = 334 failed (92%) + 29 lifted (8%)
c [basicprobe-5-1] removed 489 variables, found 24359 hbrs
c [bate-3] eliminated 48 asymmetric tautologies during probing
c [unhide-13] limit 535188 with penalty 0 = 0 + 0
c [unhide-13-23] 1 units, 74 failed, 2416 tauts, 0 hbrs, 2220 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 523 transitive binary clauses
c [transred-9] found 2 units
c [cce-9] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 3 clauses out of 3 (100%) of length 13
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 11
c [cce-9-1] eliminated 1 clauses out of 9 (11%) of length 10
c [cce-9-1] eliminated 2 clauses out of 9 (22%) of length 9
c [cce-9-1] eliminated 2 clauses out of 21 (10%) of length 8
c [cce-9-1] eliminated 3 clauses out of 41 (7%) of length 7
c [cce-9-1] eliminated 3 clauses out of 139 (2%) of length 6
c [cce-9-1] eliminated 9 clauses out of 395 (2%) of length 5
c [cce-9-1] eliminated 26 clauses out of 931 (3%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 50 large clauses in 3912031 steps
c [cce-9-1] allowing another 1956015 steps for small clauses
c [cce-9-1] scheduling 17530 clauses = 12901 binary + 4629 ternary
c [cce-9-1] tried to eliminate 6370 small clauses 36%
c [cce-9-1] eliminated 571 binary clauses 4%
c [cce-9-1] eliminated 85 ternary clauses 2%
c [cce-9-1] eliminated 656 small clauses 4%
c [cce-9-1] eliminated 694 small clauses in 30000000 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 744 covered clauses in round 1
c [cce-9] eliminated 744 covered clauses in TOTAL during 1 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 4059 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 346 variables 9% in round 1 in 1365023 steps
c [elim-13-1] backward subsumption/strengthening limit 1365000
c [elim-13-1-1] backward checking 1298 touched variables 32%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 1 and strengthened 4 clauses in 138853 steps
c [elim-13-1] rescheduled 22 variables 1% by backward subsumption
c [elim-13-2] eliminated 1 variables 0% in round 2 in 7619 steps
c [elim-13-2] backward subsumption/strengthening limit 7600
c [elim-13-2-1] backward checking 8 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 0 and strengthened 0 clauses in 4659 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 347 = 9% variables out of 4059 scheduled
c [bca-9] limit of 10000000 steps and 43344 added (scaled 2)
c [bca-9] 6289 out of 7426 literals actually usable 85%
c [bca-9] added 24 blocked clauses in 17453 steps
c [sweep-8] limit 500000 penalty 1 = 1 + 0
c [sweep-8-1] 644 pos 17.3% + 3068 neg 82.7% = 3712 sched 100.0% ret 0
c [sweep-8-1] 584116 steps 18 queries 630.22 avg class size
c [sweep-8-1] 530 decisions 17 SAT calls 123.18 avg env size
c [sweep-8-1] 3422 variables remain 92% (289 retained 8%)
c [decomp-34] removed 7 variables
c [sweep-8-1] removed 7 vars (0 failed, 0 eqs, 0 impls)
c [sweep-8] removed 7 vars in TOTAL (1 rounds, 17 queries)
c [sort-queue-13] sorted 1194 enqueued variables after 23042 conflicts
c [score-dist-13] active 2511 (68%), one 0 (0%), zero 1194 (32%)
c [score-dist-13] max exp 516, different 16 (3%)
c [score-dist-13] median active exp 509, avg 508.8
c [simplification-13] removed 852 variables 18.7% (3705 remain 2%)
c [simplification-13] removed 4698 irredundant clauses 18.0% (21377 remain 2%)
c [simplification-13] maximum reduction of 19% = max (19%, 18%)
c [simplification-13] large reduction 19% >= 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 35042 (soft 25042 + delta 10000)
c [simplification-13] new conflict limit 25042 (hard 35042)
c 
c [simplification-14] limit 25042 conflicts (hard 35042) hit after 25042 conflicts
c [ternres-10] limit 4000000 with penalty 0 = 0 + 0
c [ternres-10] all 3705 free variables schedulable
c [ternres-10] 62 ternary resolvents (0 bin, 62 trn)
c [ternres-10] fully completed ternary resolution
c [simpleprobe-6] all 3705 free variables schedulable
c [simpleprobe-6] limit 11098251 penalty 0 = 0 + 0
c [decomp-36] removed 2 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 2 variables, found 2196 hbrs, 1 units
c [unhide-14] limit 554912 with penalty 0 = 0 + 0
c [unhide-14-26] 0 units, 0 failed, 2713 tauts, 0 hbrs, 2366 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 460 transitive binary clauses
c [transred-10] found 2 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 3701 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 21 blocked clauses
c [block-4] 21 < 1/100 * 21281 = 212 considered unsuccessful
c [cce-10] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 51 (2%) of length 7
c [cce-10-1] eliminated 4 clauses out of 440 (1%) of length 5
c [cce-10-1] eliminated 47 clauses out of 967 (5%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 52 large clauses in 4541387 steps
c [cce-10-1] allowing another 2270693 steps for small clauses
c [cce-10-1] scheduling 15065 clauses = 11727 binary + 3338 ternary
c [cce-10-1] tried to eliminate 6616 small clauses 44%
c [cce-10-1] eliminated 315 binary clauses 3%
c [cce-10-1] eliminated 84 ternary clauses 3%
c [cce-10-1] eliminated 399 small clauses 3%
c [cce-10-1] eliminated 399 small clauses in 30000006 steps
c [cce-10-1] incomplete small round (ATE)
c [cce-10-1] eliminated 451 covered clauses in round 1
c [cce-10] eliminated 451 covered clauses in TOTAL during 1 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 3701 variables 100%
c [elim-14] limit of 55491259 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 48 variables 1% in round 1 in 1295099 steps
c [elim-14-1] backward subsumption/strengthening limit 1295000
c [elim-14-1-1] backward checking 357 touched variables 10%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 42532 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 48 = 1% variables out of 3701 scheduled
c [bca-10] limit of 10000000 steps and 42076 added (scaled 2)
c [bca-10] 6129 out of 7308 literals actually usable 84%
c [bca-10] added 13 blocked clauses in 18916 steps
c [sweep-9] limit 1000000 penalty 0 = 0 + 0
c [sweep-9-1] 605 pos 18.0% + 2761 neg 82.0% = 3366 sched 92.1% ret 287
c [sweep-9-1] 1009679 steps 84 queries 103.85 avg class size
c [sweep-9-1] 715 decisions 81 SAT calls 52.37 avg env size
c [sweep-9-1] 1491 variables remain 41% (2159 retained 59%)
c [decomp-37] removed 5 variables
c [sweep-9-1] removed 5 vars (0 failed, 2 eqs, 2 impls)
c [sweep-9] removed 5 vars in TOTAL (1 rounds, 83 queries)
c [sort-queue-14] sorted 1135 enqueued variables after 25042 conflicts
c [score-dist-14] active 2513 (69%), one 0 (0%), zero 1135 (31%)
c [score-dist-14] max exp 516, different 16 (3%)
c [score-dist-14] median active exp 509, avg 508.8
c [simplification-14] removed 57 variables 1.5% (3648 remain 2%)
c [simplification-14] removed 640 irredundant clauses 3.0% (20737 remain 2%)
c [simplification-14] maximum reduction of 3% = max (2%, 3%)
c [simplification-14] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-14] new conflict interval 5000
c [simplification-14] penalized conflict interval 5000 = 1 * 5000
c [simplification-14] hard conflict limit 40042 (soft 30042 + delta 10000)
c [simplification-14] new conflict limit 30042 (hard 40042)
c 
c [simplification-15] limit 30042 conflicts (hard 40042) hit after 30045 conflicts
c [quatres-9] found 957 quaternary clauses 52% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [ternres-11] limit 4000000 with penalty 0 = 0 + 0
c [ternres-11] all 3648 free variables schedulable
c [ternres-11] 13 ternary resolvents (0 bin, 13 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 125000 penalty 4 = 4 + 0
c [card-5] found 376 at-most-one constraints of average size 3.4
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 125000 for elimination
c [card-5] 376 out of 376 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 0 xors of average arity 0.0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-6] limit 304271 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 7293 literals 100%
c [treelook-6] scheduling used 139814 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 304271 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 333247 steps
c [treelook-6] 7245 literals remain 99%
c [treelook-6] 3641 variables remain to probed next time 100%
c [treelook-6] removed 4 variables, found 850 hbrs
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 488 transitive binary clauses
c [transred-11] found 3 units
c [cce-11] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 3 clauses out of 152 (2%) of length 6
c [cce-11-1] eliminated 6 clauses out of 438 (1%) of length 5
c [cce-11-1] eliminated 32 clauses out of 922 (3%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 41 large clauses in 4541569 steps
c [cce-11-1] allowing another 2270784 steps for small clauses
c [cce-11-1] scheduling 15800 clauses = 11374 binary + 4426 ternary
c [cce-11-1] tried to eliminate 6609 small clauses 42%
c [cce-11-1] eliminated 294 binary clauses 3%
c [cce-11-1] eliminated 92 ternary clauses 2%
c [cce-11-1] eliminated 386 small clauses 2%
c [cce-11-1] eliminated 437 small clauses in 30000000 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 478 covered clauses in round 1
c [cce-11] eliminated 478 covered clauses in TOTAL during 1 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 3639 variables 100%
c [elim-15] limit of 60854361 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 40 variables 1% in round 1 in 1248931 steps
c [elim-15-1] backward subsumption/strengthening limit 1248900
c [elim-15-1-1] backward checking 268 touched variables 7%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 1 clauses in 32525 steps
c [elim-15-1] rescheduled 20 variables 1% by backward subsumption
c [elim-15-2] no variable eliminated in round 2 in 9905 steps
c [elim-15] fully completed in 2 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 40 = 1% variables out of 3639 scheduled
c [bca-11] limit of 10000000 steps and 40901 added (scaled 2)
c [bca-11] 5955 out of 7200 literals actually usable 83%
c [bca-11] added 4 blocked clauses in 22861 steps
c [sweep-10] limit 1000000 penalty 0 = 0 + 0
c [sweep-10-1] 446 pos 30.4% + 1023 neg 69.6% = 1469 sched 40.8% ret 2130
c [sweep-10-1] 1115217 steps 55 queries 78.84 avg class size
c [sweep-10-1] 539 decisions 53 SAT calls 43.13 avg env size
c [sweep-10-1] 1173 variables remain 33% (2423 retained 67%)
c [decomp-40] removed 4 variables
c [sweep-10-1] removed 4 vars (0 failed, 1 eqs, 1 impls)
c [sweep-10] removed 4 vars in TOTAL (1 rounds, 54 queries)
c [sort-queue-15] sorted 1088 enqueued variables after 30045 conflicts
c [score-dist-15] active 2507 (70%), one 0 (0%), zero 1088 (30%)
c [score-dist-15] max exp 516, different 16 (3%)
c [score-dist-15] median active exp 509, avg 508.9
c [simplification-15] removed 53 variables 1.5% (3595 remain 2%)
c [simplification-15] removed 585 irredundant clauses 2.8% (20152 remain 2%)
c [simplification-15] maximum reduction of 3% = max (1%, 3%)
c [simplification-15] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-15] new conflict interval 10000
c [simplification-15] penalized conflict interval 10000 = 1 * 10000
c [simplification-15] hard conflict limit 50045 (soft 40045 + delta 10000)
c [simplification-15] new conflict limit 40045 (hard 50045)
c 
c [simplification-16] limit 40045 conflicts (hard 50045) hit after 40046 conflicts
c [ternres-12] limit 4000000 with penalty 0 = 0 + 0
c [ternres-12] all 3595 free variables schedulable
c [ternres-12] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-12] fully completed ternary resolution
c [basicprobe-6] limit 18126292 penalty 0 = 0 + 0
c [basicprobe-6-0] 364 sched 10%, 77 failed, 4 lifted, 4489 hbrs
c [decomp-42] removed 106 variables
c [basicprobe-6-1] 826 sched 24%, 83 failed, 6 lifted, 7575 hbrs
c [decomp-43] removed 115 variables
c [basicprobe-6-2] 105 probes remain 3% after last round
c [basicprobe-6-2] 213 units = 199 failed (93%) + 14 lifted (7%)
c [basicprobe-6-2] removed 265 variables, found 15384 hbrs
c [bate-4] eliminated 51 asymmetric tautologies during probing
c [unhide-15] limit 362525 with penalty 1 = 1 + 0
c [unhide-15-28] 0 units, 2 failed, 2492 tauts, 0 hbrs, 12740 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 513 transitive binary clauses
c [cce-12] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 2 (50%) of length 16
c [cce-12-1] eliminated 1 clauses out of 8 (12%) of length 9
c [cce-12-1] eliminated 2 clauses out of 135 (1%) of length 6
c [cce-12-1] eliminated 4 clauses out of 382 (1%) of length 5
c [cce-12-1] eliminated 21 clauses out of 796 (3%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 29 large clauses in 3596709 steps
c [cce-12-1] allowing another 1798354 steps for small clauses
c [cce-12-1] scheduling 14188 clauses = 10537 binary + 3651 ternary
c [cce-12-1] tried to eliminate 7894 small clauses 56%
c [cce-12-1] eliminated 478 binary clauses 5%
c [cce-12-1] eliminated 35 ternary clauses 1%
c [cce-12-1] eliminated 513 small clauses 4%
c [cce-12-1] eliminated 513 small clauses in 30000004 steps
c [cce-12-1] incomplete small round (ATE)
c [cce-12-1] eliminated 542 covered clauses in round 1
c [cce-12] eliminated 542 covered clauses in TOTAL during 1 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 3329 variables 100%
c [elim-16] limit of 72505168 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 189 variables 6% in round 1 in 1090425 steps
c [elim-16-1] backward subsumption/strengthening limit 1090400
c [elim-16-1-1] backward checking 856 touched variables 26%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 2 and strengthened 2 clauses in 90222 steps
c [elim-16-1] rescheduled 17 variables 1% by backward subsumption
c [elim-16-2] eliminated 1 variables 0% in round 2 in 5441 steps
c [elim-16-2] backward subsumption/strengthening limit 5400
c [elim-16-2-1] backward checking 8 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 0 and strengthened 0 clauses in 3934 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 190 = 6% variables out of 3329 scheduled
c [bca-12] limit of 10000000 steps and 35551 added (scaled 2)
c [bca-12] 4900 out of 6280 literals actually usable 78%
c [bca-12] added 13 blocked clauses in 24629 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 10875770 penalty 0 = 0 + 0
c [sweep-11-1] 353 pos 32.4% + 737 neg 67.6% = 1090 sched 34.7% ret 2049
c [sweep-11-1] 3422062 steps 378 queries 9.71 avg class size
c [sweep-11-1] 2289 decisions 376 SAT calls 26.28 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-44] removed 22 variables
c [sweep-11-1] removed 22 vars (0 failed, 6 eqs, 8 impls)
c [sweep-11-2] 531 pos 17.0% + 2586 neg 83.0% = 3117 sched 100.0% ret 0
c [sweep-11-2] 4810570 steps 413 queries 15.33 avg class size
c [sweep-11-2] 3257 decisions 402 SAT calls 32.00 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-45] removed 21 variables
c [sweep-11-2] removed 21 vars (0 failed, 16 eqs, 17 impls)
c [sweep-11-3] 527 pos 17.0% + 2569 neg 83.0% = 3096 sched 100.0% ret 0
c [sweep-11-3] 2645963 steps 173 queries 53.80 avg class size
c [sweep-11-3] 2215 decisions 166 SAT calls 57.89 avg env size
c [sweep-11-3] 706 variables remain 23% (2381 retained 77%)
c [decomp-46] removed 19 variables
c [sweep-11-3] removed 19 vars (0 failed, 7 eqs, 11 impls)
c [sweep-11] removed 62 vars in TOTAL (3 rounds, 961 queries)
c [sort-queue-16] sorted 767 enqueued variables after 40046 conflicts
c [score-dist-16] active 2310 (75%), one 0 (0%), zero 767 (25%)
c [score-dist-16] max exp 517, different 17 (3%)
c [score-dist-16] median active exp 509, avg 509.2
c [simplification-16] removed 518 variables 14.4% (3077 remain 1%)
c [simplification-16] removed 2960 irredundant clauses 14.7% (17192 remain 2%)
c [simplification-16] maximum reduction of 15% = max (14%, 15%)
c [simplification-16] large reduction 15% >= 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 52046 (soft 42046 + delta 10000)
c [simplification-16] new conflict limit 42046 (hard 52046)
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   42.0    3076    17192     41536   15789    251 19786   32    43   17  73%    282   29   43   12  374%
c i   42.0    3075    17192     41540   15792    251 19786   32    43   17  73%    280   29   43   12  372%
c 
c [simplification-17] limit 42048 conflicts (hard 52046) hit after 42051 conflicts
c [ternres-13] limit 4000000 with penalty 0 = 0 + 0
c [ternres-13] all 3075 free variables schedulable
c [ternres-13] 20 ternary resolvents (0 bin, 20 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-47] removed 2 variables
c [simpleprobe-7] all 3075 free variables schedulable
c [simpleprobe-7] limit 14911597 penalty 0 = 0 + 0
c [decomp-48] removed 48 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 48 variables, found 1610 hbrs, 19 units
c [unhide-16] limit 745579 with penalty 0 = 0 + 0
c [unhide-16-31] 0 units, 1 failed, 2522 tauts, 0 hbrs, 9451 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 616 transitive binary clauses
c [transred-13] found 1 units
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 1 (100%) of length 24
c [cce-13-1] eliminated 1 clauses out of 4 (25%) of length 13
c [cce-13-1] eliminated 1 clauses out of 11 (9%) of length 8
c [cce-13-1] eliminated 2 clauses out of 114 (2%) of length 6
c [cce-13-1] eliminated 8 clauses out of 359 (2%) of length 5
c [cce-13-1] eliminated 40 clauses out of 793 (5%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 53 large clauses in 3570675 steps
c [cce-13-1] allowing another 1785337 steps for small clauses
c [cce-13-1] scheduling 11847 clauses = 9284 binary + 2563 ternary
c [cce-13-1] tried to eliminate 11847 small clauses 100%
c [cce-13-1] eliminated 546 binary clauses 6%
c [cce-13-1] eliminated 196 ternary clauses 8%
c [cce-13-1] eliminated 742 small clauses 6%
c [cce-13-1] eliminated 750 small clauses in 43890899 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] completed small and large (ACCE)
c [cce-13-1] eliminated 803 covered clauses in round 1
c [cce-13-2] eliminated 1 clauses out of 3 (33%) of length 13
c [cce-13-2] eliminated 1 clauses out of 10 (10%) of length 8
c [cce-13-2] eliminated 3 clauses out of 112 (3%) of length 6
c [cce-13-2] eliminated 1 clauses out of 351 (0%) of length 5
c [cce-13-2] eliminated 6 clauses out of 753 (1%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 12 large clauses in 3123147 steps
c [cce-13-2] allowing another 1561573 steps for small clauses
c [cce-13-2] scheduling 11105 clauses = 8738 binary + 2367 ternary
c [cce-13-2] tried to eliminate 11105 small clauses 100%
c [cce-13-2] eliminated 24 binary clauses 0%
c [cce-13-2] eliminated 13 ternary clauses 1%
c [cce-13-2] eliminated 37 small clauses 0%
c [cce-13-2] eliminated 37 small clauses in 39112446 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 49 covered clauses in round 2
c [cce-13-3] eliminated 1 clauses out of 109 (1%) of length 6
c [cce-13-3] eliminated 2 clauses out of 350 (1%) of length 5
c [cce-13-3] eliminated 5 clauses out of 747 (1%) of length 4
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] eliminated 8 large clauses in 3079996 steps
c [cce-13-3] allowing another 1539998 steps for small clauses
c [cce-13-3] scheduling 11068 clauses = 8714 binary + 2354 ternary
c [cce-13-3] tried to eliminate 11068 small clauses 100%
c [cce-13-3] eliminated 2 binary clauses 0%
c [cce-13-3] eliminated 6 ternary clauses 0%
c [cce-13-3] eliminated 8 small clauses 0%
c [cce-13-3] eliminated 8 small clauses in 38856437 steps
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 16 covered clauses in round 3
c [cce-13] eliminated 868 covered clauses in TOTAL during 3 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 3025 variables 100%
c [elim-17] limit of 74557988 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 157 variables 5% in round 1 in 987314 steps
c [elim-17-1] backward subsumption/strengthening limit 987300
c [elim-17-1-1] backward checking 745 touched variables 25%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 7 clauses in 83728 steps
c [elim-17-1] rescheduled 35 variables 1% by backward subsumption
c [elim-17-2] no variable eliminated in round 2 in 15412 steps
c [elim-17] fully completed in 2 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 157 = 5% variables out of 3025 scheduled
c [bca-13] limit of 10000000 steps and 32049 added (scaled 2)
c [bca-13] 4430 out of 5738 literals actually usable 77%
c [bca-13] added 8 blocked clauses in 19710 steps
c [sweep-12] limit 1118369 penalty 0 = 0 + 0
c [sweep-12-1] 216 pos 34.0% + 420 neg 66.0% = 636 sched 22.2% ret 2232
c [sweep-12-1] 1220661 steps 143 queries 18.12 avg class size
c [sweep-12-1] 900 decisions 141 SAT calls 24.46 avg env size
c [sweep-12-1] 267 variables remain 9% (2600 retained 91%)
c [decomp-49] removed 1 variables
c [sweep-12-1] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-12] 1 < 1/1000 * 2868 = 2 considered unsuccessful
c [sweep-12] removed 1 vars in TOTAL (1 rounds, 142 queries)
c [sort-queue-17] sorted 735 enqueued variables after 42051 conflicts
c [score-dist-17] active 2132 (74%), one 0 (0%), zero 735 (26%)
c [score-dist-17] max exp 517, different 17 (3%)
c [score-dist-17] median active exp 509, avg 509.4
c [simplification-17] removed 208 variables 6.8% (2867 remain 1%)
c [simplification-17] removed 1455 irredundant clauses 8.5% (15737 remain 1%)
c [simplification-17] maximum reduction of 8% = max (7%, 8%)
c [simplification-17] large reduction 8% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 54051 (soft 44051 + delta 10000)
c [simplification-17] new conflict limit 44051 (hard 54051)
c 
c [simplification-18] limit 44051 conflicts (hard 54051) hit after 46051 conflicts
c [quatres-10] found 779 quaternary clauses 49% in total
c [quatres-10-1] removed 2 duplicate quaternary clauses
c [quatres-10-2] added 2 quaternary resolvents
c [ternres-14] limit 4000000 with penalty 0 = 0 + 0
c [ternres-14] all 2867 free variables schedulable
c [ternres-14] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-14] fully completed ternary resolution
c [treelook-7] limit 390864 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 5732 literals 100%
c [treelook-7] scheduling used 115730 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 390864 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 402429 steps
c [treelook-7] 5691 literals remain 99%
c [treelook-7] 2865 variables remain to probed next time 100%
c [treelook-7] removed 0 variables, found 4482 hbrs
c [unhide-17] limit 781729 with penalty 0 = 0 + 0
c [unhide-17-34] 1 units, 0 failed, 1767 tauts, 0 hbrs, 7000 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 436 transitive binary clauses
c [transred-14] found 5 units
c [cce-14] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 1 clauses out of 2 (50%) of length 18
c [cce-14-1] eliminated 1 clauses out of 2 (50%) of length 11
c [cce-14-1] eliminated 1 clauses out of 2 (50%) of length 10
c [cce-14-1] eliminated 2 clauses out of 8 (25%) of length 9
c [cce-14-1] eliminated 1 clauses out of 15 (7%) of length 8
c [cce-14-1] eliminated 2 clauses out of 351 (1%) of length 5
c [cce-14-1] eliminated 6 clauses out of 737 (1%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 14 large clauses in 3262220 steps
c [cce-14-1] allowing another 1631110 steps for small clauses
c [cce-14-1] scheduling 12065 clauses = 8523 binary + 3542 ternary
c [cce-14-1] tried to eliminate 8611 small clauses 71%
c [cce-14-1] eliminated 30 binary clauses 0%
c [cce-14-1] eliminated 34 ternary clauses 1%
c [cce-14-1] eliminated 64 small clauses 1%
c [cce-14-1] eliminated 77 small clauses in 30000002 steps
c [cce-14-1] incomplete small round (ATE)
c [cce-14-1] eliminated 91 covered clauses in round 1
c [cce-14] eliminated 91 covered clauses in TOTAL during 1 rounds
c [cce-14] 91 < 1/100 * 15721 = 157 considered unsuccessful
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 2861 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 1563458380 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 21 variables 1% in round 1 in 961876 steps
c [elim-18-1] backward subsumption/strengthening limit 961800
c [elim-18-1-1] backward checking 159 touched variables 6%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 0 and strengthened 0 clauses in 16197 steps
c [elim-18] fully completed in 1 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 21 = 1% variables out of 2861 scheduled
c [elim-18] 21 < 1/100 * 2861 = 28 considered unsuccessful
c [bca-14] limit of 10000000 steps and 31809 added (scaled 2)
c [bca-14] 4308 out of 5682 literals actually usable 76%
c [bca-14] added 11 blocked clauses in 23064 steps
c [sort-queue-18] sorted 725 enqueued variables after 46051 conflicts
c [score-dist-18] active 2115 (74%), one 0 (0%), zero 725 (26%)
c [score-dist-18] max exp 517, different 17 (3%)
c [score-dist-18] median active exp 509, avg 509.6
c [simplification-18] removed 27 variables 0.9% (2840 remain 1%)
c [simplification-18] removed 118 irredundant clauses 0.7% (15619 remain 1%)
c [simplification-18] maximum reduction of 1% = max (1%, 1%)
c [simplification-18] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-18] new conflict interval 20000
c [simplification-18] penalized conflict interval 20000 = 1 * 20000
c [simplification-18] hard conflict limit 76051 (soft 66051 + delta 10000)
c [simplification-18] new conflict limit 66051 (hard 76051)
c 
c [simplification-19] limit 66051 conflicts (hard 76051) hit after 66051 conflicts
c [ternres-15] limit 5174934 with penalty 0 = 0 + 0
c [ternres-15] all 2840 free variables schedulable
c [ternres-15] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-15] fully completed ternary resolution
c [basicprobe-7] limit 25874670 penalty 0 = 0 + 0
c [basicprobe-7-0] 224 sched 8%, 21 failed, 1 lifted, 1188 hbrs
c [decomp-53] removed 25 variables
c [basicprobe-7-1] 739 sched 27%, 27 failed, 1 lifted, 3572 hbrs
c [decomp-54] removed 32 variables
c [basicprobe-7-2] 729 sched 26%, 6 failed, 0 lifted, 1099 hbrs
c [decomp-55] removed 6 variables
c [basicprobe-7-3] 735 sched 26%, 1 failed, 0 lifted, 128 hbrs
c [decomp-56] removed 1 variables
c [basicprobe-7-4] 734 sched 26%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-7-5] 692 probes remain 25% after last round
c [basicprobe-7-5] 57 units = 55 failed (96%) + 2 lifted (4%)
c [basicprobe-7-5] removed 64 variables, found 6002 hbrs
c [bate-5] eliminated 13 asymmetric tautologies during probing
c [unhide-18] limit 1034986 with penalty 0 = 0 + 0
c [unhide-18-36] 0 units, 0 failed, 1178 tauts, 0 hbrs, 20935 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 349 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 2776 variables 100%
c [block-5] limit of 3234333 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 4 blocked clauses
c [block-5] 4 < 1/100 * 15233 = 152 considered unsuccessful
c [bca-15] limit of 10000000 steps and 31035 added (scaled 2)
c [bca-15] 4046 out of 5554 literals actually usable 73%
c [bca-15] added 5 blocked clauses in 39707 steps
c [sweep-13] limit 776240 penalty 1 = 1 + 0
c [sweep-13-1] 91 pos 34.5% + 173 neg 65.5% = 264 sched 9.5% ret 2512
c [sweep-13-1] 781455 steps 44 queries 27.52 avg class size
c [sweep-13-1] 428 decisions 43 SAT calls 27.35 avg env size
c [sweep-13-1] 186 variables remain 7% (2590 retained 93%)
c [sweep-13-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-13] removed 0 vars in TOTAL (1 rounds, 43 queries)
c [sort-queue-19] sorted 640 enqueued variables after 66051 conflicts
c [score-dist-19] active 2136 (77%), one 0 (0%), zero 640 (23%)
c [score-dist-19] max exp 517, different 17 (3%)
c [score-dist-19] median active exp 510, avg 510.0
c [simplification-19] removed 64 variables 2.3% (2776 remain 1%)
c [simplification-19] removed 390 irredundant clauses 2.5% (15229 remain 1%)
c [simplification-19] maximum reduction of 2% = max (2%, 2%)
c [simplification-19] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-19] new conflict interval 26666
c [simplification-19] penalized conflict interval 26666 = 1 * 26666
c [simplification-19] hard conflict limit 106050 (soft 92717 + delta 13333)
c [simplification-19] new conflict limit 92717 (hard 106050)
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 -   57.4    2776    15229     89479   23895    330 19038   33    45   19  73%    494   14   31   24  132%
c 
c [simplification-20] limit 92717 conflicts (hard 106050) hit after 92721 conflicts
c [quatres-11] found 757 quaternary clauses 41% in total
c [ternres-16] limit 7152936 with penalty 0 = 0 + 0
c [ternres-16] all 2776 free variables schedulable
c [ternres-16] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-6] limit 125000 penalty 4 = 4 + 0
c [gauss-6] extracted 2 xors of average arity 3.0
c [gauss-6] connected 6 occurrences of 6 variables (average 1.0)
c [gauss-6] limit 125000 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 2776 free variables schedulable
c [simpleprobe-8] limit 28611744 penalty 0 = 0 + 0
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 0 variables, found 1049 hbrs, 0 units
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 550 transitive binary clauses
c [cce-15] limit of 17882340 steps penalty 1 = 1 + 0
c [cce-15-1] eliminated 3 clauses out of 39 (8%) of length 7
c [cce-15-1] eliminated 2 clauses out of 131 (2%) of length 6
c [cce-15-1] eliminated 1 clauses out of 334 (0%) of length 5
c [cce-15-1] eliminated 12 clauses out of 707 (2%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 18 large clauses in 3141259 steps
c [cce-15-1] allowing another 1570629 steps for small clauses
c [cce-15-1] scheduling 10662 clauses = 8465 binary + 2197 ternary
c [cce-15-1] tried to eliminate 4889 small clauses 46%
c [cce-15-1] eliminated 75 binary clauses 1%
c [cce-15-1] eliminated 17 ternary clauses 1%
c [cce-15-1] eliminated 92 small clauses 1%
c [cce-15-1] eliminated 92 small clauses in 17882348 steps
c [cce-15-1] incomplete small round (ACCE)
c [cce-15-1] eliminated 110 covered clauses in round 1
c [cce-15] eliminated 110 covered clauses in TOTAL during 1 rounds
c [cce-15] 110 < 1/100 * 15226 = 152 considered unsuccessful
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 2776 variables 100%
c [elim-19] limit of 71529361 steps penalty 1 = 1 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 39 variables 1% in round 1 in 928137 steps
c [elim-19-1] backward subsumption/strengthening limit 928100
c [elim-19-1-1] backward checking 270 touched variables 10%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 0 and strengthened 0 clauses in 29865 steps
c [elim-19] fully completed in 1 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 39 = 1% variables out of 2776 scheduled
c [bca-16] limit of 10000000 steps and 30735 added (scaled 2)
c [bca-16] 3969 out of 5476 literals actually usable 72%
c [bca-16] added 13 blocked clauses in 34974 steps
c [sort-queue-20] sorted 607 enqueued variables after 92721 conflicts
c [score-dist-20] active 2130 (78%), one 0 (0%), zero 607 (22%)
c [score-dist-20] max exp 518, different 18 (3%)
c [score-dist-20] median active exp 510, avg 510.5
c [simplification-20] removed 39 variables 1.4% (2737 remain 1%)
c [simplification-20] removed 151 irredundant clauses 1.0% (15078 remain 1%)
c [simplification-20] maximum reduction of 1% = max (1%, 1%)
c [simplification-20] geometric conflict interval increment 13333 = 26666 / 2
c [simplification-20] new conflict interval 39999
c [simplification-20] penalized conflict interval 39999 = 1 * 39999
c [simplification-20] hard conflict limit 152719 (soft 132720 + delta 19999)
c [simplification-20] new conflict limit 132720 (hard 152719)
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.9    2737    15078    122389   25036    343 19179   36    49   18  73%    703    9   27   31   89%
c 
c [simplification-21] limit 132720 conflicts (hard 152719) hit after 132721 conflicts
c [ternres-17] limit 9783615 with penalty 0 = 0 + 0
c [ternres-17] all 2737 free variables schedulable
c [ternres-17] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 305737 penalty 4 = 4 + 0
c [card-6] found 634 at-most-one constraints of average size 3.4
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 305737 for elimination
c [card-6] 634 out of 634 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [unhide-19] limit 978361 with penalty 1 = 1 + 0
c [unhide-19-38] 0 units, 0 failed, 764 tauts, 0 hbrs, 29525 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 298 transitive binary clauses
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 2737 variables 100%
c [elim-20] limit of 195672306 steps penalty 0 = 0 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 5 variables 0% in round 1 in 923292 steps
c [elim-20-1] backward subsumption/strengthening limit 923200
c [elim-20-1-1] backward checking 36 touched variables 1%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 1 and strengthened 0 clauses in 4455 steps
c [elim-20-1] rescheduled 8 variables 0% by backward subsumption
c [elim-20-2] no variable eliminated in round 2 in 2917 steps
c [elim-20] fully completed in 2 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 5 = 0% variables out of 2737 scheduled
c [elim-20] 5 < 1/100 * 2737 = 27 considered unsuccessful
c [bca-17] limit of 10000000 steps and 30716 added (scaled 2)
c [bca-17] 3944 out of 5466 literals actually usable 72%
c [bca-17] added 8 blocked clauses in 42361 steps
c [sort-queue-21] sorted 597 enqueued variables after 132721 conflicts
c [score-dist-21] active 2135 (78%), one 0 (0%), zero 597 (22%)
c [score-dist-21] max exp 518, different 18 (3%)
c [score-dist-21] median active exp 511, avg 510.8
c [simplification-21] removed 5 variables 0.2% (2732 remain 1%)
c [simplification-21] removed 13 irredundant clauses 0.1% (15065 remain 1%)
c [simplification-21] maximum reduction of 0% = max (0%, 0%)
c [simplification-21] full geometric conflict interval increment 39999
c [simplification-21] new conflict interval 79998
c [simplification-21] penalized conflict interval 79998 = 1 * 79998
c [simplification-21] hard conflict limit 252718 (soft 212719 + delta 39999)
c [simplification-21] new conflict limit 212719 (hard 252718)
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 -   70.1    2732    15065    154615   25566    336 18130   29    39   18  75%    828   -2   24   31   76%
c -   75.0    2732    15065    187949   24281    341 18131   36    50   18  72%    906    8   34   32  106%
c 
c [simplification-22] limit 212719 conflicts (hard 252718) hit after 216303 conflicts
c [ternres-18] limit 14711218 with penalty 0 = 0 + 0
c [ternres-18] all 2732 free variables schedulable
c [ternres-18] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-18] fully completed ternary resolution
c [treelook-8] limit 735560 penalty 1 = 1 + 0 boost 1
c [treelook-8] scheduled 5462 literals 100%
c [treelook-8] scheduling used 191671 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 735560 penalty 1 = 1 + 0 boost 1
c [treelook-8] used 742010 steps
c [treelook-8] 5391 literals remain 99%
c [treelook-8] 2729 variables remain to probed next time 100%
c [treelook-8] removed 1 variables, found 4070 hbrs
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 440 transitive binary clauses
c [bca-18] limit of 10000000 steps and 30700 added (scaled 2)
c [bca-18] 3921 out of 5464 literals actually usable 72%
c [bca-18] added 3 blocked clauses in 57081 steps
c [sweep-14] limit 1103341 penalty 2 = 2 + 0
c [sweep-14-1] 51 pos 28.0% + 131 neg 72.0% = 182 sched 6.7% ret 2549
c [sweep-14-1] 1107630 steps 110 queries 8.96 avg class size
c [sweep-14-1] 654 decisions 109 SAT calls 22.79 avg env size
c [sweep-14-1] 30 variables remain 1% (2701 retained 99%)
c [sweep-14-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-14] removed 0 vars in TOTAL (1 rounds, 109 queries)
c [sort-queue-22] sorted 578 enqueued variables after 216303 conflicts
c [score-dist-22] active 2153 (79%), one 0 (0%), zero 578 (21%)
c [score-dist-22] max exp 519, different 19 (4%)
c [score-dist-22] median active exp 511, avg 511.3
c [simplification-22] removed 1 variables 0.0% (2731 remain 1%)
c [simplification-22] removed 10 irredundant clauses 0.1% (15055 remain 1%)
c [simplification-22] maximum reduction of 0% = max (0%, 0%)
c [simplification-22] full geometric conflict interval increment 79998
c [simplification-22] new conflict interval 159996
c [simplification-22] penalized conflict interval 159996 = 1 * 159996
c [simplification-22] hard conflict limit 456297 (soft 376299 + delta 79998)
c [simplification-22] new conflict limit 376299 (hard 456297)
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 -   81.5    2731    15055    224085   26004    343 21713   24    36   19  65%    956   -7   18   31   59%
c -   87.1    2731    15055    259581   26055    356 21717   25    31   19  80%    984   -8   24   28   84%
c -   92.9    2731    15055    296259   26853    362 21717   22    32   19  68%   1001   -4   17   26   63%
c -   98.7    2731    15055    331624   27934    371 21720   34    46   19  74%   1011    8   42   28  148%
c -  104.9    2731    15055    368381   27963    379 21721   28    36   26  76%   1016   -2   30   28  107%
c 
c [simplification-23] limit 376299 conflicts (hard 456297) hit after 386481 conflicts
c [quatres-12] found 853 quaternary clauses 29% in total
c [ternres-19] limit 25339008 with penalty 0 = 0 + 0
c [ternres-19] all 2731 free variables schedulable
c [ternres-19] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-19] fully completed ternary resolution
c [basicprobe-8] limit 126695042 penalty 0 = 0 + 0
c [basicprobe-8-0] 703 sched 26%, 11 failed, 0 lifted, 1880 hbrs
c [decomp-66] removed 12 variables
c [basicprobe-8-1] 736 sched 27%, 8 failed, 0 lifted, 651 hbrs
c [decomp-67] removed 8 variables
c [basicprobe-8-2] 736 sched 27%, 3 failed, 0 lifted, 173 hbrs
c [decomp-68] removed 3 variables
c [basicprobe-8-3] 736 sched 27%, 0 failed, 0 lifted, 27 hbrs
c [basicprobe-8-4] 735 sched 27%, 0 failed, 0 lifted, 22 hbrs
c [basicprobe-8-5] 735 sched 27%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-8-6] 735 sched 27%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-8-7] 735 sched 27%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-8-8] 735 sched 27%, 0 failed, 0 lifted, 18 hbrs
c [basicprobe-8-8] round limit 8 hit
c [basicprobe-8-8] 22 units = 22 failed (100%) + 0 lifted (0%)
c [basicprobe-8-8] removed 23 variables, found 2796 hbrs
c [bate-6] eliminated 4 asymmetric tautologies during probing
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 454 transitive binary clauses
c [cce-16] limit of 31673760 steps penalty 2 = 2 + 0
c [cce-16-1] eliminated 1 clauses out of 16 (6%) of length 8
c [cce-16-1] eliminated 2 clauses out of 335 (1%) of length 5
c [cce-16-1] eliminated 3 clauses out of 711 (0%) of length 4
c [cce-16-1] completed large round (ATE)
c [cce-16-1] eliminated 6 large clauses in 2992990 steps
c [cce-16-1] allowing another 1496495 steps for small clauses
c [cce-16-1] scheduling 11506 clauses = 8316 binary + 3190 ternary
c [cce-16-1] tried to eliminate 9504 small clauses 83%
c [cce-16-1] eliminated 149 binary clauses 2%
c [cce-16-1] eliminated 30 ternary clauses 1%
c [cce-16-1] eliminated 179 small clauses 2%
c [cce-16-1] eliminated 179 small clauses in 31673764 steps
c [cce-16-1] incomplete small round (ATE)
c [cce-16-1] eliminated 185 covered clauses in round 1
c [cce-16] eliminated 185 covered clauses in TOTAL during 1 rounds
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 2708 variables 100%
c [elim-21] limit of 253390084 steps penalty 1 = 1 + 0
c [elim-21] rescheduling of touched variables disabled
c [elim-21-1] eliminated 21 variables 1% in round 1 in 894710 steps
c [elim-21-1] backward subsumption/strengthening limit 894700
c [elim-21-1-1] backward checking 133 touched variables 5%
c [elim-21-1-1] fully completed backward checking in 1 rounds
c [elim-21-1] subsumed 0 and strengthened 0 clauses in 13485 steps
c [elim-21] fully completed in 1 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 21 = 1% variables out of 2708 scheduled
c [elim-21] 21 < 1/100 * 2708 = 27 considered unsuccessful
c [bca-19] limit of 10000000 steps and 29915 added (scaled 2)
c [bca-19] 3819 out of 5376 literals actually usable 71%
c [bca-19] added 4 blocked clauses in 45554 steps
c [sort-queue-23] sorted 513 enqueued variables after 386481 conflicts
c [score-dist-23] active 2174 (81%), one 0 (0%), zero 513 (19%)
c [score-dist-23] max exp 520, different 20 (4%)
c [score-dist-23] median active exp 512, avg 511.9
c [simplification-23] removed 44 variables 1.6% (2687 remain 1%)
c [simplification-23] removed 393 irredundant clauses 2.6% (14662 remain 1%)
c [simplification-23] maximum reduction of 3% = max (2%, 3%)
c [simplification-23] geometric conflict interval increment 39999 = 159996 / 4
c [simplification-23] new conflict interval 199995
c [simplification-23] penalized conflict interval 199995 = 1 * 199995
c [simplification-23] hard conflict limit 686473 (soft 586476 + delta 99997)
c [simplification-23] new conflict limit 586476 (hard 686473)
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 -  116.0    2687    14662    415102   28690    379 22348   25    33   18  75%   1020   -5   23   28   82%
c -  122.8    2687    14662    454849   29555    384 22348   24    34   18  72%   1022   -3   31   28  114%
c -  128.7    2687    14662    494078   29984    386 22348   26    34   24  78%   1023   -0   29   26  112%
c -  135.3    2687    14662    534056   30621    389 22350   31    39   24  78%   1023    5   30   26  113%
c -  143.1    2687    14662    575913   30852    392 22352   24    32   24  76%   1024   -3   24   27   91%
c 
c [simplification-24] limit 586476 conflicts (hard 686473) hit after 596735 conflicts
c [unhide-20] limit 1976689 with penalty 2 = 2 + 0
c [unhide-20-41] 0 units, 0 failed, 2350 tauts, 0 hbrs, 31799 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 208 transitive binary clauses
c [bca-20] limit of 10000000 steps and 29911 added (scaled 2)
c [bca-20] 3741 out of 5376 literals actually usable 70%
c [bca-20] added 11 blocked clauses in 56408 steps
c [sort-queue-24] sorted 478 enqueued variables after 596735 conflicts
c [score-dist-24] active 2209 (82%), one 0 (0%), zero 478 (18%)
c [score-dist-24] max exp 520, different 20 (4%)
c [score-dist-24] median active exp 512, avg 512.4
c [simplification-24] removed 0 variables 0.0% (2687 remain 1%)
c [simplification-24] removed 3 irredundant clauses 0.0% (14659 remain 1%)
c [simplification-24] maximum reduction of 0% = max (0%, 0%)
c [simplification-24] full geometric conflict interval increment 199995
c [simplification-24] new conflict interval 399990
c [simplification-24] penalized conflict interval 399990 = 1 * 399990
c [simplification-24] hard conflict limit 1196720 (soft 996725 + delta 199995)
c [simplification-24] new conflict limit 996725 (hard 1196720)
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.5    2687    14659    618737   31397    383 19820   23    33   20  69%   1024   -0   19   25   78%
c i  153.2    2686    14659    630860   41432    385 19821   20    28   25  73%   1024   -5   13   24   55%
c -  158.2    2686    14659    661277   32332    386 19821   26    36   20  72%  -4857    2   25   25   99%
c -  165.0    2686    14659    704040   33026    387 19821   23    31   20  74%  -2038   -2   22   24   89%
c -  172.6    2686    14659    750094   33206    390 19821   25    31   20  80%   -493   -0   21   24   90%
c -  181.7    2686    14659    795093   34884    392 19821   30    37   27  81%    261    2   29   27  105%
c -  190.9    2686    14659    841054   35296    393 19821   24    29   27  84%    645   -6   23   28   82%
c -  199.2    2686    14659    888008   35274    394 19821   26    31   28  84%    839   -1   26   25  105%
c -  208.1    2686    14659    938019   35986    395 19821   25    31   27  79%    938    1   25   25  100%
c -  217.0    2686    14659    987326   36729    396 19821   21    25   27  83%    983   -5   17   24   72%
c 
c [simplification-25] limit 996725 conflicts (hard 1196720) hit after 996725 conflicts
c [ternres-20] limit 34420771 with penalty 1 = 1 + 0
c [ternres-20] all 2686 free variables schedulable
c [ternres-20] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-75] removed 1 variables
c [simpleprobe-9] all 2686 free variables schedulable
c [simpleprobe-9] limit 100000000 penalty 1 = 1 + 0
c [decomp-76] removed 1 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 1 variables, found 840 hbrs, 0 units
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 360 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 2685 variables 100%
c [block-6] limit of 43025964 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 0 blocked clauses
c [cce-17] limit of 172103856 steps penalty 1 = 1 + 0
c [cce-17-1] eliminated 2 clauses out of 329 (1%) of length 5
c [cce-17-1] eliminated 14 clauses out of 719 (2%) of length 4
c [cce-17-1] completed large round (ACCE)
c [cce-17-1] eliminated 16 large clauses in 3088276 steps
c [cce-17-1] allowing another 1544138 steps for small clauses
c [cce-17-1] scheduling 10240 clauses = 8130 binary + 2110 ternary
c [cce-17-1] tried to eliminate 10240 small clauses 100%
c [cce-17-1] eliminated 92 binary clauses 1%
c [cce-17-1] eliminated 29 ternary clauses 1%
c [cce-17-1] eliminated 121 small clauses 1%
c [cce-17-1] eliminated 121 small clauses in 34936832 steps
c [cce-17-1] completed small round (ACCE)
c [cce-17-1] eliminated 137 covered clauses in round 1
c [cce-17-2] eliminated 1 clauses out of 37 (3%) of length 7
c [cce-17-2] eliminated 1 clauses out of 327 (0%) of length 5
c [cce-17-2] eliminated 3 clauses out of 705 (0%) of length 4
c [cce-17-2] completed large round (ACCE)
c [cce-17-2] eliminated 5 large clauses in 2975444 steps
c [cce-17-2] allowing another 1487722 steps for small clauses
c [cce-17-2] scheduling 10119 clauses = 8038 binary + 2081 ternary
c [cce-17-2] tried to eliminate 10119 small clauses 100%
c [cce-17-2] eliminated 5 binary clauses 0%
c [cce-17-2] eliminated 5 ternary clauses 0%
c [cce-17-2] eliminated 10 small clauses 0%
c [cce-17-2] eliminated 10 small clauses in 34121844 steps
c [cce-17-2] completed small round (ACCE)
c [cce-17-2] eliminated 15 covered clauses in round 2
c [cce-17-3] completed large round (ACCE)
c [cce-17-3] allowing another 1479912 steps for small clauses
c [cce-17-3] scheduling 10109 clauses = 8033 binary + 2076 ternary
c [cce-17-3] tried to eliminate 10109 small clauses 100%
c [cce-17-3] eliminated 2 binary clauses 0%
c [cce-17-3] eliminated 2 ternary clauses 0%
c [cce-17-3] eliminated 4 small clauses 0%
c [cce-17-3] eliminated 4 small clauses in 34025770 steps
c [cce-17-3] completed small round (ACCE)
c [cce-17-3] eliminated 4 covered clauses in round 3
c [cce-17] eliminated 156 covered clauses in TOTAL during 3 rounds
c [bca-21] limit of 10000000 steps and 29579 added (scaled 2)
c [bca-21] 3685 out of 5372 literals actually usable 69%
c [bca-21] added 5 blocked clauses in 52761 steps
c [sort-queue-25] sorted 447 enqueued variables after 996725 conflicts
c [score-dist-25] active 2238 (83%), one 0 (0%), zero 447 (17%)
c [score-dist-25] max exp 521, different 21 (4%)
c [score-dist-25] median active exp 513, avg 513.1
c [simplification-25] removed 1 variables 0.0% (2685 remain 1%)
c [simplification-25] removed 169 irredundant clauses 1.2% (14490 remain 1%)
c [simplification-25] maximum reduction of 1% = max (0%, 1%)
c [simplification-25] geometric conflict interval increment 199995 = 399990 / 2
c [simplification-25] new conflict interval 599985
c [simplification-25] penalized conflict interval 599985 = 1 * 599985
c [simplification-25] hard conflict limit 1896702 (soft 1596710 + delta 299992)
c [simplification-25] new conflict limit 1596710 (hard 1896702)
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 -  228.3    2685    14490   1035739   37218    451 20374   24    31   20  79%   1005   -2   21   26   82%
c -  238.5    2685    14490   1087823   36857    454 20374   26    31   25  84%   1015   -2   25   26   97%
c -  247.2    2685    14490   1142662   37145    456 20374   20    24   25  83%   1020   -5   18   23   78%
c -  256.1    2685    14490   1196779   39144    465 20376   40    50   27  80%   1022   19   42   26  165%
c -  267.1    2685    14490   1249825   39981    465 20377   30    37   27  81%   1023    1   25   28   88%
c -  276.4    2685    14490   1300834   39990    467 20377   26    32   27  80%   1024   -1   32   25  127%
c -  287.2    2685    14490   1354908   40337    467 20377   28    34   27  82%   1024    2   29   25  116%
c -  297.7    2685    14490   1411447   41559    466 20378   21    26   27  80%   1024   -5   20   24   82%
c -  306.6    2685    14490   1466170   42213    472 20378   22    28   27  78%   1024   -1   18   23   80%
c -  316.9    2685    14490   1521199   43316    474 20378   21    27   26  79%   1024   -1   22   22   99%
c -  326.6    2685    14490   1574987   43061    476 20378   26    32   27  81%   1024    1   29   24  122%
c 
c [simplification-26] limit 1596710 conflicts (hard 1896702) hit after 1597301 conflicts
c [ternres-21] limit 116007138 with penalty 0 = 0 + 0
c [ternres-21] all 2685 free variables schedulable
c [ternres-21] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-21] fully completed ternary resolution
c [gauss-7] limit 1450089 penalty 4 = 4 + 0
c [gauss-7] extracted 14 xors of average arity 3.0
c [gauss-7] connected 42 occurrences of 15 variables (average 2.8)
c [gauss-7] limit 1450089 penalty 4 = 4 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-9] limit 11600713 penalty 0 = 0 + 0 boost 1
c [treelook-9] scheduled 5368 literals 100%
c [treelook-9] scheduling used 229146 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 11600713 penalty 0 = 0 + 0 boost 1
c [treelook-9] used 11622162 steps
c [treelook-9] 3262 literals remain 62%
c [treelook-9] 2381 variables remain to probed next time 91%
c [decomp-78] removed 5 variables
c [treelook-9] removed 73 variables, found 81079 hbrs
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 1599 transitive binary clauses
c [transred-22] found 1 units
c [cce-18] almost no limit of 4000000000 steps
c [cce-18-1] eliminated 1 clauses out of 119 (1%) of length 6
c [cce-18-1] eliminated 3 clauses out of 678 (0%) of length 4
c [cce-18-1] completed large round (ATE)
c [cce-18-1] eliminated 4 large clauses in 2443473 steps
c [cce-18-1] allowing another 1221736 steps for small clauses
c [cce-18-1] scheduling 9960 clauses = 7982 binary + 1978 ternary
c [cce-18-1] tried to eliminate 9960 small clauses 100%
c [cce-18-1] eliminated 94 binary clauses 1%
c [cce-18-1] eliminated 20 ternary clauses 1%
c [cce-18-1] eliminated 114 small clauses 1%
c [cce-18-1] eliminated 121 small clauses in 29988844 steps
c [cce-18-1] completed small round (ATE)
c [cce-18-1] eliminated 125 covered clauses in round 1
c [cce-18-2] completed large round (ATE)
c [cce-18-2] allowing another 1214632 steps for small clauses
c [cce-18-2] scheduling 9846 clauses = 7888 binary + 1958 ternary
c [cce-18-2] tried to eliminate 9846 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 125 covered clauses in TOTAL during 2 rounds
c [cce-18] 125 < 1/100 * 13956 = 139 considered unsuccessful
c [elim-22] scheduling all variables this time
c [elim-22] scheduled 2611 variables 100%
c [elim-22] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-22] rescheduling of touched variables disabled
c [elim-22-1] eliminated 66 variables 3% in round 1 in 841786 steps
c [elim-22-1] backward subsumption/strengthening limit 841700
c [elim-22-1-1] backward checking 396 touched variables 15%
c [elim-22-1-1] fully completed backward checking in 1 rounds
c [elim-22-1] subsumed 0 and strengthened 5 clauses in 44430 steps
c [elim-22-1] rescheduled 11 variables 0% by backward subsumption
c [elim-22-2] no variable eliminated in round 2 in 4592 steps
c [elim-22] fully completed in 2 rounds
c [elim-22] transition to [ all 0 rem 0 ] state
c [elim-22] eliminated 66 = 3% variables out of 2611 scheduled
c [bca-22] limit of 10000000 steps and 28145 added (scaled 2)
c [bca-22] 3452 out of 5092 literals actually usable 68%
c [bca-22] added 4 blocked clauses in 58520 steps
c [sweep-15] limit 4350267 penalty 3 = 3 + 0
c [sweep-15-1] 3 pos 10.0% + 27 neg 90.0% = 30 sched 1.2% ret 2515
c [sweep-15-1] 86007 steps 24 queries 5.33 avg class size
c [sweep-15-1] 149 decisions 23 SAT calls 22.48 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-79] removed 1 variables
c [sweep-15-1] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-15-2] 447 pos 17.6% + 2097 neg 82.4% = 2544 sched 100.0% ret 0
c [sweep-15-2] 4306100 steps 26 queries 160.35 avg class size
c [sweep-15-2] 1082 decisions 25 SAT calls 197.20 avg env size
c [sweep-15-2] 1830 variables remain 72% (714 retained 28%)
c [sweep-15-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-15] 1 < 1/1000 * 2545 = 2 considered unsuccessful
c [sweep-15] removed 1 vars in TOTAL (2 rounds, 48 queries)
c [sort-queue-26] sorted 358 enqueued variables after 1597301 conflicts
c [score-dist-26] active 2186 (86%), one 0 (0%), zero 358 (14%)
c [score-dist-26] max exp 522, different 22 (4%)
c [score-dist-26] median active exp 515, avg 513.9
c [simplification-26] removed 141 variables 5.3% (2544 remain 1%)
c [simplification-26] removed 720 irredundant clauses 5.0% (13770 remain 1%)
c [simplification-26] maximum reduction of 5% = max (5%, 5%)
c [simplification-26] large reduction 5% >= 5% limit
c [simplification-26] next conflict interval 15973 = min (1597301/100, 599985)
c [simplification-26] penalized conflict interval 15973 = 1 * 15973
c [simplification-26] hard conflict limit 1623274 (soft 1613274 + delta 10000)
c [simplification-26] new conflict limit 1613274 (hard 1623274)
c 
c [simplification-27] limit 1613274 conflicts (hard 1623274) hit after 1623274 conflicts
c [quatres-13] found 1123 quaternary clauses 18% in total
c [quatres-13-2] added 2 single-self-subsuming ternary resolvents
c [basicprobe-9] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-9-0] 705 sched 28%, 37 failed, 0 lifted, 1373 hbrs
c [decomp-82] removed 46 variables
c [basicprobe-9-1] 682 sched 27%, 3 failed, 0 lifted, 561 hbrs
c [decomp-83] removed 4 variables
c [basicprobe-9-2] 678 sched 27%, 0 failed, 0 lifted, 41 hbrs
c [decomp-84] removed 1 variables
c [basicprobe-9-3] 678 sched 27%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-9-4] 678 sched 27%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-9-4] fully completed probing
c [basicprobe-9-4] 40 units = 40 failed (100%) + 0 lifted (0%)
c [basicprobe-9-4] removed 51 variables, found 1976 hbrs
c [bate-7] eliminated 15 asymmetric tautologies during probing
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 1061 transitive binary clauses
c [bca-23] limit of 10000000 steps and 27313 added (scaled 2)
c [bca-23] 3288 out of 4988 literals actually usable 66%
c [bca-23] added 4 blocked clauses in 79786 steps
c [sort-queue-27] sorted 334 enqueued variables after 1623274 conflicts
c [score-dist-27] active 2159 (87%), one 0 (0%), zero 334 (13%)
c [score-dist-27] max exp 522, different 22 (4%)
c [score-dist-27] median active exp 515, avg 513.9
c [simplification-27] removed 51 variables 2.0% (2493 remain 1%)
c [simplification-27] removed 415 irredundant clauses 3.0% (13355 remain 1%)
c [simplification-27] maximum reduction of 3% = max (2%, 3%)
c [simplification-27] geometric conflict interval increment 149996 = 599985 / 4
c [simplification-27] new conflict interval 749981
c [simplification-27] penalized conflict interval 749981 = 1 * 749981
c [simplification-27] hard conflict limit 2748245 (soft 2373255 + delta 374990)
c [simplification-27] new conflict limit 2373255 (hard 2748245)
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 -  345.0    2493    13355   1644833   42760    384 71602   23    29   26  82%   1024   -2   18   25   72%
c -  355.3    2493    13355   1703632   43613    385 71602   25    32   25  80%   1024    3   25   23  108%
c -  364.6    2493    13355   1761371   45178    388 71602   24    30   25  80%   1024    2   23   23  104%
c -  373.3    2493    13355   1816521   45713    394 71604   17    22   26  80%   1024   -5   16   21   77%
c i  378.6    2492    13355   1851110   74730    408 71612   18    22   37  80%   1024   -4    9   20   46%
c i  379.5    2484    13355   1858916   81881    410 71613   11    15   41  71% -16161   -9    9   19   47%
c -  382.1    2484    13355   1873263   46440    415 71613   37    52   26  70% -12889   24   44   22  202%
c -  394.5    2484    13355   1927947   46446    419 71614   32    44   39  72%  -5016    2   35   31  115%
c -  407.5    2484    13355   1983514   48219    423 71614   33    47   38  70%  -1563    1   34   33  103%
c -  420.2    2484    13355   2037813   47824    424 71614   39    51   39  77%   -106    3   40   35  113%
c -  431.4    2484    13355   2092290   49858    424 71614   44    60   41  73%    532    6   45   39  115%
c -  444.0    2484    13355   2145929   49485    425 71615   44    63   40  70%    807    6   43   42  103%
c -  459.6    2484    13355   2201675   49128    425 71615   43    56   40  76%    931   -4   40   44   91%
c -  474.8    2484    13355   2259520   50407    426 71616   45    61   41  75%    986    3   44   44  100%
c -  491.4    2484    13355   2317449   51312    427 71616   38    47   41  79%   1008   -7   37   41   89%
c -  505.1    2484    13355   2373645   52439    429 71616   32    42   41  77%   1017   -6   28   37   76%
c 
c [simplification-28] limit 2373255 conflicts (hard 2748245) hit after 2409109 conflicts
c [ternres-22] limit 97849995 with penalty 1 = 1 + 0
c [ternres-22] all 2484 free variables schedulable
c [ternres-22] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-22] fully completed ternary resolution
c [card-7] limit 6115624 penalty 4 = 4 + 0
c [card-7] found 1230 at-most-one constraints of average size 3.4
c [card-7] found 24 at-most-two constraints of average size 4.1
c [card-7] using previous limit 6115624 for elimination
c [card-7] 1253 out of 1254 constraints (100%) meet size limits
c [card-7] no units found
c [card-7] generated 2889 at-most-one constraints, 2256 used 78%
c [card-7] exported 9953 binary clauses, 4.4 per/constraint
c [decomp-86] removed 9 variables
c [simpleprobe-10] all 2484 free variables schedulable
c [simpleprobe-10] limit 200000000 penalty 0 = 0 + 0
c [decomp-87] removed 1 variables
c [simpleprobe-10] fully completed simple probing
c [simpleprobe-10] removed 1 variables, found 4872 hbrs, 0 units
c [unhide-21] limit 2500000 with penalty 3 = 3 + 0
c [unhide-21-43] 0 units, 0 failed, 28911 tauts, 0 hbrs, 258070 literals
c [transred-24] limit 2000000 with penalty 0 = 0 + 0
c [transred-24] removed 832 transitive binary clauses
c [cce-19] limit of 489249975 steps penalty 1 = 1 + 0
c [cce-19-1] eliminated 1 clauses out of 1 (100%) of length 24
c [cce-19-1] eliminated 1 clauses out of 1 (100%) of length 21
c [cce-19-1] eliminated 1 clauses out of 32 (3%) of length 7
c [cce-19-1] eliminated 11 clauses out of 670 (2%) of length 4
c [cce-19-1] completed large round (ACCE)
c [cce-19-1] eliminated 14 large clauses in 2471526 steps
c [cce-19-1] allowing another 1235763 steps for small clauses
c [cce-19-1] scheduling 10237 clauses = 7648 binary + 2589 ternary
c [cce-19-1] tried to eliminate 10237 small clauses 100%
c [cce-19-1] eliminated 159 binary clauses 2%
c [cce-19-1] eliminated 71 ternary clauses 3%
c [cce-19-1] eliminated 230 small clauses 2%
c [cce-19-1] eliminated 230 small clauses in 28956345 steps
c [cce-19-1] completed small round (ACCE)
c [cce-19-1] eliminated 244 covered clauses in round 1
c [cce-19-2] eliminated 2 clauses out of 313 (1%) of length 5
c [cce-19-2] eliminated 1 clauses out of 659 (0%) of length 4
c [cce-19-2] completed large round (ACCE)
c [cce-19-2] eliminated 3 large clauses in 2441397 steps
c [cce-19-2] allowing another 1220698 steps for small clauses
c [cce-19-2] scheduling 10007 clauses = 7489 binary + 2518 ternary
c [cce-19-2] tried to eliminate 10007 small clauses 100%
c [cce-19-2] eliminated 8 binary clauses 0%
c [cce-19-2] eliminated 10 ternary clauses 0%
c [cce-19-2] eliminated 18 small clauses 0%
c [cce-19-2] eliminated 18 small clauses in 28167464 steps
c [cce-19-2] completed small round (ACCE)
c [cce-19-2] eliminated 21 covered clauses in round 2
c [cce-19-3] eliminated 1 clauses out of 31 (3%) of length 7
c [cce-19-3] eliminated 1 clauses out of 311 (0%) of length 5
c [cce-19-3] eliminated 1 clauses out of 658 (0%) of length 4
c [cce-19-3] completed large round (ACCE)
c [cce-19-3] eliminated 3 large clauses in 2426157 steps
c [cce-19-3] allowing another 1213078 steps for small clauses
c [cce-19-3] scheduling 9989 clauses = 7481 binary + 2508 ternary
c [cce-19-3] tried to eliminate 9989 small clauses 100%
c [cce-19-3] eliminated 7 binary clauses 0%
c [cce-19-3] eliminated 1 ternary clauses 0%
c [cce-19-3] eliminated 8 small clauses 0%
c [cce-19-3] eliminated 8 small clauses in 28008160 steps
c [cce-19-3] completed small round (ACCE)
c [cce-19-3] eliminated 11 covered clauses in round 3
c [cce-19] eliminated 276 covered clauses in TOTAL during 3 rounds
c [elim-23] scheduling all variables this time
c [elim-23] scheduled 2483 variables 100%
c [elim-23] almost no limit of 100000000000 steps
c [elim-23] rescheduling of touched variables disabled
c [elim-23-1] eliminated 63 variables 3% in round 1 in 784371 steps
c [elim-23-1] backward subsumption/strengthening limit 784300
c [elim-23-1-1] backward checking 382 touched variables 15%
c [elim-23-1-1] fully completed backward checking in 1 rounds
c [elim-23-1] subsumed 0 and strengthened 2 clauses in 42027 steps
c [elim-23-1] rescheduled 13 variables 1% by backward subsumption
c [elim-23-2] no variable eliminated in round 2 in 5015 steps
c [elim-23] fully completed in 2 rounds
c [elim-23] transition to [ all 0 rem 0 ] state
c [elim-23] eliminated 63 = 3% variables out of 2483 scheduled
c [bca-24] limit of 10000000 steps and 26367 added (scaled 2)
c [bca-24] 3078 out of 4842 literals actually usable 64%
c [bca-24] added 6 blocked clauses in 85067 steps
c [sort-queue-28] sorted 286 enqueued variables after 2409109 conflicts
c [score-dist-28] active 2134 (88%), one 0 (0%), zero 286 (12%)
c [score-dist-28] max exp 522, different 22 (4%)
c [score-dist-28] median active exp 515, avg 514.6
c [simplification-28] removed 64 variables 2.6% (2420 remain 1%)
c [simplification-28] removed 474 irredundant clauses 3.5% (12881 remain 1%)
c [simplification-28] maximum reduction of 4% = max (3%, 4%)
c [simplification-28] geometric conflict interval increment 149996 = 749981 / 5
c [simplification-28] new conflict interval 899977
c [simplification-28] penalized conflict interval 899977 = 1 * 899977
c [simplification-28] hard conflict limit 3759074 (soft 3309086 + delta 449988)
c [simplification-28] new conflict limit 3309086 (hard 3759074)
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 -  522.9    2420    12881   2435673   50899    419 52923   41    52   29  79%   1021    5   43   37  115%
c -  534.8    2420    12881   2492869   51274    419 52923   41    54   29  76%   1023    2   46   40  114%
c -  546.5    2420    12881   2550573   50196    419 52923   47    61   29  77%   1024    4   45   44  104%
c -  560.3    2420    12881   2610904   50178    419 52923   42    54   39  77%   1024   -4   43   45   97%
c -  576.4    2420    12881   2672753   51690    420 52924   39    47   40  83%   1024   -5   44   42  105%
c -  592.4    2420    12881   2734497   53037    420 52924   33    43   39  78%   1024   -5   38   38   99%
c -  605.7    2420    12881   2795417   54543    422 52924   50    66   40  76%   1024   10   51   43  117%
c -  619.1    2420    12881   2856085   54525    422 52924   43    53   40  82%   1024   -4   44   44  100%
c -  636.4    2420    12881   2919429   53597    422 52924   40    45   39  87%   1024   -7   40   42   95%
c -  649.8    2420    12881   2984088   54817    422 52924   35    43   39  82%   1024   -5   36   38   95%
c -  663.0    2420    12881   3048939   55927    422 52924   37    44   39  83%   1024   -3   35   38   93%
c -  678.7    2420    12881   3115894   56306    423 52924   35    43   40  82%   1024   -0   36   35  101%
c -  692.3    2420    12881   3183656   55875    425 52924   27    37   38  73%   1024   -4   28   31   91%
c -  702.6    2420    12881   3250570   57581    427 52925   33    45   37  74%   1024    6   33   30  111%
c -  715.6    2420    12881   3317881   56351    427 52925   27    37   37  74%   1024   -0   29   28  104%
c 
c [simplification-29] limit 3309086 conflicts (hard 3759074) hit after 3318190 conflicts
c [quatres-14] found 1138 quaternary clauses 17% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [ternres-23] limit 200000000 with penalty 0 = 0 + 0
c [ternres-23] all 2420 free variables schedulable
c [ternres-23] 7 ternary resolvents (0 bin, 7 trn)
c [ternres-23] fully completed ternary resolution
c [treelook-10] limit 28730050 penalty 0 = 0 + 0 boost 1
c [treelook-10] scheduled 4830 literals 100%
c [treelook-10] scheduling used 272416 steps
c [treelook-10] scheduled completely
c [treelook-10] limit 28730050 penalty 0 = 0 + 0 boost 1
c [treelook-10] used 10772169 steps
c [treelook-10] fully completed tree based probing
c [decomp-89] removed 2 variables
c [treelook-10] removed 5 variables, found 16715 hbrs
c [transred-25] limit 2000000 with penalty 0 = 0 + 0
c [transred-25] removed 1147 transitive binary clauses
c [cce-20] limit of 1436502521 steps penalty 0 = 0 + 0
c [cce-20-1] eliminated 1 clauses out of 2 (50%) of length 19
c [cce-20-1] eliminated 1 clauses out of 1 (100%) of length 17
c [cce-20-1] eliminated 2 clauses out of 6 (33%) of length 13
c [cce-20-1] eliminated 1 clauses out of 20 (5%) of length 8
c [cce-20-1] eliminated 1 clauses out of 315 (0%) of length 5
c [cce-20-1] completed large round (ATE)
c [cce-20-1] eliminated 6 large clauses in 2490761 steps
c [cce-20-1] allowing another 1245380 steps for small clauses
c [cce-20-1] scheduling 9850 clauses = 7351 binary + 2499 ternary
c [cce-20-1] tried to eliminate 9850 small clauses 100%
c [cce-20-1] eliminated 51 binary clauses 1%
c [cce-20-1] eliminated 6 ternary clauses 0%
c [cce-20-1] eliminated 57 small clauses 1%
c [cce-20-1] eliminated 57 small clauses in 27096049 steps
c [cce-20-1] completed small round (ATE)
c [cce-20-1] eliminated 63 covered clauses in round 1
c [cce-20-2] completed large round (ATE)
c [cce-20-2] allowing another 1229443 steps for small clauses
c [cce-20-2] scheduling 9793 clauses = 7300 binary + 2493 ternary
c [cce-20-2] tried to eliminate 9793 small clauses 100%
c [cce-20-2] completed small round (ATE)
c [cce-20-2] eliminated 0 covered clauses in round 2
c [cce-20] eliminated 63 covered clauses in TOTAL during 2 rounds
c [cce-20] 63 < 1/100 * 12859 = 128 considered unsuccessful
c [elim-24] scheduling all variables this time
c [elim-24] scheduled 2415 variables 100%
c [elim-24] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-24] rescheduling of touched variables disabled
c [elim-24-1] eliminated 4 variables 0% in round 1 in 770642 steps
c [elim-24-1] backward subsumption/strengthening limit 770600
c [elim-24-1-1] backward checking 61 touched variables 3%
c [elim-24-1-1] fully completed backward checking in 1 rounds
c [elim-24-1] subsumed 0 and strengthened 1 clauses in 8507 steps
c [elim-24-1] rescheduled 20 variables 1% by backward subsumption
c [elim-24-2] no variable eliminated in round 2 in 7393 steps
c [elim-24] fully completed in 2 rounds
c [elim-24] transition to [ all 0 rem 0 ] state
c [elim-24] eliminated 4 = 0% variables out of 2415 scheduled
c [elim-24] 4 < 1/100 * 2415 = 24 considered unsuccessful
c [bca-25] limit of 10000000 steps and 26186 added (scaled 2)
c [bca-25] 3046 out of 4824 literals actually usable 63%
c [bca-25] added 1 blocked clauses in 63613 steps
c [sort-queue-29] sorted 268 enqueued variables after 3318190 conflicts
c [score-dist-29] active 2143 (89%), one 0 (0%), zero 268 (11%)
c [score-dist-29] max exp 523, different 23 (4%)
c [score-dist-29] median active exp 516, avg 515.0
c [simplification-29] removed 9 variables 0.4% (2411 remain 1%)
c [simplification-29] removed 92 irredundant clauses 0.7% (12789 remain 1%)
c [simplification-29] maximum reduction of 1% = max (0%, 1%)
c [simplification-29] geometric conflict interval increment 449988 = 899977 / 2
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 4818190 (soft 4318190 + delta 500000)
c [simplification-29] new conflict limit 4318190 (hard 4818190)
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 -  730.4    2411    12789   3386790   56276    438 67416   25    31   25  78%   1024   -5   23   28   82%
c -  742.8    2411    12789   3460057   57629    440 67416   25    31   26  79%   1024   -2   28   26  109%
c -  758.4    2411    12789   3533378   59392    441 67416   30    40   37  75%   1024    2   30   30  101%
c -  774.5    2411    12789   3607135   60366    441 67416   30    37   38  81%   1024    0   30   30  102%
c -  789.6    2411    12789   3676384   59765    441 67416   32    41   38  78%   1024    2   28   32   88%
c -  804.4    2411    12789   3748366   60447    441 67416   22    31   38  72%   1024   -5   22   28   78%
c -  819.6    2411    12789   3821899   59709    441 67416   29    34   38  87%   1024   -2   29   29  101%
c -  834.3    2411    12789   3900762   62288    442 67416   28    34   37  81%   1024   -1   28   29   94%
c -  850.3    2411    12789   3977114   63065    442 67416   30    34   37  88%   1024   -2   29   30   95%
c -  866.1    2411    12789   4053479   63505    443 67416   43    52   37  83%   1024   10   39   35  111%
c -  882.7    2411    12789   4130234   62203    443 67416   31    43   37  72%   1024    3   35   34  103%
c -  899.1    2411    12789   4207876   62942    443 67416   39    46   38  85%   1024    2   42   36  117%
c -  914.2    2411    12789   4288095   63502    443 67416   32    38   37  85%   1024   -2   34   34  101%
c 
c [simplification-30] limit 4318190 conflicts (hard 4818190) hit after 4318191 conflicts
c [ternres-24] limit 200000000 with penalty 0 = 0 + 0
c [ternres-24] all 2411 free variables schedulable
c [ternres-24] 12 ternary resolvents (0 bin, 12 trn)
c [ternres-24] fully completed ternary resolution
c [basicprobe-10] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-10-0] 663 sched 28%, 10 failed, 0 lifted, 496 hbrs
c [decomp-91] removed 10 variables
c [basicprobe-10-1] 669 sched 28%, 0 failed, 0 lifted, 105 hbrs
c [basicprobe-10-2] 669 sched 28%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-10-3] 669 sched 28%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-10-4] 669 sched 28%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-10-5] 669 sched 28%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-10-5] fully completed probing
c [basicprobe-10-5] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-10-5] removed 10 variables, found 604 hbrs
c [bate-8] eliminated 8 asymmetric tautologies during probing
c [transred-26] limit 2000000 with penalty 0 = 0 + 0
c [transred-26] removed 790 transitive binary clauses
c [bca-26] limit of 10000000 steps and 26031 added (scaled 2)
c [bca-26] 3111 out of 4804 literals actually usable 65%
c [bca-26] added 5 blocked clauses in 97392 steps
c [sort-queue-30] sorted 248 enqueued variables after 4318191 conflicts
c [score-dist-30] active 2153 (90%), one 0 (0%), zero 248 (10%)
c [score-dist-30] max exp 523, different 23 (4%)
c [score-dist-30] median active exp 516, avg 515.2
c [simplification-30] removed 10 variables 0.4% (2401 remain 1%)
c [simplification-30] removed 78 irredundant clauses 0.6% (12711 remain 1%)
c [simplification-30] maximum reduction of 1% = max (0%, 1%)
c [simplification-30] geometric conflict interval increment 500000 = 1000000 / 2
c [simplification-30] conflict interval soft limit 1000000 reached
c [simplification-30] new conflict interval 1000000
c [simplification-30] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-30] hard conflict limit 5818191 (soft 5318191 + delta 500000)
c [simplification-30] new conflict limit 5318191 (hard 5818191)
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 -  933.5    2401    12711   4368005   64166    440 65065   30    36   31  84%   1024   -3   34   33  105%
c -  949.0    2401    12711   4447229   65778    440 65065   35    42   33  83%   1024    3   35   33  107%
c -  964.9    2401    12711   4528305   66143    440 65065   26    36   32  72%   1024   -1   24   29   82%
c -  984.9    2401    12711   4614664   66639    440 65065   23    32   46  73%   1024   -7   22   29   76%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 293 basic ate = 271 trn 92% + 22 lrg 8% in 8 updates
c bcas: 26 count, 223 added (59 skipped), 1073287 steps
c bkwd: tried 194162 clauses, 387780 lits, 2.00 lits/clause
c bkwd: checked 4065317 occs, 20.94 occs/clause, 10.48 occs/lit
c bkwd: subsumed 51 binary, 221 ternary, 136 large
c bkwd: strengthened 15 binary, 0 ternary (0% self), 622 large (0% self)
c blkd: 6 bces, 625 removed, 665889 resolutions, 1819239 steps
c blkd: 1794 blocking literals 0%, 8 pure
c bump: 4691605 bumped seen, 655132081 lits 139.6 on average
c card: 7 count, 0 units, 9953 am1, 37678651 steps
c card: 57 rescheduled, 544 eliminated, 26962 resolved, 62059 subsumed
c card: 18245 at-most-one constraints found, average size 4.25
c card: 18245 at-most-one constraints used 100%, average size 4.25
c card: 24 at-most-two constraints found, average size 4.12
c card: 23 at-most-two constraints used 96%, average size 4.13
c cces: 20 cces, 22203 eliminated, 21018 ate 95%, 1185 abce 5%
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: 214 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 95 decompositions, 65957 equivalent 29%
c deco: 16 decision-only clauses 0%, 61% reduction
c decs: 7661965 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 24 elims, 22933 eliminated 10%, 117 pure 1%
c elms: 66 rounds, 2.8 rounds/bve
c elms: 21899 small 95%, 909 large 4%
c elms: 64607 tried small, 21901 succeeded 34%, 42706 failed 66%
c elms: 5757 subsumed, 9704 strengthened, 317 blocked
c elms: 3970638 copies, 3631094 resolutions, 1902633 ipos
c elms: 802599 subchks, 518856 strchks
c gaus: 7 extractions, 312 extracted, 2.7 size, 3 max
c gaus: exported 0 units, 2 binary and 0 ternary equations
c gaus: 0 gc, 12931386 steps, 6465693 extr 50%, 5973 elim 0%
c glue: 31.1 orig avg, 31.1 real avg, 5.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 300121 = 43888 simple 15% + 186594 trn 62% + 69639 lrg 23%, 1456 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 4691605 clauses, 62.4 length
c lrnd: 292740765 lits = 444313546 orig - 151572781 removed 34%
c lrnd: 1786924 uips 38%, 2622142 flips 56%
c mins: 4688680 mins 100%, 108 bin 0%, 2801 size 0%
c mins: 504408635 poisoned searches, 89312130 hits, 18% hit rate
c mins: 854691435 used twice searches, 101254184 hits, 12% hit rate
c move: moved 20191, 16007 bin 79%, 4184 trn 21%
c otfs: 2639 driving 25%, 7865 restarting 75%
c otfs: str 10504, 10466 red 100%, 38 irr 0%
c otfs: str 10504, 0 bin 0%, 18 trn 0%, 10486 lrg 100%
c otfs: sub 24, 24 red 100%, 0 irr 0%
c otfs: sub 24, 0 bin 0%, 1 trn 4%, 23 lrg 96%
c phas: 8 computed, 25552 set, 0 pos (0%), 25552 neg (100%)
c prbs: 10 basic, 42791 probed, 1496 failed, 133 lifted
c prbs: 10 simple, 392301 probed, 2024 failed, 30265 eqs
c prbs: 10 treelook, 7118 probed, 99 failed, 0 lifted
c prom: 199040 locked 4% out of 5406826 tried
c prps: 1408252853 props, 181 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 14 count, 20 quat, 4 self1, 0 self2, 10 dup
c queu: 30 sorted, 7661965 next (181772 steps 0.02)
c queu: 655441249 enq (865363682 steps 1.32), 655132081 deq 100%
c redc: 2388 clauses 5%, 48293 tried 1%, 5 sat 0%
c redc: 5269 lits 1%, 476514 tried 0%, 5 sat 0%
c redc: 156 times jump level reduced, 7.2 levels on average
c reds: 80 count, 58659.0 conflicts per reduce
c reds: 0 memlim 0%, 80 arith 100%
c reds: 3580225 collected 92%, 302746 retired 8%
c rmbd: 3869 removed, 1317 red 34%
c rsts: 17873 restarts 99%, 128 skipped 1%
c rsts: 128 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 30 count, 30 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 4691605 count (3801414 tried 0.8), 619748 sub out of 4690848 (13.2%)
c swps: 15 count, 19 rounds, 2367 queries (124.6/round)
c swps: 2285 sat calls, 50 unsat (0.7% success rate)
c swps: 18112 decisions 7.9, 1526 conflicts 0.7
c swps; 72.6 avg class size, 34.9 avg environment size
c swps: 0 failed, 163 impls, 115 equivs
c swp0: 783 type 0 queries, 322 unsat (41.1%), 757 sat (96.7%)
c swp1: 1584 type 1 queries, 836 unsat (52.8%), 1495 sat (94.4%)
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: 24707795 calls to obtain time
c tops: 138253 fixed 60%, 24 its, 195529.92 confs/it
c trds: 26 transitive reductions, 15888 removed, 125 failed
c trds: 82690 nodes, 214852 edges, 50515375 steps
c trim: 7333302 words, 28.0 MB
c trnr: 24 count, 2 bin, 829 trn, 25923497 steps
c unhd: 21 count, 43 rounds, 18394140 steps
c unhd: 1807 non-trivial sccs of average size 2.2
c unhd: 62 units, 60 bin, 2 trn, 0 lrg
c unhd: 2671 failed, 2655 stamp, 0 lits, 10 bin, 2 trn, 0 lrg
c unhd: 103589 tauts, 7369 bin 7%, 1202 trn 1%, 217 lrg 0%
c unhd: 103589 tauts, 94801 stamp 92%, 76898 red 74%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 493438 str, 60 bin 0%, 1508 trn 0%, 491870 lrg 100%, 488881 red 99%
c vars: 2401 remaining 1% and 227143 removed 99% out of 229544
c vars: 138253 fixed 60%, 22933 eliminated 10%, 65957 equivalent 29%
c vsts: 43909419765 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 31.5 search visits per propagation, 9309.0 per conflict
c wchs: 9607372788 pushed, 18188433 enlarged, 339 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        4690868       3580225        302746     120967389      42208433       1877374
c 
c  0 0         12551   0      1263   0         0   0  34743341  29   7687386  18    207816  11     0.4
c  1 5         16909   0      6291   0      8526   3  10774860   9   3464382   8     76560   4     0.2
c  2 6        103704   2     65316   2     29020  10  22693295  19<  7761777  18    248743  13     1.3
c  3 9        332039   7    247011   7     51099  17  19143052  16   7178076  17<   309221  16     2.8
c  4 14       523450  11    366925  10     55774  18< 14381052  12   5902978  14    327895  17<    9.0
c  5 21      1123966  24<   833631  23     78040  26  10295923   9   5132342  12    388589  21    14.1
c  6 30      1517685  32   1201200  34<    57623  19   6538001   5   3548091   8    243373  13    14.5
c  7 41       868152  19    703445  20     19497   6   2031256   2   1286775   3     62727   3    11.8
c  8 54       183718   4    148429   4      3047   1    342720   0    231885   1     11206   1     6.4
c  9 69         8592   0      6713   0       119   0     13710   0      9753   0       554   0     0.6
c 10 86          102   0         1   0         1   0     10179   0      4988   0       690   0     0.0
c 
c avg                  5.5           5.6           4.4           2.3           2.9           3.6
c std                  1.4           1.3           1.5           2.0           2.0           2.0
c 
c   82.006   8% bump
c   26.990   3% cce
c   12.368   1% probe
c    6.854   1% unhide
c    4.719   0% decide
c 
c   10.540 < 1% rest (below)
c 
c    3.720   0% elim
c    2.943   0% transred
c    1.973   0% sweep
c    0.776   0% bca
c    0.364   0% card
c    0.306   0% gauss
c    0.255   0% block
c    0.165   0% ternres
c    0.038   0% quatres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    2.350   0% preprocessing     4%
c   57.045   6% inprocessing     96%
c ==================================
c   59.396   6% simplifying
c  940.112  94% search
c ==================================
c  999.511 100% all
c 
c       4692718 conflicts,        4695.0 confs/sec
c           264 ternaries,       17775.4 confs/ternary
c           117 binaries,        40108.7 confs/binary
c            24 iterations,     195529.9 confs/iteration
c 
c            80 reductions,          0.1 redus/sec,  58659.0 confs/reduction
c         17873 restarts,           17.9 rests/sec,    262.6 confs/restart
c       7661965 decisions,        7665.7 decis/sec,      1.6 decis/conflict
c    1408252853 propagations,  1408941.4 props/sec,    183.8 props/decision
c 
c 999.5 seconds, 86.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
