c launch: /data/cnf/sc2014/app/IBM_FV_2004_rule_batch_1_31_1_SAT_dat.k40.debugged.cnf.bz2
c host: atom29
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/IBM_FV_2004_rule_batch_1_31_1_SAT_dat.k40.debugged.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/IBM_FV_2004_rule_batch_1_31_1_SAT_dat.k40.debugged.cnf.bz2
c no embedded options
c found 'p cnf 52444 217642' header
c read 52444 variables, 217642 clauses, 547043 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=4
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 50629 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] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
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   50629   210196         0       0      0     0    0     0   10   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 2338 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 2338 out of 2338 constraints (100%) meet size limits
c [card-1] found 9 units
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 16385 variables
c [simpleprobe-1] all 36059 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 5612 variables
c [simpleprobe-1] 130 variables remain 0% (30317 retained 100%)
c [simpleprobe-1] removed 5612 variables, found 35460 hbrs, 747 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 9 units, 7 failed, 349 tauts, 0 hbrs, 644 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 30420 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 18857 variables 62% in round 1 in 12327619 steps
c [elim-1-1] backward subsumption/strengthening limit 7672381
c [elim-1-1-1] backward checking 21884 touched variables 72%
c [elim-1-1-1] incomplete backward checking 21619 remain 99%
c [elim-1-1] subsumed 5 and strengthened 111 clauses in 7675938 steps
c [elim-1] incomplete 385 not tried 1% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 18859 = 62% variables out of 30420 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 75533 negative 93.8% of 80551 except 5018 6.2%
c [phase-count-1] 69933 positive 86.8% of 80551 except 10618 13.2%
c [phase-count-1] less non-negative clauses 5018 than limit 8000 (10.0%)
c [phase-count-1] non-pos/non-neg = 10618/5018 = 2.12 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 11561 negative 100%
c [sort-queue-1] sorted 11561 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 11561 (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 34588 variables 74.9% (11561 remain 23%)
c [simplification-1] removed 129645 irredundant clauses 61.7% (80551 remain 38%)
c [simplification-1] maximum reduction of 75% = max (75%, 62%)
c [simplification-1] large reduction 75% >= 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.6   11560    80551       305     248     32  7655    0     4    8  10%      1    4    4    0 16155%
c i    1.6   11559    80551       306     248     32  7655    0     4    8  10%      1    4    4    0 16093%
c i    1.7   11558    80551       789     674     62  7665    1     9    8  12%      2    9    8    0 10025%
c i    1.7   11557    80551       790     674     62  7665    1     9    8  12%      2    9    8    0 9986%
c 
c [simplification-2] limit 1020 conflicts (hard 11000) hit after 1020 conflicts
c [decomp-3] removed 16 variables
c [simpleprobe-2] 40 schedulable variables 0%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 35 variables
c [simpleprobe-2] 90 variables remain 1% (11420 retained 99%)
c [simpleprobe-2] removed 35 variables, found 56 hbrs, 5 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 23020 literals 100%
c [treelook-1] scheduling used 264186 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 353153 steps
c [treelook-1] 22972 literals remain 100%
c [treelook-1] 11510 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 600 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 6978 probes remain 61% after last round
c [basicprobe-1-0] 8 units = 8 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 31 variables, found 1490 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 5 units, 10 failed, 346 tauts, 0 hbrs, 4845 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 11455 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 293 variables 3% in round 1 in 14649270 steps
c [elim-2-1] backward subsumption/strengthening limit 5350730
c [elim-2-1-1] backward checking 3228 touched variables 28%
c [elim-2-1-1] incomplete backward checking 1832 remain 57%
c [elim-2-1] subsumed 0 and strengthened 6 clauses in 5351308 steps
c [elim-2] incomplete 11 not tried 0% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 293 = 3% variables out of 11455 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 72979 negative 93.6% of 78000 except 5021 6.4%
c [phase-count-2] 67760 positive 86.9% of 78000 except 10240 13.1%
c [phase-count-2] less non-negative clauses 5021 than limit 7800 (10.0%)
c [phase-count-2] non-pos/non-neg = 10240/5021 = 2.04 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 135 negative 100%
c [sort-queue-2] sorted 6671 enqueued variables after 1020 conflicts
c [score-dist-2] active 4491 (40%), one 0 (0%), zero 6671 (60%)
c [score-dist-2] max exp 509, different 11 (2%)
c [score-dist-2] median active exp 502, avg 502.1
c [simplification-2] removed 395 variables 3.4% (11162 remain 22%)
c [simplification-2] removed 2551 irredundant clauses 3.2% (78000 remain 37%)
c [simplification-2] maximum reduction of 3% = max (3%, 3%)
c [simplification-2] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-2] new conflict interval 5000
c [simplification-2] penalized conflict interval 5000 = 1 * 5000
c [simplification-2] hard conflict limit 16020 (soft 6020 + delta 10000)
c [simplification-2] new conflict limit 6020 (hard 16020)
c 
c [simplification-3] limit of 128 binary hit after 128 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 678 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 678 out of 678 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 1 at-most-one constraints, 0 used 0%
c [card-2] exported 0 binary clauses, 0.0 per/constraint
c [decomp-6] removed 9 variables
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 2 units, 9 failed, 445 tauts, 0 hbrs, 4616 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 11139 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 136 variables 1% in round 1 in 14046826 steps
c [elim-3-1] backward subsumption/strengthening limit 5953174
c [elim-3-1-1] backward checking 911 touched variables 8%
c [elim-3-1-1] incomplete backward checking 909 remain 100%
c [elim-3-1] subsumed 0 and strengthened 19 clauses in 5954212 steps
c [elim-3] incomplete 92 not tried 1% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 136 = 1% variables out of 11139 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 71857 negative 93.5% of 76821 except 4964 6.5%
c [phase-count-3] 66931 positive 87.1% of 76821 except 9890 12.9%
c [phase-count-3] less non-negative clauses 4964 than limit 7600 (10.0%)
c [phase-count-3] non-pos/non-neg = 9890/4964 = 1.99 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 85 negative 100%
c [sort-queue-3] sorted 4380 enqueued variables after 5561 conflicts
c [score-dist-3] active 6623 (60%), one 0 (0%), zero 4380 (40%)
c [score-dist-3] max exp 509, different 29 (6%)
c [score-dist-3] median active exp 501, avg 498.7
c [simplification-3] removed 159 variables 1.4% (11003 remain 22%)
c [simplification-3] removed 1179 irredundant clauses 1.5% (76821 remain 37%)
c [simplification-3] maximum reduction of 2% = max (1%, 2%)
c [simplification-3] forced so keeping old conflict interval 5000
c [simplification-3] conflict limit remains at 6020 (hard 16020)
c [simplification-3] new binary interval 1000
c 
c [simplification-4] limit 6020 conflicts (hard 16020) hit after 6021 conflicts
c [decomp-7] removed 1 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 15582 literals 71%
c [treelook-2] scheduling used 150019 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 153429 steps
c [treelook-2] 15526 literals remain 71%
c [treelook-2] 10607 variables remain to probed next time 96%
c [treelook-2] removed 0 variables, found 156 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 6 failed, 252 tauts, 0 hbrs, 7069 literals
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 10999 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 48 variables 0% in round 1 in 13911109 steps
c [elim-4-1] backward subsumption/strengthening limit 13911100
c [elim-4-1-1] backward checking 372 touched variables 3%
c [elim-4-1-1] incomplete backward checking 67 remain 18%
c [elim-4-1] subsumed 0 and strengthened 15 clauses in 13911695 steps
c [elim-4-1] rescheduled 40 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 27923 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 48 = 0% variables out of 10999 scheduled
c [elim-4] 48 < 1/100 * 10999 = 109 considered unsuccessful
c [phase-count-4] 71531 negative 93.5% of 76496 except 4965 6.5%
c [phase-count-4] 66652 positive 87.1% of 76496 except 9844 12.9%
c [phase-count-4] less non-negative clauses 4965 than limit 7600 (10.0%)
c [phase-count-4] non-pos/non-neg = 9844/4965 = 1.98 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 85 negative 100%
c [sort-queue-4] sorted 4303 enqueued variables after 6021 conflicts
c [score-dist-4] active 6648 (61%), one 0 (0%), zero 4303 (39%)
c [score-dist-4] max exp 508, different 30 (6%)
c [score-dist-4] median active exp 502, avg 498.8
c [simplification-4] removed 52 variables 0.5% (10951 remain 22%)
c [simplification-4] removed 325 irredundant clauses 0.4% (76496 remain 36%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 25000
c [simplification-4] penalized conflict interval 25000 = 1 * 25000
c [simplification-4] hard conflict limit 43521 (soft 31021 + delta 12500)
c [simplification-4] new conflict limit 31021 (hard 43521)
c 
c [simplification-5] limit 31021 conflicts (hard 43521) hit after 31021 conflicts
c [quatres-1] found 8289 quaternary clauses 30% in total
c [quatres-1-2] added 41 single-self-subsuming ternary resolvents
c [quatres-1-2] added 343 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 10951 free variables schedulable
c [ternres-1] 4182 ternary resolvents (267 bin, 3915 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 4300 xors of average arity 2.9
c [gauss-1] connected 12448 occurrences of 602 variables (average 20.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-9] removed 88 variables
c [basicprobe-2] limit 9649706 penalty 0 = 0 + 0
c [basicprobe-2-0] 6409 sched 60%, 80 failed, 15 lifted, 7548 hbrs
c [decomp-10] removed 269 variables
c [basicprobe-2-1] 6295 probes remain 59% after last round
c [basicprobe-2-1] 100 units = 85 failed (85%) + 15 lifted (15%)
c [basicprobe-2-1] removed 275 variables, found 7620 hbrs
c [bate-1] eliminated 165 asymmetric tautologies during probing
c [unhide-5] limit 385988 with penalty 0 = 0 + 0
c [unhide-5-5] 4 units, 2 failed, 262 tauts, 0 hbrs, 61154 literals
c [transred-1] limit 1929941 with penalty 0 = 0 + 0
c [transred-1] removed 781 transitive binary clauses
c [transred-1] found 7 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 10543 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 160 blocked clauses
c [block-1] 160 < 1/100 * 73400 = 734 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 24 clauses out of 120 (20%) of length 12
c [cce-1-1] eliminated 50 clauses out of 455 (11%) of length 11
c [cce-1-1] eliminated 7 clauses out of 297 (2%) of length 10
c [cce-1-1] eliminated 110 clauses out of 1091 (10%) of length 9
c [cce-1-1] eliminated 114 clauses out of 1534 (7%) of length 8
c [cce-1-1] eliminated 41 clauses out of 2865 (1%) of length 7
c [cce-1-1] eliminated 523 clauses out of 4243 (12%) of length 6
c [cce-1-1] eliminated 14 clauses out of 5569 (0%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 883 large clauses in 30000022 steps
c [cce-1-1] allowing another 15000011 steps for small clauses
c [cce-1-1] scheduling 43640 clauses = 37207 binary + 6433 ternary
c [cce-1-1] tried to eliminate 5551 small clauses 13%
c [cce-1-1] eliminated 480 binary clauses 1%
c [cce-1-1] eliminated 67 ternary clauses 1%
c [cce-1-1] eliminated 547 small clauses 1%
c [cce-1-1] eliminated 547 small clauses in 30000009 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1430 covered clauses in round 1
c [cce-1] eliminated 1430 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 143550 added (scaled 2)
c [bca-1] 12167 out of 21076 literals actually usable 58%
c [bca-1] added 4 blocked clauses in 59351 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3819 pos 36.2% + 6718 neg 63.8% = 10537 sched 100.0% ret 0
c [sweep-1-1] 1046728 steps 44 queries 782.27 avg class size
c [sweep-1-1] 1594 decisions 39 SAT calls 148.87 avg env size
c [sweep-1-1] 9807 variables remain 93% (724 retained 7%)
c [decomp-11] removed 16 variables
c [sweep-1-1] removed 16 vars (0 failed, 5 eqs, 7 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 16 vars in TOTAL (1 rounds, 43 queries)
c [phase-count-5] 66424 negative 92.9% of 71466 except 5042 7.1%
c [phase-count-5] 61818 positive 86.5% of 71466 except 9648 13.5%
c [phase-5] phase bias: 31 positive 100%, 0 negative 0%
c [sort-queue-5] sorted 3018 enqueued variables after 31021 conflicts
c [score-dist-5] active 7503 (71%), one 0 (0%), zero 3018 (29%)
c [score-dist-5] max exp 509, different 124 (24%)
c [score-dist-5] median active exp 501, avg 489.4
c [simplification-5] removed 430 variables 3.9% (10521 remain 21%)
c [simplification-5] removed 5030 irredundant clauses 6.6% (71466 remain 34%)
c [simplification-5] maximum reduction of 7% = max (4%, 7%)
c [simplification-5] large reduction 7% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 43021 (soft 33021 + delta 10000)
c [simplification-5] new conflict limit 33021 (hard 43021)
c 
c [simplification-6] limit 33021 conflicts (hard 43021) hit after 33023 conflicts
c [quatres-2] found 8342 quaternary clauses 32% in total
c [quatres-2-1] removed 2 duplicate quaternary clauses
c [quatres-2-2] added 14 single-self-subsuming ternary resolvents
c [quatres-2-2] added 405 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 10521 free variables schedulable
c [ternres-2] 61 ternary resolvents (2 bin, 59 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 331 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 331 out of 331 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 3515 xors of average arity 3.0
c [gauss-2] connected 10469 occurrences of 462 variables (average 22.7)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 64 schedulable variables 1%
c [simpleprobe-3] limit 8333621 penalty 0 = 0 + 0
c [decomp-13] removed 448 variables
c [simpleprobe-3] 783 variables remain 8% (9290 retained 92%)
c [simpleprobe-3] removed 448 variables, found 2150 hbrs, 18 units
c [unhide-6] limit 416681 with penalty 0 = 0 + 0
c [unhide-6-6] 2 units, 2 failed, 1228 tauts, 0 hbrs, 114431 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 636 transitive binary clauses
c [transred-2] found 3 units
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 6 clauses out of 880 (1%) of length 9
c [cce-2-1] eliminated 6 clauses out of 1258 (0%) of length 8
c [cce-2-1] eliminated 35 clauses out of 2737 (1%) of length 7
c [cce-2-1] eliminated 15 clauses out of 3757 (0%) of length 6
c [cce-2-1] eliminated 221 clauses out of 5264 (4%) of length 5
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 283 large clauses in 30000007 steps
c [cce-2-1] allowing another 15000003 steps for small clauses
c [cce-2-1] scheduling 40165 clauses = 34168 binary + 5997 ternary
c [cce-2-1] tried to eliminate 6786 small clauses 17%
c [cce-2-1] eliminated 569 binary clauses 2%
c [cce-2-1] eliminated 88 ternary clauses 1%
c [cce-2-1] eliminated 657 small clauses 2%
c [cce-2-1] eliminated 698 small clauses in 30000111 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 981 covered clauses in round 1
c [cce-2] eliminated 981 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 10067 variables 100%
c [elim-5] limit of 20834052 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 295 variables 3% in round 1 in 15420395 steps
c [elim-5-1] backward subsumption/strengthening limit 5413657
c [elim-5-1-1] backward checking 2715 touched variables 27%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 10 and strengthened 12 clauses in 2661865 steps
c [elim-5-1] rescheduled 65 variables 1% by backward subsumption
c [elim-5-2] eliminated 3 variables 0% in round 2 in 56347 steps
c [elim-5-2] backward subsumption/strengthening limit 56300
c [elim-5-2-1] backward checking 27 touched variables 0%
c [elim-5-2-1] incomplete backward checking 0 remain 0%
c [elim-5-2] subsumed 2 and strengthened 5 clauses in 56301 steps
c [elim-5-2] rescheduled 11 variables 0% by backward subsumption
c [elim-5-3] eliminated 2 variables 0% in round 3 in 24460 steps
c [elim-5-3] backward subsumption/strengthening limit 24400
c [elim-5-3-1] backward checking 10 touched variables 0%
c [elim-5-3-1] incomplete backward checking 0 remain 0%
c [elim-5-3] subsumed 0 and strengthened 1 clauses in 24401 steps
c [elim-5] incomplete 5 not tried 0% in round 3
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 300 = 3% variables out of 10067 scheduled
c [bca-2] limit of 10000000 steps and 131528 added (scaled 2)
c [bca-2] 11064 out of 19536 literals actually usable 57%
c [bca-2] added 30 blocked clauses in 51348 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 3080 pos 33.9% + 6018 neg 66.1% = 9098 sched 93.2% ret 669
c [sweep-2-1] 1001155 steps 74 queries 504.39 avg class size
c [sweep-2-1] 2136 decisions 68 SAT calls 96.65 avg env size
c [sweep-2-1] 7666 variables remain 78% (2101 retained 22%)
c [decomp-14] removed 14 variables
c [sweep-2-1] removed 14 vars (0 failed, 5 eqs, 10 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 14 vars in TOTAL (1 rounds, 73 queries)
c [phase-count-6] 61535 negative 93.9% of 65511 except 3976 6.1%
c [phase-count-6] 56336 positive 86.0% of 65511 except 9175 14.0%
c [phase-count-6] less non-negative clauses 3976 than limit 6500 (10.0%)
c [phase-count-6] non-pos/non-neg = 9175/3976 = 2.31 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 36 negative 100%
c [sort-queue-6] sorted 2780 enqueued variables after 33023 conflicts
c [score-dist-6] active 6973 (71%), one 0 (0%), zero 2780 (29%)
c [score-dist-6] max exp 510, different 131 (26%)
c [score-dist-6] median active exp 501, avg 490.9
c [simplification-6] removed 768 variables 7.3% (9753 remain 19%)
c [simplification-6] removed 5955 irredundant clauses 8.3% (65511 remain 31%)
c [simplification-6] maximum reduction of 8% = max (7%, 8%)
c [simplification-6] large reduction 8% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 45023 (soft 35023 + delta 10000)
c [simplification-6] new conflict limit 35023 (hard 45023)
c 
c [simplification-7] limit 35023 conflicts (hard 45023) hit after 35024 conflicts
c [quatres-3] found 8490 quaternary clauses 33% in total
c [quatres-3-1] removed 5 duplicate quaternary clauses
c [quatres-3-2] added 7 single-self-subsuming ternary resolvents
c [quatres-3-2] added 281 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 9753 free variables schedulable
c [ternres-3] 151 ternary resolvents (2 bin, 149 trn)
c [ternres-3] fully completed ternary resolution
c [unhide-7] limit 443982 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 0 failed, 79 tauts, 0 hbrs, 18485 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 340 transitive binary clauses
c [transred-3] found 3 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 9750 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 9 blocked clauses
c [block-2] 9 < 1/100 * 65404 = 654 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 9 clauses out of 410 (2%) of length 11
c [cce-3-1] eliminated 3 clauses out of 310 (1%) of length 10
c [cce-3-1] eliminated 4 clauses out of 548 (1%) of length 9
c [cce-3-1] eliminated 6 clauses out of 981 (1%) of length 8
c [cce-3-1] eliminated 101 clauses out of 3244 (3%) of length 7
c [cce-3-1] eliminated 120 clauses out of 3818 (3%) of length 6
c [cce-3-1] eliminated 86 clauses out of 4907 (2%) of length 5
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 329 large clauses in 30000007 steps
c [cce-3-1] allowing another 15000003 steps for small clauses
c [cce-3-1] scheduling 38007 clauses = 32408 binary + 5599 ternary
c [cce-3-1] tried to eliminate 6668 small clauses 18%
c [cce-3-1] eliminated 914 binary clauses 3%
c [cce-3-1] eliminated 82 ternary clauses 1%
c [cce-3-1] eliminated 996 small clauses 3%
c [cce-3-1] eliminated 996 small clauses in 30000004 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1325 covered clauses in round 1
c [cce-3] eliminated 1325 covered clauses in TOTAL during 1 rounds
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 9750 variables 100%
c [elim-6] limit of 44398234 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 140 variables 1% in round 1 in 14566159 steps
c [elim-6-1] backward subsumption/strengthening limit 14566100
c [elim-6-1-1] backward checking 938 touched variables 10%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 6 and strengthened 6 clauses in 1699195 steps
c [elim-6-1] rescheduled 37 variables 0% by backward subsumption
c [elim-6-2] eliminated 3 variables 0% in round 2 in 37158 steps
c [elim-6-2] backward subsumption/strengthening limit 37100
c [elim-6-2-1] backward checking 28 touched variables 0%
c [elim-6-2-1] incomplete backward checking 24 remain 86%
c [elim-6-2] subsumed 0 and strengthened 0 clauses in 38529 steps
c [elim-6-2] fully rescheduled 9607 variables 99%
c [elim-6-3] eliminated 15 variables 0% in round 3 in 14505202 steps
c [elim-6-3] backward subsumption/strengthening limit 13551991
c [elim-6-3-1] backward checking 153 touched variables 2%
c [elim-6-3-1] fully completed backward checking in 1 rounds
c [elim-6-3] subsumed 2 and strengthened 5 clauses in 181824 steps
c [elim-6] incomplete 19 not tried 0% in round 3
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 158 = 2% variables out of 9750 scheduled
c [bca-3] limit of 10000000 steps and 127591 added (scaled 2)
c [bca-3] 10779 out of 19186 literals actually usable 56%
c [bca-3] added 68 blocked clauses in 50409 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2558 pos 34.1% + 4954 neg 65.9% = 7512 sched 78.3% ret 2080
c [sweep-3-1] 1002553 steps 77 queries 431.23 avg class size
c [sweep-3-1] 2046 decisions 73 SAT calls 73.81 avg env size
c [sweep-3-1] 6637 variables remain 69% (2955 retained 31%)
c [decomp-16] removed 6 variables
c [sweep-3-1] removed 6 vars (0 failed, 6 eqs, 12 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 6 vars in TOTAL (1 rounds, 76 queries)
c [phase-count-7] 59768 negative 94.1% of 63535 except 3767 5.9%
c [phase-count-7] 54762 positive 86.2% of 63535 except 8773 13.8%
c [phase-count-7] less non-negative clauses 3767 than limit 6300 (10.0%)
c [phase-count-7] non-pos/non-neg = 8773/3767 = 2.33 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 29 negative 100%
c [sort-queue-7] sorted 2650 enqueued variables after 35024 conflicts
c [score-dist-7] active 6936 (72%), one 0 (0%), zero 2650 (28%)
c [score-dist-7] max exp 510, different 137 (27%)
c [score-dist-7] median active exp 501, avg 490.2
c [simplification-7] removed 167 variables 1.7% (9586 remain 19%)
c [simplification-7] removed 1976 irredundant clauses 3.0% (63535 remain 30%)
c [simplification-7] maximum reduction of 3% = max (2%, 3%)
c [simplification-7] geometric conflict interval increment 6250 = 25000 / 4
c [simplification-7] new conflict interval 31250
c [simplification-7] penalized conflict interval 31250 = 1 * 31250
c [simplification-7] hard conflict limit 81899 (soft 66274 + delta 15625)
c [simplification-7] new conflict limit 66274 (hard 81899)
c 
c [simplification-8] limit 66274 conflicts (hard 81899) hit after 66274 conflicts
c [quatres-4] found 8973 quaternary clauses 32% in total
c [quatres-4-1] removed 6 duplicate quaternary clauses
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 14 single-self-subsuming ternary resolvents
c [quatres-4-2] added 168 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 9586 free variables schedulable
c [ternres-4] 85 ternary resolvents (1 bin, 84 trn)
c [ternres-4] 16 variables remain 0% (9570 retained 100%)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 1479 xors of average arity 3.0
c [gauss-3] connected 4413 occurrences of 448 variables (average 9.9)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 2 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 464 transitive binary clauses
c [transred-4] found 10 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 3 clauses out of 304 (1%) of length 10
c [cce-4-1] eliminated 2 clauses out of 548 (0%) of length 9
c [cce-4-1] eliminated 3 clauses out of 967 (0%) of length 8
c [cce-4-1] eliminated 6 clauses out of 3159 (0%) of length 7
c [cce-4-1] eliminated 29 clauses out of 3762 (1%) of length 6
c [cce-4-1] eliminated 289 clauses out of 4885 (6%) of length 5
c [cce-4-1] eliminated 978 clauses out of 7053 (14%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 1310 large clauses in 40118564 steps
c [cce-4-1] allowing another 20059282 steps for small clauses
c [cce-4-1] scheduling 36317 clauses = 30849 binary + 5468 ternary
c [cce-4-1] tried to eliminate 36317 small clauses 100%
c [cce-4-1] eliminated 1550 binary clauses 5%
c [cce-4-1] eliminated 299 ternary clauses 5%
c [cce-4-1] eliminated 1849 small clauses 5%
c [cce-4-1] eliminated 1925 small clauses in 93673696 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 3235 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 17470531 steps for small clauses
c [cce-4-2] scheduling 34468 clauses = 29299 binary + 5169 ternary
c [cce-4-2] tried to eliminate 34468 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 3235 covered clauses in TOTAL during 2 rounds
c [elim-7] no untried remaining variables left
c [elim-7] scheduled 9573 variables 100%
c [elim-7] limit of 78166288 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 180 variables 2% in round 1 in 13322916 steps
c [elim-7-1] backward subsumption/strengthening limit 13322900
c [elim-7-1-1] backward checking 1214 touched variables 13%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 7 and strengthened 13 clauses in 1409425 steps
c [elim-7-1] rescheduled 67 variables 1% by backward subsumption
c [elim-7-2] eliminated 4 variables 0% in round 2 in 58571 steps
c [elim-7-2] backward subsumption/strengthening limit 58500
c [elim-7-2-1] backward checking 19 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 1 and strengthened 0 clauses in 29590 steps
c [elim-7-2] rescheduled 3 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 2283 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 184 = 2% variables out of 9573 scheduled
c [bca-4] limit of 10000000 steps and 120083 added (scaled 2)
c [bca-4] 9811 out of 18780 literals actually usable 52%
c [bca-4] added 41 blocked clauses in 68555 steps
c [sweep-4] limit 1172494 penalty 0 = 0 + 0
c [sweep-4-1] 2220 pos 34.2% + 4265 neg 65.8% = 6485 sched 69.1% ret 2904
c [sweep-4-1] 1172955 steps 92 queries 457.39 avg class size
c [sweep-4-1] 2700 decisions 88 SAT calls 85.59 avg env size
c [sweep-4-1] 5393 variables remain 58% (3985 retained 42%)
c [decomp-18] removed 14 variables
c [sweep-4-1] removed 14 vars (0 failed, 3 eqs, 7 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 14 vars in TOTAL (1 rounds, 91 queries)
c [phase-count-8] 56164 negative 94.0% of 59718 except 3554 6.0%
c [phase-count-8] 51386 positive 86.0% of 59718 except 8332 14.0%
c [phase-count-8] less non-negative clauses 3554 than limit 5900 (10.0%)
c [phase-count-8] non-pos/non-neg = 8332/3554 = 2.34 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 12 negative 100%
c [sort-queue-8] sorted 2356 enqueued variables after 66274 conflicts
c [score-dist-8] active 7019 (75%), one 0 (0%), zero 2356 (25%)
c [score-dist-8] max exp 510, different 215 (42%)
c [score-dist-8] median active exp 493, avg 471.3
c [simplification-8] removed 211 variables 2.2% (9375 remain 19%)
c [simplification-8] removed 3817 irredundant clauses 6.0% (59718 remain 28%)
c [simplification-8] maximum reduction of 6% = max (2%, 6%)
c [simplification-8] large reduction 6% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 78274 (soft 68274 + delta 10000)
c [simplification-8] new conflict limit 68274 (hard 78274)
c 
c [simplification-9] limit 68274 conflicts (hard 78274) hit after 68274 conflicts
c [quatres-5] found 8165 quaternary clauses 31% in total
c [quatres-5-1] removed 12 duplicate quaternary clauses
c [quatres-5-2] added 8 single-self-subsuming ternary resolvents
c [quatres-5-2] added 133 quaternary resolvents
c [ternres-5] limit 4009492 with penalty 0 = 0 + 0
c [ternres-5] 16 schedulable variables 0%
c [ternres-5] 29 ternary resolvents (2 bin, 27 trn)
c [ternres-5] fully completed ternary resolution
c [treelook-3] limit 100237 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 8183 literals 44%
c [treelook-3] scheduling used 100317 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 100237 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 104136 steps
c [treelook-3] 8103 literals remain 43%
c [treelook-3] 7069 variables remain to probed next time 75%
c [treelook-3] removed 0 variables, found 69 hbrs
c [unhide-8] limit 400949 with penalty 1 = 1 + 0
c [unhide-8-8] 0 units, 20 failed, 852 tauts, 0 hbrs, 89631 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 383 transitive binary clauses
c [transred-5] found 2 units
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 14
c [cce-5-1] eliminated 1 clauses out of 42 (2%) of length 12
c [cce-5-1] eliminated 2 clauses out of 387 (1%) of length 11
c [cce-5-1] eliminated 5 clauses out of 301 (2%) of length 10
c [cce-5-1] eliminated 4 clauses out of 553 (1%) of length 9
c [cce-5-1] eliminated 4 clauses out of 914 (0%) of length 8
c [cce-5-1] eliminated 20 clauses out of 3115 (1%) of length 7
c [cce-5-1] eliminated 81 clauses out of 3802 (2%) of length 6
c [cce-5-1] eliminated 114 clauses out of 4565 (2%) of length 5
c [cce-5-1] eliminated 1 clauses out of 6162 (0%) of length 4
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 233 large clauses in 30000001 steps
c [cce-5-1] allowing another 15000000 steps for small clauses
c [cce-5-1] scheduling 34632 clauses = 28688 binary + 5944 ternary
c [cce-5-1] tried to eliminate 7403 small clauses 21%
c [cce-5-1] eliminated 561 binary clauses 2%
c [cce-5-1] eliminated 111 ternary clauses 2%
c [cce-5-1] eliminated 672 small clauses 2%
c [cce-5-1] eliminated 731 small clauses in 30000005 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 964 covered clauses in round 1
c [cce-5] eliminated 964 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 9364 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1603796900 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 153 variables 2% in round 1 in 12631418 steps
c [elim-8-1] backward subsumption/strengthening limit 12631400
c [elim-8-1-1] backward checking 1026 touched variables 11%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1 and strengthened 11 clauses in 1293928 steps
c [elim-8-1] rescheduled 33 variables 0% by backward subsumption
c [elim-8-2] eliminated 2 variables 0% in round 2 in 87806 steps
c [elim-8-2] backward subsumption/strengthening limit 87800
c [elim-8-2-1] backward checking 28 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 64528 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 156 = 2% variables out of 9364 scheduled
c [bca-5] limit of 10000000 steps and 117123 added (scaled 2)
c [bca-5] 9708 out of 18418 literals actually usable 53%
c [bca-5] added 60 blocked clauses in 60856 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 12028470 penalty 0 = 0 + 0
c [sweep-5-1] 1800 pos 34.1% + 3482 neg 65.9% = 5282 sched 57.4% ret 3926
c [sweep-5-1] 7585651 steps 858 queries 45.59 avg class size
c [sweep-5-1] 13457 decisions 746 SAT calls 47.07 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-21] removed 127 variables
c [sweep-5-1] removed 127 vars (0 failed, 123 eqs, 210 impls)
c [sweep-5-2] 3039 pos 33.5% + 6042 neg 66.5% = 9081 sched 100.0% ret 0
c [sweep-5-2] 4848903 steps 381 queries 126.02 avg class size
c [sweep-5-2] 8059 decisions 355 SAT calls 60.83 avg env size
c [sweep-5-2] 2545 variables remain 28% (6534 retained 72%)
c [decomp-22] removed 36 variables
c [sweep-5-2] removed 36 vars (0 failed, 28 eqs, 50 impls)
c [sweep-5] removed 163 vars in TOTAL (2 rounds, 1237 queries)
c [sort-queue-9] sorted 1621 enqueued variables after 68274 conflicts
c [score-dist-9] active 7424 (82%), one 0 (0%), zero 1621 (18%)
c [score-dist-9] max exp 511, different 210 (41%)
c [score-dist-9] median active exp 503, avg 485.2
c [simplification-9] removed 330 variables 3.5% (9045 remain 18%)
c [simplification-9] removed 1525 irredundant clauses 2.6% (58193 remain 28%)
c [simplification-9] maximum reduction of 4% = max (4%, 3%)
c [simplification-9] geometric conflict interval increment 6250 = 31250 / 5
c [simplification-9] new conflict interval 37500
c [simplification-9] penalized conflict interval 37500 = 1 * 37500
c [simplification-9] hard conflict limit 124524 (soft 105774 + delta 18750)
c [simplification-9] new conflict limit 105774 (hard 124524)
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 -   36.8    9045    58193     90619   28675   4043 12742   43    70   12  62%    760   10   44   27  164%
c 
c [simplification-10] limit 105774 conflicts (hard 124524) hit after 105775 conflicts
c [quatres-6] found 8506 quaternary clauses 31% in total
c [quatres-6-1] removed 8 duplicate quaternary clauses
c [quatres-6-2] added 25 single-self-subsuming ternary resolvents
c [quatres-6-2] added 123 quaternary resolvents
c [ternres-6] limit 6150917 with penalty 0 = 0 + 0
c [ternres-6] all 9045 free variables schedulable
c [ternres-6] 354 ternary resolvents (7 bin, 347 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 384432 penalty 3 = 3 + 0
c [card-4] found 208 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 384432 for elimination
c [card-4] 208 out of 208 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-23] removed 3 variables
c [basicprobe-3] limit 30754587 penalty 0 = 0 + 0
c [basicprobe-3-0] 5161 sched 57%, 30 failed, 0 lifted, 2009 hbrs
c [decomp-24] removed 37 variables
c [basicprobe-3-1] 5290 sched 59%, 9 failed, 0 lifted, 392 hbrs
c [decomp-25] removed 10 variables
c [basicprobe-3-2] 5267 sched 59%, 0 failed, 0 lifted, 73 hbrs
c [basicprobe-3-3] 5262 sched 58%, 0 failed, 0 lifted, 20 hbrs
c [basicprobe-3-4] 2635 probes remain 29% after last round
c [basicprobe-3-4] 39 units = 39 failed (100%) + 0 lifted (0%)
c [basicprobe-3-4] removed 47 variables, found 2497 hbrs
c [bate-2] eliminated 43 asymmetric tautologies during probing
c [unhide-9] limit 1230183 with penalty 0 = 0 + 0
c [unhide-9-10] 0 units, 0 failed, 1135 tauts, 0 hbrs, 128921 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 810 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 8995 variables 100%
c [block-3] limit of 15377293 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 34 blocked clauses
c [block-3] 34 < 1/100 * 57295 = 572 considered unsuccessful
c [cce-6] limit of 30754587 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 41 (2%) of length 12
c [cce-6-1] eliminated 6 clauses out of 386 (2%) of length 11
c [cce-6-1] eliminated 9 clauses out of 297 (3%) of length 10
c [cce-6-1] eliminated 4 clauses out of 546 (1%) of length 9
c [cce-6-1] eliminated 24 clauses out of 873 (3%) of length 8
c [cce-6-1] eliminated 19 clauses out of 2991 (1%) of length 7
c [cce-6-1] eliminated 56 clauses out of 3743 (1%) of length 6
c [cce-6-1] eliminated 152 clauses out of 4416 (3%) of length 5
c [cce-6-1] eliminated 112 clauses out of 6088 (2%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 383 large clauses in 30713764 steps
c [cce-6-1] allowing another 15356882 steps for small clauses
c [cce-6-1] scheduling 32212 clauses = 27107 binary + 5105 ternary
c [cce-6-1] tried to eliminate 9261 small clauses 29%
c [cce-6-1] eliminated 47 binary clauses 0%
c [cce-6-1] eliminated 22 ternary clauses 0%
c [cce-6-1] eliminated 69 small clauses 0%
c [cce-6-1] eliminated 69 small clauses in 30754643 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 452 covered clauses in round 1
c [cce-6] eliminated 452 covered clauses in TOTAL during 1 rounds
c [cce-6] 452 < 1/100 * 57261 = 572 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 8992 variables 100%
c [elim-9] limit of 123018351 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 166 variables 2% in round 1 in 12010262 steps
c [elim-9-1] backward subsumption/strengthening limit 12010200
c [elim-9-1-1] backward checking 1147 touched variables 13%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 5 and strengthened 22 clauses in 2488964 steps
c [elim-9-1] rescheduled 90 variables 1% by backward subsumption
c [elim-9-2] eliminated 5 variables 0% in round 2 in 2582628 steps
c [elim-9-2] backward subsumption/strengthening limit 2582600
c [elim-9-2-1] backward checking 53 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 6 clauses in 1583666 steps
c [elim-9-2] rescheduled 29 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 2490705 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 171 = 2% variables out of 8992 scheduled
c [bca-6] limit of 10000000 steps and 113223 added (scaled 2)
c [bca-6] 8623 out of 17644 literals actually usable 49%
c [bca-6] added 24 blocked clauses in 56222 steps
c [sweep-6] limit 1845275 penalty 0 = 0 + 0
c [sweep-6-1] 830 pos 33.7% + 1631 neg 66.3% = 2461 sched 27.9% ret 6360
c [sweep-6-1] 1860359 steps 216 queries 98.04 avg class size
c [sweep-6-1] 3359 decisions 202 SAT calls 40.03 avg env size
c [sweep-6-1] 1403 variables remain 16% (7417 retained 84%)
c [decomp-28] removed 18 variables
c [sweep-6-1] removed 18 vars (0 failed, 17 eqs, 27 impls)
c [sweep-6] removed 18 vars in TOTAL (1 rounds, 215 queries)
c [sort-queue-10] sorted 1326 enqueued variables after 105775 conflicts
c [score-dist-10] active 7477 (85%), one 0 (0%), zero 1326 (15%)
c [score-dist-10] max exp 510, different 274 (54%)
c [score-dist-10] median active exp 490, avg 453.8
c [simplification-10] removed 242 variables 2.7% (8803 remain 17%)
c [simplification-10] removed 1892 irredundant clauses 3.3% (56301 remain 27%)
c [simplification-10] maximum reduction of 3% = max (3%, 3%)
c [simplification-10] geometric conflict interval increment 9375 = 37500 / 4
c [simplification-10] new conflict interval 46875
c [simplification-10] penalized conflict interval 46875 = 1 * 46875
c [simplification-10] hard conflict limit 176087 (soft 152650 + delta 23437)
c [simplification-10] new conflict limit 152650 (hard 176087)
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 -   49.6    8803    56301    132425   32053   4213 12617   44    72   16  61%    884   11   34   30  115%
c 
c [simplification-11] limit 152650 conflicts (hard 176087) hit after 155419 conflicts
c [quatres-7] found 8494 quaternary clauses 30% in total
c [quatres-7-1] removed 11 duplicate quaternary clauses
c [quatres-7-2] added 21 single-self-subsuming ternary resolvents
c [quatres-7-2] added 179 quaternary resolvents
c [ternres-7] limit 8993785 with penalty 0 = 0 + 0
c [ternres-7] all 8803 free variables schedulable
c [ternres-7] 270 ternary resolvents (10 bin, 260 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-4] limit 500000 penalty 2 = 2 + 0
c [gauss-4] extracted 597 xors of average arity 3.0
c [gauss-4] connected 1783 occurrences of 311 variables (average 5.7)
c [gauss-4] limit 500000 penalty 2 = 2 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-29] removed 6 variables
c [simpleprobe-4] 652 schedulable variables 7%
c [simpleprobe-4] limit 35975143 penalty 0 = 0 + 0
c [decomp-30] removed 43 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 43 variables, found 919 hbrs, 2 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 939 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 8754 variables 100%
c [elim-10] limit of 179875716 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 18 variables 0% in round 1 in 11819201 steps
c [elim-10-1] backward subsumption/strengthening limit 11819200
c [elim-10-1-1] backward checking 312 touched variables 4%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 1 and strengthened 3 clauses in 777080 steps
c [elim-10-1] rescheduled 21 variables 0% by backward subsumption
c [elim-10-2] eliminated 1 variables 0% in round 2 in 76246 steps
c [elim-10-2] backward subsumption/strengthening limit 76200
c [elim-10-2-1] backward checking 9 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 23623 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 19 = 0% variables out of 8754 scheduled
c [elim-10] 19 < 1/100 * 8754 = 87 considered unsuccessful
c [bca-7] limit of 10000000 steps and 112403 added (scaled 2)
c [bca-7] 8125 out of 17472 literals actually usable 47%
c [bca-7] added 10 blocked clauses in 74182 steps
c [sweep-7] limit 2698135 penalty 0 = 0 + 0
c [sweep-7-1] 473 pos 34.1% + 913 neg 65.9% = 1386 sched 15.9% ret 7349
c [sweep-7-1] 2701979 steps 246 queries 39.74 avg class size
c [sweep-7-1] 4728 decisions 230 SAT calls 62.09 avg env size
c [sweep-7-1] 441 variables remain 5% (8294 retained 95%)
c [decomp-31] removed 19 variables
c [sweep-7-1] removed 19 vars (0 failed, 18 eqs, 30 impls)
c [sweep-7] removed 19 vars in TOTAL (1 rounds, 245 queries)
c [sort-queue-11] sorted 1280 enqueued variables after 155419 conflicts
c [score-dist-11] active 7436 (85%), one 63 (1%), zero 1217 (14%)
c [score-dist-11] max exp 510, different 297 (58%)
c [score-dist-11] median active exp 501, avg 440.5
c [simplification-11] removed 87 variables 1.0% (8716 remain 17%)
c [simplification-11] removed 414 irredundant clauses 0.7% (55887 remain 27%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 23437 = 46875 / 2
c [simplification-11] new conflict interval 70312
c [simplification-11] penalized conflict interval 70312 = 1 * 70312
c [simplification-11] hard conflict limit 260887 (soft 225731 + delta 35156)
c [simplification-11] new conflict limit 225731 (hard 260887)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   57.9    8716    55887    163231   33353   4523 12570   44    72   12  62%    937   11   41   32  131%
c -   65.9    8716    55887    193576   32831   4558 12583   45    63   18  71%    969    4   57   33  172%
c -   75.2    8716    55887    226333   34278   4600 12595   37    51   19  73%    991   -7   37   35  107%
c 
c [simplification-12] limit 225731 conflicts (hard 260887) hit after 231050 conflicts
c [quatres-8] found 8772 quaternary clauses 30% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 12 single-self-subsuming ternary resolvents
c [quatres-8-2] added 44 quaternary resolvents
c [ternres-8] limit 14590041 with penalty 0 = 0 + 0
c [ternres-8] all 8716 free variables schedulable
c [ternres-8] 113 ternary resolvents (10 bin, 103 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-32] removed 4 variables
c [unhide-10] limit 1459004 with penalty 1 = 1 + 0
c [unhide-10-12] 0 units, 0 failed, 677 tauts, 0 hbrs, 76838 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 305 transitive binary clauses
c [cce-7] limit of 36475102 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 19 clauses out of 379 (5%) of length 11
c [cce-7-1] eliminated 13 clauses out of 281 (5%) of length 10
c [cce-7-1] eliminated 3 clauses out of 553 (1%) of length 9
c [cce-7-1] eliminated 6 clauses out of 795 (1%) of length 8
c [cce-7-1] eliminated 16 clauses out of 2937 (1%) of length 7
c [cce-7-1] eliminated 44 clauses out of 3685 (1%) of length 6
c [cce-7-1] eliminated 74 clauses out of 4251 (2%) of length 5
c [cce-7-1] eliminated 300 clauses out of 6103 (5%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 475 large clauses in 31333240 steps
c [cce-7-1] allowing another 15666620 steps for small clauses
c [cce-7-1] scheduling 31735 clauses = 26136 binary + 5599 ternary
c [cce-7-1] tried to eliminate 10616 small clauses 33%
c [cce-7-1] eliminated 582 binary clauses 2%
c [cce-7-1] eliminated 122 ternary clauses 2%
c [cce-7-1] eliminated 704 small clauses 2%
c [cce-7-1] eliminated 704 small clauses in 36475105 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1179 covered clauses in round 1
c [cce-7] eliminated 1179 covered clauses in TOTAL during 1 rounds
c [bca-8] limit of 10000000 steps and 109854 added (scaled 2)
c [bca-8] 8434 out of 17426 literals actually usable 48%
c [bca-8] added 34 blocked clauses in 60346 steps
c [sweep-8] limit 4377012 penalty 0 = 0 + 0
c [sweep-8-1] 160 pos 36.4% + 280 neg 63.6% = 440 sched 5.1% ret 8272
c [sweep-8-1] 1428838 steps 212 queries 16.29 avg class size
c [sweep-8-1] 2462 decisions 193 SAT calls 33.02 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-33] removed 23 variables
c [sweep-8-1] removed 23 vars (0 failed, 18 eqs, 36 impls)
c [sweep-8-2] 2871 pos 33.0% + 5818 neg 67.0% = 8689 sched 100.0% ret 0
c [sweep-8-2] 2950889 steps 188 queries 259.66 avg class size
c [sweep-8-2] 4746 decisions 184 SAT calls 60.66 avg env size
c [sweep-8-2] 4397 variables remain 51% (4292 retained 49%)
c [decomp-34] removed 4 variables
c [sweep-8-2] removed 4 vars (0 failed, 5 eqs, 10 impls)
c [sweep-8] removed 27 vars in TOTAL (2 rounds, 398 queries)
c [sort-queue-12] sorted 1938 enqueued variables after 231050 conflicts
c [score-dist-12] active 6747 (78%), one 799 (9%), zero 1139 (13%)
c [score-dist-12] max exp 510, different 304 (59%)
c [score-dist-12] median active exp 502, avg 457.7
c [simplification-12] removed 31 variables 0.4% (8685 remain 17%)
c [simplification-12] removed 1278 irredundant clauses 2.3% (54609 remain 26%)
c [simplification-12] maximum reduction of 2% = max (0%, 2%)
c [simplification-12] geometric conflict interval increment 23437 = 70312 / 3
c [simplification-12] new conflict interval 93749
c [simplification-12] penalized conflict interval 93749 = 1 * 93749
c [simplification-12] hard conflict limit 371673 (soft 324799 + delta 46874)
c [simplification-12] new conflict limit 324799 (hard 371673)
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 -   86.2    8685    54609    258937   34950   4697 12652   31    43   17  73%   1004  -10   36   34  105%
c -   95.9    8685    54609    292329   36172   4714 12660   35    43   18  82%   1012   -7   36   34  107%
c -  106.3    8685    54609    325488   36289   4743 12664   25    34   18  73%   1017  -12   25   32   78%
c -  116.4    8685    54609    360837   37086   4768 12679   23    31   19  74%   1020  -10   19   29   68%
c 
c [simplification-13] limit 324799 conflicts (hard 371673) hit after 371673 conflicts
c [quatres-9] found 8650 quaternary clauses 30% in total
c [quatres-9-1] removed 6 duplicate quaternary clauses
c [quatres-9-2] added 10 single-self-subsuming ternary resolvents
c [quatres-9-2] added 32 quaternary resolvents
c [ternres-9] limit 25554556 with penalty 0 = 0 + 0
c [ternres-9] all 8685 free variables schedulable
c [ternres-9] 244 ternary resolvents (9 bin, 235 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-35] removed 2 variables
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 503 transitive binary clauses
c [transred-9] found 2 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 1277727830 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 268 (0%) of length 10
c [cce-8-1] eliminated 2 clauses out of 550 (0%) of length 9
c [cce-8-1] eliminated 3 clauses out of 786 (0%) of length 8
c [cce-8-1] eliminated 10 clauses out of 2920 (0%) of length 7
c [cce-8-1] eliminated 22 clauses out of 3631 (1%) of length 6
c [cce-8-1] eliminated 18 clauses out of 4169 (0%) of length 5
c [cce-8-1] eliminated 5 clauses out of 5806 (0%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 61 large clauses in 27351132 steps
c [cce-8-1] allowing another 13675566 steps for small clauses
c [cce-8-1] scheduling 30502 clauses = 25470 binary + 5032 ternary
c [cce-8-1] tried to eliminate 30502 small clauses 100%
c [cce-8-1] eliminated 151 binary clauses 1%
c [cce-8-1] eliminated 60 ternary clauses 1%
c [cce-8-1] eliminated 211 small clauses 1%
c [cce-8-1] eliminated 234 small clauses in 62421337 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 295 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 13644764 steps for small clauses
c [cce-8-2] scheduling 30291 clauses = 25319 binary + 4972 ternary
c [cce-8-2] tried to eliminate 30291 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 295 covered clauses in TOTAL during 2 rounds
c [cce-8] 295 < 1/100 * 54532 = 545 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 8680 variables 100%
c [elim-11] limit of 255545566 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 205 variables 2% in round 1 in 11252862 steps
c [elim-11-1] backward subsumption/strengthening limit 11252800
c [elim-11-1-1] backward checking 1407 touched variables 16%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 2 and strengthened 12 clauses in 1171994 steps
c [elim-11-1] rescheduled 61 variables 1% by backward subsumption
c [elim-11-2] eliminated 3 variables 0% in round 2 in 120204 steps
c [elim-11-2] backward subsumption/strengthening limit 120200
c [elim-11-2-1] backward checking 46 touched variables 1%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 3 and strengthened 1 clauses in 45787 steps
c [elim-11-2] rescheduled 15 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 19191 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 208 = 2% variables out of 8680 scheduled
c [bca-9] limit of 10000000 steps and 108157 added (scaled 2)
c [bca-9] 7984 out of 16946 literals actually usable 47%
c [bca-9] added 18 blocked clauses in 59495 steps
c [sweep-9] limit 7666366 penalty 0 = 0 + 0
c [sweep-9-1] 1390 pos 32.7% + 2865 neg 67.3% = 4255 sched 50.2% ret 4217
c [sweep-9-1] 5366868 steps 723 queries 26.82 avg class size
c [sweep-9-1] 10652 decisions 696 SAT calls 42.21 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-36] removed 29 variables
c [sweep-9-1] removed 29 vars (0 failed, 28 eqs, 55 impls)
c [sweep-9-2] 2745 pos 32.5% + 5698 neg 67.5% = 8443 sched 100.0% ret 0
c [sweep-9-2] 2303021 steps 145 queries 249.95 avg class size
c [sweep-9-2] 3953 decisions 144 SAT calls 75.70 avg env size
c [sweep-9-2] 4543 variables remain 54% (3900 retained 46%)
c [sweep-9-2] removed 0 vars (0 failed, 0 eqs, 4 impls)
c [sweep-9] removed 29 vars in TOTAL (2 rounds, 866 queries)
c [sort-queue-13] sorted 2169 enqueued variables after 371673 conflicts
c [score-dist-13] active 6274 (74%), one 1221 (14%), zero 948 (11%)
c [score-dist-13] max exp 511, different 210 (41%)
c [score-dist-13] median active exp 503, avg 489.2
c [simplification-13] removed 242 variables 2.8% (8443 remain 17%)
c [simplification-13] removed 865 irredundant clauses 1.6% (53744 remain 26%)
c [simplification-13] maximum reduction of 3% = max (3%, 2%)
c [simplification-13] geometric conflict interval increment 23437 = 93749 / 4
c [simplification-13] new conflict interval 117186
c [simplification-13] penalized conflict interval 117186 = 1 * 117186
c [simplification-13] hard conflict limit 547452 (soft 488859 + delta 58593)
c [simplification-13] new conflict limit 488859 (hard 547452)
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 -  131.1    8443    53744    404565   37665   4822 11863   34    46   18  74%   1022    6   30   28  107%
c -  142.0    8443    53744    440242   38467   4840 11872   29    37   18  80%   1023   -6   20   31   64%
c -  153.1    8443    53744    477549   39446   4853 11877   27    33   19  84%   1023   -8   29   30   96%
c 
c [simplification-14] limit 488859 conflicts (hard 547452) hit after 492649 conflicts
c [quatres-10] found 8744 quaternary clauses 29% in total
c [quatres-10-1] removed 9 duplicate quaternary clauses
c [quatres-10-2] added 18 single-self-subsuming ternary resolvents
c [quatres-10-2] added 131 quaternary resolvents
c [ternres-10] limit 35027782 with penalty 0 = 0 + 0
c [ternres-10] all 8443 free variables schedulable
c [ternres-10] 183 ternary resolvents (9 bin, 174 trn)
c [ternres-10] fully completed ternary resolution
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 444 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 8443 variables 100%
c [block-4] limit of 43784728 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 13 blocked clauses
c [block-4] 13 < 1/100 * 53671 = 536 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 8443 variables 100%
c [elim-12] limit of 700555648 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 17 variables 0% in round 1 in 11124440 steps
c [elim-12-1] backward subsumption/strengthening limit 11124400
c [elim-12-1-1] backward checking 211 touched variables 2%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 0 and strengthened 1 clauses in 607793 steps
c [elim-12-1] rescheduled 5 variables 0% by backward subsumption
c [elim-12-2] no variable eliminated in round 2 in 4836 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 17 = 0% variables out of 8443 scheduled
c [elim-12] 17 < 1/100 * 8443 = 84 considered unsuccessful
c [bca-10] limit of 10000000 steps and 107756 added (scaled 2)
c [bca-10] 7586 out of 16854 literals actually usable 45%
c [bca-10] added 8 blocked clauses in 71399 steps
c [sweep-10] limit 10508334 penalty 0 = 0 + 0
c [sweep-10-1] 1404 pos 31.0% + 3129 neg 69.0% = 4533 sched 53.8% ret 3893
c [sweep-10-1] 6791393 steps 670 queries 47.63 avg class size
c [sweep-10-1] 11839 decisions 652 SAT calls 55.65 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-39] removed 15 variables
c [sweep-10-1] removed 15 vars (0 failed, 19 eqs, 43 impls)
c [sweep-10-2] 2658 pos 31.6% + 5753 neg 68.4% = 8411 sched 100.0% ret 0
c [sweep-10-2] 3726076 steps 233 queries 153.23 avg class size
c [sweep-10-2] 5376 decisions 231 SAT calls 77.27 avg env size
c [sweep-10-2] 3055 variables remain 36% (5356 retained 64%)
c [decomp-40] removed 3 variables
c [sweep-10-2] removed 3 vars (0 failed, 1 eqs, 2 impls)
c [sweep-10] removed 18 vars in TOTAL (2 rounds, 901 queries)
c [sort-queue-14] sorted 1637 enqueued variables after 492649 conflicts
c [score-dist-14] active 6771 (81%), one 850 (10%), zero 787 (9%)
c [score-dist-14] max exp 511, different 249 (49%)
c [score-dist-14] median active exp 503, avg 455.1
c [simplification-14] removed 35 variables 0.4% (8408 remain 17%)
c [simplification-14] removed 194 irredundant clauses 0.4% (53550 remain 25%)
c [simplification-14] maximum reduction of 0% = max (0%, 0%)
c [simplification-14] full geometric conflict interval increment 117186
c [simplification-14] new conflict interval 234372
c [simplification-14] penalized conflict interval 234372 = 1 * 234372
c [simplification-14] hard conflict limit 844207 (soft 727021 + delta 117186)
c [simplification-14] new conflict limit 727021 (hard 844207)
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 -  165.0    8408    53550    515502   39525   5082 11726   30    38   14  77%   1024   -1   37   29  128%
c -  177.4    8408    53550    555386   40999   5090 11727   28    33   20  86%   1024   -6   28   30   95%
c -  188.1    8408    53550    594611   41762   5115 11733   28    36   20  78%   1024   -3   23   29   80%
c -  198.1    8408    53550    632855   41745   5147 11736   28    36   20  78%   1024   -3   32   28  113%
c -  208.6    8408    53550    673474   42865   5171 11737   17    21   20  79%   1024  -15   17   26   65%
c -  220.0    8408    53550    714598   43959   5186 11739   23    31   20  73%   1024   -1   19   23   80%
c 
c [simplification-15] limit 727021 conflicts (hard 844207) hit after 748560 conflicts
c [quatres-11] found 9048 quaternary clauses 29% in total
c [quatres-11-1] removed 3 duplicate quaternary clauses
c [quatres-11-2] added 14 single-self-subsuming ternary resolvents
c [quatres-11-2] added 44 quaternary resolvents
c [ternres-11] limit 55231575 with penalty 0 = 0 + 0
c [ternres-11] all 8408 free variables schedulable
c [ternres-11] 116 ternary resolvents (10 bin, 106 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1725986 penalty 4 = 4 + 0
c [card-5] found 776 at-most-one constraints of average size 3.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1725986 for elimination
c [card-5] 776 out of 776 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] generated 107 at-most-one constraints, 43 used 40%
c [card-5] exported 44 binary clauses, 1.0 per/constraint
c [gauss-5] limit 1380789 penalty 3 = 3 + 0
c [gauss-5] extracted 2066 xors of average arity 3.0
c [gauss-5] connected 6174 occurrences of 453 variables (average 13.6)
c [gauss-5] limit 1380789 penalty 3 = 3 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-41] removed 3 variables
c [treelook-4] limit 690394 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 15445 literals 92%
c [treelook-4] scheduling used 347269 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 690394 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 693673 steps
c [treelook-4] 14903 literals remain 89%
c [treelook-4] 6261 variables remain to probed next time 74%
c [decomp-42] removed 4 variables
c [treelook-4] removed 4 variables, found 429 hbrs
c [unhide-11] limit 2761578 with penalty 2 = 2 + 0
c [unhide-11-14] 0 units, 2 failed, 459 tauts, 0 hbrs, 231383 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 289 transitive binary clauses
c [cce-9] limit of 138078938 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 4 clauses out of 358 (1%) of length 11
c [cce-9-1] eliminated 6 clauses out of 269 (2%) of length 10
c [cce-9-1] eliminated 12 clauses out of 565 (2%) of length 9
c [cce-9-1] eliminated 18 clauses out of 786 (2%) of length 8
c [cce-9-1] eliminated 23 clauses out of 2871 (1%) of length 7
c [cce-9-1] eliminated 55 clauses out of 3610 (2%) of length 6
c [cce-9-1] eliminated 71 clauses out of 4129 (2%) of length 5
c [cce-9-1] eliminated 97 clauses out of 5889 (2%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 286 large clauses in 28855788 steps
c [cce-9-1] allowing another 14427894 steps for small clauses
c [cce-9-1] scheduling 30004 clauses = 24621 binary + 5383 ternary
c [cce-9-1] tried to eliminate 30004 small clauses 100%
c [cce-9-1] eliminated 956 binary clauses 4%
c [cce-9-1] eliminated 239 ternary clauses 4%
c [cce-9-1] eliminated 1195 small clauses 4%
c [cce-9-1] eliminated 1210 small clauses in 65957060 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] completed small and large (ACCE)
c [cce-9-1] eliminated 1496 covered clauses in round 1
c [cce-9-2] eliminated 1 clauses out of 1 (100%) of length 13
c [cce-9-2] eliminated 4 clauses out of 354 (1%) of length 11
c [cce-9-2] eliminated 3 clauses out of 263 (1%) of length 10
c [cce-9-2] eliminated 2 clauses out of 553 (0%) of length 9
c [cce-9-2] eliminated 2 clauses out of 768 (0%) of length 8
c [cce-9-2] eliminated 7 clauses out of 2848 (0%) of length 7
c [cce-9-2] eliminated 9 clauses out of 3555 (0%) of length 6
c [cce-9-2] eliminated 12 clauses out of 4058 (0%) of length 5
c [cce-9-2] eliminated 18 clauses out of 5792 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 58 large clauses in 27673089 steps
c [cce-9-2] allowing another 13836544 steps for small clauses
c [cce-9-2] scheduling 28809 clauses = 23665 binary + 5144 ternary
c [cce-9-2] tried to eliminate 28809 small clauses 100%
c [cce-9-2] eliminated 13 binary clauses 0%
c [cce-9-2] eliminated 6 ternary clauses 0%
c [cce-9-2] eliminated 19 small clauses 0%
c [cce-9-2] eliminated 19 small clauses in 62615793 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 77 covered clauses in round 2
c [cce-9-3] eliminated 1 clauses out of 2841 (0%) of length 7
c [cce-9-3] incomplete large round (ACCE)
c [cce-9-3] eliminated 1 large clauses in 9506086 steps
c [cce-9-3] allowing another 4753043 steps for small clauses
c [cce-9-3] scheduling 28790 clauses = 23652 binary + 5138 ternary
c [cce-9-3] tried to eliminate 2069 small clauses 7%
c [cce-9-3] incomplete small round (ACCE)
c [cce-9-3] eliminated 1 covered clauses in round 3
c [cce-9] eliminated 1574 covered clauses in TOTAL during 3 rounds
c [bca-11] limit of 10000000 steps and 104448 added (scaled 2)
c [bca-11] 7535 out of 16800 literals actually usable 45%
c [bca-11] added 14 blocked clauses in 91702 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 165694720 penalty 0 = 0 + 0
c [sweep-11-1] 997 pos 32.7% + 2055 neg 67.3% = 3052 sched 36.3% ret 5347
c [sweep-11-1] 6416091 steps 601 queries 37.89 avg class size
c [sweep-11-1] 9649 decisions 590 SAT calls 47.64 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-43] removed 16 variables
c [sweep-11-1] removed 16 vars (0 failed, 14 eqs, 25 impls)
c [sweep-11-2] 2767 pos 33.0% + 5616 neg 67.0% = 8383 sched 100.0% ret 0
c [sweep-11-2] 10005018 steps 771 queries 67.71 avg class size
c [sweep-11-2] 14612 decisions 764 SAT calls 55.29 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-44] removed 20 variables
c [sweep-11-2] removed 20 vars (0 failed, 10 eqs, 24 impls)
c [sweep-11-3] 2760 pos 33.0% + 5603 neg 67.0% = 8363 sched 100.0% ret 0
c [sweep-11-3] 9322542 steps 758 queries 55.69 avg class size
c [sweep-11-3] 13377 decisions 748 SAT calls 52.58 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-45] removed 8 variables
c [sweep-11-3] removed 8 vars (0 failed, 11 eqs, 27 impls)
c [sweep-11] removed 44 vars in TOTAL (3 rounds, 2127 queries)
c [sort-queue-15] sorted 1862 enqueued variables after 748560 conflicts
c [score-dist-15] active 6493 (78%), one 1229 (15%), zero 633 (8%)
c [score-dist-15] max exp 511, different 227 (44%)
c [score-dist-15] median active exp 503, avg 477.0
c [simplification-15] removed 53 variables 0.6% (8355 remain 17%)
c [simplification-15] removed 1809 irredundant clauses 3.4% (51741 remain 25%)
c [simplification-15] maximum reduction of 3% = max (1%, 3%)
c [simplification-15] geometric conflict interval increment 58593 = 234372 / 4
c [simplification-15] new conflict interval 292965
c [simplification-15] penalized conflict interval 292965 = 1 * 292965
c [simplification-15] hard conflict limit 1188007 (soft 1041525 + delta 146482)
c [simplification-15] new conflict limit 1041525 (hard 1188007)
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 -  237.9    8355    51741    756991   44620   5537 13146   22    30   16  75%   1024    0   21   23   95%
c -  250.1    8355    51741    798794   45458   5572 13158   38    61   23  62%   1024   28   39   24  159%
c i  252.9    8354    51741    809330   55521   5586 13159   33    56   30  58%   1024   19   24   26   90%
c -  260.9    8354    51741    839998   45922   5615 13165   24    32   23  74%  -7014   -9   30   27  113%
c -  272.9    8354    51741    882902   46493   5644 13169   19    28   23  68%  -3152  -10   17   26   65%
c -  283.5    8354    51741    925068   47667   5673 13176   22    31   23  70%  -1171   -3   33   23  141%
c -  295.4    8354    51741    970141   48245   5707 13183   27    62   23  44%    -79   26   44   24  181%
c -  309.6    8354    51741   1013878   49306   5722 13185   44    53   24  83%    458    7   39   34  116%
c -  325.8    8354    51741   1057943   50352   5726 13186   33    38   24  87%    735   -8   28   35   79%
c -  340.4    8354    51741   1103791   50146   5736 13188   29    36   36  82%    880   -6   30   32   92%
c 
c [simplification-16] limit 1041525 conflicts (hard 1188007) hit after 1123333 conflicts
c [quatres-12] found 9319 quaternary clauses 28% in total
c [quatres-12-1] removed 5 duplicate quaternary clauses
c [quatres-12-2] added 33 single-self-subsuming ternary resolvents
c [quatres-12-2] added 55 quaternary resolvents
c [ternres-12] limit 88502466 with penalty 0 = 0 + 0
c [ternres-12] all 8354 free variables schedulable
c [ternres-12] 376 ternary resolvents (9 bin, 367 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-46] removed 4 variables
c [basicprobe-4] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-4-0] 2330 sched 28%, 8 failed, 0 lifted, 769 hbrs
c [decomp-47] removed 10 variables
c [basicprobe-4-1] 4505 sched 54%, 11 failed, 0 lifted, 946 hbrs
c [decomp-48] removed 11 variables
c [basicprobe-4-2] 4484 sched 54%, 1 failed, 0 lifted, 149 hbrs
c [decomp-49] removed 1 variables
c [basicprobe-4-3] 4480 sched 54%, 0 failed, 0 lifted, 57 hbrs
c [basicprobe-4-4] 4480 sched 54%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-4-5] 4479 sched 54%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-4-6] 4479 sched 54%, 0 failed, 0 lifted, 17 hbrs
c [basicprobe-4-7] 4479 sched 54%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-4-8] 4479 sched 54%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-4-8] round limit 8 hit
c [basicprobe-4-8] 20 units = 20 failed (100%) + 0 lifted (0%)
c [basicprobe-4-8] removed 22 variables, found 1972 hbrs
c [bate-3] eliminated 16 asymmetric tautologies during probing
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 1033 transitive binary clauses
c [cce-10] limit of 442512332 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 20 clauses out of 346 (6%) of length 11
c [cce-10-1] eliminated 23 clauses out of 258 (9%) of length 10
c [cce-10-1] eliminated 6 clauses out of 537 (1%) of length 9
c [cce-10-1] eliminated 9 clauses out of 769 (1%) of length 8
c [cce-10-1] eliminated 18 clauses out of 2808 (1%) of length 7
c [cce-10-1] eliminated 24 clauses out of 3502 (1%) of length 6
c [cce-10-1] eliminated 37 clauses out of 4046 (1%) of length 5
c [cce-10-1] eliminated 38 clauses out of 5740 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 175 large clauses in 24813259 steps
c [cce-10-1] allowing another 12406629 steps for small clauses
c [cce-10-1] scheduling 28641 clauses = 23536 binary + 5105 ternary
c [cce-10-1] tried to eliminate 28641 small clauses 100%
c [cce-10-1] eliminated 88 binary clauses 0%
c [cce-10-1] eliminated 10 ternary clauses 0%
c [cce-10-1] eliminated 98 small clauses 0%
c [cce-10-1] eliminated 98 small clauses in 56154593 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 273 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 12272337 steps for small clauses
c [cce-10-2] scheduling 28543 clauses = 23448 binary + 5095 ternary
c [cce-10-2] tried to eliminate 28543 small clauses 100%
c [cce-10-2] completed small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 273 covered clauses in TOTAL during 2 rounds
c [cce-10] 273 < 1/100 * 51558 = 515 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 8329 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 275 variables 3% in round 1 in 10732537 steps
c [elim-13-1] backward subsumption/strengthening limit 10732500
c [elim-13-1-1] backward checking 1726 touched variables 21%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 2 and strengthened 8 clauses in 1229192 steps
c [elim-13-1] rescheduled 36 variables 0% by backward subsumption
c [elim-13-2] eliminated 2 variables 0% in round 2 in 125107 steps
c [elim-13-2] backward subsumption/strengthening limit 125100
c [elim-13-2-1] backward checking 17 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 0 and strengthened 0 clauses in 37114 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 277 = 3% variables out of 8329 scheduled
c [bca-12] limit of 10000000 steps and 102343 added (scaled 2)
c [bca-12] 6547 out of 16106 literals actually usable 41%
c [bca-12] added 6 blocked clauses in 64479 steps
c [sweep-12] limit 26550739 penalty 0 = 0 + 0
c [sweep-12-1] 2667 pos 33.1% + 5385 neg 66.9% = 8052 sched 100.0% ret 0
c [sweep-12-1] 7759529 steps 732 queries 46.51 avg class size
c [sweep-12-1] 12311 decisions 725 SAT calls 49.76 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-55] removed 7 variables
c [sweep-12-1] removed 7 vars (0 failed, 9 eqs, 25 impls)
c [sweep-12-2] 2665 pos 33.1% + 5380 neg 66.9% = 8045 sched 100.0% ret 0
c [sweep-12-2] 8323370 steps 738 queries 44.67 avg class size
c [sweep-12-2] 13079 decisions 736 SAT calls 51.81 avg env size
c [sweep-12-2] fully completed sweeping round
c [decomp-56] removed 1 variables
c [sweep-12-2] removed 1 vars (0 failed, 3 eqs, 25 impls)
c [sweep-12-3] 2664 pos 33.1% + 5380 neg 66.9% = 8044 sched 100.0% ret 0
c [sweep-12-3] 9277422 steps 762 queries 59.06 avg class size
c [sweep-12-3] 12477 decisions 753 SAT calls 46.76 avg env size
c [sweep-12-3] fully completed sweeping round
c [decomp-57] removed 8 variables
c [sweep-12-3] removed 8 vars (0 failed, 10 eqs, 27 impls)
c [sweep-12] removed 16 vars in TOTAL (3 rounds, 2229 queries)
c [sort-queue-16] sorted 1923 enqueued variables after 1123333 conflicts
c [score-dist-16] active 6113 (76%), one 1408 (18%), zero 515 (6%)
c [score-dist-16] max exp 511, different 160 (31%)
c [score-dist-16] median active exp 504, avg 496.6
c [simplification-16] removed 318 variables 3.8% (8036 remain 16%)
c [simplification-16] removed 915 irredundant clauses 1.8% (50826 remain 24%)
c [simplification-16] maximum reduction of 4% = max (4%, 2%)
c [simplification-16] geometric conflict interval increment 58593 = 292965 / 5
c [simplification-16] new conflict interval 351558
c [simplification-16] penalized conflict interval 351558 = 1 * 351558
c [simplification-16] hard conflict limit 1650670 (soft 1474891 + delta 175779)
c [simplification-16] new conflict limit 1474891 (hard 1650670)
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 -  369.5    8036    50826   1171196   50129   5505 13043   26    31   22  83%    973   -6   23   30   77%
c -  384.3    8036    50826   1218432   51185   5533 13044   31    36   22  85%    999   -3   20   31   65%
c -  396.1    8036    50826   1265151   51899   5573 13050   22    29   22  75%   1012   -8   20   27   72%
c -  410.2    8036    50826   1312880   51851   5585 13052   35    41   22  84%   1018    4   29   29  100%
c -  427.9    8036    50826   1362230   52795   5614 13056   24    32   31  74%   1021   -2   23   26   88%
c -  446.0    8036    50826   1412337   53235   5625 13057   24    29   32  83%   1023   -4   23   26   89%
c -  466.3    8036    50826   1464905   54347   5636 13057   20    23   34  88%   1023   -6   18   23   76%
c 
c [simplification-17] limit 1474891 conflicts (hard 1650670) hit after 1474891 conflicts
c [quatres-13] found 9475 quaternary clauses 28% in total
c [quatres-13-1] removed 8 duplicate quaternary clauses
c [quatres-13-1] added 1 double-self-subsuming ternary resolvents
c [quatres-13-2] added 25 single-self-subsuming ternary resolvents
c [quatres-13-2] added 266 quaternary resolvents
c [ternres-13] limit 127397396 with penalty 0 = 0 + 0
c [ternres-13] all 8036 free variables schedulable
c [ternres-13] 255 ternary resolvents (10 bin, 245 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-58] removed 1 variables
c [simpleprobe-5] all 8035 free variables schedulable
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-59] removed 10 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 10 variables, found 4745 hbrs, 4 units
c [unhide-12] limit 10000000 with penalty 1 = 1 + 0
c [unhide-12-23] 0 units, 3 failed, 5273 tauts, 0 hbrs, 225377 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 693 transitive binary clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 8024 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 164 variables 2% in round 1 in 10671226 steps
c [elim-14-1] backward subsumption/strengthening limit 10671200
c [elim-14-1-1] backward checking 1123 touched variables 14%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 3 and strengthened 15 clauses in 1136055 steps
c [elim-14-1] rescheduled 58 variables 1% by backward subsumption
c [elim-14-2] eliminated 5 variables 0% in round 2 in 161153 steps
c [elim-14-2] backward subsumption/strengthening limit 161100
c [elim-14-2-1] backward checking 44 touched variables 1%
c [elim-14-2-1] incomplete backward checking 41 remain 93%
c [elim-14-2] subsumed 0 and strengthened 0 clauses in 161707 steps
c [elim-14-2] fully rescheduled 7855 variables 98%
c [elim-14-3] eliminated 3 variables 0% in round 3 in 10622500 steps
c [elim-14-3] backward subsumption/strengthening limit 10622500
c [elim-14-3-1] backward checking 75 touched variables 1%
c [elim-14-3-1] fully completed backward checking in 1 rounds
c [elim-14-3] subsumed 0 and strengthened 0 clauses in 59286 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 172 = 2% variables out of 8024 scheduled
c [bca-13] limit of 10000000 steps and 101356 added (scaled 2)
c [bca-13] 6191 out of 15706 literals actually usable 39%
c [bca-13] added 12 blocked clauses in 64036 steps
c [sweep-13] limit 38219218 penalty 0 = 0 + 0
c [sweep-13-1] 2590 pos 33.0% + 5262 neg 67.0% = 7852 sched 100.0% ret 0
c [sweep-13-1] 8122060 steps 707 queries 48.12 avg class size
c [sweep-13-1] 13635 decisions 702 SAT calls 48.39 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-60] removed 7 variables
c [sweep-13-1] removed 7 vars (0 failed, 8 eqs, 21 impls)
c [sweep-13-2] 2586 pos 33.0% + 5259 neg 67.0% = 7845 sched 100.0% ret 0
c [sweep-13-2] 8306036 steps 720 queries 40.93 avg class size
c [sweep-13-2] 12705 decisions 716 SAT calls 46.27 avg env size
c [sweep-13-2] fully completed sweeping round
c [decomp-61] removed 11 variables
c [sweep-13-2] removed 11 vars (0 failed, 6 eqs, 12 impls)
c [sweep-13-3] 2578 pos 32.9% + 5256 neg 67.1% = 7834 sched 100.0% ret 0
c [sweep-13-3] 8276389 steps 717 queries 47.30 avg class size
c [sweep-13-3] 12701 decisions 713 SAT calls 47.18 avg env size
c [sweep-13-3] fully completed sweeping round
c [decomp-62] removed 17 variables
c [sweep-13-3] removed 17 vars (0 failed, 8 eqs, 11 impls)
c [sweep-13] removed 35 vars in TOTAL (3 rounds, 2141 queries)
c [sort-queue-17] sorted 1741 enqueued variables after 1474891 conflicts
c [score-dist-17] active 6076 (78%), one 1295 (17%), zero 446 (6%)
c [score-dist-17] max exp 512, different 175 (34%)
c [score-dist-17] median active exp 503, avg 490.8
c [simplification-17] removed 219 variables 2.7% (7817 remain 15%)
c [simplification-17] removed 598 irredundant clauses 1.2% (50228 remain 24%)
c [simplification-17] maximum reduction of 3% = max (3%, 1%)
c [simplification-17] geometric conflict interval increment 87889 = 351558 / 4
c [simplification-17] new conflict interval 439447
c [simplification-17] penalized conflict interval 439447 = 1 * 439447
c [simplification-17] hard conflict limit 2134061 (soft 1914338 + delta 219723)
c [simplification-17] new conflict limit 1914338 (hard 2134061)
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 -  492.2    7817    50228   1529630   53987   5514 12427   27    33   22  80%   1024    4   21   23   89%
c -  511.8    7817    50228   1582770   55188   5519 12428   20    22   24  90%   1024   -4   19   21   91%
c -  529.0    7817    50228   1634643   54608   5536 12431   23    27   24  84%   1024   -0   23   22  101%
c i  531.6    7816    50228   1643343   62238   5536 12431   19    24   31  80%   1024   -4   17   22   76%
c -  545.0    7816    50228   1686604   55122   5554 12433   31    39   24  80%  -5817    4   33   27  122%
c -  562.6    7816    50228   1740565   56559   5572 12438   32    41   34  78%  -1979    5   36   29  124%
c -  578.9    7816    50228   1795206   57539   5594 12444   20    31   33  64%   -281   -4   17   27   65%
c -  593.8    7816    50228   1848641   57571   5613 12447   25    35   33  71%    447   -3   16   28   59%
c -  613.0    7816    50228   1907450   58856   5619 12449   26    30   34  85%    789   -3   31   26  118%
c 
c [simplification-18] limit 1914338 conflicts (hard 2134061) hit after 1934589 conflicts
c [quatres-14] found 9806 quaternary clauses 28% in total
c [quatres-14-1] removed 17 duplicate quaternary clauses
c [quatres-14-1] added 2 double-self-subsuming ternary resolvents
c [quatres-14-2] added 53 single-self-subsuming ternary resolvents
c [quatres-14-2] added 286 quaternary resolvents
c [ternres-14] limit 177682284 with penalty 0 = 0 + 0
c [ternres-14] all 7816 free variables schedulable
c [ternres-14] 799 ternary resolvents (11 bin, 788 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-63] removed 3 variables
c [unhide-13] limit 20000000 with penalty 0 = 0 + 0
c [unhide-13-37] 1 units, 9 failed, 1484 tauts, 0 hbrs, 314947 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 201 transitive binary clauses
c [cce-11] limit of 444205712 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 3 clauses out of 37 (8%) of length 12
c [cce-11-1] eliminated 6 clauses out of 231 (3%) of length 10
c [cce-11-1] eliminated 7 clauses out of 579 (1%) of length 9
c [cce-11-1] eliminated 4 clauses out of 802 (0%) of length 8
c [cce-11-1] eliminated 14 clauses out of 2474 (1%) of length 7
c [cce-11-1] eliminated 48 clauses out of 3445 (1%) of length 6
c [cce-11-1] eliminated 86 clauses out of 3866 (2%) of length 5
c [cce-11-1] eliminated 201 clauses out of 6041 (3%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 369 large clauses in 25798007 steps
c [cce-11-1] allowing another 12899003 steps for small clauses
c [cce-11-1] scheduling 27206 clauses = 22268 binary + 4938 ternary
c [cce-11-1] tried to eliminate 27206 small clauses 100%
c [cce-11-1] eliminated 470 binary clauses 2%
c [cce-11-1] eliminated 182 ternary clauses 4%
c [cce-11-1] eliminated 652 small clauses 2%
c [cce-11-1] eliminated 660 small clauses in 54703633 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 1029 covered clauses in round 1
c [cce-11-2] eliminated 3 clauses out of 798 (0%) of length 8
c [cce-11-2] eliminated 3 clauses out of 2460 (0%) of length 7
c [cce-11-2] eliminated 3 clauses out of 3780 (0%) of length 5
c [cce-11-2] eliminated 1 clauses out of 5840 (0%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 10 large clauses in 25124626 steps
c [cce-11-2] allowing another 12562313 steps for small clauses
c [cce-11-2] scheduling 26554 clauses = 21798 binary + 4756 ternary
c [cce-11-2] tried to eliminate 26554 small clauses 100%
c [cce-11-2] eliminated 14 binary clauses 0%
c [cce-11-2] eliminated 2 ternary clauses 0%
c [cce-11-2] eliminated 16 small clauses 0%
c [cce-11-2] eliminated 16 small clauses in 53375619 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 26 covered clauses in round 2
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] allowing another 12544139 steps for small clauses
c [cce-11-3] scheduling 26538 clauses = 21784 binary + 4754 ternary
c [cce-11-3] tried to eliminate 26538 small clauses 100%
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 0 covered clauses in round 3
c [cce-11] eliminated 1055 covered clauses in TOTAL during 3 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 7809 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 193 variables 2% in round 1 in 10395840 steps
c [elim-15-1] backward subsumption/strengthening limit 10395800
c [elim-15-1-1] backward checking 1172 touched variables 15%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 5 and strengthened 9 clauses in 1071780 steps
c [elim-15-1] rescheduled 52 variables 1% by backward subsumption
c [elim-15-2] eliminated 2 variables 0% in round 2 in 2136803 steps
c [elim-15-2] backward subsumption/strengthening limit 2136800
c [elim-15-2-1] backward checking 15 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 0 and strengthened 0 clauses in 30049 steps
c [elim-15] fully completed in 2 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 195 = 2% variables out of 7809 scheduled
c [bca-14] limit of 10000000 steps and 98082 added (scaled 2)
c [bca-14] 5789 out of 15230 literals actually usable 38%
c [bca-14] added 12 blocked clauses in 76918 steps
c [sweep-14] limit 53304685 penalty 0 = 0 + 0
c [sweep-14-1] 2392 pos 31.4% + 5222 neg 68.6% = 7614 sched 100.0% ret 0
c [sweep-14-1] 9354946 steps 684 queries 29.36 avg class size
c [sweep-14-1] 12788 decisions 677 SAT calls 51.82 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-64] removed 7 variables
c [sweep-14-1] removed 7 vars (0 failed, 7 eqs, 11 impls)
c [sweep-14-2] 2386 pos 31.4% + 5221 neg 68.6% = 7607 sched 100.0% ret 0
c [sweep-14-2] 8531047 steps 671 queries 30.63 avg class size
c [sweep-14-2] 12705 decisions 667 SAT calls 51.33 avg env size
c [sweep-14-2] fully completed sweeping round
c [decomp-65] removed 10 variables
c [sweep-14-2] removed 10 vars (0 failed, 6 eqs, 11 impls)
c [sweep-14-3] 2382 pos 31.4% + 5215 neg 68.6% = 7597 sched 100.0% ret 0
c [sweep-14-3] 9137696 steps 698 queries 56.57 avg class size
c [sweep-14-3] 13157 decisions 694 SAT calls 46.84 avg env size
c [sweep-14-3] fully completed sweeping round
c [decomp-66] removed 12 variables
c [sweep-14-3] removed 12 vars (0 failed, 3 eqs, 7 impls)
c [sweep-14] removed 29 vars in TOTAL (3 rounds, 2050 queries)
c [sort-queue-18] sorted 2049 enqueued variables after 1934589 conflicts
c [score-dist-18] active 5536 (73%), one 1653 (22%), zero 396 (5%)
c [score-dist-18] max exp 512, different 192 (37%)
c [score-dist-18] median active exp 504, avg 485.3
c [simplification-18] removed 231 variables 3.0% (7585 remain 15%)
c [simplification-18] removed 1656 irredundant clauses 3.3% (48572 remain 23%)
c [simplification-18] maximum reduction of 3% = max (3%, 3%)
c [simplification-18] geometric conflict interval increment 109861 = 439447 / 4
c [simplification-18] new conflict interval 549308
c [simplification-18] penalized conflict interval 549308 = 1 * 549308
c [simplification-18] hard conflict limit 2758551 (soft 2483897 + delta 274654)
c [simplification-18] new conflict limit 2483897 (hard 2758551)
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 -  649.0    7585    48572   1984504   58225   5951 11390   24    28   23  84%    951   -3   22   25   90%
c -  667.4    7585    48572   2045118   59420   5977 11394   23    40   25  57%    995   12   26   22  118%
c -  687.5    7585    48572   2102290   60237   6001 11397   19    25   25  74%   1012   -2   37   21  178%
c -  709.0    7585    48572   2161934   59943   6019 11398   23    27   25  84%   1019   -4   22   24   90%
c -  728.9    7585    48572   2221554   60512   6035 11398   24    31   36  79%   1022    0   39   24  158%
c -  750.8    7585    48572   2285614   62113   6050 11399   18    28   36  62%   1023    1   22   22  100%
c -  770.7    7585    48572   2345028   62192   6069 11401   21    25   36  85%   1024   -6   17   24   73%
c -  792.2    7585    48572   2408791   62769   6076 11403   21    26   36  80%   1024   -3   18   23   78%
c -  812.3    7585    48572   2472386   63175   6085 11404   27    32   36  85%   1024    3   24   24  103%
c -  832.9    7585    48572   2538889   63921   6092 11405   19    21   36  89%   1024   -5   17   21   82%
c 
c [simplification-19] limit 2483897 conflicts (hard 2758551) hit after 2552689 conflicts
c [quatres-15] found 9974 quaternary clauses 29% in total
c [quatres-15-1] removed 19 duplicate quaternary clauses
c [quatres-15-1] added 2 double-self-subsuming ternary resolvents
c [quatres-15-2] added 65 single-self-subsuming ternary resolvents
c [quatres-15-2] added 324 quaternary resolvents
c [ternres-15] limit 200000000 with penalty 0 = 0 + 0
c [ternres-15] all 7585 free variables schedulable
c [ternres-15] 486 ternary resolvents (12 bin, 474 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-67] removed 1 variables
c [treelook-5] limit 6322371 penalty 2 = 2 + 0 boost 1
c [treelook-5] scheduled 13960 literals 92%
c [treelook-5] scheduling used 351545 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 6322371 penalty 2 = 2 + 0 boost 1
c [treelook-5] used 6323965 steps
c [treelook-5] 10285 literals remain 68%
c [treelook-5] 5464 variables remain to probed next time 72%
c [decomp-68] removed 7 variables
c [treelook-5] removed 20 variables, found 5179 hbrs
c [unhide-14] limit 20000000 with penalty 0 = 0 + 0
c [unhide-14-52] 0 units, 0 failed, 3135 tauts, 0 hbrs, 189792 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 213 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 7564 variables 100%
c [block-5] limit of 50000000 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 22 blocked clauses
c [block-5] 22 < 1/100 * 48378 = 483 considered unsuccessful
c [cce-12] limit of 1264474272 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 9 clauses out of 34 (26%) of length 12
c [cce-12-1] eliminated 19 clauses out of 300 (6%) of length 11
c [cce-12-1] eliminated 3 clauses out of 225 (1%) of length 10
c [cce-12-1] eliminated 9 clauses out of 557 (2%) of length 9
c [cce-12-1] eliminated 7 clauses out of 796 (1%) of length 8
c [cce-12-1] eliminated 9 clauses out of 2410 (0%) of length 7
c [cce-12-1] eliminated 18 clauses out of 3389 (1%) of length 6
c [cce-12-1] eliminated 45 clauses out of 3727 (1%) of length 5
c [cce-12-1] eliminated 56 clauses out of 5898 (1%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 175 large clauses in 23047771 steps
c [cce-12-1] allowing another 11523885 steps for small clauses
c [cce-12-1] scheduling 26276 clauses = 21223 binary + 5053 ternary
c [cce-12-1] tried to eliminate 26276 small clauses 100%
c [cce-12-1] eliminated 80 binary clauses 0%
c [cce-12-1] eliminated 71 ternary clauses 1%
c [cce-12-1] eliminated 151 small clauses 1%
c [cce-12-1] eliminated 151 small clauses in 50088825 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 326 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 11413955 steps for small clauses
c [cce-12-2] scheduling 26125 clauses = 21143 binary + 4982 ternary
c [cce-12-2] tried to eliminate 26125 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 326 covered clauses in TOTAL during 2 rounds
c [cce-12] 326 < 1/100 * 48356 = 483 considered unsuccessful
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 7563 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 102 variables 1% in round 1 in 10210720 steps
c [elim-16-1] backward subsumption/strengthening limit 10210700
c [elim-16-1-1] backward checking 818 touched variables 11%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 1 and strengthened 9 clauses in 1433397 steps
c [elim-16-1] rescheduled 33 variables 0% by backward subsumption
c [elim-16-2] no variable eliminated in round 2 in 2072361 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 102 = 1% variables out of 7563 scheduled
c [bca-15] limit of 10000000 steps and 96376 added (scaled 2)
c [bca-15] 5535 out of 14924 literals actually usable 37%
c [bca-15] added 4 blocked clauses in 77309 steps
c [sweep-15] limit 75868456 penalty 0 = 0 + 0
c [sweep-15-1] 2381 pos 31.9% + 5080 neg 68.1% = 7461 sched 100.0% ret 0
c [sweep-15-1] 10121842 steps 657 queries 38.38 avg class size
c [sweep-15-1] 11908 decisions 657 SAT calls 47.20 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-69] removed 2 variables
c [sweep-15-1] removed 2 vars (0 failed, 3 eqs, 1 impls)
c [sweep-15-2] 2379 pos 31.9% + 5080 neg 68.1% = 7459 sched 100.0% ret 0
c [sweep-15-2] 10996423 steps 666 queries 41.71 avg class size
c [sweep-15-2] 11839 decisions 663 SAT calls 48.61 avg env size
c [sweep-15-2] fully completed sweeping round
c [decomp-70] removed 4 variables
c [sweep-15-2] removed 4 vars (0 failed, 3 eqs, 10 impls)
c [sweep-15-3] 2377 pos 31.9% + 5078 neg 68.1% = 7455 sched 100.0% ret 0
c [sweep-15-3] 9906610 steps 702 queries 30.29 avg class size
c [sweep-15-3] 12317 decisions 697 SAT calls 47.16 avg env size
c [sweep-15-3] fully completed sweeping round
c [decomp-71] removed 10 variables
c [sweep-15-3] removed 10 vars (0 failed, 4 eqs, 8 impls)
c [sweep-15] removed 16 vars in TOTAL (3 rounds, 2022 queries)
c [sort-queue-19] sorted 2091 enqueued variables after 2552689 conflicts
c [score-dist-19] active 5354 (72%), one 1717 (23%), zero 374 (5%)
c [score-dist-19] max exp 512, different 189 (37%)
c [score-dist-19] median active exp 504, avg 488.2
c [simplification-19] removed 140 variables 1.8% (7445 remain 15%)
c [simplification-19] removed 823 irredundant clauses 1.7% (47749 remain 23%)
c [simplification-19] maximum reduction of 2% = max (2%, 2%)
c [simplification-19] geometric conflict interval increment 183102 = 549308 / 3
c [simplification-19] new conflict interval 732410
c [simplification-19] penalized conflict interval 732410 = 1 * 732410
c [simplification-19] hard conflict limit 3651304 (soft 3285099 + delta 366205)
c [simplification-19] new conflict limit 3285099 (hard 3651304)
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 -  865.5    7445    47749   2615678   63955   6252 13661   24    32   26  75%   1024    6   21   21  102%
c -  885.6    7445    47749   2681461   65280   6270 13664   24    29   26  83%   1024    2   21   21   99%
c -  904.1    7445    47749   2747799   66298   6286 13669   28    48   25  59%   1024   21   29   20  142%
c -  922.9    7445    47749   2808300   65528   6295 13670   28    33   26  86%   1024   -5   29   27  106%
c -  944.4    7445    47749   2871577   66994   6303 13671   27    32   37  83%   1024   -3   22   28   77%
c -  966.3    7445    47749   2933030   67265   6315 13672   26    33   37  80%   1024   -1   23   27   85%
c -  989.7    7445    47749   3003221   67970   6322 13674   19    25   37  79%   1024   -3   24   22  107%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 224 basic ate = 157 trn 70% + 67 lrg 30% in 3 updates
c bcas: 15 count, 345 added (122 skipped), 986607 steps
c bkwd: tried 173513 clauses, 346877 lits, 2.00 lits/clause
c bkwd: checked 35527963 occs, 204.76 occs/clause, 102.42 occs/lit
c bkwd: subsumed 1 binary, 25 ternary, 30 large
c bkwd: strengthened 0 binary, 1 ternary (100% self), 289 large (0% self)
c blkd: 5 bces, 238 removed, 1365411 resolutions, 3602120 steps
c blkd: 2387 blocking literals 2%, 10 pure
c bump: 3043787 bumped seen, 722146210 lits 237.3 on average
c card: 5 count, 9 units, 44 am1, 13215165 steps
c card: 134 rescheduled, 1182 eliminated, 35339 resolved, 10218 subsumed
c card: 4331 at-most-one constraints found, average size 3.00
c card: 4331 at-most-one constraints used 100%, average size 3.00
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 12 cces, 12867 eliminated, 9978 ate 78%, 2889 abce 22%
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: 764685 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 134 gcs, 0 rescored clauses, 11835 rescored vars
c dcps: 71 decompositions, 15345 equivalent 29%
c deco: 2378 decision-only clauses 0%, 64% reduction
c decs: 6171856 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 16 elims, 21302 eliminated 41%, 152 pure 1%
c elms: 45 rounds, 2.8 rounds/bve
c elms: 18830 small 88%, 2310 large 11%
c elms: 26646 tried small, 18830 succeeded 71%, 7816 failed 29%
c elms: 6748 subsumed, 20697 strengthened, 382 blocked
c elms: 4800414 copies, 6081633 resolutions, 579830 ipos
c elms: 3653239 subchks, 4626384 strchks
c gaus: 5 extractions, 11957 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 1 ternary equations
c gaus: 0 gc, 13762088 steps, 6881044 extr 50%, 349984 elim 3%
c glue: 26.3 orig avg, 26.3 real avg, 5.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 67565 = 43330 simple 64% + 21041 trn 31% + 3194 lrg 5%, 2303 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3043787 clauses, 73.0 length
c lrnd: 222205173 lits = 512588227 orig - 290383054 removed 57%
c lrnd: 646666 uips 21%, 2043142 flips 67%
c mins: 3034796 mins 100%, 603 bin 0%, 6010 size 0%
c mins: 601158060 poisoned searches, 73230965 hits, 12% hit rate
c mins: 1036667329 used twice searches, 36423940 hits, 4% hit rate
c move: moved 8278, 6587 bin 80%, 1691 trn 20%
c otfs: 6603 driving 21%, 24183 restarting 79%
c otfs: str 30786, 30505 red 99%, 281 irr 1%
c otfs: str 30786, 0 bin 0%, 125 trn 0%, 30661 lrg 100%
c otfs: sub 122, 122 red 100%, 0 irr 0%
c otfs: sub 122, 0 bin 0%, 5 trn 4%, 117 lrg 96%
c phas: 8 computed, 11974 set, 31 pos (0%), 11943 neg (100%)
c prbs: 4 basic, 138511 probed, 152 failed, 15 lifted
c prbs: 5 simple, 131291 probed, 776 failed, 13044 eqs
c prbs: 5 treelook, 4381 probed, 10 failed, 0 lifted
c prom: 513580 locked 2% out of 22602402 tried
c prps: 1702117605 props, 272 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 15 count, 2814 quat, 360 self1, 7 self2, 214 dup
c queu: 19 sorted, 6171856 next (358626 steps 0.06)
c queu: 788362036 enq (1159839749 steps 1.47), 722146210 deq 92%
c redc: 13734 clauses 27%, 51783 tried 2%, 46 sat 0%
c redc: 23379 lits 4%, 559933 tried 0%, 46 sat 0%
c redc: 782 times jump level reduced, 8.8 levels on average
c reds: 59 count, 51476.2 conflicts per reduce
c reds: 0 memlim 0%, 59 arith 100%
c reds: 2330883 collected 93%, 182885 retired 7%
c rmbd: 9151 removed, 8216 red 90%
c rsts: 22520 restarts 100%, 90 skipped 0%
c rsts: 90 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: 19 count, 18 confs 95%, 0 vars 0%
c simp: 0 its 0%, 1 bin 5%, 0 trns 0%
c subl: 3043787 count (5995865 tried 2.0), 318256 sub out of 3038836 (10.5%)
c swps: 15 count, 29 rounds, 14714 queries (507.4/round)
c swps: 14403 sat calls, 79 unsat (0.9% success rate)
c swps: 266367 decisions 18.5, 13297 conflicts 0.9
c swps; 62.6 avg class size, 51.0 avg environment size
c swps: 0 failed, 748 impls, 381 equivs
c swp0: 4891 type 0 queries, 1006 unsat (20.6%), 4816 sat (98.5%)
c swp1: 9823 type 1 queries, 2724 unsat (27.7%), 9517 sat (96.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: 18455389 calls to obtain time
c tops: 8352 fixed 16%, 6 its, 506182.17 confs/it
c trds: 15 transitive reductions, 8034 removed, 27 failed
c trds: 214244 nodes, 481007 edges, 29484792 steps
c trim: 3149147 words, 12.0 MB
c trnr: 15 count, 371 bin, 7333 trn, 50145101 steps
c unhd: 14 count, 52 rounds, 65647145 steps
c unhd: 134 non-trivial sccs of average size 2.1
c unhd: 23 units, 23 bin, 0 trn, 0 lrg
c unhd: 70 failed, 68 stamp, 0 lits, 1 bin, 1 trn, 0 lrg
c unhd: 15976 tauts, 158 bin 1%, 2734 trn 17%, 1091 lrg 7%
c unhd: 15976 tauts, 11993 stamp 75%, 14677 red 92%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1468133 str, 23 bin 0%, 1740 trn 0%, 1466370 lrg 100%, 1456153 red 99%
c vars: 7445 remaining 14% and 44999 removed 86% out of 52444
c vars: 8352 fixed 16%, 21302 eliminated 41%, 15345 equivalent 29%
c vsts: 31332330187 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 18.5 search visits per propagation, 10240.7 per conflict
c wchs: 5944264479 pushed, 26947295 enlarged, 224 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3041650       2330883        182885     299566832      96627599       2175665
c 
c  0 0         29363   1      1374   0         0   0 154516369  52  37595642  39    378335  17     0.6
c  1 5         14697   0      3080   0      6034   3  31434558  10<  9732112  10    120652   6     0.2
c  2 6         69086   2     28481   1     20006  11  57343614  19  19630140  20<   314378  14     0.9
c  3 9        263746   9    169941   7     38091  21  34421980  11  15672162  16    484801  22<    3.4
c  4 14       712758  23    540865  23     45795  25< 13721561   5   8167090   8    451006  21     8.2
c  5 21       963165  32<   769980  33<    38565  21   5306980   2   3746069   4    266462  12    10.0
c  6 30       624970  21    519383  22     20562  11   1945364   1   1452856   2    110647   5     7.7
c  7 41       248279   8    209156   9      8859   5    624876   0    458461   0     35740   2     6.2
c  8 54        80381   3     65545   3      3450   2    178956   0    125712   0      9855   0     4.0
c  9 69        26315   1     19498   1      1207   1     54374   0     36487   0      2911   0     2.0
c 10 86         8327   0      3553   0       292   0     17181   0     10378   0       865   0     1.5
c 11 126         563   0        27   0        24   0      1019   0       490   0        13   0     0.2
c 
c avg                  5.0           5.1           4.2           1.2           1.7           2.9
c std                  1.4           1.3           1.6           1.5           1.7           1.9
c 
c  123.901  12% bump
c   19.050   2% unhide
c   17.361   2% cce
c   10.559   1% sweep
c    8.792   1% rescore
c    6.680   1% probe
c 
c   13.980 < 1% rest (below)
c 
c    6.183   1% elim
c    3.844   0% decide
c    1.435   0% transred
c    0.681   0% bca
c    0.432   0% quatres
c    0.429   0% block
c    0.397   0% ternres
c    0.382   0% gauss
c    0.198   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    1.532   0% preprocessing     2%
c   64.239   6% inprocessing     98%
c ==================================
c   65.772   7% simplifying
c  934.212  93% search
c ==================================
c  999.985 100% all
c 
c       3037093 conflicts,        3037.1 confs/sec
c          2569 ternaries,        1182.2 confs/ternary
c           865 binaries,         3511.1 confs/binary
c             6 iterations,     506182.2 confs/iteration
c 
c            59 reductions,          0.1 redus/sec,  51476.2 confs/reduction
c         22520 restarts,           22.5 rests/sec,    134.9 confs/restart
c       6171856 decisions,        6171.9 decis/sec,      2.0 decis/conflict
c    1702117605 propagations,  1702142.5 props/sec,    275.8 props/decision
c 
c 1000.0 seconds, 68.1 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
