c launch: /data/cnf/sc2014/app/6s17-opt.cnf.bz2
c host: atom07
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/6s17-opt.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/6s17-opt.cnf.bz2
c no embedded options
c found 'p cnf 47657 139163' header
c read 47657 variables, 139163 clauses, 324711 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=0
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 47271 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] STATIC (--score=0)
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   47271   137669         0       0      0     0    0     0    9   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 17 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 17 out of 17 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 37 at-most-one constraints, 26 used 70%
c [card-1] exported 37 binary clauses, 1.4 per/constraint
c [decomp-1] removed 748 variables
c [simpleprobe-1] all 46898 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 1214 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 1214 variables, found 1969 hbrs, 161 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 1 units, 1 failed, 18 tauts, 0 hbrs, 6 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 45647 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 33377 variables 73% in round 1 in 9763130 steps
c [elim-1-1] backward subsumption/strengthening limit 9763100
c [elim-1-1-1] backward checking 32926 touched variables 72%
c [elim-1-1-1] incomplete backward checking 32884 remain 100%
c [elim-1-1] subsumed 12 and strengthened 70 clauses in 9764708 steps
c [elim-1-1] rescheduled 181 variables 0% by backward subsumption
c [elim-1-2] eliminated 4 variables 0% in round 2 in 193712 steps
c [elim-1-2] backward subsumption/strengthening limit 193700
c [elim-1-2-1] backward checking 32889 touched variables 72%
c [elim-1-2-1] incomplete backward checking 32864 remain 100%
c [elim-1-2] subsumed 0 and strengthened 1 clauses in 193855 steps
c [elim-1-2] rescheduled 4 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 3281 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 33384 = 73% variables out of 45647 scheduled
c [phase-count-1] 60341 negative 90.0% of 67077 except 6736 10.0%
c [phase-count-1] 56202 positive 83.8% of 67077 except 10875 16.2%
c [phase-1] phase bias: 3109 positive 25%, 9154 negative 75%
c [sort-queue-1] sorted 12263 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 12263 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 35008 variables 74.1% (12263 remain 26%)
c [simplification-1] removed 70592 irredundant clauses 51.3% (67077 remain 49%)
c [simplification-1] maximum reduction of 74% = max (74%, 51%)
c [simplification-1] large reduction 74% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    1.6   12262    67076       726     552     94   113    1    58    7   1%      3   57    5    0 9289%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 36 variables
c [simpleprobe-2] all 12227 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 1 variables
c [simpleprobe-2] 4190 variables remain 34% (8036 retained 66%)
c [simpleprobe-2] removed 1 variables, found 474 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 24452 literals 100%
c [treelook-1] scheduling used 274958 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 315028 steps
c [treelook-1] 24292 literals remain 99%
c [treelook-1] 12224 variables remain to probed next time 100%
c [treelook-1] removed 2 variables, found 2207 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 6064 probes remain 50% after last round
c [basicprobe-1-0] removed 0 variables, found 3956 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 2 failed, 754 tauts, 0 hbrs, 1222 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 12222 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 2361 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 26 (8%) of length 16
c [cce-1-1] eliminated 2 clauses out of 35 (6%) of length 15
c [cce-1-1] eliminated 2 clauses out of 46 (4%) of length 14
c [cce-1-1] eliminated 3 clauses out of 71 (4%) of length 12
c [cce-1-1] eliminated 3 clauses out of 53 (6%) of length 11
c [cce-1-1] eliminated 16 clauses out of 168 (10%) of length 10
c [cce-1-1] eliminated 15 clauses out of 322 (5%) of length 9
c [cce-1-1] eliminated 41 clauses out of 631 (6%) of length 8
c [cce-1-1] eliminated 73 clauses out of 1223 (6%) of length 7
c [cce-1-1] eliminated 267 clauses out of 3074 (9%) of length 6
c [cce-1-1] eliminated 327 clauses out of 6109 (5%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 751 large clauses in 30000006 steps
c [cce-1-1] allowing another 15000003 steps for small clauses
c [cce-1-1] scheduling 21658 clauses = 13433 binary + 8225 ternary
c [cce-1-1] tried to eliminate 11847 small clauses 55%
c [cce-1-1] eliminated 132 binary clauses 1%
c [cce-1-1] eliminated 252 ternary clauses 3%
c [cce-1-1] eliminated 384 small clauses 2%
c [cce-1-1] eliminated 384 small clauses in 30000000 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1135 covered clauses in round 1
c [cce-1] eliminated 1135 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 12194 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 651 variables 5% in round 1 in 9730892 steps
c [elim-2-1] backward subsumption/strengthening limit 9730800
c [elim-2-1-1] backward checking 3879 touched variables 32%
c [elim-2-1-1] incomplete backward checking 3731 remain 96%
c [elim-2-1] subsumed 3 and strengthened 18 clauses in 9733964 steps
c [elim-2-1] rescheduled 50 variables 0% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 276662 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 652 = 5% variables out of 12194 scheduled
c [bca-1] limit of 10000000 steps and 125624 added (scaled 2)
c [bca-1] 20684 out of 23086 literals actually usable 90%
c [bca-1] added 812 blocked clauses in 55855 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 4832 pos 41.9% + 6710 neg 58.1% = 11542 sched 100.0% ret 0
c [sweep-1-1] 1000084 steps 127 queries 986.30 avg class size
c [sweep-1-1] 1996 decisions 121 SAT calls 30.28 avg env size
c [sweep-1-1] 9782 variables remain 85% (1760 retained 15%)
c [decomp-6] removed 46 variables
c [sweep-1-1] removed 46 vars (0 failed, 6 eqs, 6 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 46 vars in TOTAL (1 rounds, 126 queries)
c [sort-queue-2] sorted 11496 enqueued variables after 1000 conflicts
c [score-dist-2] active 0 (0%), one 0 (0%), zero 11496 (100%)
c [score-dist-2] max exp 0, different 1 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 766 variables 6.2% (11496 remain 24%)
c [simplification-2] removed 4578 irredundant clauses 6.8% (62498 remain 45%)
c [simplification-2] maximum reduction of 7% = max (6%, 7%)
c [simplification-2] large reduction 7% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3004 conflicts
c [quatres-1] found 13462 quaternary clauses 51% in total
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 38 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1073 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 11496 free variables schedulable
c [ternres-1] 6391 ternary resolvents (139 bin, 6252 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 299 at-most-one constraints of average size 3.9
c [card-2] found 51 at-most-two constraints of average size 4.1
c [card-2] using previous limit 1000000 for elimination
c [card-2] 350 out of 350 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 2 at-most-one constraints, 1 used 50%
c [card-2] exported 1 binary clauses, 1.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 5596 xors of average arity 3.1
c [gauss-1] connected 17134 occurrences of 1239 variables (average 13.8)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 11 ternary equations
c [decomp-7] removed 18 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 22956 literals 100%
c [treelook-2] scheduling used 298230 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 317407 steps
c [treelook-2] 22893 literals remain 100%
c [treelook-2] 11478 variables remain to probed next time 100%
c [decomp-8] removed 6 variables
c [treelook-2] removed 6 variables, found 511 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 2 units, 0 failed, 351 tauts, 0 hbrs, 1045 literals
c [transred-1] limit 130690 with penalty 0 = 0 + 0
c [transred-1] removed 36 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 11470 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 13 blocked clauses
c [block-2] 13 < 1/100 * 62325 = 623 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 2 clauses out of 52 (4%) of length 14
c [cce-2-1] eliminated 3 clauses out of 81 (4%) of length 12
c [cce-2-1] eliminated 3 clauses out of 80 (4%) of length 11
c [cce-2-1] eliminated 14 clauses out of 192 (7%) of length 10
c [cce-2-1] eliminated 3 clauses out of 326 (1%) of length 9
c [cce-2-1] eliminated 33 clauses out of 771 (4%) of length 8
c [cce-2-1] eliminated 66 clauses out of 1670 (4%) of length 7
c [cce-2-1] eliminated 94 clauses out of 2805 (3%) of length 6
c [cce-2-1] eliminated 2 clauses out of 6247 (0%) of length 5
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 220 large clauses in 30001156 steps
c [cce-2-1] allowing another 15000578 steps for small clauses
c [cce-2-1] scheduling 29084 clauses = 12384 binary + 16700 ternary
c [cce-2-1] tried to eliminate 12954 small clauses 45%
c [cce-2-1] eliminated 40 binary clauses 0%
c [cce-2-1] eliminated 341 ternary clauses 2%
c [cce-2-1] eliminated 381 small clauses 1%
c [cce-2-1] eliminated 381 small clauses in 30000002 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 601 covered clauses in round 1
c [cce-2] eliminated 601 covered clauses in TOTAL during 1 rounds
c [cce-2] 601 < 1/100 * 62306 = 623 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 11468 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 168 variables 1% in round 1 in 11747107 steps
c [elim-3-1] backward subsumption/strengthening limit 8252893
c [elim-3-1-1] backward checking 1254 touched variables 11%
c [elim-3-1-1] incomplete backward checking 1235 remain 98%
c [elim-3-1] subsumed 1 and strengthened 5 clauses in 8254233 steps
c [elim-3] incomplete 20 not tried 0% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 168 = 1% variables out of 11468 scheduled
c [bca-2] limit of 10000000 steps and 123870 added (scaled 2)
c [bca-2] 15830 out of 22602 literals actually usable 70%
c [bca-2] added 7 blocked clauses in 46000 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 4151 pos 43.4% + 5420 neg 56.6% = 9571 sched 84.7% ret 1729
c [sweep-2-1] 1000698 steps 140 queries 682.84 avg class size
c [sweep-2-1] 2311 decisions 138 SAT calls 31.21 avg env size
c [sweep-2-1] 8249 variables remain 73% (3049 retained 27%)
c [decomp-9] removed 35 variables
c [sweep-2-1] removed 35 vars (0 failed, 5 eqs, 5 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 35 vars in TOTAL (1 rounds, 139 queries)
c [sort-queue-3] sorted 11265 enqueued variables after 3004 conflicts
c [score-dist-3] active 0 (0%), one 0 (0%), zero 11265 (100%)
c [score-dist-3] max exp 0, different 1 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 231 variables 2.0% (11265 remain 24%)
c [simplification-3] removed 1092 irredundant clauses 1.7% (61406 remain 45%)
c [simplification-3] maximum reduction of 2% = max (2%, 2%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 6666
c [simplification-3] penalized conflict interval 6666 = 1 * 6666
c [simplification-3] hard conflict limit 19670 (soft 9670 + delta 10000)
c [simplification-3] new conflict limit 9670 (hard 19670)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    5.7   11264    61406      3601    3699   7551  8245    3   221    8   2%     30  214    7    0 2201%
c 
c [simplification-4] limit 9670 conflicts (hard 19670) hit after 9670 conflicts
c [quatres-2] found 15161 quaternary clauses 51% in total
c [quatres-2-1] added 2 double-self-subsuming ternary resolvents
c [quatres-2-2] added 34 single-self-subsuming ternary resolvents
c [quatres-2-2] added 573 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 11264 free variables schedulable
c [ternres-2] 739 ternary resolvents (73 bin, 666 trn)
c [ternres-2] 2 variables remain 0% (11262 retained 100%)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 5645 xors of average arity 3.1
c [gauss-2] connected 17231 occurrences of 1233 variables (average 14.0)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] connected 1547 occurrences of 1233 variables (average 1.3)
c [gauss-2] fully completed
c [decomp-10] removed 33 variables
c [gauss-2] exported 1 unary, 0 binary and 8 ternary equations
c [unhide-4] limit 101132 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 7 failed, 1232 tauts, 0 hbrs, 3461 literals
c [transred-2] limit 505660 with penalty 0 = 0 + 0
c [transred-2] removed 125 transitive binary clauses
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 11228 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 59 variables 1% in round 1 in 12462944 steps
c [elim-4-1] backward subsumption/strengthening limit 12462900
c [elim-4-1-1] backward checking 508 touched variables 5%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 5 and strengthened 26 clauses in 10517849 steps
c [elim-4-1] rescheduled 34 variables 0% by backward subsumption
c [elim-4-2] eliminated 3 variables 0% in round 2 in 416216 steps
c [elim-4-2] backward subsumption/strengthening limit 416200
c [elim-4-2-1] backward checking 13 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 2 and strengthened 11 clauses in 40129 steps
c [elim-4-2] rescheduled 13 variables 0% by backward subsumption
c [elim-4-3] eliminated 1 variables 0% in round 3 in 22998 steps
c [elim-4-3] backward subsumption/strengthening limit 22900
c [elim-4-3-1] backward checking 10 touched variables 0%
c [elim-4-3-1] incomplete backward checking 0 remain 0%
c [elim-4-3] subsumed 3 and strengthened 2 clauses in 22901 steps
c [elim-4] incomplete 7 not tried 0% in round 3
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 63 = 1% variables out of 11228 scheduled
c [elim-4] 63 < 1/100 * 11228 = 112 considered unsuccessful
c [bca-3] limit of 10000000 steps and 122999 added (scaled 2)
c [bca-3] 12093 out of 22332 literals actually usable 54%
c [bca-3] added 8 blocked clauses in 42036 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 3629 pos 44.5% + 4527 neg 55.5% = 8156 sched 73.0% ret 3009
c [sweep-3-1] 1007566 steps 117 queries 766.15 avg class size
c [sweep-3-1] 1859 decisions 109 SAT calls 31.83 avg env size
c [sweep-3-1] 7217 variables remain 65% (3948 retained 35%)
c [decomp-12] removed 36 variables
c [sweep-3-1] removed 36 vars (0 failed, 11 eqs, 17 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 36 vars in TOTAL (1 rounds, 116 queries)
c [sort-queue-4] sorted 11129 enqueued variables after 9670 conflicts
c [score-dist-4] active 0 (0%), one 0 (0%), zero 11129 (100%)
c [score-dist-4] max exp 0, different 1 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 135 variables 1.2% (11129 remain 24%)
c [simplification-4] removed 405 irredundant clauses 0.7% (61001 remain 44%)
c [simplification-4] maximum reduction of 1% = max (1%, 1%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 16666
c [simplification-4] penalized conflict interval 16666 = 1 * 16666
c [simplification-4] hard conflict limit 36336 (soft 26336 + delta 10000)
c [simplification-4] new conflict limit 26336 (hard 36336)
c 
c [simplification-5] limit 26336 conflicts (hard 36336) hit after 26336 conflicts
c [quatres-3] found 16555 quaternary clauses 49% in total
c [quatres-3-1] removed 4 duplicate quaternary clauses
c [quatres-3-1] added 4 double-self-subsuming ternary resolvents
c [quatres-3-2] added 24 single-self-subsuming ternary resolvents
c [quatres-3-2] added 270 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 2 schedulable variables 0%
c [ternres-3] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 5382 xors of average arity 3.1
c [gauss-3] connected 16524 occurrences of 1190 variables (average 13.9)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 8 variables
c [basicprobe-2] limit 4077723 penalty 1 = 1 + 0
c [basicprobe-2-0] 1075 probes remain 10% after last round
c [basicprobe-2-0] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 4 variables, found 8727 hbrs
c [bate-1] eliminated 38 asymmetric tautologies during probing
c [unhide-5] limit 326217 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 0 failed, 232 tauts, 0 hbrs, 7992 literals
c [transred-3] limit 1631089 with penalty 0 = 0 + 0
c [transred-3] removed 875 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 11117 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 4 blocked clauses
c [block-3] 4 < 1/100 * 60857 = 608 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 2 clauses out of 57 (4%) of length 14
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 2 large clauses in 15000001 steps
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3-1] scheduling 19635 clauses = 11978 binary + 7657 ternary
c [cce-3-1] tried to eliminate 1301 small clauses 7%
c [cce-3-1] eliminated 9 binary clauses 0%
c [cce-3-1] eliminated 10 ternary clauses 0%
c [cce-3-1] eliminated 19 small clauses 0%
c [cce-3-1] eliminated 19 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 21 covered clauses in round 1
c [cce-3] eliminated 21 covered clauses in TOTAL during 1 rounds
c [cce-3] 21 < 1/100 * 60853 = 608 considered unsuccessful
c [bca-4] limit of 10000000 steps and 122577 added (scaled 2)
c [bca-4] 9004 out of 22236 literals actually usable 40%
c [bca-4] added 31 blocked clauses in 48896 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 3313 pos 46.0% + 3886 neg 54.0% = 7199 sched 64.8% ret 3918
c [sweep-4-1] 1001434 steps 115 queries 567.95 avg class size
c [sweep-4-1] 1806 decisions 102 SAT calls 39.30 avg env size
c [sweep-4-1] 5962 variables remain 54% (5155 retained 46%)
c [decomp-14] removed 94 variables
c [sweep-4-1] removed 94 vars (0 failed, 14 eqs, 13 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 94 vars in TOTAL (1 rounds, 114 queries)
c [sort-queue-5] sorted 11023 enqueued variables after 26336 conflicts
c [score-dist-5] active 0 (0%), one 0 (0%), zero 11023 (100%)
c [score-dist-5] max exp 0, different 1 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 106 variables 1.0% (11023 remain 23%)
c [simplification-5] removed 176 irredundant clauses 0.3% (60824 remain 44%)
c [simplification-5] maximum reduction of 1% = max (1%, 0%)
c [simplification-5] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-5] new conflict interval 26666
c [simplification-5] penalized conflict interval 26666 = 1 * 26666
c [simplification-5] hard conflict limit 66335 (soft 53002 + delta 13333)
c [simplification-5] new conflict limit 53002 (hard 66335)
c 
c [simplification-6] limit 53002 conflicts (hard 66335) hit after 53003 conflicts
c [quatres-4] found 17804 quaternary clauses 46% in total
c [quatres-4-1] removed 4 duplicate quaternary clauses
c [quatres-4-1] added 2 double-self-subsuming ternary resolvents
c [quatres-4-2] added 36 single-self-subsuming ternary resolvents
c [quatres-4-2] added 153 quaternary resolvents
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 231 at-most-one constraints of average size 3.6
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 231 out of 231 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-15] removed 8 variables
c [simpleprobe-3] 3775 schedulable variables 34%
c [simpleprobe-3] limit 15219101 penalty 0 = 0 + 0
c [decomp-16] removed 48 variables
c [simpleprobe-3] 53 variables remain 0% (10914 retained 100%)
c [simpleprobe-3] removed 48 variables, found 2345 hbrs, 0 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 1151 transitive binary clauses
c [elim-5] no untried remaining variables left
c [elim-5] scheduled 10967 variables 100%
c [elim-5] limit of 38047752 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 66 variables 1% in round 1 in 12598225 steps
c [elim-5-1] backward subsumption/strengthening limit 12598200
c [elim-5-1-1] backward checking 526 touched variables 5%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 2 and strengthened 19 clauses in 8469166 steps
c [elim-5-1] rescheduled 80 variables 1% by backward subsumption
c [elim-5-2] eliminated 1 variables 0% in round 2 in 108762 steps
c [elim-5-2] backward subsumption/strengthening limit 108700
c [elim-5-2-1] backward checking 13 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 0 and strengthened 0 clauses in 30956 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 67 = 1% variables out of 10967 scheduled
c [elim-5] 67 < 1/100 * 10967 = 109 considered unsuccessful
c [bca-5] limit of 10000000 steps and 121267 added (scaled 2)
c [bca-5] 7315 out of 21802 literals actually usable 34%
c [bca-5] added 40 blocked clauses in 68167 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 11414320 penalty 0 = 0 + 0
c [sweep-5-1] 2647 pos 45.5% + 3175 neg 54.5% = 5822 sched 53.4% ret 5078
c [sweep-5-1] 10712027 steps 1018 queries 65.55 avg class size
c [sweep-5-1] 19282 decisions 971 SAT calls 44.64 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-17] removed 187 variables
c [sweep-5-1] removed 187 vars (0 failed, 180 eqs, 129 impls)
c [sweep-5-2] 4696 pos 43.8% + 6017 neg 56.2% = 10713 sched 100.0% ret 0
c [sweep-5-2] 714274 steps 55 queries 1467.98 avg class size
c [sweep-5-2] 1164 decisions 52 SAT calls 52.58 avg env size
c [sweep-5-2] 9806 variables remain 92% (907 retained 8%)
c [decomp-18] removed 5 variables
c [sweep-5-2] removed 5 vars (0 failed, 4 eqs, 3 impls)
c [sweep-5] removed 192 vars in TOTAL (2 rounds, 1071 queries)
c [sort-queue-6] sorted 10708 enqueued variables after 53003 conflicts
c [score-dist-6] active 0 (0%), one 0 (0%), zero 10708 (100%)
c [score-dist-6] max exp 0, different 1 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 315 variables 2.9% (10708 remain 23%)
c [simplification-6] removed 778 irredundant clauses 1.3% (60045 remain 44%)
c [simplification-6] maximum reduction of 3% = max (3%, 1%)
c [simplification-6] geometric conflict interval increment 6666 = 26666 / 4
c [simplification-6] new conflict interval 33332
c [simplification-6] penalized conflict interval 33332 = 1 * 33332
c [simplification-6] hard conflict limit 103001 (soft 86335 + delta 16666)
c [simplification-6] new conflict limit 86335 (hard 103001)
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   31.4   10707    60045     65384   61372   8565 16817   10   514   21   2%    618  212   10    6  175%
c i   32.9   10706    60045     68660   64518   8613 16820   10   530   21   2%   -255  218   10    6  174%
c -   33.9   10706    60044     70580   20580   8650 16820   10   541   17   2%   -293  222   10    6  177%
c 
c [simplification-7] limit 86335 conflicts (hard 103001) hit after 87772 conflicts
c [quatres-5] found 18983 quaternary clauses 43% in total
c [quatres-5-1] removed 8 duplicate quaternary clauses
c [quatres-5-1] added 5 double-self-subsuming ternary resolvents
c [quatres-5-2] added 44 single-self-subsuming ternary resolvents
c [quatres-5-2] added 180 quaternary resolvents
c [ternres-4] limit 3375805 with penalty 1 = 1 + 0
c [ternres-4] all 10706 free variables schedulable
c [ternres-4] 1740 ternary resolvents (78 bin, 1662 trn)
c [ternres-4] 18 variables remain 0% (10688 retained 100%)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] extracted 2458 xors of average arity 3.0
c [gauss-4] connected 7356 occurrences of 1027 variables (average 7.2)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-19] removed 6 variables
c [treelook-3] limit 675161 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 21400 literals 100%
c [treelook-3] scheduling used 403278 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 675161 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 786919 steps
c [treelook-3] 21387 literals remain 100%
c [treelook-3] 10700 variables remain to probed next time 100%
c [treelook-3] removed 0 variables, found 771 hbrs
c [unhide-6] limit 675161 with penalty 1 = 1 + 0
c [unhide-6-6] 1 units, 20 failed, 2003 tauts, 0 hbrs, 12889 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 461 transitive binary clauses
c [transred-5] found 3 units
c [bca-6] limit of 10000000 steps and 120533 added (scaled 2)
c [bca-6] 7793 out of 21382 literals actually usable 36%
c [bca-6] added 31 blocked clauses in 58079 steps
c [sweep-6] limit 2025483 penalty 0 = 0 + 0
c [sweep-6-1] 4301 pos 43.9% + 5489 neg 56.1% = 9790 sched 91.6% ret 900
c [sweep-6-1] 2033885 steps 143 queries 632.11 avg class size
c [sweep-6-1] 3724 decisions 139 SAT calls 53.01 avg env size
c [sweep-6-1] 6900 variables remain 65% (3789 retained 35%)
c [decomp-21] removed 13 variables
c [sweep-6-1] removed 13 vars (0 failed, 4 eqs, 4 impls)
c [sweep-6] removed 13 vars in TOTAL (1 rounds, 142 queries)
c [sort-queue-7] sorted 10677 enqueued variables after 87772 conflicts
c [score-dist-7] active 0 (0%), one 0 (0%), zero 10677 (100%)
c [score-dist-7] max exp 0, different 1 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 29 variables 0.3% (10677 remain 23%)
c [simplification-7] removed 266 irredundant clauses 0.4% (59777 remain 43%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 33332
c [simplification-7] new conflict interval 66664
c [simplification-7] penalized conflict interval 66664 = 1 * 66664
c [simplification-7] hard conflict limit 187768 (soft 154436 + delta 33332)
c [simplification-7] new conflict limit 154436 (hard 187768)
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   43.2   10676    59755     95633   44602  10428 15331   10   618   13   2%    116  234    9    7  129%
c i   43.7   10675    59753     96777   45622  10474 15336   10   679   13   1%   -149  290   10    7  141%
c i   46.4   10674    59751    103692   52280  10558 15341   10   532   14   2%   -174  123   11    8  142%
c -   56.8   10674    59747    128087   32326  10855 15369   10   458   13   2%    123   21   11    8  127%
c i   58.3   10673    59746    132260   36333  10909 15375   11   534   14   2%    178   94   11    9  122%
c 
c [simplification-8] limit 154436 conflicts (hard 187768) hit after 154436 conflicts
c [quatres-6] found 20797 quaternary clauses 39% in total
c [quatres-6-1] removed 2 duplicate quaternary clauses
c [quatres-6-1] added 9 double-self-subsuming ternary resolvents
c [quatres-6-2] added 90 single-self-subsuming ternary resolvents
c [quatres-6-2] added 185 quaternary resolvents
c [ternres-5] limit 13083093 with penalty 0 = 0 + 0
c [ternres-5] 18 schedulable variables 0%
c [ternres-5] 662 ternary resolvents (26 bin, 636 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-22] removed 14 variables
c [basicprobe-3] limit 65415469 penalty 0 = 0 + 0
c [basicprobe-3-0] 1247 sched 12%, 8 failed, 0 lifted, 1515 hbrs
c [decomp-23] removed 10 variables
c [basicprobe-3-1] 6278 sched 59%, 26 failed, 0 lifted, 2855 hbrs
c [decomp-24] removed 44 variables
c [basicprobe-3-2] 6169 sched 58%, 1 failed, 0 lifted, 109 hbrs
c [decomp-25] removed 2 variables
c [basicprobe-3-3] 6167 sched 58%, 0 failed, 0 lifted, 29 hbrs
c [basicprobe-3-4] 6167 sched 58%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-3-5] 6167 sched 58%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-3-6] 6167 sched 58%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-3-7] 6166 sched 58%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-3-8] 6166 sched 58%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-8] round limit 8 hit
c [basicprobe-3-8] 35 units = 35 failed (100%) + 0 lifted (0%)
c [basicprobe-3-8] removed 56 variables, found 4531 hbrs
c [bate-2] eliminated 42 asymmetric tautologies during probing
c [unhide-7] limit 2616618 with penalty 0 = 0 + 0
c [unhide-7-9] 0 units, 0 failed, 1569 tauts, 0 hbrs, 32343 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 401 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 10607 variables 100%
c [block-4] limit of 32707734 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 75 blocked clauses
c [block-4] 75 < 1/100 * 59451 = 594 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 163538672 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 3 clauses out of 198 (2%) of length 10
c [cce-4-1] eliminated 4 clauses out of 375 (1%) of length 9
c [cce-4-1] eliminated 8 clauses out of 656 (1%) of length 8
c [cce-4-1] eliminated 20 clauses out of 1471 (1%) of length 7
c [cce-4-1] eliminated 67 clauses out of 2741 (2%) of length 6
c [cce-4-1] eliminated 598 clauses out of 6164 (10%) of length 5
c [cce-4-1] eliminated 1217 clauses out of 12894 (9%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 1917 large clauses in 89005381 steps
c [cce-4-1] allowing another 44502690 steps for small clauses
c [cce-4-1] scheduling 26945 clauses = 11494 binary + 15451 ternary
c [cce-4-1] tried to eliminate 26945 small clauses 100%
c [cce-4-1] eliminated 192 binary clauses 2%
c [cce-4-1] eliminated 625 ternary clauses 4%
c [cce-4-1] eliminated 817 small clauses 3%
c [cce-4-1] eliminated 817 small clauses in 98378071 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 2734 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 32580345 steps for small clauses
c [cce-4-2] scheduling 26128 clauses = 11302 binary + 14826 ternary
c [cce-4-2] tried to eliminate 17324 small clauses 66%
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 2734 covered clauses in TOTAL during 2 rounds
c [bca-7] limit of 10000000 steps and 114248 added (scaled 2)
c [bca-7] 5079 out of 21212 literals actually usable 24%
c [bca-7] added 2 blocked clauses in 69402 steps
c [sweep-7] limit 3924928 penalty 0 = 0 + 0
c [sweep-7-1] 3217 pos 47.0% + 3626 neg 53.0% = 6843 sched 64.5% ret 3762
c [sweep-7-1] 3935600 steps 233 queries 325.58 avg class size
c [sweep-7-1] 5801 decisions 235 SAT calls 57.50 avg env size
c [sweep-7-1] 3790 variables remain 36% (6814 retained 64%)
c [decomp-31] removed 41 variables
c [sweep-7-1] removed 41 vars (0 failed, 22 eqs, 12 impls)
c [sweep-7] removed 41 vars in TOTAL (1 rounds, 232 queries)
c [sort-queue-8] sorted 10564 enqueued variables after 154436 conflicts
c [score-dist-8] active 0 (0%), one 0 (0%), zero 10564 (100%)
c [score-dist-8] max exp 0, different 1 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 109 variables 1.0% (10564 remain 22%)
c [simplification-8] removed 3125 irredundant clauses 5.2% (56614 remain 41%)
c [simplification-8] maximum reduction of 5% = max (1%, 5%)
c [simplification-8] large reduction 5% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 166436 (soft 156436 + delta 10000)
c [simplification-8] new conflict limit 156436 (hard 166436)
c 
c [simplification-9] limit 156436 conflicts (hard 166436) hit after 156436 conflicts
c [quatres-7] found 19733 quaternary clauses 39% in total
c [quatres-7-1] removed 8 duplicate quaternary clauses
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 43 single-self-subsuming ternary resolvents
c [quatres-7-2] added 122 quaternary resolvents
c [ternres-6] limit 13245373 with penalty 0 = 0 + 0
c [ternres-6] all 10564 free variables schedulable
c [ternres-6] 1726 ternary resolvents (107 bin, 1619 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-32] removed 4 variables
c [simpleprobe-4] 51 schedulable variables 0%
c [simpleprobe-4] limit 52981494 penalty 0 = 0 + 0
c [decomp-33] removed 7 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 7 variables, found 685 hbrs, 3 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 334 transitive binary clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 10553 variables 100%
c [elim-6] limit of 66226868 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 444 variables 4% in round 1 in 12182020 steps
c [elim-6-1] backward subsumption/strengthening limit 12182000
c [elim-6-1-1] backward checking 2227 touched variables 21%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 10 and strengthened 45 clauses in 3047543 steps
c [elim-6-1] rescheduled 118 variables 1% by backward subsumption
c [elim-6-2] eliminated 8 variables 0% in round 2 in 501461 steps
c [elim-6-2] backward subsumption/strengthening limit 501400
c [elim-6-2-1] backward checking 51 touched variables 0%
c [elim-6-2-1] incomplete backward checking 48 remain 94%
c [elim-6-2] subsumed 3 and strengthened 0 clauses in 503213 steps
c [elim-6-2] rescheduled 8 variables 0% by backward subsumption
c [elim-6-3] no variable eliminated in round 3 in 8694 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 452 = 4% variables out of 10553 scheduled
c [bca-8] limit of 10000000 steps and 112553 added (scaled 2)
c [bca-8] 4690 out of 20204 literals actually usable 23%
c [bca-8] added 7 blocked clauses in 66846 steps
c [sweep-8] limit 3973612 penalty 0 = 0 + 0
c [sweep-8-1] 1710 pos 47.8% + 1868 neg 52.2% = 3578 sched 35.4% ret 6523
c [sweep-8-1] 3980260 steps 297 queries 95.76 avg class size
c [sweep-8-1] 6234 decisions 299 SAT calls 45.06 avg env size
c [sweep-8-1] 1521 variables remain 15% (8580 retained 85%)
c [decomp-34] removed 34 variables
c [sweep-8-1] removed 34 vars (0 failed, 31 eqs, 23 impls)
c [sweep-8] removed 34 vars in TOTAL (1 rounds, 296 queries)
c [sort-queue-9] sorted 10067 enqueued variables after 156436 conflicts
c [score-dist-9] active 0 (0%), one 0 (0%), zero 10067 (100%)
c [score-dist-9] max exp 0, different 1 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 497 variables 4.7% (10067 remain 21%)
c [simplification-9] removed 850 irredundant clauses 1.5% (55762 remain 41%)
c [simplification-9] maximum reduction of 5% = max (5%, 2%)
c [simplification-9] large reduction 5% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 168436 (soft 158436 + delta 10000)
c [simplification-9] new conflict limit 158436 (hard 168436)
c 
c [simplification-10] limit 158436 conflicts (hard 168436) hit after 158436 conflicts
c [quatres-8] found 19653 quaternary clauses 39% in total
c [quatres-8-1] removed 8 duplicate quaternary clauses
c [quatres-8-1] added 2 double-self-subsuming ternary resolvents
c [quatres-8-2] added 67 single-self-subsuming ternary resolvents
c [quatres-8-2] added 208 quaternary resolvents
c [ternres-7] limit 13390039 with penalty 0 = 0 + 0
c [ternres-7] all 10067 free variables schedulable
c [ternres-7] 983 ternary resolvents (85 bin, 898 trn)
c [ternres-7] fully completed ternary resolution
c [card-4] limit 836877 penalty 3 = 3 + 0
c [card-4] found 379 at-most-one constraints of average size 3.3
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 836877 for elimination
c [card-4] 379 out of 379 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-5] limit 669501 penalty 2 = 2 + 0
c [gauss-5] extracted 1502 xors of average arity 3.0
c [gauss-5] connected 4502 occurrences of 912 variables (average 4.9)
c [gauss-5] limit 669501 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-35] removed 3 variables
c [unhide-8] limit 1339003 with penalty 1 = 1 + 0
c [unhide-8-11] 0 units, 29 failed, 1364 tauts, 0 hbrs, 6498 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 284 transitive binary clauses
c [transred-8] found 1 units
c [cce-5] limit of 33475099 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 4 clauses out of 197 (2%) of length 10
c [cce-5-1] eliminated 3 clauses out of 393 (1%) of length 9
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 7 large clauses in 33475100 steps
c [cce-5-1] allowing another 16737550 steps for small clauses
c [cce-5-1] scheduling 18009 clauses = 10652 binary + 7357 ternary
c [cce-5-1] tried to eliminate 3360 small clauses 19%
c [cce-5-1] eliminated 26 binary clauses 0%
c [cce-5-1] eliminated 43 ternary clauses 1%
c [cce-5-1] eliminated 69 small clauses 0%
c [cce-5-1] eliminated 72 small clauses in 33475100 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 79 covered clauses in round 1
c [cce-5] eliminated 79 covered clauses in TOTAL during 1 rounds
c [cce-5] 79 < 1/100 * 55675 = 556 considered unsuccessful
c [bca-9] limit of 10000000 steps and 112161 added (scaled 2)
c [bca-9] 4514 out of 20116 literals actually usable 22%
c [bca-9] added 9 blocked clauses in 68531 steps
c [sweep-9] limit 4017011 penalty 0 = 0 + 0
c [sweep-9-1] 657 pos 43.2% + 863 neg 56.8% = 1520 sched 15.1% ret 8537
c [sweep-9-1] 4023716 steps 270 queries 82.50 avg class size
c [sweep-9-1] 5930 decisions 254 SAT calls 53.15 avg env size
c [sweep-9-1] 618 variables remain 6% (9437 retained 94%)
c [decomp-36] removed 60 variables
c [sweep-9-1] removed 60 vars (0 failed, 46 eqs, 33 impls)
c [sweep-9] removed 60 vars in TOTAL (1 rounds, 269 queries)
c [sort-queue-10] sorted 9997 enqueued variables after 158436 conflicts
c [score-dist-10] active 0 (0%), one 0 (0%), zero 9997 (100%)
c [score-dist-10] max exp 0, different 1 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 70 variables 0.7% (9997 remain 21%)
c [simplification-10] removed 257 irredundant clauses 0.5% (55505 remain 40%)
c [simplification-10] maximum reduction of 1% = max (1%, 0%)
c [simplification-10] geometric conflict interval increment 33332 = 66664 / 2
c [simplification-10] new conflict interval 99996
c [simplification-10] penalized conflict interval 99996 = 1 * 99996
c [simplification-10] hard conflict limit 308430 (soft 258432 + delta 49998)
c [simplification-10] new conflict limit 258432 (hard 308430)
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.3    9997    55496    183898   37528  12198 14878   12   572   12   2%    433   94   11   10  114%
c i   90.0    9996    55496    186885   40421  12222 14879   12   538   14   2%    459   56   12   10  115%
c i   90.4    9995    55493    188445   41926  12236 14880   12   550   14   2%   -185   67   11   10  113%
c i   95.3    9994    55487    205289   58136  12392 14899   12   618   15   2%    -76  120   14   10  135%
c i  100.8    9993    55484    221984   74328  12508 14913   12   570   18   2%    -36   56   11   11   98%
c i  102.9    9992    55483    228832   80947  12551 14915   12   556   25   2%   -169   37   12   11  112%
c -  106.1    9992    55482    237207   45659  12599 14919   13   613   13   2%   -122   90   13   11  118%
c 
c [simplification-11] limit 258432 conflicts (hard 308430) hit after 258432 conflicts
c [quatres-9] found 21583 quaternary clauses 35% in total
c [quatres-9-1] removed 4 duplicate quaternary clauses
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 81 single-self-subsuming ternary resolvents
c [quatres-9-2] added 173 quaternary resolvents
c [ternres-8] limit 21514962 with penalty 0 = 0 + 0
c [ternres-8] all 9992 free variables schedulable
c [ternres-8] 1592 ternary resolvents (104 bin, 1488 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-37] removed 17 variables
c [treelook-4] limit 1075748 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 19960 literals 100%
c [treelook-4] scheduling used 468307 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1075748 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 1077042 steps
c [treelook-4] 19809 literals remain 99%
c [treelook-4] 9968 variables remain to probed next time 100%
c [decomp-38] removed 4 variables
c [treelook-4] removed 16 variables, found 2463 hbrs
c [unhide-9] limit 4302992 with penalty 0 = 0 + 0
c [unhide-9-15] 0 units, 8 failed, 1930 tauts, 0 hbrs, 41679 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 106 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 9961 variables 100%
c [elim-7] limit of 215149620 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 117 variables 1% in round 1 in 20149871 steps
c [elim-7-1] backward subsumption/strengthening limit 20149800
c [elim-7-1-1] backward checking 754 touched variables 8%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 1 and strengthened 7 clauses in 1869372 steps
c [elim-7-1] rescheduled 16 variables 0% by backward subsumption
c [elim-7-2] eliminated 2 variables 0% in round 2 in 121842 steps
c [elim-7-2] backward subsumption/strengthening limit 121800
c [elim-7-2-1] backward checking 14 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 5 clauses in 36784 steps
c [elim-7-2] rescheduled 13 variables 0% by backward subsumption
c [elim-7-3] eliminated 1 variables 0% in round 3 in 45406 steps
c [elim-7-3] backward subsumption/strengthening limit 45400
c [elim-7-3-1] backward checking 12 touched variables 0%
c [elim-7-3-1] fully completed backward checking in 1 rounds
c [elim-7-3] subsumed 0 and strengthened 0 clauses in 32788 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 120 = 1% variables out of 9961 scheduled
c [bca-10] limit of 10000000 steps and 110689 added (scaled 2)
c [bca-10] 3121 out of 19684 literals actually usable 16%
c [bca-10] added 4 blocked clauses in 72611 steps
c [sweep-10] limit 6454488 penalty 0 = 0 + 0
c [sweep-10-1] 260 pos 44.0% + 331 neg 56.0% = 591 sched 6.0% ret 9250
c [sweep-10-1] 3209852 steps 301 queries 23.11 avg class size
c [sweep-10-1] 5997 decisions 280 SAT calls 41.80 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-39] removed 46 variables
c [sweep-10-1] removed 46 vars (0 failed, 39 eqs, 35 impls)
c [sweep-10-2] 4341 pos 44.3% + 5454 neg 55.7% = 9795 sched 100.0% ret 0
c [sweep-10-2] 3246934 steps 191 queries 343.23 avg class size
c [sweep-10-2] 5025 decisions 197 SAT calls 63.45 avg env size
c [sweep-10-2] 5456 variables remain 56% (4338 retained 44%)
c [decomp-40] removed 19 variables
c [sweep-10-2] removed 19 vars (0 failed, 15 eqs, 7 impls)
c [sweep-10] removed 65 vars in TOTAL (2 rounds, 490 queries)
c [sort-queue-11] sorted 9776 enqueued variables after 258432 conflicts
c [score-dist-11] active 0 (0%), one 0 (0%), zero 9776 (100%)
c [score-dist-11] max exp 0, different 1 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 216 variables 2.2% (9776 remain 21%)
c [simplification-11] removed 674 irredundant clauses 1.2% (54807 remain 40%)
c [simplification-11] maximum reduction of 2% = max (2%, 1%)
c [simplification-11] geometric conflict interval increment 33332 = 99996 / 3
c [simplification-11] new conflict interval 133328
c [simplification-11] penalized conflict interval 133328 = 1 * 133328
c [simplification-11] hard conflict limit 458424 (soft 391760 + delta 66664)
c [simplification-11] new conflict limit 391760 (hard 458424)
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 -  122.3    9776    54805    287505   51764  12995 15088   13   448   14   3%    492  -65   14   12  117%
c i  127.3    9775    54805    307193   71030  13072 15090   14   522   18   3%    630   23   14   12  110%
c -  135.5    9775    54805    334701   57232  13160 15098   14   555   14   3%    -52   56   15   13  114%
c -  147.1    9775    54804    380877   62613  13319 15113   15   422   20   4%    492  -55   15   14  111%
c 
c [simplification-12] limit 391760 conflicts (hard 458424) hit after 391761 conflicts
c [quatres-10] found 22931 quaternary clauses 33% in total
c [quatres-10-1] removed 13 duplicate quaternary clauses
c [quatres-10-1] added 4 double-self-subsuming ternary resolvents
c [quatres-10-2] added 107 single-self-subsuming ternary resolvents
c [quatres-10-2] added 226 quaternary resolvents
c [ternres-9] limit 31285563 with penalty 0 = 0 + 0
c [ternres-9] all 9775 free variables schedulable
c [ternres-9] 1851 ternary resolvents (123 bin, 1728 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-41] removed 11 variables
c [basicprobe-4] limit 156427819 penalty 0 = 0 + 0
c [basicprobe-4-0] 5707 sched 59%, 16 failed, 0 lifted, 1485 hbrs
c [decomp-42] removed 26 variables
c [basicprobe-4-1] 5674 sched 58%, 0 failed, 0 lifted, 96 hbrs
c [decomp-43] removed 1 variables
c [basicprobe-4-2] 5675 sched 58%, 0 failed, 0 lifted, 22 hbrs
c [basicprobe-4-3] 5674 sched 58%, 0 failed, 0 lifted, 10 hbrs
c [basicprobe-4-4] 5673 sched 58%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-4-5] 5673 sched 58%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-4-6] 5673 sched 58%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-6] fully completed probing
c [basicprobe-4-6] 16 units = 16 failed (100%) + 0 lifted (0%)
c [basicprobe-4-6] removed 27 variables, found 1618 hbrs
c [bate-3] eliminated 16 asymmetric tautologies during probing
c [unhide-10] limit 6257112 with penalty 0 = 0 + 0
c [unhide-10-20] 0 units, 0 failed, 1682 tauts, 0 hbrs, 36183 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 162 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 9738 variables 100%
c [block-5] limit of 39106954 steps penalty 3 = 3 + 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 * 54632 = 546 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 9736 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 12514225580 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 44 variables 0% in round 1 in 19818070 steps
c [elim-8-1] backward subsumption/strengthening limit 19818000
c [elim-8-1-1] backward checking 426 touched variables 4%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 1712659 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 44 = 0% variables out of 9736 scheduled
c [elim-8] 44 < 1/100 * 9736 = 97 considered unsuccessful
c [bca-11] limit of 10000000 steps and 109755 added (scaled 2)
c [bca-11] 2925 out of 19386 literals actually usable 15%
c [bca-11] added 6 blocked clauses in 78409 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 93856690 penalty 0 = 0 + 0
c [sweep-11-1] 2491 pos 46.1% + 2910 neg 53.9% = 5401 sched 55.7% ret 4291
c [sweep-11-1] 16377437 steps 839 queries 34.14 avg class size
c [sweep-11-1] 17887 decisions 796 SAT calls 54.83 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-48] removed 123 variables
c [sweep-11-1] removed 123 vars (0 failed, 127 eqs, 106 impls)
c [sweep-11-2] 4275 pos 44.7% + 5294 neg 55.3% = 9569 sched 100.0% ret 0
c [sweep-11-2] 16553923 steps 892 queries 59.64 avg class size
c [sweep-11-2] 19232 decisions 866 SAT calls 55.34 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-49] removed 94 variables
c [sweep-11-2] removed 94 vars (0 failed, 113 eqs, 80 impls)
c [sweep-11-3] 4234 pos 44.7% + 5241 neg 55.3% = 9475 sched 100.0% ret 0
c [sweep-11-3] 14949407 steps 894 queries 60.73 avg class size
c [sweep-11-3] 18388 decisions 861 SAT calls 54.02 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-50] removed 81 variables
c [sweep-11-3] removed 81 vars (0 failed, 100 eqs, 82 impls)
c [sweep-11] removed 298 vars in TOTAL (3 rounds, 2622 queries)
c [sort-queue-12] sorted 9394 enqueued variables after 391761 conflicts
c [score-dist-12] active 0 (0%), one 0 (0%), zero 9394 (100%)
c [score-dist-12] max exp 0, different 1 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 381 variables 3.9% (9394 remain 20%)
c [simplification-12] removed 668 irredundant clauses 1.2% (54136 remain 39%)
c [simplification-12] maximum reduction of 4% = max (4%, 1%)
c [simplification-12] geometric conflict interval increment 26665 = 133328 / 5
c [simplification-12] new conflict interval 159993
c [simplification-12] penalized conflict interval 159993 = 1 * 159993
c [simplification-12] hard conflict limit 631750 (soft 551754 + delta 79996)
c [simplification-12] new conflict limit 551754 (hard 631750)
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  155.6    9393    54129    395201   76808  12700 15402   15   649   17   2%    596  153   16   14  113%
c i  157.1    9392    54126    402415   83712  12742 15404   14   547   19   3%   -609   36   14   14  101%
c i  160.6    9391    54122    417383   98327  12792 15407   15   506   28   3%   -368   -6   16   14  113%
c i  161.1    9390    54122    419781  100672  12800 15409   15   541   29   3%   -524   28   14   14   99%
c -  162.8    9390    54122    425360   66947  12822 15410   15   510   15   3%   -453   -3   17   14  118%
c -  173.4    9390    54122    468515   70133  12932 15417   15   381   24   4%    259 -111   17   15  114%
c i  179.7    9389    54121    495418   96463  12997 15422   15   405   27   4%    517  -66   15   15  100%
c -  184.1    9389    54121    512022   72347  13032 15423   14   404   15   4%   -302  -59   13   15   90%
c 
c [simplification-13] limit 551754 conflicts (hard 631750) hit after 551755 conflicts
c [quatres-11] found 24362 quaternary clauses 31% in total
c [quatres-11-1] removed 74 duplicate quaternary clauses
c [quatres-11-1] added 6 double-self-subsuming ternary resolvents
c [quatres-11-2] added 119 single-self-subsuming ternary resolvents
c [quatres-11-2] added 334 quaternary resolvents
c [ternres-10] limit 42763273 with penalty 0 = 0 + 0
c [ternres-10] all 9389 free variables schedulable
c [ternres-10] 3174 ternary resolvents (173 bin, 3001 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-51] removed 23 variables
c [simpleprobe-5] all 9371 free variables schedulable
c [simpleprobe-5] limit 171053092 penalty 0 = 0 + 0
c [decomp-52] removed 49 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 49 variables, found 2269 hbrs, 21 units
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1009 transitive binary clauses
c [cce-6] limit of 53454091 steps penalty 2 = 2 + 0
c [cce-6-1] eliminated 2 clauses out of 10 (20%) of length 16
c [cce-6-1] eliminated 1 clauses out of 86 (1%) of length 11
c [cce-6-1] eliminated 8 clauses out of 212 (4%) of length 10
c [cce-6-1] eliminated 20 clauses out of 411 (5%) of length 9
c [cce-6-1] eliminated 11 clauses out of 593 (2%) of length 8
c [cce-6-1] eliminated 22 clauses out of 1400 (2%) of length 7
c [cce-6-1] eliminated 223 clauses out of 2818 (8%) of length 6
c [cce-6-1] eliminated 471 clauses out of 5635 (8%) of length 5
c [cce-6-1] eliminated 327 clauses out of 11587 (3%) of length 4
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 1085 large clauses in 53454093 steps
c [cce-6-1] allowing another 26727046 steps for small clauses
c [cce-6-1] scheduling 23319 clauses = 10121 binary + 13198 ternary
c [cce-6-1] tried to eliminate 19249 small clauses 83%
c [cce-6-1] eliminated 147 binary clauses 1%
c [cce-6-1] eliminated 391 ternary clauses 3%
c [cce-6-1] eliminated 538 small clauses 2%
c [cce-6-1] eliminated 538 small clauses in 53454091 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 1623 covered clauses in round 1
c [cce-6] eliminated 1623 covered clauses in TOTAL during 1 rounds
c [bca-12] limit of 10000000 steps and 105028 added (scaled 2)
c [bca-12] 2108 out of 18646 literals actually usable 11%
c [bca-12] added 3 blocked clauses in 115997 steps
c [sweep-12] limit 12828981 penalty 0 = 0 + 0
c [sweep-12-1] 4162 pos 44.6% + 5160 neg 55.4% = 9322 sched 100.0% ret 0
c [sweep-12-1] 12832046 steps 498 queries 83.69 avg class size
c [sweep-12-1] 17633 decisions 492 SAT calls 92.67 avg env size
c [sweep-12-1] 997 variables remain 11% (8324 retained 89%)
c [decomp-53] removed 33 variables
c [sweep-12-1] removed 33 vars (0 failed, 36 eqs, 29 impls)
c [sweep-12] removed 33 vars in TOTAL (1 rounds, 497 queries)
c [sort-queue-13] sorted 9289 enqueued variables after 551755 conflicts
c [score-dist-13] active 0 (0%), one 0 (0%), zero 9289 (100%)
c [score-dist-13] max exp 0, different 1 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 100 variables 1.1% (9289 remain 20%)
c [simplification-13] removed 2132 irredundant clauses 3.9% (51984 remain 38%)
c [simplification-13] maximum reduction of 4% = max (1%, 4%)
c [simplification-13] geometric conflict interval increment 31998 = 159993 / 5
c [simplification-13] new conflict interval 191991
c [simplification-13] penalized conflict interval 191991 = 1 * 191991
c [simplification-13] hard conflict limit 839741 (soft 743746 + delta 95995)
c [simplification-13] new conflict limit 743746 (hard 839741)
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 -  197.2    9289    51983    555993   75391  15623 16436   16   640   15   3%    346  139   17   15  112%
c -  207.9    9289    51981    600529   77193  15734 16444   16   360   24   4%    681 -109   17   15  108%
c i  216.3    9288    51981    634212  110019  15802 16446   14   395   22   4%    819  -79   14   15   90%
c -  219.4    9288    51981    646912   79600  15839 16447   15   628   24   2%   -960  144   17   15  111%
c -  230.9    9288    51981    694087   82627  15954 16451   14   348   16   4%     58 -117   15   15  100%
c i  235.7    9287    51981    714062  102155  15986 16454   15   389   22   4%    312  -66   15   15  101%
c -  243.6    9287    51981    741599   85371  16050 16459   14   342   16   4%   -276  -85   16   15  108%
c i  243.8    9286    51981    742258   86011  16053 16460   14   388   19   4%   -263  -38   14   15   93%
c 
c [simplification-14] limit 743746 conflicts (hard 839741) hit after 776816 conflicts
c [quatres-12] found 25468 quaternary clauses 29% in total
c [quatres-12-1] removed 28 duplicate quaternary clauses
c [quatres-12-1] added 10 double-self-subsuming ternary resolvents
c [quatres-12-2] added 97 single-self-subsuming ternary resolvents
c [quatres-12-2] added 244 quaternary resolvents
c [ternres-11] limit 59962116 with penalty 0 = 0 + 0
c [ternres-11] all 9286 free variables schedulable
c [ternres-11] 1611 ternary resolvents (122 bin, 1489 trn)
c [ternres-11] fully completed ternary resolution
c [gauss-6] limit 1499052 penalty 3 = 3 + 0
c [gauss-6] extracted 2754 xors of average arity 3.0
c [gauss-6] connected 8228 occurrences of 870 variables (average 9.5)
c [gauss-6] limit 1499052 penalty 3 = 3 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-54] removed 10 variables
c [treelook-5] limit 5996211 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 18552 literals 100%
c [treelook-5] scheduling used 606708 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 5996211 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 5996369 steps
c [treelook-5] 16583 literals remain 90%
c [treelook-5] 9251 variables remain to probed next time 100%
c [decomp-55] removed 7 variables
c [treelook-5] removed 20 variables, found 8524 hbrs
c [unhide-11] limit 5996211 with penalty 1 = 1 + 0
c [unhide-11-23] 0 units, 3 failed, 3694 tauts, 0 hbrs, 80610 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 674 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 9255 variables 100%
c [elim-9] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 242 variables 3% in round 1 in 17438734 steps
c [elim-9-1] backward subsumption/strengthening limit 17438700
c [elim-9-1-1] backward checking 1257 touched variables 14%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 7 and strengthened 9 clauses in 1881128 steps
c [elim-9-1] rescheduled 33 variables 0% by backward subsumption
c [elim-9-2] eliminated 1 variables 0% in round 2 in 33894 steps
c [elim-9-2] backward subsumption/strengthening limit 33800
c [elim-9-2-1] backward checking 7 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 30403 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 243 = 3% variables out of 9255 scheduled
c [bca-13] limit of 10000000 steps and 102340 added (scaled 2)
c [bca-13] 2032 out of 18026 literals actually usable 11%
c [bca-13] added 10 blocked clauses in 118914 steps
c [sweep-13] limit 17988634 penalty 0 = 0 + 0
c [sweep-13-1] 382 pos 40.5% + 562 neg 59.5% = 944 sched 10.5% ret 8068
c [sweep-13-1] 7986666 steps 345 queries 22.66 avg class size
c [sweep-13-1] 7912 decisions 330 SAT calls 59.75 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-56] removed 34 variables
c [sweep-13-1] removed 34 vars (0 failed, 34 eqs, 29 impls)
c [sweep-13-2] 3843 pos 42.8% + 5135 neg 57.2% = 8978 sched 100.0% ret 0
c [sweep-13-2] 10011147 steps 326 queries 123.36 avg class size
c [sweep-13-2] 10459 decisions 326 SAT calls 76.28 avg env size
c [sweep-13-2] 1959 variables remain 22% (7019 retained 78%)
c [decomp-57] removed 13 variables
c [sweep-13-2] removed 13 vars (0 failed, 13 eqs, 11 impls)
c [sweep-13] removed 47 vars in TOTAL (2 rounds, 669 queries)
c [sort-queue-14] sorted 8965 enqueued variables after 776816 conflicts
c [score-dist-14] active 0 (0%), one 0 (0%), zero 8965 (100%)
c [score-dist-14] max exp 0, different 1 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 321 variables 3.5% (8965 remain 19%)
c [simplification-14] removed 1333 irredundant clauses 2.6% (50647 remain 37%)
c [simplification-14] maximum reduction of 3% = max (3%, 3%)
c [simplification-14] geometric conflict interval increment 47997 = 191991 / 4
c [simplification-14] new conflict interval 239988
c [simplification-14] penalized conflict interval 239988 = 1 * 239988
c [simplification-14] hard conflict limit 1136798 (soft 1016804 + delta 119994)
c [simplification-14] new conflict limit 1016804 (hard 1136798)
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 -  258.2    8965    50646    792557   87379  15477 18552   15   440   16   3%    219  -30   16   15  112%
c i  259.5    8964    50646    798228   92771  15493 18552   14   436   28   3%    285  -36   12   15   83%
c -  268.6    8964    50644    841007   90885  15593 18558   12   350   17   3%    177 -178   11   15   73%
c -  279.1    8964    50644    890335   95264  15734 18563   16   578   17   3%    625  117   17   15  117%
c -  289.4    8964    50643    938860   97624  15836 18570   14   355   18   4%    834 -196   13   15   85%
c -  299.4    8964    50643    987234  103054  15881 18573   14   527   18   3%    933  104   16   14  115%
c 
c [simplification-15] limit 1016804 conflicts (hard 1136798) hit after 1016804 conflicts
c [quatres-13] found 26494 quaternary clauses 27% in total
c [quatres-13-1] removed 20 duplicate quaternary clauses
c [quatres-13-1] added 8 double-self-subsuming ternary resolvents
c [quatres-13-2] added 108 single-self-subsuming ternary resolvents
c [quatres-13-2] added 280 quaternary resolvents
c [ternres-12] limit 77302823 with penalty 0 = 0 + 0
c [ternres-12] all 8964 free variables schedulable
c [ternres-12] 2921 ternary resolvents (194 bin, 2727 trn)
c [ternres-12] fully completed ternary resolution
c [card-5] limit 2415713 penalty 4 = 4 + 0
c [card-5] found 448 at-most-one constraints of average size 3.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2415713 for elimination
c [card-5] 448 out of 448 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-58] removed 18 variables
c [basicprobe-5] limit 386514115 penalty 0 = 0 + 0
c [basicprobe-5-0] 5203 sched 58%, 9 failed, 0 lifted, 1889 hbrs
c [decomp-59] removed 15 variables
c [basicprobe-5-1] 5143 sched 58%, 0 failed, 0 lifted, 91 hbrs
c [basicprobe-5-2] 5145 sched 58%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-5-3] 5145 sched 58%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-5-4] 5145 sched 58%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-5-5] 5145 sched 58%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-5] fully completed probing
c [basicprobe-5-5] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-5-5] removed 15 variables, found 1999 hbrs
c [bate-4] eliminated 16 asymmetric tautologies during probing
c [unhide-12] limit 15460564 with penalty 0 = 0 + 0
c [unhide-12-31] 0 units, 0 failed, 3761 tauts, 0 hbrs, 160440 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 145 transitive binary clauses
c [cce-7] limit of 193257057 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 4 clauses out of 195 (2%) of length 10
c [cce-7-1] eliminated 6 clauses out of 383 (2%) of length 9
c [cce-7-1] eliminated 12 clauses out of 559 (2%) of length 8
c [cce-7-1] eliminated 42 clauses out of 1374 (3%) of length 7
c [cce-7-1] eliminated 82 clauses out of 2624 (3%) of length 6
c [cce-7-1] eliminated 220 clauses out of 5133 (4%) of length 5
c [cce-7-1] eliminated 820 clauses out of 11111 (7%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 1186 large clauses in 154421885 steps
c [cce-7-1] allowing another 77210942 steps for small clauses
c [cce-7-1] scheduling 16752 clauses = 9593 binary + 7159 ternary
c [cce-7-1] tried to eliminate 16752 small clauses 100%
c [cce-7-1] eliminated 222 binary clauses 2%
c [cce-7-1] eliminated 455 ternary clauses 6%
c [cce-7-1] eliminated 677 small clauses 4%
c [cce-7-1] eliminated 677 small clauses in 125593564 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 1863 covered clauses in round 1
c [cce-7-2] eliminated 2 clauses out of 377 (1%) of length 9
c [cce-7-2] eliminated 5 clauses out of 547 (1%) of length 8
c [cce-7-2] eliminated 3 clauses out of 1332 (0%) of length 7
c [cce-7-2] eliminated 4 clauses out of 2542 (0%) of length 6
c [cce-7-2] incomplete large round (ACCE)
c [cce-7-2] eliminated 14 large clauses in 67663494 steps
c [cce-7-2] allowing another 33831747 steps for small clauses
c [cce-7-2] scheduling 16075 clauses = 9371 binary + 6704 ternary
c [cce-7-2] tried to eliminate 9478 small clauses 59%
c [cce-7-2] eliminated 4 binary clauses 0%
c [cce-7-2] eliminated 9 ternary clauses 0%
c [cce-7-2] eliminated 13 small clauses 0%
c [cce-7-2] eliminated 13 small clauses in 67663494 steps
c [cce-7-2] incomplete small round (ACCE)
c [cce-7-2] eliminated 27 covered clauses in round 2
c [cce-7] eliminated 1890 covered clauses in TOTAL during 2 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 8932 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 259 variables 3% in round 1 in 15840818 steps
c [elim-10-1] backward subsumption/strengthening limit 15840800
c [elim-10-1-1] backward checking 1233 touched variables 14%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 4 and strengthened 9 clauses in 4751525 steps
c [elim-10-1] rescheduled 35 variables 0% by backward subsumption
c [elim-10-2] eliminated 7 variables 0% in round 2 in 5562196 steps
c [elim-10-2] backward subsumption/strengthening limit 5562100
c [elim-10-2-1] backward checking 28 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 1 and strengthened 0 clauses in 1219900 steps
c [elim-10-2] rescheduled 6 variables 0% by backward subsumption
c [elim-10-3] eliminated 4 variables 0% in round 3 in 1431 steps
c [elim-10-3] backward subsumption/strengthening limit 1400
c [elim-10-3-1] backward checking 16 touched variables 0%
c [elim-10-3-1] incomplete backward checking 5 remain 31%
c [elim-10-3] subsumed 0 and strengthened 0 clauses in 1841 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 270 = 3% variables out of 8932 scheduled
c [bca-14] limit of 10000000 steps and 97195 added (scaled 2)
c [bca-14] 1405 out of 17326 literals actually usable 8%
c [bca-14] added 11 blocked clauses in 127860 steps
c [sweep-14] limit 23190846 penalty 0 = 0 + 0
c [sweep-14-1] 896 pos 48.2% + 963 neg 51.8% = 1859 sched 21.5% ret 6803
c [sweep-14-1] 9907474 steps 474 queries 25.28 avg class size
c [sweep-14-1] 14854 decisions 462 SAT calls 81.13 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-64] removed 38 variables
c [sweep-14-1] removed 38 vars (0 failed, 40 eqs, 31 impls)
c [sweep-14-2] 3811 pos 44.2% + 4813 neg 55.8% = 8624 sched 100.0% ret 0
c [sweep-14-2] 13287449 steps 480 queries 76.48 avg class size
c [sweep-14-2] 15262 decisions 457 SAT calls 84.97 avg env size
c [sweep-14-2] 612 variables remain 7% (8012 retained 93%)
c [decomp-65] removed 41 variables
c [sweep-14-2] removed 41 vars (0 failed, 47 eqs, 50 impls)
c [sweep-14] removed 79 vars in TOTAL (2 rounds, 952 queries)
c [sort-queue-15] sorted 8583 enqueued variables after 1016804 conflicts
c [score-dist-15] active 0 (0%), one 0 (0%), zero 8583 (100%)
c [score-dist-15] max exp 0, different 1 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 381 variables 4.3% (8583 remain 18%)
c [simplification-15] removed 2557 irredundant clauses 5.0% (48086 remain 35%)
c [simplification-15] maximum reduction of 5% = max (4%, 5%)
c [simplification-15] large reduction 5% >= 5% limit
c [simplification-15] next conflict interval 10168 = min (1016804/100, 239988)
c [simplification-15] penalized conflict interval 10168 = 1 * 10168
c [simplification-15] hard conflict limit 1036972 (soft 1026972 + delta 10000)
c [simplification-15] new conflict limit 1026972 (hard 1036972)
c 
c [simplification-16] limit 1026972 conflicts (hard 1036972) hit after 1028334 conflicts
c [quatres-14] found 25253 quaternary clauses 26% in total
c [quatres-14-1] removed 40 duplicate quaternary clauses
c [quatres-14-1] added 5 double-self-subsuming ternary resolvents
c [quatres-14-2] added 66 single-self-subsuming ternary resolvents
c [quatres-14-2] added 195 quaternary resolvents
c [ternres-13] limit 78146464 with penalty 0 = 0 + 0
c [ternres-13] all 8583 free variables schedulable
c [ternres-13] 1574 ternary resolvents (134 bin, 1440 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-66] removed 9 variables
c [simpleprobe-6] all 8574 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-67] removed 12 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 12 variables, found 2326 hbrs, 6 units
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 1000 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 3907323200 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 97 (1%) of length 13
c [cce-8-1] eliminated 1 clauses out of 41 (2%) of length 12
c [cce-8-1] eliminated 1 clauses out of 87 (1%) of length 11
c [cce-8-1] eliminated 3 clauses out of 194 (2%) of length 10
c [cce-8-1] eliminated 10 clauses out of 392 (3%) of length 9
c [cce-8-1] eliminated 12 clauses out of 578 (2%) of length 8
c [cce-8-1] eliminated 19 clauses out of 1369 (1%) of length 7
c [cce-8-1] eliminated 65 clauses out of 2611 (2%) of length 6
c [cce-8-1] eliminated 104 clauses out of 5013 (2%) of length 5
c [cce-8-1] eliminated 163 clauses out of 10225 (2%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 379 large clauses in 58419647 steps
c [cce-8-1] allowing another 29209823 steps for small clauses
c [cce-8-1] scheduling 15616 clauses = 9014 binary + 6602 ternary
c [cce-8-1] tried to eliminate 15616 small clauses 100%
c [cce-8-1] eliminated 29 binary clauses 0%
c [cce-8-1] eliminated 52 ternary clauses 1%
c [cce-8-1] eliminated 81 small clauses 1%
c [cce-8-1] eliminated 81 small clauses in 54743770 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 460 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 28543696 steps for small clauses
c [cce-8-2] scheduling 15536 clauses = 8985 binary + 6551 ternary
c [cce-8-2] tried to eliminate 15536 small clauses 100%
c [cce-8-2] eliminated 1 ternary clauses 0%
c [cce-8-2] eliminated 1 small clauses 0%
c [cce-8-2] eliminated 1 small clauses in 53886969 steps
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 1 covered clauses in round 2
c [cce-8-3] completed large round (ATE)
c [cce-8-3] allowing another 28543709 steps for small clauses
c [cce-8-3] scheduling 15535 clauses = 8985 binary + 6550 ternary
c [cce-8-3] tried to eliminate 15535 small clauses 100%
c [cce-8-3] completed small round (ATE)
c [cce-8-3] eliminated 0 covered clauses in round 3
c [cce-8] eliminated 461 covered clauses in TOTAL during 3 rounds
c [cce-8] 461 < 1/100 * 47977 = 479 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 8562 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 68 variables 1% in round 1 in 15294407 steps
c [elim-11-1] backward subsumption/strengthening limit 15294400
c [elim-11-1-1] backward checking 489 touched variables 6%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 0 and strengthened 1 clauses in 1342914 steps
c [elim-11-1] rescheduled 4 variables 0% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 3990 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 68 = 1% variables out of 8562 scheduled
c [elim-11] 68 < 1/100 * 8562 = 85 considered unsuccessful
c [bca-15] limit of 10000000 steps and 95588 added (scaled 2)
c [bca-15] 1263 out of 16990 literals actually usable 7%
c [bca-15] added 5 blocked clauses in 138188 steps
c [sweep-15] limit 23443939 penalty 0 = 0 + 0
c [sweep-15-1] 237 pos 39.8% + 359 neg 60.2% = 596 sched 7.0% ret 7898
c [sweep-15-1] 6038319 steps 247 queries 17.21 avg class size
c [sweep-15-1] 7021 decisions 219 SAT calls 75.07 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-68] removed 35 variables
c [sweep-15-1] removed 35 vars (0 failed, 37 eqs, 46 impls)
c [sweep-15-2] 3753 pos 44.4% + 4706 neg 55.6% = 8459 sched 100.0% ret 0
c [sweep-15-2] 17479378 steps 565 queries 92.20 avg class size
c [sweep-15-2] 20704 decisions 547 SAT calls 99.59 avg env size
c [sweep-15-2] 244 variables remain 3% (8215 retained 97%)
c [decomp-69] removed 41 variables
c [sweep-15-2] removed 41 vars (0 failed, 45 eqs, 44 impls)
c [sweep-15] removed 76 vars in TOTAL (2 rounds, 810 queries)
c [sort-queue-16] sorted 8418 enqueued variables after 1028334 conflicts
c [score-dist-16] active 0 (0%), one 0 (0%), zero 8418 (100%)
c [score-dist-16] max exp 0, different 1 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 165 variables 1.9% (8418 remain 18%)
c [simplification-16] removed 826 irredundant clauses 1.7% (47260 remain 34%)
c [simplification-16] maximum reduction of 2% = max (2%, 2%)
c [simplification-16] geometric conflict interval increment 79996 = 239988 / 3
c [simplification-16] new conflict interval 319984
c [simplification-16] penalized conflict interval 319984 = 1 * 319984
c [simplification-16] hard conflict limit 1508310 (soft 1348318 + delta 159992)
c [simplification-16] new conflict limit 1348318 (hard 1508310)
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 -  337.9    8418    47259   1036919   99477  16688 15915   14   361   19   4%    981  -94   13   14   91%
c i  342.9    8417    47256   1059544  121398  16769 15917   15   614   36   2%    994  194   17   14  117%
c -  349.2    8417    47254   1087981  101971  16843 15920   16   640   19   2%  -1683  188   17   15  115%
c -  360.4    8417    47254   1139699  104912  16948 15923   16   627   20   3%   -206  103   16   15  107%
c -  370.7    8417    47254   1191911  108984  17018 15928   16   536   28   3%    470   86   17   15  114%
c i  376.0    8416    47250   1218951  135298  17074 15930   15   570   28   3%    657   97   12   15   80%
c -  381.8    8416    47250   1243340  110725  17117 15931   16   734   20   2%   -973  216   16   15  106%
c -  393.5    8416    47250   1296025  113340  17197 15933   16   590   20   3%    130   49   15   16   95%
c i  394.3    8415    47250   1300122  117282  17207 15936   15   592   25   3%    184   47   18   16  115%
c 
c [simplification-17] limit 1348318 conflicts (hard 1508310) hit after 1348318 conflicts
c [quatres-15] found 26479 quaternary clauses 24% in total
c [quatres-15-1] removed 14 duplicate quaternary clauses
c [quatres-15-1] added 2 double-self-subsuming ternary resolvents
c [quatres-15-2] added 64 single-self-subsuming ternary resolvents
c [quatres-15-2] added 208 quaternary resolvents
c [ternres-14] limit 101672518 with penalty 0 = 0 + 0
c [ternres-14] all 8415 free variables schedulable
c [ternres-14] 1000 ternary resolvents (95 bin, 905 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-70] removed 13 variables
c [treelook-6] limit 10167251 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 16804 literals 100%
c [treelook-6] scheduling used 704639 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 10167251 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 10167287 steps
c [treelook-6] 8621 literals remain 51%
c [treelook-6] 6805 variables remain to probed next time 81%
c [decomp-71] removed 3 variables
c [treelook-6] removed 7 variables, found 4025 hbrs
c [unhide-13] limit 10000000 with penalty 1 = 1 + 0
c [unhide-13-35] 0 units, 0 failed, 3023 tauts, 0 hbrs, 176529 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 550 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 8398 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 26 blocked clauses
c [block-6] 26 < 1/100 * 47148 = 471 considered unsuccessful
c [bca-16] limit of 10000000 steps and 95237 added (scaled 2)
c [bca-16] 1113 out of 16798 literals actually usable 7%
c [bca-16] added 1 blocked clauses in 165928 steps
c [sweep-16] limit 30501755 penalty 0 = 0 + 0
c [sweep-16-1] 101 pos 42.4% + 137 neg 57.6% = 238 sched 2.8% ret 8160
c [sweep-16-1] 4354920 steps 123 queries 10.76 avg class size
c [sweep-16-1] 3371 decisions 118 SAT calls 69.80 avg env size
c [sweep-16-1] fully completed sweeping round
c [decomp-72] removed 8 variables
c [sweep-16-1] removed 8 vars (0 failed, 7 eqs, 9 impls)
c [sweep-16-2] 3668 pos 43.7% + 4722 neg 56.3% = 8390 sched 100.0% ret 0
c [sweep-16-2] 21912785 steps 670 queries 69.00 avg class size
c [sweep-16-2] 24843 decisions 662 SAT calls 94.76 avg env size
c [sweep-16-2] fully completed sweeping round
c [decomp-73] removed 33 variables
c [sweep-16-2] removed 33 vars (0 failed, 37 eqs, 31 impls)
c [sweep-16-3] 3651 pos 43.7% + 4706 neg 56.3% = 8357 sched 100.0% ret 0
c [sweep-16-3] 4320872 steps 88 queries 383.28 avg class size
c [sweep-16-3] 5508 decisions 87 SAT calls 141.07 avg env size
c [sweep-16-3] 5183 variables remain 62% (3174 retained 38%)
c [sweep-16-3] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-16] removed 41 vars in TOTAL (3 rounds, 878 queries)
c [sort-queue-17] sorted 8357 enqueued variables after 1348318 conflicts
c [score-dist-17] active 0 (0%), one 0 (0%), zero 8357 (100%)
c [score-dist-17] max exp 0, different 1 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 58 variables 0.7% (8357 remain 18%)
c [simplification-17] removed 161 irredundant clauses 0.3% (47089 remain 34%)
c [simplification-17] maximum reduction of 1% = max (1%, 0%)
c [simplification-17] geometric conflict interval increment 159992 = 319984 / 2
c [simplification-17] new conflict interval 479976
c [simplification-17] penalized conflict interval 479976 = 1 * 479976
c [simplification-17] hard conflict limit 2068282 (soft 1828294 + delta 239988)
c [simplification-17] new conflict limit 1828294 (hard 2068282)
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 -  408.8    8357    47089   1348318  115796  16658 16536   17   614   15   3%      4   50   15   16   92%
c -  419.8    8357    47089   1402511  119635  16729 16537   13   388   22   3%    578 -175   11   16   68%
c -  431.3    8357    47089   1455800  123726  16786 16538   15   517   33   3%    826  121   17   15  115%
c i  431.8    8356    47089   1457779  125640  16792 16540   16   575   37   3%    832  175   18   15  117%
c -  444.5    8356    47089   1508699  123231  16887 16547   14   522   22   3%   -215  111   17   15  116%
c -  459.7    8356    47089   1565057  125629  16965 16548   16   607   31   3%    500  136   18   15  115%
c -  473.5    8356    47088   1622376  129509  17043 16550   17   618   32   3%    805   92   18   16  115%
c -  489.1    8356    47088   1678792  132037  17092 16553   17   594   22   3%    932  118   16   16  103%
c -  503.6    8356    47087   1735378  132840  17156 16554   16   547   23   3%    985   29   18   16  110%
c -  518.2    8356    47087   1793883  136482  17218 16557   16   512   23   3%   1008  -27   16   16   98%
c 
c [simplification-18] limit 1828294 conflicts (hard 2068282) hit after 1832705 conflicts
c [quatres-16] found 28533 quaternary clauses 22% in total
c [quatres-16-1] removed 24 duplicate quaternary clauses
c [quatres-16-1] added 3 double-self-subsuming ternary resolvents
c [quatres-16-2] added 116 single-self-subsuming ternary resolvents
c [quatres-16-2] added 211 quaternary resolvents
c [ternres-15] limit 144008249 with penalty 0 = 0 + 0
c [ternres-15] all 8356 free variables schedulable
c [ternres-15] 3000 ternary resolvents (114 bin, 2886 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-75] removed 2 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 4821 sched 58%, 5 failed, 0 lifted, 732 hbrs
c [decomp-76] removed 9 variables
c [basicprobe-6-1] 4819 sched 58%, 0 failed, 0 lifted, 301 hbrs
c [basicprobe-6-2] 4816 sched 58%, 0 failed, 0 lifted, 27 hbrs
c [basicprobe-6-3] 4816 sched 58%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-6-4] 4816 sched 58%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-6-5] 4816 sched 58%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-6-6] 4816 sched 58%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-6] fully completed probing
c [basicprobe-6-6] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-6-6] removed 9 variables, found 1063 hbrs
c [bate-5] eliminated 8 asymmetric tautologies during probing
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 679 transitive binary clauses
c [cce-9] limit of 360020623 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 4 clauses out of 181 (2%) of length 10
c [cce-9-1] eliminated 12 clauses out of 384 (3%) of length 9
c [cce-9-1] eliminated 10 clauses out of 572 (2%) of length 8
c [cce-9-1] eliminated 37 clauses out of 1343 (3%) of length 7
c [cce-9-1] eliminated 75 clauses out of 2577 (3%) of length 6
c [cce-9-1] eliminated 204 clauses out of 4913 (4%) of length 5
c [cce-9-1] eliminated 266 clauses out of 9965 (3%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 608 large clauses in 138067320 steps
c [cce-9-1] allowing another 69033660 steps for small clauses
c [cce-9-1] scheduling 15337 clauses = 8823 binary + 6514 ternary
c [cce-9-1] tried to eliminate 15337 small clauses 100%
c [cce-9-1] eliminated 120 binary clauses 1%
c [cce-9-1] eliminated 128 ternary clauses 2%
c [cce-9-1] eliminated 248 small clauses 2%
c [cce-9-1] eliminated 248 small clauses in 110632346 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 856 covered clauses in round 1
c [cce-9-2] eliminated 1 clauses out of 372 (0%) of length 9
c [cce-9-2] eliminated 1 clauses out of 562 (0%) of length 8
c [cce-9-2] eliminated 2 clauses out of 1306 (0%) of length 7
c [cce-9-2] eliminated 2 clauses out of 2502 (0%) of length 6
c [cce-9-2] eliminated 9 clauses out of 4709 (0%) of length 5
c [cce-9-2] eliminated 14 clauses out of 9699 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 29 large clauses in 131201623 steps
c [cce-9-2] allowing another 65600811 steps for small clauses
c [cce-9-2] scheduling 15091 clauses = 8703 binary + 6388 ternary
c [cce-9-2] tried to eliminate 15091 small clauses 100%
c [cce-9-2] eliminated 5 binary clauses 0%
c [cce-9-2] eliminated 5 ternary clauses 0%
c [cce-9-2] eliminated 10 small clauses 0%
c [cce-9-2] eliminated 10 small clauses in 106288412 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 39 covered clauses in round 2
c [cce-9-3] eliminated 1 clauses out of 4700 (0%) of length 5
c [cce-9-3] eliminated 1 clauses out of 9685 (0%) of length 4
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] eliminated 2 large clauses in 129821226 steps
c [cce-9-3] allowing another 64910613 steps for small clauses
c [cce-9-3] scheduling 15081 clauses = 8698 binary + 6383 ternary
c [cce-9-3] tried to eliminate 15081 small clauses 100%
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 2 covered clauses in round 3
c [cce-9] eliminated 897 covered clauses in TOTAL during 3 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 8346 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 177 variables 2% in round 1 in 14523986 steps
c [elim-12-1] backward subsumption/strengthening limit 14523900
c [elim-12-1-1] backward checking 853 touched variables 10%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 1 and strengthened 1 clauses in 2499605 steps
c [elim-12-1] rescheduled 11 variables 0% by backward subsumption
c [elim-12-2] no variable eliminated in round 2 in 4536005 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 177 = 2% variables out of 8346 scheduled
c [bca-17] limit of 10000000 steps and 92483 added (scaled 2)
c [bca-17] 955 out of 16340 literals actually usable 6%
c [bca-17] added 6 blocked clauses in 171242 steps
c [sweep-17] limit 43202474 penalty 0 = 0 + 0
c [sweep-17-1] 2302 pos 45.3% + 2775 neg 54.7% = 5077 sched 62.1% ret 3092
c [sweep-17-1] 20438970 steps 595 queries 36.43 avg class size
c [sweep-17-1] 20840 decisions 580 SAT calls 94.52 avg env size
c [sweep-17-1] fully completed sweeping round
c [decomp-82] removed 55 variables
c [sweep-17-1] removed 55 vars (0 failed, 57 eqs, 49 impls)
c [sweep-17-2] 3569 pos 44.0% + 4545 neg 56.0% = 8114 sched 100.0% ret 0
c [sweep-17-2] 22771086 steps 618 queries 29.81 avg class size
c [sweep-17-2] 23455 decisions 598 SAT calls 102.82 avg env size
c [sweep-17-2] 52 variables remain 1% (8058 retained 99%)
c [decomp-83] removed 57 variables
c [sweep-17-2] removed 57 vars (0 failed, 51 eqs, 48 impls)
c [sweep-17] removed 112 vars in TOTAL (2 rounds, 1211 queries)
c [sort-queue-18] sorted 8057 enqueued variables after 1832705 conflicts
c [score-dist-18] active 0 (0%), one 0 (0%), zero 8057 (100%)
c [score-dist-18] max exp 0, different 1 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 299 variables 3.6% (8057 remain 17%)
c [simplification-18] removed 1497 irredundant clauses 3.2% (45590 remain 33%)
c [simplification-18] maximum reduction of 4% = max (4%, 3%)
c [simplification-18] geometric conflict interval increment 95995 = 479976 / 5
c [simplification-18] new conflict interval 575971
c [simplification-18] penalized conflict interval 575971 = 1 * 575971
c [simplification-18] hard conflict limit 2696661 (soft 2408676 + delta 287985)
c [simplification-18] new conflict limit 2408676 (hard 2696661)
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 -  563.7    8057    45583   1853013  135408  18006 14753   16   354   33   4%   1018 -134   16   16  101%
c i  563.9    8056    45583   1853888  136264  18007 14753   16   379   38   4%   1018 -107   17   16  112%
c -  579.6    8056    45578   1913344  139285  18085 14757   16   443   23   4%  -1516  -17   17   16  107%
c -  596.1    8056    45576   1973538  142598  18137 14759   15   396   23   4%     10   21   15   15   98%
c i  597.5    8055    45576   1979433  148360  18138 14759   16   542   29   3%     97  156   18   15  114%
c -  611.5    8055    45576   2034781  145500  18259 14763   13   465   24   3%   -231   46   12   15   83%
c -  627.8    8055    45575   2096303  147835  18329 14766   16   517   24   3%    533   19   15   15  101%
c -  642.8    8055    45570   2159640  152971  18397 14771   14   299   36   5%    837 -142   14   15   98%
c -  658.4    8055    45570   2220999  155885  18474 14774   15   514   25   3%    951  135   16   14  115%
c -  678.0    8055    45568   2282719  156076  18561 14777   14   659   25   2%    995  242   13   14   87%
c -  696.7    8055    45568   2347721  159459  18640 14782   15   512   25   3%   1013   92   13   15   92%
c i  714.2    8054    45567   2407412  217733  18711 14786   15   453   40   3%   1020   10   12   15   78%
c -  716.2    8054    45567   2412878  162601  18718 14786   16   574   26   3%  -5197  126   16   15  105%
c -  736.5    8054    45567   2481138  167274  18823 14792   14   506   37   3%  -1183  153   18   14  126%
c 
c [simplification-19] limit 2408676 conflicts (hard 2696661) hit after 2531461 conflicts
c [quatres-17] found 30229 quaternary clauses 20% in total
c [quatres-17-1] removed 44 duplicate quaternary clauses
c [quatres-17-1] added 2 double-self-subsuming ternary resolvents
c [quatres-17-2] added 104 single-self-subsuming ternary resolvents
c [quatres-17-2] added 381 quaternary resolvents
c [ternres-16] limit 200000000 with penalty 0 = 0 + 0
c [ternres-16] all 8054 free variables schedulable
c [ternres-16] 2544 ternary resolvents (78 bin, 2466 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-7] limit 2679841 penalty 4 = 4 + 0
c [gauss-7] extracted 3698 xors of average arity 3.1
c [gauss-7] connected 11298 occurrences of 748 variables (average 15.1)
c [gauss-7] limit 2679841 penalty 4 = 4 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-84] removed 5 variables
c [simpleprobe-7] all 8049 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-85] removed 8 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 8 variables, found 1855 hbrs, 2 units
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 961 transitive binary clauses
c [cce-10] limit of 1071936764 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 2 clauses out of 41 (5%) of length 12
c [cce-10-1] eliminated 7 clauses out of 106 (7%) of length 11
c [cce-10-1] eliminated 11 clauses out of 196 (6%) of length 10
c [cce-10-1] eliminated 10 clauses out of 381 (3%) of length 9
c [cce-10-1] eliminated 18 clauses out of 579 (3%) of length 8
c [cce-10-1] eliminated 37 clauses out of 1340 (3%) of length 7
c [cce-10-1] eliminated 65 clauses out of 2524 (3%) of length 6
c [cce-10-1] eliminated 96 clauses out of 4716 (2%) of length 5
c [cce-10-1] eliminated 127 clauses out of 9572 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 373 large clauses in 50317177 steps
c [cce-10-1] allowing another 25158588 steps for small clauses
c [cce-10-1] scheduling 14777 clauses = 8477 binary + 6300 ternary
c [cce-10-1] tried to eliminate 14777 small clauses 100%
c [cce-10-1] eliminated 21 binary clauses 0%
c [cce-10-1] eliminated 59 ternary clauses 1%
c [cce-10-1] eliminated 80 small clauses 1%
c [cce-10-1] eliminated 80 small clauses in 47896387 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 453 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 24535057 steps for small clauses
c [cce-10-2] scheduling 14698 clauses = 8456 binary + 6242 ternary
c [cce-10-2] tried to eliminate 14698 small clauses 100%
c [cce-10-2] eliminated 1 ternary clauses 0%
c [cce-10-2] eliminated 1 small clauses 0%
c [cce-10-2] eliminated 1 small clauses in 47107481 steps
c [cce-10-2] completed small round (ATE)
c [cce-10-2] eliminated 1 covered clauses in round 2
c [cce-10-3] completed large round (ATE)
c [cce-10-3] allowing another 24536110 steps for small clauses
c [cce-10-3] scheduling 14697 clauses = 8456 binary + 6241 ternary
c [cce-10-3] tried to eliminate 14697 small clauses 100%
c [cce-10-3] completed small round (ATE)
c [cce-10-3] eliminated 0 covered clauses in round 3
c [cce-10] eliminated 454 covered clauses in TOTAL during 3 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 8041 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 93 variables 1% in round 1 in 13868064 steps
c [elim-13-1] backward subsumption/strengthening limit 13868000
c [elim-13-1-1] backward checking 592 touched variables 7%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 6 clauses in 1303443 steps
c [elim-13-1] rescheduled 24 variables 0% by backward subsumption
c [elim-13-2] eliminated 1 variables 0% in round 2 in 45209 steps
c [elim-13-2] backward subsumption/strengthening limit 45200
c [elim-13-2-1] backward checking 19 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 0 and strengthened 0 clauses in 26543 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 94 = 1% variables out of 8041 scheduled
c [bca-18] limit of 10000000 steps and 90222 added (scaled 2)
c [bca-18] 556 out of 15896 literals actually usable 3%
c [bca-18] added 1 blocked clauses in 206208 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 20 pos 41.7% + 28 neg 58.3% = 48 sched 0.6% ret 7899
c [sweep-18-1] 1056920 steps 33 queries 6.85 avg class size
c [sweep-18-1] 937 decisions 33 SAT calls 77.97 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-86] removed 1 variables
c [sweep-18-1] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-18-2] 3462 pos 43.6% + 4484 neg 56.4% = 7946 sched 100.0% ret 0
c [sweep-18-2] 28832987 steps 588 queries 42.44 avg class size
c [sweep-18-2] 25507 decisions 577 SAT calls 122.83 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-87] removed 37 variables
c [sweep-18-2] removed 37 vars (0 failed, 37 eqs, 29 impls)
c [sweep-18-3] 3449 pos 43.6% + 4460 neg 56.4% = 7909 sched 100.0% ret 0
c [sweep-18-3] 30733843 steps 579 queries 35.44 avg class size
c [sweep-18-3] 26576 decisions 585 SAT calls 125.90 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-88] removed 9 variables
c [sweep-18-3] removed 9 vars (0 failed, 11 eqs, 7 impls)
c [sweep-18] removed 47 vars in TOTAL (3 rounds, 1197 queries)
c [sort-queue-19] sorted 7900 enqueued variables after 2531461 conflicts
c [score-dist-19] active 0 (0%), one 0 (0%), zero 7900 (100%)
c [score-dist-19] max exp 0, different 1 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 154 variables 1.9% (7900 remain 17%)
c [simplification-19] removed 997 irredundant clauses 2.2% (44570 remain 32%)
c [simplification-19] maximum reduction of 2% = max (2%, 2%)
c [simplification-19] geometric conflict interval increment 191990 = 575971 / 3
c [simplification-19] new conflict interval 767961
c [simplification-19] penalized conflict interval 767961 = 1 * 767961
c [simplification-19] hard conflict limit 3683402 (soft 3299422 + delta 383980)
c [simplification-19] new conflict limit 3299422 (hard 3683402)
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 -  764.9    7900    44570   2553380  167644  20161 14572   14   441   25   3%    291   45   12   14   85%
c -  783.1    7900    44568   2619703  171729  20224 14575   14   472   26   3%    758   95   17   14  118%
c i  794.1    7899    44568   2663160  214126  20283 14577   15   533   49   3%    887  112   14   14  100%
c -  801.2    7899    44568   2685875  173846  20312 14580   14   341   27   4%  -1943  -88   10   14   73%
c -  820.7    7899    44567   2753443  176986  20364 14580   16   514   27   3%    -34   48   16   15  107%
c -  843.2    7899    44567   2820909  178988  20417 14582   14   327   39   4%    646  -77   17   14  119%
c -  864.3    7899    44565   2890423  181076  20475 14584   15   470   41   3%    893  106   15   14  110%
c -  885.8    7899    44565   2960612  182549  20542 14585   12   170   27   7%    979 -228   12   14   83%
c -  910.0    7899    44565   3032143  185378  20610 14586   15   732   27   2%   1009  262   15   15  104%
c -  930.4    7899    44565   3104031  189366  20685 14589   14   291   28   5%   1019 -163   14   15   96%
c -  949.4    7899    44564   3175402  192015  20750 14589   16   660   28   2%   1022  192   17   15  112%
c -  971.4    7899    44564   3246329  194174  20798 14590   15   657   42   2%   1023  122   13   15   83%
c 
c [simplification-20] limit 3299422 conflicts (hard 3683402) hit after 3299422 conflicts
c [quatres-18] found 32019 quaternary clauses 18% in total
c [quatres-18-1] removed 33 duplicate quaternary clauses
c [quatres-18-1] added 15 double-self-subsuming ternary resolvents
c [quatres-18-2] added 109 single-self-subsuming ternary resolvents
c [quatres-18-2] added 267 quaternary resolvents
c [ternres-17] limit 200000000 with penalty 0 = 0 + 0
c [ternres-17] all 7899 free variables schedulable
c [ternres-17] 1951 ternary resolvents (135 bin, 1816 trn)
c [ternres-17] fully completed ternary resolution
c [decomp-89] removed 4 variables
c [treelook-7] limit 29830278 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 14818 literals 94%
c [treelook-7] scheduling used 880582 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 29830278 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 10484509 steps
c [treelook-7] fully completed tree based probing
c [decomp-90] removed 2 variables
c [treelook-7] removed 8 variables, found 3048 hbrs
c [unhide-14] limit 5000000 with penalty 2 = 2 + 0
c [unhide-14-37] 0 units, 0 failed, 4103 tauts, 0 hbrs, 220138 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 584 transitive binary clauses
c [cce-11] limit of 1491513915 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 2 clauses out of 8 (25%) of length 16
c [cce-11-1] eliminated 13 clauses out of 99 (13%) of length 13
c [cce-11-1] eliminated 3 clauses out of 43 (7%) of length 12
c [cce-11-1] eliminated 9 clauses out of 92 (10%) of length 11
c [cce-11-1] eliminated 10 clauses out of 190 (5%) of length 10
c [cce-11-1] eliminated 28 clauses out of 383 (7%) of length 9
c [cce-11-1] eliminated 25 clauses out of 566 (4%) of length 8
c [cce-11-1] eliminated 62 clauses out of 1318 (5%) of length 7
c [cce-11-1] eliminated 112 clauses out of 2456 (5%) of length 6
c [cce-11-1] eliminated 180 clauses out of 4594 (4%) of length 5
c [cce-11-1] eliminated 266 clauses out of 9371 (3%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 710 large clauses in 99334254 steps
c [cce-11-1] allowing another 49667127 steps for small clauses
c [cce-11-1] scheduling 19148 clauses = 8267 binary + 10881 ternary
c [cce-11-1] tried to eliminate 19148 small clauses 100%
c [cce-11-1] eliminated 111 binary clauses 1%
c [cce-11-1] eliminated 422 ternary clauses 4%
c [cce-11-1] eliminated 533 small clauses 3%
c [cce-11-1] eliminated 533 small clauses in 96687659 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 1243 covered clauses in round 1
c [cce-11-2] eliminated 1 clauses out of 40 (2%) of length 12
c [cce-11-2] eliminated 5 clauses out of 83 (6%) of length 11
c [cce-11-2] eliminated 3 clauses out of 180 (2%) of length 10
c [cce-11-2] eliminated 2 clauses out of 355 (1%) of length 9
c [cce-11-2] eliminated 8 clauses out of 541 (1%) of length 8
c [cce-11-2] eliminated 6 clauses out of 1256 (0%) of length 7
c [cce-11-2] eliminated 36 clauses out of 2344 (2%) of length 6
c [cce-11-2] eliminated 47 clauses out of 4414 (1%) of length 5
c [cce-11-2] eliminated 55 clauses out of 9105 (1%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 163 large clauses in 95253685 steps
c [cce-11-2] allowing another 47626842 steps for small clauses
c [cce-11-2] scheduling 18615 clauses = 8156 binary + 10459 ternary
c [cce-11-2] tried to eliminate 18615 small clauses 100%
c [cce-11-2] eliminated 64 binary clauses 1%
c [cce-11-2] eliminated 42 ternary clauses 0%
c [cce-11-2] eliminated 106 small clauses 1%
c [cce-11-2] eliminated 106 small clauses in 93004836 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 269 covered clauses in round 2
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 120 basic ate = 47 trn 39% + 73 lrg 61% in 5 updates
c bcas: 18 count, 994 added (132 skipped), 1719169 steps
c bkwd: tried 118528 clauses, 236856 lits, 2.00 lits/clause
c bkwd: checked 42513785 occs, 358.68 occs/clause, 179.49 occs/lit
c bkwd: subsumed 0 binary, 20 ternary, 35 large
c bkwd: strengthened 0 binary, 12 ternary (100% self), 223 large (0% self)
c blkd: 6 bces, 2525 removed, 1905163 resolutions, 4832318 steps
c blkd: 2126 blocking literals 2%, 34 pure
c bump: 0 bumped seen, 0 lits 0.0 on average
c card: 5 count, 0 units, 38 am1, 13702255 steps
c card: 10 rescheduled, 67 eliminated, 4383 resolved, 4942 subsumed
c card: 1374 at-most-one constraints found, average size 3.43
c card: 1374 at-most-one constraints used 100%, average size 3.43
c card: 51 at-most-two constraints found, average size 4.08
c card: 51 at-most-two constraints used 100%, average size 4.08
c cces: 11 cces, 11404 eliminated, 9828 ate 86%, 1576 abce 14%
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: 463874 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 142 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 90 decompositions, 3035 equivalent 6%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 111367862 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 13 elims, 35832 eliminated 75%, 71 pure 0%
c elms: 37 rounds, 2.8 rounds/bve
c elms: 34130 small 95%, 1597 large 4%
c elms: 59214 tried small, 34130 succeeded 58%, 25084 failed 42%
c elms: 2901 subsumed, 3901 strengthened, 331 blocked
c elms: 3713009 copies, 4959866 resolutions, 1716744 ipos
c elms: 2066303 subchks, 1207285 strchks
c gaus: 7 extractions, 27035 extracted, 3.0 size, 4 max
c gaus: exported 1 units, 0 binary and 21 ternary equations
c gaus: 1 gc, 23702684 steps, 11851342 extr 50%, 1710100 elim 7%
c glue: 14.4 orig avg, 14.4 real avg, 3.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 61147 = 11923 simple 19% + 39621 trn 65% + 9603 lrg 16%, 984 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3313180 clauses, 28.6 length
c lrnd: 94679217 lits = 127164455 orig - 32485238 removed 26%
c lrnd: 1801683 uips 54%, 504254 flips 15%
c mins: 3225996 mins 97%, 782 bin 0%, 86401 size 3%
c mins: 107435873 poisoned searches, 14464609 hits, 13% hit rate
c mins: 216355588 used twice searches, 27400381 hits, 13% hit rate
c move: moved 5967, 1704 bin 29%, 4263 trn 71%
c otfs: 13066 driving 31%, 29377 restarting 69%
c otfs: str 42443, 41712 red 98%, 731 irr 2%
c otfs: str 42443, 0 bin 0%, 819 trn 2%, 41624 lrg 98%
c otfs: sub 601, 425 red 71%, 176 irr 29%
c otfs: sub 601, 0 bin 0%, 81 trn 13%, 520 lrg 87%
c phas: 1 computed, 12263 set, 3109 pos (25%), 9154 neg (75%)
c prbs: 6 basic, 322076 probed, 69 failed, 0 lifted
c prbs: 7 simple, 184665 probed, 194 failed, 2259 eqs
c prbs: 7 treelook, 25315 probed, 37 failed, 0 lifted
c prom: 723846 locked 17% out of 4361052 tried
c prps: 1248428060 props, 11 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 18 count, 5283 quat, 1347 self1, 82 self2, 671 dup
c queu: 19 sorted, 111367862 next (0 steps 0.00)
c queu: 235574 enq (235554 steps 1.00), 0 deq 0%
c redc: 47422 clauses 11%, 420348 tried 13%, 10 sat 0%
c redc: 62499 lits 1%, 4366976 tried 3%, 10 sat 0%
c redc: 1036 times jump level reduced, 60.0 levels on average
c reds: 57 count, 57884.6 conflicts per reduce
c reds: 0 memlim 0%, 57 arith 100%
c reds: 2215143 collected 76%, 716869 retired 24%
c rmbd: 2549 removed, 2036 red 80%
c rsts: 37149 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 20 count, 20 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 3313180 count (1349233 tried 0.4), 77153 sub out of 3301283 (2.3%)
c swps: 18 count, 30 rounds, 11831 queries (394.4/round)
c swps: 11493 sat calls, 853 unsat (2.3% success rate)
c swps: 341518 decisions 29.7, 26824 conflicts 2.3
c swps; 110.8 avg class size, 74.5 avg environment size
c swps: 0 failed, 969 impls, 1170 equivs
c swp0: 3933 type 0 queries, 1003 unsat (25.5%), 3694 sat (93.9%)
c swp1: 7898 type 1 queries, 3220 unsat (40.8%), 6967 sat (88.2%)
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: 222736224 calls to obtain time
c tops: 891 fixed 2%, 31 its, 106432.97 confs/it
c trds: 18 transitive reductions, 9537 removed, 4 failed
c trds: 213177 nodes, 241603 edges, 32016092 steps
c trim: 468480 words, 1.8 MB
c trnr: 17 count, 1780 bin, 31679 trn, 308076232 steps
c unhd: 14 count, 37 rounds, 62738938 steps
c unhd: 164 non-trivial sccs of average size 2.0
c unhd: 4 units, 4 bin, 0 trn, 0 lrg
c unhd: 70 failed, 70 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 25716 tauts, 602 bin 2%, 8445 trn 33%, 3489 lrg 14%
c unhd: 25716 tauts, 13180 stamp 51%, 25345 red 99%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 781035 str, 4 bin 0%, 975 trn 0%, 780056 lrg 100%, 777063 red 99%
c vars: 7899 remaining 17% and 39758 removed 83% out of 47657
c vars: 891 fixed 2%, 35832 eliminated 75%, 3035 equivalent 6%
c vsts: 30306067820 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 24.5 search visits per propagation, 9041.1 per conflict
c wchs: 9986312743 pushed, 27603890 enlarged, 345 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3306566       2215143        716869     190911623      27395990       1955812
c 
c  0 0        192066   6      8218   0         0   0 147296113  77< 15249891  56    875984  45     5.4
c  1 5        139193   4     74601   3     46177   6  18574196  10   3325572  12<   238309  12<    0.7
c  2 6        515725  16    361107  16    120225  17  16782673   9   4328504  16    389423  20     1.7
c  3 9        923920  28<   701973  32<   174409  24   5043278   3   2553746   9    282007  14     3.0
c  4 14       911257  28    670985  30    188271  26<  2130431   1   1327381   5    126562   6     3.8
c  5 21       439919  13    293890  13    117810  16    792045   0    462761   2     33866   2     1.9
c  6 30       138049   4     81773   4     48522   7    224765   0    117836   0      7763   0     0.9
c  7 41        35551   1     18091   1     15663   2     53277   0     24526   0      1550   0     0.4
c  8 54         8369   0      3566   0      4338   1     11697   0      4666   0       297   0     0.1
c  9 69         2020   0       774   0      1148   0      2561   0       922   0        44   0     0.0
c 10 86          478   0       162   0       291   0       567   0       182   0         7   0     0.0
c 11 126          19   0         3   0        15   0        20   0         3   0         0   0     0.0
c 
c avg                  3.3           3.5           3.6           0.4           1.0           1.3
c std                  1.5           1.2           1.5           0.9           1.4           1.5
c 
c   68.365   7% cce
c   68.273   7% decide
c   14.300   1% sweep
c   11.486   1% probe
c    7.769   1% unhide
c 
c   15.654 < 1% rest (below)
c 
c    6.515   1% elim
c    2.377   0% quatres
c    2.255   0% ternres
c    2.101   0% transred
c    0.909   0% bca
c    0.816   0% gauss
c    0.490   0% block
c    0.192   0% card
c    0.000   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.456   0% preprocessing     1%
c  118.729  12% inprocessing     99%
c ==================================
c  120.185  12% simplifying
c  879.829  88% search
c ==================================
c 1000.015 100% all
c 
c       3299422 conflicts,        3299.4 confs/sec
c          8342 ternaries,         395.5 confs/ternary
c           621 binaries,         5313.1 confs/binary
c            31 iterations,     106433.0 confs/iteration
c 
c            57 reductions,          0.1 redus/sec,  57884.6 confs/reduction
c         37149 restarts,           37.1 rests/sec,     88.8 confs/restart
c     111367862 decisions,      111366.2 decis/sec,     33.8 decis/conflict
c    1248428060 propagations,  1248409.5 props/sec,     11.2 props/decision
c 
c 1000.0 seconds, 73.1 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
