c launch: /data/cnf/sc2014/app/6s16-opt.cnf.bz2
c host: atom09
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/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 --score=3
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 [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] SUM (--score=3)
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 1002 conflicts
c [decomp-3] removed 8 variables
c [simpleprobe-2] all 8129 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 2 variables
c [simpleprobe-2] 1653 variables remain 20% (6474 retained 80%)
c [simpleprobe-2] removed 2 variables, found 593 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 16254 literals 100%
c [treelook-1] scheduling used 189055 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 304007 steps
c [treelook-1] 16145 literals remain 99%
c [treelook-1] 8127 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 1818 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 3099 probes remain 38% after last round
c [basicprobe-1-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1 variables, found 3656 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 8126 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 1743 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 100 (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 2037 (9%) of length 6
c [cce-1-1] eliminated 285 clauses out of 3254 (9%) of length 5
c [cce-1-1] eliminated 425 clauses out of 8076 (5%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 1024 large clauses in 28408721 steps
c [cce-1-1] allowing another 14204360 steps for small clauses
c [cce-1-1] scheduling 13798 clauses = 8103 binary + 5695 ternary
c [cce-1-1] tried to eliminate 5193 small clauses 38%
c [cce-1-1] eliminated 38 binary clauses 0%
c [cce-1-1] eliminated 100 ternary clauses 2%
c [cce-1-1] eliminated 138 small clauses 1%
c [cce-1-1] eliminated 138 small clauses in 30000003 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1162 covered clauses in round 1
c [cce-1] eliminated 1162 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 8123 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 532 variables 7% in round 1 in 6399214 steps
c [elim-2-1] backward subsumption/strengthening limit 6399200
c [elim-2-1-1] backward checking 2861 touched variables 35%
c [elim-2-1-1] incomplete backward checking 2817 remain 98%
c [elim-2-1] subsumed 6 and strengthened 13 clauses in 6399308 steps
c [elim-2-1] rescheduled 70 variables 1% by backward subsumption
c [elim-2-2] eliminated 6 variables 0% in round 2 in 104594 steps
c [elim-2-2] backward subsumption/strengthening limit 104500
c [elim-2-2-1] backward checking 2827 touched variables 35%
c [elim-2-2-1] incomplete backward checking 2825 remain 100%
c [elim-2-2] subsumed 0 and strengthened 0 clauses in 104946 steps
c [elim-2-2] fully rescheduled 7585 variables 93%
c [elim-2-3] eliminated 22 variables 0% in round 3 in 6250378 steps
c [elim-2-3] backward subsumption/strengthening limit 741560
c [elim-2-3-1] backward checking 2846 touched variables 35%
c [elim-2-3-1] incomplete backward checking 2788 remain 98%
c [elim-2-3] subsumed 0 and strengthened 3 clauses in 742546 steps
c [elim-2] incomplete 8 not tried 0% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 560 = 7% variables out of 8123 scheduled
c [bca-1] limit of 10000000 steps and 81730 added (scaled 2)
c [bca-1] 13563 out of 15128 literals actually usable 90%
c [bca-1] added 533 blocked clauses in 37012 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3152 pos 41.7% + 4411 neg 58.3% = 7563 sched 100.0% ret 0
c [sweep-1-1] 1000007 steps 123 queries 233.98 avg class size
c [sweep-1-1] 1806 decisions 115 SAT calls 44.31 avg env size
c [sweep-1-1] 5577 variables remain 74% (1986 retained 26%)
c [decomp-6] removed 19 variables
c [sweep-1-1] removed 19 vars (0 failed, 7 eqs, 15 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 19 vars in TOTAL (1 rounds, 122 queries)
c [sort-queue-2] sorted 4955 enqueued variables after 1002 conflicts
c [score-dist-2] active 2589 (34%), one 0 (0%), zero 4955 (66%)
c [score-dist-2] max exp 520, different 18 (3%)
c [score-dist-2] median active exp 512, avg 511.6
c [simplification-2] removed 593 variables 7.3% (7544 remain 24%)
c [simplification-2] removed 3566 irredundant clauses 8.1% (40599 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 13002 (soft 3002 + delta 10000)
c [simplification-2] new conflict limit 3002 (hard 13002)
c 
c [simplification-3] limit 3002 conflicts (hard 13002) hit after 3002 conflicts
c [quatres-1] found 7861 quaternary clauses 49% in total
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 11 single-self-subsuming ternary resolvents
c [quatres-1-2] added 597 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 7544 free variables schedulable
c [ternres-1] 4082 ternary resolvents (45 bin, 4037 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 348 at-most-one constraints of average size 3.5
c [card-2] found 37 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 384 out of 385 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 12 at-most-one constraints, 10 used 83%
c [card-2] exported 11 binary clauses, 1.1 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 4376 xors of average arity 3.0
c [gauss-1] connected 13128 occurrences of 901 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 10 ternary equations
c [decomp-7] removed 10 variables
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 1 units, 0 failed, 804 tauts, 0 hbrs, 1972 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 36 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 7533 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 9 blocked clauses
c [block-2] 9 < 1/100 * 40551 = 405 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 1 clauses out of 123 (1%) of length 10
c [cce-2-1] eliminated 12 clauses out of 263 (5%) of length 9
c [cce-2-1] eliminated 24 clauses out of 456 (5%) of length 8
c [cce-2-1] eliminated 49 clauses out of 988 (5%) of length 7
c [cce-2-1] eliminated 100 clauses out of 2031 (5%) of length 6
c [cce-2-1] eliminated 116 clauses out of 3333 (3%) of length 5
c [cce-2-1] eliminated 332 clauses out of 7720 (4%) of length 4
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 636 large clauses in 30000005 steps
c [cce-2-1] allowing another 15000002 steps for small clauses
c [cce-2-1] scheduling 12935 clauses = 7412 binary + 5523 ternary
c [cce-2-1] tried to eliminate 6715 small clauses 52%
c [cce-2-1] eliminated 36 binary clauses 0%
c [cce-2-1] eliminated 103 ternary clauses 2%
c [cce-2-1] eliminated 139 small clauses 1%
c [cce-2-1] eliminated 139 small clauses in 30000000 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 775 covered clauses in round 1
c [cce-2] eliminated 775 covered clauses in TOTAL during 1 rounds
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 7533 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 74 variables 1% in round 1 in 7105054 steps
c [elim-3-1] backward subsumption/strengthening limit 7105000
c [elim-3-1-1] backward checking 545 touched variables 7%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 2 and strengthened 2 clauses in 1392893 steps
c [elim-3-1] rescheduled 21 variables 0% by backward subsumption
c [elim-3-2] no variable eliminated in round 2 in 19080 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 74 = 1% variables out of 7533 scheduled
c [elim-3] 74 < 1/100 * 7533 = 75 considered unsuccessful
c [bca-2] limit of 10000000 steps and 80056 added (scaled 2)
c [bca-2] 10145 out of 14920 literals actually usable 68%
c [bca-2] added 1 blocked clauses in 28336 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2286 pos 41.5% + 3225 neg 58.5% = 5511 sched 73.9% ret 1948
c [sweep-2-1] 1000900 steps 182 queries 303.60 avg class size
c [sweep-2-1] 2667 decisions 175 SAT calls 27.18 avg env size
c [sweep-2-1] 3590 variables remain 48% (3867 retained 52%)
c [decomp-8] removed 22 variables
c [sweep-2-1] removed 22 vars (0 failed, 14 eqs, 11 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 22 vars in TOTAL (1 rounds, 181 queries)
c [sort-queue-3] sorted 2439 enqueued variables after 3002 conflicts
c [score-dist-3] active 4998 (67%), one 0 (0%), zero 2439 (33%)
c [score-dist-3] max exp 523, different 22 (4%)
c [score-dist-3] median active exp 515, avg 514.4
c [simplification-3] removed 107 variables 1.4% (7437 remain 24%)
c [simplification-3] removed 973 irredundant clauses 2.4% (39624 remain 44%)
c [simplification-3] maximum reduction of 2% = max (1%, 2%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 6666
c [simplification-3] penalized conflict interval 6666 = 1 * 6666
c [simplification-3] hard conflict limit 19668 (soft 9668 + delta 10000)
c [simplification-3] new conflict limit 9668 (hard 19668)
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    4.4    7436    39624      5877    5207   4565  6502   10   120    8   8%     73  115   14    1 1329%
c i    4.5    7435    39624      6974    6062   4594  6516   10   131    8   8%     29  123   10    1  800%
c i    4.6    7434    39624      7072    6136   4596  6517   10   130    8   8%     26  122   10    1  860%
c i    4.6    7433    39624      7329    6330   4597  6517   10   127    8   8%     20  119    9    1  748%
c 
c [simplification-4] limit 9668 conflicts (hard 19668) hit after 9668 conflicts
c [quatres-2] found 8285 quaternary clauses 50% in total
c [quatres-2-1] added 3 double-self-subsuming ternary resolvents
c [quatres-2-2] added 17 single-self-subsuming ternary resolvents
c [quatres-2-2] added 253 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 7433 free variables schedulable
c [ternres-2] 953 ternary resolvents (41 bin, 912 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 4461 xors of average arity 3.0
c [gauss-2] connected 13355 occurrences of 878 variables (average 15.2)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 7 ternary equations
c [decomp-9] removed 17 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 11543 literals 78%
c [treelook-2] scheduling used 150004 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150531 steps
c [treelook-2] 11513 literals remain 78%
c [treelook-2] 6874 variables remain to probed next time 93%
c [treelook-2] removed 2 variables, found 212 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 3 failed, 88 tauts, 0 hbrs, 5126 literals
c [transred-2] limit 312335 with penalty 0 = 0 + 0
c [transred-2] removed 160 transitive binary clauses
c [transred-2] found 2 units
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 3 clauses out of 90 (3%) of length 11
c [cce-3-1] eliminated 2 clauses out of 263 (1%) of length 9
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 5 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3-1] scheduling 19431 clauses = 7244 binary + 12187 ternary
c [cce-3-1] tried to eliminate 3300 small clauses 17%
c [cce-3-1] eliminated 13 binary clauses 0%
c [cce-3-1] eliminated 97 ternary clauses 1%
c [cce-3-1] eliminated 110 small clauses 1%
c [cce-3-1] eliminated 118 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 123 covered clauses in round 1
c [cce-3] eliminated 123 covered clauses in TOTAL during 1 rounds
c [cce-3] 123 < 1/100 * 39550 = 395 considered unsuccessful
c [bca-3] limit of 10000000 steps and 79621 added (scaled 2)
c [bca-3] 7657 out of 14824 literals actually usable 52%
c [bca-3] added 0 blocked clauses in 26760 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1510 pos 42.3% + 2059 neg 57.7% = 3569 sched 48.2% ret 3842
c [sweep-3-1] 1002770 steps 114 queries 201.38 avg class size
c [sweep-3-1] 2592 decisions 108 SAT calls 41.68 avg env size
c [sweep-3-1] 2727 variables remain 37% (4681 retained 63%)
c [decomp-11] removed 16 variables
c [sweep-3-1] removed 16 vars (0 failed, 9 eqs, 12 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 16 vars in TOTAL (1 rounds, 113 queries)
c [sort-queue-4] sorted 920 enqueued variables after 9668 conflicts
c [score-dist-4] active 6475 (88%), one 0 (0%), zero 920 (12%)
c [score-dist-4] max exp 526, different 23 (4%)
c [score-dist-4] median active exp 518, avg 517.6
c [simplification-4] removed 38 variables 0.5% (7395 remain 24%)
c [simplification-4] removed 217 irredundant clauses 0.5% (39407 remain 44%)
c [simplification-4] maximum reduction of 1% = max (1%, 1%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 16666
c [simplification-4] penalized conflict interval 16666 = 1 * 16666
c [simplification-4] hard conflict limit 36334 (soft 26334 + delta 10000)
c [simplification-4] new conflict limit 26334 (hard 36334)
c 
c [simplification-5] limit 26334 conflicts (hard 36334) hit after 26336 conflicts
c [quatres-3] found 8570 quaternary clauses 50% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 2 double-self-subsuming ternary resolvents
c [quatres-3-2] added 12 single-self-subsuming ternary resolvents
c [quatres-3-2] added 117 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 7395 free variables schedulable
c [ternres-3] 229 ternary resolvents (21 bin, 208 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 4500 xors of average arity 3.0
c [gauss-3] connected 13496 occurrences of 859 variables (average 15.7)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 10 variables
c [basicprobe-2] limit 4811621 penalty 0 = 0 + 0
c [basicprobe-2-0] 2969 sched 40%, 36 failed, 6 lifted, 7468 hbrs
c [decomp-13] removed 72 variables
c [basicprobe-2-1] 2104 probes remain 29% after last round
c [basicprobe-2-1] 47 units = 41 failed (87%) + 6 lifted (13%)
c [basicprobe-2-1] removed 77 variables, found 8609 hbrs
c [bate-1] eliminated 10 asymmetric tautologies during probing
c [unhide-4] limit 192464 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 0 failed, 1147 tauts, 0 hbrs, 30376 literals
c [transred-3] limit 962324 with penalty 0 = 0 + 0
c [transred-3] removed 265 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 7308 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 116 blocked clauses
c [block-3] 116 < 1/100 * 39184 = 391 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 7293 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 200000000 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 76 variables 1% in round 1 in 7627498 steps
c [elim-4-1] backward subsumption/strengthening limit 7627400
c [elim-4-1-1] backward checking 600 touched variables 8%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 2 and strengthened 4 clauses in 3120889 steps
c [elim-4-1] rescheduled 15 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 21567 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 77 = 1% variables out of 7293 scheduled
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1187 pos 44.8% + 1462 neg 55.2% = 2649 sched 36.7% ret 4567
c [sweep-4-1] 1010712 steps 185 queries 132.41 avg class size
c [sweep-4-1] 3277 decisions 181 SAT calls 40.91 avg env size
c [sweep-4-1] 1578 variables remain 22% (5638 retained 78%)
c [decomp-14] removed 29 variables
c [sweep-4-1] removed 29 vars (0 failed, 17 eqs, 13 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 29 vars in TOTAL (1 rounds, 184 queries)
c [sort-queue-5] sorted 718 enqueued variables after 26336 conflicts
c [score-dist-5] active 6469 (90%), one 0 (0%), zero 718 (10%)
c [score-dist-5] max exp 529, different 26 (5%)
c [score-dist-5] median active exp 522, avg 520.5
c [simplification-5] removed 208 variables 2.8% (7187 remain 23%)
c [simplification-5] removed 631 irredundant clauses 1.6% (38776 remain 43%)
c [simplification-5] maximum reduction of 3% = max (3%, 2%)
c [simplification-5] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-5] new conflict interval 21666
c [simplification-5] penalized conflict interval 21666 = 1 * 21666
c [simplification-5] hard conflict limit 58835 (soft 48002 + delta 10833)
c [simplification-5] new conflict limit 48002 (hard 58835)
c 
c [simplification-6] limit 48002 conflicts (hard 58835) hit after 48003 conflicts
c [quatres-4] found 8757 quaternary clauses 49% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-1] added 3 double-self-subsuming ternary resolvents
c [quatres-4-2] added 15 single-self-subsuming ternary resolvents
c [quatres-4-2] added 79 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 7187 free variables schedulable
c [ternres-4] 252 ternary resolvents (16 bin, 236 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 212 at-most-one constraints of average size 3.4
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 212 out of 212 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-15] removed 3 variables
c [simpleprobe-3] 1448 schedulable variables 20%
c [simpleprobe-3] limit 7203102 penalty 0 = 0 + 0
c [decomp-16] removed 26 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 26 variables, found 1327 hbrs, 1 units
c [transred-4] limit 1800775 with penalty 0 = 0 + 0
c [transred-4] removed 764 transitive binary clauses
c [transred-4] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 150000000 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 3 clauses out of 283 (1%) of length 9
c [cce-4-1] eliminated 7 clauses out of 418 (2%) of length 8
c [cce-4-1] eliminated 8 clauses out of 949 (1%) of length 7
c [cce-4-1] eliminated 19 clauses out of 1906 (1%) of length 6
c [cce-4-1] eliminated 21 clauses out of 3252 (1%) of length 5
c [cce-4-1] eliminated 58 clauses out of 7363 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 116 large clauses in 30122649 steps
c [cce-4-1] allowing another 15061324 steps for small clauses
c [cce-4-1] scheduling 18739 clauses = 6993 binary + 11746 ternary
c [cce-4-1] tried to eliminate 18739 small clauses 100%
c [cce-4-1] eliminated 63 binary clauses 1%
c [cce-4-1] eliminated 403 ternary clauses 3%
c [cce-4-1] eliminated 466 small clauses 2%
c [cce-4-1] eliminated 468 small clauses in 47942251 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 584 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 14670738 steps for small clauses
c [cce-4-2] scheduling 18273 clauses = 6930 binary + 11343 ternary
c [cce-4-2] tried to eliminate 18273 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 584 covered clauses in TOTAL during 2 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 7157 variables 100%
c [elim-5] limit of 36015510 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 93 variables 1% in round 1 in 9877458 steps
c [elim-5-1] backward subsumption/strengthening limit 9877400
c [elim-5-1-1] backward checking 536 touched variables 7%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 832777 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 93 = 1% variables out of 7157 scheduled
c [bca-4] limit of 10000000 steps and 76623 added (scaled 2)
c [bca-4] 5405 out of 14130 literals actually usable 38%
c [bca-4] added 8 blocked clauses in 50111 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 656 pos 42.9% + 874 neg 57.1% = 1530 sched 21.7% ret 5534
c [sweep-5-1] 4444916 steps 515 queries 39.09 avg class size
c [sweep-5-1] 11044 decisions 499 SAT calls 42.04 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-17] removed 81 variables
c [sweep-5-1] removed 81 vars (0 failed, 81 eqs, 57 impls)
c [sweep-5-2] 2951 pos 42.3% + 4032 neg 57.7% = 6983 sched 100.0% ret 0
c [sweep-5-2] 5588906 steps 540 queries 62.27 avg class size
c [sweep-5-2] 12401 decisions 503 SAT calls 51.69 avg env size
c [sweep-5-2] 768 variables remain 11% (6213 retained 89%)
c [decomp-18] removed 72 variables
c [sweep-5-2] removed 72 vars (0 failed, 73 eqs, 76 impls)
c [sweep-5] removed 153 vars in TOTAL (2 rounds, 1053 queries)
c [sort-queue-6] sorted 434 enqueued variables after 48003 conflicts
c [score-dist-6] active 6477 (94%), one 0 (0%), zero 434 (6%)
c [score-dist-6] max exp 531, different 27 (5%)
c [score-dist-6] median active exp 523, avg 522.0
c [simplification-6] removed 276 variables 3.8% (6911 remain 22%)
c [simplification-6] removed 969 irredundant clauses 2.5% (37805 remain 42%)
c [simplification-6] maximum reduction of 4% = max (4%, 2%)
c [simplification-6] geometric conflict interval increment 4333 = 21666 / 5
c [simplification-6] new conflict interval 25999
c [simplification-6] penalized conflict interval 25999 = 1 * 25999
c [simplification-6] hard conflict limit 87001 (soft 74002 + delta 12999)
c [simplification-6] new conflict limit 74002 (hard 87001)
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 -   19.6    6911    37804     66416   26563   5280 11545   24   147   11  16%    600   64   19   16  120%
c 
c [simplification-7] limit 74002 conflicts (hard 87001) hit after 74003 conflicts
c [quatres-5] found 9096 quaternary clauses 48% in total
c [quatres-5-1] removed 9 duplicate quaternary clauses
c [quatres-5-1] added 5 double-self-subsuming ternary resolvents
c [quatres-5-2] added 59 single-self-subsuming ternary resolvents
c [quatres-5-2] added 83 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 6911 free variables schedulable
c [ternres-5] 919 ternary resolvents (59 bin, 860 trn)
c [ternres-5] 2 variables remain 0% (6909 retained 100%)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] extracted 3262 xors of average arity 3.0
c [gauss-4] connected 9729 occurrences of 824 variables (average 11.8)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-19] removed 6 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 13011 literals 94%
c [treelook-3] scheduling used 273824 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 303956 steps
c [treelook-3] 12930 literals remain 94%
c [treelook-3] 6374 variables remain to probed next time 92%
c [treelook-3] removed 5 variables, found 237 hbrs
c [unhide-5] limit 287934 with penalty 1 = 1 + 0
c [unhide-5-5] 1 units, 22 failed, 173 tauts, 0 hbrs, 27682 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 471 transitive binary clauses
c [transred-5] found 2 units
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 98 (1%) of length 11
c [cce-5-1] eliminated 2 clauses out of 301 (1%) of length 9
c [cce-5-1] eliminated 2 clauses out of 414 (0%) of length 8
c [cce-5-1] eliminated 5 clauses out of 917 (1%) of length 7
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 10 large clauses in 30000001 steps
c [cce-5-1] allowing another 15000000 steps for small clauses
c [cce-5-1] scheduling 17672 clauses = 6665 binary + 11007 ternary
c [cce-5-1] tried to eliminate 3955 small clauses 22%
c [cce-5-1] eliminated 30 binary clauses 0%
c [cce-5-1] eliminated 42 ternary clauses 0%
c [cce-5-1] eliminated 72 small clauses 0%
c [cce-5-1] eliminated 101 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 111 covered clauses in round 1
c [cce-5] eliminated 111 covered clauses in TOTAL during 1 rounds
c [cce-5] 111 < 1/100 * 37593 = 375 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 6889 variables 100%
c [elim-6] limit of 57586963 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 116 variables 2% in round 1 in 9702650 steps
c [elim-6-1] backward subsumption/strengthening limit 9702600
c [elim-6-1-1] backward checking 636 touched variables 9%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 3 and strengthened 9 clauses in 1806329 steps
c [elim-6-1] rescheduled 41 variables 1% by backward subsumption
c [elim-6-2] eliminated 3 variables 0% in round 2 in 2158421 steps
c [elim-6-2] backward subsumption/strengthening limit 2158400
c [elim-6-2-1] backward checking 31 touched variables 0%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 0 and strengthened 0 clauses in 566206 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 119 = 2% variables out of 6889 scheduled
c [bca-5] limit of 10000000 steps and 74635 added (scaled 2)
c [bca-5] 5142 out of 13542 literals actually usable 38%
c [bca-5] added 19 blocked clauses in 43307 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 265 pos 36.3% + 465 neg 63.7% = 730 sched 10.8% ret 6040
c [sweep-6-1] 1017124 steps 146 queries 58.78 avg class size
c [sweep-6-1] 2389 decisions 132 SAT calls 34.74 avg env size
c [sweep-6-1] 383 variables remain 6% (6387 retained 94%)
c [decomp-21] removed 33 variables
c [sweep-6-1] removed 33 vars (0 failed, 29 eqs, 25 impls)
c [sweep-6] removed 33 vars in TOTAL (1 rounds, 145 queries)
c [sort-queue-7] sorted 402 enqueued variables after 74003 conflicts
c [score-dist-7] active 6335 (94%), one 0 (0%), zero 402 (6%)
c [score-dist-7] max exp 532, different 28 (5%)
c [score-dist-7] median active exp 524, avg 523.1
c [simplification-7] removed 174 variables 2.5% (6737 remain 22%)
c [simplification-7] removed 899 irredundant clauses 2.4% (36905 remain 41%)
c [simplification-7] maximum reduction of 3% = max (3%, 2%)
c [simplification-7] geometric conflict interval increment 6499 = 25999 / 4
c [simplification-7] new conflict interval 32498
c [simplification-7] penalized conflict interval 32498 = 1 * 32498
c [simplification-7] hard conflict limit 122750 (soft 106501 + delta 16249)
c [simplification-7] new conflict limit 106501 (hard 122750)
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 -   28.3    6737    36905    103863   29100   5714 10399   34    90   11  38%    785   -8   36   22  163%
c 
c [simplification-8] limit 106501 conflicts (hard 122750) hit after 122751 conflicts
c [quatres-6] found 9060 quaternary clauses 47% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-1] added 2 double-self-subsuming ternary resolvents
c [quatres-6-2] added 17 single-self-subsuming ternary resolvents
c [quatres-6-2] added 35 quaternary resolvents
c [ternres-6] limit 4806072 with penalty 0 = 0 + 0
c [ternres-6] 2 schedulable variables 0%
c [ternres-6] 258 ternary resolvents (11 bin, 247 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-22] removed 1 variables
c [basicprobe-3] limit 24030363 penalty 0 = 0 + 0
c [basicprobe-3-0] 2029 sched 30%, 7 failed, 1 lifted, 915 hbrs
c [decomp-23] removed 14 variables
c [basicprobe-3-1] 4003 sched 60%, 3 failed, 0 lifted, 257 hbrs
c [decomp-24] removed 5 variables
c [basicprobe-3-2] 4000 sched 60%, 1 failed, 0 lifted, 21 hbrs
c [decomp-25] removed 1 variables
c [basicprobe-3-3] 3999 sched 60%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-4] 3999 sched 60%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-4] fully completed probing
c [basicprobe-3-4] 12 units = 11 failed (92%) + 1 lifted (8%)
c [basicprobe-3-4] removed 20 variables, found 1194 hbrs
c [bate-2] eliminated 4 asymmetric tautologies during probing
c [unhide-6] limit 961214 with penalty 0 = 0 + 0
c [unhide-6-7] 0 units, 0 failed, 1011 tauts, 0 hbrs, 54134 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 255 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 6716 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 55 blocked clauses
c [block-4] 55 < 1/100 * 36800 = 368 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 6711 variables 100%
c [elim-7] limit of 96121453 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 57 variables 1% in round 1 in 9543840 steps
c [elim-7-1] backward subsumption/strengthening limit 9543800
c [elim-7-1-1] backward checking 413 touched variables 6%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 17 clauses in 745899 steps
c [elim-7-1] rescheduled 40 variables 1% by backward subsumption
c [elim-7-2] eliminated 1 variables 0% in round 2 in 40717 steps
c [elim-7-2] backward subsumption/strengthening limit 40700
c [elim-7-2-1] backward checking 10 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 18191 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 58 = 1% variables out of 6711 scheduled
c [elim-7] 58 < 1/100 * 6711 = 67 considered unsuccessful
c [bca-6] limit of 10000000 steps and 73864 added (scaled 2)
c [bca-6] 5057 out of 13308 literals actually usable 38%
c [bca-6] added 2 blocked clauses in 55592 steps
c [sweep-7] limit 1441821 penalty 0 = 0 + 0
c [sweep-7-1] 138 pos 37.5% + 230 neg 62.5% = 368 sched 5.5% ret 6285
c [sweep-7-1] 1032772 steps 204 queries 20.54 avg class size
c [sweep-7-1] 2875 decisions 193 SAT calls 30.11 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-27] removed 26 variables
c [sweep-7-1] removed 26 vars (0 failed, 24 eqs, 23 impls)
c [sweep-7-2] 2760 pos 41.6% + 3867 neg 58.4% = 6627 sched 100.0% ret 0
c [sweep-7-2] 434104 steps 42 queries 754.79 avg class size
c [sweep-7-2] 961 decisions 41 SAT calls 43.37 avg env size
c [sweep-7-2] 6063 variables remain 91% (564 retained 9%)
c [sweep-7-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7] removed 26 vars in TOTAL (2 rounds, 244 queries)
c [sort-queue-8] sorted 398 enqueued variables after 122751 conflicts
c [score-dist-8] active 6229 (94%), one 0 (0%), zero 398 (6%)
c [score-dist-8] max exp 534, different 30 (6%)
c [score-dist-8] median active exp 526, avg 524.2
c [simplification-8] removed 110 variables 1.6% (6627 remain 22%)
c [simplification-8] removed 371 irredundant clauses 1.0% (36534 remain 41%)
c [simplification-8] maximum reduction of 2% = max (2%, 1%)
c [simplification-8] geometric conflict interval increment 10832 = 32498 / 3
c [simplification-8] new conflict interval 43330
c [simplification-8] penalized conflict interval 43330 = 1 * 43330
c [simplification-8] hard conflict limit 187746 (soft 166081 + delta 21665)
c [simplification-8] new conflict limit 166081 (hard 187746)
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 -   34.0    6627    36534    137608   30131   5378 10120   22    85   11  26%    881   -7   18   26   69%
c -   37.5    6627    36532    169571   28366   5395 10124   43    69   16  62%    936  -21   36   28  127%
c i   38.9    6626    36532    183214   39672   5396 10125   47    62   21  76%    953  -24   50   30  164%
c 
c [simplification-9] limit 166081 conflicts (hard 187746) hit after 187747 conflicts
c [quatres-7] found 9100 quaternary clauses 47% in total
c [quatres-7-1] removed 5 duplicate quaternary clauses
c [quatres-7-2] added 13 single-self-subsuming ternary resolvents
c [quatres-7-2] added 71 quaternary resolvents
c [ternres-7] limit 7183617 with penalty 0 = 0 + 0
c [ternres-7] all 6626 free variables schedulable
c [ternres-7] 631 ternary resolvents (39 bin, 592 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-29] removed 4 variables
c [simpleprobe-4] all 6623 free variables schedulable
c [simpleprobe-4] limit 28734470 penalty 0 = 0 + 0
c [decomp-30] removed 23 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 23 variables, found 803 hbrs, 4 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 588 transitive binary clauses
c [cce-6] limit of 17959043 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 4 clauses out of 77 (5%) of length 11
c [cce-6-1] eliminated 13 clauses out of 427 (3%) of length 8
c [cce-6-1] eliminated 17 clauses out of 834 (2%) of length 7
c [cce-6-1] eliminated 40 clauses out of 1836 (2%) of length 6
c [cce-6-1] eliminated 63 clauses out of 3179 (2%) of length 5
c [cce-6-1] eliminated 36 clauses out of 7303 (0%) of length 4
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 173 large clauses in 17959046 steps
c [cce-6-1] allowing another 8979523 steps for small clauses
c [cce-6-1] scheduling 16884 clauses = 6367 binary + 10517 ternary
c [cce-6-1] tried to eliminate 1048 small clauses 6%
c [cce-6-1] eliminated 2 binary clauses 0%
c [cce-6-1] eliminated 5 ternary clauses 0%
c [cce-6-1] eliminated 7 small clauses 0%
c [cce-6-1] eliminated 7 small clauses in 17959047 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 180 covered clauses in round 1
c [cce-6] eliminated 180 covered clauses in TOTAL during 1 rounds
c [cce-6] 180 < 1/100 * 36405 = 364 considered unsuccessful
c [bca-7] limit of 10000000 steps and 73231 added (scaled 2)
c [bca-7] 5250 out of 13202 literals actually usable 40%
c [bca-7] added 0 blocked clauses in 55869 steps
c [sweep-8] limit 2155085 penalty 0 = 0 + 0
c [sweep-8-1] 2485 pos 41.2% + 3553 neg 58.8% = 6038 sched 91.5% ret 562
c [sweep-8-1] 2232637 steps 224 queries 145.93 avg class size
c [sweep-8-1] 4618 decisions 221 SAT calls 43.99 avg env size
c [sweep-8-1] 2488 variables remain 38% (4110 retained 62%)
c [decomp-31] removed 6 variables
c [sweep-8-1] removed 6 vars (0 failed, 4 eqs, 6 impls)
c [sweep-8] removed 6 vars in TOTAL (1 rounds, 223 queries)
c [sort-queue-9] sorted 380 enqueued variables after 187747 conflicts
c [score-dist-9] active 6214 (94%), one 0 (0%), zero 380 (6%)
c [score-dist-9] max exp 535, different 30 (6%)
c [score-dist-9] median active exp 526, avg 525.0
c [simplification-9] removed 32 variables 0.5% (6594 remain 21%)
c [simplification-9] removed 327 irredundant clauses 0.9% (36205 remain 40%)
c [simplification-9] maximum reduction of 1% = max (0%, 1%)
c [simplification-9] geometric conflict interval increment 21665 = 43330 / 2
c [simplification-9] new conflict interval 64995
c [simplification-9] penalized conflict interval 64995 = 1 * 64995
c [simplification-9] hard conflict limit 285239 (soft 252742 + delta 32497)
c [simplification-9] new conflict limit 252742 (hard 285239)
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 -   42.5    6594    36205    207394   29962   5833 10304   25    68   12  37%   -956  -13   27   30   93%
c i   45.1    6593    36203    231676   49966   5846 10305   29   103   22  28%   -343   11   17   29   57%
c -   46.7    6593    36203    243938   29547   5847 10305   21    81   16  27%   -747  -10   41   28  146%
c i   47.2    6592    36203    248651   33083   5851 10305   29    91   18  31%   -625   -1   35   28  124%
c -   50.0    6592    36203    280667   31022   5861 10311   18   225   16   8%   -153   94   17   25   69%
c 
c [simplification-10] limit 252742 conflicts (hard 285239) hit after 285242 conflicts
c [quatres-8] found 9182 quaternary clauses 47% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-1] added 3 double-self-subsuming ternary resolvents
c [quatres-8-2] added 35 single-self-subsuming ternary resolvents
c [quatres-8-2] added 21 quaternary resolvents
c [ternres-8] limit 10687170 with penalty 0 = 0 + 0
c [ternres-8] all 6592 free variables schedulable
c [ternres-8] 333 ternary resolvents (31 bin, 302 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 667948 penalty 3 = 3 + 0
c [card-4] found 378 at-most-one constraints of average size 3.2
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 667948 for elimination
c [card-4] 378 out of 378 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-5] limit 534358 penalty 2 = 2 + 0
c [gauss-5] extracted 1595 xors of average arity 3.0
c [gauss-5] connected 4776 occurrences of 744 variables (average 6.4)
c [gauss-5] limit 534358 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 4 variables
c [treelook-4] limit 1068717 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 12394 literals 94%
c [treelook-4] scheduling used 270503 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1068717 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 1068770 steps
c [treelook-4] 12092 literals remain 92%
c [treelook-4] 6077 variables remain to probed next time 92%
c [decomp-33] removed 3 variables
c [treelook-4] removed 5 variables, found 2335 hbrs
c [unhide-7] limit 1068717 with penalty 1 = 1 + 0
c [unhide-7-9] 1 units, 3 failed, 806 tauts, 0 hbrs, 31724 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 255 transitive binary clauses
c [transred-8] found 2 units
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 6579 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2137434180 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 71 variables 1% in round 1 in 9334892 steps
c [elim-8-1] backward subsumption/strengthening limit 9334800
c [elim-8-1-1] backward checking 382 touched variables 6%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1 and strengthened 0 clauses in 743366 steps
c [elim-8-1] rescheduled 10 variables 0% by backward subsumption
c [elim-8-2] eliminated 5 variables 0% in round 2 in 43424 steps
c [elim-8-2] backward subsumption/strengthening limit 43400
c [elim-8-2-1] backward checking 18 touched variables 0%
c [elim-8-2-1] incomplete backward checking 14 remain 78%
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 43871 steps
c [elim-8-2] fully rescheduled 6503 variables 99%
c [elim-8-3] eliminated 12 variables 0% in round 3 in 9247622 steps
c [elim-8-3] backward subsumption/strengthening limit 9247600
c [elim-8-3-1] backward checking 74 touched variables 1%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 0 and strengthened 0 clauses in 583563 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 88 = 1% variables out of 6579 scheduled
c [sweep-9] limit 3206151 penalty 0 = 0 + 0
c [sweep-9-1] 1083 pos 44.5% + 1353 neg 55.5% = 2436 sched 37.5% ret 4055
c [sweep-9-1] 3208066 steps 335 queries 53.08 avg class size
c [sweep-9-1] 7444 decisions 334 SAT calls 45.01 avg env size
c [sweep-9-1] 572 variables remain 9% (5919 retained 91%)
c [decomp-34] removed 24 variables
c [sweep-9-1] removed 24 vars (0 failed, 26 eqs, 23 impls)
c [sweep-9] removed 24 vars in TOTAL (1 rounds, 334 queries)
c [sort-queue-10] sorted 338 enqueued variables after 285242 conflicts
c [score-dist-10] active 6129 (95%), one 0 (0%), zero 338 (5%)
c [score-dist-10] max exp 536, different 31 (6%)
c [score-dist-10] median active exp 528, avg 526.2
c [simplification-10] removed 125 variables 1.9% (6467 remain 21%)
c [simplification-10] removed 397 irredundant clauses 1.1% (35806 remain 40%)
c [simplification-10] maximum reduction of 2% = max (2%, 1%)
c [simplification-10] geometric conflict interval increment 21665 = 64995 / 3
c [simplification-10] new conflict interval 86660
c [simplification-10] penalized conflict interval 86660 = 1 * 86660
c [simplification-10] hard conflict limit 415232 (soft 371902 + delta 43330)
c [simplification-10] new conflict limit 371902 (hard 415232)
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 -   55.9    6467    35806    316394   31902   5818 10286   32   149   15  21%    342    8   35   26  137%
c -   60.8    6467    35806    353393   32326   5828 10288   21    81   15  26%    636  -44   21   25   83%
c -   65.2    6467    35806    391397   33328   5832 10288   19    26   15  72%    807  -63   20   23   89%
c 
c [simplification-11] limit 371902 conflicts (hard 415232) hit after 415232 conflicts
c [quatres-9] found 9215 quaternary clauses 45% in total
c [quatres-9-1] added 2 double-self-subsuming ternary resolvents
c [quatres-9-2] added 22 single-self-subsuming ternary resolvents
c [quatres-9-2] added 49 quaternary resolvents
c [ternres-9] limit 18421171 with penalty 0 = 0 + 0
c [ternres-9] all 6467 free variables schedulable
c [ternres-9] 216 ternary resolvents (23 bin, 193 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-35] removed 1 variables
c [basicprobe-4] limit 92105856 penalty 0 = 0 + 0
c [basicprobe-4-0] 3816 sched 59%, 6 failed, 0 lifted, 306 hbrs
c [decomp-36] removed 6 variables
c [basicprobe-4-1] 3810 sched 59%, 0 failed, 0 lifted, 21 hbrs
c [basicprobe-4-2] 3810 sched 59%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-3] 3810 sched 59%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-3] fully completed probing
c [basicprobe-4-3] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-4-3] removed 6 variables, found 328 hbrs
c [bate-3] eliminated 5 asymmetric tautologies during probing
c [unhide-8] limit 3684234 with penalty 0 = 0 + 0
c [unhide-8-13] 0 units, 0 failed, 528 tauts, 0 hbrs, 56024 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 143 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 6460 variables 100%
c [elim-9] limit of 368423427 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 23 variables 0% in round 1 in 9173698 steps
c [elim-9-1] backward subsumption/strengthening limit 9173600
c [elim-9-1-1] backward checking 202 touched variables 3%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 4 clauses in 655498 steps
c [elim-9-1] rescheduled 9 variables 0% by backward subsumption
c [elim-9-2] eliminated 1 variables 0% in round 2 in 4046 steps
c [elim-9-2] backward subsumption/strengthening limit 4000
c [elim-9-2-1] backward checking 11 touched variables 0%
c [elim-9-2-1] incomplete backward checking 0 remain 0%
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 4001 steps
c [elim-9-2] fully rescheduled 6436 variables 100%
c [elim-9-3] eliminated 1 variables 0% in round 3 in 9139374 steps
c [elim-9-3] backward subsumption/strengthening limit 9139300
c [elim-9-3-1] backward checking 25 touched variables 0%
c [elim-9-3-1] fully completed backward checking in 1 rounds
c [elim-9-3] subsumed 0 and strengthened 1 clauses in 87515 steps
c [elim-9] incomplete 7 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 25 = 0% variables out of 6460 scheduled
c [elim-9] 25 < 1/100 * 6460 = 64 considered unsuccessful
c [bca-8] limit of 10000000 steps and 72045 added (scaled 2)
c [bca-8] 5330 out of 12872 literals actually usable 41%
c [bca-8] added 4 blocked clauses in 65025 steps
c [sweep-10] limit 5526351 penalty 0 = 0 + 0
c [sweep-10-1] 243 pos 43.1% + 321 neg 56.9% = 564 sched 8.8% ret 5871
c [sweep-10-1] 1794987 steps 259 queries 28.93 avg class size
c [sweep-10-1] 4029 decisions 252 SAT calls 33.56 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-39] removed 22 variables
c [sweep-10-1] removed 22 vars (0 failed, 22 eqs, 15 impls)
c [sweep-10-2] 2551 pos 39.8% + 3862 neg 60.2% = 6413 sched 100.0% ret 0
c [sweep-10-2] 3751702 steps 302 queries 107.19 avg class size
c [sweep-10-2] 6254 decisions 305 SAT calls 45.01 avg env size
c [sweep-10-2] 1671 variables remain 26% (4741 retained 74%)
c [decomp-40] removed 14 variables
c [sweep-10-2] removed 14 vars (0 failed, 12 eqs, 7 impls)
c [sweep-10] removed 36 vars in TOTAL (2 rounds, 559 queries)
c [sort-queue-11] sorted 299 enqueued variables after 415232 conflicts
c [score-dist-11] active 6100 (95%), one 0 (0%), zero 299 (5%)
c [score-dist-11] max exp 538, different 33 (6%)
c [score-dist-11] median active exp 529, avg 526.8
c [simplification-11] removed 68 variables 1.1% (6399 remain 21%)
c [simplification-11] removed 208 irredundant clauses 0.6% (35598 remain 40%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 43330 = 86660 / 2
c [simplification-11] new conflict interval 129990
c [simplification-11] penalized conflict interval 129990 = 1 * 129990
c [simplification-11] hard conflict limit 610217 (soft 545222 + delta 64995)
c [simplification-11] new conflict limit 545222 (hard 610217)
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 -   72.4    6399    35598    431964   33474   5744  9605   26   124   12  21%    907   60   45   21  209%
c -   77.7    6399    35597    472721   34697   5752  9605   16   115   17  14%    961   19   15   22   67%
c -   82.6    6399    35595    513028   35991   5757  9607   17   129   17  13%    990   20   11   20   57%
c -   87.8    6399    35595    550299   35174   5759  9607   31    98   17  31%   1005  -12   46   23  197%
c 
c [simplification-12] limit 545222 conflicts (hard 610217) hit after 553225 conflicts
c [quatres-10] found 9328 quaternary clauses 44% in total
c [quatres-10-1] removed 4 duplicate quaternary clauses
c [quatres-10-2] added 22 single-self-subsuming ternary resolvents
c [quatres-10-2] added 88 quaternary resolvents
c [ternres-10] limit 25593914 with penalty 0 = 0 + 0
c [ternres-10] all 6399 free variables schedulable
c [ternres-10] 402 ternary resolvents (25 bin, 377 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-41] removed 2 variables
c [simpleprobe-5] all 6397 free variables schedulable
c [simpleprobe-5] limit 102375656 penalty 0 = 0 + 0
c [decomp-42] removed 5 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 5 variables, found 835 hbrs, 1 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 453 transitive binary clauses
c [transred-10] found 2 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 6390 variables 100%
c [block-5] limit of 31992392 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 23 blocked clauses
c [block-5] 23 < 1/100 * 35546 = 355 considered unsuccessful
c [cce-7] limit of 31992392 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 1 clauses out of 283 (0%) of length 9
c [cce-7-1] eliminated 8 clauses out of 434 (2%) of length 8
c [cce-7-1] eliminated 11 clauses out of 786 (1%) of length 7
c [cce-7-1] eliminated 2 clauses out of 1771 (0%) of length 6
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 22 large clauses in 31992393 steps
c [cce-7-1] allowing another 15996196 steps for small clauses
c [cce-7-1] scheduling 16366 clauses = 6178 binary + 10188 ternary
c [cce-7-1] tried to eliminate 5459 small clauses 33%
c [cce-7-1] eliminated 45 binary clauses 1%
c [cce-7-1] eliminated 112 ternary clauses 1%
c [cce-7-1] eliminated 157 small clauses 1%
c [cce-7-1] eliminated 157 small clauses in 31993165 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 179 covered clauses in round 1
c [cce-7] eliminated 179 covered clauses in TOTAL during 1 rounds
c [cce-7] 179 < 1/100 * 35516 = 355 considered unsuccessful
c [bca-9] limit of 10000000 steps and 71457 added (scaled 2)
c [bca-9] 5042 out of 12782 literals actually usable 39%
c [bca-9] added 9 blocked clauses in 50104 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 76781740 penalty 0 = 0 + 0
c [sweep-11-1] 720 pos 43.2% + 946 neg 56.8% = 1666 sched 26.1% ret 4724
c [sweep-11-1] 3203577 steps 472 queries 31.39 avg class size
c [sweep-11-1] 7841 decisions 471 SAT calls 36.76 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-43] removed 15 variables
c [sweep-11-1] removed 15 vars (0 failed, 15 eqs, 11 impls)
c [sweep-11-2] 2633 pos 41.3% + 3742 neg 58.7% = 6375 sched 100.0% ret 0
c [sweep-11-2] 6168159 steps 713 queries 52.50 avg class size
c [sweep-11-2] 13088 decisions 708 SAT calls 39.08 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-44] removed 23 variables
c [sweep-11-2] removed 23 vars (0 failed, 24 eqs, 22 impls)
c [sweep-11-3] 2623 pos 41.3% + 3729 neg 58.7% = 6352 sched 100.0% ret 0
c [sweep-11-3] 5461864 steps 699 queries 44.81 avg class size
c [sweep-11-3] 12825 decisions 700 SAT calls 39.34 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-45] removed 10 variables
c [sweep-11-3] removed 10 vars (0 failed, 10 eqs, 6 impls)
c [sweep-11] removed 48 vars in TOTAL (3 rounds, 1881 queries)
c [sort-queue-12] sorted 232 enqueued variables after 553225 conflicts
c [score-dist-12] active 6110 (96%), one 0 (0%), zero 232 (4%)
c [score-dist-12] max exp 538, different 33 (6%)
c [score-dist-12] median active exp 530, avg 527.9
c [simplification-12] removed 57 variables 0.9% (6342 remain 21%)
c [simplification-12] removed 305 irredundant clauses 0.9% (35290 remain 39%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 64995 = 129990 / 2
c [simplification-12] new conflict interval 194985
c [simplification-12] penalized conflict interval 194985 = 1 * 194985
c [simplification-12] hard conflict limit 845702 (soft 748210 + delta 97492)
c [simplification-12] new conflict limit 748210 (hard 845702)
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 -   96.7    6342    35289    591176   36743   6208 10127   42   110   16  38%   1014   -4   54   26  208%
c -  102.1    6342    35289    630517   37412   6209 10127   32   105   17  30%   1018   -6   35   30  117%
c -  107.4    6342    35288    671620   37649   6214 10127   60    86   17  70%   1021  -21   68   36  190%
c -  112.8    6342    35288    713701   38186   6218 10127   27   107   17  26%   1022    1   27   33   80%
c 
c [simplification-13] limit 748210 conflicts (hard 845702) hit after 748211 conflicts
c [quatres-11] found 9598 quaternary clauses 44% in total
c [quatres-11-1] removed 4 duplicate quaternary clauses
c [quatres-11-1] added 4 double-self-subsuming ternary resolvents
c [quatres-11-2] added 37 single-self-subsuming ternary resolvents
c [quatres-11-2] added 57 quaternary resolvents
c [ternres-11] limit 35441481 with penalty 0 = 0 + 0
c [ternres-11] all 6342 free variables schedulable
c [ternres-11] 463 ternary resolvents (25 bin, 438 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-46] removed 1 variables
c [treelook-5] limit 3544148 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 11914 literals 94%
c [treelook-5] scheduling used 348653 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 3544148 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 3548025 steps
c [treelook-5] 10019 literals remain 79%
c [treelook-5] 5830 variables remain to probed next time 92%
c [decomp-47] removed 1 variables
c [treelook-5] removed 3 variables, found 3012 hbrs
c [unhide-9] limit 3544148 with penalty 1 = 1 + 0
c [unhide-9-17] 1 units, 0 failed, 1485 tauts, 0 hbrs, 111356 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 335 transitive binary clauses
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 6337 variables 100%
c [elim-10] limit of 354414819 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 82 variables 1% in round 1 in 9058275 steps
c [elim-10-1] backward subsumption/strengthening limit 9058200
c [elim-10-1-1] backward checking 439 touched variables 7%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 2 and strengthened 7 clauses in 746541 steps
c [elim-10-1] rescheduled 25 variables 0% by backward subsumption
c [elim-10-2] no variable eliminated in round 2 in 276113 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 82 = 1% variables out of 6337 scheduled
c [bca-10] limit of 10000000 steps and 70458 added (scaled 2)
c [bca-10] 4892 out of 12512 literals actually usable 39%
c [bca-10] added 5 blocked clauses in 76876 steps
c [sweep-12] limit 10632444 penalty 0 = 0 + 0
c [sweep-12-1] 2552 pos 40.8% + 3703 neg 59.2% = 6255 sched 100.0% ret 0
c [sweep-12-1] 6331906 steps 659 queries 33.31 avg class size
c [sweep-12-1] 12605 decisions 661 SAT calls 43.75 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-48] removed 13 variables
c [sweep-12-1] removed 13 vars (0 failed, 14 eqs, 11 impls)
c [sweep-12-2] 2547 pos 40.8% + 3695 neg 59.2% = 6242 sched 100.0% ret 0
c [sweep-12-2] 4310502 steps 387 queries 81.54 avg class size
c [sweep-12-2] 9358 decisions 385 SAT calls 50.98 avg env size
c [sweep-12-2] 879 variables remain 14% (5363 retained 86%)
c [decomp-49] removed 5 variables
c [sweep-12-2] removed 5 vars (0 failed, 6 eqs, 3 impls)
c [sweep-12] removed 18 vars in TOTAL (2 rounds, 1044 queries)
c [sort-queue-13] sorted 191 enqueued variables after 748211 conflicts
c [score-dist-13] active 6046 (97%), one 0 (0%), zero 191 (3%)
c [score-dist-13] max exp 539, different 34 (6%)
c [score-dist-13] median active exp 531, avg 528.6
c [simplification-13] removed 105 variables 1.7% (6237 remain 20%)
c [simplification-13] removed 462 irredundant clauses 1.3% (34826 remain 39%)
c [simplification-13] maximum reduction of 2% = max (2%, 1%)
c [simplification-13] geometric conflict interval increment 64995 = 194985 / 3
c [simplification-13] new conflict interval 259980
c [simplification-13] penalized conflict interval 259980 = 1 * 259980
c [simplification-13] hard conflict limit 1138181 (soft 1008191 + delta 129990)
c [simplification-13] new conflict limit 1008191 (hard 1138181)
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 -  121.7    6237    34826    759072   38541   6276 11279   44    83   14  53%   1023  -20   59   33  181%
c i  121.7    6236    34826    759519   38979   6276 11279   43    83   17  52%   1023  -20   40   33  123%
c -  128.6    6236    34826    808382   39734   6278 11279   62    71   20  88%  -2824  -19   64   45  141%
c -  134.7    6236    34826    858463   39199   6280 11279   22   150   20  14%   -768   61   19   43   44%
c -  142.2    6236    34826    918467   40065   6280 11279   36    79   20  46%    307   -2   28   43   65%
c -  148.5    6236    34826    971550   42276   6281 11279   46    62   21  74%    705  -16   51   43  119%
c -  155.7    6236    34826   1029377   41444   6284 11279   39    67   21  59%    892   -3   28   44   64%
c 
c [simplification-14] limit 1008191 conflicts (hard 1138181) hit after 1029803 conflicts
c [quatres-12] found 9551 quaternary clauses 43% in total
c [quatres-12-1] removed 3 duplicate quaternary clauses
c [quatres-12-1] added 1 double-self-subsuming ternary resolvents
c [quatres-12-2] added 11 single-self-subsuming ternary resolvents
c [quatres-12-2] added 59 quaternary resolvents
c [ternres-12] limit 51512208 with penalty 0 = 0 + 0
c [ternres-12] all 6236 free variables schedulable
c [ternres-12] 541 ternary resolvents (29 bin, 512 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-6] limit 1287805 penalty 3 = 3 + 0
c [gauss-6] extracted 3563 xors of average arity 3.0
c [gauss-6] connected 10703 occurrences of 719 variables (average 14.9)
c [gauss-6] limit 1287805 penalty 3 = 3 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-5] limit 257561041 penalty 0 = 0 + 0
c [basicprobe-5-0] 3665 sched 59%, 1 failed, 0 lifted, 358 hbrs
c [decomp-51] removed 2 variables
c [basicprobe-5-1] 3677 sched 59%, 0 failed, 0 lifted, 226 hbrs
c [basicprobe-5-2] 3681 sched 59%, 0 failed, 0 lifted, 98 hbrs
c [basicprobe-5-3] 3695 sched 59%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-5-4] 3694 sched 59%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-4] fully completed probing
c [basicprobe-5-4] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-5-4] removed 2 variables, found 683 hbrs
c [bate-4] eliminated 4 asymmetric tautologies during probing
c [unhide-10] limit 10302441 with penalty 0 = 0 + 0
c [unhide-10-30] 0 units, 0 failed, 854 tauts, 0 hbrs, 60476 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 150 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 6234 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 50 variables 1% in round 1 in 9018222 steps
c [elim-11-1] backward subsumption/strengthening limit 9018200
c [elim-11-1-1] backward checking 242 touched variables 4%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 0 and strengthened 1 clauses in 607339 steps
c [elim-11-1] rescheduled 7 variables 0% by backward subsumption
c [elim-11-2] eliminated 1 variables 0% in round 2 in 2297 steps
c [elim-11-2] backward subsumption/strengthening limit 2200
c [elim-11-2-1] backward checking 11 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 0 and strengthened 0 clauses in 2201 steps
c [elim-11-2] fully rescheduled 6183 variables 99%
c [elim-11-3] eliminated 4 variables 0% in round 3 in 8981595 steps
c [elim-11-3] backward subsumption/strengthening limit 8981500
c [elim-11-3-1] backward checking 31 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 526264 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 55 = 1% variables out of 6234 scheduled
c [elim-11] 55 < 1/100 * 6234 = 62 considered unsuccessful
c [bca-11] limit of 10000000 steps and 70016 added (scaled 2)
c [bca-11] 4753 out of 12360 literals actually usable 38%
c [bca-11] added 14 blocked clauses in 53062 steps
c [sweep-13] limit 15453662 penalty 0 = 0 + 0
c [sweep-13-1] 349 pos 40.6% + 511 neg 59.4% = 860 sched 13.9% ret 5319
c [sweep-13-1] 1864367 steps 341 queries 25.99 avg class size
c [sweep-13-1] 4473 decisions 337 SAT calls 30.59 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-55] removed 7 variables
c [sweep-13-1] removed 7 vars (0 failed, 9 eqs, 7 impls)
c [sweep-13-2] 2479 pos 40.2% + 3693 neg 59.8% = 6172 sched 100.0% ret 0
c [sweep-13-2] 5550282 steps 660 queries 32.48 avg class size
c [sweep-13-2] 12266 decisions 652 SAT calls 40.87 avg env size
c [sweep-13-2] fully completed sweeping round
c [decomp-56] removed 15 variables
c [sweep-13-2] removed 15 vars (0 failed, 16 eqs, 9 impls)
c [sweep-13-3] 2471 pos 40.1% + 3686 neg 59.9% = 6157 sched 100.0% ret 0
c [sweep-13-3] 5827500 steps 690 queries 43.66 avg class size
c [sweep-13-3] 12201 decisions 685 SAT calls 39.93 avg env size
c [sweep-13-3] fully completed sweeping round
c [decomp-57] removed 16 variables
c [sweep-13-3] removed 16 vars (0 failed, 21 eqs, 13 impls)
c [sweep-13] removed 38 vars in TOTAL (3 rounds, 1688 queries)
c [sort-queue-14] sorted 150 enqueued variables after 1029803 conflicts
c [score-dist-14] active 5991 (98%), one 0 (0%), zero 150 (2%)
c [score-dist-14] max exp 540, different 35 (6%)
c [score-dist-14] median active exp 531, avg 529.1
c [simplification-14] removed 95 variables 1.5% (6141 remain 20%)
c [simplification-14] removed 239 irredundant clauses 0.7% (34587 remain 38%)
c [simplification-14] maximum reduction of 2% = max (2%, 1%)
c [simplification-14] geometric conflict interval increment 86660 = 259980 / 3
c [simplification-14] new conflict interval 346640
c [simplification-14] penalized conflict interval 346640 = 1 * 346640
c [simplification-14] hard conflict limit 1549763 (soft 1376443 + delta 173320)
c [simplification-14] new conflict limit 1376443 (hard 1549763)
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  162.2    6140    34587   1043084   54807   6415 10718   29    85   20  34%    917   13   28   41   68%
c -  167.0    6140    34587   1078203   41629   6416 10719   42    66   18  64%  -1672  -14   47   37  128%
c -  173.9    6140    34587   1142656   42855   6418 10719   40    54   19  73%     16  -15   37   38   97%
c -  180.3    6140    34587   1199483   43875   6418 10719   43    57   19  76%    600  -10   39   38  104%
c -  186.7    6140    34587   1256900   43533   6420 10719   40    56   19  71%    848   -9   33   36   91%
c -  194.6    6140    34587   1322859   43979   6421 10719   46    50   19  92%    960   -8   47   39  122%
c -  201.1    6140    34587   1372642   44853   6427 10719   25    76   27  33%    994    8   24   32   75%
c 
c [simplification-15] limit 1376443 conflicts (hard 1549763) hit after 1376443 conflicts
c [quatres-13] found 9700 quaternary clauses 43% in total
c [quatres-13-1] removed 8 duplicate quaternary clauses
c [quatres-13-1] added 6 double-self-subsuming ternary resolvents
c [quatres-13-2] added 17 single-self-subsuming ternary resolvents
c [quatres-13-2] added 73 quaternary resolvents
c [ternres-13] limit 72251746 with penalty 0 = 0 + 0
c [ternres-13] all 6140 free variables schedulable
c [ternres-13] 696 ternary resolvents (38 bin, 658 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 2257867 penalty 4 = 4 + 0
c [card-5] found 372 at-most-one constraints of average size 3.1
c [card-5] found 49 at-most-two constraints of average size 4.0
c [card-5] using previous limit 2257867 for elimination
c [card-5] 421 out of 421 constraints (100%) meet size limits
c [card-5] found 1 units
c [card-5] no units found
c [card-5] generated 23 at-most-one constraints, 7 used 30%
c [card-5] exported 10 binary clauses, 1.4 per/constraint
c [decomp-58] removed 4 variables
c [simpleprobe-6] all 6137 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-59] removed 8 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 8 variables, found 1154 hbrs, 1 units
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 566 transitive binary clauses
c [bca-12] limit of 10000000 steps and 69847 added (scaled 2)
c [bca-12] 4704 out of 12260 literals actually usable 38%
c [bca-12] added 3 blocked clauses in 59436 steps
c [sweep-14] limit 21675523 penalty 0 = 0 + 0
c [sweep-14-1] 2512 pos 41.0% + 3617 neg 59.0% = 6129 sched 100.0% ret 0
c [sweep-14-1] 5986882 steps 651 queries 51.78 avg class size
c [sweep-14-1] 11972 decisions 649 SAT calls 40.28 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-60] removed 3 variables
c [sweep-14-1] removed 3 vars (0 failed, 3 eqs, 7 impls)
c [sweep-14-2] 2511 pos 41.0% + 3615 neg 59.0% = 6126 sched 100.0% ret 0
c [sweep-14-2] 6538981 steps 636 queries 79.26 avg class size
c [sweep-14-2] 11311 decisions 639 SAT calls 41.02 avg env size
c [sweep-14-2] fully completed sweeping round
c [decomp-61] removed 7 variables
c [sweep-14-2] removed 7 vars (0 failed, 7 eqs, 6 impls)
c [sweep-14-3] 2506 pos 41.0% + 3613 neg 59.0% = 6119 sched 100.0% ret 0
c [sweep-14-3] 7107242 steps 647 queries 51.16 avg class size
c [sweep-14-3] 11724 decisions 647 SAT calls 38.87 avg env size
c [sweep-14-3] fully completed sweeping round
c [decomp-62] removed 11 variables
c [sweep-14-3] removed 11 vars (0 failed, 12 eqs, 12 impls)
c [sweep-14] removed 21 vars in TOTAL (3 rounds, 1931 queries)
c [sort-queue-15] sorted 111 enqueued variables after 1376443 conflicts
c [score-dist-15] active 5997 (98%), one 0 (0%), zero 111 (2%)
c [score-dist-15] max exp 541, different 35 (6%)
c [score-dist-15] median active exp 531, avg 529.6
c [simplification-15] removed 32 variables 0.5% (6108 remain 20%)
c [simplification-15] removed 78 irredundant clauses 0.2% (34509 remain 38%)
c [simplification-15] maximum reduction of 1% = max (1%, 0%)
c [simplification-15] geometric conflict interval increment 173320 = 346640 / 2
c [simplification-15] new conflict interval 519960
c [simplification-15] penalized conflict interval 519960 = 1 * 519960
c [simplification-15] hard conflict limit 2156383 (soft 1896403 + delta 259980)
c [simplification-15] new conflict limit 1896403 (hard 2156383)
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 -  208.5    6108    34509   1427135   45566   7068 11231   21    91   19  23%   1011   25   20   29   69%
c -  216.2    6108    34509   1498968   45657   7078 11231   18    99   19  18%   1020   10   18   22   82%
c -  221.9    6108    34506   1554655   47691   7083 11231   25    80   19  32%   1022  -10   25   22  112%
c -  227.5    6108    34506   1605853   48714   7083 11231   23    59   20  39%   1023  -19   21   24   87%
c -  235.1    6108    34506   1662079   48775   7098 11231   29    66   19  45%   1024  -15   28   25  108%
c -  241.9    6108    34506   1719408   48931   7103 11232   29    67   28  43%   1024  -15   13   25   50%
c -  249.5    6108    34506   1781421   51151   7105 11232   27    64   29  42%   1024  -13   28   28   99%
c -  258.8    6108    34506   1863638   50407   7105 11232   43    44   29  98%   1024  -17   44   33  132%
c 
c [simplification-16] limit 1896403 conflicts (hard 2156383) hit after 1925792 conflicts
c [quatres-14] found 10001 quaternary clauses 42% in total
c [quatres-14-1] removed 9 duplicate quaternary clauses
c [quatres-14-1] added 1 double-self-subsuming ternary resolvents
c [quatres-14-2] added 17 single-self-subsuming ternary resolvents
c [quatres-14-2] added 47 quaternary resolvents
c [ternres-14] limit 104264074 with penalty 0 = 0 + 0
c [ternres-14] all 6108 free variables schedulable
c [ternres-14] 458 ternary resolvents (35 bin, 423 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-63] removed 1 variables
c [treelook-6] limit 10426407 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 11480 literals 94%
c [treelook-6] scheduling used 389638 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 10426407 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 6059074 steps
c [treelook-6] fully completed tree based probing
c [treelook-6] removed 6 variables, found 2262 hbrs
c [unhide-11] limit 10000000 with penalty 1 = 1 + 0
c [unhide-11-38] 1 units, 0 failed, 1490 tauts, 0 hbrs, 166478 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 223 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 651650462 steps penalty 3 = 3 + 0
c [cce-8-1] eliminated 6 clauses out of 257 (2%) of length 9
c [cce-8-1] eliminated 12 clauses out of 382 (3%) of length 8
c [cce-8-1] eliminated 18 clauses out of 789 (2%) of length 7
c [cce-8-1] eliminated 94 clauses out of 1722 (5%) of length 6
c [cce-8-1] eliminated 131 clauses out of 3026 (4%) of length 5
c [cce-8-1] eliminated 282 clauses out of 7050 (4%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 543 large clauses in 24216881 steps
c [cce-8-1] allowing another 12108440 steps for small clauses
c [cce-8-1] scheduling 15748 clauses = 5923 binary + 9825 ternary
c [cce-8-1] tried to eliminate 15748 small clauses 100%
c [cce-8-1] eliminated 74 binary clauses 1%
c [cce-8-1] eliminated 311 ternary clauses 3%
c [cce-8-1] eliminated 385 small clauses 2%
c [cce-8-1] eliminated 385 small clauses in 35037340 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 928 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 11230589 steps for small clauses
c [cce-8-2] scheduling 15363 clauses = 5849 binary + 9514 ternary
c [cce-8-2] tried to eliminate 15363 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 928 covered clauses in TOTAL during 2 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 6100 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 133 variables 2% in round 1 in 8525210 steps
c [elim-12-1] backward subsumption/strengthening limit 8525200
c [elim-12-1-1] backward checking 653 touched variables 11%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 0 and strengthened 7 clauses in 787920 steps
c [elim-12-1] rescheduled 23 variables 0% by backward subsumption
c [elim-12-2] eliminated 1 variables 0% in round 2 in 193127 steps
c [elim-12-2] backward subsumption/strengthening limit 193100
c [elim-12-2-1] backward checking 15 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 0 and strengthened 0 clauses in 21658 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 134 = 2% variables out of 6100 scheduled
c [bca-13] limit of 10000000 steps and 67175 added (scaled 2)
c [bca-13] 4136 out of 11934 literals actually usable 35%
c [bca-13] added 6 blocked clauses in 92181 steps
c [sweep-15] limit 31279222 penalty 0 = 0 + 0
c [sweep-15-1] 2471 pos 41.4% + 3495 neg 58.6% = 5966 sched 100.0% ret 0
c [sweep-15-1] 6874993 steps 610 queries 53.66 avg class size
c [sweep-15-1] 11561 decisions 607 SAT calls 39.66 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-65] removed 14 variables
c [sweep-15-1] removed 14 vars (0 failed, 15 eqs, 9 impls)
c [sweep-15-2] 2463 pos 41.4% + 3489 neg 58.6% = 5952 sched 100.0% ret 0
c [sweep-15-2] 7031896 steps 566 queries 47.37 avg class size
c [sweep-15-2] 11630 decisions 564 SAT calls 43.76 avg env size
c [sweep-15-2] fully completed sweeping round
c [decomp-66] removed 2 variables
c [sweep-15-2] removed 2 vars (0 failed, 3 eqs, 3 impls)
c [sweep-15-3] 2462 pos 41.4% + 3488 neg 58.6% = 5950 sched 100.0% ret 0
c [sweep-15-3] 6597100 steps 599 queries 61.47 avg class size
c [sweep-15-3] 11091 decisions 597 SAT calls 41.65 avg env size
c [sweep-15-3] fully completed sweeping round
c [decomp-67] removed 11 variables
c [sweep-15-3] removed 11 vars (0 failed, 13 eqs, 8 impls)
c [sweep-15] removed 27 vars in TOTAL (3 rounds, 1772 queries)
c [sort-queue-16] sorted 94 enqueued variables after 1925792 conflicts
c [score-dist-16] active 5845 (98%), one 0 (0%), zero 94 (2%)
c [score-dist-16] max exp 542, different 36 (7%)
c [score-dist-16] median active exp 532, avg 530.5
c [simplification-16] removed 169 variables 2.8% (5939 remain 19%)
c [simplification-16] removed 1351 irredundant clauses 3.9% (33155 remain 37%)
c [simplification-16] maximum reduction of 4% = max (3%, 4%)
c [simplification-16] geometric conflict interval increment 103992 = 519960 / 5
c [simplification-16] new conflict interval 623952
c [simplification-16] penalized conflict interval 623952 = 1 * 623952
c [simplification-16] hard conflict limit 2861720 (soft 2549744 + delta 311976)
c [simplification-16] new conflict limit 2549744 (hard 2861720)
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 -  274.4    5939    33155   1950612   50896   7015 10404   33    60   15  55%   1024   -1   37   33  112%
c -  281.4    5939    33155   2009363   51256   7018 10404   24    51   22  47%   1024  -12   24   28   84%
c -  288.0    5939    33154   2069612   51357   7023 10404   21    49   22  42%   1024  -17   25   23  110%
c -  295.7    5939    33154   2135186   52162   7024 10404   29    60   22  48%   1024    1   28   27  102%
c -  303.3    5939    33153   2203255   53317   7026 10404   35    52   23  67%   1024  -10   42   28  149%
c -  312.6    5939    33152   2286936   51296   7031 10404   35    44   23  79%   1024  -12   37   31  117%
c -  325.4    5939    33152   2385672   55050   7031 10404   29    62   24  47%   1024   15   19   34   57%
c -  334.5    5939    33152   2462353   54293   7039 10404   20    58   24  35%   1024    3   22   30   74%
c -  345.5    5939    33152   2554095   55635   7045 10404   29    52   24  56%   1024   -1   17   31   56%
c 
c [simplification-17] limit 2549744 conflicts (hard 2861720) hit after 2554137 conflicts
c [quatres-15] found 9703 quaternary clauses 40% in total
c [quatres-15-1] removed 8 duplicate quaternary clauses
c [quatres-15-1] added 2 double-self-subsuming ternary resolvents
c [quatres-15-2] added 66 single-self-subsuming ternary resolvents
c [quatres-15-2] added 110 quaternary resolvents
c [ternres-15] limit 144383194 with penalty 0 = 0 + 0
c [ternres-15] all 5939 free variables schedulable
c [ternres-15] 574 ternary resolvents (30 bin, 544 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-68] removed 3 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 3505 sched 59%, 4 failed, 0 lifted, 189 hbrs
c [decomp-69] removed 4 variables
c [basicprobe-6-1] 3500 sched 59%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-6-2] 3500 sched 59%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-2] fully completed probing
c [basicprobe-6-2] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-6-2] removed 4 variables, found 192 hbrs
c [unhide-12] limit 20000000 with penalty 0 = 0 + 0
c [unhide-12-58] 0 units, 0 failed, 980 tauts, 0 hbrs, 82792 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 104 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 5932 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 19 blocked clauses
c [block-6] 19 < 1/100 * 33112 = 331 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 5927 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 18 variables 0% in round 1 in 8414052 steps
c [elim-13-1] backward subsumption/strengthening limit 8414000
c [elim-13-1-1] backward checking 146 touched variables 2%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 0 clauses in 544427 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 18 = 0% variables out of 5927 scheduled
c [elim-13] 18 < 1/100 * 5927 = 59 considered unsuccessful
c [bca-14] limit of 10000000 steps and 66806 added (scaled 2)
c [bca-14] 4010 out of 11820 literals actually usable 34%
c [bca-14] added 3 blocked clauses in 65109 steps
c [sweep-16] limit 43314958 penalty 0 = 0 + 0
c [sweep-16-1] 2404 pos 40.7% + 3505 neg 59.3% = 5909 sched 100.0% ret 0
c [sweep-16-1] 7313851 steps 621 queries 49.81 avg class size
c [sweep-16-1] 11465 decisions 625 SAT calls 41.71 avg env size
c [sweep-16-1] fully completed sweeping round
c [decomp-71] removed 28 variables
c [sweep-16-1] removed 28 vars (0 failed, 26 eqs, 12 impls)
c [sweep-16-2] 2390 pos 40.6% + 3491 neg 59.4% = 5881 sched 100.0% ret 0
c [sweep-16-2] 7005693 steps 634 queries 53.76 avg class size
c [sweep-16-2] 11096 decisions 624 SAT calls 39.51 avg env size
c [sweep-16-2] fully completed sweeping round
c [decomp-72] removed 18 variables
c [sweep-16-2] removed 18 vars (0 failed, 20 eqs, 17 impls)
c [sweep-16-3] 2383 pos 40.6% + 3480 neg 59.4% = 5863 sched 100.0% ret 0
c [sweep-16-3] 6338834 steps 613 queries 86.66 avg class size
c [sweep-16-3] 10863 decisions 611 SAT calls 38.20 avg env size
c [sweep-16-3] fully completed sweeping round
c [decomp-73] removed 5 variables
c [sweep-16-3] removed 5 vars (0 failed, 8 eqs, 4 impls)
c [sweep-16] removed 51 vars in TOTAL (3 rounds, 1865 queries)
c [sort-queue-17] sorted 81 enqueued variables after 2554137 conflicts
c [score-dist-17] active 5777 (99%), one 0 (0%), zero 81 (1%)
c [score-dist-17] max exp 543, different 36 (7%)
c [score-dist-17] median active exp 532, avg 530.9
c [simplification-17] removed 81 variables 1.4% (5858 remain 19%)
c [simplification-17] removed 220 irredundant clauses 0.7% (32932 remain 37%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] geometric conflict interval increment 311976 = 623952 / 2
c [simplification-17] new conflict interval 935928
c [simplification-17] penalized conflict interval 935928 = 1 * 935928
c [simplification-17] hard conflict limit 3958029 (soft 3490065 + delta 467964)
c [simplification-17] new conflict limit 3490065 (hard 3958029)
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 -  359.0    5858    32932   2621179   55498   6871  9970   29    49   20  59%   1024  -13   23   27   88%
c -  368.5    5858    32932   2701936   56522   6872  9970   24    56   20  42%   1024   -5   24   27   90%
c -  378.7    5858    32932   2795612   58235   6873  9970   33    49   22  66%   1024   -2   24   30   79%
c -  394.5    5858    32932   2922218   58527   6876  9970   36    36   24  99%   1024   -7   33   35   94%
c -  412.1    5858    32932   3067420   58072   6877  9970   34    35   34  98%   1024   -5   34   33  105%
c -  422.7    5858    32932   3154507   57578   6878  9973   37    42   33  88%   1024   -8   37   30  123%
c -  434.8    5858    32932   3253530   58457   6883  9973   27    66   33  41%   1024   15   19   30   63%
c -  445.6    5858    32932   3347408   59592   6884  9973   24    59   33  42%   1024    7   19   30   66%
c -  458.5    5858    32932   3450984   59871   6885  9973   36    36   33  99%   1024  -11   36   31  116%
c 
c [simplification-18] limit 3490065 conflicts (hard 3958029) hit after 3491383 conflicts
c [quatres-16] found 9818 quaternary clauses 39% in total
c [quatres-16-1] removed 12 duplicate quaternary clauses
c [quatres-16-1] added 4 double-self-subsuming ternary resolvents
c [quatres-16-2] added 38 single-self-subsuming ternary resolvents
c [quatres-16-2] added 74 quaternary resolvents
c [ternres-16] limit 200000000 with penalty 0 = 0 + 0
c [ternres-16] all 5858 free variables schedulable
c [ternres-16] 1047 ternary resolvents (61 bin, 986 trn)
c [ternres-16] fully completed ternary resolution
c [simpleprobe-7] all 5858 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-75] removed 5 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 5 variables, found 1113 hbrs, 2 units
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 579 transitive binary clauses
c [cce-9] limit of 265858561 steps penalty 2 = 2 + 0
c [cce-9-1] eliminated 3 clauses out of 79 (4%) of length 11
c [cce-9-1] eliminated 14 clauses out of 288 (5%) of length 9
c [cce-9-1] eliminated 19 clauses out of 390 (5%) of length 8
c [cce-9-1] eliminated 25 clauses out of 772 (3%) of length 7
c [cce-9-1] eliminated 69 clauses out of 1694 (4%) of length 6
c [cce-9-1] eliminated 142 clauses out of 2919 (5%) of length 5
c [cce-9-1] eliminated 259 clauses out of 6610 (4%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 531 large clauses in 52352364 steps
c [cce-9-1] allowing another 26176182 steps for small clauses
c [cce-9-1] scheduling 10509 clauses = 5581 binary + 4928 ternary
c [cce-9-1] tried to eliminate 10509 small clauses 100%
c [cce-9-1] eliminated 100 binary clauses 2%
c [cce-9-1] eliminated 309 ternary clauses 6%
c [cce-9-1] eliminated 409 small clauses 4%
c [cce-9-1] eliminated 409 small clauses in 47304112 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] completed small and large (ACCE)
c [cce-9-1] eliminated 940 covered clauses in round 1
c [cce-9-2] eliminated 1 clauses out of 371 (0%) of length 8
c [cce-9-2] eliminated 5 clauses out of 1625 (0%) of length 6
c [cce-9-2] eliminated 12 clauses out of 2777 (0%) of length 5
c [cce-9-2] eliminated 16 clauses out of 6351 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 34 large clauses in 54679597 steps
c [cce-9-2] allowing another 27339798 steps for small clauses
c [cce-9-2] scheduling 10101 clauses = 5481 binary + 4620 ternary
c [cce-9-2] tried to eliminate 10101 small clauses 100%
c [cce-9-2] eliminated 21 binary clauses 0%
c [cce-9-2] eliminated 8 ternary clauses 0%
c [cce-9-2] eliminated 29 small clauses 0%
c [cce-9-2] eliminated 29 small clauses in 48595578 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 63 covered clauses in round 2
c [cce-9-3] eliminated 5 clauses out of 2765 (0%) of length 5
c [cce-9-3] eliminated 5 clauses out of 6335 (0%) of length 4
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] eliminated 10 large clauses in 54133908 steps
c [cce-9-3] allowing another 27066954 steps for small clauses
c [cce-9-3] scheduling 10072 clauses = 5460 binary + 4612 ternary
c [cce-9-3] tried to eliminate 10072 small clauses 100%
c [cce-9-3] eliminated 10 binary clauses 0%
c [cce-9-3] eliminated 7 ternary clauses 0%
c [cce-9-3] eliminated 17 small clauses 0%
c [cce-9-3] eliminated 17 small clauses in 48254613 steps
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 27 covered clauses in round 3
c [cce-9] eliminated 1030 covered clauses in TOTAL during 3 rounds
c [bca-15] limit of 10000000 steps and 64487 added (scaled 2)
c [bca-15] 3795 out of 11708 literals actually usable 32%
c [bca-15] added 7 blocked clauses in 88262 steps
c [sweep-17] limit 63806054 penalty 0 = 0 + 0
c [sweep-17-1] 2403 pos 41.1% + 3450 neg 58.9% = 5853 sched 100.0% ret 0
c [sweep-17-1] 6932295 steps 612 queries 62.21 avg class size
c [sweep-17-1] 11568 decisions 615 SAT calls 43.24 avg env size
c [sweep-17-1] fully completed sweeping round
c [decomp-76] removed 11 variables
c [sweep-17-1] removed 11 vars (0 failed, 11 eqs, 6 impls)
c [sweep-17-2] 2399 pos 41.1% + 3443 neg 58.9% = 5842 sched 100.0% ret 0
c [sweep-17-2] 6779917 steps 602 queries 33.03 avg class size
c [sweep-17-2] 11942 decisions 596 SAT calls 47.49 avg env size
c [sweep-17-2] fully completed sweeping round
c [decomp-77] removed 11 variables
c [sweep-17-2] removed 11 vars (0 failed, 10 eqs, 11 impls)
c [sweep-17-3] 2398 pos 41.1% + 3433 neg 58.9% = 5831 sched 100.0% ret 0
c [sweep-17-3] 6399570 steps 628 queries 51.46 avg class size
c [sweep-17-3] 11591 decisions 624 SAT calls 44.29 avg env size
c [sweep-17-3] fully completed sweeping round
c [decomp-78] removed 5 variables
c [sweep-17-3] removed 5 vars (0 failed, 7 eqs, 7 impls)
c [sweep-17] removed 27 vars in TOTAL (3 rounds, 1839 queries)
c [sort-queue-18] sorted 46 enqueued variables after 3491383 conflicts
c [score-dist-18] active 5780 (99%), one 0 (0%), zero 46 (1%)
c [score-dist-18] max exp 544, different 36 (7%)
c [score-dist-18] median active exp 533, avg 531.4
c [simplification-18] removed 32 variables 0.5% (5826 remain 19%)
c [simplification-18] removed 1116 irredundant clauses 3.4% (31816 remain 35%)
c [simplification-18] maximum reduction of 3% = max (1%, 3%)
c [simplification-18] geometric conflict interval increment 233982 = 935928 / 4
c [simplification-18] conflict interval soft limit 1000000 reached
c [simplification-18] new conflict interval 1000000
c [simplification-18] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-18] hard conflict limit 4991383 (soft 4491383 + delta 500000)
c [simplification-18] new conflict limit 4491383 (hard 4991383)
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 -  484.3    5826    31816   3569159   61049   8166 10894   26    52   25  50%   1024    7   30   30   99%
c -  494.4    5826    31816   3657310   61211   8168 10894   26    67   25  38%   1024   18   18   27   66%
c -  503.9    5826    31816   3733871   62489   8172 10894   24    60   25  39%   1024    1   21   26   79%
c -  513.0    5826    31816   3805591   62035   8175 10894   23    45   25  51%   1024  -14   22   24   92%
c -  524.3    5826    31816   3890974   64173   8175 10894   25    45   25  56%   1024   -8   21   28   74%
c -  532.7    5826    31816   3965854   64947   8178 10894   30    56   25  53%   1024    2   32   25  128%
c -  541.1    5826    31816   4042077   64754   8182 10894   22   167   25  13%   1024  105   21   23   91%
c i  542.0    5825    31815   4050900   72525   8187 10894   15   142   32  11%   1024   67   14   22   62%
c -  548.6    5825    31815   4117921   65145   8196 10894   12   154   36   8% -16146   50   11   18   62%
c -  558.9    5825    31813   4196579   65861   8200 10894   27    53   36  52%  -4146  -22   28   21  132%
c -  570.7    5825    31813   4280893   67772   8202 10894   26    48   36  54%   -404  -14   22   25   91%
c -  579.6    5825    31813   4357558   67508   8208 10895   24    60   37  41%    581    2   26   24  106%
c -  589.7    5825    31813   4436610   68089   8210 10895   28    44   37  64%    891   -9   27   25  106%
c 
c [simplification-19] limit 4491383 conflicts (hard 4991383) hit after 4491385 conflicts
c [quatres-17] found 9711 quaternary clauses 38% in total
c [quatres-17-1] removed 8 duplicate quaternary clauses
c [quatres-17-1] added 3 double-self-subsuming ternary resolvents
c [quatres-17-2] added 32 single-self-subsuming ternary resolvents
c [quatres-17-2] added 89 quaternary resolvents
c [ternres-17] limit 200000000 with penalty 0 = 0 + 0
c [ternres-17] all 5825 free variables schedulable
c [ternres-17] 483 ternary resolvents (41 bin, 442 trn)
c [ternres-17] fully completed ternary resolution
c [gauss-7] limit 3125000 penalty 4 = 4 + 0
c [gauss-7] extracted 3432 xors of average arity 3.0
c [gauss-7] connected 10324 occurrences of 676 variables (average 15.3)
c [gauss-7] limit 3125000 penalty 4 = 4 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-7] limit 28404627 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 11650 literals 100%
c [treelook-7] scheduling used 474876 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 28404627 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 5060935 steps
c [treelook-7] fully completed tree based probing
c [decomp-80] removed 2 variables
c [treelook-7] removed 4 variables, found 815 hbrs
c [unhide-13] limit 10000000 with penalty 1 = 1 + 0
c [unhide-13-64] 0 units, 0 failed, 1217 tauts, 0 hbrs, 259877 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 205 transitive binary clauses
c [cce-10] limit of 710115684 steps penalty 1 = 1 + 0
c [cce-10-1] eliminated 2 clauses out of 737 (0%) of length 7
c [cce-10-1] eliminated 1 clauses out of 1627 (0%) of length 6
c [cce-10-1] eliminated 16 clauses out of 2751 (1%) of length 5
c [cce-10-1] eliminated 33 clauses out of 6293 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 52 large clauses in 19942834 steps
c [cce-10-1] allowing another 9971417 steps for small clauses
c [cce-10-1] scheduling 14687 clauses = 5428 binary + 9259 ternary
c [cce-10-1] tried to eliminate 14687 small clauses 100%
c [cce-10-1] eliminated 5 binary clauses 0%
c [cce-10-1] eliminated 60 ternary clauses 1%
c [cce-10-1] eliminated 65 small clauses 0%
c [cce-10-1] eliminated 65 small clauses in 29036019 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 117 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 9916945 steps for small clauses
c [cce-10-2] scheduling 14622 clauses = 5423 binary + 9199 ternary
c [cce-10-2] tried to eliminate 14622 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 117 covered clauses in TOTAL during 2 rounds
c [cce-10] 117 < 1/100 * 31757 = 317 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 5821 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 179 variables 3% in round 1 in 7908318 steps
c [elim-14-1] backward subsumption/strengthening limit 7908300
c [elim-14-1-1] backward checking 729 touched variables 13%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 2 and strengthened 7 clauses in 1859899 steps
c [elim-14-1] rescheduled 25 variables 0% by backward subsumption
c [elim-14-2] no variable eliminated in round 2 in 1488876 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 179 = 3% variables out of 5821 scheduled
c [bca-16] limit of 10000000 steps and 63313 added (scaled 2)
c [bca-16] 3533 out of 11286 literals actually usable 31%
c [bca-16] added 13 blocked clauses in 114282 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 2291 pos 40.6% + 3351 neg 59.4% = 5642 sched 100.0% ret 0
c [sweep-18-1] 8372532 steps 584 queries 48.56 avg class size
c [sweep-18-1] 12066 decisions 579 SAT calls 42.73 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-81] removed 6 variables
c [sweep-18-1] removed 6 vars (0 failed, 8 eqs, 8 impls)
c [sweep-18-2] 2289 pos 40.6% + 3347 neg 59.4% = 5636 sched 100.0% ret 0
c [sweep-18-2] 8704862 steps 581 queries 48.75 avg class size
c [sweep-18-2] 12812 decisions 579 SAT calls 43.79 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-82] removed 5 variables
c [sweep-18-2] removed 5 vars (0 failed, 7 eqs, 5 impls)
c [sweep-18-3] 2287 pos 40.6% + 3344 neg 59.4% = 5631 sched 100.0% ret 0
c [sweep-18-3] 7616196 steps 572 queries 40.16 avg class size
c [sweep-18-3] 11803 decisions 567 SAT calls 42.72 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-83] removed 4 variables
c [sweep-18-3] removed 4 vars (0 failed, 5 eqs, 5 impls)
c [sweep-18] removed 15 vars in TOTAL (3 rounds, 1734 queries)
c [sort-queue-19] sorted 38 enqueued variables after 4491385 conflicts
c [score-dist-19] active 5589 (99%), one 0 (0%), zero 38 (1%)
c [score-dist-19] max exp 545, different 37 (7%)
c [score-dist-19] median active exp 533, avg 532.0
c [simplification-19] removed 198 variables 3.4% (5627 remain 18%)
c [simplification-19] removed 578 irredundant clauses 1.8% (31235 remain 35%)
c [simplification-19] maximum reduction of 3% = max (3%, 2%)
c [simplification-19] geometric conflict interval increment 250000 = 1000000 / 4
c [simplification-19] conflict interval soft limit 1000000 reached
c [simplification-19] new conflict interval 1000000
c [simplification-19] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-19] hard conflict limit 5991385 (soft 5491385 + delta 500000)
c [simplification-19] new conflict limit 5491385 (hard 5991385)
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 -  607.3    5627    31235   4521911   67329   7716  9795   26    49   19  52%    988   -3   31   25  128%
c -  616.7    5627    31235   4603365   68117   7716  9795   22    49   26  45%   1014   -4   23   23  100%
c -  626.6    5627    31235   4681956   68941   7718  9795   28    51   28  54%   1021   -3   28   24  115%
c -  636.8    5627    31235   4766232   67936   7719  9795   28    51   28  55%   1023   -3   28   25  110%
c -  648.2    5627    31235   4856230   69379   7720  9795   26    54   28  48%   1024    2   26   25  104%
c -  659.4    5627    31235   4945587   71045   7720  9795   19    33   28  56%   1024  -10   19   22   86%
c -  669.8    5627    31235   5028606   72448   7720  9795   27    52   28  51%   1024    4   23   24   95%
c -  679.5    5627    31235   5111799   72408   7721  9795   19    55   28  35%   1024    2   18   22   85%
c -  691.2    5627    31235   5201249   70295   7721  9795   25    44   28  56%   1024   -5   25   24  104%
c -  703.2    5627    31235   5289194   71383   7724  9795   30   105   42  29%   1024   31   30   30  101%
c -  715.6    5627    31235   5375415   71556   7724  9795   24    89   42  27%   1024    7   27   29   93%
c -  727.6    5627    31235   5463131   70600   7724  9795   18    63   41  29%   1024  -11   18   22   81%
c -  739.3    5627    31235   5560965   74899   7724  9795   30    42   42  72%   1024  -12   24   22  107%
c 
c [simplification-20] limit 5491385 conflicts (hard 5991385) hit after 5576551 conflicts
c [quatres-18] found 9632 quaternary clauses 37% in total
c [quatres-18-1] removed 4 duplicate quaternary clauses
c [quatres-18-1] added 2 double-self-subsuming ternary resolvents
c [quatres-18-2] added 32 single-self-subsuming ternary resolvents
c [quatres-18-2] added 69 quaternary resolvents
c [ternres-18] limit 200000000 with penalty 0 = 0 + 0
c [ternres-18] all 5627 free variables schedulable
c [ternres-18] 814 ternary resolvents (61 bin, 753 trn)
c [ternres-18] fully completed ternary resolution
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 3379 sched 60%, 1 failed, 0 lifted, 299 hbrs
c [decomp-85] removed 2 variables
c [basicprobe-7-1] 3376 sched 60%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-7-2] 3376 sched 60%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-7-2] fully completed probing
c [basicprobe-7-2] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-7-2] removed 2 variables, found 308 hbrs
c [bate-5] eliminated 1 asymmetric tautologies during probing
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 241 transitive binary clauses
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 5625 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 12 variables 0% in round 1 in 7831199 steps
c [elim-15-1] backward subsumption/strengthening limit 7831100
c [elim-15-1-1] backward checking 100 touched variables 2%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 493034 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 12 = 0% variables out of 5625 scheduled
c [elim-15] 12 < 1/100 * 5625 = 56 considered unsuccessful
c [bca-17] limit of 10000000 steps and 63103 added (scaled 2)
c [bca-17] 3429 out of 11228 literals actually usable 31%
c [bca-17] added 10 blocked clauses in 94700 steps
c [sweep-19] limit 112400235 penalty 0 = 0 + 0
c [sweep-19-1] 2311 pos 41.2% + 3302 neg 58.8% = 5613 sched 100.0% ret 0
c [sweep-19-1] 6781016 steps 562 queries 36.18 avg class size
c [sweep-19-1] 10464 decisions 559 SAT calls 41.46 avg env size
c [sweep-19-1] fully completed sweeping round
c [sweep-19-1] removed 0 vars (0 failed, 2 eqs, 1 impls)
c [sweep-19-2] 2311 pos 41.2% + 3302 neg 58.8% = 5613 sched 100.0% ret 0
c [sweep-19-2] 7274826 steps 557 queries 47.58 avg class size
c [sweep-19-2] 10724 decisions 550 SAT calls 46.84 avg env size
c [sweep-19-2] fully completed sweeping round
c [decomp-88] removed 8 variables
c [sweep-19-2] removed 8 vars (0 failed, 9 eqs, 11 impls)
c [sweep-19-3] 2307 pos 41.2% + 3298 neg 58.8% = 5605 sched 100.0% ret 0
c [sweep-19-3] 7439004 steps 560 queries 36.77 avg class size
c [sweep-19-3] 11473 decisions 559 SAT calls 42.19 avg env size
c [sweep-19-3] fully completed sweeping round
c [decomp-89] removed 8 variables
c [sweep-19-3] removed 8 vars (0 failed, 10 eqs, 8 impls)
c [sweep-19] removed 16 vars in TOTAL (3 rounds, 1676 queries)
c [sort-queue-20] sorted 15 enqueued variables after 5576551 conflicts
c [score-dist-20] active 5582 (100%), one 0 (0%), zero 15 (0%)
c [score-dist-20] max exp 545, different 36 (7%)
c [score-dist-20] median active exp 534, avg 532.6
c [simplification-20] removed 30 variables 0.5% (5597 remain 18%)
c [simplification-20] removed 118 irredundant clauses 0.4% (31117 remain 35%)
c [simplification-20] maximum reduction of 1% = max (1%, 0%)
c [simplification-20] geometric conflict interval increment 500000 = 1000000 / 2
c [simplification-20] conflict interval soft limit 1000000 reached
c [simplification-20] new conflict interval 1000000
c [simplification-20] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-20] hard conflict limit 7076551 (soft 6576551 + delta 500000)
c [simplification-20] new conflict limit 6576551 (hard 7076551)
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 -  755.6    5597    31117   5661482   76836   8282  9765   34    39   27  88%   1024  -11   36   27  135%
c -  771.5    5597    31117   5768440   76921   8282  9765   29    40   27  74%   1024   -5   25   29   83%
c -  787.4    5597    31117   5877768   75916   8284  9765   32    34   28  95%   1024   -9   33   29  114%
c -  800.7    5597    31117   5978252   75486   8285  9765   31    54   27  57%   1024    4   34   26  129%
c -  813.6    5597    31117   6077344   76315   8285  9765   34    47   27  72%   1024   -8   37   26  140%
c -  827.0    5597    31117   6185005   77543   8287  9765   20    96   39  21%   1024   36   21   24   89%
c -  837.9    5597    31117   6273501   77180   8293  9765   14   208   39   7%   1024   34   13   19   67%
c -  851.4    5597    31117   6365509   79717   8297  9765   26   116   39  23%   1024  -50   24   18  132%
c -  863.6    5597    31117   6453884   77411   8297  9765   20    91   39  22%   1024  -24   18   21   87%
c -  878.3    5597    31117   6551249   77215   8299  9766   22    90   26  24%   1024   -7   21   23   93%
c -  893.2    5597    31117   6657002   79564   8299  9766   30    49   38  62%   1024  -20   38   24  160%
c -  905.5    5597    31117   6766633   82501   8299  9766   24    40   38  59%   1024   -7   31   25  125%
c 
c [simplification-21] limit 6576551 conflicts (hard 7076551) hit after 6769626 conflicts
c [quatres-19] found 9860 quaternary clauses 35% in total
c [quatres-19-1] added 1 double-self-subsuming ternary resolvents
c [quatres-19-2] added 13 single-self-subsuming ternary resolvents
c [quatres-19-2] added 44 quaternary resolvents
c [ternres-19] limit 200000000 with penalty 0 = 0 + 0
c [ternres-19] all 5597 free variables schedulable
c [ternres-19] 307 ternary resolvents (28 bin, 279 trn)
c [ternres-19] fully completed ternary resolution
c [card-6] limit 15132999 penalty 4 = 4 + 0
c [card-6] found 431 at-most-one constraints of average size 3.1
c [card-6] found 51 at-most-two constraints of average size 4.0
c [card-6] using previous limit 15132999 for elimination
c [card-6] 481 out of 482 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] generated 48 at-most-one constraints, 16 used 33%
c [card-6] exported 16 binary clauses, 1.0 per/constraint
c [simpleprobe-8] all 5597 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-91] removed 4 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 4 variables, found 931 hbrs, 1 units
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 513 transitive binary clauses
c [cce-11] limit of 536870911 steps penalty 2 = 2 + 0
c [cce-11-1] eliminated 1 clauses out of 81 (1%) of length 11
c [cce-11-1] eliminated 10 clauses out of 149 (7%) of length 10
c [cce-11-1] eliminated 6 clauses out of 293 (2%) of length 9
c [cce-11-1] eliminated 6 clauses out of 387 (2%) of length 8
c [cce-11-1] eliminated 8 clauses out of 744 (1%) of length 7
c [cce-11-1] eliminated 24 clauses out of 1636 (1%) of length 6
c [cce-11-1] eliminated 45 clauses out of 2759 (2%) of length 5
c [cce-11-1] eliminated 83 clauses out of 6228 (1%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 183 large clauses in 46351795 steps
c [cce-11-1] allowing another 23175897 steps for small clauses
c [cce-11-1] scheduling 9729 clauses = 5226 binary + 4503 ternary
c [cce-11-1] tried to eliminate 9729 small clauses 100%
c [cce-11-1] eliminated 21 binary clauses 0%
c [cce-11-1] eliminated 27 ternary clauses 1%
c [cce-11-1] eliminated 48 small clauses 0%
c [cce-11-1] eliminated 48 small clauses in 42418865 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 231 covered clauses in round 1
c [cce-11-2] eliminated 1 clauses out of 1612 (0%) of length 6
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 1 large clauses in 45045476 steps
c [cce-11-2] allowing another 22522738 steps for small clauses
c [cce-11-2] scheduling 9681 clauses = 5205 binary + 4476 ternary
c [cce-11-2] tried to eliminate 9681 small clauses 100%
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 1 covered clauses in round 2
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] allowing another 22440815 steps for small clauses
c [cce-11-3] scheduling 9681 clauses = 5205 binary + 4476 ternary
c [cce-11-3] tried to eliminate 9681 small clauses 100%
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 0 covered clauses in round 3
c [cce-11] eliminated 232 covered clauses in TOTAL during 3 rounds
c [cce-11] 232 < 1/100 * 31105 = 311 considered unsuccessful
c [bca-18] limit of 10000000 steps and 62564 added (scaled 2)
c [bca-18] 2384 out of 11188 literals actually usable 21%
c [bca-18] added 7 blocked clauses in 90447 steps
c [sweep-20] limit 145276793 penalty 0 = 0 + 0
c [sweep-20-1] 2325 pos 41.6% + 3268 neg 58.4% = 5593 sched 100.0% ret 0
c [sweep-20-1] 7502039 steps 542 queries 62.08 avg class size
c [sweep-20-1] 12194 decisions 540 SAT calls 45.82 avg env size
c [sweep-20-1] fully completed sweeping round
c [decomp-92] removed 4 variables
c [sweep-20-1] removed 4 vars (0 failed, 4 eqs, 6 impls)
c [sweep-20-2] 2323 pos 41.6% + 3266 neg 58.4% = 5589 sched 100.0% ret 0
c [sweep-20-2] 6420400 steps 568 queries 54.85 avg class size
c [sweep-20-2] 11393 decisions 568 SAT calls 41.53 avg env size
c [sweep-20-2] fully completed sweeping round
c [decomp-93] removed 4 variables
c [sweep-20-2] removed 4 vars (0 failed, 4 eqs, 2 impls)
c [sweep-20-3] 2322 pos 41.6% + 3263 neg 58.4% = 5585 sched 100.0% ret 0
c [sweep-20-3] 7448891 steps 546 queries 34.68 avg class size
c [sweep-20-3] 11353 decisions 548 SAT calls 44.18 avg env size
c [sweep-20-3] fully completed sweeping round
c [sweep-20-3] removed 0 vars (0 failed, 0 eqs, 3 impls)
c [sweep-20] removed 8 vars in TOTAL (3 rounds, 1653 queries)
c [sort-queue-21] sorted 9 enqueued variables after 6769626 conflicts
c [score-dist-21] active 5576 (100%), one 0 (0%), zero 9 (0%)
c [score-dist-21] max exp 546, different 30 (5%)
c [score-dist-21] median active exp 536, avg 534.9
c [simplification-21] removed 12 variables 0.2% (5585 remain 18%)
c [simplification-21] removed 247 irredundant clauses 0.8% (30870 remain 34%)
c [simplification-21] maximum reduction of 1% = max (0%, 1%)
c [simplification-21] geometric conflict interval increment 500000 = 1000000 / 2
c [simplification-21] conflict interval soft limit 1000000 reached
c [simplification-21] new conflict interval 1000000
c [simplification-21] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-21] hard conflict limit 8269626 (soft 7769626 + delta 500000)
c [simplification-21] new conflict limit 7769626 (hard 8269626)
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  932.4    5584    30870   6843106  142227   8639  9510   19    63   48  31%   1024   16   17   24   70%
c -  935.8    5584    30868   6864953   82184   8640  9510   24    60   27  39% -30732   10   29   24  121%
c -  949.7    5584    30868   6973907   82990   8640  9510   24    40   28  61%  -4999   -4   22   26   85%
c -  962.2    5584    30867   7078894   81641   8642  9510   25    66   27  38%   -190   -8   16   23   71%
c -  975.7    5584    30867   7189547   83101   8642  9510   27    38   40  69%    800   -9   20   27   74%
c -  992.9    5584    30867   7320813   85611   8645  9510   27    34   40  79%    994   -2   31   28  111%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 24 basic ate = 13 trn 54% + 11 lrg 46% in 5 updates
c bcas: 18 count, 644 added (121 skipped), 1146471 steps
c bkwd: tried 83807 clauses, 167472 lits, 2.00 lits/clause
c bkwd: checked 21833590 occs, 260.52 occs/clause, 130.37 occs/lit
c bkwd: subsumed 5 binary, 13 ternary, 30 large
c bkwd: strengthened 0 binary, 2 ternary (100% self), 218 large (0% self)
c blkd: 6 bces, 1965 removed, 1248297 resolutions, 3140008 steps
c blkd: 1165 blocking literals 2%, 28 pure
c bump: 7377061 bumped seen, 694899281 lits 94.2 on average
c card: 6 count, 1 units, 38 am1, 418903861 steps
c card: 73 rescheduled, 695 eliminated, 259089 resolved, 6201 subsumed
c card: 1742 at-most-one constraints found, average size 3.22
c card: 1742 at-most-one constraints used 100%, average size 3.22
c card: 137 at-most-two constraints found, average size 4.02
c card: 135 at-most-two constraints used 99%, average size 4.02
c cces: 11 cces, 5382 eliminated, 4941 ate 92%, 441 abce 8%
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: 135 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 94 decompositions, 1689 equivalent 5%
c deco: 312 decision-only clauses 0%, 54% reduction
c decs: 42823805 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 23233 eliminated 75%, 66 pure 0%
c elms: 42 rounds, 2.8 rounds/bve
c elms: 22039 small 95%, 1100 large 5%
c elms: 49875 tried small, 22039 succeeded 44%, 27836 failed 56%
c elms: 1597 subsumed, 2140 strengthened, 223 blocked
c elms: 3557498 copies, 4769966 resolutions, 1767776 ipos
c elms: 1693829 subchks, 1077712 strchks
c gaus: 7 extractions, 25189 extracted, 3.0 size, 4 max
c gaus: exported 0 units, 0 binary and 17 ternary equations
c gaus: 0 gc, 16385020 steps, 8192510 extr 50%, 1079636 elim 7%
c glue: 27.3 orig avg, 27.3 real avg, 5.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 38336 = 8522 simple 22% + 24392 trn 64% + 5422 lrg 14%, 519 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 7377060 clauses, 40.8 length
c lrnd: 301068543 lits = 470098764 orig - 169030221 removed 36%
c lrnd: 978725 uips 13%, 3018695 flips 41%
c mins: 7370155 mins 100%, 274 bin 0%, 6319 size 0%
c mins: 182746472 poisoned searches, 17469933 hits, 10% hit rate
c mins: 627884584 used twice searches, 121575046 hits, 19% hit rate
c move: moved 3415, 907 bin 27%, 2508 trn 73%
c otfs: 28433 driving 28%, 74928 restarting 72%
c otfs: str 103361, 103129 red 100%, 232 irr 0%
c otfs: str 103361, 0 bin 0%, 339 trn 0%, 103022 lrg 100%
c otfs: sub 8496, 8444 red 99%, 52 irr 1%
c otfs: sub 8496, 0 bin 0%, 30 trn 0%, 8466 lrg 100%
c phas: 1 computed, 8137 set, 2231 pos (27%), 5906 neg (73%)
c prbs: 7 basic, 158475 probed, 65 failed, 7 lifted
c prbs: 8 simple, 150650 probed, 110 failed, 1962 eqs
c prbs: 7 treelook, 25520 probed, 19 failed, 0 lifted
c prom: 346679 locked 2% out of 18001627 tried
c prps: 1143483359 props, 26 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 19 count, 2015 quat, 486 self1, 45 self2, 215 dup
c queu: 21 sorted, 42823805 next (1726857 steps 0.04)
c queu: 694950488 enq (995698790 steps 1.43), 694899287 deq 100%
c redc: 6256 clauses 10%, 63542 tried 1%, 1 sat 0%
c redc: 9338 lits 1%, 808988 tried 0%, 1 sat 0%
c redc: 277 times jump level reduced, 18.9 levels on average
c reds: 98 count, 75354.1 conflicts per reduce
c reds: 0 memlim 0%, 98 arith 100%
c reds: 4826696 collected 93%, 390575 retired 7%
c rmbd: 1580 removed, 1268 red 80%
c rsts: 26315 restarts 93%, 1939 skipped 7%
c rsts: 1939 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 21 count, 21 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 7377060 count (9392967 tried 1.3), 2001296 sub out of 7373873 (27.1%)
c swps: 20 count, 42 rounds, 20241 queries (481.9/round)
c swps: 20105 sat calls, 494 unsat (1.0% success rate)
c swps: 389110 decisions 19.4, 20796 conflicts 1.0
c swps; 57.8 avg class size, 41.8 avg environment size
c swps: 0 failed, 516 impls, 617 equivs
c swp0: 6731 type 0 queries, 806 unsat (12.0%), 6623 sat (98.4%)
c swp1: 13510 type 1 queries, 2801 unsat (20.7%), 13001 sat (96.2%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 100402266 calls to obtain time
c tops: 314 fixed 1%, 11 its, 671336.18 confs/it
c trds: 19 transitive reductions, 6306 removed, 9 failed
c trds: 198613 nodes, 228654 edges, 29800236 steps
c trim: 10273241 words, 39.2 MB
c trnr: 19 count, 659 bin, 12999 trn, 87654735 steps
c unhd: 13 count, 64 rounds, 66199504 steps
c unhd: 124 non-trivial sccs of average size 2.0
c unhd: 5 units, 5 bin, 0 trn, 0 lrg
c unhd: 28 failed, 27 stamp, 0 lits, 1 bin, 0 trn, 0 lrg
c unhd: 10583 tauts, 336 bin 3%, 2674 trn 25%, 861 lrg 8%
c unhd: 10583 tauts, 6712 stamp 63%, 10466 red 99%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 888019 str, 5 bin 0%, 462 trn 0%, 887552 lrg 100%, 885678 red 100%
c vars: 5587 remaining 18% and 25236 removed 82% out of 30823
c vars: 314 fixed 1%, 23233 eliminated 75%, 1689 equivalent 5%
c vsts: 54572703851 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 48.2 search visits per propagation, 7356.0 per conflict
c wchs: 7477892251 pushed, 18956838 enlarged, 251 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        7375888       4826696        390575     189312811      98369969       4634762
c 
c  0 0         25003   0      2249   0         0   0  75933462  40  24870920  25    541743  12     0.6
c  1 5         17195   0      6173   0      8461   2  18522637  10   7927702   8    233653   5     0.1
c  2 6        130305   2     79116   2     37955  10  32990636  17< 17481605  18<   803553  17     1.4
c  3 9        602211   8    447191   9     87796  22  25518185  13  16661523  17   1089912  24<    4.8
c  4 14      1633669  22   1260705  26    107570  28< 17437136   9  13689088  14   1021593  22     8.2
c  5 21      2061729  28<  1509849  31<    82857  21  12901722   7  12154488  12    765369  17     9.1
c  6 30      2117826  29   1103516  23     54236  14   4614286   2   4307126   4    149247   3    22.8
c  7 41       537922   7    262406   5      8932   2   1011300   1    944435   1     23347   1    10.8
c  8 54       191748   3    112337   2      2241   1    303670   0    268177   0      5579   0     9.4
c  9 69        57384   1     42931   1       458   0     78055   0     64030   0       760   0     5.7
c 10 86          803   0       218   0        56   0      1578   0       807   0         6   0     0.2
c 11 126          93   0         5   0        13   0       144   0        68   0         0   0     0.0
c 
c avg                  5.1           4.9           4.1           1.8           2.5           3.0
c std                  1.3           1.3           1.4           1.8           1.9           1.6
c 
c   85.235   9% bump
c   33.283   3% cce
c   28.927   3% decide
c   17.687   2% unhide
c   12.114   1% sweep
c    8.602   1% card
c 
c   14.782 < 1% rest (below)
c 
c    5.018   1% elim
c    4.933   0% probe
c    1.874   0% transred
c    0.713   0% bca
c    0.689   0% ternres
c    0.662   0% quatres
c    0.547   0% gauss
c    0.345   0% block
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.858   0% preprocessing     1%
c   87.272   9% inprocessing     99%
c ==================================
c   88.130   9% simplifying
c  911.872  91% search
c ==================================
c 1000.003 100% all
c 
c       7384698 conflicts,        7384.7 confs/sec
c           605 ternaries,       12206.1 confs/ternary
c            85 binaries,        86878.8 confs/binary
c            11 iterations,     671336.2 confs/iteration
c 
c            98 reductions,          0.1 redus/sec,  75354.1 confs/reduction
c         26315 restarts,           26.3 rests/sec,    280.6 confs/restart
c      42823805 decisions,       42823.7 decis/sec,      5.8 decis/conflict
c    1143483359 propagations,  1143480.4 props/sec,     26.7 props/decision
c 
c 1000.0 seconds, 76.5 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
