c launch: /data/cnf/sc2014/app/dated-10-13-u.cnf.bz2
c host: atom01
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/dated-10-13-u.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/dated-10-13-u.cnf.bz2
c no embedded options
c found 'p cnf 180608 815261' header
c read 180608 variables, 815261 clauses, 1862226 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 172976 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  172976   800029         0       0      0     0    0     0   35   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 10630 at-most-one constraints of average size 5.2
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 10630 out of 10630 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 87203 variables
c [simpleprobe-1] all 93405 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 61509 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 61509 variables, found 8077 hbrs, 953 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 598 failed, 5905 tauts, 0 hbrs, 271 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 31023 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 11526 variables 37% in round 1 in 12273088 steps
c [elim-1-1] backward subsumption/strengthening limit 7726912
c [elim-1-1-1] backward checking 20321 touched variables 66%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 65 and strengthened 198 clauses in 2428622 steps
c [elim-1-1] rescheduled 489 variables 2% by backward subsumption
c [elim-1-2] eliminated 114 variables 0% in round 2 in 260506 steps
c [elim-1-2] backward subsumption/strengthening limit 260500
c [elim-1-2-1] backward checking 515 touched variables 2%
c [elim-1-2-1] incomplete backward checking 0 remain 0%
c [elim-1-2] subsumed 62 and strengthened 49 clauses in 260501 steps
c [elim-1-2] rescheduled 191 variables 1% by backward subsumption
c [elim-1-3] eliminated 51 variables 0% in round 3 in 105347 steps
c [elim-1-3] backward subsumption/strengthening limit 105300
c [elim-1-3-1] backward checking 220 touched variables 1%
c [elim-1-3-1] incomplete backward checking 0 remain 0%
c [elim-1-3] subsumed 48 and strengthened 31 clauses in 105301 steps
c [elim-1] incomplete 132 not tried 0% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 11798 = 38% variables out of 31023 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 139013 negative 99.0% of 140400 except 1387 1.0%
c [phase-count-1] 117578 positive 83.7% of 140400 except 22822 16.3%
c [phase-count-1] less non-negative clauses 1387 than limit 14000 (10.0%)
c [phase-count-1] non-pos/non-neg = 22822/1387 = 16.45 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 19225 negative 100%
c [sort-queue-1] sorted 19225 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 19225 (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 118677 variables 86.1% (19225 remain 11%)
c [simplification-1] removed 659629 irredundant clauses 82.5% (140400 remain 18%)
c [simplification-1] maximum reduction of 86% = max (86%, 82%)
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    1.8   19224   140400       140     119      6  6254    0     2   14  15%      0    2    5    0 21224%
c i    1.8   19223   140400       141     119      6  6254    0     2   14  15%      0    2    5    0 21142%
c i    1.9   19222   140400       396     318      8  6257    4     9   14  42%      1    9   41    0 17352%
c i    2.0   19218   140400       616     488      8  6257    9    17   14  53%      1   17   81    1 13513%
c 
c [simplification-2] limit 1010 conflicts (hard 11000) hit after 1010 conflicts
c [decomp-3] removed 31 variables
c [simpleprobe-2] all 19194 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 966 variables
c [simpleprobe-2] 7628 variables remain 42% (10600 retained 58%)
c [simpleprobe-2] removed 966 variables, found 1920 hbrs, 357 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 32153 literals 88%
c [treelook-1] scheduling used 300002 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 360554 steps
c [treelook-1] 32137 literals remain 88%
c [treelook-1] 18215 variables remain to probed next time 100%
c [decomp-5] removed 6 variables
c [treelook-1] removed 12 variables, found 3133 hbrs
c [basicprobe-1] limit 1150235 penalty 0 = 0 + 0
c [basicprobe-1-0] 2729 probes remain 15% after last round
c [basicprobe-1-0] 12 units = 12 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 25 variables, found 5326 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 323 failed, 3255 tauts, 0 hbrs, 2515 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 17955 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 641 variables 4% in round 1 in 9883755 steps
c [elim-2-1] backward subsumption/strengthening limit 9883700
c [elim-2-1-1] backward checking 3161 touched variables 18%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 50 and strengthened 42 clauses in 634289 steps
c [elim-2-1] rescheduled 203 variables 1% by backward subsumption
c [elim-2-2] eliminated 38 variables 0% in round 2 in 126523 steps
c [elim-2-2] backward subsumption/strengthening limit 126500
c [elim-2-2-1] backward checking 162 touched variables 1%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 20 and strengthened 1 clauses in 56429 steps
c [elim-2-2] rescheduled 46 variables 0% by backward subsumption
c [elim-2-3] eliminated 19 variables 0% in round 3 in 24586 steps
c [elim-2-3] backward subsumption/strengthening limit 24500
c [elim-2-3-1] backward checking 78 touched variables 0%
c [elim-2-3-1] incomplete backward checking 0 remain 0%
c [elim-2-3] subsumed 9 and strengthened 1 clauses in 24501 steps
c [elim-2] incomplete 22 not tried 0% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 749 = 4% variables out of 17955 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 124257 negative 99.0% of 125504 except 1247 1.0%
c [phase-count-2] 103064 positive 82.1% of 125504 except 22440 17.9%
c [phase-count-2] less non-negative clauses 1247 than limit 12500 (10.0%)
c [phase-count-2] non-pos/non-neg = 22440/1247 = 18.00 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 725 negative 100%
c [sort-queue-2] sorted 11719 enqueued variables after 1010 conflicts
c [score-dist-2] active 5487 (32%), one 0 (0%), zero 11719 (68%)
c [score-dist-2] max exp 511, different 11 (2%)
c [score-dist-2] median active exp 505, avg 505.2
c [simplification-2] removed 2009 variables 10.5% (17206 remain 10%)
c [simplification-2] removed 14896 irredundant clauses 10.6% (125504 remain 16%)
c [simplification-2] maximum reduction of 11% = max (10%, 11%)
c [simplification-2] large reduction 11% >= 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 13010 (soft 3010 + delta 10000)
c [simplification-2] new conflict limit 3010 (hard 13010)
c 
c [simplification-3] limit 3010 conflicts (hard 13010) hit after 3010 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 5317 at-most-one constraints of average size 3.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 5317 out of 5317 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 21 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 30788 literals 90%
c [treelook-2] scheduling used 300002 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 318617 steps
c [treelook-2] 30741 literals remain 89%
c [treelook-2] 17155 variables remain to probed next time 100%
c [decomp-7] removed 13 variables
c [treelook-2] removed 24 variables, found 2003 hbrs
c [unhide-3] limit 136889 with penalty 0 = 0 + 0
c [unhide-3-3] 3 units, 90 failed, 5728 tauts, 0 hbrs, 3092 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 17061 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 434 variables 3% in round 1 in 9145431 steps
c [elim-3-1] backward subsumption/strengthening limit 9145400
c [elim-3-1-1] backward checking 2218 touched variables 13%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 48 and strengthened 25 clauses in 418307 steps
c [elim-3-1] rescheduled 126 variables 1% by backward subsumption
c [elim-3-2] eliminated 40 variables 0% in round 2 in 62951 steps
c [elim-3-2] backward subsumption/strengthening limit 62900
c [elim-3-2-1] backward checking 142 touched variables 1%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 23 and strengthened 5 clauses in 46373 steps
c [elim-3-2] rescheduled 57 variables 0% by backward subsumption
c [elim-3-3] eliminated 17 variables 0% in round 3 in 27937 steps
c [elim-3-3] backward subsumption/strengthening limit 27900
c [elim-3-3-1] backward checking 66 touched variables 0%
c [elim-3-3-1] incomplete backward checking 0 remain 0%
c [elim-3-3] subsumed 8 and strengthened 2 clauses in 27901 steps
c [elim-3] incomplete 15 not tried 0% in round 3
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 536 = 3% variables out of 17061 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 116200 negative 99.0% of 117371 except 1171 1.0%
c [phase-count-3] 97276 positive 82.9% of 117371 except 20095 17.1%
c [phase-count-3] less non-negative clauses 1171 than limit 11700 (10.0%)
c [phase-count-3] non-pos/non-neg = 20095/1171 = 17.16 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 511 negative 100%
c [sort-queue-3] sorted 9814 enqueued variables after 3010 conflicts
c [score-dist-3] active 6711 (41%), one 0 (0%), zero 9814 (59%)
c [score-dist-3] max exp 513, different 13 (3%)
c [score-dist-3] median active exp 507, avg 506.5
c [simplification-3] removed 681 variables 4.0% (16525 remain 10%)
c [simplification-3] removed 8133 irredundant clauses 6.5% (117371 remain 15%)
c [simplification-3] maximum reduction of 6% = max (4%, 6%)
c [simplification-3] large reduction 6% >= 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 15010 (soft 5010 + delta 10000)
c [simplification-3] new conflict limit 5010 (hard 15010)
c 
c [simplification-4] limit 5010 conflicts (hard 15010) hit after 5013 conflicts
c [decomp-8] removed 13 variables
c [basicprobe-2] limit 5438981 penalty 0 = 0 + 0
c [basicprobe-2-0] 2440 probes remain 15% after last round
c [basicprobe-2-0] 77 units = 74 failed (96%) + 3 lifted (4%)
c [basicprobe-2-0] removed 145 variables, found 20680 hbrs
c [unhide-4] limit 217559 with penalty 0 = 0 + 0
c [unhide-4-4] 2 units, 103 failed, 2401 tauts, 0 hbrs, 2901 literals
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 16242 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 435118520 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 294 variables 2% in round 1 in 8652492 steps
c [elim-4-1] backward subsumption/strengthening limit 8652400
c [elim-4-1-1] backward checking 1360 touched variables 8%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 42 and strengthened 20 clauses in 261738 steps
c [elim-4-1] rescheduled 104 variables 1% by backward subsumption
c [elim-4-2] eliminated 15 variables 0% in round 2 in 62337 steps
c [elim-4-2] backward subsumption/strengthening limit 62300
c [elim-4-2-1] backward checking 63 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 11 and strengthened 5 clauses in 29140 steps
c [elim-4-2] rescheduled 35 variables 0% by backward subsumption
c [elim-4-3] eliminated 12 variables 0% in round 3 in 17885 steps
c [elim-4-3] backward subsumption/strengthening limit 17800
c [elim-4-3-1] backward checking 55 touched variables 0%
c [elim-4-3-1] incomplete backward checking 0 remain 0%
c [elim-4-3] subsumed 12 and strengthened 5 clauses in 17801 steps
c [elim-4] incomplete 41 not tried 0% in round 3
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 351 = 2% variables out of 16242 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 112195 negative 99.0% of 113292 except 1097 1.0%
c [phase-count-4] 93450 positive 82.5% of 113292 except 19842 17.5%
c [phase-count-4] less non-negative clauses 1097 than limit 11300 (10.0%)
c [phase-count-4] non-pos/non-neg = 19842/1097 = 18.09 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 321 negative 100%
c [sort-queue-4] sorted 8992 enqueued variables after 5013 conflicts
c [score-dist-4] active 6899 (43%), one 0 (0%), zero 8992 (57%)
c [score-dist-4] max exp 513, different 13 (3%)
c [score-dist-4] median active exp 507, avg 506.9
c [simplification-4] removed 634 variables 3.8% (15891 remain 9%)
c [simplification-4] removed 4079 irredundant clauses 3.5% (113292 remain 14%)
c [simplification-4] maximum reduction of 4% = max (4%, 3%)
c [simplification-4] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-4] new conflict interval 4000
c [simplification-4] penalized conflict interval 4000 = 1 * 4000
c [simplification-4] hard conflict limit 19013 (soft 9013 + delta 10000)
c [simplification-4] new conflict limit 9013 (hard 19013)
c 
c [simplification-5] limit 9013 conflicts (hard 19013) hit after 9013 conflicts
c [quatres-1] found 8018 quaternary clauses 75% in total
c [quatres-1-2] added 18 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 15891 free variables schedulable
c [ternres-1] 289 ternary resolvents (0 bin, 289 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 208 xors of average arity 2.8
c [gauss-1] connected 579 occurrences of 289 variables (average 2.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 16 variables
c [simpleprobe-3] 6446 schedulable variables 41%
c [simpleprobe-3] limit 7508710 penalty 0 = 0 + 0
c [decomp-10] removed 238 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 238 variables, found 7125 hbrs, 87 units
c [unhide-5] limit 375435 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 67 failed, 3218 tauts, 0 hbrs, 4933 literals
c [transred-1] limit 1877177 with penalty 0 = 0 + 0
c [transred-1] removed 468 transitive binary clauses
c [transred-1] found 17 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 15579 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 681 blocked clauses
c [block-1] 681 < 1/100 * 109829 = 1098 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3 clauses out of 5 (60%) of length 8
c [cce-1-1] eliminated 1 clauses out of 51 (2%) of length 7
c [cce-1-1] eliminated 64 clauses out of 644 (10%) of length 6
c [cce-1-1] eliminated 251 clauses out of 1489 (17%) of length 5
c [cce-1-1] eliminated 2394 clauses out of 7045 (34%) of length 4
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 2713 large clauses in 30000010 steps
c [cce-1-1] allowing another 15000005 steps for small clauses
c [cce-1-1] scheduling 76256 clauses = 57308 binary + 18948 ternary
c [cce-1-1] tried to eliminate 1017 small clauses 1%
c [cce-1-1] eliminated 266 binary clauses 0%
c [cce-1-1] eliminated 58 ternary clauses 0%
c [cce-1-1] eliminated 324 small clauses 0%
c [cce-1-1] eliminated 324 small clauses in 30000008 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3037 covered clauses in round 1
c [cce-1] eliminated 3037 covered clauses in TOTAL during 1 rounds
c [elim-5] no untried remaining variables left
c [elim-5] scheduled 15577 variables 100%
c [elim-5] limit of 37543553 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 924 variables 6% in round 1 in 7654988 steps
c [elim-5-1] backward subsumption/strengthening limit 7654900
c [elim-5-1-1] backward checking 3005 touched variables 19%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 31 and strengthened 41 clauses in 503686 steps
c [elim-5-1] rescheduled 164 variables 1% by backward subsumption
c [elim-5-2] eliminated 17 variables 0% in round 2 in 76879 steps
c [elim-5-2] backward subsumption/strengthening limit 76800
c [elim-5-2-1] backward checking 118 touched variables 1%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 7 and strengthened 5 clauses in 34820 steps
c [elim-5-2] rescheduled 28 variables 0% by backward subsumption
c [elim-5-3] eliminated 10 variables 0% in round 3 in 11325 steps
c [elim-5-3] backward subsumption/strengthening limit 11300
c [elim-5-3-1] backward checking 38 touched variables 0%
c [elim-5-3-1] incomplete backward checking 0 remain 0%
c [elim-5-3] subsumed 5 and strengthened 2 clauses in 11301 steps
c [elim-5] incomplete 13 not tried 0% in round 3
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 953 = 6% variables out of 15577 scheduled
c [bca-1] limit of 10000000 steps and 206886 added (scaled 2)
c [bca-1] 26798 out of 29250 literals actually usable 92%
c [bca-1] added 14 blocked clauses in 59713 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2355 pos 16.1% + 12269 neg 83.9% = 14624 sched 100.0% ret 0
c [sweep-1-1] 1012047 steps 22 queries 2275.55 avg class size
c [sweep-1-1] 227 decisions 18 SAT calls 104.28 avg env size
c [sweep-1-1] 14359 variables remain 98% (255 retained 2%)
c [decomp-11] removed 18 variables
c [sweep-1-1] removed 18 vars (0 failed, 3 eqs, 6 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 18 vars in TOTAL (1 rounds, 21 queries)
c [phase-count-5] 102360 negative 99.3% of 103084 except 724 0.7%
c [phase-count-5] 84747 positive 82.2% of 103084 except 18337 17.8%
c [phase-count-5] less non-negative clauses 724 than limit 10300 (10.0%)
c [phase-count-5] non-pos/non-neg = 18337/724 = 25.33 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 149 negative 100%
c [sort-queue-5] sorted 7596 enqueued variables after 9013 conflicts
c [score-dist-5] active 7010 (48%), one 0 (0%), zero 7596 (52%)
c [score-dist-5] max exp 514, different 14 (3%)
c [score-dist-5] median active exp 508, avg 507.3
c [simplification-5] removed 1285 variables 8.1% (14606 remain 8%)
c [simplification-5] removed 10208 irredundant clauses 9.0% (103084 remain 13%)
c [simplification-5] maximum reduction of 9% = max (8%, 9%)
c [simplification-5] large reduction 9% >= 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 21013 (soft 11013 + delta 10000)
c [simplification-5] new conflict limit 11013 (hard 21013)
c 
c [simplification-6] limit 11013 conflicts (hard 21013) hit after 11013 conflicts
c [quatres-2] found 4740 quaternary clauses 68% in total
c [quatres-2-2] added 2 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 14606 free variables schedulable
c [ternres-2] 112 ternary resolvents (0 bin, 112 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2284 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] 2284 out of 2284 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 27021 literals 92%
c [treelook-3] scheduling used 300005 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 341544 steps
c [treelook-3] 27013 literals remain 92%
c [treelook-3] 14594 variables remain to probed next time 100%
c [treelook-3] removed 0 variables, found 1236 hbrs
c [unhide-6] limit 442001 with penalty 0 = 0 + 0
c [unhide-6-6] 3 units, 212 failed, 3147 tauts, 0 hbrs, 2393 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 407 transitive binary clauses
c [transred-2] found 4 units
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 2 clauses out of 596 (0%) of length 6
c [cce-2-1] eliminated 57 clauses out of 1382 (4%) of length 5
c [cce-2-1] eliminated 689 clauses out of 4658 (15%) of length 4
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 748 large clauses in 30000005 steps
c [cce-2-1] allowing another 15000002 steps for small clauses
c [cce-2-1] scheduling 77362 clauses = 55089 binary + 22273 ternary
c [cce-2-1] tried to eliminate 983 small clauses 1%
c [cce-2-1] eliminated 247 binary clauses 0%
c [cce-2-1] eliminated 58 ternary clauses 0%
c [cce-2-1] eliminated 305 small clauses 0%
c [cce-2-1] eliminated 840 small clauses in 30000003 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1588 covered clauses in round 1
c [cce-2] eliminated 1588 covered clauses in TOTAL during 1 rounds
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 14546 variables 100%
c [elim-6] limit of 44200189 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 220 variables 2% in round 1 in 7285521 steps
c [elim-6-1] backward subsumption/strengthening limit 7285500
c [elim-6-1-1] backward checking 1102 touched variables 8%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 7 and strengthened 13 clauses in 180419 steps
c [elim-6-1] rescheduled 48 variables 0% by backward subsumption
c [elim-6-2] eliminated 11 variables 0% in round 2 in 19605 steps
c [elim-6-2] backward subsumption/strengthening limit 19600
c [elim-6-2-1] backward checking 63 touched variables 0%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 2 and strengthened 0 clauses in 18949 steps
c [elim-6-2] rescheduled 6 variables 0% by backward subsumption
c [elim-6-3] eliminated 1 variables 0% in round 3 in 2994 steps
c [elim-6-3] backward subsumption/strengthening limit 2900
c [elim-6-3-1] backward checking 2 touched variables 0%
c [elim-6-3-1] incomplete backward checking 0 remain 0%
c [elim-6-3] subsumed 0 and strengthened 0 clauses in 2901 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 233 = 2% variables out of 14546 scheduled
c [bca-2] limit of 10000000 steps and 201585 added (scaled 2)
c [bca-2] 26008 out of 28628 literals actually usable 91%
c [bca-2] added 26 blocked clauses in 59433 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2346 pos 16.7% + 11728 neg 83.3% = 14074 sched 98.3% ret 239
c [sweep-2-1] 1007843 steps 17 queries 2039.18 avg class size
c [sweep-2-1] 311 decisions 13 SAT calls 117.46 avg env size
c [sweep-2-1] 14003 variables remain 98% (304 retained 2%)
c [decomp-14] removed 14 variables
c [sweep-2-1] removed 14 vars (0 failed, 4 eqs, 7 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 14 vars in TOTAL (1 rounds, 16 queries)
c [phase-count-6] 99774 negative 99.3% of 100468 except 694 0.7%
c [phase-count-6] 82637 positive 82.3% of 100468 except 17831 17.7%
c [phase-count-6] less non-negative clauses 694 than limit 10000 (10.0%)
c [phase-count-6] non-pos/non-neg = 17831/694 = 25.69 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 95 negative 100%
c [sort-queue-6] sorted 7276 enqueued variables after 11013 conflicts
c [score-dist-6] active 7023 (49%), one 0 (0%), zero 7276 (51%)
c [score-dist-6] max exp 515, different 15 (3%)
c [score-dist-6] median active exp 508, avg 507.5
c [simplification-6] removed 307 variables 2.1% (14299 remain 8%)
c [simplification-6] removed 2616 irredundant clauses 2.5% (100468 remain 13%)
c [simplification-6] maximum reduction of 3% = max (2%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 9000
c [simplification-6] penalized conflict interval 9000 = 1 * 9000
c [simplification-6] hard conflict limit 30013 (soft 20013 + delta 10000)
c [simplification-6] new conflict limit 20013 (hard 30013)
c 
c [simplification-7] limit 20013 conflicts (hard 30013) hit after 20013 conflicts
c [quatres-3] found 4016 quaternary clauses 64% in total
c [quatres-3-2] added 2 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 14299 free variables schedulable
c [ternres-3] 131 ternary resolvents (0 bin, 131 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 56 xors of average arity 3.0
c [gauss-2] connected 168 occurrences of 117 variables (average 1.4)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 17379579 penalty 0 = 0 + 0
c [basicprobe-3-0] 1823 probes remain 13% after last round
c [basicprobe-3-0] 214 units = 201 failed (94%) + 13 lifted (6%)
c [basicprobe-3-0] removed 289 variables, found 45926 hbrs
c [bate-1] eliminated 225 asymmetric tautologies during probing
c [unhide-7] limit 695183 with penalty 0 = 0 + 0
c [unhide-7-8] 2 units, 197 failed, 5550 tauts, 0 hbrs, 18244 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 305 transitive binary clauses
c [transred-3] found 3 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 13908 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 154 blocked clauses
c [block-2] 154 < 1/100 * 95087 = 950 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 5 clauses out of 62 (8%) of length 7
c [cce-3-1] eliminated 4 clauses out of 504 (1%) of length 6
c [cce-3-1] eliminated 26 clauses out of 1323 (2%) of length 5
c [cce-3-1] eliminated 173 clauses out of 3750 (5%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 209 large clauses in 22795080 steps
c [cce-3-1] allowing another 11397540 steps for small clauses
c [cce-3-1] scheduling 72215 clauses = 52403 binary + 19812 ternary
c [cce-3-1] tried to eliminate 1423 small clauses 2%
c [cce-3-1] eliminated 328 binary clauses 1%
c [cce-3-1] eliminated 55 ternary clauses 0%
c [cce-3-1] eliminated 383 small clauses 1%
c [cce-3-1] eliminated 383 small clauses in 30000003 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 592 covered clauses in round 1
c [cce-3] eliminated 592 covered clauses in TOTAL during 1 rounds
c [cce-3] 592 < 1/100 * 94418 = 944 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 13908 variables 100%
c [elim-7] limit of 69518316 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 447 variables 3% in round 1 in 6643539 steps
c [elim-7-1] backward subsumption/strengthening limit 6643500
c [elim-7-1-1] backward checking 2432 touched variables 17%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 3 and strengthened 35 clauses in 402674 steps
c [elim-7-1] rescheduled 111 variables 1% by backward subsumption
c [elim-7-2] eliminated 7 variables 0% in round 2 in 53469 steps
c [elim-7-2] backward subsumption/strengthening limit 53400
c [elim-7-2-1] backward checking 64 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 6 and strengthened 4 clauses in 21904 steps
c [elim-7-2] rescheduled 15 variables 0% by backward subsumption
c [elim-7-3] eliminated 3 variables 0% in round 3 in 8560 steps
c [elim-7-3] backward subsumption/strengthening limit 8500
c [elim-7-3-1] backward checking 18 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 0 and strengthened 0 clauses in 8501 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 458 = 3% variables out of 13908 scheduled
c [bca-3] limit of 10000000 steps and 186734 added (scaled 2)
c [bca-3] 24268 out of 26902 literals actually usable 90%
c [bca-3] added 26 blocked clauses in 57829 steps
c [sweep-3] limit 1042774 penalty 0 = 0 + 0
c [sweep-3-1] 2349 pos 17.8% + 10842 neg 82.2% = 13191 sched 98.1% ret 259
c [sweep-3-1] 1166198 steps 25 queries 1485.68 avg class size
c [sweep-3-1] 511 decisions 24 SAT calls 140.25 avg env size
c [sweep-3-1] 12741 variables remain 95% (703 retained 5%)
c [decomp-16] removed 40 variables
c [sweep-3-1] removed 40 vars (0 failed, 0 eqs, 3 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 40 vars in TOTAL (1 rounds, 24 queries)
c [phase-count-7] 92402 negative 99.3% of 93008 except 606 0.7%
c [phase-count-7] 76406 positive 82.1% of 93008 except 16602 17.9%
c [phase-count-7] less non-negative clauses 606 than limit 9300 (10.0%)
c [phase-count-7] non-pos/non-neg = 16602/606 = 27.40 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 66 negative 100%
c [sort-queue-7] sorted 6447 enqueued variables after 20013 conflicts
c [score-dist-7] active 6963 (52%), one 0 (0%), zero 6447 (48%)
c [score-dist-7] max exp 516, different 16 (3%)
c [score-dist-7] median active exp 508, avg 508.1
c [simplification-7] removed 889 variables 6.2% (13410 remain 8%)
c [simplification-7] removed 7460 irredundant clauses 7.4% (93008 remain 12%)
c [simplification-7] maximum reduction of 7% = max (6%, 7%)
c [simplification-7] large reduction 7% >= 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 32013 (soft 22013 + delta 10000)
c [simplification-7] new conflict limit 22013 (hard 32013)
c 
c [simplification-8] limit 22013 conflicts (hard 32013) hit after 22015 conflicts
c [quatres-4] found 3725 quaternary clauses 62% in total
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 13410 free variables schedulable
c [ternres-4] 196 ternary resolvents (1 bin, 195 trn)
c [ternres-4] fully completed ternary resolution
c [simpleprobe-4] all 13410 free variables schedulable
c [simpleprobe-4] limit 14896519 penalty 0 = 0 + 0
c [decomp-18] removed 71 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 71 variables, found 5351 hbrs, 46 units
c [unhide-8] limit 744825 with penalty 0 = 0 + 0
c [unhide-8-10] 1 units, 31 failed, 5966 tauts, 0 hbrs, 9874 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 327 transitive binary clauses
c [transred-4] found 6 units
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 13307 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1489651920 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 143 variables 1% in round 1 in 6449846 steps
c [elim-8-1] backward subsumption/strengthening limit 6449800
c [elim-8-1-1] backward checking 833 touched variables 6%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 2 and strengthened 12 clauses in 148811 steps
c [elim-8-1] rescheduled 38 variables 0% by backward subsumption
c [elim-8-2] eliminated 8 variables 0% in round 2 in 17051 steps
c [elim-8-2] backward subsumption/strengthening limit 17000
c [elim-8-2-1] backward checking 46 touched variables 0%
c [elim-8-2-1] incomplete backward checking 0 remain 0%
c [elim-8-2] subsumed 7 and strengthened 4 clauses in 17001 steps
c [elim-8-2] rescheduled 13 variables 0% by backward subsumption
c [elim-8-3] eliminated 2 variables 0% in round 3 in 23970 steps
c [elim-8-3] backward subsumption/strengthening limit 23900
c [elim-8-3-1] backward checking 31 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 0 and strengthened 0 clauses in 15155 steps
c [elim-8] fully completed in 3 rounds
c [gc-50] reconnected 53575 binary clauses (produced 0 empty 1 units)
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 157 = 1% variables out of 13307 scheduled
c [bca-4] limit of 10000000 steps and 181851 added (scaled 2)
c [bca-4] 23653 out of 26302 literals actually usable 90%
c [bca-4] added 16 blocked clauses in 56801 steps
c [sweep-4] limit 1117238 penalty 0 = 0 + 0
c [sweep-4-1] 2215 pos 17.7% + 10265 neg 82.3% = 12480 sched 94.9% ret 670
c [sweep-4-1] 1129795 steps 23 queries 1224.74 avg class size
c [sweep-4-1] 631 decisions 20 SAT calls 199.55 avg env size
c [sweep-4-1] 12075 variables remain 92% (1045 retained 8%)
c [decomp-19] removed 34 variables
c [sweep-4-1] removed 34 vars (0 failed, 4 eqs, 7 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 34 vars in TOTAL (1 rounds, 22 queries)
c [phase-count-8] 89791 negative 99.3% of 90379 except 588 0.7%
c [phase-count-8] 74277 positive 82.2% of 90379 except 16102 17.8%
c [phase-count-8] less non-negative clauses 588 than limit 9000 (10.0%)
c [phase-count-8] non-pos/non-neg = 16102/588 = 27.38 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 41 negative 100%
c [sort-queue-8] sorted 6124 enqueued variables after 22015 conflicts
c [score-dist-8] active 6992 (53%), one 0 (0%), zero 6124 (47%)
c [score-dist-8] max exp 516, different 16 (3%)
c [score-dist-8] median active exp 508, avg 508.2
c [simplification-8] removed 294 variables 2.2% (13116 remain 8%)
c [simplification-8] removed 2629 irredundant clauses 2.8% (90379 remain 11%)
c [simplification-8] maximum reduction of 3% = max (2%, 3%)
c [simplification-8] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-8] new conflict interval 14000
c [simplification-8] penalized conflict interval 14000 = 1 * 14000
c [simplification-8] hard conflict limit 46015 (soft 36015 + delta 10000)
c [simplification-8] new conflict limit 36015 (hard 46015)
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   28.2   13115    90379     33659   12405    659 52274  118   140   32  84%    396   88  100   46  218%
c 
c [simplification-9] limit 36015 conflicts (hard 46015) hit after 41407 conflicts
c [ternres-5] limit 6176043 with penalty 0 = 0 + 0
c [ternres-5] all 13115 free variables schedulable
c [ternres-5] 119 ternary resolvents (0 bin, 119 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-20] removed 1 variables
c [unhide-9] limit 1235208 with penalty 0 = 0 + 0
c [unhide-9-12] 3 units, 25 failed, 2474 tauts, 0 hbrs, 33161 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 268 transitive binary clauses
c [transred-5] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 154401080 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 2 clauses out of 505 (0%) of length 6
c [cce-4-1] eliminated 21 clauses out of 1372 (2%) of length 5
c [cce-4-1] eliminated 134 clauses out of 3631 (4%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 157 large clauses in 23060932 steps
c [cce-4-1] allowing another 11530466 steps for small clauses
c [cce-4-1] scheduling 65232 clauses = 49680 binary + 15552 ternary
c [cce-4-1] tried to eliminate 11915 small clauses 18%
c [cce-4-1] eliminated 2658 binary clauses 5%
c [cce-4-1] eliminated 423 ternary clauses 3%
c [cce-4-1] eliminated 3081 small clauses 5%
c [cce-4-1] eliminated 3249 small clauses in 154401085 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 3406 covered clauses in round 1
c [cce-4] eliminated 3406 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 13084 variables 100%
c [elim-9] limit of 123520864 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 257 variables 2% in round 1 in 6043852 steps
c [elim-9-1] backward subsumption/strengthening limit 6043800
c [elim-9-1-1] backward checking 1664 touched variables 13%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 4 and strengthened 14 clauses in 281828 steps
c [elim-9-1] rescheduled 48 variables 0% by backward subsumption
c [elim-9-2] eliminated 7 variables 0% in round 2 in 31915 steps
c [elim-9-2] backward subsumption/strengthening limit 31900
c [elim-9-2-1] backward checking 28 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 4 and strengthened 3 clauses in 17690 steps
c [elim-9-2] rescheduled 17 variables 0% by backward subsumption
c [elim-9-3] eliminated 5 variables 0% in round 3 in 9490 steps
c [elim-9-3] backward subsumption/strengthening limit 9400
c [elim-9-3-1] backward checking 19 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 1 and strengthened 0 clauses in 9401 steps
c [elim-9] incomplete 7 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 271 = 2% variables out of 13084 scheduled
c [bca-5] limit of 10000000 steps and 172389 added (scaled 2)
c [bca-5] 22570 out of 25628 literals actually usable 88%
c [bca-5] added 11 blocked clauses in 64819 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 18528120 penalty 0 = 0 + 0
c [sweep-5-1] 2091 pos 17.7% + 9708 neg 82.3% = 11799 sched 92.1% ret 1014
c [sweep-5-1] 18546229 steps 519 queries 46.77 avg class size
c [sweep-5-1] 4276 decisions 501 SAT calls 54.59 avg env size
c [sweep-5-1] 3401 variables remain 27% (9355 retained 73%)
c [decomp-21] removed 100 variables
c [sweep-5-1] removed 100 vars (0 failed, 26 eqs, 48 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 100 vars in TOTAL (1 rounds, 518 queries)
c [phase-count-9] 84620 negative 99.3% of 85184 except 564 0.7%
c [phase-count-9] 70562 positive 82.8% of 85184 except 14622 17.2%
c [phase-count-9] less non-negative clauses 564 than limit 8500 (10.0%)
c [phase-count-9] non-pos/non-neg = 14622/564 = 25.93 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 12 negative 100%
c [sort-queue-9] sorted 5340 enqueued variables after 41407 conflicts
c [score-dist-9] active 7373 (58%), one 0 (0%), zero 5340 (42%)
c [score-dist-9] max exp 517, different 17 (3%)
c [score-dist-9] median active exp 509, avg 508.7
c [simplification-9] removed 402 variables 3.1% (12713 remain 7%)
c [simplification-9] removed 5195 irredundant clauses 5.7% (85184 remain 11%)
c [simplification-9] maximum reduction of 6% = max (3%, 6%)
c [simplification-9] large reduction 6% >= 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 53407 (soft 43407 + delta 10000)
c [simplification-9] new conflict limit 43407 (hard 53407)
c 
c [simplification-10] limit 43407 conflicts (hard 53407) hit after 43409 conflicts
c [quatres-5] found 3476 quaternary clauses 57% in total
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [ternres-6] limit 6454592 with penalty 0 = 0 + 0
c [ternres-6] all 12713 free variables schedulable
c [ternres-6] 64 ternary resolvents (0 bin, 64 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 403412 penalty 3 = 3 + 0
c [card-4] found 1167 at-most-one constraints of average size 3.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 403412 for elimination
c [card-4] 1167 out of 1167 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 24 xors of average arity 3.0
c [gauss-3] connected 72 occurrences of 54 variables (average 1.3)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-4] limit 322729 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 23162 literals 91%
c [treelook-4] scheduling used 322850 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 322729 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 357698 steps
c [treelook-4] 23127 literals remain 91%
c [treelook-4] 12693 variables remain to probed next time 100%
c [decomp-23] removed 1 variables
c [treelook-4] removed 12 variables, found 881 hbrs
c [unhide-10] limit 1290918 with penalty 0 = 0 + 0
c [unhide-10-14] 5 units, 63 failed, 2638 tauts, 0 hbrs, 24877 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 219 transitive binary clauses
c [transred-6] found 8 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 12620 variables 100%
c [block-3] limit of 16136482 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 85 blocked clauses
c [block-3] 85 < 1/100 * 84091 = 840 considered unsuccessful
c [cce-5] limit of 32272964 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 2 clauses out of 10 (20%) of length 9
c [cce-5-1] eliminated 2 clauses out of 19 (11%) of length 8
c [cce-5-1] eliminated 4 clauses out of 96 (4%) of length 7
c [cce-5-1] eliminated 3 clauses out of 492 (1%) of length 6
c [cce-5-1] eliminated 23 clauses out of 1338 (2%) of length 5
c [cce-5-1] eliminated 124 clauses out of 3383 (4%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 158 large clauses in 20063263 steps
c [cce-5-1] allowing another 10031631 steps for small clauses
c [cce-5-1] scheduling 63696 clauses = 45687 binary + 18009 ternary
c [cce-5-1] tried to eliminate 1837 small clauses 3%
c [cce-5-1] eliminated 377 binary clauses 1%
c [cce-5-1] eliminated 72 ternary clauses 0%
c [cce-5-1] eliminated 449 small clauses 1%
c [cce-5-1] eliminated 449 small clauses in 32272969 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 607 covered clauses in round 1
c [cce-5] eliminated 607 covered clauses in TOTAL during 1 rounds
c [cce-5] 607 < 1/100 * 83619 = 836 considered unsuccessful
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 12616 variables 100%
c [elim-10] limit of 129091859 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 213 variables 2% in round 1 in 5787719 steps
c [elim-10-1] backward subsumption/strengthening limit 5787700
c [elim-10-1-1] backward checking 1318 touched variables 10%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 0 and strengthened 6 clauses in 224194 steps
c [elim-10-1] rescheduled 49 variables 0% by backward subsumption
c [elim-10-2] eliminated 5 variables 0% in round 2 in 23986 steps
c [elim-10-2] backward subsumption/strengthening limit 23900
c [elim-10-2-1] backward checking 26 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 0 clauses in 10982 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 224 = 2% variables out of 12616 scheduled
c [bca-6] limit of 10000000 steps and 165738 added (scaled 2)
c [bca-6] 21718 out of 24786 literals actually usable 88%
c [bca-6] added 9 blocked clauses in 59638 steps
c [sweep-6] limit 1936377 penalty 0 = 0 + 0
c [sweep-6-1] 1220 pos 37.1% + 2064 neg 62.9% = 3284 sched 26.5% ret 9108
c [sweep-6-1] 1999866 steps 69 queries 176.43 avg class size
c [sweep-6-1] 308 decisions 68 SAT calls 40.65 avg env size
c [sweep-6-1] 3095 variables remain 25% (9290 retained 75%)
c [decomp-24] removed 13 variables
c [sweep-6-1] removed 13 vars (0 failed, 2 eqs, 3 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 13 vars in TOTAL (1 rounds, 68 queries)
c [phase-count-10] 81950 negative 99.4% of 82475 except 525 0.6%
c [phase-count-10] 68350 positive 82.9% of 82475 except 14125 17.1%
c [phase-count-10] less non-negative clauses 525 than limit 8200 (10.0%)
c [phase-count-10] non-pos/non-neg = 14125/525 = 26.90 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 8 negative 100%
c [sort-queue-10] sorted 5157 enqueued variables after 43409 conflicts
c [score-dist-10] active 7222 (58%), one 0 (0%), zero 5157 (42%)
c [score-dist-10] max exp 517, different 17 (3%)
c [score-dist-10] median active exp 509, avg 508.7
c [simplification-10] removed 334 variables 2.6% (12379 remain 7%)
c [simplification-10] removed 2709 irredundant clauses 3.2% (82475 remain 10%)
c [simplification-10] maximum reduction of 3% = max (3%, 3%)
c [simplification-10] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-10] new conflict interval 19000
c [simplification-10] penalized conflict interval 19000 = 1 * 19000
c [simplification-10] hard conflict limit 72409 (soft 62409 + delta 10000)
c [simplification-10] new conflict limit 62409 (hard 72409)
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   46.4   12378    82475     56257   20764    970 59258  118   158   43  75%    207   82  142   61  233%
c i   47.2   12376    82475     58689   22023    971 59258  131   181   43  73%    -75  101  168   64  263%
c i   47.9   12375    82475     60720   23375    979 59259  137   202   44  68%   -101  119  139   67  209%
c i   48.9   12374    82475     63078   24878    981 59260  154   220   45  70%    -98  133  177   70  252%
c i   51.3   12373    82475     68741   27538    990 59262  155   204   56  76%    -43  106  146   78  188%
c i   51.3   12372    82475     68748   27539    993 59262  155   204   56  76%    -44  106  143   78  185%
c 
c [simplification-11] limit 62410 conflicts (hard 72409) hit after 72409 conflicts
c [quatres-6] found 3313 quaternary clauses 56% in total
c [quatres-6-2] added 6 quaternary resolvents
c [ternres-7] limit 9869681 with penalty 0 = 0 + 0
c [ternres-7] all 12372 free variables schedulable
c [ternres-7] 67 ternary resolvents (0 bin, 67 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-25] removed 7 variables
c [basicprobe-4] limit 49348409 penalty 0 = 0 + 0
c [basicprobe-4-0] 1892 sched 17%, 687 failed, 107 lifted, 60913 hbrs
c [decomp-26] removed 1076 variables
c [basicprobe-4-1] 1739 probes remain 15% after last round
c [basicprobe-4-1] 844 units = 737 failed (87%) + 107 lifted (13%)
c [basicprobe-4-1] removed 1141 variables, found 72115 hbrs
c [bate-2] eliminated 326 asymmetric tautologies during probing
c [unhide-11] limit 1973936 with penalty 0 = 0 + 0
c [unhide-11-17] 3 units, 90 failed, 10217 tauts, 0 hbrs, 88792 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 382 transitive binary clauses
c [transred-7] found 5 units
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 11138 variables 100%
c [elim-11] limit of 197393637 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 832 variables 7% in round 1 in 4693854 steps
c [elim-11-1] backward subsumption/strengthening limit 4693800
c [elim-11-1-1] backward checking 3499 touched variables 31%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 2 and strengthened 24 clauses in 497279 steps
c [elim-11-1] rescheduled 93 variables 1% by backward subsumption
c [elim-11-2] eliminated 7 variables 0% in round 2 in 41696 steps
c [elim-11-2] backward subsumption/strengthening limit 41600
c [elim-11-2-1] backward checking 43 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 2 and strengthened 0 clauses in 17387 steps
c [elim-11-2] rescheduled 4 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 2352 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 839 = 8% variables out of 11138 scheduled
c [bca-7] limit of 10000000 steps and 135851 added (scaled 2)
c [bca-7] 18089 out of 20600 literals actually usable 88%
c [bca-7] added 21 blocked clauses in 49893 steps
c [sweep-7] limit 2960904 penalty 0 = 0 + 0
c [sweep-7-1] 1002 pos 37.2% + 1690 neg 62.8% = 2692 sched 26.1% ret 7607
c [sweep-7-1] 2982530 steps 177 queries 76.76 avg class size
c [sweep-7-1] 689 decisions 172 SAT calls 24.27 avg env size
c [sweep-7-1] 2124 variables remain 21% (8173 retained 79%)
c [decomp-27] removed 6 variables
c [sweep-7-1] removed 6 vars (0 failed, 5 eqs, 7 impls)
c [sweep-7] 6 < 1/1000 * 10299 = 10 considered unsuccessful
c [sweep-7] removed 6 vars in TOTAL (1 rounds, 176 queries)
c [phase-count-11] 67193 negative 99.4% of 67626 except 433 0.6%
c [phase-count-11] 55175 positive 81.6% of 67626 except 12451 18.4%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 3882 enqueued variables after 72409 conflicts
c [score-dist-11] active 6411 (62%), one 0 (0%), zero 3882 (38%)
c [score-dist-11] max exp 517, different 17 (3%)
c [score-dist-11] median active exp 509, avg 509.2
c [simplification-11] removed 2079 variables 16.8% (10293 remain 6%)
c [simplification-11] removed 14849 irredundant clauses 18.0% (67626 remain 8%)
c [simplification-11] maximum reduction of 18% = max (17%, 18%)
c [simplification-11] large reduction 18% >= 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 84409 (soft 74409 + delta 10000)
c [simplification-11] new conflict limit 74409 (hard 84409)
c 
c [simplification-12] limit 74409 conflicts (hard 84409) hit after 76764 conflicts
c [quatres-7] found 3057 quaternary clauses 56% in total
c [quatres-7-2] added 2 quaternary resolvents
c [ternres-8] limit 10294754 with penalty 0 = 0 + 0
c [ternres-8] all 10293 free variables schedulable
c [ternres-8] 64 ternary resolvents (1 bin, 63 trn)
c [ternres-8] fully completed ternary resolution
c [simpleprobe-5] all 10293 free variables schedulable
c [simpleprobe-5] limit 41179016 penalty 0 = 0 + 0
c [decomp-29] removed 91 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 91 variables, found 6313 hbrs, 51 units
c [unhide-12] limit 2058950 with penalty 0 = 0 + 0
c [unhide-12-21] 0 units, 17 failed, 8433 tauts, 0 hbrs, 28594 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 474 transitive binary clauses
c [transred-8] found 1 units
c [cce-6] limit of 25736885 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 2 clauses out of 108 (2%) of length 7
c [cce-6-1] eliminated 5 clauses out of 388 (1%) of length 6
c [cce-6-1] eliminated 28 clauses out of 1151 (2%) of length 5
c [cce-6-1] eliminated 138 clauses out of 2900 (5%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 173 large clauses in 15003983 steps
c [cce-6-1] allowing another 7501991 steps for small clauses
c [cce-6-1] scheduling 50542 clauses = 37718 binary + 12824 ternary
c [cce-6-1] tried to eliminate 1984 small clauses 4%
c [cce-6-1] eliminated 299 binary clauses 1%
c [cce-6-1] eliminated 27 ternary clauses 0%
c [cce-6-1] eliminated 326 small clauses 1%
c [cce-6-1] eliminated 354 small clauses in 25736887 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 527 covered clauses in round 1
c [cce-6] eliminated 527 covered clauses in TOTAL during 1 rounds
c [cce-6] 527 < 1/100 * 66068 = 660 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 10191 variables 100%
c [elim-12] limit of 205895081 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 128 variables 1% in round 1 in 4425875 steps
c [elim-12-1] backward subsumption/strengthening limit 4425800
c [elim-12-1-1] backward checking 830 touched variables 8%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 135775 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 128 = 1% variables out of 10191 scheduled
c [bca-8] limit of 10000000 steps and 131343 added (scaled 2)
c [bca-8] 17446 out of 20128 literals actually usable 87%
c [bca-8] added 10 blocked clauses in 51081 steps
c [phase-count-12] 64969 negative 99.4% of 65391 except 422 0.6%
c [phase-count-12] 53345 positive 81.6% of 65391 except 12046 18.4%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 3726 enqueued variables after 76764 conflicts
c [score-dist-12] active 6337 (63%), one 0 (0%), zero 3726 (37%)
c [score-dist-12] max exp 517, different 17 (3%)
c [score-dist-12] median active exp 510, avg 509.3
c [simplification-12] removed 230 variables 2.2% (10063 remain 6%)
c [simplification-12] removed 2235 irredundant clauses 3.3% (65391 remain 8%)
c [simplification-12] maximum reduction of 3% = max (2%, 3%)
c [simplification-12] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-12] new conflict interval 24000
c [simplification-12] penalized conflict interval 24000 = 1 * 24000
c [simplification-12] hard conflict limit 112764 (soft 100764 + delta 12000)
c [simplification-12] new conflict limit 100764 (hard 112764)
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   67.5   10062    65391     94476   26214    607 56493   70   108   35  65%    242   -7   39   84   47%
c 
c [simplification-13] limit 100764 conflicts (hard 112764) hit after 112765 conflicts
c [quatres-8] found 2886 quaternary clauses 53% in total
c [ternres-9] limit 13933930 with penalty 0 = 0 + 0
c [ternres-9] all 10062 free variables schedulable
c [ternres-9] 19 ternary resolvents (0 bin, 19 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-30] removed 2 variables
c [treelook-5] limit 1393393 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 20116 literals 100%
c [treelook-5] scheduling used 417173 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 1393393 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1405354 steps
c [treelook-5] 20035 literals remain 100%
c [treelook-5] 10045 variables remain to probed next time 100%
c [treelook-5] removed 10 variables, found 6990 hbrs
c [unhide-13] limit 2786786 with penalty 0 = 0 + 0
c [unhide-13-24] 0 units, 5 failed, 2669 tauts, 0 hbrs, 162718 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 425 transitive binary clauses
c [transred-9] found 1 units
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 10045 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 28 variables 0% in round 1 in 4365612 steps
c [elim-13-1] backward subsumption/strengthening limit 4365600
c [elim-13-1-1] backward checking 181 touched variables 2%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 1 and strengthened 0 clauses in 36746 steps
c [elim-13-1] rescheduled 3 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 686 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 28 = 0% variables out of 10045 scheduled
c [elim-13] 28 < 1/100 * 10045 = 100 considered unsuccessful
c [bca-9] limit of 10000000 steps and 130244 added (scaled 2)
c [bca-9] 16796 out of 20036 literals actually usable 84%
c [bca-9] added 10 blocked clauses in 78176 steps
c [sweep-8] limit 2090089 penalty 1 = 1 + 0
c [sweep-8-1] 843 pos 40.6% + 1231 neg 59.4% = 2074 sched 20.7% ret 7943
c [sweep-8-1] 2093039 steps 117 queries 55.21 avg class size
c [sweep-8-1] 550 decisions 107 SAT calls 23.76 avg env size
c [sweep-8-1] 1763 variables remain 18% (8254 retained 82%)
c [decomp-32] removed 8 variables
c [sweep-8-1] removed 8 vars (0 failed, 9 eqs, 9 impls)
c [sweep-8] 8 < 1/1000 * 10017 = 10 considered unsuccessful
c [sweep-8] removed 8 vars in TOTAL (1 rounds, 116 queries)
c [phase-count-13] 64393 negative 99.3% of 64822 except 429 0.7%
c [phase-count-13] 52941 positive 81.7% of 64822 except 11881 18.3%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 3527 enqueued variables after 112765 conflicts
c [score-dist-13] active 6482 (65%), one 0 (0%), zero 3527 (35%)
c [score-dist-13] max exp 518, different 18 (3%)
c [score-dist-13] median active exp 511, avg 509.9
c [simplification-13] removed 53 variables 0.5% (10009 remain 6%)
c [simplification-13] removed 569 irredundant clauses 0.9% (64822 remain 8%)
c [simplification-13] maximum reduction of 1% = max (1%, 1%)
c [simplification-13] geometric conflict interval increment 12000 = 24000 / 2
c [simplification-13] new conflict interval 36000
c [simplification-13] penalized conflict interval 36000 = 1 * 36000
c [simplification-13] hard conflict limit 166765 (soft 148765 + delta 18000)
c [simplification-13] new conflict limit 148765 (hard 166765)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   79.7   10008    64822    116697   46997    604 60329   50    86   53  58%    176  -22   48   73   66%
c i   79.7   10007    64822    116699   46998    604 60329   49    86   53  58%    176  -22   48   73   65%
c i   79.7   10006    64822    116700   46998    604 60329   49    86   53  58%    175  -22   48   73   65%
c i   79.7   10002    64822    116701   46998    604 60329   49    86   53  58%    175  -22   48   73   65%
c -   81.5   10002    64822    121008   24775    605 60330   54    82   24  65%    -95  -25   56   72   77%
c -   91.8   10002    64822    150010   26437    610 60331   34    75   29  45%    302  -21   34   62   55%
c 
c [simplification-14] limit 148790 conflicts (hard 166765) hit after 166765 conflicts
c [ternres-10] limit 19986723 with penalty 0 = 0 + 0
c [ternres-10] all 10002 free variables schedulable
c [ternres-10] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 499668 penalty 3 = 3 + 0
c [gauss-4] extracted 16 xors of average arity 3.0
c [gauss-4] connected 48 occurrences of 45 variables (average 1.1)
c [gauss-4] limit 499668 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-5] limit 99933617 penalty 0 = 0 + 0
c [basicprobe-5-0] 1836 sched 19%, 371 failed, 51 lifted, 34681 hbrs
c [decomp-34] removed 523 variables
c [basicprobe-5-1] 1994 sched 22%, 252 failed, 24 lifted, 21993 hbrs
c [decomp-35] removed 377 variables
c [basicprobe-5-2] 492 probes remain 5% after last round
c [basicprobe-5-2] 812 units = 735 failed (91%) + 77 lifted (9%)
c [basicprobe-5-2] removed 1031 variables, found 66129 hbrs
c [bate-3] eliminated 220 asymmetric tautologies during probing
c [unhide-14] limit 3997344 with penalty 0 = 0 + 0
c [unhide-14-29] 0 units, 6 failed, 10296 tauts, 0 hbrs, 173610 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 419 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 8967 variables 100%
c [block-4] limit of 24983404 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 208 blocked clauses
c [block-4] 208 < 1/100 * 53884 = 538 considered unsuccessful
c [bca-10] limit of 10000000 steps and 107923 added (scaled 2)
c [bca-10] 14745 out of 17932 literals actually usable 82%
c [bca-10] added 7 blocked clauses in 72492 steps
c [phase-count-14] 53240 negative 99.2% of 53676 except 436 0.8%
c [phase-count-14] 43200 positive 80.5% of 53676 except 10476 19.5%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-14] sorted 2664 enqueued variables after 166765 conflicts
c [score-dist-14] active 6301 (70%), one 0 (0%), zero 2664 (30%)
c [score-dist-14] max exp 519, different 19 (4%)
c [score-dist-14] median active exp 511, avg 510.5
c [simplification-14] removed 1037 variables 10.4% (8965 remain 5%)
c [simplification-14] removed 11146 irredundant clauses 17.2% (53676 remain 7%)
c [simplification-14] maximum reduction of 17% = max (10%, 17%)
c [simplification-14] large reduction 17% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 178765 (soft 168765 + delta 10000)
c [simplification-14] new conflict limit 168765 (hard 178765)
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 -  109.7    8965    53676    178630   27014    571 54979   38    74   26  52%    557  -14   33   52   63%
c 
c [simplification-15] limit 168765 conflicts (hard 178765) hit after 178766 conflicts
c [quatres-9] found 2517 quaternary clauses 51% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [ternres-11] limit 21388525 with penalty 0 = 0 + 0
c [ternres-11] all 8965 free variables schedulable
c [ternres-11] 16 ternary resolvents (0 bin, 16 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 668391 penalty 4 = 4 + 0
c [card-5] found 1863 at-most-one constraints of average size 3.4
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 668391 for elimination
c [card-5] 1863 out of 1863 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-36] removed 39 variables
c [simpleprobe-6] all 8926 free variables schedulable
c [simpleprobe-6] limit 85554100 penalty 0 = 0 + 0
c [decomp-37] removed 23 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 23 variables, found 3581 hbrs, 1 units
c [unhide-15] limit 4277705 with penalty 0 = 0 + 0
c [unhide-15-36] 0 units, 0 failed, 5542 tauts, 0 hbrs, 54306 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 348 transitive binary clauses
c [cce-7] limit of 26735656 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 2 clauses out of 76 (3%) of length 7
c [cce-7-1] eliminated 1 clauses out of 336 (0%) of length 6
c [cce-7-1] eliminated 10 clauses out of 797 (1%) of length 5
c [cce-7-1] eliminated 55 clauses out of 2418 (2%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 68 large clauses in 8930737 steps
c [cce-7-1] allowing another 4465368 steps for small clauses
c [cce-7-1] scheduling 41405 clauses = 32171 binary + 9234 ternary
c [cce-7-1] tried to eliminate 3260 small clauses 8%
c [cce-7-1] eliminated 559 binary clauses 2%
c [cce-7-1] eliminated 45 ternary clauses 0%
c [cce-7-1] eliminated 604 small clauses 1%
c [cce-7-1] eliminated 604 small clauses in 26735659 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 672 covered clauses in round 1
c [cce-7] eliminated 672 covered clauses in TOTAL during 1 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 8903 variables 100%
c [elim-14] limit of 213885251 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 589 variables 7% in round 1 in 3443880 steps
c [elim-14-1] backward subsumption/strengthening limit 3443800
c [elim-14-1-1] backward checking 2613 touched variables 29%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 1 and strengthened 4 clauses in 345991 steps
c [elim-14-1] rescheduled 24 variables 0% by backward subsumption
c [elim-14-2] eliminated 2 variables 0% in round 2 in 9622 steps
c [elim-14-2] backward subsumption/strengthening limit 9600
c [elim-14-2-1] backward checking 13 touched variables 0%
c [elim-14-2-1] incomplete backward checking 0 remain 0%
c [elim-14-2] subsumed 0 and strengthened 3 clauses in 9601 steps
c [elim-14-2] rescheduled 7 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 2874 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 591 = 7% variables out of 8903 scheduled
c [bca-11] limit of 10000000 steps and 104239 added (scaled 2)
c [bca-11] 13726 out of 16626 literals actually usable 83%
c [bca-11] added 27 blocked clauses in 47457 steps
c [sort-queue-15] sorted 2477 enqueued variables after 178766 conflicts
c [score-dist-15] active 5835 (70%), one 0 (0%), zero 2477 (30%)
c [score-dist-15] max exp 519, different 19 (4%)
c [score-dist-15] median active exp 511, avg 510.7
c [simplification-15] removed 653 variables 7.3% (8312 remain 5%)
c [simplification-15] removed 1844 irredundant clauses 3.4% (51832 remain 6%)
c [simplification-15] maximum reduction of 7% = max (7%, 3%)
c [simplification-15] large reduction 7% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 190766 (soft 180766 + delta 10000)
c [simplification-15] new conflict limit 180766 (hard 190766)
c 
c [simplification-16] limit 180766 conflicts (hard 190766) hit after 190766 conflicts
c [ternres-12] limit 22502285 with penalty 0 = 0 + 0
c [ternres-12] all 8312 free variables schedulable
c [ternres-12] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-38] removed 1 variables
c [treelook-6] limit 2250228 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 16618 literals 100%
c [treelook-6] scheduling used 322903 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 2250228 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 2256169 steps
c [treelook-6] 16448 literals remain 99%
c [treelook-6] 8301 variables remain to probed next time 100%
c [treelook-6] removed 6 variables, found 14949 hbrs
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 385 transitive binary clauses
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 8305 variables 100%
c [elim-15] limit of 450045712 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 20 variables 0% in round 1 in 3388381 steps
c [elim-15-1] backward subsumption/strengthening limit 3388300
c [elim-15-1-1] backward checking 144 touched variables 2%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 1 clauses in 26233 steps
c [elim-15-1] rescheduled 5 variables 0% by backward subsumption
c [elim-15-2] no variable eliminated in round 2 in 1769 steps
c [elim-15] fully completed in 2 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 20 = 0% variables out of 8305 scheduled
c [elim-15] 20 < 1/100 * 8305 = 83 considered unsuccessful
c [bca-12] limit of 10000000 steps and 103966 added (scaled 2)
c [bca-12] 13406 out of 16572 literals actually usable 81%
c [bca-12] added 2 blocked clauses in 57848 steps
c [sweep-9] limit 1687671 penalty 2 = 2 + 0
c [sweep-9-1] 624 pos 40.8% + 905 neg 59.2% = 1529 sched 18.5% ret 6756
c [sweep-9-1] 1698492 steps 132 queries 59.15 avg class size
c [sweep-9-1] 537 decisions 129 SAT calls 25.04 avg env size
c [sweep-9-1] 1153 variables remain 14% (7129 retained 86%)
c [decomp-40] removed 5 variables
c [sweep-9-1] removed 5 vars (0 failed, 1 eqs, 3 impls)
c [sweep-9] 5 < 1/1000 * 8285 = 8 considered unsuccessful
c [sweep-9] removed 5 vars in TOTAL (1 rounds, 131 queries)
c [sort-queue-16] sorted 2416 enqueued variables after 190766 conflicts
c [score-dist-16] active 5864 (71%), one 0 (0%), zero 2416 (29%)
c [score-dist-16] max exp 519, different 19 (4%)
c [score-dist-16] median active exp 512, avg 510.9
c [simplification-16] removed 32 variables 0.4% (8280 remain 5%)
c [simplification-16] removed 177 irredundant clauses 0.3% (51655 remain 6%)
c [simplification-16] maximum reduction of 0% = max (0%, 0%)
c [simplification-16] full geometric conflict interval increment 36000
c [simplification-16] new conflict interval 72000
c [simplification-16] penalized conflict interval 72000 = 1 * 72000
c [simplification-16] hard conflict limit 298766 (soft 262766 + delta 36000)
c [simplification-16] new conflict limit 262766 (hard 298766)
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 -  127.0    8280    51655    216914   25702    495 58279   33    55   24  60%    764  -22   32   45   70%
c -  137.7    8280    51655    248016   26495    501 58285   45    63   25  72%    862   -9   52   45  117%
c -  147.9    8280    51655    279640   27034    503 58287   47    65   24  73%    924   -1   45   44  103%
c 
c [simplification-17] limit 262766 conflicts (hard 298766) hit after 285014 conflicts
c [ternres-13] limit 32478825 with penalty 0 = 0 + 0
c [ternres-13] all 8280 free variables schedulable
c [ternres-13] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-13] fully completed ternary resolution
c [basicprobe-6] limit 162394126 penalty 0 = 0 + 0
c [basicprobe-6-0] 739 sched 9%, 99 failed, 1 lifted, 6867 hbrs
c [decomp-42] removed 133 variables
c [basicprobe-6-1] 1940 sched 24%, 148 failed, 7 lifted, 14170 hbrs
c [decomp-43] removed 194 variables
c [basicprobe-6-2] 1859 sched 24%, 62 failed, 1 lifted, 7924 hbrs
c [decomp-44] removed 83 variables
c [basicprobe-6-3] 1845 sched 24%, 25 failed, 1 lifted, 1777 hbrs
c [decomp-45] removed 35 variables
c [basicprobe-6-4] 1847 sched 24%, 6 failed, 0 lifted, 385 hbrs
c [decomp-46] removed 8 variables
c [basicprobe-6-5] 1845 sched 24%, 2 failed, 0 lifted, 111 hbrs
c [decomp-47] removed 2 variables
c [basicprobe-6-6] 414 probes remain 5% after last round
c [basicprobe-6-6] 353 units = 343 failed (97%) + 10 lifted (3%)
c [basicprobe-6-6] removed 456 variables, found 31258 hbrs
c [bate-4] eliminated 139 asymmetric tautologies during probing
c [unhide-16] limit 3247882 with penalty 1 = 1 + 0
c [unhide-16-41] 0 units, 0 failed, 10410 tauts, 0 hbrs, 73183 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 288 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 811970630 steps penalty 1 = 1 + 0
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 10
c [cce-8-1] eliminated 2 clauses out of 81 (2%) of length 7
c [cce-8-1] eliminated 17 clauses out of 805 (2%) of length 5
c [cce-8-1] eliminated 33 clauses out of 2284 (1%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 53 large clauses in 8342482 steps
c [cce-8-1] allowing another 4171241 steps for small clauses
c [cce-8-1] scheduling 35898 clauses = 28492 binary + 7406 ternary
c [cce-8-1] tried to eliminate 35898 small clauses 100%
c [cce-8-1] eliminated 4067 binary clauses 14%
c [cce-8-1] eliminated 252 ternary clauses 3%
c [cce-8-1] eliminated 4319 small clauses 12%
c [cce-8-1] eliminated 4319 small clauses in 182593432 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] completed small and large (ATE)
c [cce-8-1] eliminated 4372 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 3889663 steps for small clauses
c [cce-8-2] scheduling 31579 clauses = 24425 binary + 7154 ternary
c [cce-8-2] tried to eliminate 31579 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 4372 covered clauses in TOTAL during 2 rounds
c [bca-13] limit of 10000000 steps and 84061 added (scaled 2)
c [bca-13] 12446 out of 15650 literals actually usable 80%
c [bca-13] added 10 blocked clauses in 58097 steps
c [sort-queue-17] sorted 2044 enqueued variables after 285014 conflicts
c [score-dist-17] active 5780 (74%), one 0 (0%), zero 2044 (26%)
c [score-dist-17] max exp 519, different 19 (4%)
c [score-dist-17] median active exp 512, avg 511.6
c [simplification-17] removed 456 variables 5.5% (7824 remain 5%)
c [simplification-17] removed 9919 irredundant clauses 19.2% (41736 remain 5%)
c [simplification-17] maximum reduction of 19% = max (6%, 19%)
c [simplification-17] large reduction 19% >= 5% limit
c [simplification-17] next conflict interval 2850 = min (285014/100, 72000)
c [simplification-17] penalized conflict interval 2850 = 1 * 2850
c [simplification-17] hard conflict limit 297864 (soft 287864 + delta 10000)
c [simplification-17] new conflict limit 287864 (hard 297864)
c 
c [simplification-18] limit 287864 conflicts (hard 297864) hit after 287864 conflicts
c [quatres-10] found 2353 quaternary clauses 49% in total
c [ternres-14] limit 32723675 with penalty 0 = 0 + 0
c [ternres-14] all 7824 free variables schedulable
c [ternres-14] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-48] removed 13 variables
c [simpleprobe-7] all 7811 free variables schedulable
c [simpleprobe-7] limit 130894700 penalty 0 = 0 + 0
c [decomp-49] removed 44 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 44 variables, found 2671 hbrs, 0 units
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 524 transitive binary clauses
c [cce-9] limit of 163618375 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 5 clauses out of 788 (1%) of length 5
c [cce-9-1] eliminated 25 clauses out of 2251 (1%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 30 large clauses in 8030514 steps
c [cce-9-1] allowing another 4015257 steps for small clauses
c [cce-9-1] scheduling 31487 clauses = 24356 binary + 7131 ternary
c [cce-9-1] tried to eliminate 31487 small clauses 100%
c [cce-9-1] eliminated 871 binary clauses 4%
c [cce-9-1] eliminated 145 ternary clauses 2%
c [cce-9-1] eliminated 1016 small clauses 3%
c [cce-9-1] eliminated 1016 small clauses in 155939345 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] completed small and large (ACCE)
c [cce-9-1] eliminated 1046 covered clauses in round 1
c [cce-9-2] eliminated 1 clauses out of 346 (0%) of length 6
c [cce-9-2] eliminated 3 clauses out of 783 (0%) of length 5
c [cce-9-2] eliminated 10 clauses out of 2226 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 14 large clauses in 7652037 steps
c [cce-9-2] allowing another 3826018 steps for small clauses
c [cce-9-2] scheduling 30471 clauses = 23485 binary + 6986 ternary
c [cce-9-2] tried to eliminate 800 small clauses 3%
c [cce-9-2] eliminated 2 binary clauses 0%
c [cce-9-2] eliminated 2 ternary clauses 0%
c [cce-9-2] eliminated 4 small clauses 0%
c [cce-9-2] eliminated 4 small clauses in 7679035 steps
c [cce-9-2] incomplete small round (ACCE)
c [cce-9-2] eliminated 18 covered clauses in round 2
c [cce-9] eliminated 1064 covered clauses in TOTAL during 2 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 7767 variables 100%
c [elim-16] limit of 327236750 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 810 variables 10% in round 1 in 2589033 steps
c [elim-16-1] backward subsumption/strengthening limit 2589000
c [elim-16-1-1] backward checking 3191 touched variables 41%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 5 and strengthened 4 clauses in 342938 steps
c [elim-16-1] rescheduled 52 variables 1% by backward subsumption
c [elim-16-2] eliminated 3 variables 0% in round 2 in 22852 steps
c [elim-16-2] backward subsumption/strengthening limit 22800
c [elim-16-2-1] backward checking 20 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 15451 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 813 = 10% variables out of 7767 scheduled
c [bca-14] limit of 10000000 steps and 80144 added (scaled 2)
c [bca-14] 11192 out of 13910 literals actually usable 80%
c [bca-14] added 15 blocked clauses in 40835 steps
c [sort-queue-18] sorted 1865 enqueued variables after 287864 conflicts
c [score-dist-18] active 5089 (73%), one 0 (0%), zero 1865 (27%)
c [score-dist-18] max exp 519, different 19 (4%)
c [score-dist-18] median active exp 513, avg 511.8
c [simplification-18] removed 870 variables 11.1% (6954 remain 4%)
c [simplification-18] removed 1961 irredundant clauses 4.7% (39775 remain 5%)
c [simplification-18] maximum reduction of 11% = max (11%, 5%)
c [simplification-18] large reduction 11% >= 5% limit
c [simplification-18] next conflict interval 2878 = min (287864/100, 72000)
c [simplification-18] penalized conflict interval 2878 = 1 * 2878
c [simplification-18] hard conflict limit 300742 (soft 290742 + delta 10000)
c [simplification-18] new conflict limit 290742 (hard 300742)
c 
c [simplification-19] limit 290742 conflicts (hard 300742) hit after 290742 conflicts
c [ternres-15] limit 32931522 with penalty 0 = 0 + 0
c [ternres-15] all 6954 free variables schedulable
c [ternres-15] 10 ternary resolvents (1 bin, 9 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 411644 penalty 4 = 4 + 0
c [gauss-5] extracted 11 xors of average arity 3.0
c [gauss-5] connected 33 occurrences of 24 variables (average 1.4)
c [gauss-5] limit 411644 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-7] limit 3293152 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 13904 literals 100%
c [treelook-7] scheduling used 262696 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 3293152 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 3322070 steps
c [treelook-7] 13638 literals remain 98%
c [treelook-7] 6947 variables remain to probed next time 100%
c [treelook-7] removed 3 variables, found 14042 hbrs
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 532 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 6951 variables 100%
c [block-5] limit of 20582201 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 18 blocked clauses
c [block-5] 18 < 1/100 * 39721 = 397 considered unsuccessful
c [cce-10] limit of 164657610 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 1 (100%) of length 32
c [cce-10-1] eliminated 1 clauses out of 1 (100%) of length 27
c [cce-10-1] eliminated 1 clauses out of 1 (100%) of length 24
c [cce-10-1] eliminated 1 clauses out of 1 (100%) of length 21
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 16
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 13
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 12
c [cce-10-1] eliminated 5 clauses out of 41 (12%) of length 8
c [cce-10-1] eliminated 2 clauses out of 114 (2%) of length 7
c [cce-10-1] eliminated 7 clauses out of 455 (2%) of length 6
c [cce-10-1] eliminated 15 clauses out of 925 (2%) of length 5
c [cce-10-1] eliminated 40 clauses out of 2014 (2%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 77 large clauses in 9335097 steps
c [cce-10-1] allowing another 4667548 steps for small clauses
c [cce-10-1] scheduling 29633 clauses = 22681 binary + 6952 ternary
c [cce-10-1] tried to eliminate 29633 small clauses 100%
c [cce-10-1] eliminated 326 binary clauses 1%
c [cce-10-1] eliminated 42 ternary clauses 1%
c [cce-10-1] eliminated 368 small clauses 1%
c [cce-10-1] eliminated 368 small clauses in 141746029 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 445 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 4557471 steps for small clauses
c [cce-10-2] scheduling 29265 clauses = 22355 binary + 6910 ternary
c [cce-10-2] tried to eliminate 3863 small clauses 13%
c [cce-10-2] incomplete small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 445 covered clauses in TOTAL during 2 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 6951 variables 100%
c [elim-17] limit of 658630443 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 52 variables 1% in round 1 in 2465421 steps
c [elim-17-1] backward subsumption/strengthening limit 2465400
c [elim-17-1-1] backward checking 446 touched variables 6%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 1 clauses in 55879 steps
c [elim-17-1] rescheduled 12 variables 0% by backward subsumption
c [elim-17-2] eliminated 1 variables 0% in round 2 in 3391 steps
c [elim-17-2] backward subsumption/strengthening limit 3300
c [elim-17-2-1] backward checking 10 touched variables 0%
c [elim-17-2-1] incomplete backward checking 0 remain 0%
c [elim-17-2] subsumed 0 and strengthened 1 clauses in 3301 steps
c [elim-17-2] rescheduled 9 variables 0% by backward subsumption
c [elim-17-3] eliminated 1 variables 0% in round 3 in 3461 steps
c [elim-17-3] backward subsumption/strengthening limit 3400
c [elim-17-3-1] backward checking 11 touched variables 0%
c [elim-17-3-1] incomplete backward checking 0 remain 0%
c [elim-17-3] subsumed 0 and strengthened 0 clauses in 3401 steps
c [elim-17] fully completed in 3 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 54 = 1% variables out of 6951 scheduled
c [elim-17] 54 < 1/100 * 6951 = 69 considered unsuccessful
c [bca-15] limit of 10000000 steps and 79020 added (scaled 2)
c [bca-15] 11006 out of 13796 literals actually usable 80%
c [bca-15] added 4 blocked clauses in 42738 steps
c [sort-queue-19] sorted 1842 enqueued variables after 290742 conflicts
c [score-dist-19] active 5055 (73%), one 0 (0%), zero 1842 (27%)
c [score-dist-19] max exp 519, different 19 (4%)
c [score-dist-19] median active exp 513, avg 511.8
c [simplification-19] removed 57 variables 0.8% (6897 remain 4%)
c [simplification-19] removed 566 irredundant clauses 1.4% (39209 remain 5%)
c [simplification-19] maximum reduction of 1% = max (1%, 1%)
c [simplification-19] geometric conflict interval increment 36000 = 72000 / 2
c [simplification-19] new conflict interval 108000
c [simplification-19] penalized conflict interval 108000 = 1 * 108000
c [simplification-19] hard conflict limit 452742 (soft 398742 + delta 54000)
c [simplification-19] new conflict limit 398742 (hard 452742)
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  179.3    6896    39209    311294   37879    621 56976   33    43   33  77%    962  -21   19   44   43%
c i  179.3    6895    39209    311295   37879    621 56976   33    43   33  77%    959  -21   19   44   43%
c i  179.3    6894    39209    311296   37879    621 56976   33    43   33  77%    956  -21   19   44   43%
c i  179.3    6893    39209    311297   37879    621 56976   33    43   33  77%    953  -21   19   44   42%
c i  179.3    6892    39209    311298   37879    621 56976   33    43   33  77%    951  -21   19   44   42%
c i  179.3    6891    39209    311299   37879    621 56976   33    43   33  77%    948  -21   19   44   42%
c -  185.5    6891    39209    331708   27584    624 56977   35    47   24  74%  -1283  -14   33   42   78%
c -  195.5    6891    39209    364086   28410    625 56977   34    45   26  76%   -384  -11   36   39   92%
c -  206.3    6891    39209    397209   28927    626 56977   31    39   33  78%    175  -11   30   37   83%
c -  216.4    6891    39209    431352   28326    631 56980   30    35   31  84%    520   -9   29   33   87%
c 
c [simplification-20] limit 398792 conflicts (hard 452742) hit after 451926 conflicts
c [ternres-16] limit 48243091 with penalty 0 = 0 + 0
c [ternres-16] all 6891 free variables schedulable
c [ternres-16] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-52] removed 7 variables
c [basicprobe-7] limit 241215458 penalty 0 = 0 + 0
c [basicprobe-7-0] 549 sched 8%, 51 failed, 0 lifted, 1800 hbrs
c [decomp-53] removed 324 variables
c [basicprobe-7-1] 1628 sched 27%, 301 failed, 61 lifted, 10926 hbrs
c [decomp-54] removed 689 variables
c [basicprobe-7-2] 1327 sched 24%, 150 failed, 17 lifted, 17925 hbrs
c [decomp-55] removed 347 variables
c [basicprobe-7-3] 1306 sched 24%, 65 failed, 3 lifted, 9147 hbrs
c [decomp-56] removed 152 variables
c [basicprobe-7-4] 1291 sched 24%, 39 failed, 2 lifted, 2146 hbrs
c [decomp-57] removed 65 variables
c [basicprobe-7-5] 1278 sched 25%, 49 failed, 2 lifted, 2639 hbrs
c [decomp-58] removed 136 variables
c [basicprobe-7-6] 1249 sched 24%, 27 failed, 0 lifted, 4074 hbrs
c [decomp-59] removed 52 variables
c [basicprobe-7-7] 1242 sched 24%, 12 failed, 0 lifted, 1380 hbrs
c [decomp-60] removed 19 variables
c [basicprobe-7-8] 1248 sched 24%, 3 failed, 0 lifted, 235 hbrs
c [basicprobe-7-8] round limit 8 hit
c [basicprobe-7-8] 782 units = 697 failed (89%) + 85 lifted (11%)
c [basicprobe-7-8] removed 1787 variables, found 50272 hbrs
c [bate-5] eliminated 156 asymmetric tautologies during probing
c [unhide-17] limit 2412154 with penalty 2 = 2 + 0
c [unhide-17-44] 0 units, 0 failed, 8349 tauts, 0 hbrs, 74502 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 556 transitive binary clauses
c [cce-11] limit of 241215458 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 2 clauses out of 8 (25%) of length 10
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 9
c [cce-11-1] eliminated 2 clauses out of 18 (11%) of length 8
c [cce-11-1] eliminated 3 clauses out of 67 (4%) of length 7
c [cce-11-1] eliminated 10 clauses out of 229 (4%) of length 6
c [cce-11-1] eliminated 15 clauses out of 519 (3%) of length 5
c [cce-11-1] eliminated 35 clauses out of 1197 (3%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 68 large clauses in 4890052 steps
c [cce-11-1] allowing another 2445026 steps for small clauses
c [cce-11-1] scheduling 20816 clauses = 16578 binary + 4238 ternary
c [cce-11-1] tried to eliminate 20816 small clauses 100%
c [cce-11-1] eliminated 1289 binary clauses 8%
c [cce-11-1] eliminated 285 ternary clauses 7%
c [cce-11-1] eliminated 1574 small clauses 8%
c [cce-11-1] eliminated 1574 small clauses in 77224619 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 1642 covered clauses in round 1
c [cce-11-2] eliminated 2 clauses out of 219 (1%) of length 6
c [cce-11-2] eliminated 3 clauses out of 504 (1%) of length 5
c [cce-11-2] eliminated 5 clauses out of 1162 (0%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 10 large clauses in 4613136 steps
c [cce-11-2] allowing another 2306568 steps for small clauses
c [cce-11-2] scheduling 19245 clauses = 15289 binary + 3956 ternary
c [cce-11-2] tried to eliminate 19245 small clauses 100%
c [cce-11-2] eliminated 62 binary clauses 0%
c [cce-11-2] eliminated 38 ternary clauses 1%
c [cce-11-2] eliminated 100 small clauses 1%
c [cce-11-2] eliminated 100 small clauses in 72529088 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 110 covered clauses in round 2
c [cce-11-3] eliminated 2 clauses out of 501 (0%) of length 5
c [cce-11-3] eliminated 1 clauses out of 1157 (0%) of length 4
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] eliminated 3 large clauses in 4557539 steps
c [cce-11-3] allowing another 2278769 steps for small clauses
c [cce-11-3] scheduling 19145 clauses = 15227 binary + 3918 ternary
c [cce-11-3] tried to eliminate 19145 small clauses 100%
c [cce-11-3] eliminated 48 binary clauses 0%
c [cce-11-3] eliminated 10 ternary clauses 0%
c [cce-11-3] eliminated 58 small clauses 0%
c [cce-11-3] eliminated 58 small clauses in 71978883 steps
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 61 covered clauses in round 3
c [cce-11] eliminated 1813 covered clauses in TOTAL during 3 rounds
c [bca-16] limit of 10000000 steps and 51780 added (scaled 2)
c [bca-16] 7604 out of 10208 literals actually usable 74%
c [bca-16] added 9 blocked clauses in 62306 steps
c [sweep-10] limit 1809115 penalty 3 = 3 + 0
c [sweep-10-1] 249 pos 31.6% + 540 neg 68.4% = 789 sched 15.5% ret 4314
c [sweep-10-1] 1812417 steps 166 queries 20.07 avg class size
c [sweep-10-1] 825 decisions 165 SAT calls 21.79 avg env size
c [sweep-10-1] 348 variables remain 7% (4755 retained 93%)
c [decomp-61] removed 9 variables
c [sweep-10-1] removed 9 vars (0 failed, 0 eqs, 3 impls)
c [sweep-10] removed 9 vars in TOTAL (1 rounds, 165 queries)
c [sort-queue-20] sorted 1188 enqueued variables after 451926 conflicts
c [score-dist-20] active 3906 (77%), one 0 (0%), zero 1188 (23%)
c [score-dist-20] max exp 520, different 20 (4%)
c [score-dist-20] median active exp 514, avg 512.6
c [simplification-20] removed 1797 variables 26.1% (5094 remain 3%)
c [simplification-20] removed 13624 irredundant clauses 34.7% (25585 remain 3%)
c [simplification-20] maximum reduction of 35% = max (26%, 35%)
c [simplification-20] large reduction 35% >= 5% limit
c [simplification-20] next conflict interval 4519 = min (451926/100, 108000)
c [simplification-20] penalized conflict interval 4519 = 1 * 4519
c [simplification-20] hard conflict limit 466445 (soft 456445 + delta 10000)
c [simplification-20] new conflict limit 456445 (hard 466445)
c 
c [simplification-21] limit 456445 conflicts (hard 466445) hit after 456448 conflicts
c [ternres-17] limit 48591490 with penalty 0 = 0 + 0
c [ternres-17] all 5094 free variables schedulable
c [ternres-17] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 1518484 penalty 4 = 4 + 0
c [card-6] found 2079 at-most-one constraints of average size 3.5
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 1518484 for elimination
c [card-6] 2079 out of 2079 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] generated 502 at-most-one constraints, 473 used 94%
c [card-6] exported 5839 binary clauses, 12.3 per/constraint
c [simpleprobe-8] all 5094 free variables schedulable
c [simpleprobe-8] limit 194365960 penalty 0 = 0 + 0
c [decomp-63] removed 80 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 80 variables, found 3710 hbrs, 0 units
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 1072 transitive binary clauses
c [cce-12] limit of 242957450 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 4 clauses out of 1156 (0%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 4 large clauses in 4415509 steps
c [cce-12-1] allowing another 2207754 steps for small clauses
c [cce-12-1] scheduling 19584 clauses = 15105 binary + 4479 ternary
c [cce-12-1] tried to eliminate 19584 small clauses 100%
c [cce-12-1] eliminated 3 binary clauses 0%
c [cce-12-1] eliminated 45 ternary clauses 1%
c [cce-12-1] eliminated 48 small clauses 0%
c [cce-12-1] eliminated 48 small clauses in 73006658 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 52 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 2205349 steps for small clauses
c [cce-12-2] scheduling 19536 clauses = 15102 binary + 4434 ternary
c [cce-12-2] tried to eliminate 19536 small clauses 100%
c [cce-12-2] completed small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 52 covered clauses in TOTAL during 2 rounds
c [cce-12] 52 < 1/100 * 25465 = 254 considered unsuccessful
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 5014 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 8000000000 steps penalty 1 = 1 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 514 variables 10% in round 1 in 1544135 steps
c [elim-18-1] backward subsumption/strengthening limit 1544100
c [elim-18-1-1] backward checking 1683 touched variables 34%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 0 and strengthened 1 clauses in 160100 steps
c [elim-18-1] rescheduled 4 variables 0% by backward subsumption
c [elim-18-2] eliminated 1 variables 0% in round 2 in 775 steps
c [elim-18-2] backward subsumption/strengthening limit 700
c [elim-18-2-1] backward checking 10 touched variables 0%
c [elim-18-2-1] incomplete backward checking 0 remain 0%
c [elim-18-2] subsumed 0 and strengthened 0 clauses in 701 steps
c [elim-18-2] fully rescheduled 4499 variables 90%
c [elim-18-3] eliminated 2 variables 0% in round 3 in 1506950 steps
c [elim-18-3] backward subsumption/strengthening limit 1506900
c [elim-18-3-1] backward checking 14 touched variables 0%
c [elim-18-3-1] fully completed backward checking in 1 rounds
c [elim-18-3] subsumed 0 and strengthened 0 clauses in 7010 steps
c [elim-18] fully completed in 3 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 517 = 10% variables out of 5014 scheduled
c [bca-17] limit of 10000000 steps and 50208 added (scaled 2)
c [bca-17] 6740 out of 8996 literals actually usable 75%
c [bca-17] added 21 blocked clauses in 32240 steps
c [sort-queue-21] sorted 1054 enqueued variables after 456448 conflicts
c [score-dist-21] active 3443 (77%), one 0 (0%), zero 1054 (23%)
c [score-dist-21] max exp 520, different 20 (4%)
c [score-dist-21] median active exp 514, avg 512.9
c [simplification-21] removed 597 variables 11.7% (4497 remain 3%)
c [simplification-21] removed 785 irredundant clauses 3.1% (24800 remain 3%)
c [simplification-21] maximum reduction of 12% = max (12%, 3%)
c [simplification-21] large reduction 12% >= 5% limit
c [simplification-21] next conflict interval 4564 = min (456448/100, 108000)
c [simplification-21] penalized conflict interval 4564 = 1 * 4564
c [simplification-21] hard conflict limit 471012 (soft 461012 + delta 10000)
c [simplification-21] new conflict limit 461012 (hard 471012)
c 
c [simplification-22] limit 461012 conflicts (hard 471012) hit after 461016 conflicts
c [quatres-11] found 1443 quaternary clauses 41% in total
c [quatres-11-1] removed 1 duplicate quaternary clauses
c [quatres-11-2] added 6 quaternary resolvents
c [ternres-18] limit 48795657 with penalty 0 = 0 + 0
c [ternres-18] all 4497 free variables schedulable
c [ternres-18] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-18] fully completed ternary resolution
c [treelook-8] limit 4879565 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 8991 literals 100%
c [treelook-8] scheduling used 229406 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 4879565 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 4889434 steps
c [treelook-8] 8629 literals remain 96%
c [treelook-8] 4494 variables remain to probed next time 100%
c [treelook-8] removed 0 variables, found 22128 hbrs
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 1100 transitive binary clauses
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 4497 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 1 variables 0% in round 1 in 1505604 steps
c [elim-19-1] backward subsumption/strengthening limit 1505600
c [elim-19-1-1] backward checking 10 touched variables 0%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 0 and strengthened 0 clauses in 3122 steps
c [elim-19] fully completed in 1 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 1 = 0% variables out of 4497 scheduled
c [elim-19] 1 < 1/100 * 4497 = 44 considered unsuccessful
c [bca-18] limit of 10000000 steps and 50179 added (scaled 2)
c [bca-18] 6598 out of 8994 literals actually usable 73%
c [bca-18] added 2 blocked clauses in 36184 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 36596742 penalty 2 = 2 + 0
c [sweep-11-1] 94 pos 29.0% + 230 neg 71.0% = 324 sched 7.2% ret 4172
c [sweep-11-1] 1222051 steps 229 queries 9.10 avg class size
c [sweep-11-1] 1091 decisions 228 SAT calls 22.18 avg env size
c [sweep-11-1] fully completed sweeping round
c [sweep-11-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-11-2] 734 pos 16.3% + 3762 neg 83.7% = 4496 sched 100.0% ret 0
c [sweep-11-2] 10399536 steps 641 queries 19.22 avg class size
c [sweep-11-2] 5738 decisions 640 SAT calls 49.42 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-67] removed 3 variables
c [sweep-11-2] removed 3 vars (0 failed, 3 eqs, 4 impls)
c [sweep-11-3] 732 pos 16.3% + 3761 neg 83.7% = 4493 sched 100.0% ret 0
c [sweep-11-3] 10319366 steps 631 queries 12.42 avg class size
c [sweep-11-3] 5028 decisions 627 SAT calls 49.96 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-68] removed 17 variables
c [sweep-11-3] removed 17 vars (0 failed, 5 eqs, 6 impls)
c [sweep-11] removed 20 vars in TOTAL (3 rounds, 1498 queries)
c [sort-queue-22] sorted 958 enqueued variables after 461016 conflicts
c [score-dist-22] active 3518 (79%), one 0 (0%), zero 958 (21%)
c [score-dist-22] max exp 520, different 20 (4%)
c [score-dist-22] median active exp 514, avg 512.7
c [simplification-22] removed 21 variables 0.5% (4476 remain 3%)
c [simplification-22] removed 150 irredundant clauses 0.6% (24650 remain 3%)
c [simplification-22] maximum reduction of 1% = max (0%, 1%)
c [simplification-22] geometric conflict interval increment 54000 = 108000 / 2
c [simplification-22] new conflict interval 162000
c [simplification-22] penalized conflict interval 162000 = 1 * 162000
c [simplification-22] hard conflict limit 704016 (soft 623016 + delta 81000)
c [simplification-22] new conflict limit 623016 (hard 704016)
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 -  251.9    4476    24650    504743   29621    445 69713   31    38   22  83%    859   -3   29   31   92%
c -  261.3    4476    24650    542028   30814    445 69714   27    32   22  85%    931   -5   27   29   92%
c i  266.0    4475    24650    562832   50395    448 69716   31    47   33  66%    956    8   32   30  108%
c -  269.6    4475    24650    577081   30983    448 69716   31    47   30  67%  -2243    6   31   30  102%
c i  274.4    4474    24650    597152   50085    449 69718   31    45   47  69%  -1381    3   33   30  110%
c i  275.0    4473    24650    599381   52163    449 69718   32    45   47  71%  -1766    2   34   30  112%
c -  278.7    4473    24650    612687   30781    449 69718   33    49   29  67%  -1332    6   36   31  117%
c -  289.0    4473    24650    649696   31307    449 69722   36    49   30  73%   -316    3   50   33  149%
c 
c [simplification-23] limit 623016 conflicts (hard 704016) hit after 667557 conflicts
c [ternres-19] limit 66111201 with penalty 0 = 0 + 0
c [ternres-19] all 4473 free variables schedulable
c [ternres-19] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-69] removed 4 variables
c [basicprobe-8] limit 330556005 penalty 0 = 0 + 0
c [basicprobe-8-0] 1270 sched 29%, 63 failed, 1 lifted, 3399 hbrs
c [decomp-70] removed 79 variables
c [basicprobe-8-1] 1216 sched 28%, 38 failed, 1 lifted, 4955 hbrs
c [decomp-71] removed 49 variables
c [basicprobe-8-2] 1193 sched 28%, 16 failed, 0 lifted, 2431 hbrs
c [decomp-72] removed 18 variables
c [basicprobe-8-3] 1194 sched 28%, 5 failed, 0 lifted, 881 hbrs
c [decomp-73] removed 5 variables
c [basicprobe-8-4] 1198 sched 28%, 0 failed, 0 lifted, 121 hbrs
c [basicprobe-8-5] 1198 sched 28%, 0 failed, 0 lifted, 37 hbrs
c [basicprobe-8-6] 1198 sched 28%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-8-7] 1198 sched 28%, 0 failed, 0 lifted, 10 hbrs
c [basicprobe-8-8] 1198 sched 28%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-8-8] round limit 8 hit
c [basicprobe-8-8] 124 units = 122 failed (98%) + 2 lifted (2%)
c [basicprobe-8-8] removed 151 variables, found 11847 hbrs
c [bate-6] eliminated 35 asymmetric tautologies during probing
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 1106 transitive binary clauses
c [cce-13] boosting limit by 10
c [cce-13] limit of 1652780025 steps penalty 1 = 1 + 0
c [cce-13-1] eliminated 2 clauses out of 2 (100%) of length 25
c [cce-13-1] eliminated 1 clauses out of 1 (100%) of length 14
c [cce-13-1] eliminated 1 clauses out of 19 (5%) of length 8
c [cce-13-1] eliminated 2 clauses out of 209 (1%) of length 6
c [cce-13-1] eliminated 5 clauses out of 552 (1%) of length 5
c [cce-13-1] eliminated 32 clauses out of 1215 (3%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 43 large clauses in 5326531 steps
c [cce-13-1] allowing another 2663265 steps for small clauses
c [cce-13-1] scheduling 17679 clauses = 13579 binary + 4100 ternary
c [cce-13-1] tried to eliminate 17679 small clauses 100%
c [cce-13-1] eliminated 370 binary clauses 3%
c [cce-13-1] eliminated 154 ternary clauses 4%
c [cce-13-1] eliminated 524 small clauses 3%
c [cce-13-1] eliminated 524 small clauses in 66352104 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 567 covered clauses in round 1
c [cce-13-2] eliminated 1 clauses out of 207 (0%) of length 6
c [cce-13-2] eliminated 17 clauses out of 1183 (1%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 18 large clauses in 5093844 steps
c [cce-13-2] allowing another 2546922 steps for small clauses
c [cce-13-2] scheduling 17155 clauses = 13209 binary + 3946 ternary
c [cce-13-2] tried to eliminate 17155 small clauses 100%
c [cce-13-2] eliminated 21 binary clauses 0%
c [cce-13-2] eliminated 21 ternary clauses 1%
c [cce-13-2] eliminated 42 small clauses 0%
c [cce-13-2] eliminated 42 small clauses in 64074426 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 60 covered clauses in round 2
c [cce-13-3] eliminated 2 clauses out of 547 (0%) of length 5
c [cce-13-3] eliminated 1 clauses out of 1166 (0%) of length 4
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] eliminated 3 large clauses in 4960215 steps
c [cce-13-3] allowing another 2480107 steps for small clauses
c [cce-13-3] scheduling 17113 clauses = 13188 binary + 3925 ternary
c [cce-13-3] tried to eliminate 17113 small clauses 100%
c [cce-13-3] eliminated 5 binary clauses 0%
c [cce-13-3] eliminated 3 ternary clauses 0%
c [cce-13-3] eliminated 8 small clauses 0%
c [cce-13-3] eliminated 8 small clauses in 63650230 steps
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 11 covered clauses in round 3
c [cce-13] eliminated 638 covered clauses in TOTAL during 3 rounds
c [bca-19] limit of 10000000 steps and 46196 added (scaled 2)
c [bca-19] 6068 out of 8644 literals actually usable 70%
c [bca-19] added 2 blocked clauses in 61509 steps
c [sweep-12] limit 9916680 penalty 1 = 1 + 0
c [sweep-12-1] 799 pos 18.5% + 3522 neg 81.5% = 4321 sched 100.0% ret 0
c [sweep-12-1] 10439814 steps 205 queries 47.33 avg class size
c [sweep-12-1] 3743 decisions 201 SAT calls 113.12 avg env size
c [sweep-12-1] 995 variables remain 23% (3322 retained 77%)
c [decomp-78] removed 10 variables
c [sweep-12-1] removed 10 vars (0 failed, 6 eqs, 4 impls)
c [sweep-12] removed 10 vars in TOTAL (1 rounds, 204 queries)
c [sort-queue-23] sorted 840 enqueued variables after 667557 conflicts
c [score-dist-23] active 3471 (81%), one 0 (0%), zero 840 (19%)
c [score-dist-23] max exp 521, different 21 (4%)
c [score-dist-23] median active exp 514, avg 513.0
c [simplification-23] removed 162 variables 3.6% (4311 remain 2%)
c [simplification-23] removed 1902 irredundant clauses 7.7% (22748 remain 3%)
c [simplification-23] maximum reduction of 8% = max (4%, 8%)
c [simplification-23] large reduction 8% >= 5% limit
c [simplification-23] next conflict interval 6675 = min (667557/100, 162000)
c [simplification-23] penalized conflict interval 6675 = 1 * 6675
c [simplification-23] hard conflict limit 684232 (soft 674232 + delta 10000)
c [simplification-23] new conflict limit 674232 (hard 684232)
c 
c [simplification-24] limit 674232 conflicts (hard 684232) hit after 684237 conflicts
c [quatres-12] found 1312 quaternary clauses 33% in total
c [ternres-20] limit 67365965 with penalty 0 = 0 + 0
c [ternres-20] all 4311 free variables schedulable
c [ternres-20] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-20] fully completed ternary resolution
c [simpleprobe-9] all 4311 free variables schedulable
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-80] removed 36 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 36 variables, found 3143 hbrs, 14 units
c [unhide-18] limit 1684149 with penalty 3 = 3 + 0
c [unhide-18-46] 0 units, 0 failed, 11683 tauts, 0 hbrs, 195413 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 760 transitive binary clauses
c [cce-14] limit of 336829827 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 1 clauses out of 5 (20%) of length 10
c [cce-14-1] eliminated 2 clauses out of 521 (0%) of length 5
c [cce-14-1] eliminated 2 clauses out of 1132 (0%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 5 large clauses in 4671724 steps
c [cce-14-1] allowing another 2335862 steps for small clauses
c [cce-14-1] scheduling 16683 clauses = 13027 binary + 3656 ternary
c [cce-14-1] tried to eliminate 16683 small clauses 100%
c [cce-14-1] eliminated 30 binary clauses 0%
c [cce-14-1] eliminated 49 ternary clauses 1%
c [cce-14-1] eliminated 79 small clauses 0%
c [cce-14-1] eliminated 79 small clauses in 61430735 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 84 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 2325661 steps for small clauses
c [cce-14-2] scheduling 16604 clauses = 12997 binary + 3607 ternary
c [cce-14-2] tried to eliminate 16604 small clauses 100%
c [cce-14-2] completed small round (ATE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 84 covered clauses in TOTAL during 2 rounds
c [cce-14] 84 < 1/100 * 22527 = 225 considered unsuccessful
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 4275 variables 100%
c [elim-20] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 196 variables 5% in round 1 in 1363536 steps
c [elim-20-1] backward subsumption/strengthening limit 1363500
c [elim-20-1-1] backward checking 876 touched variables 20%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 1 and strengthened 1 clauses in 84371 steps
c [elim-20-1] rescheduled 10 variables 0% by backward subsumption
c [elim-20-2] no variable eliminated in round 2 in 2868 steps
c [elim-20] fully completed in 2 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 196 = 5% variables out of 4275 scheduled
c [bca-20] limit of 10000000 steps and 45177 added (scaled 2)
c [bca-20] 5706 out of 8160 literals actually usable 70%
c [bca-20] added 11 blocked clauses in 47447 steps
c [sweep-13] limit 20209789 penalty 0 = 0 + 0
c [sweep-13-1] 268 pos 29.3% + 647 neg 70.7% = 915 sched 22.4% ret 3164
c [sweep-13-1] 6295141 steps 421 queries 7.66 avg class size
c [sweep-13-1] 3080 decisions 420 SAT calls 37.82 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-81] removed 4 variables
c [sweep-13-1] removed 4 vars (0 failed, 3 eqs, 3 impls)
c [sweep-13-2] 655 pos 16.1% + 3420 neg 83.9% = 4075 sched 100.0% ret 0
c [sweep-13-2] 13924811 steps 422 queries 25.60 avg class size
c [sweep-13-2] 5899 decisions 417 SAT calls 73.91 avg env size
c [sweep-13-2] 249 variables remain 6% (3811 retained 94%)
c [decomp-82] removed 26 variables
c [sweep-13-2] removed 26 vars (0 failed, 12 eqs, 6 impls)
c [sweep-13] removed 30 vars in TOTAL (2 rounds, 841 queries)
c [sort-queue-24] sorted 798 enqueued variables after 684237 conflicts
c [score-dist-24] active 3251 (80%), one 0 (0%), zero 798 (20%)
c [score-dist-24] max exp 521, different 21 (4%)
c [score-dist-24] median active exp 514, avg 513.1
c [simplification-24] removed 262 variables 6.1% (4049 remain 2%)
c [simplification-24] removed 665 irredundant clauses 2.9% (22083 remain 3%)
c [simplification-24] maximum reduction of 6% = max (6%, 3%)
c [simplification-24] large reduction 6% >= 5% limit
c [simplification-24] next conflict interval 6842 = min (684237/100, 162000)
c [simplification-24] penalized conflict interval 6842 = 1 * 6842
c [simplification-24] hard conflict limit 701079 (soft 691079 + delta 10000)
c [simplification-24] new conflict limit 691079 (hard 701079)
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  312.9    4048    22083    684816   35972    511 55259   29    40   28  73%    240   -5   27   32   82%
c i  313.1    4043    22083    686244   37315    512 55259   28    40   28  71%   -734   -6   25   32   78%
c i  313.1    4042    22083    686440   37505    512 55259   28    40   28  70%   -790   -6   24   32   76%
c i  315.1    4041    22083    696665   47048    512 55261   30    43   28  70%   -784   -2   30   32   94%
c 
c [simplification-25] limit 691079 conflicts (hard 701079) hit after 701081 conflicts
c [ternres-21] limit 68452703 with penalty 0 = 0 + 0
c [ternres-21] all 4041 free variables schedulable
c [ternres-21] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-21] fully completed ternary resolution
c [gauss-6] limit 855658 penalty 4 = 4 + 0
c [gauss-6] extracted 35 xors of average arity 2.8
c [gauss-6] connected 97 occurrences of 39 variables (average 2.5)
c [gauss-6] limit 855658 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-83] removed 1 variables
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 638 transitive binary clauses
c [transred-21] found 5 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 4035 variables 100%
c [block-6] limit of 42782939 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 8 blocked clauses
c [block-6] 8 < 1/100 * 21981 = 219 considered unsuccessful
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 4035 variables 100%
c [elim-21] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-21] rescheduling of touched variables disabled
c [elim-21-1] eliminated 46 variables 1% in round 1 in 1328078 steps
c [elim-21-1] backward subsumption/strengthening limit 1328000
c [elim-21-1-1] backward checking 261 touched variables 6%
c [elim-21-1-1] fully completed backward checking in 1 rounds
c [elim-21-1] subsumed 0 and strengthened 1 clauses in 29287 steps
c [elim-21-1] rescheduled 6 variables 0% by backward subsumption
c [elim-21-2] no variable eliminated in round 2 in 2159 steps
c [elim-21] fully completed in 2 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 46 = 1% variables out of 4035 scheduled
c [bca-21] limit of 10000000 steps and 44346 added (scaled 2)
c [bca-21] 5452 out of 7980 literals actually usable 68%
c [bca-21] added 4 blocked clauses in 61960 steps
c [sweep-14] limit 20535811 penalty 0 = 0 + 0
c [sweep-14-1] 78 pos 31.7% + 168 neg 68.3% = 246 sched 6.2% ret 3743
c [sweep-14-1] 1559810 steps 165 queries 6.90 avg class size
c [sweep-14-1] 818 decisions 162 SAT calls 23.88 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-84] removed 2 variables
c [sweep-14-1] removed 2 vars (0 failed, 3 eqs, 1 impls)
c [sweep-14-2] 642 pos 16.1% + 3345 neg 83.9% = 3987 sched 100.0% ret 0
c [sweep-14-2] 18979585 steps 440 queries 20.83 avg class size
c [sweep-14-2] 6394 decisions 437 SAT calls 72.55 avg env size
c [sweep-14-2] 177 variables remain 4% (3803 retained 96%)
c [decomp-85] removed 12 variables
c [sweep-14-2] removed 12 vars (0 failed, 3 eqs, 4 impls)
c [sweep-14] removed 14 vars in TOTAL (2 rounds, 603 queries)
c [sort-queue-25] sorted 766 enqueued variables after 701081 conflicts
c [score-dist-25] active 3209 (81%), one 0 (0%), zero 766 (19%)
c [score-dist-25] max exp 521, different 21 (4%)
c [score-dist-25] median active exp 514, avg 513.0
c [simplification-25] removed 66 variables 1.6% (3975 remain 2%)
c [simplification-25] removed 302 irredundant clauses 1.4% (21781 remain 3%)
c [simplification-25] maximum reduction of 2% = max (2%, 1%)
c [simplification-25] geometric conflict interval increment 54000 = 162000 / 3
c [simplification-25] new conflict interval 216000
c [simplification-25] penalized conflict interval 216000 = 1 * 216000
c [simplification-25] hard conflict limit 1025081 (soft 917081 + delta 108000)
c [simplification-25] new conflict limit 917081 (hard 1025081)
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  319.1    3974    21781    707681   56841    518 54014   26    38   40  67%   -641   -6   19   31   59%
c -  322.1    3974    21781    718743   31723    520 54014   21    30   23  70%   -530  -13   17   30   57%
c -  330.9    3974    21781    757752   32885    522 54014   23    32   24  72%    167   -7   24   27   88%
c -  340.2    3974    21781    797660   33644    525 54014   23    32   23  74%    558   -4   25   26   97%
c i  342.8    3973    21781    810183   45010    525 54014   26    33   31  80%    639   -2   28   26  107%
c -  350.1    3973    21781    837968   32792    528 54015   23    32   24  71%   -293   -2   24   25   93%
c -  359.7    3973    21781    879479   34681    532 54017   20    28   23  72%    325   -5   18   24   75%
c i  361.5    3972    21781    886857   41446    535 54017   18    25   29  71%    399   -8   13   23   54%
c i  366.5    3971    21781    907745   60112    542 54020   23    32   50  72%   -315    1   26   22  117%
c -  370.1    3971    21781    921634   35272    542 54020   22    29   32  76%   -327   -1   20   22   90%
c i  371.2    3970    21781    926404   39734    542 54020   24    32   38  75%   -233    2   30   22  135%
c 
c [simplification-26] limit 917081 conflicts (hard 1025081) hit after 954760 conflicts
c [ternres-22] limit 90085350 with penalty 0 = 0 + 0
c [ternres-22] all 3955 free variables schedulable
c [ternres-22] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-22] fully completed ternary resolution
c [decomp-86] removed 21 variables
c [treelook-9] limit 4504267 penalty 1 = 1 + 0 boost 1
c [treelook-9] scheduled 7906 literals 100%
c [treelook-9] scheduling used 319909 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 4504267 penalty 1 = 1 + 0 boost 1
c [treelook-9] used 4514656 steps
c [treelook-9] 7480 literals remain 95%
c [treelook-9] 3944 variables remain to probed next time 100%
c [treelook-9] removed 8 variables, found 18730 hbrs
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 754 transitive binary clauses
c [transred-22] found 3 units
c [cce-15] limit of 225213375 steps penalty 1 = 1 + 0
c [cce-15-1] eliminated 1 clauses out of 1 (100%) of length 20
c [cce-15-1] eliminated 1 clauses out of 2 (50%) of length 13
c [cce-15-1] eliminated 1 clauses out of 2 (50%) of length 12
c [cce-15-1] eliminated 1 clauses out of 8 (12%) of length 10
c [cce-15-1] eliminated 1 clauses out of 17 (6%) of length 8
c [cce-15-1] eliminated 1 clauses out of 69 (1%) of length 7
c [cce-15-1] eliminated 5 clauses out of 207 (2%) of length 6
c [cce-15-1] eliminated 17 clauses out of 518 (3%) of length 5
c [cce-15-1] eliminated 40 clauses out of 1071 (4%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 68 large clauses in 5019886 steps
c [cce-15-1] allowing another 2509943 steps for small clauses
c [cce-15-1] scheduling 16153 clauses = 12373 binary + 3780 ternary
c [cce-15-1] tried to eliminate 16153 small clauses 100%
c [cce-15-1] eliminated 308 binary clauses 2%
c [cce-15-1] eliminated 84 ternary clauses 2%
c [cce-15-1] eliminated 392 small clauses 2%
c [cce-15-1] eliminated 415 small clauses in 60208972 steps
c [cce-15-1] completed small round (ACCE)
c [cce-15-1] eliminated 483 covered clauses in round 1
c [cce-15-2] eliminated 4 clauses out of 501 (1%) of length 5
c [cce-15-2] completed large round (ACCE)
c [cce-15-2] eliminated 4 large clauses in 4681710 steps
c [cce-15-2] allowing another 2340855 steps for small clauses
c [cce-15-2] scheduling 15761 clauses = 12065 binary + 3696 ternary
c [cce-15-2] tried to eliminate 15761 small clauses 100%
c [cce-15-2] eliminated 17 binary clauses 0%
c [cce-15-2] eliminated 12 ternary clauses 0%
c [cce-15-2] eliminated 29 small clauses 0%
c [cce-15-2] eliminated 29 small clauses in 57673890 steps
c [cce-15-2] completed small round (ACCE)
c [cce-15-2] eliminated 33 covered clauses in round 2
c [cce-15-3] eliminated 1 clauses out of 68 (1%) of length 7
c [cce-15-3] eliminated 1 clauses out of 497 (0%) of length 5
c [cce-15-3] completed large round (ACCE)
c [cce-15-3] eliminated 2 large clauses in 4649553 steps
c [cce-15-3] allowing another 2324776 steps for small clauses
c [cce-15-3] scheduling 15732 clauses = 12048 binary + 3684 ternary
c [cce-15-3] tried to eliminate 15732 small clauses 100%
c [cce-15-3] eliminated 3 binary clauses 0%
c [cce-15-3] eliminated 3 small clauses 0%
c [cce-15-3] eliminated 3 small clauses in 57401326 steps
c [cce-15-3] completed small round (ACCE)
c [cce-15-3] eliminated 5 covered clauses in round 3
c [cce-15] eliminated 521 covered clauses in TOTAL during 3 rounds
c [elim-22] scheduling all variables this time
c [elim-22] scheduled 3943 variables 100%
c [elim-22] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-22] rescheduling of touched variables disabled
c [elim-22-1] eliminated 71 variables 2% in round 1 in 1270379 steps
c [elim-22-1] backward subsumption/strengthening limit 1270300
c [elim-22-1-1] backward checking 415 touched variables 11%
c [elim-22-1-1] fully completed backward checking in 1 rounds
c [elim-22-1] subsumed 3 and strengthened 3 clauses in 40144 steps
c [elim-22-1] rescheduled 11 variables 0% by backward subsumption
c [elim-22-2] eliminated 1 variables 0% in round 2 in 5737 steps
c [elim-22-2] backward subsumption/strengthening limit 5700
c [elim-22-2-1] backward checking 10 touched variables 0%
c [elim-22-2-1] fully completed backward checking in 1 rounds
c [elim-22-2] subsumed 0 and strengthened 0 clauses in 3468 steps
c [elim-22] fully completed in 2 rounds
c [elim-22] transition to [ all 0 rem 0 ] state
c [elim-22] eliminated 72 = 2% variables out of 3943 scheduled
c [bca-22] limit of 10000000 steps and 42598 added (scaled 2)
c [bca-22] 5293 out of 7744 literals actually usable 68%
c [bca-22] added 5 blocked clauses in 69882 steps
c [sweep-15] limit 27025605 penalty 0 = 0 + 0
c [sweep-15-1] 27 pos 16.1% + 141 neg 83.9% = 168 sched 4.3% ret 3703
c [sweep-15-1] 601613 steps 125 queries 7.56 avg class size
c [sweep-15-1] 543 decisions 124 SAT calls 22.51 avg env size
c [sweep-15-1] fully completed sweeping round
c [sweep-15-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-15-2] 604 pos 15.6% + 3267 neg 84.4% = 3871 sched 100.0% ret 0
c [sweep-15-2] 13981480 steps 548 queries 14.41 avg class size
c [sweep-15-2] 6934 decisions 539 SAT calls 57.11 avg env size
c [sweep-15-2] fully completed sweeping round
c [decomp-89] removed 16 variables
c [sweep-15-2] removed 16 vars (0 failed, 9 eqs, 6 impls)
c [sweep-15-3] 602 pos 15.6% + 3253 neg 84.4% = 3855 sched 100.0% ret 0
c [sweep-15-3] 12487910 steps 300 queries 22.58 avg class size
c [sweep-15-3] 5737 decisions 291 SAT calls 87.94 avg env size
c [sweep-15-3] 487 variables remain 13% (3365 retained 87%)
c [decomp-90] removed 10 variables
c [sweep-15-3] removed 10 vars (0 failed, 8 eqs, 10 impls)
c [sweep-15] removed 26 vars in TOTAL (3 rounds, 970 queries)
c [sort-queue-26] sorted 685 enqueued variables after 954760 conflicts
c [score-dist-26] active 3160 (82%), one 0 (0%), zero 685 (18%)
c [score-dist-26] max exp 521, different 21 (4%)
c [score-dist-26] median active exp 514, avg 513.3
c [simplification-26] removed 110 variables 2.8% (3845 remain 2%)
c [simplification-26] removed 900 irredundant clauses 4.1% (20881 remain 3%)
c [simplification-26] maximum reduction of 4% = max (3%, 4%)
c [simplification-26] geometric conflict interval increment 43200 = 216000 / 5
c [simplification-26] new conflict interval 259200
c [simplification-26] penalized conflict interval 259200 = 1 * 259200
c [simplification-26] hard conflict limit 1343560 (soft 1213960 + delta 129600)
c [simplification-26] new conflict limit 1213960 (hard 1343560)
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  384.6    3844    20881    955690   59941    589 69323   25    32   40  77%     31    1   23   23  100%
c i  385.1    3843    20881    957561   61531    591 69323   24    30   40  79%   -318   -1   22   23   97%
c -  388.2    3843    20881    971611   35432    592 69324   22    28   25  81%   -144   -3   25   23  111%
c i  389.0    3842    20881    975255   38331    617 69330   18    22   30  81%    -80   -8    6   22   27%
c i  397.1    3814    20881   1012486   72819    656 69338   26    35   43  75%    239    9   30   20  148%
c -  398.3    3814    20881   1016267   37855    657 69338   24    33   25  72%   -260    6   22   20  111%
c i  400.0    3813    20881   1024039   45176    664 69338   22    30   31  73%   -129    3   20   20   97%
c -  409.1    3813    20881   1058869   38083    678 69341   27    38   25  70%    238    8   24   22  111%
c -  420.4    3813    20881   1102234   37646    682 69342   33    42   25  77%    619   11   40   24  168%
c -  432.6    3813    20881   1147323   38477    690 69343   24    32   25  75%    820   -4   25   27   96%
c -  445.4    3813    20881   1192970   39723    692 69343   42    53   26  80%    922   11   39   32  122%
c 
c [simplification-27] limit 1213960 conflicts (hard 1343560) hit after 1213964 conflicts
c [quatres-13] found 1391 quaternary clauses 22% in total
c [quatres-13-2] added 1 single-self-subsuming ternary resolvents
c [quatres-13-2] added 4 quaternary resolvents
c [ternres-23] limit 114886622 with penalty 0 = 0 + 0
c [ternres-23] all 3813 free variables schedulable
c [ternres-23] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-23] fully completed ternary resolution
c [decomp-91] removed 32 variables
c [basicprobe-9] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-9-0] 1054 sched 28%, 87 failed, 6 lifted, 7904 hbrs
c [decomp-92] removed 102 variables
c [basicprobe-9-1] 1010 sched 27%, 31 failed, 1 lifted, 4311 hbrs
c [decomp-93] removed 33 variables
c [basicprobe-9-2] 1001 sched 27%, 11 failed, 0 lifted, 1124 hbrs
c [decomp-94] removed 12 variables
c [basicprobe-9-3] 1006 sched 27%, 5 failed, 1 lifted, 223 hbrs
c [decomp-95] removed 6 variables
c [basicprobe-9-4] 1010 sched 28%, 1 failed, 0 lifted, 58 hbrs
c [decomp-96] removed 1 variables
c [basicprobe-9-5] 1012 sched 28%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-9-6] 1012 sched 28%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-9-7] 1012 sched 28%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-9-8] 1012 sched 28%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-9-8] round limit 8 hit
c [basicprobe-9-8] 143 units = 135 failed (94%) + 8 lifted (6%)
c [basicprobe-9-8] removed 154 variables, found 13653 hbrs
c [bate-7] eliminated 43 asymmetric tautologies during probing
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 818 transitive binary clauses
c [cce-16] limit of 574433112 steps penalty 0 = 0 + 0
c [cce-16-1] eliminated 1 clauses out of 3 (33%) of length 12
c [cce-16-1] eliminated 1 clauses out of 58 (2%) of length 7
c [cce-16-1] eliminated 3 clauses out of 175 (2%) of length 6
c [cce-16-1] eliminated 5 clauses out of 442 (1%) of length 5
c [cce-16-1] eliminated 3 clauses out of 951 (0%) of length 4
c [cce-16-1] completed large round (ATE)
c [cce-16-1] eliminated 13 large clauses in 3846417 steps
c [cce-16-1] allowing another 1923208 steps for small clauses
c [cce-16-1] scheduling 14757 clauses = 11615 binary + 3142 ternary
c [cce-16-1] tried to eliminate 14757 small clauses 100%
c [cce-16-1] eliminated 360 binary clauses 3%
c [cce-16-1] eliminated 19 ternary clauses 1%
c [cce-16-1] eliminated 379 small clauses 3%
c [cce-16-1] eliminated 379 small clauses in 47979503 steps
c [cce-16-1] completed small round (ATE)
c [cce-16-1] eliminated 392 covered clauses in round 1
c [cce-16-2] completed large round (ATE)
c [cce-16-2] allowing another 1913569 steps for small clauses
c [cce-16-2] scheduling 14378 clauses = 11255 binary + 3123 ternary
c [cce-16-2] tried to eliminate 14378 small clauses 100%
c [cce-16-2] completed small round (ATE)
c [cce-16-2] eliminated 0 covered clauses in round 2
c [cce-16] eliminated 392 covered clauses in TOTAL during 2 rounds
c [elim-23] scheduling all variables this time
c [elim-23] scheduled 3659 variables 100%
c [elim-23] almost no limit of 100000000000 steps
c [elim-23] rescheduling of touched variables disabled
c [elim-23-1] eliminated 148 variables 4% in round 1 in 1147698 steps
c [elim-23-1] backward subsumption/strengthening limit 1147600
c [elim-23-1-1] backward checking 791 touched variables 22%
c [elim-23-1-1] fully completed backward checking in 1 rounds
c [elim-23-1] subsumed 1 and strengthened 3 clauses in 80260 steps
c [elim-23-1] rescheduled 37 variables 1% by backward subsumption
c [elim-23-2] eliminated 1 variables 0% in round 2 in 12643 steps
c [elim-23-2] backward subsumption/strengthening limit 12600
c [elim-23-2-1] backward checking 5 touched variables 0%
c [elim-23-2-1] fully completed backward checking in 1 rounds
c [elim-23-2] subsumed 0 and strengthened 0 clauses in 4043 steps
c [elim-23] fully completed in 2 rounds
c [elim-23] transition to [ all 0 rem 0 ] state
c [elim-23] eliminated 149 = 4% variables out of 3659 scheduled
c [bca-23] limit of 10000000 steps and 38387 added (scaled 2)
c [bca-23] 4676 out of 7022 literals actually usable 67%
c [bca-23] added 18 blocked clauses in 50329 steps
c [sweep-16] limit 34465986 penalty 0 = 0 + 0
c [sweep-16-1] 97 pos 20.9% + 367 neg 79.1% = 464 sched 13.2% ret 3046
c [sweep-16-1] 2748553 steps 269 queries 7.11 avg class size
c [sweep-16-1] 1690 decisions 267 SAT calls 31.51 avg env size
c [sweep-16-1] fully completed sweeping round
c [sweep-16-1] removed 0 vars (0 failed, 1 eqs, 0 impls)
c [sweep-16-2] 503 pos 14.3% + 3007 neg 85.7% = 3510 sched 100.0% ret 0
c [sweep-16-2] 13104371 steps 508 queries 13.37 avg class size
c [sweep-16-2] 6491 decisions 506 SAT calls 57.89 avg env size
c [sweep-16-2] fully completed sweeping round
c [decomp-101] removed 1 variables
c [sweep-16-2] removed 1 vars (0 failed, 2 eqs, 1 impls)
c [sweep-16-3] 503 pos 14.3% + 3006 neg 85.7% = 3509 sched 100.0% ret 0
c [sweep-16-3] 14121713 steps 511 queries 12.25 avg class size
c [sweep-16-3] 6227 decisions 508 SAT calls 62.28 avg env size
c [sweep-16-3] fully completed sweeping round
c [decomp-102] removed 5 variables
c [sweep-16-3] removed 5 vars (0 failed, 6 eqs, 3 impls)
c [sweep-16] removed 6 vars in TOTAL (3 rounds, 1285 queries)
c [sort-queue-27] sorted 515 enqueued variables after 1213964 conflicts
c [score-dist-27] active 2989 (85%), one 0 (0%), zero 515 (15%)
c [score-dist-27] max exp 521, different 21 (4%)
c [score-dist-27] median active exp 515, avg 513.7
c [simplification-27] removed 309 variables 8.1% (3504 remain 2%)
c [simplification-27] removed 2012 irredundant clauses 9.6% (18869 remain 2%)
c [simplification-27] maximum reduction of 10% = max (8%, 10%)
c [simplification-27] large reduction 10% >= 5% limit
c [simplification-27] next conflict interval 12139 = min (1213964/100, 259200)
c [simplification-27] penalized conflict interval 12139 = 1 * 12139
c [simplification-27] hard conflict limit 1236103 (soft 1226103 + delta 10000)
c [simplification-27] new conflict limit 1226103 (hard 1236103)
c 
c [simplification-28] limit 1226103 conflicts (hard 1236103) hit after 1226104 conflicts
c [ternres-24] limit 115921618 with penalty 0 = 0 + 0
c [ternres-24] all 3504 free variables schedulable
c [ternres-24] 8 ternary resolvents (0 bin, 8 trn)
c [ternres-24] fully completed ternary resolution
c [card-7] limit 3622550 penalty 4 = 4 + 0
c [card-7] found 1716 at-most-one constraints of average size 3.6
c [card-7] found 23 at-most-two constraints of average size 4.0
c [card-7] using previous limit 3622550 for elimination
c [card-7] 1738 out of 1739 constraints (100%) meet size limits
c [card-7] no units found
c [card-7] generated 3423 at-most-one constraints, 2768 used 81%
c [card-7] exported 18720 binary clauses, 6.8 per/constraint
c [simpleprobe-10] all 3504 free variables schedulable
c [simpleprobe-10] limit 200000000 penalty 0 = 0 + 0
c [decomp-104] removed 1 variables
c [simpleprobe-10] fully completed simple probing
c [simpleprobe-10] removed 1 variables, found 4602 hbrs, 1 units
c [transred-24] limit 2000000 with penalty 0 = 0 + 0
c [transred-24] removed 1380 transitive binary clauses
c [cce-17] limit of 579608092 steps penalty 0 = 0 + 0
c [cce-17-1] eliminated 2 clauses out of 3 (67%) of length 26
c [cce-17-1] eliminated 2 clauses out of 2 (100%) of length 25
c [cce-17-1] eliminated 1 clauses out of 1 (100%) of length 20
c [cce-17-1] eliminated 1 clauses out of 1 (100%) of length 18
c [cce-17-1] eliminated 1 clauses out of 1 (100%) of length 17
c [cce-17-1] eliminated 1 clauses out of 2 (50%) of length 15
c [cce-17-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-17-1] eliminated 1 clauses out of 5 (20%) of length 11
c [cce-17-1] eliminated 2 clauses out of 26 (8%) of length 8
c [cce-17-1] eliminated 1 clauses out of 58 (2%) of length 7
c [cce-17-1] eliminated 3 clauses out of 196 (2%) of length 6
c [cce-17-1] eliminated 5 clauses out of 463 (1%) of length 5
c [cce-17-1] eliminated 16 clauses out of 995 (2%) of length 4
c [cce-17-1] completed large round (ACCE)
c [cce-17-1] eliminated 37 large clauses in 4627456 steps
c [cce-17-1] allowing another 2313728 steps for small clauses
c [cce-17-1] scheduling 13944 clauses = 10981 binary + 2963 ternary
c [cce-17-1] tried to eliminate 13944 small clauses 100%
c [cce-17-1] eliminated 131 binary clauses 1%
c [cce-17-1] eliminated 100 ternary clauses 3%
c [cce-17-1] eliminated 231 small clauses 2%
c [cce-17-1] eliminated 231 small clauses in 47579616 steps
c [cce-17-1] completed small round (ACCE)
c [cce-17-1] eliminated 268 covered clauses in round 1
c [cce-17-2] eliminated 1 clauses out of 1 (100%) of length 15
c [cce-17-2] eliminated 1 clauses out of 193 (1%) of length 6
c [cce-17-2] eliminated 3 clauses out of 979 (0%) of length 4
c [cce-17-2] completed large round (ACCE)
c [cce-17-2] eliminated 5 large clauses in 4481799 steps
c [cce-17-2] allowing another 2240899 steps for small clauses
c [cce-17-2] scheduling 13713 clauses = 10850 binary + 2863 ternary
c [cce-17-2] tried to eliminate 13713 small clauses 100%
c [cce-17-2] eliminated 15 binary clauses 0%
c [cce-17-2] eliminated 5 ternary clauses 0%
c [cce-17-2] eliminated 20 small clauses 0%
c [cce-17-2] eliminated 20 small clauses in 46328860 steps
c [cce-17-2] completed small round (ACCE)
c [cce-17-2] eliminated 25 covered clauses in round 2
c [cce-17-3] eliminated 1 clauses out of 458 (0%) of length 5
c [cce-17-3] eliminated 1 clauses out of 976 (0%) of length 4
c [cce-17-3] completed large round (ACCE)
c [cce-17-3] eliminated 2 large clauses in 4455994 steps
c [cce-17-3] allowing another 2227997 steps for small clauses
c [cce-17-3] scheduling 13693 clauses = 10835 binary + 2858 ternary
c [cce-17-3] tried to eliminate 13693 small clauses 100%
c [cce-17-3] eliminated 1 binary clauses 0%
c [cce-17-3] eliminated 1 small clauses 0%
c [cce-17-3] eliminated 1 small clauses in 46183410 steps
c [cce-17-3] completed small round (ACCE)
c [cce-17-3] eliminated 3 covered clauses in round 3
c [cce-17] eliminated 296 covered clauses in TOTAL during 3 rounds
c [elim-24] scheduling all variables this time
c [elim-24] scheduled 3503 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 37 variables 1% in round 1 in 1108786 steps
c [elim-24-1] backward subsumption/strengthening limit 1108700
c [elim-24-1-1] backward checking 280 touched variables 8%
c [elim-24-1-1] fully completed backward checking in 1 rounds
c [elim-24-1] subsumed 0 and strengthened 2 clauses in 26105 steps
c [elim-24-1] rescheduled 5 variables 0% by backward subsumption
c [elim-24-2] no variable eliminated in round 2 in 2208 steps
c [elim-24] fully completed in 2 rounds
c [elim-24] transition to [ all 0 rem 0 ] state
c [elim-24] eliminated 37 = 1% variables out of 3503 scheduled
c [bca-24] limit of 10000000 steps and 37654 added (scaled 2)
c [bca-24] 4411 out of 6934 literals actually usable 64%
c [bca-24] added 4 blocked clauses in 62469 steps
c [sweep-17] limit 34776485 penalty 0 = 0 + 0
c [sweep-17-1] 465 pos 13.4% + 3001 neg 86.6% = 3466 sched 100.0% ret 0
c [sweep-17-1] 24517511 steps 488 queries 14.90 avg class size
c [sweep-17-1] 7479 decisions 487 SAT calls 79.51 avg env size
c [sweep-17-1] fully completed sweeping round
c [sweep-17-1] removed 0 vars (0 failed, 1 eqs, 0 impls)
c [sweep-17-2] 465 pos 13.4% + 3001 neg 86.6% = 3466 sched 100.0% ret 0
c [sweep-17-2] 11028517 steps 71 queries 74.58 avg class size
c [sweep-17-2] 2908 decisions 70 SAT calls 205.84 avg env size
c [sweep-17-2] 1335 variables remain 39% (2129 retained 61%)
c [decomp-106] removed 2 variables
c [sweep-17-2] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-17] 2 < 1/1000 * 3466 = 3 considered unsuccessful
c [sweep-17] removed 2 vars in TOTAL (2 rounds, 557 queries)
c [sort-queue-28] sorted 497 enqueued variables after 1226104 conflicts
c [score-dist-28] active 2967 (86%), one 0 (0%), zero 497 (14%)
c [score-dist-28] max exp 521, different 21 (4%)
c [score-dist-28] median active exp 515, avg 513.7
c [simplification-28] removed 40 variables 1.1% (3464 remain 2%)
c [simplification-28] removed 372 irredundant clauses 2.0% (18497 remain 2%)
c [simplification-28] maximum reduction of 2% = max (1%, 2%)
c [simplification-28] geometric conflict interval increment 86400 = 259200 / 3
c [simplification-28] new conflict interval 345600
c [simplification-28] penalized conflict interval 345600 = 1 * 345600
c [simplification-28] hard conflict limit 1744504 (soft 1571704 + delta 172800)
c [simplification-28] new conflict limit 1571704 (hard 1744504)
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 -  475.0    3464    18497   1256142   39917    576 81099   33    42   25  79%    985   -2   28   33   85%
c -  487.0    3464    18497   1303726   41371    580 81099   26    33   26  81%   1005   -6   25   30   83%
c -  498.8    3464    18497   1350236   42296    584 81099   26    35   26  74%   1015   -2   30   29  105%
c -  511.3    3464    18497   1397636   42023    587 81100   27    32   25  84%   1020   -3   27   27   98%
c -  523.5    3464    18497   1446806   42798    591 81105   26    31   26  83%   1022   -3   19   27   71%
c -  534.3    3464    18497   1495589   43009    597 81105   17    24   35  72%   1023   -8   13   24   52%
c -  546.2    3464    18497   1545897   44163    601 81106   21    26   36  82%   1024   -1   27   21  130%
c 
c [simplification-29] limit 1571704 conflicts (hard 1744504) hit after 1571706 conflicts
c [quatres-14] found 1491 quaternary clauses 20% in total
c [quatres-14-2] added 1 quaternary resolvents
c [ternres-25] limit 151459965 with penalty 0 = 0 + 0
c [ternres-25] all 3464 free variables schedulable
c [ternres-25] 11 ternary resolvents (1 bin, 10 trn)
c [ternres-25] fully completed ternary resolution
c [treelook-10] limit 15145996 penalty 0 = 0 + 0 boost 1
c [treelook-10] scheduled 6927 literals 100%
c [treelook-10] scheduling used 381437 steps
c [treelook-10] scheduled completely
c [treelook-10] limit 15145996 penalty 0 = 0 + 0 boost 1
c [treelook-10] used 15153787 steps
c [treelook-10] 4439 literals remain 64%
c [treelook-10] 3112 variables remain to probed next time 90%
c [treelook-10] removed 19 variables, found 43738 hbrs
c [unhide-19] limit 1250000 with penalty 4 = 4 + 0
c [unhide-19-48] 0 units, 1 failed, 27070 tauts, 0 hbrs, 149582 literals
c [transred-25] limit 2000000 with penalty 0 = 0 + 0
c [transred-25] removed 940 transitive binary clauses
c [cce-18] almost no limit of 4000000000 steps
c [cce-18-1] eliminated 1 clauses out of 1 (100%) of length 18
c [cce-18-1] eliminated 1 clauses out of 1 (100%) of length 16
c [cce-18-1] eliminated 3 clauses out of 957 (0%) of length 4
c [cce-18-1] completed large round (ATE)
c [cce-18-1] eliminated 5 large clauses in 4178484 steps
c [cce-18-1] allowing another 2089242 steps for small clauses
c [cce-18-1] scheduling 13604 clauses = 10832 binary + 2772 ternary
c [cce-18-1] tried to eliminate 13604 small clauses 100%
c [cce-18-1] eliminated 82 binary clauses 1%
c [cce-18-1] eliminated 8 ternary clauses 0%
c [cce-18-1] eliminated 90 small clauses 1%
c [cce-18-1] eliminated 90 small clauses in 44005172 steps
c [cce-18-1] completed small round (ATE)
c [cce-18-1] eliminated 95 covered clauses in round 1
c [cce-18-2] completed large round (ATE)
c [cce-18-2] allowing another 2075859 steps for small clauses
c [cce-18-2] scheduling 13514 clauses = 10750 binary + 2764 ternary
c [cce-18-2] tried to eliminate 13514 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 95 covered clauses in TOTAL during 2 rounds
c [cce-18] 95 < 1/100 * 18319 = 183 considered unsuccessful
c [elim-25] scheduling all variables this time
c [elim-25] scheduled 3444 variables 100%
c [elim-25] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-25] rescheduling of touched variables disabled
c [elim-25-1] eliminated 15 variables 0% in round 1 in 1079832 steps
c [elim-25-1] backward subsumption/strengthening limit 1079800
c [elim-25-1-1] backward checking 127 touched variables 4%
c [elim-25-1-1] fully completed backward checking in 1 rounds
c [elim-25-1] subsumed 0 and strengthened 0 clauses in 15992 steps
c [elim-25] fully completed in 1 rounds
c [elim-25] transition to [ all 0 rem 0 ] state
c [elim-25] eliminated 15 = 0% variables out of 3444 scheduled
c [elim-25] 15 < 1/100 * 3444 = 34 considered unsuccessful
c [bca-25] limit of 10000000 steps and 37056 added (scaled 2)
c [bca-25] 4369 out of 6860 literals actually usable 64%
c [bca-25] added 22 blocked clauses in 75154 steps
c [sort-queue-29] sorted 465 enqueued variables after 1571706 conflicts
c [score-dist-29] active 2964 (86%), one 0 (0%), zero 465 (14%)
c [score-dist-29] max exp 522, different 22 (4%)
c [score-dist-29] median active exp 515, avg 514.0
c [simplification-29] removed 35 variables 1.0% (3429 remain 2%)
c [simplification-29] removed 290 irredundant clauses 1.6% (18207 remain 2%)
c [simplification-29] maximum reduction of 2% = max (1%, 2%)
c [simplification-29] geometric conflict interval increment 115200 = 345600 / 3
c [simplification-29] new conflict interval 460800
c [simplification-29] penalized conflict interval 460800 = 1 * 460800
c [simplification-29] hard conflict limit 2262906 (soft 2032506 + delta 230400)
c [simplification-29] new conflict limit 2032506 (hard 2262906)
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 -  562.9    3429    18207   1599246   44976    570 93409   26    35   27  75%   1024    7   28   22  130%
c -  572.2    3429    18207   1649306   45312    571 93409   19    26   27  75%   1024   -4   19   22   84%
c -  583.3    3429    18207   1701472   45452    571 93409   27    34   26  79%   1024    3   29   24  120%
c -  593.7    3429    18207   1754584   45882    571 93409   29    35   26  82%   1024    3   20   25   80%
c -  604.8    3429    18207   1809950   46520    574 93409   22    29   26  76%   1024   -3   15   25   62%
c -  615.1    3429    18207   1862825   46977    577 93409   19    27   26  70%   1024   -4   17   23   71%
c -  626.2    3429    18207   1917803   48019    577 93409   27    33   27  82%   1024   -2   22   27   81%
c -  637.9    3429    18207   1974968   48296    577 93409   20    26   38  80%   1024   -7   20   25   78%
c -  648.2    3429    18207   2030475   49101    589 93410   20    27   37  75%   1024    1   16   20   79%
c 
c [simplification-30] limit 2032506 conflicts (hard 2262906) hit after 2032510 conflicts
c [quatres-15] found 1566 quaternary clauses 17% in total
c [quatres-15-1] removed 1 duplicate quaternary clauses
c [quatres-15-2] added 1 single-self-subsuming ternary resolvents
c [quatres-15-2] added 1 quaternary resolvents
c [ternres-26] limit 199568116 with penalty 0 = 0 + 0
c [ternres-26] all 3429 free variables schedulable
c [ternres-26] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-26] fully completed ternary resolution
c [basicprobe-10] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-10-0] 996 sched 34%, 339 failed, 20 lifted, 6418 hbrs
c [decomp-110] removed 672 variables
c [basicprobe-10-1] 632 sched 23%, 53 failed, 0 lifted, 10840 hbrs
c [decomp-111] removed 80 variables
c [basicprobe-10-2] 647 sched 24%, 22 failed, 0 lifted, 5612 hbrs
c [decomp-112] removed 22 variables
c [basicprobe-10-3] 641 sched 24%, 3 failed, 0 lifted, 1094 hbrs
c [decomp-113] removed 4 variables
c [basicprobe-10-4] 637 sched 24%, 0 failed, 0 lifted, 100 hbrs
c [basicprobe-10-5] 636 sched 24%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-10-6] 636 sched 24%, 0 failed, 0 lifted, 16 hbrs
c [basicprobe-10-7] 636 sched 24%, 0 failed, 0 lifted, 20 hbrs
c [basicprobe-10-8] 636 sched 24%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-10-8] round limit 8 hit
c [basicprobe-10-8] 437 units = 417 failed (95%) + 20 lifted (5%)
c [basicprobe-10-8] removed 778 variables, found 24124 hbrs
c [bate-8] eliminated 80 asymmetric tautologies during probing
c [transred-26] limit 2000000 with penalty 0 = 0 + 0
c [transred-26] removed 1504 transitive binary clauses
c [bca-26] limit of 10000000 steps and 26343 added (scaled 2)
c [bca-26] 3782 out of 5304 literals actually usable 71%
c [bca-26] added 4 blocked clauses in 57171 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 259 pos 23.0% + 867 neg 77.0% = 1126 sched 42.5% ret 1525
c [sweep-18-1] 9461115 steps 414 queries 10.53 avg class size
c [sweep-18-1] 3084 decisions 393 SAT calls 45.27 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-118] removed 17 variables
c [sweep-18-1] removed 17 vars (0 failed, 20 eqs, 3 impls)
c [sweep-18-2] 412 pos 15.6% + 2222 neg 84.4% = 2634 sched 100.0% ret 0
c [sweep-18-2] 19428926 steps 425 queries 11.88 avg class size
c [sweep-18-2] 5719 decisions 398 SAT calls 75.15 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-119] removed 21 variables
c [sweep-18-2] removed 21 vars (0 failed, 28 eqs, 6 impls)
c [sweep-18-3] 405 pos 15.5% + 2208 neg 84.5% = 2613 sched 100.0% ret 0
c [sweep-18-3] 23108990 steps 448 queries 12.12 avg class size
c [sweep-18-3] 6455 decisions 437 SAT calls 57.80 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-120] removed 3 variables
c [sweep-18-3] removed 3 vars (0 failed, 10 eqs, 2 impls)
c [sweep-18] removed 41 vars in TOTAL (3 rounds, 1284 queries)
c [sort-queue-30] sorted 313 enqueued variables after 2032510 conflicts
c [score-dist-30] active 2297 (88%), one 0 (0%), zero 313 (12%)
c [score-dist-30] max exp 522, different 22 (4%)
c [score-dist-30] median active exp 515, avg 513.7
c [simplification-30] removed 819 variables 23.9% (2610 remain 2%)
c [simplification-30] removed 5466 irredundant clauses 30.0% (12741 remain 2%)
c [simplification-30] maximum reduction of 30% = max (24%, 30%)
c [simplification-30] large reduction 30% >= 5% limit
c [simplification-30] next conflict interval 20325 = min (2032510/100, 460800)
c [simplification-30] penalized conflict interval 20325 = 1 * 20325
c [simplification-30] hard conflict limit 2062997 (soft 2052835 + delta 10162)
c [simplification-30] new conflict limit 2052835 (hard 2062997)
c 
c [simplification-31] limit 2052835 conflicts (hard 2062997) hit after 2060745 conflicts
c [quatres-16] found 1170 quaternary clauses 16% in total
c [quatres-16-1] removed 6 duplicate quaternary clauses
c [quatres-16-2] added 1 single-self-subsuming ternary resolvents
c [quatres-16-2] added 3 quaternary resolvents
c [ternres-27] limit 200000000 with penalty 0 = 0 + 0
c [ternres-27] all 2610 free variables schedulable
c [ternres-27] 15 ternary resolvents (1 bin, 14 trn)
c [ternres-27] fully completed ternary resolution
c [decomp-121] removed 1 variables
c [simpleprobe-11] all 2609 free variables schedulable
c [simpleprobe-11] limit 200000000 penalty 0 = 0 + 0
c [decomp-122] removed 9 variables
c [simpleprobe-11] fully completed simple probing
c [simpleprobe-11] removed 9 variables, found 3844 hbrs, 1 units
c [transred-27] limit 2000000 with penalty 0 = 0 + 0
c [transred-27] removed 1626 transitive binary clauses
c [transred-27] found 2 units
c [cce-19] limit of 505567792 steps penalty 1 = 1 + 0
c [cce-19-1] eliminated 3 clauses out of 60 (5%) of length 6
c [cce-19-1] eliminated 4 clauses out of 202 (2%) of length 5
c [cce-19-1] eliminated 36 clauses out of 593 (6%) of length 4
c [cce-19-1] completed large round (ACCE)
c [cce-19-1] eliminated 43 large clauses in 1745146 steps
c [cce-19-1] allowing another 872573 steps for small clauses
c [cce-19-1] scheduling 9620 clauses = 7574 binary + 2046 ternary
c [cce-19-1] tried to eliminate 9620 small clauses 100%
c [cce-19-1] eliminated 597 binary clauses 8%
c [cce-19-1] eliminated 54 ternary clauses 3%
c [cce-19-1] eliminated 651 small clauses 7%
c [cce-19-1] eliminated 673 small clauses in 20806456 steps
c [cce-19-1] completed small round (ACCE)
c [cce-19-1] eliminated 716 covered clauses in round 1
c [cce-19-2] eliminated 1 clauses out of 557 (0%) of length 4
c [cce-19-2] completed large round (ACCE)
c [cce-19-2] eliminated 1 large clauses in 1643206 steps
c [cce-19-2] allowing another 821603 steps for small clauses
c [cce-19-2] scheduling 8969 clauses = 6977 binary + 1992 ternary
c [cce-19-2] tried to eliminate 8969 small clauses 100%
c [cce-19-2] eliminated 19 binary clauses 0%
c [cce-19-2] eliminated 11 ternary clauses 1%
c [cce-19-2] eliminated 30 small clauses 0%
c [cce-19-2] eliminated 30 small clauses in 19354192 steps
c [cce-19-2] completed small round (ACCE)
c [cce-19-2] eliminated 31 covered clauses in round 2
c [cce-19-3] completed large round (ACCE)
c [cce-19-3] allowing another 818842 steps for small clauses
c [cce-19-3] scheduling 8939 clauses = 6958 binary + 1981 ternary
c [cce-19-3] tried to eliminate 8939 small clauses 100%
c [cce-19-3] eliminated 1 binary clauses 0%
c [cce-19-3] eliminated 2 ternary clauses 0%
c [cce-19-3] eliminated 3 small clauses 0%
c [cce-19-3] eliminated 3 small clauses in 19270956 steps
c [cce-19-3] completed small round (ACCE)
c [cce-19-3] eliminated 3 covered clauses in round 3
c [cce-19] eliminated 750 covered clauses in TOTAL during 3 rounds
c [elim-26] scheduling all variables this time
c [elim-26] scheduled 2598 variables 100%
c [elim-26] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-26] rescheduling of touched variables disabled
c [elim-26-1] eliminated 390 variables 15% in round 1 in 711345 steps
c [elim-26-1] backward subsumption/strengthening limit 711300
c [elim-26-1-1] backward checking 1116 touched variables 43%
c [elim-26-1-1] fully completed backward checking in 1 rounds
c [elim-26-1] subsumed 5 and strengthened 3 clauses in 96693 steps
c [elim-26-1] rescheduled 65 variables 3% by backward subsumption
c [elim-26-2] eliminated 1 variables 0% in round 2 in 22553 steps
c [elim-26-2] backward subsumption/strengthening limit 22500
c [elim-26-2-1] backward checking 11 touched variables 0%
c [elim-26-2-1] fully completed backward checking in 1 rounds
c [elim-26-2] subsumed 0 and strengthened 0 clauses in 5524 steps
c [elim-26] fully completed in 2 rounds
c [elim-26] transition to [ all 0 rem 0 ] state
c [elim-26] eliminated 391 = 15% variables out of 2598 scheduled
c [bca-27] limit of 10000000 steps and 23699 added (scaled 2)
c [bca-27] 3000 out of 4416 literals actually usable 68%
c [bca-27] added 15 blocked clauses in 60566 steps
c [sweep-19] limit 60668135 penalty 0 = 0 + 0
c [sweep-19-1] 268 pos 12.1% + 1939 neg 87.9% = 2207 sched 100.0% ret 0
c [sweep-19-1] 18367284 steps 374 queries 14.50 avg class size
c [sweep-19-1] 5694 decisions 369 SAT calls 54.19 avg env size
c [sweep-19-1] fully completed sweeping round
c [decomp-123] removed 2 variables
c [sweep-19-1] removed 2 vars (0 failed, 5 eqs, 3 impls)
c [sweep-19-2] 268 pos 12.2% + 1937 neg 87.8% = 2205 sched 100.0% ret 0
c [sweep-19-2] 23600441 steps 349 queries 16.39 avg class size
c [sweep-19-2] 6868 decisions 345 SAT calls 69.05 avg env size
c [sweep-19-2] fully completed sweeping round
c [decomp-124] removed 2 variables
c [sweep-19-2] removed 2 vars (0 failed, 4 eqs, 0 impls)
c [sweep-19-3] 268 pos 12.2% + 1935 neg 87.8% = 2203 sched 100.0% ret 0
c [sweep-19-3] 19008170 steps 139 queries 25.55 avg class size
c [sweep-19-3] 5084 decisions 139 SAT calls 109.68 avg env size
c [sweep-19-3] 514 variables remain 23% (1683 retained 77%)
c [decomp-125] removed 7 variables
c [sweep-19-3] removed 7 vars (0 failed, 2 eqs, 1 impls)
c [sweep-19] removed 11 vars in TOTAL (3 rounds, 859 queries)
c [sort-queue-31] sorted 260 enqueued variables after 2060745 conflicts
c [score-dist-31] active 1936 (88%), one 0 (0%), zero 260 (12%)
c [score-dist-31] max exp 522, different 22 (4%)
c [score-dist-31] median active exp 515, avg 513.6
c [simplification-31] removed 414 variables 15.9% (2196 remain 1%)
c [simplification-31] removed 1287 irredundant clauses 10.1% (11454 remain 1%)
c [simplification-31] maximum reduction of 16% = max (16%, 10%)
c [simplification-31] large reduction 16% >= 5% limit
c [simplification-31] next conflict interval 20607 = min (2060745/100, 460800)
c [simplification-31] penalized conflict interval 20607 = 1 * 20607
c [simplification-31] hard conflict limit 2091655 (soft 2081352 + delta 10303)
c [simplification-31] new conflict limit 2081352 (hard 2091655)
c 
c [simplification-32] limit 2081352 conflicts (hard 2091655) hit after 2081356 conflicts
c [quatres-17] found 1184 quaternary clauses 17% in total
c [quatres-17-2] added 3 quaternary resolvents
c [ternres-28] limit 200000000 with penalty 0 = 0 + 0
c [ternres-28] all 2196 free variables schedulable
c [ternres-28] 10 ternary resolvents (1 bin, 9 trn)
c [ternres-28] fully completed ternary resolution
c [gauss-7] limit 2551414 penalty 4 = 4 + 0
c [gauss-7] extracted 21 xors of average arity 3.0
c [gauss-7] connected 63 occurrences of 21 variables (average 3.0)
c [gauss-7] limit 2551414 penalty 4 = 4 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-11] limit 20411317 penalty 0 = 0 + 0 boost 1
c [treelook-11] scheduled 4387 literals 100%
c [treelook-11] scheduling used 286392 steps
c [treelook-11] scheduled completely
c [treelook-11] limit 20411317 penalty 0 = 0 + 0 boost 1
c [treelook-11] used 7852953 steps
c [treelook-11] fully completed tree based probing
c [decomp-127] removed 1 variables
c [treelook-11] removed 22 variables, found 26787 hbrs
c [unhide-20] limit 2500000 with penalty 3 = 3 + 0
c [unhide-20-51] 0 units, 7 failed, 19857 tauts, 0 hbrs, 103511 literals
c [transred-28] limit 2000000 with penalty 0 = 0 + 0
c [transred-28] removed 986 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 2172 variables 100%
c [block-7] limit of 50000000 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 5 blocked clauses
c [block-7] 5 < 1/100 * 11199 = 111 considered unsuccessful
c [cce-20] limit of 1020565862 steps penalty 0 = 0 + 0
c [cce-20-1] eliminated 1 clauses out of 1 (100%) of length 25
c [cce-20-1] eliminated 2 clauses out of 32 (6%) of length 7
c [cce-20-1] eliminated 3 clauses out of 80 (4%) of length 6
c [cce-20-1] eliminated 3 clauses out of 270 (1%) of length 5
c [cce-20-1] eliminated 14 clauses out of 589 (2%) of length 4
c [cce-20-1] completed large round (ATE)
c [cce-20-1] eliminated 23 large clauses in 1893700 steps
c [cce-20-1] allowing another 946850 steps for small clauses
c [cce-20-1] scheduling 8361 clauses = 6471 binary + 1890 ternary
c [cce-20-1] tried to eliminate 8361 small clauses 100%
c [cce-20-1] eliminated 141 binary clauses 2%
c [cce-20-1] eliminated 60 ternary clauses 3%
c [cce-20-1] eliminated 201 small clauses 2%
c [cce-20-1] eliminated 201 small clauses in 17116568 steps
c [cce-20-1] completed small round (ATE)
c [cce-20-1] eliminated 224 covered clauses in round 1
c [cce-20-2] completed large round (ATE)
c [cce-20-2] allowing another 896325 steps for small clauses
c [cce-20-2] scheduling 8160 clauses = 6330 binary + 1830 ternary
c [cce-20-2] tried to eliminate 8160 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 224 covered clauses in TOTAL during 2 rounds
c [elim-27] scheduling all variables this time
c [elim-27] scheduled 2172 variables 100%
c [elim-27] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-27] rescheduling of touched variables disabled
c [elim-27-1] eliminated 42 variables 2% in round 1 in 644280 steps
c [elim-27-1] backward subsumption/strengthening limit 644200
c [elim-27-1-1] backward checking 301 touched variables 14%
c [elim-27-1-1] fully completed backward checking in 1 rounds
c [elim-27-1] subsumed 0 and strengthened 0 clauses in 30025 steps
c [elim-27] fully completed in 1 rounds
c [elim-27] transition to [ all 0 rem 0 ] state
c [elim-27] eliminated 42 = 2% variables out of 2172 scheduled
c [bca-28] limit of 10000000 steps and 22524 added (scaled 2)
c [bca-28] 2721 out of 4262 literals actually usable 64%
c [bca-28] added 17 blocked clauses in 83383 steps
c [sweep-20] limit 61233951 penalty 0 = 0 + 0
c [sweep-20-1] 105 pos 20.9% + 398 neg 79.1% = 503 sched 23.6% ret 1627
c [sweep-20-1] 14146383 steps 265 queries 6.21 avg class size
c [sweep-20-1] 2840 decisions 263 SAT calls 52.73 avg env size
c [sweep-20-1] fully completed sweeping round
c [decomp-128] removed 2 variables
c [sweep-20-1] removed 2 vars (0 failed, 1 eqs, 0 impls)
c [sweep-20-2] 288 pos 13.5% + 1840 neg 86.5% = 2128 sched 100.0% ret 0
c [sweep-20-2] 46181946 steps 354 queries 12.74 avg class size
c [sweep-20-2] 8491 decisions 351 SAT calls 73.32 avg env size
c [sweep-20-2] fully completed sweeping round
c [decomp-129] removed 6 variables
c [sweep-20-2] removed 6 vars (0 failed, 3 eqs, 2 impls)
c [sweep-20-3] 288 pos 13.6% + 1834 neg 86.4% = 2122 sched 100.0% ret 0
c [sweep-20-3] 1123634 steps 10 queries 395.80 avg class size
c [sweep-20-3] 326 decisions 9 SAT calls 87.67 avg env size
c [sweep-20-3] 2093 variables remain 99% (29 retained 1%)
c [sweep-20-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-20] removed 8 vars in TOTAL (3 rounds, 626 queries)
c [sort-queue-32] sorted 228 enqueued variables after 2081356 conflicts
c [score-dist-32] active 1894 (89%), one 0 (0%), zero 228 (11%)
c [score-dist-32] max exp 522, different 22 (4%)
c [score-dist-32] median active exp 515, avg 513.6
c [simplification-32] removed 74 variables 3.4% (2122 remain 1%)
c [simplification-32] removed 584 irredundant clauses 5.1% (10870 remain 1%)
c [simplification-32] maximum reduction of 5% = max (3%, 5%)
c [simplification-32] large reduction 5% >= 5% limit
c [simplification-32] next conflict interval 20813 = min (2081356/100, 460800)
c [simplification-32] penalized conflict interval 20813 = 1 * 20813
c [simplification-32] hard conflict limit 2112575 (soft 2102169 + delta 10406)
c [simplification-32] new conflict limit 2102169 (hard 2112575)
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 -  674.6    2122    10870   2103444   48941    419 46100   19    24   24  80%   1024   -4   20   21   93%
c 
c [simplification-33] limit 2102169 conflicts (hard 2112575) hit after 2112575 conflicts
c [quatres-18] found 1201 quaternary clauses 17% in total
c [quatres-18-1] removed 8 duplicate quaternary clauses
c [quatres-18-2] added 3 quaternary resolvents
c [ternres-29] limit 200000000 with penalty 0 = 0 + 0
c [ternres-29] all 2122 free variables schedulable
c [ternres-29] 6 ternary resolvents (1 bin, 5 trn)
c [ternres-29] fully completed ternary resolution
c [basicprobe-11] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-11-0] 649 sched 34%, 201 failed, 2 lifted, 1139 hbrs
c [decomp-132] removed 258 variables
c [basicprobe-11-1] 460 sched 25%, 31 failed, 2 lifted, 3141 hbrs
c [decomp-133] removed 45 variables
c [basicprobe-11-2] 439 sched 24%, 6 failed, 0 lifted, 1961 hbrs
c [decomp-134] removed 16 variables
c [basicprobe-11-3] 437 sched 24%, 0 failed, 0 lifted, 298 hbrs
c [decomp-135] removed 7 variables
c [basicprobe-11-4] 433 sched 24%, 0 failed, 0 lifted, 64 hbrs
c [basicprobe-11-5] 433 sched 24%, 0 failed, 0 lifted, 24 hbrs
c [basicprobe-11-6] 433 sched 24%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-11-7] 433 sched 24%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-11-8] 433 sched 24%, 1 failed, 0 lifted, 14 hbrs
c [basicprobe-11-8] round limit 8 hit
c [basicprobe-11-8] 243 units = 239 failed (98%) + 4 lifted (2%)
c [basicprobe-11-8] removed 327 variables, found 6666 hbrs
c [bate-9] eliminated 71 asymmetric tautologies during probing
c [transred-29] limit 2000000 with penalty 0 = 0 + 0
c [transred-29] removed 915 transitive binary clauses
c [cce-21] limit of 1037735096 steps penalty 0 = 0 + 0
c [cce-21-1] eliminated 1 clauses out of 1 (100%) of length 23
c [cce-21-1] eliminated 1 clauses out of 2 (50%) of length 15
c [cce-21-1] eliminated 2 clauses out of 3 (67%) of length 11
c [cce-21-1] eliminated 1 clauses out of 4 (25%) of length 10
c [cce-21-1] eliminated 1 clauses out of 3 (33%) of length 9
c [cce-21-1] eliminated 2 clauses out of 30 (7%) of length 6
c [cce-21-1] eliminated 4 clauses out of 98 (4%) of length 5
c [cce-21-1] eliminated 36 clauses out of 437 (8%) of length 4
c [cce-21-1] completed large round (ACCE)
c [cce-21-1] eliminated 48 large clauses in 707646 steps
c [cce-21-1] allowing another 353823 steps for small clauses
c [cce-21-1] scheduling 6063 clauses = 4583 binary + 1480 ternary
c [cce-21-1] tried to eliminate 6063 small clauses 100%
c [cce-21-1] eliminated 257 binary clauses 6%
c [cce-21-1] eliminated 88 ternary clauses 6%
c [cce-21-1] eliminated 345 small clauses 6%
c [cce-21-1] eliminated 351 small clauses in 6314036 steps
c [cce-21-1] completed small round (ACCE)
c [cce-21-1] eliminated 399 covered clauses in round 1
c [cce-21-2] eliminated 1 clauses out of 7 (14%) of length 7
c [cce-21-2] eliminated 1 clauses out of 94 (1%) of length 5
c [cce-21-2] eliminated 4 clauses out of 401 (1%) of length 4
c [cce-21-2] completed large round (ACCE)
c [cce-21-2] eliminated 6 large clauses in 618252 steps
c [cce-21-2] allowing another 309126 steps for small clauses
c [cce-21-2] scheduling 5718 clauses = 4326 binary + 1392 ternary
c [cce-21-2] tried to eliminate 5718 small clauses 100%
c [cce-21-2] eliminated 22 binary clauses 1%
c [cce-21-2] eliminated 13 ternary clauses 1%
c [cce-21-2] eliminated 35 small clauses 1%
c [cce-21-2] eliminated 35 small clauses in 5690221 steps
c [cce-21-2] completed small round (ACCE)
c [cce-21-2] eliminated 41 covered clauses in round 2
c [cce-21-3] eliminated 1 clauses out of 28 (4%) of length 6
c [cce-21-3] eliminated 1 clauses out of 93 (1%) of length 5
c [cce-21-3] eliminated 1 clauses out of 397 (0%) of length 4
c [cce-21-3] completed large round (ACCE)
c [cce-21-3] eliminated 3 large clauses in 605404 steps
c [cce-21-3] allowing another 302702 steps for small clauses
c [cce-21-3] scheduling 5683 clauses = 4304 binary + 1379 ternary
c [cce-21-3] tried to eliminate 5683 small clauses 100%
c [cce-21-3] eliminated 14 binary clauses 0%
c [cce-21-3] eliminated 1 ternary clauses 0%
c [cce-21-3] eliminated 15 small clauses 0%
c [cce-21-3] eliminated 15 small clauses in 5609917 steps
c [cce-21-3] completed small round (ACCE)
c [cce-21-3] eliminated 18 covered clauses in round 3
c [cce-21] eliminated 458 covered clauses in TOTAL during 3 rounds
c [elim-28] scheduling all variables this time
c [elim-28] scheduled 1795 variables 100%
c [elim-28] boosting limit by 20
c [elim-28] limit of 16000000000 steps penalty 0 = 0 + 0
c [elim-28] rescheduling of touched variables disabled
c [elim-28-1] eliminated 291 variables 16% in round 1 in 452131 steps
c [elim-28-1] backward subsumption/strengthening limit 452100
c [elim-28-1-1] backward checking 806 touched variables 45%
c [elim-28-1-1] fully completed backward checking in 1 rounds
c [elim-28-1] subsumed 0 and strengthened 0 clauses in 54862 steps
c [elim-28] fully completed in 1 rounds
c [elim-28] transition to [ all 0 rem 0 ] state
c [elim-28] eliminated 291 = 16% variables out of 1795 scheduled
c [bca-29] limit of 10000000 steps and 15635 added (scaled 2)
c [bca-29] 1869 out of 3010 literals actually usable 62%
c [bca-29] added 12 blocked clauses in 45417 steps
c [sweep-21] limit 62264105 penalty 0 = 0 + 0
c [sweep-21-1] 205 pos 13.8% + 1278 neg 86.2% = 1483 sched 98.6% ret 21
c [sweep-21-1] 20258225 steps 251 queries 11.64 avg class size
c [sweep-21-1] 5892 decisions 249 SAT calls 55.43 avg env size
c [sweep-21-1] fully completed sweeping round
c [decomp-140] removed 19 variables
c [sweep-21-1] removed 19 vars (0 failed, 5 eqs, 3 impls)
c [sweep-21-2] 205 pos 13.8% + 1280 neg 86.2% = 1485 sched 100.0% ret 0
c [sweep-21-2] 26991910 steps 245 queries 14.08 avg class size
c [sweep-21-2] 6508 decisions 244 SAT calls 60.74 avg env size
c [sweep-21-2] fully completed sweeping round
c [decomp-141] removed 7 variables
c [sweep-21-2] removed 7 vars (0 failed, 2 eqs, 0 impls)
c [sweep-21-3] 205 pos 13.9% + 1273 neg 86.1% = 1478 sched 100.0% ret 0
c [sweep-21-3] 15642177 steps 60 queries 46.25 avg class size
c [sweep-21-3] 3390 decisions 59 SAT calls 101.73 avg env size
c [sweep-21-3] 506 variables remain 34% (971 retained 66%)
c [decomp-142] removed 3 variables
c [sweep-21-3] removed 3 vars (0 failed, 3 eqs, 1 impls)
c [sweep-21] removed 29 vars in TOTAL (3 rounds, 553 queries)
c [sort-queue-33] sorted 130 enqueued variables after 2112575 conflicts
c [score-dist-33] active 1345 (91%), one 0 (0%), zero 130 (9%)
c [score-dist-33] max exp 522, different 22 (4%)
c [score-dist-33] median active exp 515, avg 513.8
c [simplification-33] removed 647 variables 30.5% (1475 remain 1%)
c [simplification-33] removed 3580 irredundant clauses 32.9% (7290 remain 1%)
c [simplification-33] maximum reduction of 33% = max (30%, 33%)
c [simplification-33] large reduction 33% >= 5% limit
c [simplification-33] next conflict interval 21125 = min (2112575/100, 460800)
c [simplification-33] penalized conflict interval 21125 = 1 * 21125
c [simplification-33] hard conflict limit 2144262 (soft 2133700 + delta 10562)
c [simplification-33] new conflict limit 2133700 (hard 2144262)
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  680.0    1474     7290   2113491   46244    355 16687   17    21   19  80%   1024   -6   12   21   58%
c i  680.0    1473     7290   2113647   46385    355 16687   17    21   19  80%  -1380   -7   11   21   55%
c i  680.6    1451     7290   2118583   50805    366 16690   10    13   21  79% -14859  -14    6   20   28%
c i  680.7    1450     7290   2119236   51291    386 16698   10    12   21  79% -14793  -14    5   20   24%
c i  681.2    1037     7290   2123385   55142    389 16698    8    11   22  75% -13928  -15    6   19   31%
c i  682.0    1035     7290   2130639   61695    408 16705    8    10   22  78% -12422  -14    6   18   33%
c i  682.2    1022     7290   2131962   62926    413 16706    8    10   22  75% -12235  -14    6   18   35%
c i  682.3    1019     7290   2132808   63607    423 16713    8    10   22  75% -12094  -14    6   17   36%
c i  683.0    1016     7290   2137980   68288    440 16721    8    11   23  75% -11132  -12    7   17   40%
c i  683.1     969     7290   2138668   68856    453 16723    8    10   23  74% -11044  -12    6   17   36%
c i  683.1     926     7290   2138671   68856    453 16725    8    10   23  74% -11044  -12    6   17   35%
c i  683.1     893     7290   2138698   68879    453 16726    8    10   23  75% -11040  -12    6   17   34%
c i  683.1     862     7290   2138702   68879    454 16728    8    10   23  75% -11040  -12    6   17   34%
c i  683.1     825     7290   2138731   68888    458 16729    8    10   23  75% -11036  -12    5   17   33%
c i  683.1     666     7290   2138744   68889    459 16732    8    10   23  75% -11034  -12    5   17   32%
c i  683.1     531     7290   2138745   68889    459 16732    8    10   23  75% -11034  -12    5   17   32%
c 0  683.1     282     7290   2138745   68889    459 16732    8    10   23  75% -11034  -12    5   17   32%
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 
s UNSATISFIABLE
c
c bate: 1295 basic ate = 1208 trn 93% + 87 lrg 7% in 9 updates
c bcas: 29 count, 354 added (1104 skipped), 1662867 steps
c bkwd: tried 262778 clauses, 524928 lits, 2.00 lits/clause
c bkwd: checked 5738937 occs, 21.84 occs/clause, 10.93 occs/lit
c bkwd: subsumed 68 binary, 223 ternary, 207 large
c bkwd: strengthened 25 binary, 4 ternary (100% self), 546 large (0% self)
c blkd: 7 bces, 1159 removed, 1276138 resolutions, 3488751 steps
c blkd: 3259 blocking literals 1%, 8 pure
c bump: 2166752 bumped seen, 413197379 lits 190.7 on average
c card: 7 count, 0 units, 24559 am1, 46600096 steps
c card: 141 rescheduled, 1322 eliminated, 33333 resolved, 79972 subsumed
c card: 25056 at-most-one constraints found, average size 4.27
c card: 25056 at-most-one constraints used 100%, average size 4.27
c card: 23 at-most-two constraints found, average size 4.04
c card: 22 at-most-two constraints used 96%, average size 4.05
c cces: 21 cces, 20851 eliminated, 18461 ate 89%, 2390 abce 11%
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: 2677487 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 276 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 142 decompositions, 52633 equivalent 29%
c deco: 43310 decision-only clauses 2%, 58% reduction
c decs: 3648609 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 28 elims, 19719 eliminated 11%, 138 pure 1%
c elms: 85 rounds, 3.0 rounds/bve
c elms: 18660 small 95%, 913 large 5%
c elms: 94859 tried small, 18661 succeeded 20%, 76198 failed 80%
c elms: 5618 subsumed, 9686 strengthened, 839 blocked
c elms: 6210029 copies, 5644305 resolutions, 3159043 ipos
c elms: 1097141 subchks, 693449 strchks
c gaus: 7 extractions, 371 extracted, 2.9 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12154190 steps, 6077095 extr 50%, 9582 elim 0%
c glue: 31.0 orig avg, 31.0 real avg, 5.2 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 587160 = 50337 simple 9% + 450070 trn 77% + 86753 lrg 15%, 2826 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2166752 clauses, 83.0 length
c lrnd: 179938659 lits = 281211894 orig - 101273235 removed 36%
c lrnd: 753496 uips 35%, 1290676 flips 60%
c mins: 2120812 mins 98%, 178 bin 0%, 1594 size 0%
c mins: 609495771 poisoned searches, 84943589 hits, 14% hit rate
c mins: 786958019 used twice searches, 41581769 hits, 5% hit rate
c move: moved 18417, 14165 bin 77%, 4252 trn 23%
c otfs: 1304 driving 24%, 4186 restarting 76%
c otfs: str 5490, 5450 red 99%, 40 irr 1%
c otfs: str 5490, 0 bin 0%, 32 trn 1%, 5458 lrg 99%
c otfs: sub 15, 15 red 100%, 0 irr 0%
c otfs: sub 15, 0 bin 0%, 0 trn 0%, 15 lrg 100%
c phas: 14 computed, 21155 set, 2 pos (0%), 21153 neg (100%)
c prbs: 11 basic, 120154 probed, 3712 failed, 329 lifted
c prbs: 11 simple, 358184 probed, 1511 failed, 21756 eqs
c prbs: 11 treelook, 8159 probed, 72 failed, 0 lifted
c prom: 118482 locked 4% out of 2859778 tried
c prps: 1172563553 props, 296 props/dec
c prps: 92% srch, 8% simp, 0% lkhd
c quat: 18 count, 50 quat, 6 self1, 0 self2, 27 dup
c queu: 33 sorted, 3648609 next (102213 steps 0.03)
c queu: 413498817 enq (633516481 steps 1.53), 413197379 deq 100%
c redc: 4374 clauses 11%, 40091 tried 2%, 6 sat 0%
c redc: 11431 lits 2%, 496929 tried 0%, 6 sat 0%
c redc: 342 times jump level reduced, 6.5 levels on average
c reds: 44 count, 48607.8 conflicts per reduce
c reds: 0 memlim 0%, 44 arith 100%
c reds: 1573128 collected 93%, 117319 retired 7%
c rmbd: 5181 removed, 2768 red 53%
c rsts: 9688 restarts 99%, 102 skipped 1%
c rsts: 102 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: 33 count, 33 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 2166752 count (1652790 tried 0.8), 209162 sub out of 2165467 (9.7%)
c swps: 21 count, 38 rounds, 10537 queries (277.3/round)
c swps: 10397 sat calls, 106 unsat (2.8% success rate)
c swps: 139016 decisions 13.4, 29311 conflicts 2.8
c swps; 34.7 avg class size, 59.3 avg environment size
c swps: 0 failed, 166 impls, 199 equivs
c swp0: 3501 type 0 queries, 1337 unsat (38.2%), 3448 sat (98.5%)
c swp1: 7036 type 1 queries, 3185 unsat (45.3%), 6890 sat (97.9%)
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: 11631464 calls to obtain time
c tops: 107974 fixed 60%, 55 its, 38886.27 confs/it
c trds: 29 transitive reductions, 19926 removed, 56 failed
c trds: 90746 nodes, 237082 edges, 56037420 steps
c trim: 2478516 words, 9.5 MB
c trnr: 29 count, 7 bin, 1181 trn, 51545811 steps
c unhd: 20 count, 51 rounds, 40473621 steps
c unhd: 692 non-trivial sccs of average size 2.2
c unhd: 22 units, 18 bin, 4 trn, 0 lrg
c unhd: 1835 failed, 1805 stamp, 0 lits, 22 bin, 6 trn, 0 lrg
c unhd: 154808 tauts, 6700 bin 4%, 1308 trn 1%, 465 lrg 0%
c unhd: 154808 tauts, 146335 stamp 95%, 133691 red 86%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1206472 str, 18 bin 0%, 908 trn 0%, 1205546 lrg 100%, 1202908 red 100%
c vars: 282 remaining 0% and 180326 removed 100% out of 180608
c vars: 107974 fixed 60%, 19719 eliminated 11%, 52633 equivalent 29%
c vsts: 21986269405 visits, 95% srch, 5% simp, 0% lkhd
c vsts: 19.4 search visits per propagation, 9797.5 per conflict
c wchs: 4267651524 pushed, 24097007 enlarged, 451 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2165517       1573128        117319      59944323      19154059        816980
c 
c  0 0         17587   1      1561   0         0   0  23354761  39   5313066  28    123273  15     0.5
c  1 5         14961   1      3660   0      3354   3   4694706   8   1366448   7     46125   6     0.5
c  2 6         77642   4     33591   2     14043  12   9485002  16<  3072888  16    139405  17     2.3
c  3 9        221188  10    145841   9     23544  20   9252645  15   3277820  17<   169523  21<    4.7
c  4 14       395822  18    315477  20     24870  21<  6048523  10   2628427  14    138146  17     7.2
c  5 21       529102  24<   419721  27<    26145  22   3317383   6   1710122   9     99633  12     7.5
c  6 30       495726  23    384988  24     15677  13   1826396   3    972050   5     55767   7    11.6
c  7 41       250937  12    192343  12      5943   5   1011550   2    425401   2     21834   3     7.0
c  8 54        74037   3     55406   4      1772   2    368886   1    169877   1     12739   2     6.6
c  9 69        24072   1     15851   1       669   1    162279   0     72147   0      4772   1     6.2
c 10 86        18105   1      3353   0       673   1    322966   1     87786   0      3855   0     7.1
c 11 126       43850   2      1336   0       629   1     95449   0     55605   0      1856   0    13.4
c 12 230        2488   0         0   0         0   0      3777   0      2422   0        52   0     1.8
c 
c avg                  5.2           5.2           4.3           2.0           2.5           3.2
c std                  1.8           1.4           1.7           2.1           2.2           2.1
c 
c   68.745  10% bump
c   48.492   7% cce
c   35.846   5% probe
c   25.719   4% unhide
c   16.308   2% sweep
c    6.073   1% elim
c 
c    8.706 < 1% rest (below)
c 
c    3.369   0% transred
c    1.999   0% decide
c    1.384   0% bca
c    0.591   0% block
c    0.510   0% gauss
c    0.415   0% card
c    0.325   0% ternres
c    0.114   0% quatres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.702   0% preprocessing     1%
c  142.201  21% inprocessing     99%
c ==================================
c  143.903  21% simplifying
c  539.168  79% search
c ==================================
c  683.075 100% all
c 
c       2138745 conflicts,        3131.1 confs/sec
c           394 ternaries,        5428.3 confs/ternary
c           148 binaries,        14451.0 confs/binary
c            55 iterations,      38886.3 confs/iteration
c 
c            44 reductions,          0.1 redus/sec,  48607.8 confs/reduction
c          9688 restarts,           14.2 rests/sec,    220.8 confs/restart
c       3648609 decisions,        5341.4 decis/sec,      1.7 decis/conflict
c    1172563553 propagations,  1716596.5 props/sec,    321.4 props/decision
c 
c 683.1 seconds, 61.4 MB
c launch: done
