c launch: /data/cnf/sc2014/app/6s16-opt.cnf.bz2
c host: atom19
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 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 fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/6s16-opt.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/6s16-opt.cnf.bz2
c no embedded options
c found 'p cnf 30823 89899' header
c read 30823 variables, 89899 clauses, 209763 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 --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 30819 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 
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   30819    89898         0       0      0     0    0     0    5   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 1 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] 1 out of 1 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 1 at-most-one constraints, 1 used 100%
c [card-1] exported 1 binary clauses, 1.0 per/constraint
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 30819 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 1046 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 1046 variables, found 1766 hbrs, 100 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 2 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 29773 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 21616 variables 73% in round 1 in 6027372 steps
c [elim-1-1] backward subsumption/strengthening limit 6027300
c [elim-1-1-1] backward checking 21440 touched variables 72%
c [elim-1-1-1] incomplete backward checking 21209 remain 99%
c [elim-1-1] subsumed 30 and strengthened 120 clauses in 6028562 steps
c [elim-1-1] rescheduled 345 variables 1% by backward subsumption
c [elim-1-2] eliminated 16 variables 0% in round 2 in 237000 steps
c [elim-1-2] backward subsumption/strengthening limit 237000
c [elim-1-2-1] backward checking 21241 touched variables 71%
c [elim-1-2-1] incomplete backward checking 21190 remain 100%
c [elim-1-2] subsumed 0 and strengthened 25 clauses in 237109 steps
c [elim-1-2] rescheduled 64 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 36678 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 21636 = 73% variables out of 29773 scheduled
c [phase-count-1] 39188 negative 88.7% of 44165 except 4977 11.3%
c [phase-count-1] 36975 positive 83.7% of 44165 except 7190 16.3%
c [phase-1] phase bias: 2231 positive 27%, 5906 negative 73%
c [sort-queue-1] sorted 8137 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 8137 (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 22682 variables 73.6% (8137 remain 26%)
c [simplification-1] removed 45733 irredundant clauses 50.9% (44165 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 [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 9 variables
c [simpleprobe-2] all 8128 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 3 variables
c [simpleprobe-2] 1244 variables remain 15% (6881 retained 85%)
c [simpleprobe-2] removed 3 variables, found 607 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 16250 literals 100%
c [treelook-1] scheduling used 188934 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300001 steps
c [treelook-1] 16196 literals remain 100%
c [treelook-1] 8125 variables remain to probed next time 100%
c [decomp-5] removed 2 variables
c [treelook-1] removed 2 variables, found 2127 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 3127 probes remain 39% after last round
c [basicprobe-1-0] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 2 variables, found 4456 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 8121 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 1739 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 38 (5%) of length 15
c [cce-1-1] eliminated 2 clauses out of 32 (6%) of length 14
c [cce-1-1] eliminated 1 clauses out of 101 (1%) of length 10
c [cce-1-1] eliminated 2 clauses out of 230 (1%) of length 9
c [cce-1-1] eliminated 52 clauses out of 407 (13%) of length 8
c [cce-1-1] eliminated 63 clauses out of 785 (8%) of length 7
c [cce-1-1] eliminated 192 clauses out of 2034 (9%) of length 6
c [cce-1-1] eliminated 285 clauses out of 3258 (9%) of length 5
c [cce-1-1] eliminated 427 clauses out of 8075 (5%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 1026 large clauses in 28407681 steps
c [cce-1-1] allowing another 14203840 steps for small clauses
c [cce-1-1] scheduling 13787 clauses = 8100 binary + 5687 ternary
c [cce-1-1] tried to eliminate 7736 small clauses 56%
c [cce-1-1] eliminated 74 binary clauses 1%
c [cce-1-1] eliminated 162 ternary clauses 3%
c [cce-1-1] eliminated 236 small clauses 2%
c [cce-1-1] eliminated 236 small clauses in 30000002 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1262 covered clauses in round 1
c [cce-1] eliminated 1262 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 8118 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 534 variables 7% in round 1 in 6389495 steps
c [elim-2-1] backward subsumption/strengthening limit 6389400
c [elim-2-1-1] backward checking 2863 touched variables 35%
c [elim-2-1-1] incomplete backward checking 2813 remain 98%
c [elim-2-1] subsumed 7 and strengthened 13 clauses in 6390771 steps
c [elim-2-1] rescheduled 72 variables 1% by backward subsumption
c [elim-2-2] eliminated 7 variables 0% in round 2 in 105393 steps
c [elim-2-2] backward subsumption/strengthening limit 105300
c [elim-2-2-1] backward checking 2824 touched variables 35%
c [elim-2-2-1] incomplete backward checking 2822 remain 100%
c [elim-2-2] subsumed 0 and strengthened 0 clauses in 106389 steps
c [elim-2-2] fully rescheduled 7577 variables 93%
c [elim-2-3] eliminated 23 variables 0% in round 3 in 6236188 steps
c [elim-2-3] backward subsumption/strengthening limit 771764
c [elim-2-3-1] backward checking 2851 touched variables 35%
c [elim-2-3-1] incomplete backward checking 2838 remain 100%
c [elim-2-3] subsumed 0 and strengthened 1 clauses in 772959 steps
c [elim-2] incomplete 4 not tried 0% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 564 = 7% variables out of 8118 scheduled
c [bca-1] limit of 10000000 steps and 81460 added (scaled 2)
c [bca-1] 12827 out of 15110 literals actually usable 85%
c [bca-1] added 493 blocked clauses in 35057 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2991 pos 39.6% + 4563 neg 60.4% = 7554 sched 100.0% ret 0
c [sweep-1-1] 1022069 steps 153 queries 372.34 avg class size
c [sweep-1-1] 2163 decisions 153 SAT calls 27.84 avg env size
c [sweep-1-1] 5486 variables remain 73% (2068 retained 27%)
c [decomp-6] removed 20 variables
c [sweep-1-1] removed 20 vars (0 failed, 4 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 20 vars in TOTAL (1 rounds, 152 queries)
c [sort-queue-2] sorted 7534 enqueued variables after 1000 conflicts
c [score-dist-2] active 0 (0%), one 3905 (52%), zero 3629 (48%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 603 variables 7.4% (7534 remain 24%)
c [simplification-2] removed 3703 irredundant clauses 8.4% (40462 remain 45%)
c [simplification-2] maximum reduction of 8% = max (7%, 8%)
c [simplification-2] large reduction 8% >= 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  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    2.7    7533    40462      2853    2151    965  7594    3    57    5   5%     29   55    7    0 2682%
c i    2.7    7532    40462      2884    2178    967  7594    3    59    5   5%     28   57    7    0 2619%
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3001 conflicts
c [quatres-1] found 7950 quaternary clauses 49% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 19 single-self-subsuming ternary resolvents
c [quatres-1-2] added 529 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 7532 free variables schedulable
c [ternres-1] 4280 ternary resolvents (66 bin, 4214 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 423 at-most-one constraints of average size 3.4
c [card-2] found 32 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 455 out of 455 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 15 at-most-one constraints, 10 used 67%
c [card-2] exported 10 binary clauses, 1.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 4429 xors of average arity 3.0
c [gauss-1] connected 13243 occurrences of 907 variables (average 14.6)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-7] removed 21 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 15022 literals 100%
c [treelook-2] scheduling used 206489 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 300620 steps
c [treelook-2] 14888 literals remain 99%
c [treelook-2] 7511 variables remain to probed next time 100%
c [treelook-2] removed 0 variables, found 17 hbrs
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 837 tauts, 0 hbrs, 1488 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 73 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 7511 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 18 blocked clauses
c [block-2] 18 < 1/100 * 40407 = 404 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 2 clauses out of 99 (2%) of length 13
c [cce-2-1] eliminated 3 clauses out of 127 (2%) of length 10
c [cce-2-1] eliminated 10 clauses out of 261 (4%) of length 9
c [cce-2-1] eliminated 19 clauses out of 478 (4%) of length 8
c [cce-2-1] eliminated 55 clauses out of 962 (6%) of length 7
c [cce-2-1] eliminated 103 clauses out of 2029 (5%) of length 6
c [cce-2-1] eliminated 129 clauses out of 3377 (4%) of length 5
c [cce-2-1] eliminated 341 clauses out of 7682 (4%) of length 4
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 662 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2-1] scheduling 19612 clauses = 7368 binary + 12244 ternary
c [cce-2-1] tried to eliminate 16771 small clauses 86%
c [cce-2-1] eliminated 44 binary clauses 1%
c [cce-2-1] eliminated 384 ternary clauses 3%
c [cce-2-1] eliminated 428 small clauses 2%
c [cce-2-1] eliminated 428 small clauses in 30000011 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1090 covered clauses in round 1
c [cce-2] eliminated 1090 covered clauses in TOTAL during 1 rounds
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 7511 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 123 variables 2% in round 1 in 7130949 steps
c [elim-3-1] backward subsumption/strengthening limit 7130900
c [elim-3-1-1] backward checking 859 touched variables 11%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 2 and strengthened 1 clauses in 989220 steps
c [elim-3-1] rescheduled 8 variables 0% by backward subsumption
c [elim-3-2] eliminated 1 variables 0% in round 2 in 9098 steps
c [elim-3-2] backward subsumption/strengthening limit 9000
c [elim-3-2-1] backward checking 6 touched variables 0%
c [elim-3-2-1] incomplete backward checking 0 remain 0%
c [elim-3-2] subsumed 1 and strengthened 5 clauses in 9001 steps
c [elim-3-2] rescheduled 6 variables 0% by backward subsumption
c [elim-3-3] no variable eliminated in round 3 in 4394 steps
c [elim-3] fully completed in 3 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 124 = 2% variables out of 7511 scheduled
c [bca-2] limit of 10000000 steps and 78930 added (scaled 2)
c [bca-2] 9394 out of 14776 literals actually usable 64%
c [bca-2] added 7 blocked clauses in 27567 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2237 pos 41.6% + 3137 neg 58.4% = 5374 sched 72.7% ret 2013
c [sweep-2-1] 1002085 steps 134 queries 300.60 avg class size
c [sweep-2-1] 1694 decisions 132 SAT calls 26.12 avg env size
c [sweep-2-1] 4338 variables remain 59% (3048 retained 41%)
c [decomp-9] removed 13 variables
c [sweep-2-1] removed 13 vars (0 failed, 9 eqs, 10 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 13 vars in TOTAL (1 rounds, 133 queries)
c [sort-queue-3] sorted 7374 enqueued variables after 3001 conflicts
c [score-dist-3] active 0 (0%), one 5468 (74%), zero 1906 (26%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 158 variables 2.1% (7374 remain 24%)
c [simplification-3] removed 1378 irredundant clauses 3.4% (39084 remain 43%)
c [simplification-3] maximum reduction of 3% = max (2%, 3%)
c [simplification-3] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-3] new conflict interval 5000
c [simplification-3] penalized conflict interval 5000 = 1 * 5000
c [simplification-3] hard conflict limit 18001 (soft 8001 + delta 10000)
c [simplification-3] new conflict limit 8001 (hard 18001)
c 
c [simplification-4] limit 8001 conflicts (hard 18001) hit after 8002 conflicts
c [quatres-2] found 8571 quaternary clauses 49% in total
c [quatres-2-1] added 5 double-self-subsuming ternary resolvents
c [quatres-2-2] added 35 single-self-subsuming ternary resolvents
c [quatres-2-2] added 261 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 7374 free variables schedulable
c [ternres-2] 572 ternary resolvents (25 bin, 547 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-10] removed 23 variables
c [basicprobe-2] limit 1398368 penalty 0 = 0 + 0
c [basicprobe-2-0] 1209 probes remain 16% after last round
c [basicprobe-2-0] 11 units = 9 failed (82%) + 2 lifted (18%)
c [basicprobe-2-0] removed 9 variables, found 2951 hbrs
c [transred-2] limit 279673 with penalty 0 = 0 + 0
c [transred-2] removed 191 transitive binary clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 3 clauses out of 72 (4%) of length 11
c [cce-3-1] eliminated 2 clauses out of 133 (2%) of length 10
c [cce-3-1] eliminated 2 clauses out of 285 (1%) of length 9
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 7 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3-1] scheduling 18706 clauses = 7187 binary + 11519 ternary
c [cce-3-1] tried to eliminate 2762 small clauses 15%
c [cce-3-1] eliminated 7 binary clauses 0%
c [cce-3-1] eliminated 24 ternary clauses 0%
c [cce-3-1] eliminated 31 small clauses 0%
c [cce-3-1] eliminated 57 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 64 covered clauses in round 1
c [cce-3] eliminated 64 covered clauses in TOTAL during 1 rounds
c [cce-3] 64 < 1/100 * 39046 = 390 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 7342 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 39 variables 1% in round 1 in 7442157 steps
c [elim-4-1] backward subsumption/strengthening limit 7442100
c [elim-4-1-1] backward checking 346 touched variables 5%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 5 and strengthened 1 clauses in 2487328 steps
c [elim-4-1] rescheduled 10 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 399539 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 40 = 1% variables out of 7342 scheduled
c [elim-4] 40 < 1/100 * 7342 = 73 considered unsuccessful
c [bca-3] limit of 10000000 steps and 78384 added (scaled 2)
c [bca-3] 6019 out of 14606 literals actually usable 41%
c [bca-3] added 0 blocked clauses in 21284 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1744 pos 40.7% + 2546 neg 59.3% = 4290 sched 58.8% ret 3012
c [sweep-3-1] 1006986 steps 143 queries 221.93 avg class size
c [sweep-3-1] 2469 decisions 136 SAT calls 30.57 avg env size
c [sweep-3-1] 3223 variables remain 44% (4077 retained 56%)
c [decomp-11] removed 29 variables
c [sweep-3-1] removed 29 vars (0 failed, 10 eqs, 14 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 29 vars in TOTAL (1 rounds, 142 queries)
c [sort-queue-4] sorted 7273 enqueued variables after 8002 conflicts
c [score-dist-4] active 0 (0%), one 6721 (92%), zero 552 (8%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 101 variables 1.4% (7273 remain 24%)
c [simplification-4] removed 289 irredundant clauses 0.7% (38792 remain 43%)
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 15000
c [simplification-4] penalized conflict interval 15000 = 1 * 15000
c [simplification-4] hard conflict limit 33002 (soft 23002 + delta 10000)
c [simplification-4] new conflict limit 23002 (hard 33002)
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    8.2    7272    38792      8266    7221   5518  9844    6   106    6   6%     65   99    8    1 1083%
c i    8.7    7271    38792     11769   10131   5675  9871    6   112    6   6%     37  100    7    1  682%
c i    8.7    7270    38792     11875   10212   5684  9875    6   113    6   6%     33  100    7    1  648%
c i    9.0    7269    38789     13814   11774   5789  9900    7   120    6   6%     17  104    7    1  566%
c i    9.0    7268    38789     14171   12082   5800  9901    7   121    6   6%     11  104    8    1  592%
c i    9.0    7267    38789     14173   12082   5801  9901    7   121    6   6%     11  104    7    1  588%
c i    9.0    7266    38789     14175   12082   5802  9901    7   121    6   6%     11  104    7    1  584%
c i    9.0    7265    38789     14177   12082   5803  9901    7   121    6   6%     11  104    7    1  581%
c i    9.5    7264    38788     18316   15620   5917  9935    7   116    6   6%     43   93    8    2  498%
c i    9.5    7263    38788     18322   15620   5920  9935    7   116    6   6%     42   93    8    2  489%
c 
c [simplification-5] limit of 12 iterations hit after 12 iterations
c [quatres-3] found 9361 quaternary clauses 47% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 62 single-self-subsuming ternary resolvents
c [quatres-3-2] added 216 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 7263 free variables schedulable
c [ternres-3] 752 ternary resolvents (39 bin, 713 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 3484 xors of average arity 3.0
c [gauss-2] connected 10343 occurrences of 902 variables (average 11.5)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 30 variables
c [simpleprobe-3] 1098 schedulable variables 15%
c [simpleprobe-3] limit 2592853 penalty 0 = 0 + 0
c [decomp-13] removed 23 variables
c [simpleprobe-3] 422 variables remain 6% (6788 retained 94%)
c [simpleprobe-3] removed 23 variables, found 1435 hbrs, 8 units
c [transred-3] limit 648213 with penalty 0 = 0 + 0
c [transred-3] removed 657 transitive binary clauses
c [transred-3] found 2 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 7208 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 69 blocked clauses
c [block-3] 69 < 1/100 * 38582 = 385 considered unsuccessful
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1467 pos 46.3% + 1703 neg 53.7% = 3170 sched 44.0% ret 4029
c [sweep-4-1] 1008791 steps 122 queries 176.37 avg class size
c [sweep-4-1] 2404 decisions 117 SAT calls 39.63 avg env size
c [sweep-4-1] 2384 variables remain 33% (4815 retained 67%)
c [decomp-14] removed 19 variables
c [sweep-4-1] removed 19 vars (0 failed, 16 eqs, 12 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 19 vars in TOTAL (1 rounds, 121 queries)
c [sort-queue-5] sorted 7180 enqueued variables after 18322 conflicts
c [score-dist-5] active 0 (0%), one 7110 (99%), zero 70 (1%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 83 variables 1.1% (7180 remain 23%)
c [simplification-5] removed 292 irredundant clauses 0.8% (38496 remain 43%)
c [simplification-5] maximum reduction of 1% = max (1%, 1%)
c [simplification-5] forced so keeping old conflict interval 15000
c [simplification-5] conflict limit remains at 23018 (hard 33002)
c [simplification-5] new iteration interval 100
c 
c [simplification-6] limit 23018 conflicts (hard 33002) hit after 23020 conflicts
c [quatres-4] found 9741 quaternary clauses 46% in total
c [quatres-4-1] removed 5 duplicate quaternary clauses
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 42 single-self-subsuming ternary resolvents
c [quatres-4-2] added 110 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 7180 free variables schedulable
c [ternres-4] 225 ternary resolvents (9 bin, 216 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 277 at-most-one constraints of average size 3.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 277 out of 277 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-15] removed 6 variables
c [unhide-3] limit 41318 with penalty 2 = 2 + 0
c [unhide-3-3] 1 units, 0 failed, 199 tauts, 0 hbrs, 6333 literals
c [transred-4] limit 826368 with penalty 0 = 0 + 0
c [transred-4] removed 494 transitive binary clauses
c [transred-4] found 9 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 150000000 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 2 clauses out of 264 (1%) of length 9
c [cce-4-1] eliminated 9 clauses out of 439 (2%) of length 8
c [cce-4-1] eliminated 9 clauses out of 924 (1%) of length 7
c [cce-4-1] eliminated 12 clauses out of 1889 (1%) of length 6
c [cce-4-1] eliminated 27 clauses out of 3258 (1%) of length 5
c [cce-4-1] eliminated 59 clauses out of 7426 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 118 large clauses in 29989065 steps
c [cce-4-1] allowing another 14994532 steps for small clauses
c [cce-4-1] scheduling 12424 clauses = 7002 binary + 5422 ternary
c [cce-4-1] tried to eliminate 12424 small clauses 100%
c [cce-4-1] eliminated 26 binary clauses 0%
c [cce-4-1] eliminated 182 ternary clauses 3%
c [cce-4-1] eliminated 208 small clauses 2%
c [cce-4-1] eliminated 240 small clauses in 37159766 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 358 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 14656182 steps for small clauses
c [cce-4-2] scheduling 12216 clauses = 6976 binary + 5240 ternary
c [cce-4-2] tried to eliminate 12216 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 358 covered clauses in TOTAL during 2 rounds
c [cce-4] 358 < 1/100 * 38402 = 384 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 7164 variables 100%
c [elim-5] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 91 variables 1% in round 1 in 9905626 steps
c [elim-5-1] backward subsumption/strengthening limit 94374
c [elim-5-1-1] backward checking 583 touched variables 8%
c [elim-5-1-1] incomplete backward checking 438 remain 75%
c [elim-5-1] subsumed 0 and strengthened 4 clauses in 94857 steps
c [elim-5] incomplete 11 not tried 0% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 91 = 1% variables out of 7164 scheduled
c [bca-4] limit of 10000000 steps and 76416 added (scaled 2)
c [bca-4] 3113 out of 14148 literals actually usable 22%
c [bca-4] added 3 blocked clauses in 26170 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 953 pos 40.8% + 1384 neg 59.2% = 2337 sched 33.0% ret 4736
c [sweep-5-1] 5307540 steps 581 queries 50.48 avg class size
c [sweep-5-1] 11075 decisions 558 SAT calls 37.53 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-16] removed 105 variables
c [sweep-5-1] removed 105 vars (0 failed, 101 eqs, 75 impls)
c [sweep-5-2] 2719 pos 39.0% + 4249 neg 61.0% = 6968 sched 100.0% ret 0
c [sweep-5-2] 4739973 steps 431 queries 76.41 avg class size
c [sweep-5-2] 8289 decisions 410 SAT calls 41.90 avg env size
c [sweep-5-2] 1226 variables remain 18% (5738 retained 82%)
c [decomp-17] removed 83 variables
c [sweep-5-2] removed 83 vars (0 failed, 64 eqs, 64 impls)
c [sweep-5] removed 188 vars in TOTAL (2 rounds, 1010 queries)
c [sort-queue-6] sorted 6885 enqueued variables after 23020 conflicts
c [score-dist-6] active 0 (0%), one 6849 (99%), zero 36 (1%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 295 variables 4.1% (6885 remain 22%)
c [simplification-6] removed 763 irredundant clauses 2.0% (37732 remain 42%)
c [simplification-6] maximum reduction of 4% = max (4%, 2%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 19000
c [simplification-6] penalized conflict interval 19000 = 1 * 19000
c [simplification-6] hard conflict limit 52020 (soft 42020 + delta 10000)
c [simplification-6] new conflict limit 42020 (hard 52020)
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   13.1    6884    37731     25086   21847   6343 10483    8   113    8   7%     79   81    7    2  322%
c i   13.2    6883    37731     25367   22094   6345 10488    8   115    8   7%     58   83    8    2  343%
c i   13.2    6882    37728     25979   22620   6368 10495    8   110    8   7%     29   78    7    2  307%
c i   13.2    6881    37728     25984   22623   6369 10495    8   110    8   7%     29   77    7    2  303%
c i   13.3    6880    37726     26685   23248   6382 10500    8   111    8   7%     12   77    8    2  341%
c i   13.4    6879    37723     26835   23370   6386 10502    8   110    8   7%      9   76    8    2  322%
c i   13.6    6878    37718     28442   24765   6441 10508    7   104    8   7%      5   69    7    2  267%
c i   13.7    6877    37714     29834   25944   6483 10522    7   101    8   7%      2   65    8    3  318%
c i   13.8    6876    37714     30272   26338   6493 10525    8   102    8   7%     -1   65    9    3  326%
c i   13.8    6875    37714     30273   26338   6493 10525    8   102    8   7%     -1   65    9    3  325%
c i   13.8    6874    37714     30274   26338   6493 10525    8   102    8   7%     -1   65    9    3  324%
c i   14.1    6873    37710     32917   28650   6556 10543    8   105    8   7%     16   65    8    3  277%
c i   14.7    6872    37709     37037   32288   6658 10566    8   105   11   7%     36   61    8    3  258%
c i   14.7    6871    37708     37085   32329   6660 10567    8   106   11   7%     34   62    8    3  253%
c i   14.9    6870    37708     38420   33534   6679 10570    8   104    9   8%      9   59    8    3  246%
c i   15.2    6869    37708     40274   35227   6727 10577    8    98    9   8%      6   52    8    3  233%
c 
c [simplification-7] limit 42042 conflicts (hard 52020) hit after 42043 conflicts
c [quatres-5] found 10657 quaternary clauses 42% in total
c [quatres-5-1] removed 17 duplicate quaternary clauses
c [quatres-5-1] added 6 double-self-subsuming ternary resolvents
c [quatres-5-2] added 98 single-self-subsuming ternary resolvents
c [quatres-5-2] added 174 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 6869 free variables schedulable
c [ternres-5] 1418 ternary resolvents (54 bin, 1364 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-18] removed 36 variables
c [treelook-3] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 8194 literals 60%
c [treelook-3] scheduling used 150004 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 251396 steps
c [treelook-3] 8152 literals remain 60%
c [treelook-3] 5931 variables remain to probed next time 87%
c [treelook-3] removed 1 variables, found 637 hbrs
c [transred-5] limit 1648843 with penalty 0 = 0 + 0
c [transred-5] removed 650 transitive binary clauses
c [transred-5] found 14 units
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 6832 variables 100%
c [elim-6] limit of 32976869 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 160 variables 2% in round 1 in 9762238 steps
c [elim-6-1] backward subsumption/strengthening limit 9762200
c [elim-6-1-1] backward checking 751 touched variables 11%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 1 and strengthened 11 clauses in 911088 steps
c [elim-6-1] rescheduled 41 variables 1% by backward subsumption
c [elim-6-2] eliminated 3 variables 0% in round 2 in 2279922 steps
c [elim-6-2] backward subsumption/strengthening limit 2279900
c [elim-6-2-1] backward checking 30 touched variables 0%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 1 and strengthened 4 clauses in 26320 steps
c [elim-6-2] rescheduled 9 variables 0% by backward subsumption
c [elim-6-3] eliminated 3 variables 0% in round 3 in 15126 steps
c [elim-6-3] backward subsumption/strengthening limit 15100
c [elim-6-3-1] backward checking 11 touched variables 0%
c [elim-6-3-1] incomplete backward checking 0 remain 0%
c [elim-6-3] subsumed 2 and strengthened 2 clauses in 15173 steps
c [elim-6] incomplete 9 not tried 0% in round 3
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 166 = 2% variables out of 6832 scheduled
c [bca-5] limit of 10000000 steps and 73665 added (scaled 2)
c [bca-5] 1908 out of 13334 literals actually usable 14%
c [bca-5] added 6 blocked clauses in 39439 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 457 pos 40.5% + 672 neg 59.5% = 1129 sched 16.9% ret 5537
c [sweep-6-1] 1019435 steps 46 queries 82.59 avg class size
c [sweep-6-1] 936 decisions 42 SAT calls 43.36 avg env size
c [sweep-6-1] 980 variables remain 15% (5686 retained 85%)
c [decomp-20] removed 5 variables
c [sweep-6-1] removed 5 vars (0 failed, 3 eqs, 6 impls)
c [sweep-6] 5 < 1/1000 * 6666 = 6 considered unsuccessful
c [sweep-6] removed 5 vars in TOTAL (1 rounds, 45 queries)
c [sort-queue-7] sorted 6661 enqueued variables after 42043 conflicts
c [score-dist-7] active 0 (0%), one 6652 (100%), zero 9 (0%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 208 variables 3.0% (6661 remain 22%)
c [simplification-7] removed 1256 irredundant clauses 3.3% (36451 remain 41%)
c [simplification-7] maximum reduction of 3% = max (3%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 24000
c [simplification-7] penalized conflict interval 24000 = 1 * 24000
c [simplification-7] hard conflict limit 78043 (soft 66043 + delta 12000)
c [simplification-7] new conflict limit 66043 (hard 78043)
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   16.7    6660    36450     45755   38720   7236 10060    8   102   10   8%     55   52    9    4  247%
c i   16.8    6659    36450     46530   39414   7255 10062    8   101   10   8%     21   50    8    4  224%
c i   17.9    6658    36450     53125   45351   7397 10092    8    99   11   8%     69   44    8    4  192%
c i   17.9    6657    36450     53127   45352   7397 10092    8    99   11   8%     69   43    8    4  191%
c i   18.3    6656    36450     55546   47568   7437 10098    8    96   11   8%     13   39    8    4  193%
c i   18.5    6655    36450     56689   48617   7453 10103    8    91   11   9%     -2   34    8    4  188%
c i   18.9    6654    36450     59076   50788   7494 10114    8    91   11   9%      6   32    8    5  176%
c i   19.3    6653    36450     61387   52922   7517 10124    8    91   11   9%      6   32    9    5  185%
c 
c [simplification-8] limit 66048 conflicts (hard 78043) hit after 66049 conflicts
c [quatres-6] found 11329 quaternary clauses 39% in total
c [quatres-6-1] removed 5 duplicate quaternary clauses
c [quatres-6-1] added 2 double-self-subsuming ternary resolvents
c [quatres-6-2] added 93 single-self-subsuming ternary resolvents
c [quatres-6-2] added 195 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 6653 free variables schedulable
c [ternres-6] 1046 ternary resolvents (35 bin, 1011 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 1364 xors of average arity 3.0
c [gauss-3] connected 4040 occurrences of 760 variables (average 5.3)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-21] removed 29 variables
c [basicprobe-3] limit 14502429 penalty 0 = 0 + 0
c [basicprobe-3-0] 1354 sched 20%, 10 failed, 1 lifted, 2367 hbrs
c [decomp-22] removed 18 variables
c [basicprobe-3-1] 3893 sched 59%, 32 failed, 0 lifted, 3032 hbrs
c [decomp-23] removed 52 variables
c [basicprobe-3-2] 3829 sched 58%, 0 failed, 0 lifted, 159 hbrs
c [basicprobe-3-3] 629 probes remain 10% after last round
c [basicprobe-3-3] 43 units = 42 failed (98%) + 1 lifted (2%)
c [basicprobe-3-3] removed 70 variables, found 5582 hbrs
c [bate-1] eliminated 9 asymmetric tautologies during probing
c [unhide-4] limit 290048 with penalty 1 = 1 + 0
c [unhide-4-4] 0 units, 0 failed, 1658 tauts, 0 hbrs, 31255 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 445 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 6554 variables 100%
c [block-4] limit of 12500000 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 280 blocked clauses
c [block-4] 280 < 1/100 * 36123 = 361 considered unsuccessful
c [elim-7] no untried remaining variables left
c [elim-7] scheduled 6513 variables 100%
c [elim-7] limit of 58009719 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 93 variables 1% in round 1 in 9381713 steps
c [elim-7-1] backward subsumption/strengthening limit 9381700
c [elim-7-1-1] backward checking 506 touched variables 8%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 7 and strengthened 15 clauses in 1316591 steps
c [elim-7-1] rescheduled 48 variables 1% by backward subsumption
c [elim-7-2] eliminated 1 variables 0% in round 2 in 2069983 steps
c [elim-7-2] backward subsumption/strengthening limit 2069900
c [elim-7-2-1] backward checking 6 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 17963 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 94 = 1% variables out of 6513 scheduled
c [bca-6] limit of 10000000 steps and 71696 added (scaled 2)
c [bca-6] 1365 out of 12840 literals actually usable 11%
c [bca-6] added 7 blocked clauses in 57187 steps
c [sort-queue-8] sorted 6419 enqueued variables after 66049 conflicts
c [score-dist-8] active 0 (0%), one 6416 (100%), zero 3 (0%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 234 variables 3.5% (6419 remain 21%)
c [simplification-8] removed 979 irredundant clauses 2.7% (35471 remain 39%)
c [simplification-8] maximum reduction of 4% = max (4%, 3%)
c [simplification-8] geometric conflict interval increment 4800 = 24000 / 5
c [simplification-8] new conflict interval 28800
c [simplification-8] penalized conflict interval 28800 = 1 * 28800
c [simplification-8] hard conflict limit 109249 (soft 94849 + delta 14400)
c [simplification-8] new conflict limit 94849 (hard 109249)
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   22.8    6418    35471     73144   60874   7412 10906    8    78   13  11%    139   13   10    5  183%
c -   24.1    6418    35471     79497   26703   7503 10919    9    79    9  11%     51   13    9    6  158%
c i   26.5    6417    35471     93953   40188   7643 10944    9    69   11  13%    244    1    9    6  150%
c 
c [simplification-9] limit 94849 conflicts (hard 109249) hit after 94849 conflicts
c [quatres-7] found 11853 quaternary clauses 36% in total
c [quatres-7-1] removed 9 duplicate quaternary clauses
c [quatres-7-1] added 4 double-self-subsuming ternary resolvents
c [quatres-7-2] added 106 single-self-subsuming ternary resolvents
c [quatres-7-2] added 271 quaternary resolvents
c [ternres-7] limit 4526718 with penalty 0 = 0 + 0
c [ternres-7] all 6417 free variables schedulable
c [ternres-7] 1368 ternary resolvents (60 bin, 1308 trn)
c [ternres-7] 6 variables remain 0% (6411 retained 100%)
c [decomp-25] removed 32 variables
c [simpleprobe-4] 353 schedulable variables 6%
c [simpleprobe-4] limit 18106873 penalty 0 = 0 + 0
c [decomp-26] removed 32 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 32 variables, found 1244 hbrs, 4 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 559 transitive binary clauses
c [cce-5] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 5 clauses out of 119 (4%) of length 10
c [cce-5-1] eliminated 7 clauses out of 270 (3%) of length 9
c [cce-5-1] eliminated 5 clauses out of 439 (1%) of length 8
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 17 large clauses in 7500001 steps
c [cce-5-1] allowing another 3750000 steps for small clauses
c [cce-5-1] scheduling 16472 clauses = 6234 binary + 10238 ternary
c [cce-5-1] tried to eliminate 1876 small clauses 11%
c [cce-5-1] eliminated 25 binary clauses 0%
c [cce-5-1] eliminated 33 ternary clauses 0%
c [cce-5-1] eliminated 58 small clauses 0%
c [cce-5-1] eliminated 58 small clauses in 7500001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 75 covered clauses in round 1
c [cce-5] eliminated 75 covered clauses in TOTAL during 1 rounds
c [cce-5] 75 < 1/100 * 35255 = 352 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 6355 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1810687320 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 54 variables 1% in round 1 in 9210331 steps
c [elim-8-1] backward subsumption/strengthening limit 9210300
c [elim-8-1-1] backward checking 303 touched variables 5%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1 and strengthened 1 clauses in 687165 steps
c [elim-8-1] rescheduled 8 variables 0% by backward subsumption
c [elim-8-2] no variable eliminated in round 2 in 3590 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 54 = 1% variables out of 6355 scheduled
c [elim-8] 54 < 1/100 * 6355 = 63 considered unsuccessful
c [bca-7] limit of 10000000 steps and 70584 added (scaled 2)
c [bca-7] 1568 out of 12604 literals actually usable 12%
c [bca-7] added 8 blocked clauses in 44025 steps
c [sweep-7] limit 679007 penalty 1 = 1 + 0
c [sweep-7-1] 367 pos 41.2% + 524 neg 58.8% = 891 sched 14.1% ret 5410
c [sweep-7-1] 723930 steps 38 queries 100.37 avg class size
c [sweep-7-1] 1072 decisions 34 SAT calls 73.82 avg env size
c [sweep-7-1] 765 variables remain 12% (5536 retained 88%)
c [decomp-27] removed 8 variables
c [sweep-7-1] removed 8 vars (0 failed, 6 eqs, 5 impls)
c [sweep-7] removed 8 vars in TOTAL (1 rounds, 37 queries)
c [sort-queue-9] sorted 6293 enqueued variables after 94849 conflicts
c [score-dist-9] active 0 (0%), one 6292 (100%), zero 1 (0%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 124 variables 1.9% (6293 remain 20%)
c [simplification-9] removed 562 irredundant clauses 1.6% (34909 remain 39%)
c [simplification-9] maximum reduction of 2% = max (2%, 2%)
c [simplification-9] geometric conflict interval increment 9600 = 28800 / 3
c [simplification-9] new conflict interval 38400
c [simplification-9] penalized conflict interval 38400 = 1 * 38400
c [simplification-9] hard conflict limit 152449 (soft 133249 + delta 19200)
c [simplification-9] new conflict limit 133249 (hard 152449)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   28.4    6292    34909     98369   43911   8604 11408    8    71   11  12%    -10    3    8    6  132%
c i   33.0    6291    34909    125779   69526   8812 11448    8    71   19  11%    294    4    9    7  123%
c i   33.1    6290    34909    126822   70421   8826 11450    7    66   19  11%     35   -1    8    7  119%
c -   34.4    6290    34909    133148   39565   8856 11462    9    60   14  15%    -31   -7   10    7  134%
c 
c [simplification-10] limit 133249 conflicts (hard 152449) hit after 152449 conflicts
c [quatres-8] found 12607 quaternary clauses 30% in total
c [quatres-8-1] removed 15 duplicate quaternary clauses
c [quatres-8-1] added 4 double-self-subsuming ternary resolvents
c [quatres-8-2] added 124 single-self-subsuming ternary resolvents
c [quatres-8-2] added 163 quaternary resolvents
c [ternres-8] limit 7358188 with penalty 0 = 0 + 0
c [ternres-8] 6 schedulable variables 0%
c [ternres-8] 677 ternary resolvents (44 bin, 633 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 459886 penalty 3 = 3 + 0
c [card-4] found 203 at-most-one constraints of average size 3.2
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 459886 for elimination
c [card-4] 203 out of 203 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] extracted 2451 xors of average arity 3.0
c [gauss-4] connected 7291 occurrences of 713 variables (average 10.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-28] removed 21 variables
c [treelook-4] limit 735818 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 11570 literals 92%
c [treelook-4] scheduling used 330994 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 735818 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 737947 steps
c [treelook-4] 11508 literals remain 92%
c [treelook-4] 5415 variables remain to probed next time 86%
c [treelook-4] removed 0 variables, found 562 hbrs
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 392 transitive binary clauses
c [transred-8] found 4 units
c [bca-8] limit of 10000000 steps and 70450 added (scaled 2)
c [bca-8] 1488 out of 12532 literals actually usable 12%
c [bca-8] added 0 blocked clauses in 60818 steps
c [sweep-8] limit 2207456 penalty 0 = 0 + 0
c [sweep-8-1] 345 pos 45.4% + 415 neg 54.6% = 760 sched 12.1% ret 5505
c [sweep-8-1] 2255207 steps 106 queries 33.09 avg class size
c [sweep-8-1] 2001 decisions 92 SAT calls 65.99 avg env size
c [sweep-8-1] 441 variables remain 7% (5824 retained 93%)
c [decomp-30] removed 35 variables
c [sweep-8-1] removed 35 vars (0 failed, 29 eqs, 30 impls)
c [sweep-8] removed 35 vars in TOTAL (1 rounds, 105 queries)
c [sort-queue-10] sorted 6230 enqueued variables after 152449 conflicts
c [score-dist-10] active 0 (0%), one 6229 (100%), zero 1 (0%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 60 variables 1.0% (6230 remain 20%)
c [simplification-10] removed 101 irredundant clauses 0.3% (34808 remain 39%)
c [simplification-10] maximum reduction of 1% = max (1%, 0%)
c [simplification-10] geometric conflict interval increment 19200 = 38400 / 2
c [simplification-10] new conflict interval 57600
c [simplification-10] penalized conflict interval 57600 = 1 * 57600
c [simplification-10] hard conflict limit 238849 (soft 210049 + delta 28800)
c [simplification-10] new conflict limit 210049 (hard 238849)
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   37.2    6229    34808    152613   57699   9094 11599    8    47   14  18%    239  -17    9    7  123%
c i   38.9    6228    34806    164979   69157   9150 11610    8    37   14  21%     35  -24    5    8   64%
c -   41.4    6228    34805    181715   53372   9188 11614    7    35   15  20%    106  -23    6    8   82%
c -   47.5    6228    34802    219455   57131   9277 11622    7    22   15  34%    508  -29    7    8   88%
c 
c [simplification-11] limit 210049 conflicts (hard 238849) hit after 238851 conflicts
c [quatres-9] found 13039 quaternary clauses 25% in total
c [quatres-9-1] removed 4 duplicate quaternary clauses
c [quatres-9-1] added 9 double-self-subsuming ternary resolvents
c [quatres-9-2] added 59 single-self-subsuming ternary resolvents
c [quatres-9-2] added 95 quaternary resolvents
c [ternres-9] limit 11659566 with penalty 0 = 0 + 0
c [ternres-9] all 6228 free variables schedulable
c [ternres-9] 1751 ternary resolvents (75 bin, 1676 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-31] removed 13 variables
c [basicprobe-4] limit 58297832 penalty 0 = 0 + 0
c [basicprobe-4-0] 681 sched 11%, 6 failed, 0 lifted, 555 hbrs
c [decomp-32] removed 11 variables
c [basicprobe-4-1] 3681 sched 60%, 21 failed, 0 lifted, 2333 hbrs
c [decomp-33] removed 42 variables
c [basicprobe-4-2] 3668 sched 60%, 1 failed, 0 lifted, 361 hbrs
c [decomp-34] removed 1 variables
c [basicprobe-4-3] 3668 sched 60%, 0 failed, 0 lifted, 64 hbrs
c [basicprobe-4-4] 3667 sched 60%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-4-5] 3666 sched 59%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-4-6] 3666 sched 59%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-6] fully completed probing
c [basicprobe-4-6] 28 units = 28 failed (100%) + 0 lifted (0%)
c [basicprobe-4-6] removed 54 variables, found 3323 hbrs
c [bate-2] eliminated 9 asymmetric tautologies during probing
c [unhide-5] limit 582978 with penalty 2 = 2 + 0
c [unhide-5-5] 0 units, 0 failed, 290 tauts, 0 hbrs, 43817 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 437 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 6163 variables 100%
c [elim-9] limit of 116595665 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 80 variables 1% in round 1 in 9030016 steps
c [elim-9-1] backward subsumption/strengthening limit 9030000
c [elim-9-1-1] backward checking 415 touched variables 7%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 3 clauses in 716312 steps
c [elim-9-1] rescheduled 10 variables 0% by backward subsumption
c [elim-9-2] eliminated 2 variables 0% in round 2 in 42562 steps
c [elim-9-2] backward subsumption/strengthening limit 42500
c [elim-9-2-1] backward checking 14 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 2 and strengthened 0 clauses in 32285 steps
c [elim-9-2] rescheduled 7 variables 0% by backward subsumption
c [elim-9-3] eliminated 2 variables 0% in round 3 in 100977 steps
c [elim-9-3] backward subsumption/strengthening limit 100900
c [elim-9-3-1] backward checking 11 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 0 and strengthened 0 clauses in 101616 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 84 = 1% variables out of 6163 scheduled
c [sweep-9] limit 3497869 penalty 0 = 0 + 0
c [sweep-9-1] 182 pos 43.4% + 237 neg 56.6% = 419 sched 6.9% ret 5660
c [sweep-9-1] 3523987 steps 142 queries 14.54 avg class size
c [sweep-9-1] 2518 decisions 120 SAT calls 59.92 avg env size
c [sweep-9-1] 108 variables remain 2% (5971 retained 98%)
c [decomp-38] removed 28 variables
c [sweep-9-1] removed 28 vars (0 failed, 28 eqs, 25 impls)
c [sweep-9] removed 28 vars in TOTAL (1 rounds, 141 queries)
c [sort-queue-11] sorted 6051 enqueued variables after 238851 conflicts
c [score-dist-11] active 0 (0%), one 6051 (100%), zero 0 (0%)
c [score-dist-11] max exp 1, different 1 (50%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 177 variables 2.8% (6051 remain 20%)
c [simplification-11] removed 829 irredundant clauses 2.4% (33973 remain 38%)
c [simplification-11] maximum reduction of 3% = max (3%, 2%)
c [simplification-11] geometric conflict interval increment 14400 = 57600 / 4
c [simplification-11] new conflict interval 72000
c [simplification-11] penalized conflict interval 72000 = 1 * 72000
c [simplification-11] hard conflict limit 346851 (soft 310851 + delta 36000)
c [simplification-11] new conflict limit 310851 (hard 346851)
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 -   56.7    6051    33972    260013   60187   9430 12867    9    42   17  21%    746   -1   11    8  133%
c -   63.7    6051    33972    298331   62583   9470 12873   10    44   17  24%    869    4   13    8  153%
c 
c [simplification-12] limit 310851 conflicts (hard 346851) hit after 319669 conflicts
c [quatres-10] found 12990 quaternary clauses 23% in total
c [quatres-10-1] removed 12 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 77 single-self-subsuming ternary resolvents
c [quatres-10-2] added 136 quaternary resolvents
c [ternres-10] limit 16865445 with penalty 0 = 0 + 0
c [ternres-10] all 6051 free variables schedulable
c [ternres-10] 1190 ternary resolvents (60 bin, 1130 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-39] removed 13 variables
c [simpleprobe-5] all 6038 free variables schedulable
c [simpleprobe-5] limit 67461783 penalty 0 = 0 + 0
c [decomp-40] removed 14 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 14 variables, found 1895 hbrs, 0 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 748 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 6024 variables 100%
c [block-5] limit of 21081807 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 184 blocked clauses
c [block-5] 184 < 1/100 * 33901 = 339 considered unsuccessful
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 6004 variables 100%
c [elim-10] limit of 337308917 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 81 variables 1% in round 1 in 8810382 steps
c [elim-10-1] backward subsumption/strengthening limit 8810300
c [elim-10-1-1] backward checking 375 touched variables 6%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 0 and strengthened 2 clauses in 674328 steps
c [elim-10-1] rescheduled 8 variables 0% by backward subsumption
c [elim-10-2] eliminated 1 variables 0% in round 2 in 2378 steps
c [elim-10-2] backward subsumption/strengthening limit 2300
c [elim-10-2-1] backward checking 10 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 0 and strengthened 0 clauses in 2301 steps
c [elim-10-2] fully rescheduled 5922 variables 99%
c [elim-10-3] eliminated 19 variables 0% in round 3 in 8773076 steps
c [elim-10-3] backward subsumption/strengthening limit 8773000
c [elim-10-3-1] backward checking 101 touched variables 2%
c [elim-10-3-1] fully completed backward checking in 1 rounds
c [elim-10-3] subsumed 0 and strengthened 0 clauses in 598935 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 101 = 2% variables out of 6004 scheduled
c [bca-9] limit of 10000000 steps and 67360 added (scaled 2)
c [bca-9] 1582 out of 11808 literals actually usable 13%
c [bca-9] added 8 blocked clauses in 84631 steps
c [sweep-10] limit 5059633 penalty 0 = 0 + 0
c [sweep-10-1] 51 pos 49.0% + 53 neg 51.0% = 104 sched 1.8% ret 5799
c [sweep-10-1] 1675053 steps 63 queries 8.92 avg class size
c [sweep-10-1] 1384 decisions 55 SAT calls 58.44 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-41] removed 9 variables
c [sweep-10-1] removed 9 vars (0 failed, 11 eqs, 11 impls)
c [sweep-10-2] 2474 pos 42.0% + 3420 neg 58.0% = 5894 sched 100.0% ret 0
c [sweep-10-2] 3421873 steps 44 queries 293.61 avg class size
c [sweep-10-2] 1737 decisions 42 SAT calls 158.05 avg env size
c [sweep-10-2] 4753 variables remain 81% (1141 retained 19%)
c [decomp-42] removed 1 variables
c [sweep-10-2] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-10] removed 10 vars in TOTAL (2 rounds, 105 queries)
c [sort-queue-12] sorted 5893 enqueued variables after 319669 conflicts
c [score-dist-12] active 0 (0%), one 5893 (100%), zero 0 (0%)
c [score-dist-12] max exp 1, different 1 (50%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 158 variables 2.6% (5893 remain 19%)
c [simplification-12] removed 681 irredundant clauses 2.0% (33291 remain 37%)
c [simplification-12] maximum reduction of 3% = max (3%, 2%)
c [simplification-12] geometric conflict interval increment 18000 = 72000 / 4
c [simplification-12] new conflict interval 90000
c [simplification-12] penalized conflict interval 90000 = 1 * 90000
c [simplification-12] hard conflict limit 454669 (soft 409669 + delta 45000)
c [simplification-12] new conflict limit 409669 (hard 454669)
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   69.7    5892    33291    329413   90829  10223 13006    7    26   18  27%    928  -12    9    8  115%
c -   72.7    5892    33291    340222   67616  10244 13010   10    39   18  26%  -1271    1   11    8  126%
c -   80.6    5892    33291    378824   69163  10266 13015   10    42   18  25%   -249    3   10    9  118%
c 
c [simplification-13] limit 409669 conflicts (hard 454669) hit after 411877 conflicts
c [quatres-11] found 13092 quaternary clauses 21% in total
c [quatres-11-1] removed 6 duplicate quaternary clauses
c [quatres-11-1] added 2 double-self-subsuming ternary resolvents
c [quatres-11-2] added 42 single-self-subsuming ternary resolvents
c [quatres-11-2] added 55 quaternary resolvents
c [ternres-11] limit 23229729 with penalty 0 = 0 + 0
c [ternres-11] all 5892 free variables schedulable
c [ternres-11] 336 ternary resolvents (33 bin, 303 trn)
c [ternres-11] 1 variables remain 0% (5891 retained 100%)
c [gauss-5] limit 1161486 penalty 2 = 2 + 0
c [gauss-5] extracted 2469 xors of average arity 3.0
c [gauss-5] connected 7389 occurrences of 647 variables (average 11.4)
c [gauss-5] limit 1161486 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-43] removed 3 variables
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 413 transitive binary clauses
c [transred-11] found 2 units
c [cce-6] limit of 14518581 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 6 clauses out of 119 (5%) of length 10
c [cce-6-1] eliminated 6 clauses out of 260 (2%) of length 9
c [cce-6-1] eliminated 12 clauses out of 435 (3%) of length 8
c [cce-6-1] eliminated 28 clauses out of 791 (4%) of length 7
c [cce-6-1] eliminated 81 clauses out of 1764 (5%) of length 6
c [cce-6-1] eliminated 156 clauses out of 2975 (5%) of length 5
c [cce-6-1] eliminated 28 clauses out of 6756 (0%) of length 4
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 317 large clauses in 14518597 steps
c [cce-6-1] allowing another 7259298 steps for small clauses
c [cce-6-1] scheduling 10537 clauses = 5851 binary + 4686 ternary
c [cce-6-1] tried to eliminate 3859 small clauses 37%
c [cce-6-1] eliminated 31 binary clauses 1%
c [cce-6-1] eliminated 60 ternary clauses 1%
c [cce-6-1] eliminated 91 small clauses 1%
c [cce-6-1] eliminated 96 small clauses in 14518585 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 413 covered clauses in round 1
c [cce-6] eliminated 413 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 5887 variables 100%
c [elim-11] limit of 464594592 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 61 variables 1% in round 1 in 8522397 steps
c [elim-11-1] backward subsumption/strengthening limit 8522300
c [elim-11-1-1] backward checking 408 touched variables 7%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 12 and strengthened 0 clauses in 719124 steps
c [elim-11-1] rescheduled 28 variables 0% by backward subsumption
c [elim-11-2] eliminated 11 variables 0% in round 2 in 236696 steps
c [elim-11-2] backward subsumption/strengthening limit 236600
c [elim-11-2-1] backward checking 41 touched variables 1%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 1 and strengthened 0 clauses in 48666 steps
c [elim-11-2] rescheduled 9 variables 0% by backward subsumption
c [elim-11-3] eliminated 3 variables 0% in round 3 in 95792 steps
c [elim-11-3] backward subsumption/strengthening limit 95700
c [elim-11-3-1] backward checking 3 touched variables 0%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 0 and strengthened 0 clauses in 21167 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 75 = 1% variables out of 5887 scheduled
c [bca-10] limit of 10000000 steps and 65958 added (scaled 2)
c [bca-10] 1598 out of 11626 literals actually usable 14%
c [bca-10] added 8 blocked clauses in 103991 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 69689180 penalty 0 = 0 + 0
c [sweep-11-1] 2000 pos 42.8% + 2675 neg 57.2% = 4675 sched 80.4% ret 1137
c [sweep-11-1] 19931249 steps 693 queries 25.36 avg class size
c [sweep-11-1] 13681 decisions 604 SAT calls 73.17 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-44] removed 186 variables
c [sweep-11-1] removed 186 vars (0 failed, 196 eqs, 202 impls)
c [sweep-11-2] 2369 pos 42.1% + 3257 neg 57.9% = 5626 sched 100.0% ret 0
c [sweep-11-2] 19787543 steps 577 queries 27.27 avg class size
c [sweep-11-2] 13466 decisions 546 SAT calls 72.90 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-45] removed 63 variables
c [sweep-11-2] removed 63 vars (0 failed, 75 eqs, 70 impls)
c [sweep-11-3] 2347 pos 42.2% + 3216 neg 57.8% = 5563 sched 100.0% ret 0
c [sweep-11-3] 20327920 steps 556 queries 33.83 avg class size
c [sweep-11-3] 12996 decisions 536 SAT calls 75.90 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-46] removed 36 variables
c [sweep-11-3] removed 36 vars (0 failed, 52 eqs, 29 impls)
c [sweep-11] removed 285 vars in TOTAL (3 rounds, 1823 queries)
c [sort-queue-13] sorted 5527 enqueued variables after 411877 conflicts
c [score-dist-13] active 0 (0%), one 5527 (100%), zero 0 (0%)
c [score-dist-13] max exp 1, different 1 (50%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 365 variables 6.2% (5527 remain 18%)
c [simplification-13] removed 895 irredundant clauses 2.7% (32396 remain 36%)
c [simplification-13] maximum reduction of 6% = max (6%, 3%)
c [simplification-13] large reduction 6% >= 5% limit
c [simplification-13] next conflict interval 4118 = min (411877/100, 90000)
c [simplification-13] penalized conflict interval 4118 = 1 * 4118
c [simplification-13] hard conflict limit 425995 (soft 415995 + delta 10000)
c [simplification-13] new conflict limit 415995 (hard 425995)
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   90.2    5526    32396    414368  105168   8576 12242   10    39   23  25%    284    1   10    9  119%
c -   91.0    5526    32396    416995   72906   8580 12242   10    40   13  25%   -879    2    9    9   99%
c 
c [simplification-14] limit 415995 conflicts (hard 425995) hit after 425996 conflicts
c [quatres-12] found 12915 quaternary clauses 21% in total
c [quatres-12-1] removed 48 duplicate quaternary clauses
c [quatres-12-2] added 66 single-self-subsuming ternary resolvents
c [quatres-12-2] added 187 quaternary resolvents
c [ternres-12] limit 24211163 with penalty 0 = 0 + 0
c [ternres-12] 1 schedulable variables 0%
c [ternres-12] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-47] removed 1 variables
c [treelook-5] limit 1210558 penalty 1 = 1 + 0 boost 1
c [treelook-5] scheduled 10268 literals 93%
c [treelook-5] scheduling used 380259 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 1210558 penalty 1 = 1 + 0 boost 1
c [treelook-5] used 1220737 steps
c [treelook-5] 10133 literals remain 92%
c [treelook-5] 4782 variables remain to probed next time 87%
c [decomp-48] removed 3 variables
c [treelook-5] removed 8 variables, found 2140 hbrs
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 755 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 5518 variables 100%
c [elim-12] limit of 484223273 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 53 variables 1% in round 1 in 8379437 steps
c [elim-12-1] backward subsumption/strengthening limit 8379400
c [elim-12-1-1] backward checking 307 touched variables 6%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 4 and strengthened 0 clauses in 598547 steps
c [elim-12-1] rescheduled 10 variables 0% by backward subsumption
c [elim-12-2] no variable eliminated in round 2 in 1404046 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 53 = 1% variables out of 5518 scheduled
c [elim-12] 53 < 1/100 * 5518 = 55 considered unsuccessful
c [bca-11] limit of 10000000 steps and 63882 added (scaled 2)
c [bca-11] 1504 out of 10932 literals actually usable 14%
c [bca-11] added 11 blocked clauses in 84076 steps
c [sweep-12] limit 7263349 penalty 0 = 0 + 0
c [sweep-12-1] 2220 pos 40.6% + 3245 neg 59.4% = 5465 sched 100.0% ret 0
c [sweep-12-1] 7268589 steps 230 queries 95.42 avg class size
c [sweep-12-1] 6132 decisions 230 SAT calls 70.16 avg env size
c [sweep-12-1] 1314 variables remain 24% (4151 retained 76%)
c [decomp-49] removed 13 variables
c [sweep-12-1] removed 13 vars (0 failed, 11 eqs, 5 impls)
c [sweep-12] removed 13 vars in TOTAL (1 rounds, 229 queries)
c [sort-queue-14] sorted 5452 enqueued variables after 425996 conflicts
c [score-dist-14] active 0 (0%), one 5452 (100%), zero 0 (0%)
c [score-dist-14] max exp 1, different 1 (50%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 74 variables 1.3% (5452 remain 18%)
c [simplification-14] removed 849 irredundant clauses 2.6% (31546 remain 35%)
c [simplification-14] maximum reduction of 3% = max (1%, 3%)
c [simplification-14] geometric conflict interval increment 22500 = 90000 / 4
c [simplification-14] new conflict interval 112500
c [simplification-14] penalized conflict interval 112500 = 1 * 112500
c [simplification-14] hard conflict limit 594746 (soft 538496 + delta 56250)
c [simplification-14] new conflict limit 538496 (hard 594746)
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 -   99.3    5452    31545    458246   76813   8273 12875   10    41   18  25%    -45    5   11    9  127%
c -  107.4    5452    31545    497981   78233   8309 12881   10    37   18  26%    441    1    8    9   92%
c 
c [simplification-15] limit 538496 conflicts (hard 594746) hit after 538497 conflicts
c [quatres-13] found 13036 quaternary clauses 19% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-1] added 9 double-self-subsuming ternary resolvents
c [quatres-13-2] added 57 single-self-subsuming ternary resolvents
c [quatres-13-2] added 61 quaternary resolvents
c [card-5] limit 997686 penalty 4 = 4 + 0
c [card-5] found 280 at-most-one constraints of average size 3.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 997686 for elimination
c [card-5] 280 out of 280 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-50] removed 1 variables
c [basicprobe-5] limit 159629898 penalty 0 = 0 + 0
c [basicprobe-5-0] 3226 sched 59%, 2 failed, 0 lifted, 493 hbrs
c [decomp-51] removed 3 variables
c [basicprobe-5-1] 3213 sched 59%, 0 failed, 0 lifted, 28 hbrs
c [basicprobe-5-2] 3213 sched 59%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-5-3] 3213 sched 59%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-5-4] 3213 sched 59%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-5-5] 3213 sched 59%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-5] fully completed probing
c [basicprobe-5-5] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-5-5] removed 3 variables, found 530 hbrs
c [bate-3] eliminated 8 asymmetric tautologies during probing
c [unhide-6] limit 798149 with penalty 3 = 3 + 0
c [unhide-6-6] 0 units, 0 failed, 2756 tauts, 0 hbrs, 69191 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 370 transitive binary clauses
c [cce-7] limit of 39907474 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 4 clauses out of 32 (12%) of length 13
c [cce-7-1] eliminated 2 clauses out of 78 (3%) of length 12
c [cce-7-1] eliminated 1 clauses out of 110 (1%) of length 10
c [cce-7-1] eliminated 6 clauses out of 238 (3%) of length 9
c [cce-7-1] eliminated 23 clauses out of 388 (6%) of length 8
c [cce-7-1] eliminated 71 clauses out of 793 (9%) of length 7
c [cce-7-1] eliminated 164 clauses out of 1648 (10%) of length 6
c [cce-7-1] eliminated 292 clauses out of 2759 (11%) of length 5
c [cce-7-1] eliminated 549 clauses out of 6542 (8%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 1112 large clauses in 28738020 steps
c [cce-7-1] allowing another 14369010 steps for small clauses
c [cce-7-1] scheduling 10124 clauses = 5462 binary + 4662 ternary
c [cce-7-1] tried to eliminate 10124 small clauses 100%
c [cce-7-1] eliminated 247 binary clauses 5%
c [cce-7-1] eliminated 321 ternary clauses 7%
c [cce-7-1] eliminated 568 small clauses 6%
c [cce-7-1] eliminated 568 small clauses in 32418181 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 1680 covered clauses in round 1
c [cce-7-2] eliminated 2 clauses out of 365 (1%) of length 8
c [cce-7-2] eliminated 5 clauses out of 722 (1%) of length 7
c [cce-7-2] incomplete large round (ACCE)
c [cce-7-2] eliminated 7 large clauses in 7489294 steps
c [cce-7-2] allowing another 3744647 steps for small clauses
c [cce-7-2] scheduling 9556 clauses = 5215 binary + 4341 ternary
c [cce-7-2] tried to eliminate 2284 small clauses 24%
c [cce-7-2] eliminated 1 ternary clauses 0%
c [cce-7-2] eliminated 1 small clauses 0%
c [cce-7-2] eliminated 1 small clauses in 7489299 steps
c [cce-7-2] incomplete small round (ACCE)
c [cce-7-2] eliminated 8 covered clauses in round 2
c [cce-7] eliminated 1688 covered clauses in TOTAL during 2 rounds
c [bca-12] limit of 10000000 steps and 60429 added (scaled 2)
c [bca-12] 1581 out of 10898 literals actually usable 15%
c [bca-12] added 2 blocked clauses in 118819 steps
c [sweep-13] limit 9577793 penalty 0 = 0 + 0
c [sweep-13-1] 609 pos 46.5% + 700 neg 53.5% = 1309 sched 24.0% ret 4139
c [sweep-13-1] 9606063 steps 309 queries 20.86 avg class size
c [sweep-13-1] 6300 decisions 307 SAT calls 64.83 avg env size
c [sweep-13-1] 87 variables remain 2% (5361 retained 98%)
c [decomp-56] removed 23 variables
c [sweep-13-1] removed 23 vars (0 failed, 28 eqs, 12 impls)
c [sweep-13] removed 23 vars in TOTAL (1 rounds, 308 queries)
c [sort-queue-15] sorted 5425 enqueued variables after 538497 conflicts
c [score-dist-15] active 0 (0%), one 5425 (100%), zero 0 (0%)
c [score-dist-15] max exp 1, different 1 (50%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 27 variables 0.5% (5425 remain 18%)
c [simplification-15] removed 1725 irredundant clauses 5.5% (29819 remain 33%)
c [simplification-15] maximum reduction of 5% = max (0%, 5%)
c [simplification-15] large reduction 5% >= 5% limit
c [simplification-15] next conflict interval 5384 = min (538497/100, 112500)
c [simplification-15] penalized conflict interval 5384 = 1 * 5384
c [simplification-15] hard conflict limit 553881 (soft 543881 + delta 10000)
c [simplification-15] new conflict limit 543881 (hard 553881)
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 -  118.7    5425    29819    539818   81512   8029 12150    8    42   14  20%    716    7    6    9   73%
c 
c [simplification-16] limit 543881 conflicts (hard 553881) hit after 553882 conflicts
c [quatres-14] found 12381 quaternary clauses 18% in total
c [quatres-14-1] removed 15 duplicate quaternary clauses
c [quatres-14-1] added 2 double-self-subsuming ternary resolvents
c [quatres-14-2] added 34 single-self-subsuming ternary resolvents
c [quatres-14-2] added 131 quaternary resolvents
c [ternres-13] limit 16518434 with penalty 1 = 1 + 0
c [ternres-13] all 5425 free variables schedulable
c [ternres-13] 1132 ternary resolvents (31 bin, 1101 trn)
c [ternres-13] fully completed ternary resolution
c [simpleprobe-6] all 5425 free variables schedulable
c [simpleprobe-6] limit 132147473 penalty 0 = 0 + 0
c [decomp-58] removed 7 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 7 variables, found 1283 hbrs, 0 units
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 802 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 825921710 steps penalty 1 = 1 + 0
c [cce-8-1] eliminated 2 clauses out of 355 (1%) of length 8
c [cce-8-1] eliminated 3 clauses out of 717 (0%) of length 7
c [cce-8-1] eliminated 16 clauses out of 1484 (1%) of length 6
c [cce-8-1] eliminated 24 clauses out of 2467 (1%) of length 5
c [cce-8-1] eliminated 28 clauses out of 5976 (0%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 73 large clauses in 16422276 steps
c [cce-8-1] allowing another 8211138 steps for small clauses
c [cce-8-1] scheduling 13856 clauses = 5196 binary + 8660 ternary
c [cce-8-1] tried to eliminate 13856 small clauses 100%
c [cce-8-1] eliminated 2 binary clauses 0%
c [cce-8-1] eliminated 222 ternary clauses 3%
c [cce-8-1] eliminated 224 small clauses 2%
c [cce-8-1] eliminated 224 small clauses in 24929309 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 297 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 8049810 steps for small clauses
c [cce-8-2] scheduling 13632 clauses = 5194 binary + 8438 ternary
c [cce-8-2] tried to eliminate 13632 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 297 covered clauses in TOTAL during 2 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 5418 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 303 variables 6% in round 1 in 7252202 steps
c [elim-13-1] backward subsumption/strengthening limit 7252200
c [elim-13-1-1] backward checking 1087 touched variables 20%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 11 clauses in 803344 steps
c [elim-13-1] rescheduled 29 variables 1% by backward subsumption
c [elim-13-2] eliminated 1 variables 0% in round 2 in 328550 steps
c [elim-13-2] backward subsumption/strengthening limit 328500
c [elim-13-2-1] backward checking 0 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 17991 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 304 = 6% variables out of 5418 scheduled
c [bca-13] limit of 10000000 steps and 58626 added (scaled 2)
c [bca-13] 1493 out of 10230 literals actually usable 15%
c [bca-13] added 13 blocked clauses in 94433 steps
c [sweep-14] limit 9911060 penalty 0 = 0 + 0
c [sweep-14-1] 36 pos 50.0% + 36 neg 50.0% = 72 sched 1.4% ret 5042
c [sweep-14-1] 573336 steps 47 queries 9.91 avg class size
c [sweep-14-1] 852 decisions 43 SAT calls 38.51 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-59] removed 3 variables
c [sweep-14-1] removed 3 vars (0 failed, 3 eqs, 4 impls)
c [sweep-14-2] 2061 pos 40.3% + 3050 neg 59.7% = 5111 sched 100.0% ret 0
c [sweep-14-2] 9337990 steps 220 queries 68.81 avg class size
c [sweep-14-2] 6842 decisions 221 SAT calls 74.87 avg env size
c [sweep-14-2] 1204 variables remain 24% (3905 retained 76%)
c [decomp-60] removed 11 variables
c [sweep-14-2] removed 11 vars (0 failed, 10 eqs, 5 impls)
c [sweep-14] removed 14 vars in TOTAL (2 rounds, 265 queries)
c [sort-queue-16] sorted 5100 enqueued variables after 553882 conflicts
c [score-dist-16] active 0 (0%), one 5100 (100%), zero 0 (0%)
c [score-dist-16] max exp 1, different 1 (50%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 325 variables 6.0% (5100 remain 17%)
c [simplification-16] removed 917 irredundant clauses 3.1% (28902 remain 32%)
c [simplification-16] maximum reduction of 6% = max (6%, 3%)
c [simplification-16] large reduction 6% >= 5% limit
c [simplification-16] next conflict interval 5538 = min (553882/100, 112500)
c [simplification-16] penalized conflict interval 5538 = 1 * 5538
c [simplification-16] hard conflict limit 569420 (soft 559420 + delta 10000)
c [simplification-16] new conflict limit 559420 (hard 569420)
c 
c [simplification-17] limit 559420 conflicts (hard 569420) hit after 559421 conflicts
c [quatres-15] found 12038 quaternary clauses 18% in total
c [quatres-15-1] removed 6 duplicate quaternary clauses
c [quatres-15-1] added 3 double-self-subsuming ternary resolvents
c [quatres-15-2] added 17 single-self-subsuming ternary resolvents
c [quatres-15-2] added 81 quaternary resolvents
c [ternres-14] limit 33418883 with penalty 0 = 0 + 0
c [ternres-14] all 5100 free variables schedulable
c [ternres-14] 189 ternary resolvents (17 bin, 172 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-6] limit 835472 penalty 3 = 3 + 0
c [gauss-6] extracted 1843 xors of average arity 3.0
c [gauss-6] connected 5529 occurrences of 549 variables (average 10.1)
c [gauss-6] limit 835472 penalty 3 = 3 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-6] limit 3341888 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 9495 literals 93%
c [treelook-6] scheduling used 402859 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3341888 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 3345950 steps
c [treelook-6] 8542 literals remain 84%
c [treelook-6] 4396 variables remain to probed next time 86%
c [treelook-6] removed 1 variables, found 1623 hbrs
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 455 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 5099 variables 100%
c [block-6] limit of 20886802 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 8 blocked clauses
c [block-6] 8 < 1/100 * 28890 = 288 considered unsuccessful
c [cce-9] limit of 167094417 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 28 (4%) of length 13
c [cce-9-1] eliminated 2 clauses out of 87 (2%) of length 12
c [cce-9-1] eliminated 3 clauses out of 76 (4%) of length 11
c [cce-9-1] eliminated 3 clauses out of 122 (2%) of length 10
c [cce-9-1] eliminated 19 clauses out of 271 (7%) of length 9
c [cce-9-1] eliminated 34 clauses out of 424 (8%) of length 8
c [cce-9-1] eliminated 80 clauses out of 802 (10%) of length 7
c [cce-9-1] eliminated 69 clauses out of 1560 (4%) of length 6
c [cce-9-1] eliminated 87 clauses out of 2475 (4%) of length 5
c [cce-9-1] eliminated 92 clauses out of 5926 (2%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 390 large clauses in 27912287 steps
c [cce-9-1] allowing another 13956143 steps for small clauses
c [cce-9-1] scheduling 12824 clauses = 4893 binary + 7931 ternary
c [cce-9-1] tried to eliminate 12824 small clauses 100%
c [cce-9-1] eliminated 33 binary clauses 1%
c [cce-9-1] eliminated 90 ternary clauses 1%
c [cce-9-1] eliminated 123 small clauses 1%
c [cce-9-1] eliminated 123 small clauses in 33762692 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 513 covered clauses in round 1
c [cce-9-2] eliminated 1 clauses out of 2388 (0%) of length 5
c [cce-9-2] eliminated 1 clauses out of 5834 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 2 large clauses in 26116582 steps
c [cce-9-2] allowing another 13058291 steps for small clauses
c [cce-9-2] scheduling 12701 clauses = 4860 binary + 7841 ternary
c [cce-9-2] tried to eliminate 12701 small clauses 100%
c [cce-9-2] eliminated 1 ternary clauses 0%
c [cce-9-2] eliminated 1 small clauses 0%
c [cce-9-2] eliminated 1 small clauses in 32439182 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 3 covered clauses in round 2
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] allowing another 13020169 steps for small clauses
c [cce-9-3] scheduling 12700 clauses = 4860 binary + 7840 ternary
c [cce-9-3] tried to eliminate 12700 small clauses 100%
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 0 covered clauses in round 3
c [cce-9] eliminated 516 covered clauses in TOTAL during 3 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 5099 variables 100%
c [elim-14] limit of 668377671 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 67 variables 1% in round 1 in 6963134 steps
c [elim-14-1] backward subsumption/strengthening limit 6963100
c [elim-14-1-1] backward checking 411 touched variables 8%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 4 clauses in 587846 steps
c [elim-14-1] rescheduled 12 variables 0% by backward subsumption
c [elim-14-2] eliminated 1 variables 0% in round 2 in 172371 steps
c [elim-14-2] backward subsumption/strengthening limit 172300
c [elim-14-2-1] backward checking 13 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 0 and strengthened 1 clauses in 52778 steps
c [elim-14-2] rescheduled 9 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 135237 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 68 = 1% variables out of 5099 scheduled
c [bca-14] limit of 10000000 steps and 57319 added (scaled 2)
c [bca-14] 1458 out of 10064 literals actually usable 14%
c [bca-14] added 7 blocked clauses in 99182 steps
c [sweep-15] limit 10025665 penalty 0 = 0 + 0
c [sweep-15-1] 504 pos 42.5% + 681 neg 57.5% = 1185 sched 23.6% ret 3846
c [sweep-15-1] 8348823 steps 323 queries 14.38 avg class size
c [sweep-15-1] 6345 decisions 325 SAT calls 59.61 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-63] removed 14 variables
c [sweep-15-1] removed 14 vars (0 failed, 14 eqs, 8 impls)
c [sweep-15-2] 2076 pos 41.4% + 2941 neg 58.6% = 5017 sched 100.0% ret 0
c [sweep-15-2] 1691226 steps 39 queries 249.46 avg class size
c [sweep-15-2] 1167 decisions 38 SAT calls 115.47 avg env size
c [sweep-15-2] 4090 variables remain 82% (927 retained 18%)
c [sweep-15-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-15] removed 14 vars in TOTAL (2 rounds, 360 queries)
c [sort-queue-17] sorted 5017 enqueued variables after 559421 conflicts
c [score-dist-17] active 0 (0%), one 5017 (100%), zero 0 (0%)
c [score-dist-17] max exp 1, different 1 (50%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 83 variables 1.6% (5017 remain 16%)
c [simplification-17] removed 642 irredundant clauses 2.2% (28260 remain 31%)
c [simplification-17] maximum reduction of 2% = max (2%, 2%)
c [simplification-17] geometric conflict interval increment 37500 = 112500 / 3
c [simplification-17] new conflict interval 150000
c [simplification-17] penalized conflict interval 150000 = 1 * 150000
c [simplification-17] hard conflict limit 784421 (soft 709421 + delta 75000)
c [simplification-17] new conflict limit 709421 (hard 784421)
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 -  134.2    5017    28260    582973   83079   8444 11124   10    42   19  22%    865    6   12    9  131%
c -  142.0    5017    28260    622705   84471   8461 11126   10    41   20  24%    937    4   11    9  126%
c -  149.3    5017    28260    663635   86648   8486 11127    8    27   20  32%    977   -8   11    9  124%
c -  158.0    5017    28260    704193   87184   8501 11128   10    39   20  26%    999    4   12    9  134%
c 
c [simplification-18] limit 709421 conflicts (hard 784421) hit after 711023 conflicts
c [quatres-16] found 12036 quaternary clauses 17% in total
c [quatres-16-1] removed 4 duplicate quaternary clauses
c [quatres-16-1] added 2 double-self-subsuming ternary resolvents
c [quatres-16-2] added 29 single-self-subsuming ternary resolvents
c [quatres-16-2] added 56 quaternary resolvents
c [ternres-15] limit 44408860 with penalty 0 = 0 + 0
c [ternres-15] all 5017 free variables schedulable
c [ternres-15] 247 ternary resolvents (21 bin, 226 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-65] removed 2 variables
c [basicprobe-6] limit 222044301 penalty 0 = 0 + 0
c [basicprobe-6-0] 2955 sched 59%, 1 failed, 0 lifted, 361 hbrs
c [decomp-66] removed 2 variables
c [basicprobe-6-1] 2957 sched 59%, 0 failed, 0 lifted, 24 hbrs
c [basicprobe-6-2] 2956 sched 59%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-6-3] 2956 sched 59%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-3] fully completed probing
c [basicprobe-6-3] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-6-3] removed 2 variables, found 389 hbrs
c [bate-4] eliminated 1 asymmetric tautologies during probing
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 338 transitive binary clauses
c [cce-10] limit of 222044301 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 4 clauses out of 85 (5%) of length 11
c [cce-10-1] eliminated 4 clauses out of 126 (3%) of length 10
c [cce-10-1] eliminated 18 clauses out of 272 (7%) of length 9
c [cce-10-1] eliminated 12 clauses out of 396 (3%) of length 8
c [cce-10-1] eliminated 21 clauses out of 727 (3%) of length 7
c [cce-10-1] eliminated 24 clauses out of 1520 (2%) of length 6
c [cce-10-1] eliminated 29 clauses out of 2411 (1%) of length 5
c [cce-10-1] eliminated 24 clauses out of 5811 (0%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 136 large clauses in 16027329 steps
c [cce-10-1] allowing another 8013664 steps for small clauses
c [cce-10-1] scheduling 12529 clauses = 4794 binary + 7735 ternary
c [cce-10-1] tried to eliminate 12529 small clauses 100%
c [cce-10-1] eliminated 6 binary clauses 0%
c [cce-10-1] eliminated 19 ternary clauses 0%
c [cce-10-1] eliminated 25 small clauses 0%
c [cce-10-1] eliminated 25 small clauses in 22591056 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 161 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 7867072 steps for small clauses
c [cce-10-2] scheduling 12504 clauses = 4788 binary + 7716 ternary
c [cce-10-2] tried to eliminate 12504 small clauses 100%
c [cce-10-2] completed small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 161 covered clauses in TOTAL during 2 rounds
c [cce-10] 161 < 1/100 * 28240 = 282 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 5013 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 27 variables 1% in round 1 in 6812307 steps
c [elim-15-1] backward subsumption/strengthening limit 6812300
c [elim-15-1-1] backward checking 182 touched variables 4%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 5 clauses in 112378 steps
c [elim-15-1] rescheduled 9 variables 0% by backward subsumption
c [elim-15-2] no variable eliminated in round 2 in 5844 steps
c [elim-15] fully completed in 2 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 27 = 1% variables out of 5013 scheduled
c [elim-15] 27 < 1/100 * 5013 = 50 considered unsuccessful
c [bca-15] limit of 10000000 steps and 56798 added (scaled 2)
c [bca-15] 1449 out of 9974 literals actually usable 15%
c [bca-15] added 3 blocked clauses in 96808 steps
c [sweep-16] limit 13322658 penalty 0 = 0 + 0
c [sweep-16-1] 1666 pos 41.0% + 2397 neg 59.0% = 4063 sched 81.5% ret 923
c [sweep-16-1] 13942825 steps 357 queries 43.31 avg class size
c [sweep-16-1] 8876 decisions 361 SAT calls 62.71 avg env size
c [sweep-16-1] 319 variables remain 6% (4667 retained 94%)
c [decomp-69] removed 14 variables
c [sweep-16-1] removed 14 vars (0 failed, 15 eqs, 9 impls)
c [sweep-16] removed 14 vars in TOTAL (1 rounds, 356 queries)
c [sort-queue-18] sorted 4972 enqueued variables after 711023 conflicts
c [score-dist-18] active 0 (0%), one 4972 (100%), zero 0 (0%)
c [score-dist-18] max exp 1, different 1 (50%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 45 variables 0.9% (4972 remain 16%)
c [simplification-18] removed 268 irredundant clauses 0.9% (27992 remain 31%)
c [simplification-18] maximum reduction of 1% = max (1%, 1%)
c [simplification-18] geometric conflict interval increment 75000 = 150000 / 2
c [simplification-18] new conflict interval 225000
c [simplification-18] penalized conflict interval 225000 = 1 * 225000
c [simplification-18] hard conflict limit 1048523 (soft 936023 + delta 112500)
c [simplification-18] new conflict limit 936023 (hard 1048523)
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 -  167.6    4972    27991    746692   90835   8645 10701   10    45   20  21%   1011   12    8    9   81%
c -  179.2    4972    27991    791420   93295   8668 10702   11    36   20  30%   1017    3   12    9  126%
c -  188.1    4972    27991    835764   96763   8683 10702    9    31   20  28%   1021   -5    7    9   73%
c -  196.9    4972    27991    879940   99187   8697 10703   10    33   20  32%   1022   -7   12    9  129%
c i  205.8    4971    27991    923600  140763   8719 10709    9    34   31  28%   1023   -6    8    9   84%
c -  206.0    4971    27991    924112  101661   8719 10709   10    32   20  30%  -2100   -8   10    9  108%
c -  217.0    4971    27991    968001  101800   8737 10709   11    32   20  34%  -3082   -4   12   10  128%
c -  223.1    4971    27991   1018362  106409   8758 10710    9    92   21   9%   -880   54   10    9  105%
c 
c [simplification-19] limit 936023 conflicts (hard 1048523) hit after 1048525 conflicts
c [quatres-17] found 12283 quaternary clauses 15% in total
c [quatres-17-1] removed 12 duplicate quaternary clauses
c [quatres-17-1] added 4 double-self-subsuming ternary resolvents
c [quatres-17-2] added 51 single-self-subsuming ternary resolvents
c [quatres-17-2] added 107 quaternary resolvents
c [ternres-16] limit 71280600 with penalty 0 = 0 + 0
c [ternres-16] all 4971 free variables schedulable
c [ternres-16] 536 ternary resolvents (26 bin, 510 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-70] removed 6 variables
c [simpleprobe-7] all 4966 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-71] removed 5 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 5 variables, found 858 hbrs, 1 units
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 551 transitive binary clauses
c [bca-16] limit of 10000000 steps and 56568 added (scaled 2)
c [bca-16] 1417 out of 9924 literals actually usable 14%
c [bca-16] added 3 blocked clauses in 135455 steps
c [sweep-17] limit 21384180 penalty 0 = 0 + 0
c [sweep-17-1] 141 pos 44.8% + 174 neg 55.2% = 315 sched 6.3% ret 4646
c [sweep-17-1] 3337747 steps 143 queries 11.58 avg class size
c [sweep-17-1] 2488 decisions 136 SAT calls 59.63 avg env size
c [sweep-17-1] fully completed sweeping round
c [decomp-72] removed 7 variables
c [sweep-17-1] removed 7 vars (0 failed, 8 eqs, 10 impls)
c [sweep-17-2] 1977 pos 39.9% + 2977 neg 60.1% = 4954 sched 100.0% ret 0
c [sweep-17-2] 18961024 steps 372 queries 31.32 avg class size
c [sweep-17-2] 9575 decisions 382 SAT calls 69.05 avg env size
c [sweep-17-2] 301 variables remain 6% (4652 retained 94%)
c [decomp-73] removed 22 variables
c [sweep-17-2] removed 22 vars (0 failed, 22 eqs, 7 impls)
c [sweep-17] removed 29 vars in TOTAL (2 rounds, 513 queries)
c [sort-queue-19] sorted 4932 enqueued variables after 1048525 conflicts
c [score-dist-19] active 0 (0%), one 4932 (100%), zero 0 (0%)
c [score-dist-19] max exp 1, different 1 (50%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 39 variables 0.8% (4932 remain 16%)
c [simplification-19] removed 118 irredundant clauses 0.4% (27873 remain 31%)
c [simplification-19] maximum reduction of 1% = max (1%, 0%)
c [simplification-19] geometric conflict interval increment 112500 = 225000 / 2
c [simplification-19] new conflict interval 337500
c [simplification-19] penalized conflict interval 337500 = 1 * 337500
c [simplification-19] hard conflict limit 1554775 (soft 1386025 + delta 168750)
c [simplification-19] new conflict limit 1386025 (hard 1554775)
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 -  235.0    4932    27873   1062871  103836   9086 10527   11    37   23  30%     59  -14   11    9  121%
c i  235.1    4931    27873   1063573  104490   9086 10527   11    34   28  32%     69  -17   11    9  119%
c -  245.0    4931    27873   1111497  107495   9092 10528    9    32   24  29%   -505   -8   13    9  134%
c -  256.4    4931    27873   1160392  110642   9101 10528   10    36   24  29%    299   -2   11    9  121%
c i  265.2    4930    27872   1209994  151715   9171 10542    7     8   37  89%    684  -23    5    9   56%
c -  266.1    3580    27872   1212563  111222   9172 10542    8    21   25  38%  -1349   -9    8    9   86%
c i  266.2    3579    27872   1213978  112562   9178 10544    8    19   30  40%  -1436  -11    6    9   66%
c i  273.8    3578    27872   1248984  145666   9188 10551   10    27   36  36%   -483   -3   11    9  120%
c -  279.7    3578    27872   1261626  112362   9195 10554   12    36   25  32%   -676    5   11   10  115%
c -  291.1    3578    27872   1312571  117046   9209 10557   10    33   25  32%    242   -2    7   10   77%
c -  304.7    3578    27872   1362240  117409   9228 10559   12    34   25  34%    658   -0   11   10  107%
c 
c [simplification-20] limit 1386025 conflicts (hard 1554775) hit after 1386025 conflicts
c [quatres-18] found 7582 quaternary clauses 11% in total
c [quatres-18-1] removed 12 duplicate quaternary clauses
c [quatres-18-1] added 3 double-self-subsuming ternary resolvents
c [quatres-18-2] added 48 single-self-subsuming ternary resolvents
c [quatres-18-2] added 270 quaternary resolvents
c [ternres-17] limit 101273340 with penalty 0 = 0 + 0
c [ternres-17] all 3578 free variables schedulable
c [ternres-17] 239 ternary resolvents (18 bin, 221 trn)
c [ternres-17] fully completed ternary resolution
c [decomp-74] removed 1883 variables
c [treelook-7] limit 10127334 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 5537 literals 91%
c [treelook-7] scheduling used 430856 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 10127334 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 6471790 steps
c [treelook-7] fully completed tree based probing
c [decomp-75] removed 82 variables
c [treelook-7] removed 112 variables, found 8834 hbrs
c [unhide-7] limit 1250000 with penalty 4 = 4 + 0
c [unhide-7-7] 0 units, 0 failed, 832 tauts, 0 hbrs, 68469 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 916 transitive binary clauses
c [cce-11] limit of 253183352 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 14
c [cce-11-1] eliminated 2 clauses out of 4 (50%) of length 13
c [cce-11-1] eliminated 6 clauses out of 25 (24%) of length 12
c [cce-11-1] eliminated 17 clauses out of 25 (68%) of length 11
c [cce-11-1] eliminated 11 clauses out of 38 (29%) of length 10
c [cce-11-1] eliminated 26 clauses out of 66 (39%) of length 9
c [cce-11-1] eliminated 35 clauses out of 85 (41%) of length 8
c [cce-11-1] eliminated 51 clauses out of 169 (30%) of length 7
c [cce-11-1] eliminated 101 clauses out of 432 (23%) of length 6
c [cce-11-1] eliminated 290 clauses out of 1141 (25%) of length 5
c [cce-11-1] eliminated 430 clauses out of 3605 (12%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 970 large clauses in 9245654 steps
c [cce-11-1] allowing another 4622827 steps for small clauses
c [cce-11-1] scheduling 5646 clauses = 2795 binary + 2851 ternary
c [cce-11-1] tried to eliminate 5646 small clauses 100%
c [cce-11-1] eliminated 388 binary clauses 14%
c [cce-11-1] eliminated 320 ternary clauses 11%
c [cce-11-1] eliminated 708 small clauses 13%
c [cce-11-1] eliminated 708 small clauses in 10283108 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 1678 covered clauses in round 1
c [cce-11-2] eliminated 1 clauses out of 50 (2%) of length 8
c [cce-11-2] eliminated 2 clauses out of 118 (2%) of length 7
c [cce-11-2] eliminated 3 clauses out of 331 (1%) of length 6
c [cce-11-2] eliminated 10 clauses out of 851 (1%) of length 5
c [cce-11-2] eliminated 56 clauses out of 3175 (2%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 72 large clauses in 7595234 steps
c [cce-11-2] allowing another 3797617 steps for small clauses
c [cce-11-2] scheduling 4940 clauses = 2407 binary + 2533 ternary
c [cce-11-2] tried to eliminate 4940 small clauses 100%
c [cce-11-2] eliminated 39 binary clauses 2%
c [cce-11-2] eliminated 41 ternary clauses 2%
c [cce-11-2] eliminated 80 small clauses 2%
c [cce-11-2] eliminated 80 small clauses in 8505930 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 152 covered clauses in round 2
c [cce-11-3] eliminated 1 clauses out of 49 (2%) of length 8
c [cce-11-3] eliminated 3 clauses out of 328 (1%) of length 6
c [cce-11-3] eliminated 2 clauses out of 841 (0%) of length 5
c [cce-11-3] eliminated 38 clauses out of 3119 (1%) of length 4
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] eliminated 44 large clauses in 7480773 steps
c [cce-11-3] allowing another 3740386 steps for small clauses
c [cce-11-3] scheduling 4860 clauses = 2368 binary + 2492 ternary
c [cce-11-3] tried to eliminate 4860 small clauses 100%
c [cce-11-3] eliminated 12 binary clauses 1%
c [cce-11-3] eliminated 8 ternary clauses 0%
c [cce-11-3] eliminated 20 small clauses 0%
c [cce-11-3] eliminated 20 small clauses in 8410633 steps
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 64 covered clauses in round 3
c [cce-11] eliminated 1894 covered clauses in TOTAL during 3 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 2937 variables 100%
c [elim-16] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 662 variables 23% in round 1 in 2073569 steps
c [elim-16-1] backward subsumption/strengthening limit 2073500
c [elim-16-1-1] backward checking 985 touched variables 34%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 3 and strengthened 12 clauses in 162477 steps
c [elim-16-1] rescheduled 38 variables 1% by backward subsumption
c [elim-16-2] eliminated 2 variables 0% in round 2 in 112301 steps
c [elim-16-2] backward subsumption/strengthening limit 112300
c [elim-16-2-1] backward checking 15 touched variables 1%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 0 and strengthened 5 clauses in 18375 steps
c [elim-16-2] rescheduled 7 variables 0% by backward subsumption
c [elim-16-3] eliminated 2 variables 0% in round 3 in 6077 steps
c [elim-16-3] backward subsumption/strengthening limit 6000
c [elim-16-3-1] backward checking 11 touched variables 0%
c [elim-16-3-1] incomplete backward checking 0 remain 0%
c [elim-16-3] subsumed 0 and strengthened 7 clauses in 6001 steps
c [elim-16] incomplete 12 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 666 = 23% variables out of 2937 scheduled
c [bca-17] limit of 10000000 steps and 26101 added (scaled 2)
c [bca-17] 410 out of 4544 literals actually usable 9%
c [bca-17] added 12 blocked clauses in 115517 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 31 pos 33.3% + 62 neg 66.7% = 93 sched 4.1% ret 2178
c [sweep-18-1] 3469668 steps 42 queries 6.88 avg class size
c [sweep-18-1] 1146 decisions 41 SAT calls 92.24 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-76] removed 4 variables
c [sweep-18-1] removed 4 vars (0 failed, 4 eqs, 2 impls)
c [sweep-18-2] 896 pos 39.5% + 1371 neg 60.5% = 2267 sched 100.0% ret 0
c [sweep-18-2] 16100723 steps 201 queries 21.19 avg class size
c [sweep-18-2] 6663 decisions 205 SAT calls 105.64 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-77] removed 13 variables
c [sweep-18-2] removed 13 vars (0 failed, 14 eqs, 5 impls)
c [sweep-18-3] 891 pos 39.5% + 1363 neg 60.5% = 2254 sched 100.0% ret 0
c [sweep-18-3] 18638912 steps 197 queries 23.64 avg class size
c [sweep-18-3] 6790 decisions 206 SAT calls 115.52 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-78] removed 17 variables
c [sweep-18-3] removed 17 vars (0 failed, 18 eqs, 9 impls)
c [sweep-18] removed 34 vars in TOTAL (3 rounds, 437 queries)
c [sort-queue-20] sorted 2237 enqueued variables after 1386025 conflicts
c [score-dist-20] active 0 (0%), one 2237 (100%), zero 0 (0%)
c [score-dist-20] max exp 1, different 1 (50%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 1341 variables 37.5% (2237 remain 7%)
c [simplification-20] removed 15227 irredundant clauses 54.6% (12645 remain 14%)
c [simplification-20] maximum reduction of 55% = max (37%, 55%)
c [simplification-20] large reduction 55% >= 5% limit
c [simplification-20] next conflict interval 13860 = min (1386025/100, 337500)
c [simplification-20] penalized conflict interval 13860 = 1 * 13860
c [simplification-20] hard conflict limit 1409885 (soft 1399885 + delta 10000)
c [simplification-20] new conflict limit 1399885 (hard 1409885)
c 
c [simplification-21] limit 1399885 conflicts (hard 1409885) hit after 1399886 conflicts
c [quatres-19] found 8114 quaternary clauses 11% in total
c [quatres-19-1] removed 71 duplicate quaternary clauses
c [quatres-19-1] added 3 double-self-subsuming ternary resolvents
c [quatres-19-2] added 69 single-self-subsuming ternary resolvents
c [quatres-19-2] added 153 quaternary resolvents
c [ternres-18] limit 102378044 with penalty 0 = 0 + 0
c [ternres-18] all 2237 free variables schedulable
c [ternres-18] 905 ternary resolvents (14 bin, 891 trn)
c [ternres-18] fully completed ternary resolution
c [card-6] limit 3199313 penalty 4 = 4 + 0
c [card-6] found 281 at-most-one constraints of average size 3.0
c [card-6] found 60 at-most-two constraints of average size 4.0
c [card-6] using previous limit 3199313 for elimination
c [card-6] 340 out of 341 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-79] removed 2 variables
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 1197 sched 54%, 3 failed, 0 lifted, 295 hbrs
c [decomp-80] removed 3 variables
c [basicprobe-7-1] 1200 sched 54%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-7-2] 1200 sched 54%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-7-2] fully completed probing
c [basicprobe-7-2] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-7-2] removed 3 variables, found 309 hbrs
c [bate-5] eliminated 40 asymmetric tautologies during probing
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 396 transitive binary clauses
c [cce-12] limit of 511890220 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 28 (4%) of length 11
c [cce-12-1] eliminated 4 clauses out of 28 (14%) of length 10
c [cce-12-1] eliminated 8 clauses out of 62 (13%) of length 9
c [cce-12-1] eliminated 10 clauses out of 83 (12%) of length 8
c [cce-12-1] eliminated 3 clauses out of 179 (2%) of length 7
c [cce-12-1] eliminated 22 clauses out of 392 (6%) of length 6
c [cce-12-1] eliminated 88 clauses out of 943 (9%) of length 5
c [cce-12-1] eliminated 82 clauses out of 2978 (3%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 218 large clauses in 4084792 steps
c [cce-12-1] allowing another 2042396 steps for small clauses
c [cce-12-1] scheduling 4047 clauses = 1849 binary + 2198 ternary
c [cce-12-1] tried to eliminate 4047 small clauses 100%
c [cce-12-1] eliminated 10 binary clauses 1%
c [cce-12-1] eliminated 16 ternary clauses 1%
c [cce-12-1] eliminated 26 small clauses 1%
c [cce-12-1] eliminated 26 small clauses in 4509182 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 244 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 1905670 steps for small clauses
c [cce-12-2] scheduling 4022 clauses = 1839 binary + 2183 ternary
c [cce-12-2] tried to eliminate 4022 small clauses 100%
c [cce-12-2] eliminated 1 ternary clauses 0%
c [cce-12-2] eliminated 1 small clauses 0%
c [cce-12-2] eliminated 1 small clauses in 4357387 steps
c [cce-12-2] completed small round (ATE)
c [cce-12-2] eliminated 1 covered clauses in round 2
c [cce-12-3] completed large round (ATE)
c [cce-12-3] allowing another 1905471 steps for small clauses
c [cce-12-3] scheduling 4021 clauses = 1839 binary + 2182 ternary
c [cce-12-3] tried to eliminate 4021 small clauses 100%
c [cce-12-3] completed small round (ATE)
c [cce-12-3] eliminated 0 covered clauses in round 3
c [cce-12] eliminated 245 covered clauses in TOTAL during 3 rounds
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 2232 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 55 variables 2% in round 1 in 1805554 steps
c [elim-17-1] backward subsumption/strengthening limit 1805500
c [elim-17-1-1] backward checking 262 touched variables 12%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 64015 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 55 = 2% variables out of 2232 scheduled
c [bca-18] limit of 10000000 steps and 24979 added (scaled 2)
c [bca-18] 320 out of 4356 literals actually usable 7%
c [bca-18] added 26 blocked clauses in 127314 steps
c [sweep-19] limit 30713413 penalty 0 = 0 + 0
c [sweep-19-1] 878 pos 40.3% + 1299 neg 59.7% = 2177 sched 100.0% ret 0
c [sweep-19-1] 18245822 steps 179 queries 21.05 avg class size
c [sweep-19-1] 6220 decisions 182 SAT calls 115.98 avg env size
c [sweep-19-1] fully completed sweeping round
c [decomp-82] removed 3 variables
c [sweep-19-1] removed 3 vars (0 failed, 4 eqs, 1 impls)
c [sweep-19-2] 876 pos 40.3% + 1298 neg 59.7% = 2174 sched 100.0% ret 0
c [sweep-19-2] 12511848 steps 107 queries 29.35 avg class size
c [sweep-19-2] 4264 decisions 106 SAT calls 153.54 avg env size
c [sweep-19-2] 241 variables remain 11% (1931 retained 89%)
c [decomp-83] removed 5 variables
c [sweep-19-2] removed 5 vars (0 failed, 1 eqs, 1 impls)
c [sweep-19] removed 8 vars in TOTAL (2 rounds, 284 queries)
c [sort-queue-21] sorted 2169 enqueued variables after 1399886 conflicts
c [score-dist-21] active 0 (0%), one 2169 (100%), zero 0 (0%)
c [score-dist-21] max exp 1, different 1 (50%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 68 variables 3.0% (2169 remain 7%)
c [simplification-21] removed 603 irredundant clauses 4.8% (12034 remain 13%)
c [simplification-21] maximum reduction of 5% = max (3%, 5%)
c [simplification-21] large reduction 5% >= 5% limit
c [simplification-21] next conflict interval 13998 = min (1399886/100, 337500)
c [simplification-21] penalized conflict interval 13998 = 1 * 13998
c [simplification-21] hard conflict limit 1423884 (soft 1413884 + delta 10000)
c [simplification-21] new conflict limit 1413884 (hard 1423884)
c 
c [simplification-22] limit 1413884 conflicts (hard 1423884) hit after 1413885 conflicts
c [quatres-20] found 7897 quaternary clauses 10% in total
c [quatres-20-1] removed 10 duplicate quaternary clauses
c [quatres-20-1] added 2 double-self-subsuming ternary resolvents
c [quatres-20-2] added 29 single-self-subsuming ternary resolvents
c [quatres-20-2] added 62 quaternary resolvents
c [ternres-19] limit 103480619 with penalty 0 = 0 + 0
c [ternres-19] all 2169 free variables schedulable
c [ternres-19] 203 ternary resolvents (10 bin, 193 trn)
c [ternres-19] fully completed ternary resolution
c [gauss-7] limit 1293507 penalty 4 = 4 + 0
c [gauss-7] extracted 1464 xors of average arity 3.0
c [gauss-7] connected 4396 occurrences of 329 variables (average 13.4)
c [gauss-7] limit 1293507 penalty 4 = 4 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 1 ternary equations
c [simpleprobe-8] all 2169 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-85] removed 2 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 2 variables, found 1966 hbrs, 0 units
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 651 transitive binary clauses
c [cce-13] boosting limit by 10
c [cce-13] limit of 5174030960 steps penalty 0 = 0 + 0
c [cce-13-1] eliminated 3 clauses out of 70 (4%) of length 8
c [cce-13-1] eliminated 3 clauses out of 192 (2%) of length 7
c [cce-13-1] eliminated 4 clauses out of 368 (1%) of length 6
c [cce-13-1] eliminated 17 clauses out of 888 (2%) of length 5
c [cce-13-1] eliminated 25 clauses out of 2888 (1%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 52 large clauses in 6117005 steps
c [cce-13-1] allowing another 3058502 steps for small clauses
c [cce-13-1] scheduling 3900 clauses = 1788 binary + 2112 ternary
c [cce-13-1] tried to eliminate 3900 small clauses 100%
c [cce-13-1] eliminated 17 binary clauses 1%
c [cce-13-1] eliminated 11 ternary clauses 1%
c [cce-13-1] eliminated 28 small clauses 1%
c [cce-13-1] eliminated 28 small clauses in 6032243 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 80 covered clauses in round 1
c [cce-13-2] eliminated 1 clauses out of 2863 (0%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 1 large clauses in 5945270 steps
c [cce-13-2] allowing another 2972635 steps for small clauses
c [cce-13-2] scheduling 3872 clauses = 1771 binary + 2101 ternary
c [cce-13-2] tried to eliminate 3872 small clauses 100%
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 1 covered clauses in round 2
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] allowing another 2975779 steps for small clauses
c [cce-13-3] scheduling 3872 clauses = 1771 binary + 2101 ternary
c [cce-13-3] tried to eliminate 3872 small clauses 100%
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 0 covered clauses in round 3
c [cce-13] eliminated 81 covered clauses in TOTAL during 3 rounds
c [cce-13] 81 < 1/100 * 12024 = 120 considered unsuccessful
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 2167 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 16000000000 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 16 variables 1% in round 1 in 1755493 steps
c [elim-18-1] backward subsumption/strengthening limit 1755400
c [elim-18-1-1] backward checking 161 touched variables 7%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 0 and strengthened 0 clauses in 38719 steps
c [elim-18] fully completed in 1 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 16 = 1% variables out of 2167 scheduled
c [elim-18] 16 < 1/100 * 2167 = 21 considered unsuccessful
c [bca-19] limit of 10000000 steps and 24626 added (scaled 2)
c [bca-19] 292 out of 4304 literals actually usable 7%
c [bca-19] added 2 blocked clauses in 142263 steps
c [sweep-20] limit 31044185 penalty 0 = 0 + 0
c [sweep-20-1] 97 pos 41.8% + 135 neg 58.2% = 232 sched 10.8% ret 1919
c [sweep-20-1] 7763852 steps 87 queries 10.55 avg class size
c [sweep-20-1] 3078 decisions 88 SAT calls 109.93 avg env size
c [sweep-20-1] fully completed sweeping round
c [decomp-86] removed 2 variables
c [sweep-20-1] removed 2 vars (0 failed, 2 eqs, 0 impls)
c [sweep-20-2] 894 pos 41.6% + 1255 neg 58.4% = 2149 sched 100.0% ret 0
c [sweep-20-2] 22506532 steps 174 queries 21.41 avg class size
c [sweep-20-2] 6939 decisions 178 SAT calls 139.99 avg env size
c [sweep-20-2] fully completed sweeping round
c [decomp-87] removed 10 variables
c [sweep-20-2] removed 10 vars (0 failed, 10 eqs, 4 impls)
c [sweep-20-3] 891 pos 41.7% + 1248 neg 58.3% = 2139 sched 100.0% ret 0
c [sweep-20-3] 1045449 steps 3 queries 822.67 avg class size
c [sweep-20-3] 143 decisions 2 SAT calls 258.00 avg env size
c [sweep-20-3] 2139 variables remain 100% (0 retained 0%)
c [sweep-20-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-20] removed 12 vars in TOTAL (3 rounds, 261 queries)
c [sort-queue-22] sorted 2139 enqueued variables after 1413885 conflicts
c [score-dist-22] active 0 (0%), one 2139 (100%), zero 0 (0%)
c [score-dist-22] max exp 1, different 1 (50%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 30 variables 1.4% (2139 remain 7%)
c [simplification-22] removed 125 irredundant clauses 1.0% (11909 remain 13%)
c [simplification-22] maximum reduction of 1% = max (1%, 1%)
c [simplification-22] geometric conflict interval increment 168750 = 337500 / 2
c [simplification-22] new conflict interval 506250
c [simplification-22] penalized conflict interval 506250 = 1 * 506250
c [simplification-22] hard conflict limit 2173260 (soft 1920135 + delta 253125)
c [simplification-22] new conflict limit 1920135 (hard 2173260)
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 -  325.6    2139    11908   1422941  106430   5897  7028   10    34   22  31%    879   -4   11   10  110%
c -  334.9    2139    11907   1472535  110238   5915  7028   11    40   23  27%    956    5   11   10  111%
c -  347.4    2139    11907   1521381  109494   5947  7030   10    42   23  24%    992   10    8   10   87%
c -  361.4    2139    11907   1574573  112029   5967  7032   10    39   25  27%   1010    5   12   10  119%
c -  372.5    2139    11907   1627769  116376   5979  7033   10    33   25  29%   1018   -3    9   10   95%
c -  386.0    2139    11907   1679055  116302   6003  7034   11    38   25  28%   1021    3   10   10  101%
c -  397.3    2139    11907   1732685  120034   6015  7037   10    25   25  39%   1023  -10   11   10  110%
c -  414.0    2139    11907   1786538  120640   6036  7039   11    32   25  33%   1023   -1    7   10   74%
c i  417.8    2138    11907   1804488  137723   6047  7039   10    35   33  30%   1024    1    7   10   69%
c -  428.3    2137    11907   1841180  123641   6060  7039   11    31   25  34%  -4013    0    9   10   92%
c -  441.5    2137    11907   1894951  125225   6085  7040   11    33   25  33%  -1194   -0   13   10  125%
c -  454.7    2137    11907   1949650  126979   6114  7045   10    32   25  31%     62   -0   11   10  104%
c 
c [simplification-23] limit 1920135 conflicts (hard 2173260) hit after 1949719 conflicts
c [quatres-21] found 8383 quaternary clauses 9% in total
c [quatres-21-1] removed 6 duplicate quaternary clauses
c [quatres-21-2] added 40 single-self-subsuming ternary resolvents
c [quatres-21-2] added 110 quaternary resolvents
c [ternres-20] limit 154625193 with penalty 0 = 0 + 0
c [ternres-20] all 2137 free variables schedulable
c [ternres-20] 410 ternary resolvents (17 bin, 393 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-89] removed 3 variables
c [treelook-8] limit 15462519 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 4272 literals 100%
c [treelook-8] scheduling used 431911 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 15462519 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 2324815 steps
c [treelook-8] fully completed tree based probing
c [decomp-90] removed 13 variables
c [treelook-8] removed 15 variables, found 798 hbrs
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 526 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 2121 variables 100%
c [block-7] limit of 50000000 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 1 blocked clauses
c [block-7] 1 < 1/100 * 11860 = 118 considered unsuccessful
c [bca-20] limit of 10000000 steps and 24527 added (scaled 2)
c [bca-20] 253 out of 4244 literals actually usable 6%
c [bca-20] added 4 blocked clauses in 127209 steps
c [sweep-21] limit 46387558 penalty 0 = 0 + 0
c [sweep-21-1] 831 pos 39.2% + 1290 neg 60.8% = 2121 sched 100.0% ret 0
c [sweep-21-1] 17495564 steps 191 queries 17.15 avg class size
c [sweep-21-1] 5985 decisions 188 SAT calls 116.53 avg env size
c [sweep-21-1] fully completed sweeping round
c [decomp-91] removed 20 variables
c [sweep-21-1] removed 20 vars (0 failed, 25 eqs, 19 impls)
c [sweep-21-2] 824 pos 39.2% + 1277 neg 60.8% = 2101 sched 100.0% ret 0
c [sweep-21-2] 19447970 steps 184 queries 18.15 avg class size
c [sweep-21-2] 6639 decisions 189 SAT calls 107.69 avg env size
c [sweep-21-2] fully completed sweeping round
c [decomp-92] removed 13 variables
c [sweep-21-2] removed 13 vars (0 failed, 18 eqs, 2 impls)
c [sweep-21-3] 816 pos 39.1% + 1272 neg 60.9% = 2088 sched 100.0% ret 0
c [sweep-21-3] 9988378 steps 52 queries 80.50 avg class size
c [sweep-21-3] 3003 decisions 52 SAT calls 152.44 avg env size
c [sweep-21-3] 698 variables remain 33% (1390 retained 67%)
c [decomp-93] removed 5 variables
c [sweep-21-3] removed 5 vars (0 failed, 6 eqs, 2 impls)
c [sweep-21] removed 38 vars in TOTAL (3 rounds, 424 queries)
c [sort-queue-23] sorted 2083 enqueued variables after 1949719 conflicts
c [score-dist-23] active 0 (0%), one 2083 (100%), zero 0 (0%)
c [score-dist-23] max exp 1, different 1 (50%)
c [score-dist-23] median active exp 0, avg 0.0
c [simplification-23] removed 54 variables 2.5% (2083 remain 7%)
c [simplification-23] removed 61 irredundant clauses 0.5% (11846 remain 13%)
c [simplification-23] maximum reduction of 3% = max (3%, 1%)
c [simplification-23] geometric conflict interval increment 126562 = 506250 / 4
c [simplification-23] new conflict interval 632812
c [simplification-23] penalized conflict interval 632812 = 1 * 632812
c [simplification-23] hard conflict limit 2898937 (soft 2582531 + delta 316406)
c [simplification-23] new conflict limit 2582531 (hard 2898937)
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 -  470.0    2083    11845   2003559  126962   6139  6998   11    36   23  29%    601    3    9   10   91%
c -  484.6    2083    11845   2059765  131110   6147  7000   10    30   27  33%    845   -1   12   10  119%
c -  499.7    2083    11845   2113967  130504   6160  7002    8    18   27  46%    946  -13    6   10   63%
c -  516.5    2083    11845   2172519  132227   6180  7004   11    29   27  36%    992   -0   12   10  123%
c -  533.0    2083    11845   2229831  133029   6198  7006   11    30   27  37%   1011    0   13   11  123%
c -  544.6    2083    11845   2288579  137453   6208  7008   10    29   28  35%   1019    1    9   10   89%
c -  559.5    2083    11845   2345059  137656   6218  7009   11    28   20  41%   1022   -1   11   11  108%
c i  577.8    2082    11845   2400297  189864   6225  7015   12    28   41  44%   1023    6   12   10  119%
c -  579.9    2082    11845   2404601  138898   6224  7017   12    31   29  37%  -7692    8   11   10  106%
c -  597.6    2082    11845   2463841  139290   6235  7017   11    32   29  33%  -2563    5   11   11  101%
c -  611.0    2082    11845   2523987  142869   6241  7017   12    31   30  39%   -409    2   12   11  115%
c 
c [simplification-24] limit 2582531 conflicts (hard 2898937) hit after 2582533 conflicts
c [quatres-22] found 8861 quaternary clauses 9% in total
c [quatres-22-1] removed 15 duplicate quaternary clauses
c [quatres-22-1] added 1 double-self-subsuming ternary resolvents
c [quatres-22-2] added 78 single-self-subsuming ternary resolvents
c [quatres-22-2] added 115 quaternary resolvents
c [ternres-21] limit 200000000 with penalty 0 = 0 + 0
c [ternres-21] all 2082 free variables schedulable
c [ternres-21] 687 ternary resolvents (13 bin, 674 trn)
c [ternres-21] fully completed ternary resolution
c [decomp-94] removed 3 variables
c [basicprobe-8] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 1097 sched 53%, 4 failed, 0 lifted, 208 hbrs
c [decomp-95] removed 4 variables
c [basicprobe-8-1] 1081 sched 52%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-8-2] 1081 sched 52%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-8-3] 1081 sched 52%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-8-4] 1081 sched 52%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-8-5] 1081 sched 52%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-8-5] fully completed probing
c [basicprobe-8-5] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-8-5] removed 4 variables, found 226 hbrs
c [bate-6] eliminated 7 asymmetric tautologies during probing
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 433 transitive binary clauses
c [cce-14] limit of 562576427 steps penalty 1 = 1 + 0
c [cce-14-1] eliminated 1 clauses out of 26 (4%) of length 11
c [cce-14-1] eliminated 2 clauses out of 28 (7%) of length 10
c [cce-14-1] eliminated 3 clauses out of 59 (5%) of length 9
c [cce-14-1] eliminated 2 clauses out of 61 (3%) of length 8
c [cce-14-1] eliminated 2 clauses out of 177 (1%) of length 7
c [cce-14-1] eliminated 9 clauses out of 360 (2%) of length 6
c [cce-14-1] eliminated 22 clauses out of 856 (3%) of length 5
c [cce-14-1] eliminated 74 clauses out of 2834 (3%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 115 large clauses in 3601699 steps
c [cce-14-1] allowing another 1800849 steps for small clauses
c [cce-14-1] scheduling 3864 clauses = 1731 binary + 2133 ternary
c [cce-14-1] tried to eliminate 3864 small clauses 100%
c [cce-14-1] eliminated 23 binary clauses 1%
c [cce-14-1] eliminated 29 ternary clauses 1%
c [cce-14-1] eliminated 52 small clauses 1%
c [cce-14-1] eliminated 52 small clauses in 3908614 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 167 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 1742353 steps for small clauses
c [cce-14-2] scheduling 3812 clauses = 1708 binary + 2104 ternary
c [cce-14-2] tried to eliminate 3812 small clauses 100%
c [cce-14-2] completed small round (ATE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 167 covered clauses in TOTAL during 2 rounds
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 2076 variables 100%
c [elim-19] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 50 variables 2% in round 1 in 1770744 steps
c [elim-19-1] backward subsumption/strengthening limit 1770700
c [elim-19-1-1] backward checking 296 touched variables 14%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 1 and strengthened 16 clauses in 77374 steps
c [elim-19-1] rescheduled 35 variables 2% by backward subsumption
c [elim-19-2] eliminated 2 variables 0% in round 2 in 21884 steps
c [elim-19-2] backward subsumption/strengthening limit 21800
c [elim-19-2-1] backward checking 25 touched variables 1%
c [elim-19-2-1] fully completed backward checking in 1 rounds
c [elim-19-2] subsumed 0 and strengthened 0 clauses in 9435 steps
c [elim-19] fully completed in 2 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 52 = 3% variables out of 2076 scheduled
c [bca-21] limit of 10000000 steps and 23617 added (scaled 2)
c [bca-21] 215 out of 4050 literals actually usable 5%
c [bca-21] added 1 blocked clauses in 182963 steps
c [sweep-22] limit 67509171 penalty 0 = 0 + 0
c [sweep-22-1] 273 pos 40.6% + 400 neg 59.4% = 673 sched 33.3% ret 1351
c [sweep-22-1] 22258259 steps 150 queries 9.77 avg class size
c [sweep-22-1] 4830 decisions 146 SAT calls 114.88 avg env size
c [sweep-22-1] fully completed sweeping round
c [decomp-100] removed 33 variables
c [sweep-22-1] removed 33 vars (0 failed, 37 eqs, 22 impls)
c [sweep-22-2] 791 pos 39.7% + 1200 neg 60.3% = 1991 sched 100.0% ret 0
c [sweep-22-2] 31443640 steps 199 queries 16.16 avg class size
c [sweep-22-2] 7013 decisions 197 SAT calls 139.48 avg env size
c [sweep-22-2] fully completed sweeping round
c [decomp-101] removed 33 variables
c [sweep-22-2] removed 33 vars (0 failed, 43 eqs, 18 impls)
c [sweep-22-3] 780 pos 39.8% + 1178 neg 60.2% = 1958 sched 100.0% ret 0
c [sweep-22-3] 15105911 steps 29 queries 110.83 avg class size
c [sweep-22-3] 2119 decisions 27 SAT calls 275.07 avg env size
c [sweep-22-3] 1062 variables remain 54% (896 retained 46%)
c [decomp-102] removed 2 variables
c [sweep-22-3] removed 2 vars (0 failed, 3 eqs, 0 impls)
c [sweep-22] removed 68 vars in TOTAL (3 rounds, 375 queries)
c [sort-queue-24] sorted 1956 enqueued variables after 2582533 conflicts
c [score-dist-24] active 0 (0%), one 1956 (100%), zero 0 (0%)
c [score-dist-24] max exp 1, different 1 (50%)
c [score-dist-24] median active exp 0, avg 0.0
c [simplification-24] removed 126 variables 6.1% (1956 remain 6%)
c [simplification-24] removed 484 irredundant clauses 4.1% (11361 remain 13%)
c [simplification-24] maximum reduction of 6% = max (6%, 4%)
c [simplification-24] large reduction 6% >= 5% limit
c [simplification-24] next conflict interval 25825 = min (2582533/100, 632812)
c [simplification-24] penalized conflict interval 25825 = 1 * 25825
c [simplification-24] hard conflict limit 2621270 (soft 2608358 + delta 12912)
c [simplification-24] new conflict limit 2608358 (hard 2621270)
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 -  638.1    1956    11361   2593657  137176   5968  5946   11    27   27  41%    529    3    9   10   86%
c 
c [simplification-25] limit 2608358 conflicts (hard 2621270) hit after 2608358 conflicts
c [quatres-23] found 8464 quaternary clauses 9% in total
c [quatres-23-1] removed 48 duplicate quaternary clauses
c [quatres-23-1] added 2 double-self-subsuming ternary resolvents
c [quatres-23-2] added 68 single-self-subsuming ternary resolvents
c [quatres-23-2] added 73 quaternary resolvents
c [ternres-22] limit 200000000 with penalty 0 = 0 + 0
c [ternres-22] all 1956 free variables schedulable
c [ternres-22] 517 ternary resolvents (22 bin, 495 trn)
c [ternres-22] fully completed ternary resolution
c [gauss-8] limit 5693472 penalty 3 = 3 + 0
c [gauss-8] extracted 1492 xors of average arity 3.0
c [gauss-8] connected 4442 occurrences of 314 variables (average 14.1)
c [gauss-8] limit 5693472 penalty 3 = 3 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-9] all 1956 free variables schedulable
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-104] removed 11 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 11 variables, found 1083 hbrs, 0 units
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 615 transitive binary clauses
c [cce-15] limit of 1138694586 steps penalty 0 = 0 + 0
c [cce-15-1] eliminated 1 clauses out of 58 (2%) of length 9
c [cce-15-1] eliminated 1 clauses out of 48 (2%) of length 8
c [cce-15-1] eliminated 7 clauses out of 167 (4%) of length 7
c [cce-15-1] eliminated 34 clauses out of 365 (9%) of length 6
c [cce-15-1] eliminated 78 clauses out of 850 (9%) of length 5
c [cce-15-1] eliminated 116 clauses out of 2708 (4%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 237 large clauses in 4809096 steps
c [cce-15-1] allowing another 2404548 steps for small clauses
c [cce-15-1] scheduling 4923 clauses = 1572 binary + 3351 ternary
c [cce-15-1] tried to eliminate 4923 small clauses 100%
c [cce-15-1] eliminated 46 binary clauses 3%
c [cce-15-1] eliminated 113 ternary clauses 3%
c [cce-15-1] eliminated 159 small clauses 3%
c [cce-15-1] eliminated 159 small clauses in 5642592 steps
c [cce-15-1] completed small round (ACCE)
c [cce-15-1] eliminated 396 covered clauses in round 1
c [cce-15-2] eliminated 2 clauses out of 160 (1%) of length 7
c [cce-15-2] eliminated 8 clauses out of 772 (1%) of length 5
c [cce-15-2] eliminated 10 clauses out of 2592 (0%) of length 4
c [cce-15-2] completed large round (ACCE)
c [cce-15-2] eliminated 20 large clauses in 4483239 steps
c [cce-15-2] allowing another 2241619 steps for small clauses
c [cce-15-2] scheduling 4764 clauses = 1526 binary + 3238 ternary
c [cce-15-2] tried to eliminate 4764 small clauses 100%
c [cce-15-2] eliminated 5 binary clauses 0%
c [cce-15-2] eliminated 5 ternary clauses 0%
c [cce-15-2] eliminated 10 small clauses 0%
c [cce-15-2] eliminated 10 small clauses in 5336451 steps
c [cce-15-2] completed small round (ACCE)
c [cce-15-2] eliminated 30 covered clauses in round 2
c [cce-15-3] eliminated 1 clauses out of 2582 (0%) of length 4
c [cce-15-3] completed large round (ACCE)
c [cce-15-3] eliminated 1 large clauses in 4480284 steps
c [cce-15-3] allowing another 2240142 steps for small clauses
c [cce-15-3] scheduling 4754 clauses = 1521 binary + 3233 ternary
c [cce-15-3] tried to eliminate 4754 small clauses 100%
c [cce-15-3] completed small round (ACCE)
c [cce-15-3] eliminated 1 covered clauses in round 3
c [cce-15] eliminated 427 covered clauses in TOTAL during 3 rounds
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 1945 variables 100%
c [elim-20] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 53 variables 3% in round 1 in 1689110 steps
c [elim-20-1] backward subsumption/strengthening limit 1689100
c [elim-20-1-1] backward checking 360 touched variables 19%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 1 and strengthened 8 clauses in 95669 steps
c [elim-20-1] rescheduled 30 variables 2% by backward subsumption
c [elim-20-2] eliminated 1 variables 0% in round 2 in 165619 steps
c [elim-20-2] backward subsumption/strengthening limit 165600
c [elim-20-2-1] backward checking 19 touched variables 1%
c [elim-20-2-1] fully completed backward checking in 1 rounds
c [elim-20-2] subsumed 0 and strengthened 0 clauses in 7061 steps
c [elim-20] fully completed in 2 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 54 = 3% variables out of 1945 scheduled
c [bca-22] limit of 10000000 steps and 21978 added (scaled 2)
c [bca-22] 206 out of 3784 literals actually usable 5%
c [bca-22] added 12 blocked clauses in 143958 steps
c [sweep-23] limit 68321675 penalty 0 = 0 + 0
c [sweep-23-1] 433 pos 42.2% + 592 neg 57.8% = 1025 sched 54.2% ret 866
c [sweep-23-1] 16281827 steps 140 queries 12.05 avg class size
c [sweep-23-1] 4004 decisions 143 SAT calls 95.64 avg env size
c [sweep-23-1] fully completed sweeping round
c [decomp-105] removed 8 variables
c [sweep-23-1] removed 8 vars (0 failed, 9 eqs, 3 impls)
c [sweep-23-2] 765 pos 40.6% + 1118 neg 59.4% = 1883 sched 100.0% ret 0
c [sweep-23-2] 30324888 steps 166 queries 23.47 avg class size
c [sweep-23-2] 6566 decisions 173 SAT calls 124.05 avg env size
c [sweep-23-2] fully completed sweeping round
c [decomp-106] removed 8 variables
c [sweep-23-2] removed 8 vars (0 failed, 9 eqs, 2 impls)
c [sweep-23-3] 763 pos 40.7% + 1112 neg 59.3% = 1875 sched 100.0% ret 0
c [sweep-23-3] 21794926 steps 114 queries 30.03 avg class size
c [sweep-23-3] 4258 decisions 112 SAT calls 120.62 avg env size
c [sweep-23-3] 168 variables remain 9% (1707 retained 91%)
c [decomp-107] removed 7 variables
c [sweep-23-3] removed 7 vars (0 failed, 8 eqs, 9 impls)
c [sweep-23] removed 23 vars in TOTAL (3 rounds, 417 queries)
c [sort-queue-25] sorted 1868 enqueued variables after 2608358 conflicts
c [score-dist-25] active 0 (0%), one 1868 (100%), zero 0 (0%)
c [score-dist-25] max exp 1, different 1 (50%)
c [score-dist-25] median active exp 0, avg 0.0
c [simplification-25] removed 88 variables 4.5% (1868 remain 6%)
c [simplification-25] removed 778 irredundant clauses 6.8% (10583 remain 12%)
c [simplification-25] maximum reduction of 7% = max (4%, 7%)
c [simplification-25] large reduction 7% >= 5% limit
c [simplification-25] next conflict interval 26083 = min (2608358/100, 632812)
c [simplification-25] penalized conflict interval 26083 = 1 * 26083
c [simplification-25] hard conflict limit 2647482 (soft 2634441 + delta 13041)
c [simplification-25] new conflict limit 2634441 (hard 2647482)
c 
c [simplification-26] limit 2634441 conflicts (hard 2647482) hit after 2634441 conflicts
c [quatres-24] found 7977 quaternary clauses 9% in total
c [quatres-24-1] removed 30 duplicate quaternary clauses
c [quatres-24-1] added 1 double-self-subsuming ternary resolvents
c [quatres-24-2] added 29 single-self-subsuming ternary resolvents
c [quatres-24-2] added 65 quaternary resolvents
c [ternres-23] limit 200000000 with penalty 0 = 0 + 0
c [ternres-23] all 1868 free variables schedulable
c [ternres-23] 190 ternary resolvents (12 bin, 178 trn)
c [ternres-23] fully completed ternary resolution
c [decomp-108] removed 1 variables
c [treelook-9] limit 23040425 penalty 0 = 0 + 0 boost 1
c [treelook-9] scheduled 3734 literals 100%
c [treelook-9] scheduling used 535498 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 23040425 penalty 0 = 0 + 0 boost 1
c [treelook-9] used 2031371 steps
c [treelook-9] fully completed tree based probing
c [treelook-9] removed 1 variables, found 275 hbrs
c [unhide-8] limit 1250000 with penalty 4 = 4 + 0
c [unhide-8-8] 0 units, 0 failed, 4720 tauts, 0 hbrs, 132377 literals
c [transred-24] limit 2000000 with penalty 0 = 0 + 0
c [transred-24] removed 333 transitive binary clauses
c [cce-16] limit of 1152021284 steps penalty 0 = 0 + 0
c [cce-16-1] eliminated 5 clauses out of 310 (2%) of length 6
c [cce-16-1] eliminated 15 clauses out of 824 (2%) of length 5
c [cce-16-1] eliminated 20 clauses out of 2525 (1%) of length 4
c [cce-16-1] completed large round (ATE)
c [cce-16-1] eliminated 40 large clauses in 3006497 steps
c [cce-16-1] allowing another 1503248 steps for small clauses
c [cce-16-1] scheduling 3451 clauses = 1488 binary + 1963 ternary
c [cce-16-1] tried to eliminate 3451 small clauses 100%
c [cce-16-1] eliminated 17 binary clauses 1%
c [cce-16-1] eliminated 27 ternary clauses 1%
c [cce-16-1] eliminated 44 small clauses 1%
c [cce-16-1] eliminated 44 small clauses in 3255345 steps
c [cce-16-1] completed small round (ATE)
c [cce-16-1] eliminated 84 covered clauses in round 1
c [cce-16-2] completed large round (ATE)
c [cce-16-2] allowing another 1479137 steps for small clauses
c [cce-16-2] scheduling 3408 clauses = 1471 binary + 1937 ternary
c [cce-16-2] tried to eliminate 3408 small clauses 100%
c [cce-16-2] eliminated 1 ternary clauses 0%
c [cce-16-2] eliminated 1 small clauses 0%
c [cce-16-2] eliminated 1 small clauses in 3204067 steps
c [cce-16-2] completed small round (ATE)
c [cce-16-2] eliminated 1 covered clauses in round 2
c [cce-16-3] completed large round (ATE)
c [cce-16-3] allowing another 1479469 steps for small clauses
c [cce-16-3] scheduling 3407 clauses = 1471 binary + 1936 ternary
c [cce-16-3] tried to eliminate 3407 small clauses 100%
c [cce-16-3] completed small round (ATE)
c [cce-16-3] eliminated 0 covered clauses in round 3
c [cce-16] eliminated 85 covered clauses in TOTAL during 3 rounds
c [cce-16] 85 < 1/100 * 10549 = 105 considered unsuccessful
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 1866 variables 100%
c [elim-21] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-21] rescheduling of touched variables disabled
c [elim-21-1] eliminated 21 variables 1% in round 1 in 1616586 steps
c [elim-21-1] backward subsumption/strengthening limit 1616500
c [elim-21-1-1] backward checking 151 touched variables 8%
c [elim-21-1-1] fully completed backward checking in 1 rounds
c [elim-21-1] subsumed 0 and strengthened 0 clauses in 40875 steps
c [elim-21] fully completed in 1 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 21 = 1% variables out of 1866 scheduled
c [bca-23] limit of 10000000 steps and 21556 added (scaled 2)
c [bca-23] 198 out of 3692 literals actually usable 5%
c [bca-23] added 5 blocked clauses in 161141 steps
c [sweep-24] limit 69121277 penalty 0 = 0 + 0
c [sweep-24-1] 62 pos 37.8% + 102 neg 62.2% = 164 sched 8.9% ret 1681
c [sweep-24-1] 10334497 steps 68 queries 7.87 avg class size
c [sweep-24-1] 2356 decisions 70 SAT calls 96.33 avg env size
c [sweep-24-1] fully completed sweeping round
c [decomp-110] removed 3 variables
c [sweep-24-1] removed 3 vars (0 failed, 3 eqs, 1 impls)
c [sweep-24-2] 746 pos 40.5% + 1096 neg 59.5% = 1842 sched 100.0% ret 0
c [sweep-24-2] 29970496 steps 176 queries 18.74 avg class size
c [sweep-24-2] 6386 decisions 183 SAT calls 108.25 avg env size
c [sweep-24-2] fully completed sweeping round
c [decomp-111] removed 15 variables
c [sweep-24-2] removed 15 vars (0 failed, 16 eqs, 4 impls)
c [sweep-24-3] 737 pos 40.3% + 1090 neg 59.7% = 1827 sched 100.0% ret 0
c [sweep-24-3] 28907603 steps 150 queries 18.96 avg class size
c [sweep-24-3] 6130 decisions 154 SAT calls 126.50 avg env size
c [sweep-24-3] 20 variables remain 1% (1807 retained 99%)
c [decomp-112] removed 4 variables
c [sweep-24-3] removed 4 vars (0 failed, 6 eqs, 0 impls)
c [sweep-24] removed 22 vars in TOTAL (3 rounds, 391 queries)
c [sort-queue-26] sorted 1823 enqueued variables after 2634441 conflicts
c [score-dist-26] active 0 (0%), one 1823 (100%), zero 0 (0%)
c [score-dist-26] max exp 1, different 1 (50%)
c [score-dist-26] median active exp 0, avg 0.0
c [simplification-26] removed 45 variables 2.4% (1823 remain 6%)
c [simplification-26] removed 222 irredundant clauses 2.1% (10361 remain 12%)
c [simplification-26] maximum reduction of 2% = max (2%, 2%)
c [simplification-26] geometric conflict interval increment 210937 = 632812 / 3
c [simplification-26] new conflict interval 843749
c [simplification-26] penalized conflict interval 843749 = 1 * 843749
c [simplification-26] hard conflict limit 3900064 (soft 3478190 + delta 421874)
c [simplification-26] new conflict limit 3478190 (hard 3900064)
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 -  662.6    1823    10361   2662419  131271   5744  4987    9    17   25  50%    851   -9    7   10   67%
c -  680.2    1823    10361   2725595  133049   5772  4990   11    27   26  40%    958    2   11   11  105%
c -  693.6    1823    10361   2789403  135913   5796  4996   10    16   27  62%    999   -8   10   10   98%
c i  697.9    1822    10361   2812271  157503   5800  4996   11    21   36  51%   1006   -0   13   10  125%
c i  699.7    1821    10361   2820234  164995   5806  4999   10    25   37  41%  -4780    3   10   10   99%
c i  702.7    1820    10361   2831675  175379   5827  5004    9    19   39  49%  -3959   -3    6   10   54%
c i  704.1    1819    10361   2835858  179310   5830  5007   10    18   39  53%  -3818   -4   12   10  120%
c -  710.1    1817    10361   2852590  137048   5847  5011   11    23   26  47%  -2781    1   11   10  104%
c i  716.8    1816    10361   2889847  171625   5871  5016   11    19   36  56%  -1131   -1   13   10  127%
c i  717.3    1815    10361   2890740  172472   5874  5021   11    20   36  57%  -1589   -1   13   10  128%
c -  725.6    1815    10361   2918824  138948   5890  5027   10    14   20  73%   -921   -5    9   10   92%
c i  730.7    1814    10361   2952435  162276   5964  5040    7     8   29  90%   -140   -8    5    9   52%
c i  730.7    1809    10361   2952438  162277   5964  5041    7     8   29  90%   -143   -8    5    9   51%
c i  732.6    1803    10361   2964259  172379   5968  5042    9    10   29  83%   -766   -4    8    9   87%
c i  734.9    1802    10361   2977224  181877   6011  5048    7     9   41  85%   -599   -5    5    9   57%
c i  735.5    1795    10361   2980698  184489   6030  5052    7     8   41  85%   -703   -5    6    9   70%
c i  736.0    1792    10361   2983141  186155   6067  5061    7     8   41  86%   -694   -5    5    9   56%
c i  736.2    1781    10361   2983985  186852   6069  5063    7     9   41  85%   -696   -5    7    9   78%
c i  736.3    1773    10361   2984364  187111   6079  5065    7     8   41  84%   -696   -5    5    9   61%
c 0  736.3    1747    10361   2984364  187111   6079  5065    7     8   41  84%   -696   -5    5    9   61%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 74 basic ate = 56 trn 76% + 18 lrg 24% in 6 updates
c bcas: 23 count, 641 added (125 skipped), 2129307 steps
c bkwd: tried 90186 clauses, 180186 lits, 2.00 lits/clause
c bkwd: checked 18588092 occs, 206.11 occs/clause, 103.16 occs/lit
c bkwd: subsumed 9 binary, 23 ternary, 49 large
c bkwd: strengthened 0 binary, 3 ternary (100% self), 274 large (0% self)
c blkd: 7 bces, 2299 removed, 1277272 resolutions, 3215369 steps
c blkd: 2112 blocking literals 3%, 73 pure
c bump: 3020042 bumped seen, 191238733 lits 63.3 on average
c card: 6 count, 0 units, 11 am1, 14105427 steps
c card: 22 rescheduled, 202 eliminated, 12360 resolved, 5799 subsumed
c card: 1465 at-most-one constraints found, average size 3.26
c card: 1465 at-most-one constraints used 100%, average size 3.26
c card: 92 at-most-two constraints found, average size 4.04
c card: 91 at-most-two constraints used 99%, average size 4.04
c cces: 16 cces, 8760 eliminated, 6966 ate 80%, 1794 abce 20%
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: 299662 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 175 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 112 decompositions, 2817 equivalent 9%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 9041560 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 21 elims, 24413 eliminated 79%, 284 pure 1%
c elms: 61 rounds, 2.9 rounds/bve
c elms: 22770 small 93%, 1286 large 5%
c elms: 51425 tried small, 22770 succeeded 44%, 28655 failed 56%
c elms: 2611 subsumed, 3103 strengthened, 511 blocked
c elms: 3467413 copies, 4658936 resolutions, 1823834 ipos
c elms: 1555369 subchks, 984899 strchks
c gaus: 8 extractions, 18996 extracted, 3.0 size, 4 max
c gaus: exported 0 units, 0 binary and 2 ternary equations
c gaus: 0 gc, 14943392 steps, 7471696 extr 50%, 869460 elim 6%
c glue: 9.6 orig avg, 9.6 real avg, 2.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 51628 = 12137 simple 24% + 34389 trn 67% + 5102 lrg 10%, 847 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3020042 clauses, 28.3 length
c lrnd: 85496607 lits = 123091610 orig - 37595003 removed 31%
c lrnd: 569767 uips 19%, 2238593 flips 74%
c mins: 2998378 mins 99%, 664 bin 0%, 21000 size 1%
c mins: 148131919 poisoned searches, 22749916 hits, 15% hit rate
c mins: 245343448 used twice searches, 11136353 hits, 5% hit rate
c move: moved 4900, 1562 bin 32%, 3338 trn 68%
c otfs: 10435 driving 29%, 25455 restarting 71%
c otfs: str 35890, 35459 red 99%, 431 irr 1%
c otfs: str 35890, 0 bin 0%, 775 trn 2%, 35115 lrg 98%
c otfs: sub 600, 534 red 89%, 66 irr 11%
c otfs: sub 600, 0 bin 0%, 78 trn 13%, 522 lrg 87%
c phas: 1 computed, 8137 set, 2231 pos (27%), 5906 neg (73%)
c prbs: 8 basic, 159058 probed, 91 failed, 3 lifted
c prbs: 9 simple, 132276 probed, 113 failed, 2000 eqs
c prbs: 9 treelook, 14839 probed, 34 failed, 0 lifted
c prom: 1031141 locked 14% out of 7560730 tried
c prps: 477720305 props, 51 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c quat: 24 count, 3676 quat, 1372 self1, 68 self2, 683 dup
c queu: 26 sorted, 9041560 next (115 steps 0.00)
c queu: 191402183 enq (0 steps 0.00), 191238733 deq 100%
c redc: 104138 clauses 16%, 661195 tried 22%, 10 sat 0%
c redc: 145071 lits 1%, 10608526 tried 9%, 10 sat 0%
c redc: 1273 times jump level reduced, 4.5 levels on average
c reds: 57 count, 52357.3 conflicts per reduce
c reds: 0 memlim 0%, 57 arith 100%
c reds: 2223139 collected 87%, 327583 retired 13%
c rmbd: 2555 removed, 2192 red 86%
c rsts: 82828 restarts 100%, 188 skipped 0%
c rsts: 188 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 26 count, 25 confs 96%, 0 vars 0%
c simp: 1 its 4%, 0 bin 0%, 0 trns 0%
c subl: 3020042 count (1322382 tried 0.4), 170277 sub out of 3012863 (5.7%)
c swps: 24 count, 44 rounds, 8434 queries (191.7/round)
c swps: 8262 sat calls, 788 unsat (5.6% success rate)
c swps: 220994 decisions 26.7, 46113 conflicts 5.6
c swps; 51.7 avg class size, 79.9 avg environment size
c swps: 0 failed, 720 impls, 952 equivs
c swp0: 2795 type 0 queries, 644 unsat (23.0%), 2608 sat (93.3%)
c swp1: 5639 type 1 queries, 2316 unsat (41.1%), 4874 sat (86.4%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 24123848 calls to obtain time
c tops: 1843 fixed 6%, 66 its, 45217.64 confs/it
c trds: 24 transitive reductions, 12200 removed, 31 failed
c trds: 205803 nodes, 223350 edges, 25025370 steps
c trim: 1144389 words, 4.4 MB
c trnr: 23 count, 701 bin, 18169 trn, 219181149 steps
c unhd: 8 count, 8 rounds, 9725080 steps
c unhd: 30 non-trivial sccs of average size 2.0
c unhd: 1 units, 1 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 11292 tauts, 173 bin 2%, 2591 trn 23%, 5310 lrg 47%
c unhd: 11292 tauts, 3218 stamp 28%, 10996 red 97%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 352932 str, 1 bin 0%, 406 trn 0%, 352525 lrg 100%, 351116 red 99%
c vars: 1750 remaining 6% and 29073 removed 94% out of 30823
c vars: 1843 fixed 6%, 24413 eliminated 79%, 2817 equivalent 9%
c vsts: 27587677431 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 58.9 search visits per propagation, 9035.0 per conflict
c wchs: 10856254768 pushed, 10183712 enlarged, 324 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3016539       2223139        327583     119208342      34103096       1940303
c 
c  0 0        280797   9    122961   6         0   0  84033077  70  19243684  56    832222  43     4.3
c  1 5        238634   8    174937   8     31853  10  14753066  12<  4806070  14<   274341  14<    1.0
c  2 6        906177  30<   709530  32     87245  27  15025177  13   6440831  19    487306  25     3.1
c  3 9       1096706  36    860143  39<   110514  34<  4437095   4   2916844   9    284846  15     5.9
c  4 14       415580  14    306603  14     73437  22    855555   1    629529   2     57880   3     2.2
c  5 21        67440   2     42814   2     20227   6     90290   0     58375   0      3323   0     0.5
c  6 30         9670   0      5373   0      3706   1     11822   0      6770   0       336   0     0.1
c  7 41         1299   0       667   0       519   0      1571   0       838   0        38   0     0.0
c  8 54          196   0       102   0        72   0       644   0       128   0        10   0     0.0
c  9 69           32   0         9   0        10   0        37   0        20   0         1   0     0.0
c 10 86            8   0         0   0         0   0         8   0         7   0         0   0     0.0
c 
c avg                  2.5           2.5           2.9           0.5           0.9           1.2
c std                  1.2           1.1           1.1           0.9           1.1           1.2
c 
c   21.279   3% sweep
c   17.907   2% cce
c    7.961   1% probe
c    7.808   1% bump
c    5.919   1% decide
c    5.058   1% elim
c 
c    8.189 < 1% rest (below)
c 
c    1.766   0% transred
c    1.651   0% quatres
c    1.448   0% unhide
c    1.368   0% ternres
c    0.894   0% bca
c    0.547   0% gauss
c    0.356   0% block
c    0.159   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.853   0% preprocessing     1%
c   61.991   8% inprocessing     99%
c ==================================
c   62.844   9% simplifying
c  673.438  91% search
c ==================================
c  736.283 100% all
c 
c       2984364 conflicts,        4053.3 confs/sec
c          3921 ternaries,         761.1 confs/ternary
c           608 binaries,         4908.5 confs/binary
c            66 iterations,      45217.6 confs/iteration
c 
c            57 reductions,          0.1 redus/sec,  52357.3 confs/reduction
c         82828 restarts,          112.5 rests/sec,     36.0 confs/restart
c       9041560 decisions,       12280.0 decis/sec,      3.0 decis/conflict
c     477720305 propagations,   648826.9 props/sec,     52.8 props/decision
c 
c 736.3 seconds, 60.0 MB
c launch: done
