c launch: /data/cnf/sc2014/app/6s16-opt.cnf.bz2
c host: atom14
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=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 30819 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] INC (--score=1)
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 1001 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] 1613 variables remain 20% (6514 retained 80%)
c [simpleprobe-2] removed 2 variables, found 603 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 189576 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 303918 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] 3103 probes remain 38% after last round
c [basicprobe-1-0] removed 0 variables, found 3826 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 8127 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 1744 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 784 (8%) of length 7
c [cce-1-1] eliminated 192 clauses out of 2036 (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 28427298 steps
c [cce-1-1] allowing another 14213649 steps for small clauses
c [cce-1-1] scheduling 13785 clauses = 8089 binary + 5696 ternary
c [cce-1-1] tried to eliminate 5214 small clauses 38%
c [cce-1-1] eliminated 38 binary clauses 0%
c [cce-1-1] eliminated 120 ternary clauses 2%
c [cce-1-1] eliminated 158 small clauses 1%
c [cce-1-1] eliminated 158 small clauses in 30000007 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1182 covered clauses in round 1
c [cce-1] eliminated 1182 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 8124 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 534 variables 7% in round 1 in 6405764 steps
c [elim-2-1] backward subsumption/strengthening limit 6405700
c [elim-2-1-1] backward checking 2880 touched variables 35%
c [elim-2-1-1] incomplete backward checking 2833 remain 98%
c [elim-2-1] subsumed 7 and strengthened 13 clauses in 6406553 steps
c [elim-2-1] rescheduled 81 variables 1% by backward subsumption
c [elim-2-2] eliminated 7 variables 0% in round 2 in 114035 steps
c [elim-2-2] backward subsumption/strengthening limit 114000
c [elim-2-2-1] backward checking 2844 touched variables 35%
c [elim-2-2-1] incomplete backward checking 2842 remain 100%
c [elim-2-2] subsumed 0 and strengthened 0 clauses in 114680 steps
c [elim-2-2] fully rescheduled 7583 variables 93%
c [elim-2-3] eliminated 20 variables 0% in round 3 in 6251532 steps
c [elim-2-3] backward subsumption/strengthening limit 707436
c [elim-2-3-1] backward checking 2860 touched variables 35%
c [elim-2-3-1] incomplete backward checking 2799 remain 98%
c [elim-2-3] subsumed 0 and strengthened 3 clauses in 708570 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 561 = 7% variables out of 8124 scheduled
c [bca-1] limit of 10000000 steps and 81678 added (scaled 2)
c [bca-1] 13370 out of 15128 literals actually usable 88%
c [bca-1] added 526 blocked clauses in 36412 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3256 pos 43.1% + 4307 neg 56.9% = 7563 sched 100.0% ret 0
c [sweep-1-1] 1021325 steps 191 queries 490.26 avg class size
c [sweep-1-1] 2698 decisions 187 SAT calls 28.85 avg env size
c [sweep-1-1] 4852 variables remain 64% (2710 retained 36%)
c [decomp-6] removed 21 variables
c [sweep-1-1] removed 21 vars (0 failed, 8 eqs, 7 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 21 vars in TOTAL (1 rounds, 190 queries)
c [sort-queue-2] sorted 4740 enqueued variables after 1001 conflicts
c [score-dist-2] active 2802 (37%), one 0 (0%), zero 4740 (63%)
c [score-dist-2] max exp 511, different 10 (2%)
c [score-dist-2] median active exp 504, avg 504.2
c [simplification-2] removed 595 variables 7.3% (7542 remain 24%)
c [simplification-2] removed 3603 irredundant clauses 8.2% (40562 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 13001 (soft 3001 + delta 10000)
c [simplification-2] new conflict limit 3001 (hard 13001)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    2.6    7541    40562      1604    1242    797  6790    3    51    6   6%     12   51    9    0 4168%
c i    2.7    7540    40562      2422    1854    831  6796    4    88    7   5%      9   87   10    0 3112%
c i    2.7    7539    40562      2423    1854    831  6796    4    88    7   5%      9   87   10    0 3100%
c i    2.7    7538    40562      2425    1854    831  6797    4    88    7   5%      9   87   10    0 3077%
c 
c [simplification-3] limit 3016 conflicts (hard 13001) hit after 3017 conflicts
c [quatres-1] found 7835 quaternary clauses 49% in total
c [quatres-1-2] added 17 single-self-subsuming ternary resolvents
c [quatres-1-2] added 608 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 7538 free variables schedulable
c [ternres-1] 4418 ternary resolvents (58 bin, 4360 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 349 at-most-one constraints of average size 3.5
c [card-2] found 38 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 386 out of 387 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 14 at-most-one constraints, 8 used 57%
c [card-2] exported 9 binary clauses, 1.1 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 4349 xors of average arity 3.0
c [gauss-1] connected 13035 occurrences of 897 variables (average 14.5)
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 13 variables
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 761 tauts, 0 hbrs, 2506 literals
c [transred-1] limit 119253 with penalty 0 = 0 + 0
c [transred-1] removed 43 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 7525 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 6 blocked clauses
c [block-2] 6 < 1/100 * 40507 = 405 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 2 clauses out of 94 (2%) of length 13
c [cce-2-1] eliminated 3 clauses out of 127 (2%) of length 10
c [cce-2-1] eliminated 10 clauses out of 258 (4%) of length 9
c [cce-2-1] eliminated 20 clauses out of 437 (5%) of length 8
c [cce-2-1] eliminated 51 clauses out of 1004 (5%) of length 7
c [cce-2-1] eliminated 98 clauses out of 2041 (5%) of length 6
c [cce-2-1] eliminated 109 clauses out of 3394 (3%) of length 5
c [cce-2-1] eliminated 310 clauses out of 7677 (4%) of length 4
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 603 large clauses in 30000007 steps
c [cce-2-1] allowing another 15000003 steps for small clauses
c [cce-2-1] scheduling 12895 clauses = 7402 binary + 5493 ternary
c [cce-2-1] tried to eliminate 4787 small clauses 37%
c [cce-2-1] eliminated 49 binary clauses 1%
c [cce-2-1] eliminated 73 ternary clauses 1%
c [cce-2-1] eliminated 122 small clauses 1%
c [cce-2-1] eliminated 122 small clauses in 30000007 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 725 covered clauses in round 1
c [cce-2] eliminated 725 covered clauses in TOTAL during 1 rounds
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 7525 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 65 variables 1% in round 1 in 7144612 steps
c [elim-3-1] backward subsumption/strengthening limit 7144600
c [elim-3-1-1] backward checking 577 touched variables 8%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 1 and strengthened 3 clauses in 930639 steps
c [elim-3-1] rescheduled 13 variables 0% by backward subsumption
c [elim-3-2] no variable eliminated in round 2 in 13609 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 65 = 1% variables out of 7525 scheduled
c [elim-3] 65 < 1/100 * 7525 = 75 considered unsuccessful
c [bca-2] limit of 10000000 steps and 80091 added (scaled 2)
c [bca-2] 9283 out of 14922 literals actually usable 62%
c [bca-2] added 0 blocked clauses in 25511 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2049 pos 42.8% + 2736 neg 57.2% = 4785 sched 64.1% ret 2675
c [sweep-2-1] 1001784 steps 172 queries 224.27 avg class size
c [sweep-2-1] 2324 decisions 166 SAT calls 28.08 avg env size
c [sweep-2-1] 3324 variables remain 45% (4134 retained 55%)
c [decomp-8] removed 21 variables
c [sweep-2-1] removed 21 vars (0 failed, 14 eqs, 18 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 21 vars in TOTAL (1 rounds, 171 queries)
c [sort-queue-3] sorted 1721 enqueued variables after 3017 conflicts
c [score-dist-3] active 5718 (77%), one 0 (0%), zero 1721 (23%)
c [score-dist-3] max exp 512, different 11 (2%)
c [score-dist-3] median active exp 505, avg 504.9
c [simplification-3] removed 99 variables 1.3% (7439 remain 24%)
c [simplification-3] removed 908 irredundant clauses 2.2% (39654 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 19683 (soft 9683 + delta 10000)
c [simplification-3] new conflict limit 9683 (hard 19683)
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.7    7438    39654      6791    6228   4810  6482   13   163    8   8%     51  153   19    1 1436%
c i    4.9    7437    39654      8458    7566   4818  6483   16   146    8  11%     21  133   15    2  822%
c 
c [simplification-4] limit 9683 conflicts (hard 19683) hit after 9684 conflicts
c [quatres-2] found 8281 quaternary clauses 50% in total
c [quatres-2-2] added 13 single-self-subsuming ternary resolvents
c [quatres-2-2] added 241 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 7437 free variables schedulable
c [ternres-2] 454 ternary resolvents (40 bin, 414 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 4438 xors of average arity 3.0
c [gauss-2] connected 13294 occurrences of 874 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 0 ternary equations
c [decomp-9] removed 15 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 11493 literals 77%
c [treelook-2] scheduling used 150010 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 162141 steps
c [treelook-2] 11483 literals remain 77%
c [treelook-2] 7125 variables remain to probed next time 96%
c [treelook-2] removed 0 variables, found 466 hbrs
c [transred-2] limit 385292 with penalty 0 = 0 + 0
c [transred-2] removed 138 transitive binary clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 4 clauses out of 68 (6%) of length 11
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 4 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3-1] scheduling 19414 clauses = 7256 binary + 12158 ternary
c [cce-3-1] tried to eliminate 2777 small clauses 14%
c [cce-3-1] eliminated 8 binary clauses 0%
c [cce-3-1] eliminated 73 ternary clauses 1%
c [cce-3-1] eliminated 81 small clauses 0%
c [cce-3-1] eliminated 81 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 85 covered clauses in round 1
c [cce-3] eliminated 85 covered clauses in TOTAL during 1 rounds
c [cce-3] 85 < 1/100 * 39632 = 396 considered unsuccessful
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1601 pos 48.4% + 1707 neg 51.6% = 3308 sched 44.6% ret 4114
c [sweep-3-1] 1010118 steps 163 queries 217.51 avg class size
c [sweep-3-1] 2702 decisions 155 SAT calls 34.74 avg env size
c [sweep-3-1] 2179 variables remain 29% (5243 retained 71%)
c [decomp-11] removed 21 variables
c [sweep-3-1] removed 21 vars (0 failed, 14 eqs, 17 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 21 vars in TOTAL (1 rounds, 162 queries)
c [sort-queue-4] sorted 1235 enqueued variables after 9684 conflicts
c [score-dist-4] active 6166 (83%), one 0 (0%), zero 1235 (17%)
c [score-dist-4] max exp 514, different 14 (3%)
c [score-dist-4] median active exp 507, avg 506.5
c [simplification-4] removed 36 variables 0.5% (7401 remain 24%)
c [simplification-4] removed 112 irredundant clauses 0.3% (39542 remain 44%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 26666
c [simplification-4] penalized conflict interval 26666 = 1 * 26666
c [simplification-4] hard conflict limit 49683 (soft 36350 + delta 13333)
c [simplification-4] new conflict limit 36350 (hard 49683)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    8.9    7400    39540     10565    9655   5091  7260   16   176    9   9%     19  158   15    2  625%
c i    8.9    7399    39540     10596    9683   5092  7260   16   177    9   9%     18  158   14    2  594%
c i    8.9    7398    39540     10667    9738   5093  7260   16   177    9   9%     17  158   13    2  568%
c 
c [simplification-5] limit 36350 conflicts (hard 49683) hit after 36352 conflicts
c [quatres-3] found 8651 quaternary clauses 49% in total
c [quatres-3-1] removed 3 duplicate quaternary clauses
c [quatres-3-1] added 3 double-self-subsuming ternary resolvents
c [quatres-3-2] added 20 single-self-subsuming ternary resolvents
c [quatres-3-2] added 115 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 7398 free variables schedulable
c [ternres-3] 246 ternary resolvents (15 bin, 231 trn)
c [ternres-3] fully completed ternary resolution
c [decomp-12] removed 6 variables
c [transred-3] limit 1478682 with penalty 0 = 0 + 0
c [transred-3] removed 473 transitive binary clauses
c [transred-3] found 5 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 7390 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 0 blocked clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 7390 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 295736460 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 51 variables 1% in round 1 in 7657697 steps
c [elim-4-1] backward subsumption/strengthening limit 7657600
c [elim-4-1-1] backward checking 350 touched variables 5%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 10 and strengthened 8 clauses in 1902241 steps
c [elim-4-1] rescheduled 24 variables 0% by backward subsumption
c [elim-4-2] eliminated 2 variables 0% in round 2 in 16136 steps
c [elim-4-2] backward subsumption/strengthening limit 16100
c [elim-4-2-1] backward checking 11 touched variables 0%
c [elim-4-2-1] incomplete backward checking 10 remain 91%
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 16108 steps
c [elim-4-2] fully rescheduled 7336 variables 99%
c [elim-4-3] eliminated 6 variables 0% in round 3 in 7626428 steps
c [elim-4-3] backward subsumption/strengthening limit 7626400
c [elim-4-3-1] backward checking 64 touched variables 1%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 0 and strengthened 4 clauses in 628485 steps
c [elim-4] incomplete 19 not tried 0% in round 3
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 60 = 1% variables out of 7390 scheduled
c [elim-4] 60 < 1/100 * 7390 = 73 considered unsuccessful
c [bca-3] limit of 10000000 steps and 79243 added (scaled 2)
c [bca-3] 6256 out of 14662 literals actually usable 43%
c [bca-3] added 0 blocked clauses in 42560 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 958 pos 44.6% + 1188 neg 55.4% = 2146 sched 29.3% ret 5184
c [sweep-4-1] 1203035 steps 100 queries 188.97 avg class size
c [sweep-4-1] 3208 decisions 95 SAT calls 81.17 avg env size
c [sweep-4-1] 1640 variables remain 22% (5690 retained 78%)
c [decomp-13] removed 29 variables
c [sweep-4-1] removed 29 vars (0 failed, 23 eqs, 26 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 29 vars in TOTAL (1 rounds, 99 queries)
c [sort-queue-5] sorted 955 enqueued variables after 36352 conflicts
c [score-dist-5] active 6346 (87%), one 0 (0%), zero 955 (13%)
c [score-dist-5] max exp 516, different 16 (3%)
c [score-dist-5] median active exp 508, avg 508.1
c [simplification-5] removed 97 variables 1.3% (7301 remain 24%)
c [simplification-5] removed 317 irredundant clauses 0.8% (39219 remain 44%)
c [simplification-5] maximum reduction of 1% = max (1%, 1%)
c [simplification-5] geometric conflict interval increment 13333 = 26666 / 2
c [simplification-5] new conflict interval 39999
c [simplification-5] penalized conflict interval 39999 = 1 * 39999
c [simplification-5] hard conflict limit 96350 (soft 76351 + delta 19999)
c [simplification-5] new conflict limit 76351 (hard 96350)
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 -   18.3    7301    39218     66237   26170   5159  7031   47   117   11  40%    577   37   64   26  241%
c 
c [simplification-6] limit 76351 conflicts (hard 96350) hit after 76351 conflicts
c [quatres-4] found 8826 quaternary clauses 48% in total
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 10 single-self-subsuming ternary resolvents
c [quatres-4-2] added 52 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 7301 free variables schedulable
c [ternres-4] 794 ternary resolvents (40 bin, 754 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 341 at-most-one constraints of average size 3.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 341 out of 341 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 3815 xors of average arity 3.0
c [gauss-3] connected 11416 occurrences of 832 variables (average 13.7)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 7 ternary equations
c [decomp-14] removed 4 variables
c [basicprobe-2] limit 8013308 penalty 1 = 1 + 0
c [basicprobe-2-0] 2964 sched 41%, 30 failed, 1 lifted, 5863 hbrs
c [decomp-15] removed 59 variables
c [basicprobe-2-1] 4305 sched 60%, 21 failed, 0 lifted, 2918 hbrs
c [decomp-16] removed 29 variables
c [basicprobe-2-2] 2813 probes remain 39% after last round
c [basicprobe-2-2] 52 units = 51 failed (98%) + 1 lifted (2%)
c [basicprobe-2-2] removed 88 variables, found 8807 hbrs
c [bate-1] eliminated 12 asymmetric tautologies during probing
c [unhide-3] limit 160266 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 128 tauts, 0 hbrs, 31292 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 611 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 150000000 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 1 clauses out of 81 (1%) of length 11
c [cce-4-1] eliminated 5 clauses out of 129 (4%) of length 10
c [cce-4-1] eliminated 8 clauses out of 403 (2%) of length 8
c [cce-4-1] eliminated 1 clauses out of 946 (0%) of length 7
c [cce-4-1] eliminated 12 clauses out of 1952 (1%) of length 6
c [cce-4-1] eliminated 30 clauses out of 3250 (1%) of length 5
c [cce-4-1] eliminated 70 clauses out of 7450 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 127 large clauses in 30378104 steps
c [cce-4-1] allowing another 15189052 steps for small clauses
c [cce-4-1] scheduling 18929 clauses = 7087 binary + 11842 ternary
c [cce-4-1] tried to eliminate 18929 small clauses 100%
c [cce-4-1] eliminated 50 binary clauses 1%
c [cce-4-1] eliminated 429 ternary clauses 4%
c [cce-4-1] eliminated 479 small clauses 3%
c [cce-4-1] eliminated 479 small clauses in 48388811 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 606 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 14671040 steps for small clauses
c [cce-4-2] scheduling 18450 clauses = 7037 binary + 11413 ternary
c [cce-4-2] tried to eliminate 18450 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 606 covered clauses in TOTAL during 2 rounds
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 676 pos 42.4% + 918 neg 57.6% = 1594 sched 22.1% ret 5615
c [sweep-5-1] 3990641 steps 531 queries 33.61 avg class size
c [sweep-5-1] 8876 decisions 490 SAT calls 36.66 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-17] removed 101 variables
c [sweep-5-1] removed 101 vars (0 failed, 102 eqs, 94 impls)
c [sweep-5-2] 2856 pos 40.2% + 4252 neg 59.8% = 7108 sched 100.0% ret 0
c [sweep-5-2] 6059552 steps 602 queries 111.77 avg class size
c [sweep-5-2] 10755 decisions 566 SAT calls 42.34 avg env size
c [sweep-5-2] 690 variables remain 10% (6418 retained 90%)
c [decomp-18] removed 86 variables
c [sweep-5-2] removed 86 vars (0 failed, 90 eqs, 71 impls)
c [sweep-5] removed 187 vars in TOTAL (2 rounds, 1131 queries)
c [sort-queue-6] sorted 616 enqueued variables after 76351 conflicts
c [score-dist-6] active 6406 (91%), one 0 (0%), zero 616 (9%)
c [score-dist-6] max exp 517, different 17 (3%)
c [score-dist-6] median active exp 509, avg 508.5
c [simplification-6] removed 279 variables 3.8% (7022 remain 23%)
c [simplification-6] removed 1060 irredundant clauses 2.7% (38158 remain 42%)
c [simplification-6] maximum reduction of 4% = max (4%, 3%)
c [simplification-6] geometric conflict interval increment 7999 = 39999 / 5
c [simplification-6] new conflict interval 47998
c [simplification-6] penalized conflict interval 47998 = 1 * 47998
c [simplification-6] hard conflict limit 148348 (soft 124349 + delta 23999)
c [simplification-6] new conflict limit 124349 (hard 148348)
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   23.8    7021    38152     88892   46270   5276 11972   16   110   19  15%    708   17   16   25   65%
c i   24.2    7020    38152     91704   48612   5280 11972   21   133   19  16%   -389   40   31   25  126%
c i   24.9    7019    38152     97991   54438   5283 11972   14   175   19   8%   -372   75   21   24   90%
c -   24.9    7019    38152     98475   28767   5284 11972   15   171   11   9%   -399   70   22   24   96%
c i   25.4    7018    38152    102336   32051   5288 11972   23   181   14  13%   -375   76   30   24  126%
c 
c [simplification-7] limit 124349 conflicts (hard 148348) hit after 126001 conflicts
c [quatres-5] found 8981 quaternary clauses 49% in total
c [quatres-5-1] removed 10 duplicate quaternary clauses
c [quatres-5-1] added 8 double-self-subsuming ternary resolvents
c [quatres-5-2] added 25 single-self-subsuming ternary resolvents
c [quatres-5-2] added 52 quaternary resolvents
c [ternres-5] limit 5159154 with penalty 0 = 0 + 0
c [ternres-5] all 7018 free variables schedulable
c [ternres-5] 947 ternary resolvents (48 bin, 899 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] extracted 4200 xors of average arity 3.0
c [gauss-4] connected 12560 occurrences of 844 variables (average 14.9)
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-19] removed 9 variables
c [simpleprobe-3] 1384 schedulable variables 20%
c [simpleprobe-3] limit 20636617 penalty 0 = 0 + 0
c [decomp-20] removed 37 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 37 variables, found 1230 hbrs, 4 units
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 849 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 12 clauses out of 888 (1%) of length 7
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 12 large clauses in 30000001 steps
c [cce-5-1] allowing another 15000000 steps for small clauses
c [cce-5-1] scheduling 18064 clauses = 6852 binary + 11212 ternary
c [cce-5-1] tried to eliminate 2809 small clauses 16%
c [cce-5-1] eliminated 22 binary clauses 0%
c [cce-5-1] eliminated 47 ternary clauses 0%
c [cce-5-1] eliminated 69 small clauses 0%
c [cce-5-1] eliminated 73 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 85 covered clauses in round 1
c [cce-5] eliminated 85 covered clauses in TOTAL during 1 rounds
c [cce-5] 85 < 1/100 * 37841 = 378 considered unsuccessful
c [sweep-6] limit 1547746 penalty 0 = 0 + 0
c [sweep-6-1] 280 pos 41.8% + 390 neg 58.2% = 670 sched 9.6% ret 6300
c [sweep-6-1] 1606138 steps 212 queries 43.71 avg class size
c [sweep-6-1] 3960 decisions 202 SAT calls 41.51 avg env size
c [sweep-6-1] 186 variables remain 3% (6784 retained 97%)
c [decomp-21] removed 35 variables
c [sweep-6-1] removed 35 vars (0 failed, 37 eqs, 32 impls)
c [sweep-6] removed 35 vars in TOTAL (1 rounds, 211 queries)
c [sort-queue-7] sorted 562 enqueued variables after 126001 conflicts
c [score-dist-7] active 6373 (92%), one 0 (0%), zero 562 (8%)
c [score-dist-7] max exp 518, different 18 (3%)
c [score-dist-7] median active exp 510, avg 509.2
c [simplification-7] removed 83 variables 1.2% (6935 remain 23%)
c [simplification-7] removed 420 irredundant clauses 1.1% (37732 remain 42%)
c [simplification-7] maximum reduction of 1% = max (1%, 1%)
c [simplification-7] geometric conflict interval increment 23999 = 47998 / 2
c [simplification-7] new conflict interval 71997
c [simplification-7] penalized conflict interval 71997 = 1 * 71997
c [simplification-7] hard conflict limit 233996 (soft 197998 + delta 35998)
c [simplification-7] new conflict limit 197998 (hard 233996)
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 -   32.6    6935    37732    130620   29380   5975 12250   43   129   12  33%     70    6   23   28   83%
c -   36.8    6935    37731    163220   27242   5979 12252   45   113   12  40%    444  -11   21   33   62%
c -   41.7    6935    37728    201427   28521   5991 12253   41   100   18  41%    700  -18   34   36   95%
c 
c [simplification-8] limit 197998 conflicts (hard 233996) hit after 229816 conflicts
c [quatres-6] found 9011 quaternary clauses 48% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-1] added 1 double-self-subsuming ternary resolvents
c [quatres-6-2] added 20 single-self-subsuming ternary resolvents
c [quatres-6-2] added 27 quaternary resolvents
c [ternres-6] limit 9635982 with penalty 0 = 0 + 0
c [ternres-6] all 6935 free variables schedulable
c [ternres-6] 456 ternary resolvents (23 bin, 433 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-22] removed 4 variables
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 478 transitive binary clauses
c [transred-6] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 6930 variables 100%
c [block-4] limit of 24089955 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 282 blocked clauses
c [block-4] 282 < 1/100 * 37656 = 376 considered unsuccessful
c [elim-5] no untried remaining variables left
c [elim-5] scheduled 6902 variables 100%
c [elim-5] limit of 48179911 steps penalty 2 = 2 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 237 variables 3% in round 1 in 9737972 steps
c [elim-5-1] backward subsumption/strengthening limit 9737900
c [elim-5-1-1] backward checking 1219 touched variables 18%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 2 and strengthened 35 clauses in 1021487 steps
c [elim-5-1] rescheduled 59 variables 1% by backward subsumption
c [elim-5-2] eliminated 3 variables 0% in round 2 in 71740 steps
c [elim-5-2] backward subsumption/strengthening limit 71700
c [elim-5-2-1] backward checking 27 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 0 and strengthened 0 clauses in 33141 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 240 = 3% variables out of 6902 scheduled
c [bca-4] limit of 10000000 steps and 73811 added (scaled 2)
c [bca-4] 5900 out of 13326 literals actually usable 44%
c [bca-4] added 15 blocked clauses in 62822 steps
c [sweep-7] limit 2890794 penalty 0 = 0 + 0
c [sweep-7-1] 65 pos 38.5% + 104 neg 61.5% = 169 sched 2.5% ret 6493
c [sweep-7-1] 490456 steps 104 queries 17.32 avg class size
c [sweep-7-1] 1618 decisions 96 SAT calls 29.73 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-23] removed 12 variables
c [sweep-7-1] removed 12 vars (1 failed, 12 eqs, 6 impls)
c [sweep-7-2] 2736 pos 41.1% + 3914 neg 58.9% = 6650 sched 100.0% ret 0
c [sweep-7-2] 2401168 steps 197 queries 139.70 avg class size
c [sweep-7-2] 5397 decisions 196 SAT calls 63.43 avg env size
c [sweep-7-2] 2964 variables remain 45% (3685 retained 55%)
c [decomp-24] removed 5 variables
c [sweep-7-2] removed 5 vars (0 failed, 5 eqs, 3 impls)
c [sweep-7] removed 17 vars in TOTAL (2 rounds, 299 queries)
c [sort-queue-8] sorted 448 enqueued variables after 229816 conflicts
c [score-dist-8] active 6197 (93%), one 0 (0%), zero 448 (7%)
c [score-dist-8] max exp 519, different 19 (4%)
c [score-dist-8] median active exp 510, avg 509.5
c [simplification-8] removed 290 variables 4.2% (6645 remain 22%)
c [simplification-8] removed 1225 irredundant clauses 3.2% (36502 remain 41%)
c [simplification-8] maximum reduction of 4% = max (4%, 3%)
c [simplification-8] geometric conflict interval increment 14399 = 71997 / 5
c [simplification-8] new conflict interval 86396
c [simplification-8] penalized conflict interval 86396 = 1 * 86396
c [simplification-8] hard conflict limit 359410 (soft 316212 + delta 43198)
c [simplification-8] new conflict limit 316212 (hard 359410)
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 -   47.6    6645    36502    242338   28499   5752 10486   25   104   12  24%    850   -7   25   34   72%
c -   52.2    6645    36502    280892   29911   5755 10486   22    62   17  36%    928  -37   21   28   73%
c 
c [simplification-9] limit 316212 conflicts (hard 359410) hit after 316213 conflicts
c [quatres-7] found 8906 quaternary clauses 46% in total
c [quatres-7-1] removed 4 duplicate quaternary clauses
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 12 single-self-subsuming ternary resolvents
c [quatres-7-2] added 75 quaternary resolvents
c [ternres-7] limit 14445720 with penalty 0 = 0 + 0
c [ternres-7] all 6645 free variables schedulable
c [ternres-7] 249 ternary resolvents (23 bin, 226 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-5] limit 1444572 penalty 1 = 1 + 0
c [gauss-5] extracted 3808 xors of average arity 3.0
c [gauss-5] connected 11436 occurrences of 773 variables (average 14.8)
c [gauss-5] limit 1444572 penalty 1 = 1 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-25] removed 2 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 310 transitive binary clauses
c [transred-7] found 4 units
c [cce-6] limit of 36114300 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 6 clauses out of 430 (1%) of length 8
c [cce-6-1] eliminated 15 clauses out of 843 (2%) of length 7
c [cce-6-1] eliminated 54 clauses out of 1905 (3%) of length 6
c [cce-6-1] eliminated 87 clauses out of 3229 (3%) of length 5
c [cce-6-1] eliminated 143 clauses out of 7287 (2%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 305 large clauses in 27856725 steps
c [cce-6-1] allowing another 13928362 steps for small clauses
c [cce-6-1] scheduling 11646 clauses = 6473 binary + 5173 ternary
c [cce-6-1] tried to eliminate 11646 small clauses 100%
c [cce-6-1] eliminated 53 binary clauses 1%
c [cce-6-1] eliminated 191 ternary clauses 4%
c [cce-6-1] eliminated 244 small clauses 2%
c [cce-6-1] eliminated 261 small clauses in 32825227 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 566 covered clauses in round 1
c [cce-6-2] incomplete large round (ATE)
c [cce-6-2] allowing another 1644551 steps for small clauses
c [cce-6-2] scheduling 11402 clauses = 6420 binary + 4982 ternary
c [cce-6-2] tried to eliminate 178 small clauses 2%
c [cce-6-2] incomplete small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 566 covered clauses in TOTAL during 2 rounds
c [sweep-8] limit 4333716 penalty 0 = 0 + 0
c [sweep-8-1] 1246 pos 42.1% + 1715 neg 57.9% = 2961 sched 44.6% ret 3678
c [sweep-8-1] 4510200 steps 513 queries 66.10 avg class size
c [sweep-8-1] 8644 decisions 510 SAT calls 35.39 avg env size
c [sweep-8-1] 296 variables remain 4% (6338 retained 96%)
c [decomp-26] removed 38 variables
c [sweep-8-1] removed 38 vars (0 failed, 35 eqs, 23 impls)
c [sweep-8] removed 38 vars in TOTAL (1 rounds, 512 queries)
c [sort-queue-9] sorted 391 enqueued variables after 316213 conflicts
c [score-dist-9] active 6210 (94%), one 0 (0%), zero 391 (6%)
c [score-dist-9] max exp 520, different 20 (4%)
c [score-dist-9] median active exp 510, avg 509.7
c [simplification-9] removed 44 variables 0.7% (6601 remain 21%)
c [simplification-9] removed 624 irredundant clauses 1.7% (35878 remain 40%)
c [simplification-9] maximum reduction of 2% = max (1%, 2%)
c [simplification-9] geometric conflict interval increment 28798 = 86396 / 3
c [simplification-9] new conflict interval 115194
c [simplification-9] penalized conflict interval 115194 = 1 * 115194
c [simplification-9] hard conflict limit 489004 (soft 431407 + delta 57597)
c [simplification-9] new conflict limit 431407 (hard 489004)
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 -   58.1    6601    35878    317774   29034   5896 10203   23   100   12  23%    969    5   23   26   90%
c -   64.5    6601    35878    354688   29142   5898 10203   20    75   12  27%    993  -15   21   24   84%
c -   71.1    6601    35878    394112   31597   5899 10203   22    51   18  42%   1007  -25   23   23   97%
c -   77.3    6601    35878    431453   33159   5899 10203   20    36   18  56%   1014  -27   20   22   90%
c 
c [simplification-10] limit 431407 conflicts (hard 489004) hit after 452727 conflicts
c [quatres-8] found 8909 quaternary clauses 46% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 21 single-self-subsuming ternary resolvents
c [quatres-8-2] added 31 quaternary resolvents
c [ternres-8] limit 25355358 with penalty 0 = 0 + 0
c [ternres-8] all 6601 free variables schedulable
c [ternres-8] 142 ternary resolvents (13 bin, 129 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 1584709 penalty 3 = 3 + 0
c [card-4] found 446 at-most-one constraints of average size 3.3
c [card-4] found 52 at-most-two constraints of average size 4.0
c [card-4] using previous limit 1584709 for elimination
c [card-4] 496 out of 498 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] generated 12 at-most-one constraints, 3 used 25%
c [card-4] exported 3 binary clauses, 1.0 per/constraint
c [decomp-27] removed 1 variables
c [treelook-3] limit 633883 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 12843 literals 97%
c [treelook-3] scheduling used 332945 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 633883 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 635619 steps
c [treelook-3] 12632 literals remain 96%
c [treelook-3] 6322 variables remain to probed next time 96%
c [treelook-3] removed 0 variables, found 453 hbrs
c [unhide-4] limit 633883 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 0 failed, 1001 tauts, 0 hbrs, 99757 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 208 transitive binary clauses
c [cce-7] limit of 126776792 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 2 clauses out of 831 (0%) of length 7
c [cce-7-1] eliminated 20 clauses out of 1808 (1%) of length 6
c [cce-7-1] eliminated 55 clauses out of 3149 (2%) of length 5
c [cce-7-1] eliminated 152 clauses out of 7106 (2%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 229 large clauses in 104429699 steps
c [cce-7-1] allowing another 52214849 steps for small clauses
c [cce-7-1] scheduling 16830 clauses = 6403 binary + 10427 ternary
c [cce-7-1] tried to eliminate 16830 small clauses 100%
c [cce-7-1] eliminated 117 binary clauses 2%
c [cce-7-1] eliminated 249 ternary clauses 2%
c [cce-7-1] eliminated 366 small clauses 2%
c [cce-7-1] eliminated 366 small clauses in 108580551 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 595 covered clauses in round 1
c [cce-7-2] incomplete large round (ACCE)
c [cce-7-2] allowing another 9098121 steps for small clauses
c [cce-7-2] scheduling 16464 clauses = 6286 binary + 10178 ternary
c [cce-7-2] tried to eliminate 3099 small clauses 19%
c [cce-7-2] eliminated 1 binary clauses 0%
c [cce-7-2] eliminated 1 small clauses 0%
c [cce-7-2] eliminated 1 small clauses in 18196242 steps
c [cce-7-2] incomplete small round (ACCE)
c [cce-7-2] eliminated 1 covered clauses in round 2
c [cce-7] eliminated 596 covered clauses in TOTAL during 2 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 6600 variables 100%
c [elim-6] limit of 253553585 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 173 variables 3% in round 1 in 9019685 steps
c [elim-6-1] backward subsumption/strengthening limit 9019600
c [elim-6-1-1] backward checking 791 touched variables 12%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 1 and strengthened 8 clauses in 798913 steps
c [elim-6-1] rescheduled 34 variables 1% by backward subsumption
c [elim-6-2] eliminated 3 variables 0% in round 2 in 26984 steps
c [elim-6-2] backward subsumption/strengthening limit 26900
c [elim-6-2-1] backward checking 20 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 19097 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 176 = 3% variables out of 6600 scheduled
c [bca-5] limit of 10000000 steps and 70550 added (scaled 2)
c [bca-5] 6609 out of 12850 literals actually usable 51%
c [bca-5] added 29 blocked clauses in 67607 steps
c [sweep-9] limit 7606607 penalty 0 = 0 + 0
c [sweep-9-1] 105 pos 37.6% + 174 neg 62.4% = 279 sched 4.3% ret 6145
c [sweep-9-1] 646402 steps 159 queries 15.85 avg class size
c [sweep-9-1] 2276 decisions 153 SAT calls 30.67 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-29] removed 10 variables
c [sweep-9-1] removed 10 vars (0 failed, 10 eqs, 6 impls)
c [sweep-9-2] 2657 pos 41.4% + 3757 neg 58.6% = 6414 sched 100.0% ret 0
c [sweep-9-2] 5093145 steps 691 queries 57.67 avg class size
c [sweep-9-2] 11441 decisions 683 SAT calls 34.90 avg env size
c [sweep-9-2] fully completed sweeping round
c [decomp-30] removed 15 variables
c [sweep-9-2] removed 15 vars (0 failed, 17 eqs, 15 impls)
c [sweep-9-3] 2652 pos 41.4% + 3747 neg 58.6% = 6399 sched 100.0% ret 0
c [sweep-9-3] 1871023 steps 175 queries 216.01 avg class size
c [sweep-9-3] 4099 decisions 174 SAT calls 46.20 avg env size
c [sweep-9-3] 3070 variables remain 48% (3328 retained 52%)
c [decomp-31] removed 2 variables
c [sweep-9-3] removed 2 vars (0 failed, 2 eqs, 0 impls)
c [sweep-9] removed 27 vars in TOTAL (3 rounds, 1022 queries)
c [sort-queue-10] sorted 301 enqueued variables after 452727 conflicts
c [score-dist-10] active 6096 (95%), one 0 (0%), zero 301 (5%)
c [score-dist-10] max exp 520, different 20 (4%)
c [score-dist-10] median active exp 510, avg 509.8
c [simplification-10] removed 204 variables 3.1% (6397 remain 21%)
c [simplification-10] removed 1008 irredundant clauses 2.8% (34869 remain 39%)
c [simplification-10] maximum reduction of 3% = max (3%, 3%)
c [simplification-10] geometric conflict interval increment 28798 = 115194 / 4
c [simplification-10] new conflict interval 143992
c [simplification-10] penalized conflict interval 143992 = 1 * 143992
c [simplification-10] hard conflict limit 668715 (soft 596719 + delta 71996)
c [simplification-10] new conflict limit 596719 (hard 668715)
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   93.4    6396    34867    464447   60933   5764  8970   22   167   22  13%   1018   94   21   22   97%
c -   94.1    6396    34866    471260   33993   5780  8976   21   145   14  15%  -4154   63   23   21  107%
c -   98.1    6396    34866    509044   34929   5786  8978   29    89   19  33%  -1889  -14   27   24  115%
c -  103.1    6396    34866    546404   35351   5788  8979   24   116   19  21%   -623   20   29   25  114%
c -  107.8    6396    34864    586309   34233   5792  8980   13   128   19  10%    128   31   10   26   37%
c 
c [simplification-11] limit 596719 conflicts (hard 668715) hit after 596719 conflicts
c [quatres-9] found 8847 quaternary clauses 44% in total
c [quatres-9-1] removed 4 duplicate quaternary clauses
c [quatres-9-1] added 2 double-self-subsuming ternary resolvents
c [quatres-9-2] added 41 single-self-subsuming ternary resolvents
c [quatres-9-2] added 71 quaternary resolvents
c [ternres-9] limit 31195385 with penalty 0 = 0 + 0
c [ternres-9] all 6396 free variables schedulable
c [ternres-9] 373 ternary resolvents (28 bin, 345 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-32] removed 3 variables
c [basicprobe-3] limit 155976926 penalty 0 = 0 + 0
c [basicprobe-3-0] 2576 sched 40%, 7 failed, 0 lifted, 316 hbrs
c [decomp-33] removed 9 variables
c [basicprobe-3-1] 3794 sched 59%, 0 failed, 0 lifted, 108 hbrs
c [basicprobe-3-2] 3791 sched 59%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-3-3] 3791 sched 59%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-3-4] 3791 sched 59%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-4] fully completed probing
c [basicprobe-3-4] 7 units = 7 failed (100%) + 0 lifted (0%)
c [basicprobe-3-4] removed 9 variables, found 430 hbrs
c [bate-2] eliminated 5 asymmetric tautologies during probing
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 221 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 1559769260 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 4 clauses out of 136 (3%) of length 10
c [cce-8-1] eliminated 7 clauses out of 271 (3%) of length 9
c [cce-8-1] eliminated 9 clauses out of 438 (2%) of length 8
c [cce-8-1] eliminated 14 clauses out of 841 (2%) of length 7
c [cce-8-1] eliminated 33 clauses out of 1826 (2%) of length 6
c [cce-8-1] eliminated 27 clauses out of 3073 (1%) of length 5
c [cce-8-1] eliminated 46 clauses out of 6945 (1%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 140 large clauses in 25290848 steps
c [cce-8-1] allowing another 12645424 steps for small clauses
c [cce-8-1] scheduling 16078 clauses = 6098 binary + 9980 ternary
c [cce-8-1] tried to eliminate 16078 small clauses 100%
c [cce-8-1] eliminated 6 binary clauses 0%
c [cce-8-1] eliminated 32 ternary clauses 0%
c [cce-8-1] eliminated 38 small clauses 0%
c [cce-8-1] eliminated 38 small clauses in 36150614 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 178 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 12450850 steps for small clauses
c [cce-8-2] scheduling 16040 clauses = 6092 binary + 9948 ternary
c [cce-8-2] tried to eliminate 16040 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 178 covered clauses in TOTAL during 2 rounds
c [cce-8] 178 < 1/100 * 34772 = 347 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 6385 variables 100%
c [elim-7] limit of 623907706 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 80 variables 1% in round 1 in 8816342 steps
c [elim-7-1] backward subsumption/strengthening limit 8816300
c [elim-7-1-1] backward checking 368 touched variables 6%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 4 clauses in 650667 steps
c [elim-7-1] rescheduled 5 variables 0% by backward subsumption
c [elim-7-2] eliminated 1 variables 0% in round 2 in 2795 steps
c [elim-7-2] backward subsumption/strengthening limit 2700
c [elim-7-2-1] backward checking 8 touched variables 0%
c [elim-7-2-1] incomplete backward checking 0 remain 0%
c [elim-7-2] subsumed 0 and strengthened 2 clauses in 2701 steps
c [elim-7-2] rescheduled 5 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 4547 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 81 = 1% variables out of 6385 scheduled
c [bca-6] limit of 10000000 steps and 69569 added (scaled 2)
c [bca-6] 5441 out of 12610 literals actually usable 43%
c [bca-6] added 26 blocked clauses in 54381 steps
c [sweep-10] limit 9358615 penalty 0 = 0 + 0
c [sweep-10-1] 1317 pos 43.5% + 1712 neg 56.5% = 3029 sched 48.0% ret 3275
c [sweep-10-1] 3802905 steps 600 queries 27.52 avg class size
c [sweep-10-1] 10456 decisions 599 SAT calls 36.54 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-37] removed 12 variables
c [sweep-10-1] removed 12 vars (0 failed, 14 eqs, 12 impls)
c [sweep-10-2] 2630 pos 41.8% + 3662 neg 58.2% = 6292 sched 100.0% ret 0
c [sweep-10-2] 5019101 steps 669 queries 46.40 avg class size
c [sweep-10-2] 12228 decisions 663 SAT calls 39.31 avg env size
c [sweep-10-2] fully completed sweeping round
c [decomp-38] removed 19 variables
c [sweep-10-2] removed 19 vars (0 failed, 22 eqs, 19 impls)
c [sweep-10-3] 2620 pos 41.8% + 3653 neg 58.2% = 6273 sched 100.0% ret 0
c [sweep-10-3] 551197 steps 63 queries 515.43 avg class size
c [sweep-10-3] 1700 decisions 61 SAT calls 56.92 avg env size
c [sweep-10-3] 5025 variables remain 80% (1248 retained 20%)
c [sweep-10-3] removed 0 vars (0 failed, 1 eqs, 0 impls)
c [sweep-10] removed 31 vars in TOTAL (3 rounds, 1329 queries)
c [sort-queue-11] sorted 176 enqueued variables after 596719 conflicts
c [score-dist-11] active 6097 (97%), one 0 (0%), zero 176 (3%)
c [score-dist-11] max exp 520, different 20 (4%)
c [score-dist-11] median active exp 511, avg 510.2
c [simplification-11] removed 123 variables 1.9% (6273 remain 20%)
c [simplification-11] removed 492 irredundant clauses 1.4% (34372 remain 38%)
c [simplification-11] maximum reduction of 2% = max (2%, 1%)
c [simplification-11] geometric conflict interval increment 47997 = 143992 / 3
c [simplification-11] new conflict interval 191989
c [simplification-11] penalized conflict interval 191989 = 1 * 191989
c [simplification-11] hard conflict limit 884702 (soft 788708 + delta 95994)
c [simplification-11] new conflict limit 788708 (hard 884702)
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 -  115.5    6273    34372    631073   36204   5851  8878   16   120   19  14%    571   17   32   24  135%
c -  120.3    6273    34372    672998   36688   5853  8878   36    69   19  52%    785  -27   25   27   95%
c -  125.4    6273    34371    717075   37205   5855  8878   36    71   19  50%    902  -29   48   27  176%
c -  131.5    6273    34371    762258   37758   5855  8878   38    69   19  56%    963  -22   35   31  112%
c -  136.9    6273    34371    804344   38302   5856  8878   41    68   19  61%    992  -14   45   32  137%
c -  144.2    6273    34371    852057   38090   5856  8878   43    64   20  67%   1008  -12   42   36  117%
c 
c [simplification-12] limit 788708 conflicts (hard 884702) hit after 867757 conflicts
c [quatres-10] found 8868 quaternary clauses 44% in total
c [quatres-10-1] removed 3 duplicate quaternary clauses
c [quatres-10-1] added 2 double-self-subsuming ternary resolvents
c [quatres-10-2] added 21 single-self-subsuming ternary resolvents
c [quatres-10-2] added 44 quaternary resolvents
c [ternres-10] limit 46068904 with penalty 0 = 0 + 0
c [ternres-10] all 6273 free variables schedulable
c [ternres-10] 354 ternary resolvents (24 bin, 330 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-6] limit 2303445 penalty 2 = 2 + 0
c [gauss-6] extracted 3713 xors of average arity 3.0
c [gauss-6] connected 11155 occurrences of 747 variables (average 14.9)
c [gauss-6] limit 2303445 penalty 2 = 2 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-40] removed 1 variables
c [simpleprobe-4] all 6272 free variables schedulable
c [simpleprobe-4] limit 184275618 penalty 0 = 0 + 0
c [decomp-41] removed 9 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 9 variables, found 788 hbrs, 3 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 433 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 6263 variables 100%
c [block-5] limit of 57586130 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 48 blocked clauses
c [block-5] 48 < 1/100 * 34328 = 343 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 6255 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 16000000000 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 22 variables 0% in round 1 in 8744561 steps
c [elim-8-1] backward subsumption/strengthening limit 8744500
c [elim-8-1-1] backward checking 142 touched variables 2%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1 and strengthened 0 clauses in 533113 steps
c [elim-8-1] rescheduled 4 variables 0% by backward subsumption
c [elim-8-2] eliminated 1 variables 0% in round 2 in 23356 steps
c [elim-8-2] backward subsumption/strengthening limit 23300
c [elim-8-2-1] backward checking 2 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 15332 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 23 = 0% variables out of 6255 scheduled
c [elim-8] 23 < 1/100 * 6255 = 62 considered unsuccessful
c [bca-7] limit of 10000000 steps and 69158 added (scaled 2)
c [bca-7] 5236 out of 12466 literals actually usable 42%
c [bca-7] added 3 blocked clauses in 63933 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 138206710 penalty 0 = 0 + 0
c [sweep-11-1] 2026 pos 40.6% + 2962 neg 59.4% = 4988 sched 80.0% ret 1244
c [sweep-11-1] 5570508 steps 657 queries 60.66 avg class size
c [sweep-11-1] 12147 decisions 653 SAT calls 38.02 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-42] removed 11 variables
c [sweep-11-1] removed 11 vars (0 failed, 13 eqs, 13 impls)
c [sweep-11-2] 2496 pos 40.1% + 3725 neg 59.9% = 6221 sched 100.0% ret 0
c [sweep-11-2] 5424688 steps 693 queries 100.59 avg class size
c [sweep-11-2] 12794 decisions 694 SAT calls 39.42 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-43] removed 12 variables
c [sweep-11-2] removed 12 vars (0 failed, 14 eqs, 7 impls)
c [sweep-11-3] 2492 pos 40.1% + 3717 neg 59.9% = 6209 sched 100.0% ret 0
c [sweep-11-3] 5254324 steps 648 queries 39.67 avg class size
c [sweep-11-3] 11522 decisions 640 SAT calls 39.78 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-44] removed 12 variables
c [sweep-11-3] removed 12 vars (0 failed, 16 eqs, 13 impls)
c [sweep-11] removed 35 vars in TOTAL (3 rounds, 1995 queries)
c [sort-queue-12] sorted 95 enqueued variables after 867757 conflicts
c [score-dist-12] active 6102 (98%), one 0 (0%), zero 95 (2%)
c [score-dist-12] max exp 521, different 21 (4%)
c [score-dist-12] median active exp 511, avg 510.5
c [simplification-12] removed 76 variables 1.2% (6197 remain 20%)
c [simplification-12] removed 238 irredundant clauses 0.7% (34133 remain 38%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 95994 = 191989 / 2
c [simplification-12] new conflict interval 287983
c [simplification-12] penalized conflict interval 287983 = 1 * 287983
c [simplification-12] hard conflict limit 1299731 (soft 1155740 + delta 143991)
c [simplification-12] new conflict limit 1155740 (hard 1299731)
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 -  151.9    6197    34133    895402   39113   6066  9224   28    67   20  42%   1016   -6   30   32   92%
c -  157.6    6197    34133    943918   40145   6067  9224   20   117   20  17%   1020   30   21   27   78%
c -  163.9    6197    34133   1000106   41050   6068  9224   18    86   20  21%   1022   -8   16   22   74%
c -  169.0    6197    34133   1048926   42350   6068  9224   14   127   20  11%   1023   35   14   20   66%
c -  174.9    6197    34133   1095570   42335   6071  9224   27   167   30  16%   1024   73   15   23   65%
c -  181.4    6197    34132   1146606   41059   6073  9224   41    67   30  60%   1024  -21   42   26  160%
c -  188.7    6197    34132   1198751   43529   6073  9224   34    65   31  53%   1024  -13   34   29  118%
c -  196.5    6197    34132   1248015   43506   6073  9224   43    52   31  83%   1024  -17   45   33  135%
c 
c [simplification-13] limit 1155740 conflicts (hard 1299731) hit after 1260635 conflicts
c [quatres-11] found 8998 quaternary clauses 43% in total
c [quatres-11-1] removed 4 duplicate quaternary clauses
c [quatres-11-2] added 25 single-self-subsuming ternary resolvents
c [quatres-11-2] added 35 quaternary resolvents
c [ternres-11] limit 69639505 with penalty 0 = 0 + 0
c [ternres-11] all 6197 free variables schedulable
c [ternres-11] 511 ternary resolvents (39 bin, 472 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-45] removed 1 variables
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 289 transitive binary clauses
c [transred-11] found 6 units
c [cce-9] limit of 174098762 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 4 clauses out of 72 (6%) of length 11
c [cce-9-1] eliminated 3 clauses out of 264 (1%) of length 9
c [cce-9-1] eliminated 8 clauses out of 410 (2%) of length 8
c [cce-9-1] eliminated 20 clauses out of 849 (2%) of length 7
c [cce-9-1] eliminated 20 clauses out of 1775 (1%) of length 6
c [cce-9-1] eliminated 59 clauses out of 3046 (2%) of length 5
c [cce-9-1] eliminated 111 clauses out of 6829 (2%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 225 large clauses in 72494326 steps
c [cce-9-1] allowing another 36247163 steps for small clauses
c [cce-9-1] scheduling 10795 clauses = 5927 binary + 4868 ternary
c [cce-9-1] tried to eliminate 10795 small clauses 100%
c [cce-9-1] eliminated 59 binary clauses 1%
c [cce-9-1] eliminated 130 ternary clauses 3%
c [cce-9-1] eliminated 189 small clauses 2%
c [cce-9-1] eliminated 219 small clauses in 62147644 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 444 covered clauses in round 1
c [cce-9-2] eliminated 1 clauses out of 1755 (0%) of length 6
c [cce-9-2] eliminated 1 clauses out of 2987 (0%) of length 5
c [cce-9-2] eliminated 3 clauses out of 6718 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 5 large clauses in 83431086 steps
c [cce-9-2] allowing another 41715543 steps for small clauses
c [cce-9-2] scheduling 10606 clauses = 5868 binary + 4738 ternary
c [cce-9-2] tried to eliminate 10606 small clauses 100%
c [cce-9-2] eliminated 1 binary clauses 0%
c [cce-9-2] eliminated 2 ternary clauses 0%
c [cce-9-2] eliminated 3 small clauses 0%
c [cce-9-2] eliminated 3 small clauses in 68806403 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 8 covered clauses in round 2
c [cce-9-3] incomplete large round (ACCE)
c [cce-9-3] allowing another 21572358 steps for small clauses
c [cce-9-3] scheduling 10603 clauses = 5867 binary + 4736 ternary
c [cce-9-3] tried to eliminate 8421 small clauses 79%
c [cce-9-3] incomplete small round (ACCE)
c [cce-9-3] eliminated 0 covered clauses in round 3
c [cce-9] eliminated 452 covered clauses in TOTAL during 3 rounds
c [bca-8] limit of 10000000 steps and 68125 added (scaled 2)
c [bca-8] 5066 out of 12382 literals actually usable 41%
c [bca-8] added 1 blocked clauses in 66818 steps
c [sweep-12] limit 20891851 penalty 0 = 0 + 0
c [sweep-12-1] 2549 pos 41.2% + 3641 neg 58.8% = 6190 sched 100.0% ret 0
c [sweep-12-1] 6095302 steps 657 queries 46.94 avg class size
c [sweep-12-1] 12208 decisions 650 SAT calls 42.80 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-46] removed 9 variables
c [sweep-12-1] removed 9 vars (0 failed, 12 eqs, 7 impls)
c [sweep-12-2] 2547 pos 41.2% + 3634 neg 58.8% = 6181 sched 100.0% ret 0
c [sweep-12-2] 5739689 steps 665 queries 65.00 avg class size
c [sweep-12-2] 12393 decisions 662 SAT calls 40.29 avg env size
c [sweep-12-2] fully completed sweeping round
c [decomp-47] removed 10 variables
c [sweep-12-2] removed 10 vars (0 failed, 13 eqs, 8 impls)
c [sweep-12-3] 2544 pos 41.2% + 3627 neg 58.8% = 6171 sched 100.0% ret 0
c [sweep-12-3] 5252479 steps 660 queries 26.45 avg class size
c [sweep-12-3] 11967 decisions 656 SAT calls 41.16 avg env size
c [sweep-12-3] fully completed sweeping round
c [decomp-48] removed 6 variables
c [sweep-12-3] removed 6 vars (0 failed, 9 eqs, 3 impls)
c [sweep-12] removed 25 vars in TOTAL (3 rounds, 1979 queries)
c [sort-queue-13] sorted 76 enqueued variables after 1260635 conflicts
c [score-dist-13] active 6089 (99%), one 0 (0%), zero 76 (1%)
c [score-dist-13] max exp 522, different 22 (4%)
c [score-dist-13] median active exp 512, avg 510.7
c [simplification-13] removed 32 variables 0.5% (6165 remain 20%)
c [simplification-13] removed 509 irredundant clauses 1.5% (33623 remain 37%)
c [simplification-13] maximum reduction of 1% = max (1%, 1%)
c [simplification-13] geometric conflict interval increment 143991 = 287983 / 2
c [simplification-13] new conflict interval 431974
c [simplification-13] penalized conflict interval 431974 = 1 * 431974
c [simplification-13] hard conflict limit 1908596 (soft 1692609 + delta 215987)
c [simplification-13] new conflict limit 1692609 (hard 1908596)
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 -  219.5    6165    33623   1301092   43478   6596  9074   38    61   22  63%   1024   -5   40   33  124%
c -  231.8    6165    33623   1375523   43844   6596  9074   39    54   23  72%   1024   -9   38   36  106%
c -  240.1    6165    33623   1437359   45236   6598  9074   25    75   23  33%   1024   13   23   33   69%
c -  247.2    6165    33623   1487900   46010   6606  9074   28    73   23  38%   1024    6   29   29   97%
c -  256.8    6165    33623   1543395   45419   6608  9074   44    56   23  79%   1024  -13   48   31  156%
c -  267.2    6165    33623   1613003   44328   6609  9074   33    77   32  43%   1024    8   47   31  149%
c 
c [simplification-14] limit 1692609 conflicts (hard 1908596) hit after 1706068 conflicts
c [quatres-12] found 9033 quaternary clauses 42% in total
c [quatres-12-1] removed 1 duplicate quaternary clauses
c [quatres-12-1] added 2 double-self-subsuming ternary resolvents
c [quatres-12-2] added 27 single-self-subsuming ternary resolvents
c [quatres-12-2] added 40 quaternary resolvents
c [ternres-12] limit 109633382 with penalty 0 = 0 + 0
c [ternres-12] all 6165 free variables schedulable
c [ternres-12] 488 ternary resolvents (32 bin, 456 trn)
c [ternres-12] fully completed ternary resolution
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 208 transitive binary clauses
c [transred-12] found 1 units
c [cce-10] limit of 548166912 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 2 clauses out of 410 (0%) of length 8
c [cce-10-1] eliminated 2 clauses out of 1746 (0%) of length 6
c [cce-10-1] eliminated 5 clauses out of 2974 (0%) of length 5
c [cce-10-1] eliminated 22 clauses out of 6700 (0%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 31 large clauses in 23320761 steps
c [cce-10-1] allowing another 11660380 steps for small clauses
c [cce-10-1] scheduling 10591 clauses = 5869 binary + 4722 ternary
c [cce-10-1] tried to eliminate 10591 small clauses 100%
c [cce-10-1] eliminated 8 binary clauses 0%
c [cce-10-1] eliminated 8 ternary clauses 0%
c [cce-10-1] eliminated 16 small clauses 0%
c [cce-10-1] eliminated 18 small clauses in 27057478 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 49 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 11642720 steps for small clauses
c [cce-10-2] scheduling 10575 clauses = 5861 binary + 4714 ternary
c [cce-10-2] tried to eliminate 10575 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 49 covered clauses in TOTAL during 2 rounds
c [cce-10] 49 < 1/100 * 33615 = 336 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 6164 variables 100%
c [elim-9] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 81 variables 1% in round 1 in 8528347 steps
c [elim-9-1] backward subsumption/strengthening limit 8528300
c [elim-9-1-1] backward checking 485 touched variables 8%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 9 clauses in 652208 steps
c [elim-9-1] rescheduled 15 variables 0% by backward subsumption
c [elim-9-2] no variable eliminated in round 2 in 23334 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 81 = 1% variables out of 6164 scheduled
c [bca-9] limit of 10000000 steps and 67390 added (scaled 2)
c [bca-9] 5023 out of 12168 literals actually usable 41%
c [bca-9] added 5 blocked clauses in 105098 steps
c [sweep-13] limit 32890014 penalty 0 = 0 + 0
c [sweep-13-1] 2468 pos 40.6% + 3615 neg 59.4% = 6083 sched 100.0% ret 0
c [sweep-13-1] 6839320 steps 686 queries 51.83 avg class size
c [sweep-13-1] 11971 decisions 665 SAT calls 40.76 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-50] removed 22 variables
c [sweep-13-1] removed 22 vars (0 failed, 28 eqs, 22 impls)
c [sweep-13-2] 2459 pos 40.6% + 3602 neg 59.4% = 6061 sched 100.0% ret 0
c [sweep-13-2] 6365425 steps 648 queries 58.67 avg class size
c [sweep-13-2] 11591 decisions 630 SAT calls 39.44 avg env size
c [sweep-13-2] fully completed sweeping round
c [decomp-51] removed 25 variables
c [sweep-13-2] removed 25 vars (0 failed, 31 eqs, 25 impls)
c [sweep-13-3] 2450 pos 40.6% + 3586 neg 59.4% = 6036 sched 100.0% ret 0
c [sweep-13-3] 7455453 steps 693 queries 56.08 avg class size
c [sweep-13-3] 12034 decisions 676 SAT calls 40.90 avg env size
c [sweep-13-3] fully completed sweeping round
c [decomp-52] removed 22 variables
c [sweep-13-3] removed 22 vars (0 failed, 28 eqs, 29 impls)
c [sweep-13] removed 69 vars in TOTAL (3 rounds, 2024 queries)
c [sort-queue-14] sorted 46 enqueued variables after 1706068 conflicts
c [score-dist-14] active 5968 (99%), one 0 (0%), zero 46 (1%)
c [score-dist-14] max exp 522, different 22 (4%)
c [score-dist-14] median active exp 512, avg 510.9
c [simplification-14] removed 151 variables 2.4% (6014 remain 20%)
c [simplification-14] removed 385 irredundant clauses 1.1% (33238 remain 37%)
c [simplification-14] maximum reduction of 2% = max (2%, 1%)
c [simplification-14] geometric conflict interval increment 143991 = 431974 / 3
c [simplification-14] new conflict interval 575965
c [simplification-14] penalized conflict interval 575965 = 1 * 575965
c [simplification-14] hard conflict limit 2570015 (soft 2282033 + delta 287982)
c [simplification-14] new conflict limit 2282033 (hard 2570015)
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 -  284.7    6014    33238   1706068   48499   6255  8589   37    55   15  68%   1024    0   17   38   45%
c -  293.8    6014    33238   1774406   49301   6256  8589   25    49   18  50%   1024   -6   34   32  107%
c -  304.2    6014    33238   1850356   48781   6259  8589   17   251   25   7%   1024  182   15   29   50%
c -  312.3    6014    33238   1916911   48104   6260  8589   37    49   24  75%   1024  -68   41   25  161%
c -  324.1    6014    33238   1996194   50593   6261  8589   39    43   25  93%   1024  -39   41   28  146%
c -  335.5    6014    33238   2073307   50974   6261  8589   39    42   25  93%   1024  -16   39   31  126%
c -  349.0    6014    33238   2185734   50243   6262  8589   31    46   25  69%   1024   -3   37   31  118%
c 
c [simplification-15] limit 2282033 conflicts (hard 2570015) hit after 2284022 conflicts
c [quatres-13] found 9073 quaternary clauses 40% in total
c [quatres-13-1] removed 10 duplicate quaternary clauses
c [quatres-13-1] added 2 double-self-subsuming ternary resolvents
c [quatres-13-2] added 25 single-self-subsuming ternary resolvents
c [quatres-13-2] added 35 quaternary resolvents
c [ternres-13] limit 154765173 with penalty 0 = 0 + 0
c [ternres-13] all 6014 free variables schedulable
c [ternres-13] 1557 ternary resolvents (82 bin, 1475 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 4836411 penalty 4 = 4 + 0
c [card-5] found 459 at-most-one constraints of average size 3.2
c [card-5] found 45 at-most-two constraints of average size 4.0
c [card-5] using previous limit 4836411 for elimination
c [card-5] 504 out of 504 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] generated 19 at-most-one constraints, 4 used 21%
c [card-5] exported 4 binary clauses, 1.0 per/constraint
c [decomp-53] removed 4 variables
c [unhide-5] limit 1250000 with penalty 4 = 4 + 0
c [unhide-5-5] 0 units, 13 failed, 162 tauts, 0 hbrs, 112894 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 197 transitive binary clauses
c [transred-13] found 1 units
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 6004 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 37 variables 1% in round 1 in 8395305 steps
c [elim-10-1] backward subsumption/strengthening limit 8395300
c [elim-10-1-1] backward checking 313 touched variables 5%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 0 and strengthened 1 clauses in 588479 steps
c [elim-10-1] rescheduled 4 variables 0% by backward subsumption
c [elim-10-2] no variable eliminated in round 2 in 2407 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 37 = 1% variables out of 6004 scheduled
c [elim-10] 37 < 1/100 * 6004 = 60 considered unsuccessful
c [bca-10] limit of 10000000 steps and 66698 added (scaled 2)
c [bca-10] 4583 out of 11936 literals actually usable 38%
c [bca-10] added 0 blocked clauses in 111225 steps
c [sweep-14] limit 46429551 penalty 0 = 0 + 0
c [sweep-14-1] 2390 pos 40.1% + 3577 neg 59.9% = 5967 sched 100.0% ret 0
c [sweep-14-1] 7287975 steps 659 queries 50.37 avg class size
c [sweep-14-1] 11561 decisions 647 SAT calls 41.55 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-54] removed 16 variables
c [sweep-14-1] removed 16 vars (0 failed, 23 eqs, 16 impls)
c [sweep-14-2] 2384 pos 40.1% + 3567 neg 59.9% = 5951 sched 100.0% ret 0
c [sweep-14-2] 7000512 steps 666 queries 43.84 avg class size
c [sweep-14-2] 11322 decisions 656 SAT calls 39.38 avg env size
c [sweep-14-2] fully completed sweeping round
c [decomp-55] removed 9 variables
c [sweep-14-2] removed 9 vars (0 failed, 17 eqs, 9 impls)
c [sweep-14-3] 2380 pos 40.1% + 3562 neg 59.9% = 5942 sched 100.0% ret 0
c [sweep-14-3] 7042466 steps 670 queries 32.34 avg class size
c [sweep-14-3] 11481 decisions 660 SAT calls 40.53 avg env size
c [sweep-14-3] fully completed sweeping round
c [decomp-56] removed 9 variables
c [sweep-14-3] removed 9 vars (0 failed, 19 eqs, 9 impls)
c [sweep-14] removed 34 vars in TOTAL (3 rounds, 1992 queries)
c [sort-queue-15] sorted 37 enqueued variables after 2284022 conflicts
c [score-dist-15] active 5896 (99%), one 0 (0%), zero 37 (1%)
c [score-dist-15] max exp 522, different 22 (4%)
c [score-dist-15] median active exp 512, avg 511.4
c [simplification-15] removed 81 variables 1.3% (5933 remain 19%)
c [simplification-15] removed 315 irredundant clauses 0.9% (32923 remain 37%)
c [simplification-15] maximum reduction of 1% = max (1%, 1%)
c [simplification-15] geometric conflict interval increment 287982 = 575965 / 2
c [simplification-15] new conflict interval 863947
c [simplification-15] penalized conflict interval 863947 = 1 * 863947
c [simplification-15] hard conflict limit 3579942 (soft 3147969 + delta 431973)
c [simplification-15] new conflict limit 3147969 (hard 3579942)
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 -  364.5    5933    32923   2285016   50374   7053  8267   34    50   18  69%   1024    3   38   33  118%
c -  376.7    5933    32921   2390344   50886   7069  8268   12   164   25   7%   1024   95   10   26   40%
c -  382.9    5933    32921   2450190   51317   7078  8269   15    76   25  19%   1024   -6   15   20   76%
c -  389.0    5933    32921   2511540   53831   7083  8269   19    68   25  28%   1024   -7   22   19  119%
c -  395.6    5933    32921   2571338   52372   7083  8269   22    69   25  32%   1024   -4   25   19  133%
c -  402.4    5933    32921   2634233   53164   7085  8269   16    71   25  23%   1024   -1   16   18   88%
c -  410.6    5933    32921   2698269   54961   7086  8269   23    66   39  34%   1024   -4   25   19  131%
c -  418.6    5933    32921   2762150   55739   7087  8269   17    68   39  26%   1024   -1   15   19   79%
c -  429.8    5933    32921   2828437   56932   7087  8269   33    60   40  56%   1024   -6   32   23  140%
c -  443.3    5933    32921   2900956   57675   7087  8269   32    60   40  53%   1024  -12   30   26  113%
c -  459.1    5933    32921   2985140   59138   7089  8269   34    58   42  59%   1024  -10   38   31  122%
c -  473.7    5933    32921   3070189   59676   7091  8269   33    57   42  58%   1024   -6   38   32  119%
c -  489.3    5933    32921   3163552   59189   7092  8269   32    53   42  61%   1024   -5   36   33  110%
c 
c [simplification-16] limit 3147969 conflicts (hard 3579942) hit after 3169646 conflicts
c [quatres-14] found 9236 quaternary clauses 38% in total
c [quatres-14-1] removed 3 duplicate quaternary clauses
c [quatres-14-1] added 2 double-self-subsuming ternary resolvents
c [quatres-14-2] added 29 single-self-subsuming ternary resolvents
c [quatres-14-2] added 89 quaternary resolvents
c [ternres-14] limit 200000000 with penalty 0 = 0 + 0
c [ternres-14] all 5933 free variables schedulable
c [ternres-14] 456 ternary resolvents (21 bin, 435 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-7] limit 6090146 penalty 3 = 3 + 0
c [gauss-7] extracted 3514 xors of average arity 3.0
c [gauss-7] connected 10542 occurrences of 707 variables (average 14.9)
c [gauss-7] limit 6090146 penalty 3 = 3 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-57] removed 1 variables
c [treelook-4] limit 3045073 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 11541 literals 97%
c [treelook-4] scheduling used 346641 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 3045073 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 3045317 steps
c [treelook-4] 9771 literals remain 82%
c [treelook-4] 5639 variables remain to probed next time 95%
c [treelook-4] removed 3 variables, found 2892 hbrs
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 429 transitive binary clauses
c [transred-14] found 1 units
c [cce-11] limit of 609014601 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 1 clauses out of 118 (1%) of length 10
c [cce-11-1] eliminated 8 clauses out of 283 (3%) of length 9
c [cce-11-1] eliminated 17 clauses out of 435 (4%) of length 8
c [cce-11-1] eliminated 33 clauses out of 806 (4%) of length 7
c [cce-11-1] eliminated 46 clauses out of 1716 (3%) of length 6
c [cce-11-1] eliminated 73 clauses out of 2973 (2%) of length 5
c [cce-11-1] eliminated 176 clauses out of 6628 (3%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 354 large clauses in 61519406 steps
c [cce-11-1] allowing another 30759703 steps for small clauses
c [cce-11-1] scheduling 14971 clauses = 5702 binary + 9269 ternary
c [cce-11-1] tried to eliminate 14971 small clauses 100%
c [cce-11-1] eliminated 77 binary clauses 1%
c [cce-11-1] eliminated 245 ternary clauses 3%
c [cce-11-1] eliminated 322 small clauses 2%
c [cce-11-1] eliminated 328 small clauses in 64967426 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 682 covered clauses in round 1
c [cce-11-2] eliminated 1 clauses out of 418 (0%) of length 8
c [cce-11-2] eliminated 2 clauses out of 1670 (0%) of length 6
c [cce-11-2] eliminated 2 clauses out of 2900 (0%) of length 5
c [cce-11-2] eliminated 4 clauses out of 6452 (0%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 9 large clauses in 59065535 steps
c [cce-11-2] allowing another 29532767 steps for small clauses
c [cce-11-2] scheduling 14649 clauses = 5625 binary + 9024 ternary
c [cce-11-2] tried to eliminate 14649 small clauses 100%
c [cce-11-2] eliminated 3 binary clauses 0%
c [cce-11-2] eliminated 1 ternary clauses 0%
c [cce-11-2] eliminated 4 small clauses 0%
c [cce-11-2] eliminated 4 small clauses in 62737236 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 13 covered clauses in round 2
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] allowing another 29244221 steps for small clauses
c [cce-11-3] scheduling 14645 clauses = 5622 binary + 9023 ternary
c [cce-11-3] tried to eliminate 14645 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 695 covered clauses in TOTAL during 3 rounds
c [sweep-15] limit 73081752 penalty 0 = 0 + 0
c [sweep-15-1] 2398 pos 40.5% + 3530 neg 59.5% = 5928 sched 100.0% ret 0
c [sweep-15-1] 6139282 steps 637 queries 38.97 avg class size
c [sweep-15-1] 11003 decisions 627 SAT calls 37.30 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-59] removed 7 variables
c [sweep-15-1] removed 7 vars (0 failed, 15 eqs, 3 impls)
c [sweep-15-2] 2393 pos 40.4% + 3528 neg 59.6% = 5921 sched 100.0% ret 0
c [sweep-15-2] 5716046 steps 657 queries 52.86 avg class size
c [sweep-15-2] 10933 decisions 643 SAT calls 40.03 avg env size
c [sweep-15-2] fully completed sweeping round
c [decomp-60] removed 21 variables
c [sweep-15-2] removed 21 vars (0 failed, 32 eqs, 12 impls)
c [sweep-15-3] 2381 pos 40.4% + 3519 neg 59.6% = 5900 sched 100.0% ret 0
c [sweep-15-3] 4880730 steps 660 queries 51.08 avg class size
c [sweep-15-3] 9830 decisions 646 SAT calls 34.62 avg env size
c [sweep-15-3] fully completed sweeping round
c [decomp-61] removed 8 variables
c [sweep-15-3] removed 8 vars (0 failed, 19 eqs, 8 impls)
c [sweep-15] removed 36 vars in TOTAL (3 rounds, 1951 queries)
c [sort-queue-16] sorted 21 enqueued variables after 3169646 conflicts
c [score-dist-16] active 5871 (100%), one 0 (0%), zero 21 (0%)
c [score-dist-16] max exp 523, different 23 (4%)
c [score-dist-16] median active exp 513, avg 511.7
c [simplification-16] removed 41 variables 0.7% (5892 remain 19%)
c [simplification-16] removed 769 irredundant clauses 2.3% (32152 remain 36%)
c [simplification-16] maximum reduction of 2% = max (1%, 2%)
c [simplification-16] geometric conflict interval increment 287982 = 863947 / 3
c [simplification-16] conflict interval soft limit 1000000 reached
c [simplification-16] new conflict interval 1000000
c [simplification-16] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-16] hard conflict limit 4669646 (soft 4169646 + delta 500000)
c [simplification-16] new conflict limit 4169646 (hard 4669646)
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 -  518.5    5892    32152   3257438   58514   7680 10797   39    53   25  74%   1024   -3   38   34  111%
c -  533.6    5892    32152   3356213   58702   7682 10797   37    49   26  75%   1024   -4   39   36  107%
c -  542.5    5892    32149   3430718   60579   7686 10797   22    76   25  29%   1024   11   24   28   85%
c -  551.7    5892    32149   3496107   59934   7687 10797   21    69   35  30%   1024   -0   22   24   93%
c -  561.2    5892    32149   3563097   57417   7692 10797   20    69   35  29%   1024    0   18   22   84%
c -  571.6    5892    32149   3634633   58608   7696 10797   21    73   35  29%   1024    4   24   20  121%
c -  584.3    5892    32149   3707566   62404   7697 10797   24    70   35  34%   1024   -1   24   22  106%
c -  597.1    5892    32149   3778247   63654   7698 10797   24    70   35  35%   1024   -1   22   23   95%
c -  612.4    5892    32146   3858100   63459   7700 10798   40    52   36  77%   1024  -26   43   28  154%
c -  632.4    5892    32144   3956387   64981   7700 10798   42    47   36  89%   1024   -9   42   36  116%
c -  652.9    5892    32144   4054431   66036   7700 10798   39    43   36  91%   1024   -7   39   35  113%
c -  668.8    5892    32144   4147521   64019   7700 10798   22    89   35  25%   1024   40   11   29   38%
c 
c [simplification-17] limit 4169646 conflicts (hard 4669646) hit after 4169646 conflicts
c [quatres-15] found 9269 quaternary clauses 37% in total
c [quatres-15-1] removed 17 duplicate quaternary clauses
c [quatres-15-1] added 2 double-self-subsuming ternary resolvents
c [quatres-15-2] added 16 single-self-subsuming ternary resolvents
c [quatres-15-2] added 48 quaternary resolvents
c [ternres-15] limit 200000000 with penalty 0 = 0 + 0
c [ternres-15] all 5892 free variables schedulable
c [ternres-15] 691 ternary resolvents (45 bin, 646 trn)
c [ternres-15] fully completed ternary resolution
c [basicprobe-4] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-4-0] 3477 sched 59%, 4 failed, 0 lifted, 491 hbrs
c [decomp-63] removed 5 variables
c [basicprobe-4-1] 3501 sched 59%, 0 failed, 0 lifted, 23 hbrs
c [basicprobe-4-2] 3503 sched 60%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-2] fully completed probing
c [basicprobe-4-2] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-4-2] removed 5 variables, found 514 hbrs
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 350 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 5887 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 36 blocked clauses
c [block-6] 36 < 1/100 * 32081 = 320 considered unsuccessful
c [cce-12] limit of 1819727703 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 2 clauses out of 268 (1%) of length 9
c [cce-12-1] eliminated 5 clauses out of 402 (1%) of length 8
c [cce-12-1] eliminated 2 clauses out of 782 (0%) of length 7
c [cce-12-1] eliminated 5 clauses out of 1655 (0%) of length 6
c [cce-12-1] eliminated 41 clauses out of 2890 (1%) of length 5
c [cce-12-1] eliminated 31 clauses out of 6420 (0%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 86 large clauses in 20846200 steps
c [cce-12-1] allowing another 10423100 steps for small clauses
c [cce-12-1] scheduling 14601 clauses = 5595 binary + 9006 ternary
c [cce-12-1] tried to eliminate 14601 small clauses 100%
c [cce-12-1] eliminated 9 binary clauses 0%
c [cce-12-1] eliminated 14 ternary clauses 0%
c [cce-12-1] eliminated 23 small clauses 0%
c [cce-12-1] eliminated 23 small clauses in 29304657 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 109 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 10322003 steps for small clauses
c [cce-12-2] scheduling 14578 clauses = 5586 binary + 8992 ternary
c [cce-12-2] tried to eliminate 14578 small clauses 100%
c [cce-12-2] completed small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 109 covered clauses in TOTAL during 2 rounds
c [cce-12] 109 < 1/100 * 32045 = 320 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 5883 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 110 variables 2% in round 1 in 7920394 steps
c [elim-11-1] backward subsumption/strengthening limit 7920300
c [elim-11-1-1] backward checking 539 touched variables 9%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 0 and strengthened 1 clauses in 613112 steps
c [elim-11-1] rescheduled 5 variables 0% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 45736 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 110 = 2% variables out of 5883 scheduled
c [bca-11] limit of 10000000 steps and 64246 added (scaled 2)
c [bca-11] 4130 out of 11548 literals actually usable 36%
c [bca-11] added 6 blocked clauses in 90649 steps
c [sweep-16] limit 109183662 penalty 0 = 0 + 0
c [sweep-16-1] 2371 pos 41.1% + 3402 neg 58.9% = 5773 sched 100.0% ret 0
c [sweep-16-1] 6991678 steps 631 queries 44.68 avg class size
c [sweep-16-1] 11658 decisions 622 SAT calls 40.82 avg env size
c [sweep-16-1] fully completed sweeping round
c [decomp-65] removed 10 variables
c [sweep-16-1] removed 10 vars (0 failed, 19 eqs, 5 impls)
c [sweep-16-2] 2366 pos 41.1% + 3397 neg 58.9% = 5763 sched 100.0% ret 0
c [sweep-16-2] 6708003 steps 622 queries 42.67 avg class size
c [sweep-16-2] 12236 decisions 609 SAT calls 44.30 avg env size
c [sweep-16-2] fully completed sweeping round
c [decomp-66] removed 6 variables
c [sweep-16-2] removed 6 vars (0 failed, 15 eqs, 8 impls)
c [sweep-16-3] 2363 pos 41.0% + 3394 neg 59.0% = 5757 sched 100.0% ret 0
c [sweep-16-3] 5947517 steps 635 queries 47.30 avg class size
c [sweep-16-3] 10627 decisions 626 SAT calls 39.54 avg env size
c [sweep-16-3] fully completed sweeping round
c [decomp-67] removed 1 variables
c [sweep-16-3] removed 1 vars (0 failed, 11 eqs, 1 impls)
c [sweep-16] removed 17 vars in TOTAL (3 rounds, 1885 queries)
c [sort-queue-17] sorted 19 enqueued variables after 4169646 conflicts
c [score-dist-17] active 5737 (100%), one 0 (0%), zero 19 (0%)
c [score-dist-17] max exp 523, different 23 (4%)
c [score-dist-17] median active exp 513, avg 511.9
c [simplification-17] removed 136 variables 2.3% (5756 remain 19%)
c [simplification-17] removed 443 irredundant clauses 1.4% (31701 remain 35%)
c [simplification-17] maximum reduction of 2% = max (2%, 1%)
c [simplification-17] geometric conflict interval increment 333333 = 1000000 / 3
c [simplification-17] conflict interval soft limit 1000000 reached
c [simplification-17] new conflict interval 1000000
c [simplification-17] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-17] hard conflict limit 5669646 (soft 5169646 + delta 500000)
c [simplification-17] new conflict limit 5169646 (hard 5669646)
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 -  692.0    5756    31701   4242582   64626   7906 10244   31    46   26  68%   1024  -11   24   28   86%
c -  721.0    5756    31701   4378901   65207   7907 10244   34    36   27  92%   1024   -7   31   33   95%
c -  746.7    5756    31701   4522050   64293   7908 10244   35    44   27  79%   1024    2   33   33   99%
c -  759.4    5756    31701   4625547   68180   7909 10244   29    42   28  69%   1024   -7   19   30   64%
c -  773.4    5756    31701   4726347   69049   7909 10244   19    51   27  37%   1024    0   16   29   56%
c -  788.5    5756    31701   4808514   61111   7910 10245   34    60   38  57%   1024    1   38   31  121%
c -  816.3    5756    31701   4899882   60951   7911 10245   35    47   38  73%   1024   -9   36   33  107%
c -  848.8    5756    31701   5005309   67598   7911 10245   32    38   40  85%   1024   -7   31   33   93%
c -  874.1    5756    31701   5109692   69192   7911 10245   36    43   40  82%   1024    1   36   34  106%
c 
c [simplification-18] limit 5169646 conflicts (hard 5669646) hit after 5219522 conflicts
c [quatres-16] found 9137 quaternary clauses 36% in total
c [quatres-16-1] removed 5 duplicate quaternary clauses
c [quatres-16-1] added 1 double-self-subsuming ternary resolvents
c [quatres-16-2] added 14 single-self-subsuming ternary resolvents
c [quatres-16-2] added 19 quaternary resolvents
c [ternres-16] limit 200000000 with penalty 0 = 0 + 0
c [ternres-16] all 5756 free variables schedulable
c [ternres-16] 421 ternary resolvents (22 bin, 399 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-8] limit 12500000 penalty 2 = 2 + 0
c [gauss-8] extracted 3463 xors of average arity 3.0
c [gauss-8] connected 10389 occurrences of 684 variables (average 15.2)
c [gauss-8] limit 12500000 penalty 2 = 2 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-5] all 5756 free variables schedulable
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-69] removed 9 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 9 variables, found 930 hbrs, 0 units
c [unhide-6] limit 2500000 with penalty 3 = 3 + 0
c [unhide-6-7] 0 units, 0 failed, 1502 tauts, 0 hbrs, 348930 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 380 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 5747 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 14 variables 0% in round 1 in 7794480 steps
c [elim-12-1] backward subsumption/strengthening limit 7794400
c [elim-12-1-1] backward checking 108 touched variables 2%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 476279 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 14 = 0% variables out of 5747 scheduled
c [elim-12] 14 < 1/100 * 5747 = 57 considered unsuccessful
c [bca-12] limit of 10000000 steps and 63949 added (scaled 2)
c [bca-12] 4195 out of 11468 literals actually usable 37%
c [bca-12] added 13 blocked clauses in 146292 steps
c [sweep-17] limit 154697728 penalty 0 = 0 + 0
c [sweep-17-1] 2203 pos 38.4% + 3530 neg 61.6% = 5733 sched 100.0% ret 0
c [sweep-17-1] 8796028 steps 626 queries 44.66 avg class size
c [sweep-17-1] 10993 decisions 621 SAT calls 40.01 avg env size
c [sweep-17-1] fully completed sweeping round
c [decomp-70] removed 7 variables
c [sweep-17-1] removed 7 vars (0 failed, 8 eqs, 7 impls)
c [sweep-17-2] 2200 pos 38.4% + 3526 neg 61.6% = 5726 sched 100.0% ret 0
c [sweep-17-2] 7567323 steps 580 queries 35.38 avg class size
c [sweep-17-2] 10312 decisions 580 SAT calls 42.18 avg env size
c [sweep-17-2] fully completed sweeping round
c [decomp-71] removed 3 variables
c [sweep-17-2] removed 3 vars (0 failed, 4 eqs, 4 impls)
c [sweep-17-3] 2198 pos 38.4% + 3525 neg 61.6% = 5723 sched 100.0% ret 0
c [sweep-17-3] 7073758 steps 583 queries 61.95 avg class size
c [sweep-17-3] 10341 decisions 584 SAT calls 37.69 avg env size
c [sweep-17-3] fully completed sweeping round
c [decomp-72] removed 5 variables
c [sweep-17-3] removed 5 vars (0 failed, 5 eqs, 5 impls)
c [sweep-17] removed 15 vars in TOTAL (3 rounds, 1786 queries)
c [sort-queue-18] sorted 18 enqueued variables after 5219522 conflicts
c [score-dist-18] active 5700 (100%), one 0 (0%), zero 18 (0%)
c [score-dist-18] max exp 524, different 24 (5%)
c [score-dist-18] median active exp 513, avg 512.0
c [simplification-18] removed 38 variables 0.7% (5718 remain 19%)
c [simplification-18] removed 145 irredundant clauses 0.5% (31556 remain 35%)
c [simplification-18] maximum reduction of 1% = max (1%, 0%)
c [simplification-18] geometric conflict interval increment 500000 = 1000000 / 2
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 6719522 (soft 6219522 + delta 500000)
c [simplification-18] new conflict limit 6219522 (hard 6719522)
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 -  905.4    5718    31556   5221489   69752   7562  9767   33    41   22  82%   1024    1   31   34   92%
c -  923.3    5718    31556   5313583   70201   7563  9767   31    35   31  90%   1024   -2   31   32   97%
c -  932.4    5718    31556   5394879   70540   7563  9767   15    67   30  23%   1024   -0   15   22   67%
c -  942.5    5718    31556   5479105   67318   7574  9768   17    62   29  28%   1024   -8   18   18  101%
c -  959.5    5718    31556   5573269   72074   7574  9768   41    57   45  71%   1024   -6   39   25  158%
c -  983.2    5718    31556   5672491   72089   7574  9768   40    57   45  69%   1024   -4   39   35  111%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 17 basic ate = 13 trn 76% + 4 lrg 24% in 2 updates
c bcas: 12 count, 624 added (41 skipped), 873308 steps
c bkwd: tried 66221 clauses, 132292 lits, 2.00 lits/clause
c bkwd: checked 16445385 occs, 248.34 occs/clause, 124.31 occs/lit
c bkwd: subsumed 6 binary, 15 ternary, 31 large
c bkwd: strengthened 0 binary, 4 ternary (100% self), 232 large (0% self)
c blkd: 6 bces, 2116 removed, 1246143 resolutions, 3132917 steps
c blkd: 1329 blocking literals 2%, 43 pure
c bump: 5762795 bumped seen, 612324757 lits 106.3 on average
c card: 5 count, 0 units, 17 am1, 12821167 steps
c card: 75 rescheduled, 686 eliminated, 71066 resolved, 5916 subsumed
c card: 1596 at-most-one constraints found, average size 3.32
c card: 1596 at-most-one constraints used 100%, average size 3.32
c card: 135 at-most-two constraints found, average size 4.01
c card: 132 at-most-two constraints used 98%, average size 4.02
c cces: 12 cces, 5269 eliminated, 4735 ate 90%, 534 abce 10%
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: 121 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 72 decompositions, 1677 equivalent 5%
c deco: 6435 decision-only clauses 0%, 61% reduction
c decs: 29479477 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 12 elims, 23122 eliminated 75%, 54 pure 0%
c elms: 33 rounds, 2.8 rounds/bve
c elms: 21939 small 95%, 1086 large 5%
c elms: 42885 tried small, 21939 succeeded 51%, 20946 failed 49%
c elms: 1404 subsumed, 2233 strengthened, 202 blocked
c elms: 2671329 copies, 3580406 resolutions, 1391830 ipos
c elms: 982725 subchks, 698491 strchks
c gaus: 8 extractions, 31300 extracted, 3.0 size, 4 max
c gaus: exported 0 units, 0 binary and 19 ternary equations
c gaus: 0 gc, 21131590 steps, 10565795 extr 50%, 1230253 elim 6%
c glue: 28.6 orig avg, 28.6 real avg, 5.2 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 28134 = 5317 simple 19% + 19797 trn 70% + 3020 lrg 11%, 511 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 5762795 clauses, 42.6 length
c lrnd: 245674656 lits = 385242912 orig - 139568256 removed 36%
c lrnd: 985008 uips 17%, 1709608 flips 30%
c mins: 5750518 mins 100%, 246 bin 0%, 5596 size 0%
c mins: 143106857 poisoned searches, 15907173 hits, 11% hit rate
c mins: 504676563 used twice searches, 93891752 hits, 19% hit rate
c move: moved 3551, 972 bin 27%, 2579 trn 73%
c otfs: 11976 driving 25%, 36421 restarting 75%
c otfs: str 48397, 48135 red 99%, 262 irr 1%
c otfs: str 48397, 0 bin 0%, 332 trn 1%, 48065 lrg 99%
c otfs: sub 4487, 4418 red 98%, 69 irr 2%
c otfs: sub 4487, 0 bin 0%, 22 trn 0%, 4465 lrg 100%
c phas: 1 computed, 8137 set, 2231 pos (27%), 5906 neg (73%)
c prbs: 4 basic, 77251 probed, 62 failed, 1 lifted
c prbs: 5 simple, 111240 probed, 107 failed, 1933 eqs
c prbs: 4 treelook, 2094 probed, 3 failed, 0 lifted
c prom: 225604 locked 2% out of 12120884 tried
c prps: 938861240 props, 31 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 16 count, 1582 quat, 336 self1, 28 self2, 183 dup
c queu: 18 sorted, 29479477 next (1022646 steps 0.03)
c queu: 612375171 enq (880719571 steps 1.44), 612324757 deq 100%
c redc: 4426 clauses 9%, 47315 tried 1%, 0 sat 0%
c redc: 6511 lits 1%, 561985 tried 0%, 0 sat 0%
c redc: 362 times jump level reduced, 19.1 levels on average
c reds: 82 count, 70215.2 conflicts per reduce
c reds: 0 memlim 0%, 82 arith 100%
c reds: 3710732 collected 91%, 370816 retired 9%
c rmbd: 1106 removed, 957 red 87%
c rsts: 20044 restarts 95%, 1096 skipped 5%
c rsts: 1096 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: 18 count, 18 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 5762795 count (7747730 tried 1.3), 1526418 sub out of 5760038 (26.5%)
c swps: 17 count, 37 rounds, 18738 queries (506.4/round)
c swps: 18443 sat calls, 482 unsat (0.9% success rate)
c swps: 333306 decisions 18.1, 17127 conflicts 0.9
c swps; 63.5 avg class size, 39.7 avg environment size
c swps: 1 failed, 563 impls, 757 equivs
c swp0: 6232 type 0 queries, 819 unsat (13.1%), 6082 sat (97.6%)
c swp1: 12506 type 1 queries, 2901 unsat (23.2%), 11899 sat (95.1%)
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: 70484986 calls to obtain time
c tops: 303 fixed 1%, 14 its, 411260.29 confs/it
c trds: 16 transitive reductions, 5617 removed, 21 failed
c trds: 183832 nodes, 187134 edges, 19308166 steps
c trim: 9015395 words, 34.4 MB
c trnr: 16 count, 553 bin, 12004 trn, 88805854 steps
c unhd: 6 count, 7 rounds, 8319607 steps
c unhd: 8 non-trivial sccs of average size 2.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 13 failed, 13 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 3554 tauts, 74 bin 2%, 1138 trn 32%, 127 lrg 4%
c unhd: 3554 tauts, 2215 stamp 62%, 3516 red 99%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 595381 str, 0 bin 0%, 165 trn 0%, 595216 lrg 100%, 593981 red 100%
c vars: 5721 remaining 19% and 25102 removed 81% out of 30823
c vars: 303 fixed 1%, 23122 eliminated 75%, 1677 equivalent 5%
c vsts: 58605752793 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 63.0 search visits per propagation, 10147.5 per conflict
c wchs: 9308052819 pushed, 9213767 enlarged, 211 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        5761620       3710732        370816     152301379      80775649       3013509
c 
c  0 0         19260   0      1121   0         0   0  62312881  41  22030706  27    467426  16     0.5
c  1 5         13782   0      3493   0      7751   2  12214101   8   5178814   6    121134   4     0.1
c  2 6        114527   2     61981   2     35317  10  29644718  19< 16894792  21<   635038  21     0.8
c  3 9        544602   9    386401  10     76469  21  19913478  13  13223235  16    742080  25<    4.5
c  4 14      1051335  18    804908  22     90271  24< 12597948   8   9400519  12    495188  16     6.7
c  5 21      1308732  23<  1060277  29<    57963  16   9663944   6   8522245  11    364625  12    10.9
c  6 30      1681385  29    893338  24     82227  22   4537923   3   4239978   5    168678   6    22.4
c  7 41       940650  16    440976  12     19042   5   1239804   1   1139026   1     15198   1    15.6
c  8 54        54450   1     37922   1      1248   0    100874   0     86725   0      1809   0     3.8
c  9 69        22402   0     17112   0       323   0     57113   0     48576   0      2197   0     3.1
c 10 86         9614   0      3173   0       193   0     17440   0     10224   0       136   0     1.8
c 11 126         881   0        30   0        12   0      1155   0       809   0         0   0     0.1
c 
c avg                  5.2           5.1           4.3           1.8           2.4           2.8
c std                  1.4           1.3           1.5           1.8           2.0           1.7
c 
c   64.632   6% bump
c   52.455   5% cce
c   19.624   2% decide
c   10.950   1% sweep
c 
c   13.150 < 1% rest (below)
c 
c    3.870   0% elim
c    2.613   0% unhide
c    2.501   0% probe
c    1.188   0% transred
c    0.688   0% ternres
c    0.651   0% gauss
c    0.554   0% bca
c    0.492   0% quatres
c    0.385   0% block
c    0.208   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.858   0% preprocessing     1%
c   77.295   8% inprocessing     99%
c ==================================
c   78.153   8% simplifying
c  921.836  92% search
c ==================================
c  999.992 100% all
c 
c       5757644 conflicts,        5757.7 confs/sec
c           454 ternaries,       12682.0 confs/ternary
c            50 binaries,       115152.9 confs/binary
c            14 iterations,     411260.3 confs/iteration
c 
c            82 reductions,          0.1 redus/sec,  70215.2 confs/reduction
c         20044 restarts,           20.0 rests/sec,    287.3 confs/restart
c      29479477 decisions,       29479.7 decis/sec,      5.1 decis/conflict
c     938861240 propagations,   938869.0 props/sec,     31.8 props/decision
c 
c 1000.0 seconds, 96.6 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
