c launch: /data/cnf/sc2014/app/bob12m02-opt.cnf.bz2
c host: atom27
c Lingeling SAT Solver
c 
c Version b7ztzud 55d9a3e9649fc56eacf3e72d8e2e2d5c615d5f18
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Fri May  1 11:44:04 CEST 2015
c compiled Fri May  1 11:44:04 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-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/bob12m02-opt.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/bob12m02-opt.cnf.bz2
c no embedded options
c found 'p cnf 26256 77806' header
c read 26256 variables, 77806 clauses, 181546 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 --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 26255 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 [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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   26255    77805         0       0      0     0    0     0    4   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] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 26255 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 1439 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 1439 variables, found 1808 hbrs, 270 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 24816 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 18525 variables 75% in round 1 in 4802932 steps
c [elim-1-1] backward subsumption/strengthening limit 4802900
c [elim-1-1-1] backward checking 16746 touched variables 68%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 1 and strengthened 13 clauses in 865130 steps
c [elim-1-1] rescheduled 24 variables 0% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 43784 steps
c [elim-1-2] backward subsumption/strengthening limit 43700
c [elim-1-2-1] backward checking 9 touched variables 0%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 1 and strengthened 0 clauses in 42391 steps
c [elim-1-2] rescheduled 4 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 2471 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 18536 = 75% variables out of 24816 scheduled
c [phase-count-1] 29490 negative 85.2% of 34619 except 5129 14.8%
c [phase-count-1] 30005 positive 86.7% of 34619 except 4614 13.3%
c [phase-1] phase bias: 1007 positive 16%, 5273 negative 84%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 6280 zero 100.00%
c [score-distribution-1] 1 different 0.02% out of total 6280 variables
c [simplification-1] removed 19975 variables 76.1% (6280 remain 24%)
c [simplification-1] removed 43186 irredundant clauses 55.5% (34619 remain 44%)
c [simplification-1] maximum reduction of 76% = max (76%, 56%)
c [simplification-1] large reduction 76% >= 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    0.7    6279    34619       305     206     41     8    0     6    4   8%      1    6    5    0 16125%
c i    0.7    6268    34619       306     206     41     8    0     6    4   8%      1    6    5    0 16062%
c 
c [simplification-2] limit 1010 conflicts (hard 11000) hit after 1010 conflicts
c [decomp-3] removed 54 variables
c [simpleprobe-2] all 6226 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 3 variables
c [simpleprobe-2] 160 variables remain 3% (6063 retained 97%)
c [simpleprobe-2] removed 3 variables, found 738 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 12446 literals 100%
c [treelook-1] scheduling used 174017 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 477269 steps
c [treelook-1] 12423 literals remain 100%
c [treelook-1] 6223 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 5534 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 4300 probes remain 69% after last round
c [basicprobe-1-0] removed 0 variables, found 3205 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 6223 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 101 blocked clauses
c [block-1] 101 < 1/100 * 34357 = 343 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 25 clauses out of 140 (18%) of length 6
c [cce-1-1] eliminated 230 clauses out of 1172 (20%) of length 5
c [cce-1-1] eliminated 95 clauses out of 15486 (1%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 350 large clauses in 29431119 steps
c [cce-1-1] allowing another 14715559 steps for small clauses
c [cce-1-1] scheduling 3415 clauses = 2212 binary + 1203 ternary
c [cce-1-1] tried to eliminate 1247 small clauses 37%
c [cce-1-1] eliminated 32 binary clauses 1%
c [cce-1-1] eliminated 67 ternary clauses 6%
c [cce-1-1] eliminated 99 small clauses 3%
c [cce-1-1] eliminated 99 small clauses in 30000003 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 449 covered clauses in round 1
c [cce-1] eliminated 449 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 6219 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 157 variables 3% in round 1 in 4422312 steps
c [elim-2-1] backward subsumption/strengthening limit 4422300
c [elim-2-1-1] backward checking 508 touched variables 8%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 2 and strengthened 4 clauses in 422707 steps
c [elim-2-1] rescheduled 21 variables 0% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 9043 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 157 = 3% variables out of 6219 scheduled
c [bca-1] limit of 10000000 steps and 67602 added (scaled 2)
c [bca-1] 9591 out of 12126 literals actually usable 79%
c [bca-1] added 30 blocked clauses in 26877 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3204 pos 52.9% + 2858 neg 47.1% = 6062 sched 100.0% ret 0
c [sweep-1-1] 1021798 steps 48 queries 397.65 avg class size
c [sweep-1-1] 662 decisions 51 SAT calls 35.55 avg env size
c [sweep-1-1] 5761 variables remain 95% (301 retained 5%)
c [decomp-6] removed 5 variables
c [sweep-1-1] removed 5 vars (0 failed, 6 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 5 vars in TOTAL (1 rounds, 47 queries)
c [score-distribution-2] 4050 pos 66.86%, 0 min 0.00%, 2007 zero 33.14%
c [score-distribution-2] 1213 different 20.03% out of total 6057 variables
c [simplification-2] removed 203 variables 3.2% (6057 remain 23%)
c [simplification-2] removed 1068 irredundant clauses 3.1% (33551 remain 43%)
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 16010 (soft 6010 + delta 10000)
c [simplification-2] new conflict limit 6010 (hard 16010)
c 
c [simplification-3] limit 6010 conflicts (hard 16010) hit after 6010 conflicts
c [quatres-1] found 15920 quaternary clauses 89% in total
c [quatres-1-2] added 7 single-self-subsuming ternary resolvents
c [quatres-1-2] added 25 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 6057 free variables schedulable
c [ternres-1] 246 ternary resolvents (31 bin, 215 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 31 at-most-one constraints of average size 3.1
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 31 out of 31 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 3 at-most-one constraints, 0 used 0%
c [card-2] exported 0 binary clauses, 0.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 43276 xors of average arity 3.3
c [gauss-1] connected 144420 occurrences of 5182 variables (average 27.9)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-7] removed 12 variables
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 430 tauts, 0 hbrs, 1509 literals
c [transred-1] limit 252608 with penalty 0 = 0 + 0
c [transred-1] removed 6 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 4 clauses out of 7 (57%) of length 13
c [cce-2-1] eliminated 2 clauses out of 10 (20%) of length 10
c [cce-2-1] eliminated 1 clauses out of 11 (9%) of length 9
c [cce-2-1] eliminated 10 clauses out of 157 (6%) of length 6
c [cce-2-1] eliminated 31 clauses out of 989 (3%) of length 5
c [cce-2-1] eliminated 7 clauses out of 15617 (0%) of length 4
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 55 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2-1] scheduling 3108 clauses = 1825 binary + 1283 ternary
c [cce-2-1] tried to eliminate 1050 small clauses 34%
c [cce-2-1] eliminated 28 ternary clauses 2%
c [cce-2-1] eliminated 28 small clauses 1%
c [cce-2-1] eliminated 28 small clauses in 30000005 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 83 covered clauses in round 1
c [cce-2] eliminated 83 covered clauses in TOTAL during 1 rounds
c [cce-2] 83 < 1/100 * 33536 = 335 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 6045 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 129 variables 2% in round 1 in 5506359 steps
c [elim-3-1] backward subsumption/strengthening limit 5506300
c [elim-3-1-1] backward checking 480 touched variables 8%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 0 and strengthened 0 clauses in 393312 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 129 = 2% variables out of 6045 scheduled
c [bca-2] limit of 10000000 steps and 67233 added (scaled 2)
c [bca-2] 2580 out of 11834 literals actually usable 22%
c [bca-2] added 18 blocked clauses in 10185 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2919 pos 51.8% + 2711 neg 48.2% = 5630 sched 95.2% ret 286
c [sweep-2-1] 1003912 steps 60 queries 272.70 avg class size
c [sweep-2-1] 709 decisions 69 SAT calls 50.62 avg env size
c [sweep-2-1] 5217 variables remain 88% (699 retained 12%)
c [decomp-8] removed 17 variables
c [sweep-2-1] removed 17 vars (0 failed, 15 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 17 vars in TOTAL (1 rounds, 59 queries)
c [score-distribution-3] 5891 pos 99.86%, 6 min 0.10%, 2 zero 0.03%
c [score-distribution-3] 1360 different 23.05% out of total 5899 variables
c [simplification-3] removed 158 variables 2.6% (5899 remain 22%)
c [simplification-3] removed 204 irredundant clauses 0.6% (33347 remain 43%)
c [simplification-3] maximum reduction of 3% = max (3%, 1%)
c [simplification-3] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 26010 (soft 16010 + delta 10000)
c [simplification-3] new conflict limit 16010 (hard 26010)
c 
c [simplification-4] limit 16010 conflicts (hard 26010) hit after 16010 conflicts
c [quatres-2] found 16776 quaternary clauses 85% in total
c [quatres-2-1] removed 3 duplicate quaternary clauses
c [quatres-2-1] added 3 double-self-subsuming ternary resolvents
c [quatres-2-2] added 221 single-self-subsuming ternary resolvents
c [quatres-2-2] added 68 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 5899 free variables schedulable
c [ternres-2] 256 ternary resolvents (81 bin, 175 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-9] removed 6 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 9576 literals 81%
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 247329 steps
c [treelook-2] 9574 literals remain 81%
c [treelook-2] 5705 variables remain to probed next time 97%
c [treelook-2] removed 0 variables, found 2331 hbrs
c [transred-2] limit 710361 with penalty 0 = 0 + 0
c [transred-2] removed 11 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5893 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 0 blocked clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 5893 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 8 variables 0% in round 1 in 7017959 steps
c [elim-4-1] backward subsumption/strengthening limit 7017900
c [elim-4-1-1] backward checking 50 touched variables 1%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 75142 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 8 = 0% variables out of 5893 scheduled
c [elim-4] 8 < 1/100 * 5893 = 58 considered unsuccessful
c [bca-3] limit of 10000000 steps and 66890 added (scaled 2)
c [bca-3] 1326 out of 11772 literals actually usable 11%
c [bca-3] added 0 blocked clauses in 14093 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2765 pos 53.2% + 2437 neg 46.8% = 5202 sched 88.4% ret 683
c [sweep-3-1] 1007645 steps 31 queries 303.87 avg class size
c [sweep-3-1] 837 decisions 34 SAT calls 106.82 avg env size
c [sweep-3-1] 4994 variables remain 85% (891 retained 15%)
c [decomp-11] removed 8 variables
c [sweep-3-1] removed 8 vars (0 failed, 10 eqs, 5 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 8 vars in TOTAL (1 rounds, 30 queries)
c [score-distribution-4] 5522 pos 93.96%, 354 min 6.02%, 1 zero 0.02%
c [score-distribution-4] 1798 different 30.59% out of total 5877 variables
c [simplification-4] removed 22 variables 0.4% (5877 remain 22%)
c [simplification-4] removed 172 irredundant clauses 0.5% (33175 remain 43%)
c [simplification-4] maximum reduction of 1% = max (0%, 1%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 20000
c [simplification-4] penalized conflict interval 20000 = 1 * 20000
c [simplification-4] hard conflict limit 46010 (soft 36010 + delta 10000)
c [simplification-4] new conflict limit 36010 (hard 46010)
c 
c [simplification-5] limit 36010 conflicts (hard 46010) hit after 36010 conflicts
c [quatres-3] found 17705 quaternary clauses 77% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 2 double-self-subsuming ternary resolvents
c [quatres-3-2] added 191 single-self-subsuming ternary resolvents
c [quatres-3-2] added 113 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 5877 free variables schedulable
c [ternres-3] 317 ternary resolvents (35 bin, 282 trn)
c [ternres-3] 15 variables remain 0% (5862 retained 100%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 23475 xors of average arity 3.0
c [gauss-2] connected 70350 occurrences of 3504 variables (average 20.1)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 14 variables
c [transred-3] limit 1827397 with penalty 0 = 0 + 0
c [transred-3] removed 144 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 23 clauses out of 154 (15%) of length 6
c [cce-3-1] eliminated 208 clauses out of 993 (21%) of length 5
c [cce-3-1] eliminated 4 clauses out of 15598 (0%) of length 4
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 235 large clauses in 15000381 steps
c [cce-3-1] allowing another 7500190 steps for small clauses
c [cce-3-1] scheduling 14814 clauses = 1369 binary + 13445 ternary
c [cce-3-1] tried to eliminate 2374 small clauses 16%
c [cce-3-1] eliminated 30 binary clauses 2%
c [cce-3-1] eliminated 142 ternary clauses 1%
c [cce-3-1] eliminated 172 small clauses 1%
c [cce-3-1] eliminated 172 small clauses in 15000006 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 407 covered clauses in round 1
c [cce-3] eliminated 407 covered clauses in TOTAL during 1 rounds
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 2615 pos 52.5% + 2367 neg 47.5% = 4982 sched 85.0% ret 881
c [sweep-4-1] 1042375 steps 20 queries 359.70 avg class size
c [sweep-4-1] 1118 decisions 20 SAT calls 229.50 avg env size
c [sweep-4-1] 4789 variables remain 82% (1074 retained 18%)
c [decomp-13] removed 8 variables
c [sweep-4-1] removed 8 vars (0 failed, 2 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 8 vars in TOTAL (1 rounds, 19 queries)
c [score-distribution-5] 5708 pos 97.49%, 147 min 2.51%, 0 zero 0.00%
c [score-distribution-5] 2181 different 37.25% out of total 5855 variables
c [simplification-5] removed 22 variables 0.4% (5855 remain 22%)
c [simplification-5] removed 439 irredundant clauses 1.3% (32736 remain 42%)
c [simplification-5] maximum reduction of 1% = max (0%, 1%)
c [simplification-5] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-5] new conflict interval 30000
c [simplification-5] penalized conflict interval 30000 = 1 * 30000
c [simplification-5] hard conflict limit 81010 (soft 66010 + delta 15000)
c [simplification-5] new conflict limit 66010 (hard 81010)
c 
c [simplification-6] limit 66010 conflicts (hard 81010) hit after 66010 conflicts
c [quatres-4] found 19061 quaternary clauses 69% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-1] added 4 double-self-subsuming ternary resolvents
c [quatres-4-2] added 223 single-self-subsuming ternary resolvents
c [quatres-4-2] added 196 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 15 schedulable variables 0%
c [ternres-4] 287 ternary resolvents (37 bin, 250 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 16 at-most-one constraints of average size 3.8
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 16 out of 16 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-14] removed 19 variables
c [basicprobe-2] limit 9869844 penalty 1 = 1 + 0
c [basicprobe-2-0] 2752 probes remain 47% after last round
c [basicprobe-2-0] removed 0 variables, found 11550 hbrs
c [bate-1] eliminated 4 asymmetric tautologies during probing
c [unhide-3] limit 197396 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 10 tauts, 0 hbrs, 6481 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 23 transitive binary clauses
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 785 (0%) of length 5
c [cce-4-1] eliminated 115 clauses out of 15572 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 118 large clauses in 26248753 steps
c [cce-4-1] allowing another 13124376 steps for small clauses
c [cce-4-1] scheduling 14612 clauses = 1337 binary + 13275 ternary
c [cce-4-1] tried to eliminate 14612 small clauses 100%
c [cce-4-1] eliminated 74 binary clauses 6%
c [cce-4-1] eliminated 807 ternary clauses 6%
c [cce-4-1] eliminated 881 small clauses 6%
c [cce-4-1] eliminated 881 small clauses in 58786049 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 999 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 12726108 steps for small clauses
c [cce-4-2] scheduling 13731 clauses = 1263 binary + 12468 ternary
c [cce-4-2] tried to eliminate 13731 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 999 covered clauses in TOTAL during 2 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 5836 variables 100%
c [elim-5] limit of 39479379 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 180 variables 3% in round 1 in 6987742 steps
c [elim-5-1] backward subsumption/strengthening limit 6987700
c [elim-5-1-1] backward checking 569 touched variables 10%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 412745 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 180 = 3% variables out of 5836 scheduled
c [bca-4] limit of 10000000 steps and 63722 added (scaled 2)
c [bca-4] 351 out of 11314 literals actually usable 3%
c [bca-4] added 0 blocked clauses in 48179 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 11843810 penalty 0 = 0 + 0
c [sweep-5-1] 2442 pos 52.9% + 2178 neg 47.1% = 4620 sched 81.7% ret 1036
c [sweep-5-1] 11866563 steps 194 queries 41.55 avg class size
c [sweep-5-1] 8131 decisions 205 SAT calls 236.76 avg env size
c [sweep-5-1] 1705 variables remain 30% (3951 retained 70%)
c [decomp-15] removed 111 variables
c [sweep-5-1] removed 111 vars (0 failed, 98 eqs, 54 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 111 vars in TOTAL (1 rounds, 193 queries)
c [score-distribution-6] 5028 pos 90.68%, 517 min 9.32%, 0 zero 0.00%
c [score-distribution-6] 2115 different 38.14% out of total 5545 variables
c [simplification-6] removed 310 variables 5.3% (5545 remain 21%)
c [simplification-6] removed 1158 irredundant clauses 3.5% (31578 remain 41%)
c [simplification-6] maximum reduction of 5% = max (5%, 4%)
c [simplification-6] large reduction 5% >= 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 78010 (soft 68010 + delta 10000)
c [simplification-6] new conflict limit 68010 (hard 78010)
c 
c [simplification-7] limit 68010 conflicts (hard 78010) hit after 68010 conflicts
c [quatres-5] found 19825 quaternary clauses 71% in total
c [quatres-5-1] removed 8 duplicate quaternary clauses
c [quatres-5-1] added 8 double-self-subsuming ternary resolvents
c [quatres-5-2] added 58 single-self-subsuming ternary resolvents
c [quatres-5-2] added 85 quaternary resolvents
c [ternres-5] limit 4115619 with penalty 0 = 0 + 0
c [ternres-5] all 5545 free variables schedulable
c [ternres-5] 425 ternary resolvents (68 bin, 357 trn)
c [ternres-5] 75 variables remain 1% (5470 retained 99%)
c [decomp-16] removed 38 variables
c [simpleprobe-3] 156 schedulable variables 3%
c [simpleprobe-3] limit 16462476 penalty 0 = 0 + 0
c [decomp-17] removed 62 variables
c [simpleprobe-3] 773 variables remain 14% (4672 retained 86%)
c [simpleprobe-3] removed 62 variables, found 22628 hbrs, 0 units
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 89 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5445 variables 100%
c [block-3] limit of 12500000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 12 clauses out of 166 (7%) of length 6
c [cce-5-1] eliminated 140 clauses out of 781 (18%) of length 5
c [cce-5-1] eliminated 127 clauses out of 16290 (1%) of length 4
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 279 large clauses in 30000002 steps
c [cce-5-1] allowing another 15000001 steps for small clauses
c [cce-5-1] scheduling 2588 clauses = 911 binary + 1677 ternary
c [cce-5-1] tried to eliminate 1776 small clauses 69%
c [cce-5-1] eliminated 57 binary clauses 6%
c [cce-5-1] eliminated 173 ternary clauses 10%
c [cce-5-1] eliminated 230 small clauses 9%
c [cce-5-1] eliminated 230 small clauses in 30000003 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 509 covered clauses in round 1
c [cce-5] eliminated 509 covered clauses in TOTAL during 1 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 5445 variables 100%
c [elim-6] limit of 82312380 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 43 variables 1% in round 1 in 6264811 steps
c [elim-6-1] backward subsumption/strengthening limit 6264800
c [elim-6-1-1] backward checking 146 touched variables 3%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 214611 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 43 = 1% variables out of 5445 scheduled
c [elim-6] 43 < 1/100 * 5445 = 54 considered unsuccessful
c [sweep-6] limit 1234685 penalty 0 = 0 + 0
c [sweep-6-1] 923 pos 57.3% + 689 neg 42.7% = 1612 sched 29.8% ret 3790
c [sweep-6-1] 1264909 steps 41 queries 102.00 avg class size
c [sweep-6-1] 1125 decisions 40 SAT calls 129.97 avg env size
c [sweep-6-1] 1480 variables remain 27% (3922 retained 73%)
c [decomp-18] removed 27 variables
c [sweep-6-1] removed 27 vars (0 failed, 23 eqs, 16 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 27 vars in TOTAL (1 rounds, 40 queries)
c [score-distribution-7] 4309 pos 80.17%, 1066 min 19.83%, 0 zero 0.00%
c [score-distribution-7] 1699 different 31.61% out of total 5375 variables
c [simplification-7] removed 170 variables 3.1% (5375 remain 20%)
c [simplification-7] removed 1159 irredundant clauses 3.7% (30419 remain 39%)
c [simplification-7] maximum reduction of 4% = max (3%, 4%)
c [simplification-7] geometric conflict interval increment 6000 = 30000 / 5
c [simplification-7] new conflict interval 36000
c [simplification-7] penalized conflict interval 36000 = 1 * 36000
c [simplification-7] hard conflict limit 122010 (soft 104010 + delta 18000)
c [simplification-7] new conflict limit 104010 (hard 122010)
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 -   29.7    5375    30419     87777   25115   4425 44256   15   114    9  13%    750   38   19   10  204%
c 
c [simplification-8] limit 104010 conflicts (hard 122010) hit after 104010 conflicts
c [quatres-6] found 21085 quaternary clauses 64% in total
c [quatres-6-1] removed 4 duplicate quaternary clauses
c [quatres-6-1] added 4 double-self-subsuming ternary resolvents
c [quatres-6-2] added 232 single-self-subsuming ternary resolvents
c [quatres-6-2] added 416 quaternary resolvents
c [ternres-6] limit 6651484 with penalty 0 = 0 + 0
c [ternres-6] 57 schedulable variables 1%
c [ternres-6] 471 ternary resolvents (86 bin, 385 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 7631 xors of average arity 3.0
c [gauss-3] connected 22800 occurrences of 3016 variables (average 7.6)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-19] removed 84 variables
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 166 transitive binary clauses
c [cce-6] limit of 33257423 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 14 clauses out of 195 (7%) of length 6
c [cce-6-1] eliminated 24 clauses out of 700 (3%) of length 5
c [cce-6-1] eliminated 78 clauses out of 16119 (0%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 116 large clauses in 29437927 steps
c [cce-6-1] allowing another 14718963 steps for small clauses
c [cce-6-1] scheduling 2233 clauses = 759 binary + 1474 ternary
c [cce-6-1] tried to eliminate 2233 small clauses 100%
c [cce-6-1] eliminated 2 binary clauses 0%
c [cce-6-1] eliminated 67 ternary clauses 5%
c [cce-6-1] eliminated 69 small clauses 3%
c [cce-6-1] eliminated 69 small clauses in 32915257 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 185 covered clauses in round 1
c [cce-6-2] incomplete large round (ATE)
c [cce-6-2] allowing another 171087 steps for small clauses
c [cce-6-2] scheduling 2164 clauses = 757 binary + 1407 ternary
c [cce-6-2] tried to eliminate 20 small clauses 1%
c [cce-6-2] incomplete small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 185 covered clauses in TOTAL during 2 rounds
c [cce-6] 185 < 1/100 * 30390 = 303 considered unsuccessful
c [sweep-7] limit 1995445 penalty 0 = 0 + 0
c [sweep-7-1] 777 pos 54.5% + 649 neg 45.5% = 1426 sched 27.0% ret 3865
c [sweep-7-1] 2013380 steps 46 queries 123.46 avg class size
c [sweep-7-1] 1213 decisions 44 SAT calls 147.66 avg env size
c [sweep-7-1] 1302 variables remain 25% (3989 retained 75%)
c [decomp-20] removed 26 variables
c [sweep-7-1] removed 26 vars (0 failed, 22 eqs, 16 impls)
c [sweep-7] removed 26 vars in TOTAL (1 rounds, 45 queries)
c [score-distribution-8] 4990 pos 94.78%, 275 min 5.22%, 0 zero 0.00%
c [score-distribution-8] 2088 different 39.66% out of total 5265 variables
c [simplification-8] removed 110 variables 2.0% (5265 remain 20%)
c [simplification-8] removed 221 irredundant clauses 0.7% (30198 remain 39%)
c [simplification-8] maximum reduction of 2% = max (2%, 1%)
c [simplification-8] geometric conflict interval increment 12000 = 36000 / 3
c [simplification-8] new conflict interval 48000
c [simplification-8] penalized conflict interval 48000 = 1 * 48000
c [simplification-8] hard conflict limit 176010 (soft 152010 + delta 24000)
c [simplification-8] new conflict limit 152010 (hard 176010)
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 -   41.2    5265    30198    145874   39837   5353 43119   12    97   10  13%    911    3    7   12   59%
c 
c [simplification-9] limit 152010 conflicts (hard 176010) hit after 153253 conflicts
c [quatres-7] found 22351 quaternary clauses 56% in total
c [quatres-7-1] removed 19 duplicate quaternary clauses
c [quatres-7-1] added 13 double-self-subsuming ternary resolvents
c [quatres-7-2] added 240 single-self-subsuming ternary resolvents
c [quatres-7-2] added 466 quaternary resolvents
c [ternres-7] limit 9241355 with penalty 0 = 0 + 0
c [ternres-7] all 5265 free variables schedulable
c [ternres-7] 1063 ternary resolvents (153 bin, 910 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-21] removed 98 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 118 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 5167 variables 100%
c [elim-7] limit of 92413558 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 30 variables 1% in round 1 in 5978298 steps
c [elim-7-1] backward subsumption/strengthening limit 5978200
c [elim-7-1-1] backward checking 151 touched variables 3%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 0 clauses in 144618 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 30 = 1% variables out of 5167 scheduled
c [elim-7] 30 < 1/100 * 5167 = 51 considered unsuccessful
c [bca-5] limit of 10000000 steps and 59132 added (scaled 2)
c [bca-5] 563 out of 10276 literals actually usable 5%
c [bca-5] added 0 blocked clauses in 46646 steps
c [sweep-8] limit 2772406 penalty 0 = 0 + 0
c [sweep-8-1] 691 pos 55.4% + 556 neg 44.6% = 1247 sched 24.3% ret 3890
c [sweep-8-1] 2794280 steps 95 queries 46.78 avg class size
c [sweep-8-1] 1375 decisions 78 SAT calls 69.82 avg env size
c [sweep-8-1] 997 variables remain 19% (4140 retained 81%)
c [decomp-22] removed 52 variables
c [sweep-8-1] removed 52 vars (0 failed, 47 eqs, 42 impls)
c [sweep-8] removed 52 vars in TOTAL (1 rounds, 94 queries)
c [score-distribution-9] 4524 pos 88.97%, 561 min 11.03%, 0 zero 0.00%
c [score-distribution-9] 2098 different 41.26% out of total 5085 variables
c [simplification-9] removed 180 variables 3.4% (5085 remain 19%)
c [simplification-9] removed 912 irredundant clauses 3.0% (29286 remain 38%)
c [simplification-9] maximum reduction of 3% = max (3%, 3%)
c [simplification-9] geometric conflict interval increment 12000 = 48000 / 4
c [simplification-9] new conflict interval 60000
c [simplification-9] penalized conflict interval 60000 = 1 * 60000
c [simplification-9] hard conflict limit 243253 (soft 213253 + delta 30000)
c [simplification-9] new conflict limit 213253 (hard 243253)
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   44.4    5084    29286    166056   55436   5440 40465    9    62   13  15%    941  -32    5   12   44%
c -   49.0    5084    29285    199155   51434   5954 40547   12    93   10  13%   -614   -1    8   12   63%
c 
c [simplification-10] limit 213253 conflicts (hard 243253) hit after 231403 conflicts
c [quatres-8] found 24076 quaternary clauses 46% in total
c [quatres-8-1] removed 27 duplicate quaternary clauses
c [quatres-8-1] added 23 double-self-subsuming ternary resolvents
c [quatres-8-2] added 301 single-self-subsuming ternary resolvents
c [quatres-8-2] added 597 quaternary resolvents
c [ternres-8] limit 12523637 with penalty 0 = 0 + 0
c [ternres-8] all 5084 free variables schedulable
c [ternres-8] 818 ternary resolvents (159 bin, 659 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 782727 penalty 3 = 3 + 0
c [card-4] found 20 at-most-one constraints of average size 3.9
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 782727 for elimination
c [card-4] 20 out of 20 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-23] removed 146 variables
c [treelook-3] limit 313090 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 7392 literals 75%
c [treelook-3] scheduling used 313125 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 313090 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 490955 steps
c [treelook-3] 7388 literals remain 75%
c [treelook-3] 4560 variables remain to probed next time 92%
c [treelook-3] removed 0 variables, found 3257 hbrs
c [unhide-4] limit 313090 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 0 failed, 5214 tauts, 0 hbrs, 21175 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 36 transitive binary clauses
c [cce-7] limit of 31309092 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 15 clauses out of 181 (8%) of length 6
c [cce-7-1] eliminated 99 clauses out of 812 (12%) of length 5
c [cce-7-1] eliminated 152 clauses out of 15804 (1%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 266 large clauses in 27223422 steps
c [cce-7-1] allowing another 13611711 steps for small clauses
c [cce-7-1] scheduling 10940 clauses = 701 binary + 10239 ternary
c [cce-7-1] tried to eliminate 7566 small clauses 69%
c [cce-7-1] eliminated 19 binary clauses 3%
c [cce-7-1] eliminated 216 ternary clauses 2%
c [cce-7-1] eliminated 235 small clauses 2%
c [cce-7-1] eliminated 235 small clauses in 31309109 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 501 covered clauses in round 1
c [cce-7] eliminated 501 covered clauses in TOTAL during 1 rounds
c [sweep-9] limit 3757091 penalty 0 = 0 + 0
c [sweep-9-1] 542 pos 57.7% + 398 neg 42.3% = 940 sched 19.0% ret 3999
c [sweep-9-1] 3838999 steps 105 queries 24.39 avg class size
c [sweep-9-1] 2016 decisions 81 SAT calls 103.14 avg env size
c [sweep-9-1] 604 variables remain 12% (4335 retained 88%)
c [decomp-25] removed 115 variables
c [sweep-9-1] removed 115 vars (0 failed, 54 eqs, 46 impls)
c [sweep-9] removed 115 vars in TOTAL (1 rounds, 104 queries)
c [score-distribution-10] 4386 pos 90.92%, 438 min 9.08%, 0 zero 0.00%
c [score-distribution-10] 2101 different 43.55% out of total 4824 variables
c [simplification-10] removed 260 variables 5.1% (4824 remain 18%)
c [simplification-10] removed 579 irredundant clauses 2.0% (28705 remain 37%)
c [simplification-10] maximum reduction of 5% = max (5%, 2%)
c [simplification-10] large reduction 5% >= 5% limit
c [simplification-10] next conflict interval 2314 = min (231403/100, 60000)
c [simplification-10] penalized conflict interval 2314 = 1 * 2314
c [simplification-10] hard conflict limit 243717 (soft 233717 + delta 10000)
c [simplification-10] new conflict limit 233717 (hard 243717)
c 
c [simplification-11] limit 233717 conflicts (hard 243717) hit after 233718 conflicts
c [quatres-9] found 23657 quaternary clauses 47% in total
c [quatres-9-1] removed 70 duplicate quaternary clauses
c [quatres-9-1] added 32 double-self-subsuming ternary resolvents
c [quatres-9-2] added 202 single-self-subsuming ternary resolvents
c [quatres-9-2] added 760 quaternary resolvents
c [ternres-9] limit 12582922 with penalty 0 = 0 + 0
c [ternres-9] all 4824 free variables schedulable
c [ternres-9] 767 ternary resolvents (178 bin, 589 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-26] removed 93 variables
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 45 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 4731 variables 100%
c [block-4] limit of 15728652 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 6 blocked clauses
c [block-4] 6 < 1/100 * 28577 = 285 considered unsuccessful
c [cce-8] boosting limit by 10
c [cce-8] limit of 629146110 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 12 clauses out of 166 (7%) of length 6
c [cce-8-1] eliminated 108 clauses out of 15521 (1%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 120 large clauses in 21895734 steps
c [cce-8-1] allowing another 10947867 steps for small clauses
c [cce-8-1] scheduling 10642 clauses = 675 binary + 9967 ternary
c [cce-8-1] tried to eliminate 10642 small clauses 100%
c [cce-8-1] eliminated 2 binary clauses 0%
c [cce-8-1] eliminated 42 ternary clauses 0%
c [cce-8-1] eliminated 44 small clauses 0%
c [cce-8-1] eliminated 44 small clauses in 32438358 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 164 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 10894003 steps for small clauses
c [cce-8-2] scheduling 10598 clauses = 673 binary + 9925 ternary
c [cce-8-2] tried to eliminate 10598 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 164 covered clauses in TOTAL during 2 rounds
c [cce-8] 164 < 1/100 * 28571 = 285 considered unsuccessful
c [sweep-10] limit 3774876 penalty 0 = 0 + 0
c [sweep-10-1] 340 pos 61.7% + 211 neg 38.3% = 551 sched 11.6% ret 4180
c [sweep-10-1] 3794242 steps 70 queries 21.00 avg class size
c [sweep-10-1] 2078 decisions 78 SAT calls 126.58 avg env size
c [sweep-10-1] 360 variables remain 8% (4371 retained 92%)
c [decomp-27] removed 31 variables
c [sweep-10-1] removed 31 vars (0 failed, 27 eqs, 11 impls)
c [sweep-10] removed 31 vars in TOTAL (1 rounds, 69 queries)
c [score-distribution-11] 3794 pos 80.72%, 906 min 19.28%, 0 zero 0.00%
c [score-distribution-11] 1819 different 38.70% out of total 4700 variables
c [simplification-11] removed 124 variables 2.6% (4700 remain 18%)
c [simplification-11] removed 308 irredundant clauses 1.1% (28397 remain 36%)
c [simplification-11] maximum reduction of 3% = max (3%, 1%)
c [simplification-11] geometric conflict interval increment 15000 = 60000 / 4
c [simplification-11] new conflict interval 75000
c [simplification-11] penalized conflict interval 75000 = 1 * 75000
c [simplification-11] hard conflict limit 346218 (soft 308718 + delta 37500)
c [simplification-11] new conflict limit 308718 (hard 346218)
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   57.6    4699    28397    243523   84954   4753 35398   12   107   18  12%    192   19    7   12   59%
c -   58.5    4699    28397    247947   57402   4845 35418   12    83   10  15%   -887   -6   13   12  108%
c i   60.2    4698    28397    256324   64436   4990 35456   14    85   13  16%   -672   -4    6   12   53%
c -   64.0    4698    28397    295255   65092   5367 35526    9    46   11  20%    -25  -37    9   11   75%
c 
c [simplification-12] limit 308718 conflicts (hard 346218) hit after 316033 conflicts
c [quatres-10] found 25213 quaternary clauses 41% in total
c [quatres-10-1] removed 37 duplicate quaternary clauses
c [quatres-10-1] added 43 double-self-subsuming ternary resolvents
c [quatres-10-2] added 257 single-self-subsuming ternary resolvents
c [quatres-10-2] added 708 quaternary resolvents
c [ternres-10] limit 15928231 with penalty 0 = 0 + 0
c [ternres-10] all 4698 free variables schedulable
c [ternres-10] 534 ternary resolvents (103 bin, 431 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 398205 penalty 3 = 3 + 0
c [gauss-4] extracted 5607 xors of average arity 3.0
c [gauss-4] connected 16738 occurrences of 2353 variables (average 7.1)
c [gauss-4] limit 398205 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-28] removed 89 variables
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 54 transitive binary clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 4609 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1592823170 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 97 variables 2% in round 1 in 5412264 steps
c [elim-8-1] backward subsumption/strengthening limit 5412200
c [elim-8-1-1] backward checking 382 touched variables 8%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 204104 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 97 = 2% variables out of 4609 scheduled
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 47784690 penalty 0 = 0 + 0
c [sweep-11-1] 190 pos 57.2% + 142 neg 42.8% = 332 sched 7.4% ret 4180
c [sweep-11-1] 7201516 steps 158 queries 10.98 avg class size
c [sweep-11-1] 2769 decisions 150 SAT calls 61.74 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-29] removed 77 variables
c [sweep-11-1] removed 77 vars (0 failed, 69 eqs, 41 impls)
c [sweep-11-2] 2300 pos 51.9% + 2135 neg 48.1% = 4435 sched 100.0% ret 0
c [sweep-11-2] 40674021 steps 700 queries 18.85 avg class size
c [sweep-11-2] 13213 decisions 653 SAT calls 83.72 avg env size
c [sweep-11-2] 60 variables remain 1% (4375 retained 99%)
c [decomp-30] removed 391 variables
c [sweep-11-2] removed 391 vars (0 failed, 396 eqs, 271 impls)
c [sweep-11] removed 468 vars in TOTAL (2 rounds, 856 queries)
c [score-distribution-12] 2600 pos 64.29%, 1444 min 35.71%, 0 zero 0.00%
c [score-distribution-12] 1356 different 33.53% out of total 4044 variables
c [simplification-12] removed 654 variables 13.9% (4044 remain 15%)
c [simplification-12] removed 1822 irredundant clauses 6.4% (26575 remain 34%)
c [simplification-12] maximum reduction of 14% = max (14%, 6%)
c [simplification-12] large reduction 14% >= 5% limit
c [simplification-12] next conflict interval 3160 = min (316033/100, 75000)
c [simplification-12] penalized conflict interval 3160 = 1 * 3160
c [simplification-12] hard conflict limit 329193 (soft 319193 + delta 10000)
c [simplification-12] new conflict limit 319193 (hard 329193)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   67.4    4043    26575    319056   73458   3289 27352   10    64   13  16%    295   -8   13   11  117%
c 
c [simplification-13] limit 319193 conflicts (hard 329193) hit after 329193 conflicts
c [quatres-11] found 23129 quaternary clauses 42% in total
c [quatres-11-1] removed 216 duplicate quaternary clauses
c [quatres-11-1] added 6 double-self-subsuming ternary resolvents
c [quatres-11-2] added 61 single-self-subsuming ternary resolvents
c [quatres-11-2] added 662 quaternary resolvents
c [ternres-11] limit 16435286 with penalty 0 = 0 + 0
c [ternres-11] all 4043 free variables schedulable
c [ternres-11] 218 ternary resolvents (30 bin, 188 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-31] removed 22 variables
c [basicprobe-3] limit 20544108 penalty 2 = 2 + 0
c [basicprobe-3-0] 2054 sched 51%, 0 failed, 0 lifted, 4134 hbrs
c [decomp-32] removed 1 variables
c [basicprobe-3-1] 2190 probes remain 54% after last round
c [basicprobe-3-1] removed 1 variables, found 4589 hbrs
c [bate-2] eliminated 2 asymmetric tautologies during probing
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 101 transitive binary clauses
c [cce-9] limit of 41088216 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 47 clauses out of 249 (19%) of length 6
c [cce-9-1] eliminated 92 clauses out of 1223 (8%) of length 5
c [cce-9-1] eliminated 153 clauses out of 14229 (1%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 292 large clauses in 19772094 steps
c [cce-9-1] allowing another 9886047 steps for small clauses
c [cce-9-1] scheduling 8576 clauses = 557 binary + 8019 ternary
c [cce-9-1] tried to eliminate 8576 small clauses 100%
c [cce-9-1] eliminated 36 binary clauses 6%
c [cce-9-1] eliminated 140 ternary clauses 2%
c [cce-9-1] eliminated 176 small clauses 2%
c [cce-9-1] eliminated 176 small clauses in 25573108 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] completed small and large (ACCE)
c [cce-9-1] eliminated 468 covered clauses in round 1
c [cce-9-2] eliminated 9 clauses out of 1131 (1%) of length 5
c [cce-9-2] eliminated 5 clauses out of 14076 (0%) of length 4
c [cce-9-2] incomplete large round (ACCE)
c [cce-9-2] eliminated 14 large clauses in 15515112 steps
c [cce-9-2] allowing another 7757556 steps for small clauses
c [cce-9-2] scheduling 8407 clauses = 521 binary + 7886 ternary
c [cce-9-2] tried to eliminate 5378 small clauses 64%
c [cce-9-2] eliminated 13 binary clauses 2%
c [cce-9-2] eliminated 11 ternary clauses 0%
c [cce-9-2] eliminated 24 small clauses 0%
c [cce-9-2] eliminated 24 small clauses in 15515137 steps
c [cce-9-2] incomplete small round (ACCE)
c [cce-9-2] eliminated 38 covered clauses in round 2
c [cce-9] eliminated 506 covered clauses in TOTAL during 2 rounds
c [bca-6] limit of 10000000 steps and 51360 added (scaled 2)
c [bca-6] 290 out of 8044 literals actually usable 4%
c [bca-6] added 0 blocked clauses in 82133 steps
c [sweep-12] limit 4930585 penalty 0 = 0 + 0
c [sweep-12-1] 31 pos 56.4% + 24 neg 43.6% = 55 sched 1.4% ret 3966
c [sweep-12-1] 1611577 steps 38 queries 7.37 avg class size
c [sweep-12-1] 709 decisions 37 SAT calls 60.73 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-33] removed 14 variables
c [sweep-12-1] removed 14 vars (0 failed, 13 eqs, 5 impls)
c [sweep-12-2] 2150 pos 53.7% + 1857 neg 46.3% = 4007 sched 100.0% ret 0
c [sweep-12-2] 3679481 steps 46 queries 168.15 avg class size
c [sweep-12-2] 2688 decisions 46 SAT calls 201.11 avg env size
c [sweep-12-2] 2454 variables remain 61% (1553 retained 39%)
c [decomp-34] removed 2 variables
c [sweep-12-2] removed 2 vars (0 failed, 2 eqs, 0 impls)
c [sweep-12] removed 16 vars in TOTAL (2 rounds, 82 queries)
c [score-distribution-13] 3314 pos 82.75%, 691 min 17.25%, 0 zero 0.00%
c [score-distribution-13] 1801 different 44.97% out of total 4005 variables
c [simplification-13] removed 38 variables 0.9% (4005 remain 15%)
c [simplification-13] removed 1158 irredundant clauses 4.4% (25417 remain 33%)
c [simplification-13] maximum reduction of 4% = max (1%, 4%)
c [simplification-13] geometric conflict interval increment 15000 = 75000 / 5
c [simplification-13] new conflict interval 90000
c [simplification-13] penalized conflict interval 90000 = 1 * 90000
c [simplification-13] hard conflict limit 464193 (soft 419193 + delta 45000)
c [simplification-13] new conflict limit 419193 (hard 464193)
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   70.8    4004    25417    331502   82946   3538 31877   11    76   16  15%   -403    3    8   11   72%
c -   72.7    4004    25417    346888   64082   3687 31894   12    84   11  14%   -260   12   14   11  129%
c i   73.7    4003    25417    353196   69576   3742 31908   12    89   13  14%   -142   15   10   11   87%
c -   78.8    4003    25417    392989   68538   4120 31984   10    31   11  32%    201  -43    8   11   73%
c i   79.9    4002    25417    400129   74020   4195 32003   10    52   13  20%    286  -20    6   11   52%
c i   82.3    3987    25417    425162   95638   4298 32022   11    58   16  19%     12  -12    7   11   60%
c i   83.4    3983    25417    432946  102155   4326 32029   12    58   19  20%   -228  -11   14   11  121%
c -   84.0    3983    25417    439262   74338   4335 32030   12    57   12  21%   -225  -12   13   11  115%
c 
c [simplification-14] limit 419193 conflicts (hard 464193) hit after 464193 conflicts
c [quatres-12] found 23583 quaternary clauses 36% in total
c [quatres-12-1] removed 21 duplicate quaternary clauses
c [quatres-12-1] added 44 double-self-subsuming ternary resolvents
c [quatres-12-2] added 103 single-self-subsuming ternary resolvents
c [quatres-12-2] added 233 quaternary resolvents
c [ternres-12] limit 21861960 with penalty 0 = 0 + 0
c [ternres-12] all 3983 free variables schedulable
c [ternres-12] 259 ternary resolvents (21 bin, 238 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-5] limit 1093098 penalty 2 = 2 + 0
c [gauss-5] extracted 16620 xors of average arity 3.0
c [gauss-5] connected 49785 occurrences of 2478 variables (average 20.1)
c [gauss-5] limit 1093098 penalty 2 = 2 + 0
c [gauss-5] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-35] removed 26 variables
c [simpleprobe-4] 519 schedulable variables 13%
c [simpleprobe-4] limit 87447840 penalty 0 = 0 + 0
c [decomp-36] removed 59 variables
c [simpleprobe-4] 993 variables remain 25% (2905 retained 75%)
c [simpleprobe-4] removed 59 variables, found 69952 hbrs, 3 units
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 76 transitive binary clauses
c [cce-10] limit of 109309800 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 15 clauses out of 97 (15%) of length 6
c [cce-10-1] eliminated 2 clauses out of 1213 (0%) of length 5
c [cce-10-1] eliminated 81 clauses out of 13848 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 98 large clauses in 13254512 steps
c [cce-10-1] allowing another 6627256 steps for small clauses
c [cce-10-1] scheduling 7958 clauses = 395 binary + 7563 ternary
c [cce-10-1] tried to eliminate 7958 small clauses 100%
c [cce-10-1] eliminated 5 binary clauses 1%
c [cce-10-1] eliminated 11 ternary clauses 0%
c [cce-10-1] eliminated 16 small clauses 0%
c [cce-10-1] eliminated 16 small clauses in 16594683 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 114 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 6590328 steps for small clauses
c [cce-10-2] scheduling 7942 clauses = 390 binary + 7552 ternary
c [cce-10-2] tried to eliminate 7942 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 114 covered clauses in TOTAL during 2 rounds
c [cce-10] 114 < 1/100 * 24709 = 247 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 3898 variables 100%
c [elim-9] limit of 218619601 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 111 variables 3% in round 1 in 5061687 steps
c [elim-9-1] backward subsumption/strengthening limit 5061600
c [elim-9-1-1] backward checking 416 touched variables 11%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 253685 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 111 = 3% variables out of 3898 scheduled
c [sweep-13] limit 6558588 penalty 0 = 0 + 0
c [sweep-13-1] 1329 pos 56.7% + 1016 neg 43.3% = 2345 sched 61.9% ret 1442
c [sweep-13-1] 6585539 steps 125 queries 56.97 avg class size
c [sweep-13-1] 3461 decisions 124 SAT calls 116.81 avg env size
c [sweep-13-1] 776 variables remain 20% (3011 retained 80%)
c [decomp-37] removed 23 variables
c [sweep-13-1] removed 23 vars (0 failed, 20 eqs, 16 impls)
c [sweep-13] removed 23 vars in TOTAL (1 rounds, 124 queries)
c [score-distribution-14] 3161 pos 83.98%, 603 min 16.02%, 0 zero 0.00%
c [score-distribution-14] 1906 different 50.64% out of total 3764 variables
c [simplification-14] removed 219 variables 5.5% (3764 remain 14%)
c [simplification-14] removed 1675 irredundant clauses 6.6% (23742 remain 31%)
c [simplification-14] maximum reduction of 7% = max (5%, 7%)
c [simplification-14] large reduction 7% >= 5% limit
c [simplification-14] next conflict interval 4641 = min (464193/100, 90000)
c [simplification-14] penalized conflict interval 4641 = 1 * 4641
c [simplification-14] hard conflict limit 478834 (soft 468834 + delta 10000)
c [simplification-14] new conflict limit 468834 (hard 478834)
c 
c [simplification-15] limit 468834 conflicts (hard 478834) hit after 478834 conflicts
c [quatres-13] found 22890 quaternary clauses 37% in total
c [quatres-13-1] removed 61 duplicate quaternary clauses
c [quatres-13-1] added 7 double-self-subsuming ternary resolvents
c [quatres-13-2] added 52 single-self-subsuming ternary resolvents
c [quatres-13-2] added 213 quaternary resolvents
c [ternres-13] limit 22223831 with penalty 0 = 0 + 0
c [ternres-13] all 3764 free variables schedulable
c [ternres-13] 79 ternary resolvents (10 bin, 69 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 694494 penalty 4 = 4 + 0
c [card-5] found 8 at-most-one constraints of average size 3.6
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 694494 for elimination
c [card-5] 8 out of 8 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-6] limit 2222383 penalty 1 = 1 + 0
c [gauss-6] extracted 14485 xors of average arity 3.0
c [gauss-6] connected 43439 occurrences of 2462 variables (average 17.6)
c [gauss-6] limit 2222383 penalty 1 = 1 + 0
c [gauss-6] connected 16576 occurrences of 2462 variables (average 6.7)
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-38] removed 5 variables
c [unhide-5] limit 277797 with penalty 4 = 4 + 0
c [unhide-5-5] 0 units, 0 failed, 24 tauts, 0 hbrs, 7207 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 35 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 3759 variables 100%
c [elim-10] limit of 444476627 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 17 variables 0% in round 1 in 4914448 steps
c [elim-10-1] backward subsumption/strengthening limit 4914400
c [elim-10-1-1] backward checking 93 touched variables 2%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 107305 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 17 = 0% variables out of 3759 scheduled
c [elim-10] 17 < 1/100 * 3759 = 37 considered unsuccessful
c [sweep-14] limit 6667149 penalty 0 = 0 + 0
c [sweep-14-1] 431 pos 56.3% + 335 neg 43.7% = 766 sched 20.5% ret 2976
c [sweep-14-1] 6983979 steps 114 queries 31.96 avg class size
c [sweep-14-1] 3468 decisions 110 SAT calls 94.36 avg env size
c [sweep-14-1] 280 variables remain 7% (3462 retained 93%)
c [decomp-39] removed 28 variables
c [sweep-14-1] removed 28 vars (0 failed, 27 eqs, 15 impls)
c [sweep-14] removed 28 vars in TOTAL (1 rounds, 113 queries)
c [score-distribution-15] 1005 pos 27.06%, 2709 min 72.94%, 0 zero 0.00%
c [score-distribution-15] 360 different 9.69% out of total 3714 variables
c [simplification-15] removed 50 variables 1.3% (3714 remain 14%)
c [simplification-15] removed 133 irredundant clauses 0.6% (23609 remain 30%)
c [simplification-15] maximum reduction of 1% = max (1%, 1%)
c [simplification-15] geometric conflict interval increment 45000 = 90000 / 2
c [simplification-15] new conflict interval 135000
c [simplification-15] penalized conflict interval 135000 = 1 * 135000
c [simplification-15] hard conflict limit 681334 (soft 613834 + delta 67500)
c [simplification-15] new conflict limit 613834 (hard 681334)
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 -   89.8    3714    23609    493950   72158   3725 72555   10    29   12  33%    482  -24    9   11   83%
c -   93.2    3714    23609    539240   73261   3788 72565   14    83   13  17%    752   41   16   11  146%
c i   95.9    3713    23609    589767   98109   3913 72581    6     7   19  90%    898  -25    4    9   44%
c -   98.5    3481    23609    602720   74227   3991 72588   12    59   13  20%  -1122   23   10   10   98%
c i   98.8    3480    23609    610040   79710   4029 72596   10    32   15  31%   -895   -4    6   10   63%
c -  100.8    3480    23609    648747   79631   4101 72608   10    23   12  42%   -217  -14    9   10   86%
c 
c [simplification-16] limit 613834 conflicts (hard 681334) hit after 681334 conflicts
c [quatres-14] found 20365 quaternary clauses 36% in total
c [quatres-14-1] removed 15 duplicate quaternary clauses
c [quatres-14-1] added 13 double-self-subsuming ternary resolvents
c [quatres-14-2] added 38 single-self-subsuming ternary resolvents
c [quatres-14-2] added 308 quaternary resolvents
c [ternres-14] limit 27672652 with penalty 0 = 0 + 0
c [ternres-14] all 3480 free variables schedulable
c [ternres-14] 75 ternary resolvents (5 bin, 70 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-40] removed 330 variables
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 114 transitive binary clauses
c [transred-14] found 2 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 3382 variables 100%
c [block-5] limit of 17295408 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 46 blocked clauses
c [block-5] 46 < 1/100 * 21154 = 211 considered unsuccessful
c [cce-11] limit of 69181632 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 8 clauses out of 8 (100%) of length 7
c [cce-11-1] eliminated 14 clauses out of 55 (25%) of length 6
c [cce-11-1] eliminated 172 clauses out of 1069 (16%) of length 5
c [cce-11-1] eliminated 225 clauses out of 12077 (2%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 419 large clauses in 7889375 steps
c [cce-11-1] allowing another 3944687 steps for small clauses
c [cce-11-1] scheduling 6553 clauses = 314 binary + 6239 ternary
c [cce-11-1] tried to eliminate 6553 small clauses 100%
c [cce-11-1] eliminated 11 binary clauses 4%
c [cce-11-1] eliminated 111 ternary clauses 2%
c [cce-11-1] eliminated 122 small clauses 2%
c [cce-11-1] eliminated 122 small clauses in 8965396 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 541 covered clauses in round 1
c [cce-11-2] eliminated 10 clauses out of 11852 (0%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 10 large clauses in 3533941 steps
c [cce-11-2] allowing another 1766970 steps for small clauses
c [cce-11-2] scheduling 6431 clauses = 303 binary + 6128 ternary
c [cce-11-2] tried to eliminate 6431 small clauses 100%
c [cce-11-2] eliminated 1 binary clauses 0%
c [cce-11-2] eliminated 1 small clauses 0%
c [cce-11-2] eliminated 1 small clauses in 4653240 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 11 covered clauses in round 2
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] allowing another 1763809 steps for small clauses
c [cce-11-3] scheduling 6430 clauses = 302 binary + 6128 ternary
c [cce-11-3] tried to eliminate 6430 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 552 covered clauses in TOTAL during 3 rounds
c [sweep-15] limit 8301795 penalty 0 = 0 + 0
c [sweep-15-1] 105 pos 47.1% + 118 neg 52.9% = 223 sched 6.6% ret 3148
c [sweep-15-1] 4731534 steps 109 queries 8.73 avg class size
c [sweep-15-1] 2218 decisions 108 SAT calls 101.43 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-41] removed 23 variables
c [sweep-15-1] removed 23 vars (0 failed, 16 eqs, 9 impls)
c [sweep-15-2] 1765 pos 52.7% + 1583 neg 47.3% = 3348 sched 100.0% ret 0
c [sweep-15-2] 3585307 steps 66 queries 79.70 avg class size
c [sweep-15-2] 2029 decisions 66 SAT calls 131.30 avg env size
c [sweep-15-2] 1916 variables remain 57% (1432 retained 43%)
c [decomp-42] removed 1 variables
c [sweep-15-2] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-15] removed 24 vars in TOTAL (2 rounds, 173 queries)
c [score-distribution-16] 965 pos 28.83%, 2382 min 71.17%, 0 zero 0.00%
c [score-distribution-16] 353 different 10.55% out of total 3347 variables
c [simplification-16] removed 133 variables 3.8% (3347 remain 13%)
c [simplification-16] removed 3087 irredundant clauses 13.1% (20522 remain 26%)
c [simplification-16] maximum reduction of 13% = max (4%, 13%)
c [simplification-16] large reduction 13% >= 5% limit
c [simplification-16] next conflict interval 6813 = min (681334/100, 135000)
c [simplification-16] penalized conflict interval 6813 = 1 * 6813
c [simplification-16] hard conflict limit 698147 (soft 688147 + delta 10000)
c [simplification-16] new conflict limit 688147 (hard 698147)
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  103.7    3346    20522    682125   92043   3528 65998    9    15   17  60%    278  -15   10   10  107%
c i  103.9    2767    20522    683982   93481   3553 66006    9    28   17  31%   -627   -2    5   10   50%
c i  105.6    2765    20522    691143   99923   3603 66008   14    77   19  18%   -649   44   14   10  136%
c 
c [simplification-17] limit 688147 conflicts (hard 698147) hit after 698148 conflicts
c [quatres-15] found 14752 quaternary clauses 38% in total
c [quatres-15-1] removed 6 duplicate quaternary clauses
c [quatres-15-1] added 15 double-self-subsuming ternary resolvents
c [quatres-15-2] added 51 single-self-subsuming ternary resolvents
c [quatres-15-2] added 395 quaternary resolvents
c [ternres-15] limit 29407576 with penalty 0 = 0 + 0
c [ternres-15] all 2765 free variables schedulable
c [ternres-15] 61 ternary resolvents (7 bin, 54 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-7] limit 1470378 penalty 2 = 2 + 0
c [gauss-7] extracted 29593 xors of average arity 3.3
c [gauss-7] connected 97365 occurrences of 2524 variables (average 38.6)
c [gauss-7] limit 1470378 penalty 2 = 2 + 0
c [decomp-43] removed 149 variables
c [gauss-7] exported 0 unary, 5 binary and 9 ternary equations
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 177 transitive binary clauses
c [cce-12] limit of 147037884 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 4 clauses out of 457 (1%) of length 5
c [cce-12-1] eliminated 94 clauses out of 8818 (1%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 98 large clauses in 4909681 steps
c [cce-12-1] allowing another 2454840 steps for small clauses
c [cce-12-1] scheduling 5142 clauses = 250 binary + 4892 ternary
c [cce-12-1] tried to eliminate 5142 small clauses 100%
c [cce-12-1] eliminated 1 binary clauses 0%
c [cce-12-1] eliminated 41 ternary clauses 1%
c [cce-12-1] eliminated 42 small clauses 1%
c [cce-12-1] eliminated 42 small clauses in 5544353 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 140 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 1157690 steps for small clauses
c [cce-12-2] scheduling 5100 clauses = 249 binary + 4851 ternary
c [cce-12-2] tried to eliminate 5100 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 140 covered clauses in TOTAL during 2 rounds
c [cce-12] 140 < 1/100 * 15599 = 155 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 2616 variables 100%
c [elim-11] limit of 294075769 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 208 variables 8% in round 1 in 2465202 steps
c [elim-11-1] backward subsumption/strengthening limit 2465200
c [elim-11-1-1] backward checking 398 touched variables 15%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 5 and strengthened 0 clauses in 165280 steps
c [elim-11-1] rescheduled 12 variables 0% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 114710 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 208 = 8% variables out of 2616 scheduled
c [sweep-16] limit 8822273 penalty 0 = 0 + 0
c [sweep-16-1] 673 pos 54.4% + 565 neg 45.6% = 1238 sched 51.4% ret 1170
c [sweep-16-1] 4850375 steps 137 queries 24.99 avg class size
c [sweep-16-1] 4395 decisions 125 SAT calls 105.99 avg env size
c [sweep-16-1] fully completed sweeping round
c [decomp-45] removed 34 variables
c [sweep-16-1] removed 34 vars (0 failed, 33 eqs, 29 impls)
c [sweep-16-2] 1280 pos 53.9% + 1094 neg 46.1% = 2374 sched 100.0% ret 0
c [sweep-16-2] 3975924 steps 77 queries 49.35 avg class size
c [sweep-16-2] 4095 decisions 83 SAT calls 164.00 avg env size
c [sweep-16-2] 125 variables remain 5% (2249 retained 95%)
c [decomp-46] removed 9 variables
c [sweep-16-2] removed 9 vars (0 failed, 8 eqs, 1 impls)
c [sweep-16] removed 43 vars in TOTAL (2 rounds, 212 queries)
c [score-distribution-17] 2052 pos 86.77%, 313 min 13.23%, 0 zero 0.00%
c [score-distribution-17] 1294 different 54.71% out of total 2365 variables
c [simplification-17] removed 400 variables 14.5% (2365 remain 9%)
c [simplification-17] removed 5513 irredundant clauses 26.9% (15009 remain 19%)
c [simplification-17] maximum reduction of 27% = max (14%, 27%)
c [simplification-17] large reduction 27% >= 5% limit
c [simplification-17] next conflict interval 6981 = min (698148/100, 135000)
c [simplification-17] penalized conflict interval 6981 = 1 * 6981
c [simplification-17] hard conflict limit 715129 (soft 705129 + delta 10000)
c [simplification-17] new conflict limit 705129 (hard 715129)
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  108.2    2364    15009    698278   55053   2629  3094   13    84   11  16%   -579   46   13   11  125%
c i  108.3    2363    15009    698481   55230   2629  3097   14    84   11  16%   -594   46   14   11  137%
c i  108.8    2362    15008    701667   58048   2662  3100   13    84   14  15%   -604   44   13   11  117%
c i  109.3    2361    15008    710540   65698   2718  3112   10    68   11  15%   -446   24   14   11  130%
c i  109.3    2360    15008    710560   65717   2718  3112   10    68   11  15%   -448   24   14   11  134%
c i  109.4    2359    15008    710997   66107   2722  3113   11    68   15  16%   -486   24   15   11  145%
c i  109.5    2358    15007    711515   66572   2732  3116   11    67   15  17%   -512   23   13   11  119%
c i  109.6    1317    15006    711585   66631   2733  3118   11    67   15  17%   -514   23   13   11  122%
c i  109.8    1315    15006    712819   67771   2738  3119   14    68   12  20%   -529   23   21   11  194%
c i  110.0    1314    15006    713465   68363   2745  3121   14    68   13  20%   -532   23   17   11  157%
c i  110.1    1313    15006    714282   69065   2756  3125   14    67   13  21%   -529   21   14   11  131%
c i  110.2    1312    15006    714611   69371   2760  3125   14    66   13  22%   -528   21   19   11  172%
c 
c [simplification-18] limit 705129 conflicts (hard 715129) hit after 715130 conflicts
c [quatres-16] found 5718 quaternary clauses 40% in total
c [quatres-16-1] removed 10 duplicate quaternary clauses
c [quatres-16-1] added 5 double-self-subsuming ternary resolvents
c [quatres-16-2] added 37 single-self-subsuming ternary resolvents
c [quatres-16-2] added 210 quaternary resolvents
c [ternres-16] limit 30114054 with penalty 0 = 0 + 0
c [ternres-16] all 1312 free variables schedulable
c [ternres-16] 30 ternary resolvents (4 bin, 26 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-8] limit 3011405 penalty 1 = 1 + 0
c [gauss-8] extracted 15417 xors of average arity 3.1
c [gauss-8] connected 48303 occurrences of 1220 variables (average 39.6)
c [gauss-8] limit 3011405 penalty 1 = 1 + 0
c [gauss-8] connected 29566 occurrences of 1220 variables (average 24.2)
c [gauss-8] connected 18788 occurrences of 1220 variables (average 15.4)
c [gauss-8] connected 14462 occurrences of 1220 variables (average 11.9)
c [gauss-8] connected 12255 occurrences of 1220 variables (average 10.0)
c [gauss-8] fully completed
c [decomp-47] removed 217 variables
c [gauss-8] exported 1 unary, 4 binary and 37 ternary equations
c [treelook-4] limit 376425 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 1769 literals 81%
c [treelook-4] scheduling used 138310 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 376425 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 143388 steps
c [treelook-4] fully completed tree based probing
c [decomp-49] removed 4 variables
c [treelook-4] removed 6 variables, found 260 hbrs
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 6 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 1089 variables 100%
c [elim-12] limit of 602281095 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 113 variables 10% in round 1 in 966637 steps
c [elim-12-1] backward subsumption/strengthening limit 966600
c [elim-12-1-1] backward checking 309 touched variables 28%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 2 and strengthened 0 clauses in 50607 steps
c [elim-12-1] rescheduled 3 variables 0% by backward subsumption
c [elim-12-2] eliminated 2 variables 0% in round 2 in 847 steps
c [elim-12-2] backward subsumption/strengthening limit 800
c [elim-12-2-1] backward checking 6 touched variables 1%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 0 and strengthened 0 clauses in 801 steps
c [elim-12-2] fully rescheduled 973 variables 89%
c [elim-12-3] eliminated 19 variables 2% in round 3 in 911937 steps
c [elim-12-3] backward subsumption/strengthening limit 911900
c [elim-12-3-1] backward checking 28 touched variables 3%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 0 and strengthened 0 clauses in 15590 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 135 = 12% variables out of 1089 scheduled
c [bca-7] limit of 10000000 steps and 12382 added (scaled 2)
c [bca-7] 27 out of 1910 literals actually usable 1%
c [bca-7] not enough literals usable
c [bca-7] added 0 blocked clauses in 19812 steps
c [sweep-17] limit 9034216 penalty 0 = 0 + 0
c [sweep-17-1] 18 pos 64.3% + 10 neg 35.7% = 28 sched 2.9% ret 926
c [sweep-17-1] 195001 steps 17 queries 6.47 avg class size
c [sweep-17-1] 1194 decisions 16 SAT calls 97.75 avg env size
c [sweep-17-1] fully completed sweeping round
c [decomp-50] removed 2 variables
c [sweep-17-1] removed 2 vars (0 failed, 2 eqs, 1 impls)
c [sweep-17-2] 489 pos 51.4% + 463 neg 48.6% = 952 sched 100.0% ret 0
c [sweep-17-2] 436065 steps 70 queries 25.60 avg class size
c [sweep-17-2] 2855 decisions 66 SAT calls 75.73 avg env size
c [sweep-17-2] fully completed sweeping round
c [decomp-51] removed 7 variables
c [sweep-17-2] removed 7 vars (0 failed, 7 eqs, 6 impls)
c [sweep-17-3] 484 pos 51.2% + 461 neg 48.8% = 945 sched 100.0% ret 0
c [sweep-17-3] 453877 steps 51 queries 31.08 avg class size
c [sweep-17-3] 2468 decisions 50 SAT calls 82.50 avg env size
c [sweep-17-3] fully completed sweeping round
c [decomp-52] removed 3 variables
c [sweep-17-3] removed 3 vars (0 failed, 3 eqs, 1 impls)
c [sweep-17] removed 12 vars in TOTAL (3 rounds, 135 queries)
c [score-distribution-18] 928 pos 98.51%, 14 min 1.49%, 0 zero 0.00%
c [score-distribution-18] 688 different 73.04% out of total 942 variables
c [simplification-18] removed 370 variables 28.2% (942 remain 4%)
c [simplification-18] removed 9096 irredundant clauses 60.6% (5910 remain 8%)
c [simplification-18] maximum reduction of 61% = max (28%, 61%)
c [simplification-18] large reduction 61% >= 5% limit
c [simplification-18] next conflict interval 7151 = min (715130/100, 135000)
c [simplification-18] penalized conflict interval 7151 = 1 * 7151
c [simplification-18] hard conflict limit 732281 (soft 722281 + delta 10000)
c [simplification-18] new conflict limit 722281 (hard 732281)
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  110.7     941     5910    715291   20294   1064    55   15    66    4  22%   -524   20   16   11  145%
c i  110.7     940     5907    715387   20376   1068    55   14    66    4  22%   -524   20   14   11  128%
c i  110.7     938     5907    715390   20376   1070    55   14    66    4  22%   -524   20   14   11  126%
c i  110.7     937     5906    715410   20382   1074    60   14    65    4  22%   -524   20   13   11  119%
c i  110.7     936     5905    715465   20389   1091    65   14    65    4  22%   -524   19   12   11  106%
c i  110.7     935     5905    715467   20389   1090    66   14    65    4  22%   -524   19   12   11  105%
c i  110.7     928     5905    715506   20408   1094    71   14    65    4  22%   -524   19   10   11   95%
c i  110.7     927     5905    715508   20408   1094    72   14    65    4  22%   -524   19   10   11   94%
c i  110.7     906     5904    715514   20408   1094    72   14    64    4  22%   -524   19   10   11   94%
c i  110.7     905     5904    715520   20406   1095    74   14    64    4  22%   -524   19   10   11   93%
c i  110.7     904     5904    715528   20409   1093    75   14    64    4  22%   -524   19   10   11   92%
c i  110.7     903     5902    715538   20407   1094    77   14    64    4  22%   -523   19   10   11   90%
c i  110.7     900     5902    715540   20407   1094    78   14    64    4  22%   -523   18   10   11   90%
c i  110.7     898     5902    715542   20407   1094    79   14    64    4  22%   -523   18   10   11   89%
c 0  110.7     894     5902    715542   20407   1094    79   14    64    4  22%   -523   18   10   11   89%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 6 basic ate = 4 trn 67% + 2 lrg 33% in 2 updates
c bcas: 7 count, 48 added (64 skipped), 247925 steps
c bkwd: tried 51512 clauses, 103008 lits, 2.00 lits/clause
c bkwd: checked 1961948 occs, 38.09 occs/clause, 19.05 occs/lit
c bkwd: subsumed 2 binary, 2 ternary, 7 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 17 large (0% self)
c blkd: 5 bces, 153 removed, 912890 resolutions, 2139936 steps
c blkd: 484 blocking literals 1%, 15 pure
c bump: 683554 bumped seen, 33416912 lits 48.9 on average
c card: 5 count, 0 units, 0 am1, 90827351 steps
c card: 3 rescheduled, 29 eliminated, 9640 resolved, 2363 subsumed
c card: 75 at-most-one constraints found, average size 3.52
c card: 75 at-most-one constraints used 100%, average size 3.52
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, 4609 eliminated, 3664 ate 79%, 945 abce 21%
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: 259352 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 89 gcs, 0 rescored clauses, 359 rescored vars
c dcps: 52 decompositions, 3303 equivalent 13%
c deco: 336 decision-only clauses 0%, 73% reduction
c decs: 4707950 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 18273749 push, 18247765 pop (18247765 dec 100%)
c dsch: 276237327 swaps, 0 down, 79515808 up
c elms: 12 elims, 19656 eliminated 75%, 74 pure 0%
c elms: 27 rounds, 2.2 rounds/bve
c elms: 19476 small 99%, 91 large 0%
c elms: 59903 tried small, 19476 succeeded 33%, 40427 failed 67%
c elms: 3796 subsumed, 530 strengthened, 19 blocked
c elms: 2031790 copies, 2867817 resolutions, 2533468 ipos
c elms: 312102 subchks, 181395 strchks
c gaus: 8 extractions, 156104 extracted, 3.2 size, 5 max
c gaus: exported 1 units, 9 binary and 48 ternary equations
c gaus: 5 gc, 17539908 steps, 8769954 extr 50%, 9815832 elim 56%
c glue: 11.3 orig avg, 11.3 real avg, 2.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 150994 = 95126 simple 63% + 50590 trn 34% + 5278 lrg 3%, 333 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 683554 clauses, 24.4 length
c lrnd: 16678939 lits = 22192294 orig - 5513355 removed 25%
c lrnd: 129411 uips 19%, 450588 flips 66%
c mins: 662019 mins 97%, 419 bin 0%, 20747 size 3%
c mins: 52842301 poisoned searches, 2566327 hits, 5% hit rate
c mins: 71453258 used twice searches, 4408479 hits, 6% hit rate
c move: moved 2249, 289 bin 13%, 1960 trn 87%
c otfs: 41260 driving 33%, 82191 restarting 67%
c otfs: str 123451, 123318 red 100%, 133 irr 0%
c otfs: str 123451, 0 bin 0%, 1430 trn 1%, 122021 lrg 99%
c otfs: sub 3654, 3637 red 100%, 17 irr 0%
c otfs: sub 3654, 0 bin 0%, 307 trn 8%, 3347 lrg 92%
c phas: 1 computed, 6280 set, 1007 pos (16%), 5273 neg (84%)
c prbs: 3 basic, 8744 probed, 0 failed, 0 lifted
c prbs: 4 simple, 78420 probed, 273 failed, 2730 eqs
c prbs: 4 treelook, 1795 probed, 2 failed, 0 lifted
c prom: 92061 locked 15% out of 629105 tried
c prps: 153827044 props, 31 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 16 count, 5455 quat, 2274 self1, 222 self2, 1694 dup
c redc: 12689 clauses 6%, 201440 tried 28%, 1 sat 0%
c redc: 17123 lits 1%, 1768005 tried 8%, 1 sat 0%
c redc: 414 times jump level reduced, 7.0 levels on average
c reds: 12 count, 59628.5 conflicts per reduce
c reds: 0 memlim 0%, 12 arith 100%
c reds: 333017 collected 84%, 63558 retired 16%
c rmbd: 2582 removed, 2564 red 99%
c rsts: 23383 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 18 count, 18 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 683554 count (444126 tried 0.6), 100809 sub out of 676695 (14.9%)
c swps: 17 count, 23 rounds, 2395 queries (104.1/round)
c swps: 2334 sat calls, 840 unsat (4.0% success rate)
c swps: 64826 decisions 27.8, 9272 conflicts 4.0
c swps; 53.9 avg class size, 109.2 avg environment size
c swps: 0 failed, 590 impls, 901 equivs
c swp0: 791 type 0 queries, 358 unsat (45.3%), 615 sat (77.7%)
c swp1: 1604 type 1 queries, 1469 unsat (91.6%), 879 sat (54.8%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 10784106 calls to obtain time
c tops: 2403 fixed 9%, 42 its, 17036.71 confs/it
c trds: 16 transitive reductions, 1201 removed, 2 failed
c trds: 57138 nodes, 59926 edges, 24679460 steps
c trim: 619408 words, 2.4 MB
c trnr: 16 count, 1008 bin, 4898 trn, 76910490 steps
c unhd: 5 count, 5 rounds, 2844027 steps
c unhd: 16 non-trivial sccs of average size 2.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 5678 tauts, 16 bin 0%, 695 trn 12%, 835 lrg 15%
c unhd: 5678 tauts, 4132 stamp 73%, 5676 red 100%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 36372 str, 0 bin 0%, 151 trn 0%, 36221 lrg 100%, 36261 red 100%
c vars: 894 remaining 3% and 25362 removed 97% out of 26256
c vars: 2403 fixed 9%, 19656 eliminated 75%, 3303 equivalent 13%
c vsts: 3149989397 visits, 96% srch, 4% simp, 0% lkhd
c vsts: 20.6 search visits per propagation, 4209.9 per conflict
c wchs: 743886973 pushed, 4852363 enlarged, 204 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         682150        333017         63558      18143394       3326405        400028
c 
c  0 0        101762  15      1671   1         0   0  12522060  69   1492063  45    156594  39     1.7
c  1 5         56573   8     21704   7      8707  14   2946367  16<   479293  14<    59580  15<    0.6
c  2 6        184641  27    102668  31     15159  24   2025461  11    797794  24    121690  30     1.7
c  3 9        199966  29<   118378  36<    14068  22<   477940   3    422318  13     55801  14     1.9
c  4 14        71982  11     46745  14      9513  15     97339   1     82729   2      5046   1     0.8
c  5 21        30231   4     19722   6      6287  10     34428   0     25547   1       658   0     0.9
c  6 30        16214   2     10200   3      3992   6     17610   0     12237   0       255   0     1.0
c  7 41        10116   1      6108   2      2593   4     10806   0      7346   0       167   0     1.5
c  8 54         6298   1      3593   1      1790   3      6645   0      4295   0       123   0     1.6
c  9 69         2941   0      1622   0       957   2      3125   0      1889   0        67   0     1.1
c 10 86         1008   0       483   0       341   1      1132   0       637   0        35   0     0.4
c 11 126         390   0       114   0       144   0       448   0       238   0        11   0     0.1
c 12 230          28   0         9   0         7   0        33   0        19   0         1   0     0.0
c 
c avg                  2.5           3.1           3.5           0.5           1.2           1.2
c std                  1.7           1.4           2.0           0.9           1.3           1.2
c 
c    9.135   8% cce
c    5.357   5% decide
c    3.818   3% sweep
c    3.198   3% elim
c    2.077   2% bump
c    1.987   2% probe
c    1.487   1% quatres
c    1.360   1% transred
c    0.969   1% gauss
c 
c    1.333 < 1% rest (below)
c 
c    0.451   0% ternres
c    0.362   0% unhide
c    0.256   0% block
c    0.148   0% bca
c    0.064   0% card
c    0.053   0% rescore
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.632   1% preprocessing     3%
c   23.808  22% inprocessing     97%
c ==================================
c   24.439  22% simplifying
c   86.260  78% search
c ==================================
c  110.700 100% all
c 
c        715542 conflicts,        6463.8 confs/sec
c          4575 ternaries,         156.4 confs/ternary
c           633 binaries,         1130.4 confs/binary
c            42 iterations,      17036.7 confs/iteration
c 
c            12 reductions,          0.1 redus/sec,  59628.5 confs/reduction
c         23383 restarts,          211.2 rests/sec,     30.6 confs/restart
c       4707950 decisions,       42529.0 decis/sec,      6.6 decis/conflict
c     153827044 propagations,  1389587.8 props/sec,     32.7 props/decision
c 
c 110.7 seconds, 34.6 MB
c launch: done
