c launch: /data/cnf/sc2014/app/6s16-opt.cnf.bz2
c host: atom04
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=5
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] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0   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 9 variables
c [simpleprobe-2] all 8128 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 6 variables
c [simpleprobe-2] 1239 variables remain 15% (6883 retained 85%)
c [simpleprobe-2] removed 6 variables, found 628 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 16244 literals 100%
c [treelook-1] scheduling used 189423 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 319258 steps
c [treelook-1] 16204 literals remain 100%
c [treelook-1] 8122 variables remain to probed next time 100%
c [decomp-5] removed 2 variables
c [treelook-1] removed 2 variables, found 1911 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 3318 probes remain 41% after last round
c [basicprobe-1-0] removed 0 variables, found 3398 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 8120 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 1746 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 427 clauses out of 8075 (5%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 1026 large clauses in 28353596 steps
c [cce-1-1] allowing another 14176798 steps for small clauses
c [cce-1-1] scheduling 13771 clauses = 8078 binary + 5693 ternary
c [cce-1-1] tried to eliminate 9583 small clauses 70%
c [cce-1-1] eliminated 95 binary clauses 1%
c [cce-1-1] eliminated 179 ternary clauses 3%
c [cce-1-1] eliminated 274 small clauses 2%
c [cce-1-1] eliminated 274 small clauses in 30001119 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1300 covered clauses in round 1
c [cce-1] eliminated 1300 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 8117 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 545 variables 7% in round 1 in 6369050 steps
c [elim-2-1] backward subsumption/strengthening limit 6369000
c [elim-2-1-1] backward checking 2858 touched variables 35%
c [elim-2-1-1] incomplete backward checking 2816 remain 99%
c [elim-2-1] subsumed 6 and strengthened 13 clauses in 6369562 steps
c [elim-2-1] rescheduled 70 variables 1% by backward subsumption
c [elim-2-2] eliminated 6 variables 0% in round 2 in 105998 steps
c [elim-2-2] backward subsumption/strengthening limit 105900
c [elim-2-2-1] backward checking 2826 touched variables 35%
c [elim-2-2-1] incomplete backward checking 2824 remain 100%
c [elim-2-2] subsumed 0 and strengthened 0 clauses in 107478 steps
c [elim-2-2] fully rescheduled 7566 variables 93%
c [elim-2-3] eliminated 21 variables 0% in round 3 in 6211415 steps
c [elim-2-3] backward subsumption/strengthening limit 836497
c [elim-2-3-1] backward checking 2837 touched variables 35%
c [elim-2-3-1] incomplete backward checking 2759 remain 97%
c [elim-2-3] subsumed 0 and strengthened 3 clauses in 836881 steps
c [elim-2] incomplete 10 not tried 0% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 572 = 7% variables out of 8117 scheduled
c [bca-1] limit of 10000000 steps and 81250 added (scaled 2)
c [bca-1] 13039 out of 15092 literals actually usable 86%
c [bca-1] added 557 blocked clauses in 35620 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3097 pos 41.0% + 4448 neg 59.0% = 7545 sched 100.0% ret 0
c [sweep-1-1] 1003893 steps 150 queries 260.28 avg class size
c [sweep-1-1] 2544 decisions 145 SAT calls 43.19 avg env size
c [sweep-1-1] 5340 variables remain 71% (2205 retained 29%)
c [decomp-6] removed 21 variables
c [sweep-1-1] removed 21 vars (0 failed, 8 eqs, 10 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 21 vars in TOTAL (1 rounds, 149 queries)
c [sort-queue-2] sorted 4393 enqueued variables after 1001 conflicts
c [score-dist-2] active 3131 (42%), one 0 (0%), zero 4393 (58%)
c [score-dist-2] max exp 770, different 231 (30%)
c [score-dist-2] median active exp 687, avg 661.3
c [simplification-2] removed 613 variables 7.5% (7524 remain 24%)
c [simplification-2] removed 3806 irredundant clauses 8.6% (40359 remain 45%)
c [simplification-2] maximum reduction of 9% = max (8%, 9%)
c [simplification-2] large reduction 9% >= 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    7523    40359      1924    1389    926  6299    2    37    7   6%     16   37    6    0 3493%
c 
c [simplification-3] limit 3001 conflicts (hard 13001) hit after 3001 conflicts
c [quatres-1] found 7906 quaternary clauses 49% in total
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 12 single-self-subsuming ternary resolvents
c [quatres-1-2] added 547 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 7523 free variables schedulable
c [ternres-1] 4269 ternary resolvents (45 bin, 4224 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 343 at-most-one constraints of average size 3.5
c [card-2] found 32 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 375 out of 375 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 5 at-most-one constraints, 1 used 20%
c [card-2] exported 1 binary clauses, 1.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 4412 xors of average arity 3.0
c [gauss-1] connected 13200 occurrences of 918 variables (average 14.4)
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 18 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 15010 literals 100%
c [treelook-2] scheduling used 206141 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 366220 steps
c [treelook-2] 14906 literals remain 99%
c [treelook-2] 7501 variables remain to probed next time 100%
c [decomp-8] removed 2 variables
c [treelook-2] removed 6 variables, found 713 hbrs
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 3 failed, 807 tauts, 0 hbrs, 1368 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 76 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 7498 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 39 blocked clauses
c [block-2] 39 < 1/100 * 40269 = 402 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 2 clauses out of 82 (2%) of length 13
c [cce-2-1] eliminated 1 clauses out of 119 (1%) of length 10
c [cce-2-1] eliminated 12 clauses out of 274 (4%) of length 9
c [cce-2-1] eliminated 22 clauses out of 469 (5%) of length 8
c [cce-2-1] eliminated 53 clauses out of 948 (6%) of length 7
c [cce-2-1] eliminated 99 clauses out of 2073 (5%) of length 6
c [cce-2-1] eliminated 122 clauses out of 3356 (4%) of length 5
c [cce-2-1] eliminated 319 clauses out of 7611 (4%) of length 4
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 630 large clauses in 30000036 steps
c [cce-2-1] allowing another 15000018 steps for small clauses
c [cce-2-1] scheduling 19561 clauses = 7343 binary + 12218 ternary
c [cce-2-1] tried to eliminate 14766 small clauses 75%
c [cce-2-1] eliminated 22 binary clauses 0%
c [cce-2-1] eliminated 316 ternary clauses 3%
c [cce-2-1] eliminated 338 small clauses 2%
c [cce-2-1] eliminated 338 small clauses in 30000003 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 968 covered clauses in round 1
c [cce-2] eliminated 968 covered clauses in TOTAL during 1 rounds
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 7496 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 124 variables 2% in round 1 in 7247622 steps
c [elim-3-1] backward subsumption/strengthening limit 7247600
c [elim-3-1-1] backward checking 880 touched variables 12%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 10 and strengthened 5 clauses in 1570744 steps
c [elim-3-1] rescheduled 28 variables 0% by backward subsumption
c [elim-3-2] eliminated 4 variables 0% in round 2 in 17489 steps
c [elim-3-2] backward subsumption/strengthening limit 17400
c [elim-3-2-1] backward checking 27 touched variables 0%
c [elim-3-2-1] incomplete backward checking 0 remain 0%
c [elim-3-2] subsumed 3 and strengthened 12 clauses in 17401 steps
c [elim-3-2] rescheduled 17 variables 0% by backward subsumption
c [elim-3-3] no variable eliminated in round 3 in 20043 steps
c [elim-3] fully completed in 3 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 128 = 2% variables out of 7496 scheduled
c [bca-2] limit of 10000000 steps and 78910 added (scaled 2)
c [bca-2] 10020 out of 14738 literals actually usable 68%
c [bca-2] added 5 blocked clauses in 29126 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2381 pos 45.5% + 2848 neg 54.5% = 5229 sched 71.0% ret 2139
c [sweep-2-1] 1022768 steps 87 queries 506.34 avg class size
c [sweep-2-1] 1144 decisions 82 SAT calls 27.70 avg env size
c [sweep-2-1] 4640 variables remain 63% (2727 retained 37%)
c [decomp-9] removed 21 variables
c [sweep-2-1] removed 21 vars (0 failed, 11 eqs, 16 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 21 vars in TOTAL (1 rounds, 86 queries)
c [sort-queue-3] sorted 2790 enqueued variables after 3001 conflicts
c [score-dist-3] active 4557 (62%), one 0 (0%), zero 2790 (38%)
c [score-dist-3] max exp 779, different 452 (58%)
c [score-dist-3] median active exp 595, avg 520.7
c [simplification-3] removed 176 variables 2.3% (7347 remain 24%)
c [simplification-3] removed 1307 irredundant clauses 3.2% (39051 remain 43%)
c [simplification-3] maximum reduction of 3% = max (2%, 3%)
c [simplification-3] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-3] new conflict interval 5000
c [simplification-3] penalized conflict interval 5000 = 1 * 5000
c [simplification-3] hard conflict limit 18001 (soft 8001 + delta 10000)
c [simplification-3] new conflict limit 8001 (hard 18001)
c 
c  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.0    7346    39051      3500    2978   5054  6321    3    62    7   6%     15   60    7    0 2317%
c i    4.5    7345    39050      7390    6216   5223  6387    6    86    7   7%     44   80    8    1 1210%
c 
c [simplification-4] limit 8001 conflicts (hard 18001) hit after 8002 conflicts
c [quatres-2] found 8521 quaternary clauses 49% in total
c [quatres-2-1] added 2 double-self-subsuming ternary resolvents
c [quatres-2-2] added 18 single-self-subsuming ternary resolvents
c [quatres-2-2] added 283 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 7345 free variables schedulable
c [ternres-2] 577 ternary resolvents (29 bin, 548 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 4540 xors of average arity 3.0
c [gauss-2] connected 13540 occurrences of 908 variables (average 14.9)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 7 ternary equations
c [decomp-10] removed 28 variables
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 107 tauts, 0 hbrs, 1689 literals
c [transred-2] limit 248171 with penalty 0 = 0 + 0
c [transred-2] removed 16 transitive binary clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 70 (1%) of length 13
c [cce-3-1] eliminated 2 clauses out of 104 (2%) of length 12
c [cce-3-1] eliminated 2 clauses out of 83 (2%) of length 11
c [cce-3-1] eliminated 1 clauses out of 274 (0%) of length 9
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 6 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3-1] scheduling 18781 clauses = 7100 binary + 11681 ternary
c [cce-3-1] tried to eliminate 2838 small clauses 15%
c [cce-3-1] eliminated 5 binary clauses 0%
c [cce-3-1] eliminated 25 ternary clauses 0%
c [cce-3-1] eliminated 30 small clauses 0%
c [cce-3-1] eliminated 30 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 36 covered clauses in round 1
c [cce-3] eliminated 36 covered clauses in TOTAL during 1 rounds
c [cce-3] 36 < 1/100 * 38960 = 389 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 7317 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 55 variables 1% in round 1 in 7621847 steps
c [elim-4-1] backward subsumption/strengthening limit 7621800
c [elim-4-1-1] backward checking 401 touched variables 5%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 2 and strengthened 10 clauses in 895795 steps
c [elim-4-1] rescheduled 25 variables 0% by backward subsumption
c [elim-4-2] eliminated 2 variables 0% in round 2 in 42072 steps
c [elim-4-2] backward subsumption/strengthening limit 42000
c [elim-4-2-1] backward checking 7 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 17060 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 57 = 1% variables out of 7317 scheduled
c [elim-4] 57 < 1/100 * 7317 = 73 considered unsuccessful
c [bca-3] limit of 10000000 steps and 78221 added (scaled 2)
c [bca-3] 7026 out of 14522 literals actually usable 48%
c [bca-3] added 4 blocked clauses in 24114 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1928 pos 42.1% + 2655 neg 57.9% = 4583 sched 63.1% ret 2677
c [sweep-3-1] 1010240 steps 122 queries 402.58 avg class size
c [sweep-3-1] 1629 decisions 113 SAT calls 27.73 avg env size
c [sweep-3-1] 3672 variables remain 51% (3588 retained 49%)
c [decomp-11] removed 25 variables
c [sweep-3-1] removed 25 vars (0 failed, 14 eqs, 18 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 25 vars in TOTAL (1 rounds, 121 queries)
c [sort-queue-4] sorted 2585 enqueued variables after 8002 conflicts
c [score-dist-4] active 4650 (64%), one 1703 (24%), zero 882 (12%)
c [score-dist-4] max exp 576, different 392 (68%)
c [score-dist-4] median active exp 436, avg 389.5
c [simplification-4] removed 110 variables 1.5% (7235 remain 23%)
c [simplification-4] removed 348 irredundant clauses 0.9% (38700 remain 43%)
c [simplification-4] maximum reduction of 1% = max (1%, 1%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 15000
c [simplification-4] penalized conflict interval 15000 = 1 * 15000
c [simplification-4] hard conflict limit 33002 (soft 23002 + delta 10000)
c [simplification-4] new conflict limit 23002 (hard 33002)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    8.0    7234    38700      8026    6849   5573  6597    6    90    8   6%     25   83    7    1  933%
c i    8.0    7233    38700      8033    6854   5573  6597    6    90    8   6%     25   83    7    1  925%
c i    8.1    7232    38700      8685    7392   5612  6604    6    91    8   7%     15   83    7    1  894%
c i    8.1    7231    38700      8692    7396   5613  6604    6    91    8   7%     14   83    7    1  881%
c i    8.1    7230    38700      8813    7489   5619  6606    6    95    8   6%     13   87    7    1  860%
c i    8.7    7229    38698     13960   11838   5788  6656    7    97    8   7%     60   83    8    1  605%
c i    8.7    7228    38698     13970   11846   5788  6656    7    96    8   7%     60   82    8    1  594%
c i    8.7    7227    38698     13971   11846   5788  6656    7    96    8   7%     59   82    8    1  592%
c i    8.8    7226    38698     14837   12560   5817  6669    7   100    8   7%     27   85    7    1  539%
c i    8.9    7225    38698     15416   13054   5838  6676    7    99    8   7%     15   83    6    1  446%
c 
c [simplification-5] limit of 13 iterations hit after 13 iterations
c [quatres-3] found 9179 quaternary clauses 48% in total
c [quatres-3-1] added 4 double-self-subsuming ternary resolvents
c [quatres-3-2] added 47 single-self-subsuming ternary resolvents
c [quatres-3-2] added 170 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 7225 free variables schedulable
c [ternres-3] 863 ternary resolvents (51 bin, 812 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 4411 xors of average arity 3.0
c [gauss-3] connected 13171 occurrences of 877 variables (average 15.0)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [decomp-12] removed 21 variables
c [gauss-3] exported 1 unary, 0 binary and 1 ternary equations
c [basicprobe-2] limit 1242754 penalty 1 = 1 + 0
c [basicprobe-2-0] 1744 probes remain 24% after last round
c [basicprobe-2-0] 11 units = 11 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 11 variables, found 3456 hbrs
c [bate-1] eliminated 6 asymmetric tautologies during probing
c [transred-3] limit 497101 with penalty 0 = 0 + 0
c [transred-3] removed 452 transitive binary clauses
c [transred-3] found 5 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 7188 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 2 blocked clauses
c [block-3] 2 < 1/100 * 38618 = 386 considered unsuccessful
c [bca-4] limit of 10000000 steps and 77913 added (scaled 2)
c [bca-4] 4792 out of 14378 literals actually usable 33%
c [bca-4] added 2 blocked clauses in 24360 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1581 pos 43.5% + 2057 neg 56.5% = 3638 sched 50.6% ret 3550
c [sweep-4-1] 1054583 steps 89 queries 225.38 avg class size
c [sweep-4-1] 1578 decisions 85 SAT calls 35.69 avg env size
c [sweep-4-1] 3052 variables remain 42% (4135 retained 58%)
c [decomp-14] removed 30 variables
c [sweep-4-1] removed 30 vars (0 failed, 11 eqs, 10 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 30 vars in TOTAL (1 rounds, 88 queries)
c [sort-queue-5] sorted 1108 enqueued variables after 15416 conflicts
c [score-dist-5] active 6050 (85%), one 862 (12%), zero 246 (3%)
c [score-dist-5] max exp 990, different 585 (59%)
c [score-dist-5] median active exp 872, avg 784.3
c [simplification-5] removed 67 variables 0.9% (7158 remain 23%)
c [simplification-5] removed 142 irredundant clauses 0.4% (38556 remain 43%)
c [simplification-5] maximum reduction of 1% = max (1%, 0%)
c [simplification-5] forced so keeping old conflict interval 15000
c [simplification-5] conflict limit remains at 23015 (hard 33002)
c [simplification-5] new iteration interval 100
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    9.6    7157    38556     16983   14561   6306  9244    7   101    9   7%     11   84    7    2  450%
c i    9.8    7156    38556     19330   16540   6391  9259    7    97    9   8%     18   77    7    2  417%
c i   10.0    7155    38556     20723   17743   6426  9268    8   104    9   7%     10   82    9    2  454%
c i   10.0    7154    38556     20725   17743   6427  9268    8   104    9   7%     10   82    9    2  451%
c i   10.0    7153    38556     20727   17743   6428  9268    8   104    9   7%     10   82    8    2  448%
c i   10.0    7152    38556     20729   17743   6429  9268    8   105    9   7%     10   83    8    2  445%
c i   10.0    7151    38556     20735   17745   6430  9268    8   105    9   7%     10   83    8    2  438%
c i   10.2    7150    38556     21805   18696   6453  9270    8   103    9   7%      6   79    8    2  381%
c i   10.3    7149    38556     22642   19376   6485  9280    8   101    9   8%      3   77    8    2  389%
c i   10.4    7148    38555     23010   19699   6492  9281    8   102    9   7%      1   77    8    2  372%
c 
c [simplification-6] limit 23031 conflicts (hard 33002) hit after 23031 conflicts
c [quatres-4] found 9615 quaternary clauses 46% in total
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 37 single-self-subsuming ternary resolvents
c [quatres-4-2] added 95 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 7148 free variables schedulable
c [ternres-4] 513 ternary resolvents (28 bin, 485 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 311 at-most-one constraints of average size 3.4
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 311 out of 311 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] extracted 4253 xors of average arity 3.0
c [gauss-4] connected 12735 occurrences of 862 variables (average 14.8)
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-15] removed 13 variables
c [simpleprobe-3] 1079 schedulable variables 15%
c [simpleprobe-3] limit 3078262 penalty 0 = 0 + 0
c [decomp-16] removed 26 variables
c [simpleprobe-3] 273 variables remain 4% (6836 retained 96%)
c [simpleprobe-3] removed 26 variables, found 1203 hbrs, 8 units
c [unhide-4] limit 76956 with penalty 1 = 1 + 0
c [unhide-4-4] 0 units, 0 failed, 1350 tauts, 0 hbrs, 8336 literals
c [transred-4] limit 769565 with penalty 0 = 0 + 0
c [transred-4] removed 260 transitive binary clauses
c [transred-4] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 150000000 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 1 clauses out of 86 (1%) of length 11
c [cce-4-1] eliminated 1 clauses out of 301 (0%) of length 9
c [cce-4-1] eliminated 6 clauses out of 404 (1%) of length 8
c [cce-4-1] eliminated 6 clauses out of 899 (1%) of length 7
c [cce-4-1] eliminated 30 clauses out of 1904 (2%) of length 6
c [cce-4-1] eliminated 47 clauses out of 3222 (1%) of length 5
c [cce-4-1] eliminated 66 clauses out of 7413 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 157 large clauses in 29601883 steps
c [cce-4-1] allowing another 14800941 steps for small clauses
c [cce-4-1] scheduling 18356 clauses = 6902 binary + 11454 ternary
c [cce-4-1] tried to eliminate 18356 small clauses 100%
c [cce-4-1] eliminated 43 binary clauses 1%
c [cce-4-1] eliminated 149 ternary clauses 1%
c [cce-4-1] eliminated 192 small clauses 1%
c [cce-4-1] eliminated 200 small clauses in 46561883 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 357 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 14419243 steps for small clauses
c [cce-4-2] scheduling 18164 clauses = 6859 binary + 11305 ternary
c [cce-4-2] tried to eliminate 18164 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 357 covered clauses in TOTAL during 2 rounds
c [cce-4] 357 < 1/100 * 38307 = 383 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 7108 variables 100%
c [elim-5] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 100 variables 1% in round 1 in 9715432 steps
c [elim-5-1] backward subsumption/strengthening limit 284568
c [elim-5-1-1] backward checking 585 touched variables 8%
c [elim-5-1-1] incomplete backward checking 517 remain 88%
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 285306 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 100 = 1% variables out of 7108 scheduled
c [bca-5] limit of 10000000 steps and 75892 added (scaled 2)
c [bca-5] 3581 out of 14018 literals actually usable 26%
c [bca-5] added 4 blocked clauses in 27012 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 1415 pos 47.6% + 1555 neg 52.4% = 2970 sched 42.4% ret 4038
c [sweep-5-1] 5980676 steps 642 queries 43.71 avg class size
c [sweep-5-1] 11051 decisions 568 SAT calls 38.65 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-17] removed 153 variables
c [sweep-5-1] removed 153 vars (0 failed, 147 eqs, 131 impls)
c [sweep-5-2] 3020 pos 44.1% + 3835 neg 55.9% = 6855 sched 100.0% ret 0
c [sweep-5-2] 4028206 steps 302 queries 107.63 avg class size
c [sweep-5-2] 6194 decisions 285 SAT calls 46.57 avg env size
c [sweep-5-2] 2057 variables remain 30% (4794 retained 70%)
c [decomp-18] removed 39 variables
c [sweep-5-2] removed 39 vars (0 failed, 41 eqs, 39 impls)
c [sweep-5] removed 192 vars in TOTAL (2 rounds, 942 queries)
c [sort-queue-6] sorted 1198 enqueued variables after 23031 conflicts
c [score-dist-6] active 5618 (82%), one 1172 (17%), zero 26 (0%)
c [score-dist-6] max exp 814, different 587 (72%)
c [score-dist-6] median active exp 538, avg 526.5
c [simplification-6] removed 332 variables 4.6% (6816 remain 22%)
c [simplification-6] removed 1152 irredundant clauses 3.0% (37403 remain 42%)
c [simplification-6] maximum reduction of 5% = max (5%, 3%)
c [simplification-6] large reduction 5% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 35031 (soft 25031 + delta 10000)
c [simplification-6] new conflict limit 25031 (hard 35031)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   13.3    6815    37401     24154   20574   6276  9966    8   108   10   7%      3   82    8    2  379%
c i   13.4    6814    37400     24775   21094   6292  9967    8   107   10   7%      1   80    8    2  345%
c 
c [simplification-7] limit 25031 conflicts (hard 35031) hit after 25032 conflicts
c [quatres-5] found 9701 quaternary clauses 46% in total
c [quatres-5-1] removed 8 duplicate quaternary clauses
c [quatres-5-1] added 2 double-self-subsuming ternary resolvents
c [quatres-5-2] added 59 single-self-subsuming ternary resolvents
c [quatres-5-2] added 138 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 6814 free variables schedulable
c [ternres-5] 1516 ternary resolvents (66 bin, 1450 trn)
c [ternres-5] 6 variables remain 0% (6808 retained 100%)
c [decomp-19] removed 13 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 13606 literals 100%
c [treelook-3] scheduling used 256780 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 333125 steps
c [treelook-3] 13572 literals remain 100%
c [treelook-3] 6801 variables remain to probed next time 100%
c [decomp-20] removed 1 variables
c [treelook-3] removed 3 variables, found 881 hbrs
c [transred-5] limit 837392 with penalty 0 = 0 + 0
c [transred-5] removed 738 transitive binary clauses
c [transred-5] found 19 units
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 6781 variables 100%
c [elim-6] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 113 variables 2% in round 1 in 9620015 steps
c [elim-6-1] backward subsumption/strengthening limit 9620000
c [elim-6-1-1] backward checking 544 touched variables 8%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 1 and strengthened 22 clauses in 830097 steps
c [elim-6-1] rescheduled 52 variables 1% by backward subsumption
c [elim-6-2] eliminated 8 variables 0% in round 2 in 2148372 steps
c [elim-6-2] backward subsumption/strengthening limit 2148300
c [elim-6-2-1] backward checking 56 touched variables 1%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 0 and strengthened 3 clauses in 589555 steps
c [elim-6-2] rescheduled 9 variables 0% by backward subsumption
c [elim-6-3] no variable eliminated in round 3 in 5871 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 121 = 2% variables out of 6781 scheduled
c [bca-6] limit of 10000000 steps and 73896 added (scaled 2)
c [bca-6] 3122 out of 13322 literals actually usable 23%
c [bca-6] added 3 blocked clauses in 27544 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 807 pos 41.0% + 1161 neg 59.0% = 1968 sched 29.5% ret 4692
c [sweep-6-1] 1079867 steps 102 queries 115.73 avg class size
c [sweep-6-1] 1668 decisions 96 SAT calls 39.02 avg env size
c [sweep-6-1] 1481 variables remain 22% (5179 retained 78%)
c [decomp-21] removed 13 variables
c [sweep-6-1] removed 13 vars (0 failed, 10 eqs, 10 impls)
c [sweep-6] removed 13 vars in TOTAL (1 rounds, 101 queries)
c [sort-queue-7] sorted 1127 enqueued variables after 25032 conflicts
c [score-dist-7] active 5520 (83%), one 1113 (17%), zero 14 (0%)
c [score-dist-7] max exp 845, different 561 (66%)
c [score-dist-7] median active exp 684, avg 628.8
c [simplification-7] removed 167 variables 2.5% (6647 remain 22%)
c [simplification-7] removed 858 irredundant clauses 2.3% (36542 remain 41%)
c [simplification-7] maximum reduction of 2% = max (2%, 2%)
c [simplification-7] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-7] new conflict interval 21666
c [simplification-7] penalized conflict interval 21666 = 1 * 21666
c [simplification-7] hard conflict limit 57531 (soft 46698 + delta 10833)
c [simplification-7] new conflict limit 46698 (hard 57531)
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   14.1    6646    36542     25596   20866   6808  9358    8   104   10   7%      1   76    8    2  348%
c i   14.2    6645    36542     25876   21109   6814  9362    8   103   10   8%      0   75    8    2  342%
c i   14.4    6644    36542     27484   22489   6865  9374    8   104   10   8%      8   74    8    2  309%
c i   14.9    6643    36542     31186   25736   6955  9393    8    98   10   8%     36   65    7    3  270%
c i   16.0    6642    36541     38461   32220   7174  9431    8    93   13   8%     86   52    8    3  231%
c i   16.5    6641    36541     41683   35116   7250  9445    8    93   11   8%     26   51    8    3  216%
c i   16.7    6640    36541     42742   36063   7276  9449    8    96   12   8%      7   53    8    4  234%
c i   17.2    6639    36541     45920   38900   7345  9462    8    90   12   9%     22   44    7    4  198%
c 
c [simplification-8] limit 46698 conflicts (hard 57531) hit after 46699 conflicts
c [quatres-6] found 10549 quaternary clauses 42% in total
c [quatres-6-1] removed 3 duplicate quaternary clauses
c [quatres-6-2] added 86 single-self-subsuming ternary resolvents
c [quatres-6-2] added 240 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] 6 schedulable variables 0%
c [ternres-6] 872 ternary resolvents (29 bin, 843 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-5] limit 1000000 penalty 1 = 1 + 0
c [gauss-5] extracted 3145 xors of average arity 3.0
c [gauss-5] connected 9378 occurrences of 789 variables (average 11.9)
c [gauss-5] limit 1000000 penalty 1 = 1 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 12 variables
c [basicprobe-3] limit 9012551 penalty 0 = 0 + 0
c [basicprobe-3-0] 1777 sched 27%, 14 failed, 3 lifted, 2442 hbrs
c [decomp-23] removed 22 variables
c [basicprobe-3-1] 3887 sched 59%, 18 failed, 0 lifted, 2342 hbrs
c [decomp-24] removed 26 variables
c [basicprobe-3-2] 1705 probes remain 26% after last round
c [basicprobe-3-2] 35 units = 32 failed (91%) + 3 lifted (9%)
c [basicprobe-3-2] removed 48 variables, found 4878 hbrs
c [bate-2] eliminated 3 asymmetric tautologies during probing
c [transred-6] limit 1802510 with penalty 0 = 0 + 0
c [transred-6] removed 679 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 6579 variables 100%
c [block-4] limit of 12500000 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 469 blocked clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 6510 variables 100%
c [elim-7] limit of 36050205 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 77 variables 1% in round 1 in 9255734 steps
c [elim-7-1] backward subsumption/strengthening limit 9255700
c [elim-7-1-1] backward checking 376 touched variables 6%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 2 and strengthened 9 clauses in 695086 steps
c [elim-7-1] rescheduled 29 variables 0% by backward subsumption
c [elim-7-2] eliminated 2 variables 0% in round 2 in 15876 steps
c [elim-7-2] backward subsumption/strengthening limit 15800
c [elim-7-2-1] backward checking 19 touched variables 0%
c [elim-7-2-1] incomplete backward checking 0 remain 0%
c [elim-7-2] subsumed 1 and strengthened 6 clauses in 15801 steps
c [elim-7-2] rescheduled 9 variables 0% by backward subsumption
c [elim-7-3] eliminated 1 variables 0% in round 3 in 6589 steps
c [elim-7-3] backward subsumption/strengthening limit 6500
c [elim-7-3-1] backward checking 10 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 0 and strengthened 0 clauses in 6501 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 80 = 1% variables out of 6510 scheduled
c [bca-7] limit of 10000000 steps and 71831 added (scaled 2)
c [bca-7] 1670 out of 12862 literals actually usable 13%
c [bca-7] added 0 blocked clauses in 42027 steps
c [sweep-7] limit 1000000 penalty 0 = 0 + 0
c [sweep-7-1] 590 pos 42.2% + 809 neg 57.8% = 1399 sched 21.8% ret 5031
c [sweep-7-1] 1000703 steps 87 queries 76.91 avg class size
c [sweep-7-1] 2021 decisions 85 SAT calls 54.68 avg env size
c [sweep-7-1] 1050 variables remain 16% (5380 retained 84%)
c [decomp-25] removed 12 variables
c [sweep-7-1] removed 12 vars (0 failed, 8 eqs, 5 impls)
c [sweep-7] removed 12 vars in TOTAL (1 rounds, 86 queries)
c [sort-queue-8] sorted 895 enqueued variables after 46699 conflicts
c [score-dist-8] active 5523 (86%), one 890 (14%), zero 5 (0%)
c [score-dist-8] max exp 983, different 529 (54%)
c [score-dist-8] median active exp 871, avg 776.2
c [simplification-8] removed 221 variables 3.3% (6418 remain 21%)
c [simplification-8] removed 1029 irredundant clauses 2.8% (35512 remain 40%)
c [simplification-8] maximum reduction of 3% = max (3%, 3%)
c [simplification-8] geometric conflict interval increment 5416 = 21666 / 4
c [simplification-8] new conflict interval 27082
c [simplification-8] penalized conflict interval 27082 = 1 * 27082
c [simplification-8] hard conflict limit 87322 (soft 73781 + delta 13541)
c [simplification-8] new conflict limit 73781 (hard 87322)
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   21.6    6417    35510     65650   56085   7411 12066    9    87   13  10%    244   28    9    5  187%
c 
c [simplification-9] limit 73781 conflicts (hard 87322) hit after 73781 conflicts
c [quatres-7] found 11199 quaternary clauses 39% in total
c [quatres-7-1] removed 6 duplicate quaternary clauses
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 88 single-self-subsuming ternary resolvents
c [quatres-7-2] added 273 quaternary resolvents
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] all 6417 free variables schedulable
c [ternres-7] 929 ternary resolvents (37 bin, 892 trn)
c [ternres-7] 1 variables remain 0% (6416 retained 100%)
c [decomp-26] removed 15 variables
c [simpleprobe-4] 241 schedulable variables 4%
c [simpleprobe-4] limit 12924284 penalty 0 = 0 + 0
c [decomp-27] removed 22 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 22 variables, found 1135 hbrs, 9 units
c [unhide-5] limit 161553 with penalty 2 = 2 + 0
c [unhide-5-5] 0 units, 0 failed, 175 tauts, 0 hbrs, 23395 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 655 transitive binary clauses
c [cce-5] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 142 (1%) of length 10
c [cce-5-1] eliminated 4 clauses out of 264 (2%) of length 9
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 5 large clauses in 7500043 steps
c [cce-5-1] allowing another 3750021 steps for small clauses
c [cce-5-1] scheduling 11325 clauses = 6248 binary + 5077 ternary
c [cce-5-1] tried to eliminate 1576 small clauses 14%
c [cce-5-1] eliminated 26 binary clauses 0%
c [cce-5-1] eliminated 64 ternary clauses 1%
c [cce-5-1] eliminated 90 small clauses 1%
c [cce-5-1] eliminated 90 small clauses in 7500001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 95 covered clauses in round 1
c [cce-5] eliminated 95 covered clauses in TOTAL during 1 rounds
c [cce-5] 95 < 1/100 * 35363 = 353 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 6381 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1292428400 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 86 variables 1% in round 1 in 9173927 steps
c [elim-8-1] backward subsumption/strengthening limit 9173900
c [elim-8-1-1] backward checking 400 touched variables 6%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1 and strengthened 3 clauses in 722703 steps
c [elim-8-1] rescheduled 10 variables 0% by backward subsumption
c [elim-8-2] eliminated 1 variables 0% in round 2 in 7185 steps
c [elim-8-2] backward subsumption/strengthening limit 7100
c [elim-8-2-1] backward checking 14 touched variables 0%
c [elim-8-2-1] incomplete backward checking 0 remain 0%
c [elim-8-2] subsumed 2 and strengthened 0 clauses in 7101 steps
c [elim-8-2] rescheduled 9 variables 0% by backward subsumption
c [elim-8-3] eliminated 1 variables 0% in round 3 in 3030 steps
c [elim-8-3] backward subsumption/strengthening limit 3000
c [elim-8-3-1] backward checking 13 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 2 and strengthened 1 clauses in 3172 steps
c [elim-8] incomplete 12 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 88 = 1% variables out of 6381 scheduled
c [sweep-8] limit 1000000 penalty 0 = 0 + 0
c [sweep-8-1] 426 pos 41.9% + 591 neg 58.1% = 1017 sched 16.2% ret 5276
c [sweep-8-1] 1018630 steps 42 queries 104.00 avg class size
c [sweep-8-1] 1156 decisions 40 SAT calls 60.02 avg env size
c [sweep-8-1] 906 variables remain 14% (5387 retained 86%)
c [decomp-28] removed 13 variables
c [sweep-8-1] removed 13 vars (0 failed, 10 eqs, 9 impls)
c [sweep-8] removed 13 vars in TOTAL (1 rounds, 41 queries)
c [sort-queue-9] sorted 1110 enqueued variables after 73781 conflicts
c [score-dist-9] active 5170 (82%), one 1108 (18%), zero 2 (0%)
c [score-dist-9] max exp 542, different 395 (73%)
c [score-dist-9] median active exp 458, avg 411.4
c [simplification-9] removed 137 variables 2.1% (6280 remain 20%)
c [simplification-9] removed 542 irredundant clauses 1.5% (34968 remain 39%)
c [simplification-9] maximum reduction of 2% = max (2%, 2%)
c [simplification-9] geometric conflict interval increment 9027 = 27082 / 3
c [simplification-9] new conflict interval 36109
c [simplification-9] penalized conflict interval 36109 = 1 * 36109
c [simplification-9] hard conflict limit 127944 (soft 109890 + delta 18054)
c [simplification-9] new conflict limit 109890 (hard 127944)
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 -   25.8    6280    34968     78975   25794   8065 11274    9    70   11  13%    132    8    8    6  140%
c i   26.1    6279    34968     81169   27823   8097 11277    9    73   12  12%    161   10    9    6  153%
c 
c [simplification-10] limit 109890 conflicts (hard 127944) hit after 121186 conflicts
c [quatres-8] found 12146 quaternary clauses 35% in total
c [quatres-8-1] removed 9 duplicate quaternary clauses
c [quatres-8-1] added 6 double-self-subsuming ternary resolvents
c [quatres-8-2] added 140 single-self-subsuming ternary resolvents
c [quatres-8-2] added 223 quaternary resolvents
c [ternres-8] limit 5672285 with penalty 0 = 0 + 0
c [ternres-8] all 6279 free variables schedulable
c [ternres-8] 1720 ternary resolvents (64 bin, 1656 trn)
c [ternres-8] 2 variables remain 0% (6277 retained 100%)
c [card-4] limit 354517 penalty 3 = 3 + 0
c [card-4] found 172 at-most-one constraints of average size 3.2
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 354517 for elimination
c [card-4] 172 out of 172 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-29] removed 18 variables
c [treelook-4] limit 567228 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 12524 literals 100%
c [treelook-4] scheduling used 372297 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 567228 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 682317 steps
c [treelook-4] 12470 literals remain 100%
c [treelook-4] 6261 variables remain to probed next time 100%
c [decomp-30] removed 1 variables
c [treelook-4] removed 2 variables, found 790 hbrs
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 391 transitive binary clauses
c [transred-8] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 6259 variables 100%
c [block-5] limit of 28361425 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 9 blocked clauses
c [block-5] 9 < 1/100 * 34912 = 349 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 6258 variables 100%
c [elim-9] limit of 113445703 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 14 variables 0% in round 1 in 9160470 steps
c [elim-9-1] backward subsumption/strengthening limit 9160400
c [elim-9-1-1] backward checking 127 touched variables 2%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 618488 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 14 = 0% variables out of 6258 scheduled
c [elim-9] 14 < 1/100 * 6258 = 62 considered unsuccessful
c [bca-8] limit of 10000000 steps and 70449 added (scaled 2)
c [bca-8] 1311 out of 12490 literals actually usable 10%
c [bca-8] added 3 blocked clauses in 66227 steps
c [sweep-9] limit 1701685 penalty 0 = 0 + 0
c [sweep-9-1] 402 pos 44.8% + 495 neg 55.2% = 897 sched 14.4% ret 5347
c [sweep-9-1] 1757219 steps 75 queries 67.63 avg class size
c [sweep-9-1] 3104 decisions 69 SAT calls 99.25 avg env size
c [sweep-9-1] 608 variables remain 10% (5636 retained 90%)
c [decomp-31] removed 12 variables
c [sweep-9-1] removed 12 vars (0 failed, 11 eqs, 13 impls)
c [sweep-9] removed 12 vars in TOTAL (1 rounds, 74 queries)
c [sort-queue-10] sorted 1005 enqueued variables after 121186 conflicts
c [score-dist-10] active 5227 (84%), one 1003 (16%), zero 2 (0%)
c [score-dist-10] max exp 950, different 586 (62%)
c [score-dist-10] median active exp 840, avg 747.7
c [simplification-10] removed 47 variables 0.7% (6232 remain 20%)
c [simplification-10] removed 141 irredundant clauses 0.4% (34827 remain 39%)
c [simplification-10] maximum reduction of 1% = max (1%, 0%)
c [simplification-10] geometric conflict interval increment 18054 = 36109 / 2
c [simplification-10] new conflict interval 54163
c [simplification-10] penalized conflict interval 54163 = 1 * 54163
c [simplification-10] hard conflict limit 202430 (soft 175349 + delta 27081)
c [simplification-10] new conflict limit 175349 (hard 202430)
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 -   35.7    6232    34827    131725   36740   9925 10727    9    59   17  16%    511   -6   10    7  129%
c -   42.0    6232    34827    179924   50425  10048 10740    8    41   18  21%    778  -16   10    8  124%
c i   42.0    6231    34827    180236   50705  10051 10740    8    41   20  21%    779  -16    9    8  117%
c 
c [simplification-11] limit 175349 conflicts (hard 202430) hit after 202430 conflicts
c [quatres-9] found 12662 quaternary clauses 29% in total
c [quatres-9-1] removed 5 duplicate quaternary clauses
c [quatres-9-1] added 6 double-self-subsuming ternary resolvents
c [quatres-9-2] added 93 single-self-subsuming ternary resolvents
c [quatres-9-2] added 123 quaternary resolvents
c [ternres-9] limit 9289602 with penalty 0 = 0 + 0
c [ternres-9] 2 schedulable variables 0%
c [ternres-9] 1140 ternary resolvents (37 bin, 1103 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-6] limit 500000 penalty 2 = 2 + 0
c [gauss-6] extracted 1217 xors of average arity 3.0
c [gauss-6] connected 3632 occurrences of 679 variables (average 5.3)
c [gauss-6] limit 500000 penalty 2 = 2 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 9 variables
c [basicprobe-4] limit 46448010 penalty 0 = 0 + 0
c [basicprobe-4-0] 1658 sched 27%, 7 failed, 0 lifted, 1017 hbrs
c [decomp-33] removed 21 variables
c [basicprobe-4-1] 3600 sched 58%, 13 failed, 0 lifted, 1593 hbrs
c [decomp-34] removed 21 variables
c [basicprobe-4-2] 3599 sched 58%, 0 failed, 0 lifted, 58 hbrs
c [basicprobe-4-3] 3598 sched 58%, 0 failed, 0 lifted, 33 hbrs
c [basicprobe-4-4] 3597 sched 58%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-4-5] 3597 sched 58%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-4-6] 3597 sched 58%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-4-7] 17 probes remain 0% after last round
c [basicprobe-4-7] 20 units = 20 failed (100%) + 0 lifted (0%)
c [basicprobe-4-7] removed 42 variables, found 2710 hbrs
c [bate-3] eliminated 3 asymmetric tautologies during probing
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 523 transitive binary clauses
c [bca-9] limit of 10000000 steps and 70095 added (scaled 2)
c [bca-9] 1535 out of 12362 literals actually usable 12%
c [bca-9] added 3 blocked clauses in 74252 steps
c [sweep-10] limit 2786880 penalty 0 = 0 + 0
c [sweep-10-1] 250 pos 41.8% + 348 neg 58.2% = 598 sched 9.7% ret 5582
c [sweep-10-1] 2794254 steps 131 queries 26.21 avg class size
c [sweep-10-1] 2529 decisions 117 SAT calls 58.62 avg env size
c [sweep-10-1] 299 variables remain 5% (5881 retained 95%)
c [decomp-40] removed 39 variables
c [sweep-10-1] removed 39 vars (0 failed, 37 eqs, 31 impls)
c [sweep-10] removed 39 vars in TOTAL (1 rounds, 130 queries)
c [sort-queue-11] sorted 3859 enqueued variables after 202430 conflicts
c [score-dist-11] active 2282 (37%), one 3857 (63%), zero 2 (0%)
c [score-dist-11] max exp 774, different 261 (34%)
c [score-dist-11] median active exp 716, avg 648.2
c [simplification-11] removed 90 variables 1.4% (6141 remain 20%)
c [simplification-11] removed 184 irredundant clauses 0.5% (34643 remain 39%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 27081 = 54163 / 2
c [simplification-11] new conflict interval 81244
c [simplification-11] penalized conflict interval 81244 = 1 * 81244
c [simplification-11] hard conflict limit 324296 (soft 283674 + delta 40622)
c [simplification-11] new conflict limit 283674 (hard 324296)
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 -   49.7    6141    34643    217024   51602   9384 11740    9    40   18  24%    -13  -13   12    8  148%
c -   55.9    6141    34643    257450   56869   9427 11751    9    44   19  22%    465   -0    9    9  106%
c i   58.6    6140    34643    274830   73536   9438 11754    9    40   22  24%    595   -3   10    9  120%
c -   62.0    6140    34643    296130   60615   9455 11756    9    29   19  32%   -371  -11   11    9  126%
c i   62.1    6139    34643    296931   61388   9455 11758    9    32   22  30%   -354   -8   11    9  126%
c 
c [simplification-12] limit 283674 conflicts (hard 324296) hit after 324296 conflicts
c [quatres-10] found 12909 quaternary clauses 24% in total
c [quatres-10-1] removed 21 duplicate quaternary clauses
c [quatres-10-1] added 4 double-self-subsuming ternary resolvents
c [quatres-10-2] added 80 single-self-subsuming ternary resolvents
c [quatres-10-2] added 90 quaternary resolvents
c [ternres-10] limit 15905364 with penalty 0 = 0 + 0
c [ternres-10] all 6139 free variables schedulable
c [ternres-10] 1259 ternary resolvents (55 bin, 1204 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-41] removed 19 variables
c [simpleprobe-5] all 6122 free variables schedulable
c [simpleprobe-5] limit 63621459 penalty 0 = 0 + 0
c [decomp-42] removed 33 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 33 variables, found 1743 hbrs, 9 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 913 transitive binary clauses
c [transred-10] found 1 units
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 6088 variables 100%
c [elim-10] limit of 159053649 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 58 variables 1% in round 1 in 9030340 steps
c [elim-10-1] backward subsumption/strengthening limit 9030300
c [elim-10-1-1] backward checking 322 touched variables 5%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 673121 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 58 = 1% variables out of 6088 scheduled
c [elim-10] 58 < 1/100 * 6088 = 60 considered unsuccessful
c [bca-10] limit of 10000000 steps and 68780 added (scaled 2)
c [bca-10] 1718 out of 12062 literals actually usable 14%
c [bca-10] added 1 blocked clauses in 90075 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 47716090 penalty 0 = 0 + 0
c [sweep-11-1] 119 pos 41.6% + 167 neg 58.4% = 286 sched 4.7% ret 5744
c [sweep-11-1] 3576175 steps 149 queries 11.54 avg class size
c [sweep-11-1] 3042 decisions 139 SAT calls 63.04 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-43] removed 27 variables
c [sweep-11-1] removed 27 vars (0 failed, 27 eqs, 22 impls)
c [sweep-11-2] 2526 pos 42.1% + 3477 neg 57.9% = 6003 sched 100.0% ret 0
c [sweep-11-2] 22376774 steps 748 queries 31.86 avg class size
c [sweep-11-2] 14205 decisions 645 SAT calls 67.08 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-44] removed 211 variables
c [sweep-11-2] removed 211 vars (0 failed, 218 eqs, 233 impls)
c [sweep-11-3] 2451 pos 42.3% + 3341 neg 57.7% = 5792 sched 100.0% ret 0
c [sweep-11-3] 16286401 steps 571 queries 25.44 avg class size
c [sweep-11-3] 12596 decisions 556 SAT calls 71.56 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-45] removed 68 variables
c [sweep-11-3] removed 68 vars (0 failed, 77 eqs, 59 impls)
c [sweep-11] removed 306 vars in TOTAL (3 rounds, 1465 queries)
c [sort-queue-12] sorted 1820 enqueued variables after 324296 conflicts
c [score-dist-12] active 3904 (68%), one 1818 (32%), zero 2 (0%)
c [score-dist-12] max exp 826, different 489 (59%)
c [score-dist-12] median active exp 627, avg 591.3
c [simplification-12] removed 415 variables 6.8% (5724 remain 19%)
c [simplification-12] removed 892 irredundant clauses 2.6% (33751 remain 38%)
c [simplification-12] maximum reduction of 7% = max (7%, 3%)
c [simplification-12] large reduction 7% >= 5% limit
c [simplification-12] next conflict interval 3242 = min (324296/100, 81244)
c [simplification-12] penalized conflict interval 3242 = 1 * 3242
c [simplification-12] hard conflict limit 337538 (soft 327538 + delta 10000)
c [simplification-12] new conflict limit 327538 (hard 337538)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   69.4    5723    33751    325290   88282   8107 11818    9    27   21  34%    -97  -10   11    9  124%
c -   70.9    5723    33747    333490   61702   8116 11819    9    39   13  22%   -363    2    6    9   63%
c 
c [simplification-13] limit 327538 conflicts (hard 337538) hit after 337538 conflicts
c [quatres-11] found 12709 quaternary clauses 24% in total
c [quatres-11-1] removed 62 duplicate quaternary clauses
c [quatres-11-1] added 10 double-self-subsuming ternary resolvents
c [quatres-11-2] added 74 single-self-subsuming ternary resolvents
c [quatres-11-2] added 165 quaternary resolvents
c [ternres-11] limit 16695513 with penalty 0 = 0 + 0
c [ternres-11] all 5723 free variables schedulable
c [ternres-11] 859 ternary resolvents (50 bin, 809 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-46] removed 8 variables
c [treelook-5] limit 1669551 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 11432 literals 100%
c [treelook-5] scheduling used 362065 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 1669551 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1676617 steps
c [treelook-5] 11058 literals remain 97%
c [treelook-5] 5702 variables remain to probed next time 100%
c [decomp-47] removed 1 variables
c [treelook-5] removed 7 variables, found 2129 hbrs
c [unhide-6] limit 417387 with penalty 3 = 3 + 0
c [unhide-6-6] 0 units, 0 failed, 3156 tauts, 0 hbrs, 25948 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 454 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 5709 variables 100%
c [block-6] limit of 41738784 steps penalty 2 = 2 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 114 blocked clauses
c [block-6] 114 < 1/100 * 33433 = 334 considered unsuccessful
c [cce-6] limit of 10434696 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 2 clauses out of 41 (5%) of length 13
c [cce-6-1] eliminated 1 clauses out of 74 (1%) of length 11
c [cce-6-1] eliminated 11 clauses out of 235 (5%) of length 9
c [cce-6-1] eliminated 26 clauses out of 377 (7%) of length 8
c [cce-6-1] eliminated 43 clauses out of 811 (5%) of length 7
c [cce-6-1] eliminated 182 clauses out of 1675 (11%) of length 6
c [cce-6-1] eliminated 227 clauses out of 2933 (8%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 492 large clauses in 10434848 steps
c [cce-6-1] allowing another 5217424 steps for small clauses
c [cce-6-1] scheduling 10745 clauses = 5723 binary + 5022 ternary
c [cce-6-1] tried to eliminate 6411 small clauses 60%
c [cce-6-1] eliminated 81 binary clauses 1%
c [cce-6-1] eliminated 224 ternary clauses 4%
c [cce-6-1] eliminated 305 small clauses 3%
c [cce-6-1] eliminated 305 small clauses in 10434757 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 797 covered clauses in round 1
c [cce-6] eliminated 797 covered clauses in TOTAL during 1 rounds
c [bca-11] limit of 10000000 steps and 65835 added (scaled 2)
c [bca-11] 1763 out of 11386 literals actually usable 15%
c [bca-11] added 1 blocked clauses in 67258 steps
c [sweep-12] limit 5008654 penalty 0 = 0 + 0
c [sweep-12-1] 2322 pos 40.8% + 3370 neg 59.2% = 5692 sched 100.0% ret 0
c [sweep-12-1] 5135346 steps 186 queries 103.60 avg class size
c [sweep-12-1] 5080 decisions 182 SAT calls 75.51 avg env size
c [sweep-12-1] 1798 variables remain 32% (3894 retained 68%)
c [decomp-48] removed 3 variables
c [sweep-12-1] removed 3 vars (0 failed, 4 eqs, 2 impls)
c [sweep-12] 3 < 1/1000 * 5692 = 5 considered unsuccessful
c [sweep-12] removed 3 vars in TOTAL (1 rounds, 185 queries)
c [sort-queue-13] sorted 2762 enqueued variables after 337538 conflicts
c [score-dist-13] active 2927 (51%), one 2760 (49%), zero 2 (0%)
c [score-dist-13] max exp 900, different 280 (31%)
c [score-dist-13] median active exp 830, avg 761.5
c [simplification-13] removed 34 variables 0.6% (5689 remain 18%)
c [simplification-13] removed 1224 irredundant clauses 3.6% (32521 remain 36%)
c [simplification-13] maximum reduction of 4% = max (1%, 4%)
c [simplification-13] geometric conflict interval increment 16248 = 81244 / 5
c [simplification-13] new conflict interval 97492
c [simplification-13] penalized conflict interval 97492 = 1 * 97492
c [simplification-13] hard conflict limit 483776 (soft 435030 + delta 48746)
c [simplification-13] new conflict limit 435030 (hard 483776)
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 -   78.3    5689    32512    375800   66348   8154 11537    9    44   18  21%    297    7    6    9   73%
c i   81.6    5688    32511    399855   88880   8172 11544    8    16   24  49%    520  -19    6    9   66%
c -   84.7    5688    32507    414653   68983   8183 11545   10    48   18  20%   -322   12   11    9  120%
c i   86.3    5687    32507    424327   78224   8192 11546    9    42   22  22%   -138    5   11    9  125%
c -   92.1    5687    32505    454472   71919   8207 11548    8    27   18  29%     46   -9    7    9   77%
c 
c [simplification-14] limit 435030 conflicts (hard 483776) hit after 478681 conflicts
c [quatres-12] found 12684 quaternary clauses 21% in total
c [quatres-12-1] removed 15 duplicate quaternary clauses
c [quatres-12-1] added 3 double-self-subsuming ternary resolvents
c [quatres-12-2] added 52 single-self-subsuming ternary resolvents
c [quatres-12-2] added 162 quaternary resolvents
c [ternres-12] limit 25440214 with penalty 0 = 0 + 0
c [ternres-12] all 5687 free variables schedulable
c [ternres-12] 413 ternary resolvents (19 bin, 394 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-49] removed 3 variables
c [basicprobe-5] limit 127201070 penalty 0 = 0 + 0
c [basicprobe-5-0] 154 sched 3%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-5-1] 3342 sched 59%, 1 failed, 0 lifted, 484 hbrs
c [decomp-51] removed 1 variables
c [basicprobe-5-2] 3326 sched 59%, 0 failed, 0 lifted, 41 hbrs
c [basicprobe-5-3] 3327 sched 59%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-5-4] 3327 sched 59%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-4] fully completed probing
c [basicprobe-5-4] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-5-4] removed 1 variables, found 541 hbrs
c [bate-4] eliminated 7 asymmetric tautologies during probing
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 272 transitive binary clauses
c [bca-12] limit of 10000000 steps and 65733 added (scaled 2)
c [bca-12] 1835 out of 11372 literals actually usable 16%
c [bca-12] added 1 blocked clauses in 97582 steps
c [sort-queue-14] sorted 2472 enqueued variables after 478681 conflicts
c [score-dist-14] active 3213 (57%), one 2470 (43%), zero 2 (0%)
c [score-dist-14] max exp 909, different 276 (30%)
c [score-dist-14] median active exp 853, avg 807.4
c [simplification-14] removed 2 variables 0.0% (5685 remain 18%)
c [simplification-14] removed 33 irredundant clauses 0.1% (32471 remain 36%)
c [simplification-14] maximum reduction of 0% = max (0%, 0%)
c [simplification-14] full geometric conflict interval increment 97492
c [simplification-14] new conflict interval 194984
c [simplification-14] penalized conflict interval 194984 = 1 * 194984
c [simplification-14] hard conflict limit 771157 (soft 673665 + delta 97492)
c [simplification-14] new conflict limit 673665 (hard 771157)
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 -  102.5    5685    32470    495839   73821   8531 11627   11    35   21  32%    504    3   10    9  115%
c -  111.1    5685    32469    536930   76591   8565 11627   11    40   21  27%    746    4   10    9  108%
c -  118.8    5685    32469    578096   78991   8585 11628   10    32   21  32%    876   -3    9   10   90%
c -  125.7    5685    32469    620926   83168   8591 11628   11    32   22  34%    947    1   13   10  141%
c -  131.8    5685    32469    663280   87603   8596 11631    8    70   22  12%    984   40   10    9  109%
c 
c [simplification-15] limit 673665 conflicts (hard 771157) hit after 673666 conflicts
c [quatres-13] found 13042 quaternary clauses 19% in total
c [quatres-13-1] added 11 double-self-subsuming ternary resolvents
c [quatres-13-2] added 81 single-self-subsuming ternary resolvents
c [quatres-13-2] added 47 quaternary resolvents
c [ternres-13] limit 38279442 with penalty 0 = 0 + 0
c [ternres-13] all 5685 free variables schedulable
c [ternres-13] 217 ternary resolvents (15 bin, 202 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 1196232 penalty 4 = 4 + 0
c [card-5] found 317 at-most-one constraints of average size 3.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1196232 for elimination
c [card-5] 317 out of 317 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-7] limit 956986 penalty 3 = 3 + 0
c [gauss-7] extracted 2411 xors of average arity 3.0
c [gauss-7] connected 7212 occurrences of 614 variables (average 11.7)
c [gauss-7] limit 956986 penalty 3 = 3 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-54] removed 2 variables
c [simpleprobe-6] all 5683 free variables schedulable
c [simpleprobe-6] limit 153117769 penalty 0 = 0 + 0
c [decomp-55] removed 8 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 8 variables, found 1268 hbrs, 0 units
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 567 transitive binary clauses
c [cce-7] limit of 47849302 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 4 clauses out of 35 (11%) of length 13
c [cce-7-1] eliminated 4 clauses out of 75 (5%) of length 11
c [cce-7-1] eliminated 1 clauses out of 113 (1%) of length 10
c [cce-7-1] eliminated 4 clauses out of 224 (2%) of length 9
c [cce-7-1] eliminated 8 clauses out of 339 (2%) of length 8
c [cce-7-1] eliminated 25 clauses out of 778 (3%) of length 7
c [cce-7-1] eliminated 35 clauses out of 1487 (2%) of length 6
c [cce-7-1] eliminated 160 clauses out of 2676 (6%) of length 5
c [cce-7-1] eliminated 646 clauses out of 6742 (10%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 887 large clauses in 32058689 steps
c [cce-7-1] allowing another 16029344 steps for small clauses
c [cce-7-1] scheduling 10450 clauses = 5634 binary + 4816 ternary
c [cce-7-1] tried to eliminate 10450 small clauses 100%
c [cce-7-1] eliminated 251 binary clauses 4%
c [cce-7-1] eliminated 308 ternary clauses 6%
c [cce-7-1] eliminated 559 small clauses 5%
c [cce-7-1] eliminated 559 small clauses in 35321642 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 1446 covered clauses in round 1
c [cce-7-2] eliminated 10 clauses out of 331 (3%) of length 8
c [cce-7-2] eliminated 12 clauses out of 753 (2%) of length 7
c [cce-7-2] eliminated 19 clauses out of 1452 (1%) of length 6
c [cce-7-2] eliminated 5 clauses out of 2516 (0%) of length 5
c [cce-7-2] incomplete large round (ACCE)
c [cce-7-2] eliminated 46 large clauses in 12527727 steps
c [cce-7-2] allowing another 6263863 steps for small clauses
c [cce-7-2] scheduling 9893 clauses = 5383 binary + 4510 ternary
c [cce-7-2] tried to eliminate 5369 small clauses 54%
c [cce-7-2] eliminated 13 binary clauses 0%
c [cce-7-2] eliminated 20 ternary clauses 0%
c [cce-7-2] eliminated 33 small clauses 0%
c [cce-7-2] eliminated 33 small clauses in 12527866 steps
c [cce-7-2] incomplete small round (ACCE)
c [cce-7-2] eliminated 79 covered clauses in round 2
c [cce-7] eliminated 1525 covered clauses in TOTAL during 2 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 5675 variables 100%
c [elim-11] limit of 191397211 steps penalty 2 = 2 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 405 variables 7% in round 1 in 7517335 steps
c [elim-11-1] backward subsumption/strengthening limit 7517300
c [elim-11-1-1] backward checking 1202 touched variables 21%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 2 and strengthened 7 clauses in 803297 steps
c [elim-11-1] rescheduled 28 variables 0% by backward subsumption
c [elim-11-2] eliminated 2 variables 0% in round 2 in 361755 steps
c [elim-11-2] backward subsumption/strengthening limit 361700
c [elim-11-2-1] backward checking 8 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 3 clauses in 22834 steps
c [elim-11-2] rescheduled 7 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 3431 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 407 = 7% variables out of 5675 scheduled
c [bca-13] limit of 10000000 steps and 59918 added (scaled 2)
c [bca-13] 1833 out of 10538 literals actually usable 17%
c [bca-13] added 6 blocked clauses in 96751 steps
c [sweep-13] limit 5741916 penalty 1 = 1 + 0
c [sweep-13-1] 617 pos 38.3% + 992 neg 61.7% = 1609 sched 30.5% ret 3659
c [sweep-13-1] 5760315 steps 172 queries 33.45 avg class size
c [sweep-13-1] 4269 decisions 175 SAT calls 66.42 avg env size
c [sweep-13-1] 549 variables remain 10% (4719 retained 90%)
c [decomp-56] removed 6 variables
c [sweep-13-1] removed 6 vars (0 failed, 6 eqs, 3 impls)
c [sweep-13] removed 6 vars in TOTAL (1 rounds, 171 queries)
c [sort-queue-15] sorted 2253 enqueued variables after 673666 conflicts
c [score-dist-15] active 3009 (57%), one 2253 (43%), zero 0 (0%)
c [score-dist-15] max exp 662, different 252 (38%)
c [score-dist-15] median active exp 606, avg 575.7
c [simplification-15] removed 423 variables 7.4% (5262 remain 17%)
c [simplification-15] removed 2906 irredundant clauses 9.0% (29563 remain 33%)
c [simplification-15] maximum reduction of 9% = max (7%, 9%)
c [simplification-15] large reduction 9% >= 5% limit
c [simplification-15] next conflict interval 6736 = min (673666/100, 194984)
c [simplification-15] penalized conflict interval 6736 = 1 * 6736
c [simplification-15] hard conflict limit 690402 (soft 680402 + delta 10000)
c [simplification-15] new conflict limit 680402 (hard 690402)
c 
c [simplification-16] limit 680402 conflicts (hard 690402) hit after 680402 conflicts
c [quatres-14] found 11738 quaternary clauses 18% 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 15 single-self-subsuming ternary resolvents
c [quatres-14-2] added 64 quaternary resolvents
c [ternres-14] limit 38767354 with penalty 0 = 0 + 0
c [ternres-14] all 5262 free variables schedulable
c [ternres-14] 194 ternary resolvents (14 bin, 180 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-57] removed 1 variables
c [treelook-6] limit 3876735 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 10517 literals 100%
c [treelook-6] scheduling used 436745 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3876735 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 3876765 steps
c [treelook-6] 8597 literals remain 82%
c [treelook-6] 5213 variables remain to probed next time 99%
c [decomp-58] removed 1 variables
c [treelook-6] removed 1 variables, found 2360 hbrs
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 540 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 969183870 steps penalty 1 = 1 + 0
c [cce-8-1] eliminated 2 clauses out of 97 (2%) of length 12
c [cce-8-1] eliminated 3 clauses out of 122 (2%) of length 10
c [cce-8-1] eliminated 18 clauses out of 258 (7%) of length 9
c [cce-8-1] eliminated 22 clauses out of 367 (6%) of length 8
c [cce-8-1] eliminated 30 clauses out of 762 (4%) of length 7
c [cce-8-1] eliminated 46 clauses out of 1574 (3%) of length 6
c [cce-8-1] eliminated 40 clauses out of 2523 (2%) of length 5
c [cce-8-1] eliminated 60 clauses out of 5963 (1%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 221 large clauses in 17867887 steps
c [cce-8-1] allowing another 8933943 steps for small clauses
c [cce-8-1] scheduling 13501 clauses = 5048 binary + 8453 ternary
c [cce-8-1] tried to eliminate 13501 small clauses 100%
c [cce-8-1] eliminated 3 binary clauses 0%
c [cce-8-1] eliminated 200 ternary clauses 2%
c [cce-8-1] eliminated 203 small clauses 2%
c [cce-8-1] eliminated 203 small clauses in 25942586 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 424 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 8644006 steps for small clauses
c [cce-8-2] scheduling 13298 clauses = 5045 binary + 8253 ternary
c [cce-8-2] tried to eliminate 13298 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 424 covered clauses in TOTAL during 2 rounds
c [bca-14] limit of 10000000 steps and 59059 added (scaled 2)
c [bca-14] 1786 out of 10522 literals actually usable 17%
c [bca-14] added 1 blocked clauses in 103389 steps
c [sweep-14] limit 11630206 penalty 0 = 0 + 0
c [sweep-14-1] 230 pos 41.9% + 319 neg 58.1% = 549 sched 10.4% ret 4711
c [sweep-14-1] 4912122 steps 216 queries 13.34 avg class size
c [sweep-14-1] 3827 decisions 214 SAT calls 48.98 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-59] removed 15 variables
c [sweep-14-1] removed 15 vars (0 failed, 16 eqs, 6 impls)
c [sweep-14-2] 2124 pos 40.5% + 3121 neg 59.5% = 5245 sched 100.0% ret 0
c [sweep-14-2] 6774863 steps 169 queries 92.51 avg class size
c [sweep-14-2] 5161 decisions 174 SAT calls 72.98 avg env size
c [sweep-14-2] 1621 variables remain 31% (3624 retained 69%)
c [decomp-60] removed 8 variables
c [sweep-14-2] removed 8 vars (0 failed, 7 eqs, 6 impls)
c [sweep-14] removed 23 vars in TOTAL (2 rounds, 383 queries)
c [sort-queue-16] sorted 2722 enqueued variables after 680402 conflicts
c [score-dist-16] active 2515 (48%), one 2722 (52%), zero 0 (0%)
c [score-dist-16] max exp 677, different 221 (33%)
c [score-dist-16] median active exp 614, avg 586.5
c [simplification-16] removed 25 variables 0.5% (5237 remain 17%)
c [simplification-16] removed 450 irredundant clauses 1.5% (29113 remain 32%)
c [simplification-16] maximum reduction of 2% = max (0%, 2%)
c [simplification-16] geometric conflict interval increment 64994 = 194984 / 3
c [simplification-16] new conflict interval 259978
c [simplification-16] penalized conflict interval 259978 = 1 * 259978
c [simplification-16] hard conflict limit 1070369 (soft 940380 + delta 129989)
c [simplification-16] new conflict limit 940380 (hard 1070369)
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 -  146.1    5237    29113    704314   83977   8564 11742   12    36   22  33%   1002    5   12    9  121%
c i  146.7    5236    29113    707493   87046   8564 11742   12    35   26  33%   1003    4   12   10  126%
c -  154.2    5236    29113    747464   86487   8578 11742   12    33   22  36%  -1430   -4   12   10  120%
c -  162.0    5236    29113    792340   90800   8586 11743    9    40   23  24%   -213    2   12   10  120%
c -  171.7    5236    29113    834253   90424   8601 11744   10    29   22  36%    371   -9    6   10   58%
c -  178.0    5236    29113    889748   94600   8626 11746    8     9   23  90%    744  -14    8    9   81%
c i  179.1    5235    29113    900034  101154   8685 11757    7     8   27  91%    785  -13    5    9   59%
c i  181.7    3764    29113    913508  113850   8689 11759   10    41   29  24%  -1659   19   10    9  115%
c -  187.3    3762    29113    936892   96399   8702 11761   10    34   23  30%  -1003    9   12    9  127%
c 
c [simplification-17] limit 940380 conflicts (hard 1070369) hit after 981659 conflicts
c [quatres-15] found 6716 quaternary clauses 12% in total
c [quatres-15-2] added 24 single-self-subsuming ternary resolvents
c [quatres-15-2] added 249 quaternary resolvents
c [ternres-15] limit 60952460 with penalty 0 = 0 + 0
c [ternres-15] all 3762 free variables schedulable
c [ternres-15] 136 ternary resolvents (9 bin, 127 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-61] removed 2042 variables
c [basicprobe-6] limit 304762301 penalty 0 = 0 + 0
c [basicprobe-6-0] 1754 sched 56%, 31 failed, 1 lifted, 3011 hbrs
c [decomp-62] removed 82 variables
c [basicprobe-6-1] 1660 sched 53%, 3 failed, 0 lifted, 538 hbrs
c [decomp-63] removed 7 variables
c [basicprobe-6-2] 1636 sched 53%, 0 failed, 0 lifted, 44 hbrs
c [basicprobe-6-3] 1637 sched 53%, 0 failed, 0 lifted, 16 hbrs
c [basicprobe-6-4] 1642 sched 53%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-6-5] 1643 sched 53%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-6-6] 1643 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-6] fully completed probing
c [basicprobe-6-6] 35 units = 34 failed (97%) + 1 lifted (3%)
c [basicprobe-6-6] removed 89 variables, found 3621 hbrs
c [bate-5] eliminated 270 asymmetric tautologies during probing
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 664 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 3106 variables 100%
c [block-7] limit of 76190575 steps penalty 3 = 3 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 548 blocked clauses
c [cce-9] limit of 304762301 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-9-1] eliminated 6 clauses out of 17 (35%) of length 12
c [cce-9-1] eliminated 14 clauses out of 27 (52%) of length 11
c [cce-9-1] eliminated 8 clauses out of 29 (28%) of length 10
c [cce-9-1] eliminated 9 clauses out of 51 (18%) of length 9
c [cce-9-1] eliminated 20 clauses out of 73 (27%) of length 8
c [cce-9-1] eliminated 30 clauses out of 158 (19%) of length 7
c [cce-9-1] eliminated 104 clauses out of 469 (22%) of length 6
c [cce-9-1] eliminated 175 clauses out of 1111 (16%) of length 5
c [cce-9-1] eliminated 341 clauses out of 3537 (10%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 708 large clauses in 10445026 steps
c [cce-9-1] allowing another 5222513 steps for small clauses
c [cce-9-1] scheduling 5683 clauses = 2953 binary + 2730 ternary
c [cce-9-1] tried to eliminate 5683 small clauses 100%
c [cce-9-1] eliminated 317 binary clauses 11%
c [cce-9-1] eliminated 219 ternary clauses 8%
c [cce-9-1] eliminated 536 small clauses 9%
c [cce-9-1] eliminated 536 small clauses in 10866055 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 1244 covered clauses in round 1
c [cce-9-2] eliminated 9 clauses out of 936 (1%) of length 5
c [cce-9-2] eliminated 51 clauses out of 3196 (2%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 60 large clauses in 8669493 steps
c [cce-9-2] allowing another 4334746 steps for small clauses
c [cce-9-2] scheduling 5148 clauses = 2636 binary + 2512 ternary
c [cce-9-2] tried to eliminate 5148 small clauses 100%
c [cce-9-2] eliminated 28 binary clauses 1%
c [cce-9-2] eliminated 23 ternary clauses 1%
c [cce-9-2] eliminated 51 small clauses 1%
c [cce-9-2] eliminated 51 small clauses in 9183873 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 111 covered clauses in round 2
c [cce-9-3] eliminated 1 clauses out of 53 (2%) of length 8
c [cce-9-3] eliminated 3 clauses out of 365 (1%) of length 6
c [cce-9-3] eliminated 6 clauses out of 927 (1%) of length 5
c [cce-9-3] eliminated 15 clauses out of 3145 (0%) of length 4
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] eliminated 25 large clauses in 8581867 steps
c [cce-9-3] allowing another 4290933 steps for small clauses
c [cce-9-3] scheduling 5097 clauses = 2608 binary + 2489 ternary
c [cce-9-3] tried to eliminate 5097 small clauses 100%
c [cce-9-3] eliminated 3 binary clauses 0%
c [cce-9-3] eliminated 12 ternary clauses 0%
c [cce-9-3] eliminated 15 small clauses 0%
c [cce-9-3] eliminated 15 small clauses in 9134871 steps
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 40 covered clauses in round 3
c [cce-9] eliminated 1395 covered clauses in TOTAL during 3 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 3004 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 604 variables 20% in round 1 in 2204854 steps
c [elim-12-1] backward subsumption/strengthening limit 2204800
c [elim-12-1-1] backward checking 1108 touched variables 37%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 3 and strengthened 17 clauses in 181940 steps
c [elim-12-1] rescheduled 51 variables 2% by backward subsumption
c [elim-12-2] eliminated 3 variables 0% in round 2 in 224764 steps
c [elim-12-2] backward subsumption/strengthening limit 224700
c [elim-12-2-1] backward checking 19 touched variables 1%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 0 and strengthened 0 clauses in 20050 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 607 = 20% variables out of 3004 scheduled
c [bca-15] limit of 10000000 steps and 27399 added (scaled 2)
c [bca-15] 395 out of 4796 literals actually usable 8%
c [bca-15] added 7 blocked clauses in 107248 steps
c [sweep-15] limit 18285738 penalty 0 = 0 + 0
c [sweep-15-1] 217 pos 39.5% + 332 neg 60.5% = 549 sched 22.9% ret 1848
c [sweep-15-1] 11056473 steps 130 queries 8.75 avg class size
c [sweep-15-1] 3989 decisions 129 SAT calls 102.93 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-68] removed 21 variables
c [sweep-15-1] removed 21 vars (0 failed, 22 eqs, 11 impls)
c [sweep-15-2] 940 pos 39.6% + 1436 neg 60.4% = 2376 sched 100.0% ret 0
c [sweep-15-2] 7882751 steps 91 queries 40.38 avg class size
c [sweep-15-2] 3280 decisions 91 SAT calls 137.46 avg env size
c [sweep-15-2] 464 variables remain 20% (1912 retained 80%)
c [decomp-69] removed 7 variables
c [sweep-15-2] removed 7 vars (0 failed, 6 eqs, 3 impls)
c [sweep-15] removed 28 vars in TOTAL (2 rounds, 219 queries)
c [sort-queue-17] sorted 275 enqueued variables after 981659 conflicts
c [score-dist-17] active 2094 (88%), one 275 (12%), zero 0 (0%)
c [score-dist-17] max exp 762, different 263 (34%)
c [score-dist-17] median active exp 680, avg 598.1
c [simplification-17] removed 1393 variables 37.0% (2369 remain 8%)
c [simplification-17] removed 15848 irredundant clauses 54.4% (13265 remain 15%)
c [simplification-17] maximum reduction of 54% = max (37%, 54%)
c [simplification-17] large reduction 54% >= 5% limit
c [simplification-17] next conflict interval 9816 = min (981659/100, 259978)
c [simplification-17] penalized conflict interval 9816 = 1 * 9816
c [simplification-17] hard conflict limit 1001475 (soft 991475 + delta 10000)
c [simplification-17] new conflict limit 991475 (hard 1001475)
c 
c [simplification-18] limit 991475 conflicts (hard 1001475) hit after 991475 conflicts
c [quatres-16] found 7432 quaternary clauses 12% in total
c [quatres-16-1] removed 42 duplicate quaternary clauses
c [quatres-16-1] added 2 double-self-subsuming ternary resolvents
c [quatres-16-2] added 34 single-self-subsuming ternary resolvents
c [quatres-16-2] added 133 quaternary resolvents
c [ternres-16] limit 61635735 with penalty 0 = 0 + 0
c [ternres-16] all 2369 free variables schedulable
c [ternres-16] 1103 ternary resolvents (31 bin, 1072 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-70] removed 2 variables
c [simpleprobe-7] all 2367 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-71] removed 5 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 5 variables, found 1136 hbrs, 0 units
c [unhide-7] limit 770446 with penalty 4 = 4 + 0
c [unhide-7-7] 0 units, 0 failed, 321 tauts, 0 hbrs, 62323 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 528 transitive binary clauses
c [cce-10] limit of 308178678 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 20 (5%) of length 12
c [cce-10-1] eliminated 4 clauses out of 21 (19%) of length 11
c [cce-10-1] eliminated 2 clauses out of 29 (7%) of length 10
c [cce-10-1] eliminated 9 clauses out of 74 (12%) of length 9
c [cce-10-1] eliminated 9 clauses out of 102 (9%) of length 8
c [cce-10-1] eliminated 6 clauses out of 209 (3%) of length 7
c [cce-10-1] eliminated 15 clauses out of 374 (4%) of length 6
c [cce-10-1] eliminated 45 clauses out of 984 (5%) of length 5
c [cce-10-1] eliminated 58 clauses out of 3111 (2%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 149 large clauses in 3583436 steps
c [cce-10-1] allowing another 1791718 steps for small clauses
c [cce-10-1] scheduling 4202 clauses = 1999 binary + 2203 ternary
c [cce-10-1] tried to eliminate 4202 small clauses 100%
c [cce-10-1] eliminated 25 binary clauses 1%
c [cce-10-1] eliminated 22 ternary clauses 1%
c [cce-10-1] eliminated 47 small clauses 1%
c [cce-10-1] eliminated 47 small clauses in 3915558 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 196 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 1724511 steps for small clauses
c [cce-10-2] scheduling 4155 clauses = 1974 binary + 2181 ternary
c [cce-10-2] tried to eliminate 4155 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 196 covered clauses in TOTAL during 2 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 2362 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 32 variables 1% in round 1 in 1953351 steps
c [elim-13-1] backward subsumption/strengthening limit 1953300
c [elim-13-1-1] backward checking 238 touched variables 10%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 2 clauses in 95491 steps
c [elim-13-1] rescheduled 12 variables 1% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 81785 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 32 = 1% variables out of 2362 scheduled
c [bca-16] limit of 10000000 steps and 26623 added (scaled 2)
c [bca-16] 352 out of 4662 literals actually usable 8%
c [bca-16] added 4 blocked clauses in 116810 steps
c [sweep-16] limit 18490720 penalty 0 = 0 + 0
c [sweep-16-1] 154 pos 34.6% + 291 neg 65.4% = 445 sched 19.1% ret 1885
c [sweep-16-1] 7741665 steps 122 queries 8.41 avg class size
c [sweep-16-1] 3607 decisions 121 SAT calls 102.31 avg env size
c [sweep-16-1] fully completed sweeping round
c [decomp-72] removed 13 variables
c [sweep-16-1] removed 13 vars (0 failed, 14 eqs, 10 impls)
c [sweep-16-2] 907 pos 39.1% + 1410 neg 60.9% = 2317 sched 100.0% ret 0
c [sweep-16-2] 10943044 steps 166 queries 38.02 avg class size
c [sweep-16-2] 5254 decisions 165 SAT calls 109.81 avg env size
c [sweep-16-2] 30 variables remain 1% (2287 retained 99%)
c [decomp-73] removed 6 variables
c [sweep-16-2] removed 6 vars (0 failed, 7 eqs, 8 impls)
c [sweep-16] removed 19 vars in TOTAL (2 rounds, 286 queries)
c [sort-queue-18] sorted 466 enqueued variables after 991475 conflicts
c [score-dist-18] active 1845 (80%), one 466 (20%), zero 0 (0%)
c [score-dist-18] max exp 789, different 224 (28%)
c [score-dist-18] median active exp 760, avg 716.4
c [simplification-18] removed 58 variables 2.4% (2311 remain 7%)
c [simplification-18] removed 372 irredundant clauses 2.8% (12893 remain 14%)
c [simplification-18] maximum reduction of 3% = max (2%, 3%)
c [simplification-18] geometric conflict interval increment 64994 = 259978 / 4
c [simplification-18] new conflict interval 324972
c [simplification-18] penalized conflict interval 324972 = 1 * 324972
c [simplification-18] hard conflict limit 1478933 (soft 1316447 + delta 162486)
c [simplification-18] new conflict limit 1316447 (hard 1478933)
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 -  207.6    2311    12893   1002212   86454   5327  4924    9    36   21  25%    276    2    8    9   88%
c i  215.9    2310    12893   1045473  126381   5349  4925   11    32   30  33%    637    3   11    9  126%
c -  217.4    2310    12893   1048847   89628   5359  4925   11    36   21  31%  -1255    6   10    9  108%
c -  229.3    2310    12893   1094609   90135   5398  4928   12    37   22  31%   -148    5   11   10  119%
c i  236.2    2309    12893   1131762  124345   5428  4933    9    42   32  22%    359   10   10   10  101%
c -  239.4    2309    12893   1143905   93597   5432  4935   10    39   23  27%   -667    5    9   10   96%
c -  249.1    2309    12893   1191458   96138   5459  4937   10    40   23  24%    206    6    8   10   82%
c -  259.4    2309    12893   1241703  100266   5475  4941    8    21   24  41%    644  -12    7   10   71%
c -  270.6    2309    12893   1287792   99778   5498  4946   10    34   24  30%    836    1   13   10  124%
c 
c [simplification-19] limit 1316447 conflicts (hard 1478933) hit after 1316447 conflicts
c [quatres-17] found 7818 quaternary clauses 11% in total
c [quatres-17-1] removed 22 duplicate quaternary clauses
c [quatres-17-1] added 1 double-self-subsuming ternary resolvents
c [quatres-17-2] added 56 single-self-subsuming ternary resolvents
c [quatres-17-2] added 92 quaternary resolvents
c [ternres-17] limit 87971130 with penalty 0 = 0 + 0
c [ternres-17] all 2309 free variables schedulable
c [ternres-17] 522 ternary resolvents (11 bin, 511 trn)
c [ternres-17] fully completed ternary resolution
c [decomp-74] removed 2 variables
c [treelook-7] limit 8797113 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 4612 literals 100%
c [treelook-7] scheduling used 429259 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 8797113 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 3164330 steps
c [treelook-7] fully completed tree based probing
c [decomp-75] removed 2 variables
c [treelook-7] removed 8 variables, found 1276 hbrs
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 403 transitive binary clauses
c [block-8] scheduling all variables this time
c [block-8] scheduled 2301 variables 100%
c [block-8] limit of 200000000 steps penalty 2 = 2 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 79 blocked clauses
c [block-8] 79 < 1/100 * 12809 = 128 considered unsuccessful
c [cce-11] limit of 439855654 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 1 clauses out of 23 (4%) of length 10
c [cce-11-1] eliminated 2 clauses out of 83 (2%) of length 8
c [cce-11-1] eliminated 8 clauses out of 199 (4%) of length 7
c [cce-11-1] eliminated 10 clauses out of 385 (3%) of length 6
c [cce-11-1] eliminated 59 clauses out of 924 (6%) of length 5
c [cce-11-1] eliminated 66 clauses out of 2988 (2%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 146 large clauses in 7544909 steps
c [cce-11-1] allowing another 3772454 steps for small clauses
c [cce-11-1] scheduling 4054 clauses = 1924 binary + 2130 ternary
c [cce-11-1] tried to eliminate 4054 small clauses 100%
c [cce-11-1] eliminated 48 binary clauses 2%
c [cce-11-1] eliminated 42 ternary clauses 2%
c [cce-11-1] eliminated 90 small clauses 2%
c [cce-11-1] eliminated 90 small clauses in 6826105 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 236 covered clauses in round 1
c [cce-11-2] eliminated 2 clauses out of 375 (1%) of length 6
c [cce-11-2] eliminated 4 clauses out of 2922 (0%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 6 large clauses in 7093377 steps
c [cce-11-2] allowing another 3546688 steps for small clauses
c [cce-11-2] scheduling 3964 clauses = 1876 binary + 2088 ternary
c [cce-11-2] tried to eliminate 3964 small clauses 100%
c [cce-11-2] eliminated 1 ternary clauses 0%
c [cce-11-2] eliminated 1 small clauses 0%
c [cce-11-2] eliminated 1 small clauses in 6464157 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 7 covered clauses in round 2
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] allowing another 3562146 steps for small clauses
c [cce-11-3] scheduling 3963 clauses = 1876 binary + 2087 ternary
c [cce-11-3] tried to eliminate 3963 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 243 covered clauses in TOTAL during 3 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 2289 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 46 variables 2% in round 1 in 1860077 steps
c [elim-14-1] backward subsumption/strengthening limit 1860000
c [elim-14-1-1] backward checking 221 touched variables 10%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 65853 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 46 = 2% variables out of 2289 scheduled
c [bca-17] limit of 10000000 steps and 25581 added (scaled 2)
c [bca-17] 281 out of 4488 literals actually usable 6%
c [bca-17] added 4 blocked clauses in 123711 steps
c [sweep-17] limit 26391339 penalty 0 = 0 + 0
c [sweep-17-1] 10 pos 38.5% + 16 neg 61.5% = 26 sched 1.2% ret 2217
c [sweep-17-1] 1382868 steps 16 queries 4.75 avg class size
c [sweep-17-1] 474 decisions 14 SAT calls 98.64 avg env size
c [sweep-17-1] fully completed sweeping round
c [decomp-76] removed 2 variables
c [sweep-17-1] removed 2 vars (0 failed, 1 eqs, 1 impls)
c [sweep-17-2] 933 pos 41.6% + 1308 neg 58.4% = 2241 sched 100.0% ret 0
c [sweep-17-2] 17227680 steps 187 queries 22.57 avg class size
c [sweep-17-2] 6640 decisions 184 SAT calls 111.32 avg env size
c [sweep-17-2] fully completed sweeping round
c [decomp-77] removed 15 variables
c [sweep-17-2] removed 15 vars (0 failed, 15 eqs, 13 impls)
c [sweep-17-3] 930 pos 41.8% + 1296 neg 58.2% = 2226 sched 100.0% ret 0
c [sweep-17-3] 7850440 steps 50 queries 71.58 avg class size
c [sweep-17-3] 2482 decisions 48 SAT calls 153.98 avg env size
c [sweep-17-3] 798 variables remain 36% (1428 retained 64%)
c [decomp-78] removed 2 variables
c [sweep-17-3] removed 2 vars (0 failed, 2 eqs, 1 impls)
c [sweep-17] removed 19 vars in TOTAL (3 rounds, 250 queries)
c [sort-queue-19] sorted 309 enqueued variables after 1316447 conflicts
c [score-dist-19] active 1915 (86%), one 309 (14%), zero 0 (0%)
c [score-dist-19] max exp 624, different 270 (43%)
c [score-dist-19] median active exp 574, avg 518.0
c [simplification-19] removed 85 variables 3.7% (2224 remain 7%)
c [simplification-19] removed 557 irredundant clauses 4.3% (12336 remain 14%)
c [simplification-19] maximum reduction of 4% = max (4%, 4%)
c [simplification-19] geometric conflict interval increment 64994 = 324972 / 5
c [simplification-19] new conflict interval 389966
c [simplification-19] penalized conflict interval 389966 = 1 * 389966
c [simplification-19] hard conflict limit 1901396 (soft 1706413 + delta 194983)
c [simplification-19] new conflict limit 1706413 (hard 1901396)
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 -  283.2    2224    12336   1339100  102553   5779  5008   10    41   23  24%    938    5    8   10   74%
c i  287.2    2223    12336   1363362  125216   5782  5009    8    20   32  40%    965  -14    6   10   59%
c i  293.1    2222    12336   1385448  145541   5790  5012   12    34   35  37%  -1643    2   13   10  125%
c -  293.9    2222    12336   1388295  103612   5798  5013   12    35   23  33%  -1843    4   13   10  123%
c -  303.7    2222    12336   1437726  106230   5810  5014   10    26   22  37%   -335   -6    9   10   85%
c -  316.2    2222    12336   1487033  106687   5829  5014   12    35   23  34%    384    6   13   10  126%
c -  326.9    2222    12336   1537722  109433   5842  5014   10    19   23  50%    729  -11   12   10  113%
c -  340.3    2222    12336   1587713  109867   5852  5016   11    31   25  36%    886    2   12   10  118%
c -  352.4    2222    12336   1640147  111700   5863  5017   12    33   25  36%    962    1   14   11  127%
c -  362.6    2222    12335   1693113  115885   5871  5017   11    32   23  33%    996   -2    9   11   87%
c 
c [simplification-20] limit 1706413 conflicts (hard 1901396) hit after 1706413 conflicts
c [quatres-18] found 7960 quaternary clauses 10% in total
c [quatres-18-1] removed 2 duplicate quaternary clauses
c [quatres-18-2] added 38 single-self-subsuming ternary resolvents
c [quatres-18-2] added 75 quaternary resolvents
c [ternres-18] limit 121454098 with penalty 0 = 0 + 0
c [ternres-18] all 2222 free variables schedulable
c [ternres-18] 281 ternary resolvents (19 bin, 262 trn)
c [ternres-18] fully completed ternary resolution
c [gauss-8] limit 1518176 penalty 4 = 4 + 0
c [gauss-8] extracted 1562 xors of average arity 3.0
c [gauss-8] connected 4682 occurrences of 347 variables (average 13.5)
c [gauss-8] limit 1518176 penalty 4 = 4 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-79] removed 1 variables
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 1233 sched 56%, 2 failed, 0 lifted, 135 hbrs
c [decomp-80] removed 2 variables
c [basicprobe-7-1] 1231 sched 55%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-7-2] 1230 sched 55%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-7-3] 1230 sched 55%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-7-4] 1230 sched 55%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-7-4] fully completed probing
c [basicprobe-7-4] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-7-4] removed 2 variables, found 149 hbrs
c [bate-6] eliminated 2 asymmetric tautologies during probing
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 283 transitive binary clauses
c [cce-12] limit of 607270492 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 2 clauses out of 193 (1%) of length 7
c [cce-12-1] eliminated 17 clauses out of 366 (5%) of length 6
c [cce-12-1] eliminated 18 clauses out of 887 (2%) of length 5
c [cce-12-1] eliminated 10 clauses out of 2890 (0%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 47 large clauses in 2960307 steps
c [cce-12-1] allowing another 1480153 steps for small clauses
c [cce-12-1] scheduling 3874 clauses = 1821 binary + 2053 ternary
c [cce-12-1] tried to eliminate 3874 small clauses 100%
c [cce-12-1] eliminated 2 binary clauses 0%
c [cce-12-1] eliminated 12 ternary clauses 1%
c [cce-12-1] eliminated 14 small clauses 0%
c [cce-12-1] eliminated 14 small clauses in 3224842 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 61 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 1468057 steps for small clauses
c [cce-12-2] scheduling 3860 clauses = 1819 binary + 2041 ternary
c [cce-12-2] tried to eliminate 3860 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 61 covered clauses in TOTAL during 2 rounds
c [cce-12] 61 < 1/100 * 12292 = 122 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 2219 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 16 variables 1% in round 1 in 1801236 steps
c [elim-15-1] backward subsumption/strengthening limit 1801200
c [elim-15-1-1] backward checking 107 touched variables 5%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 31722 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 16 = 1% variables out of 2219 scheduled
c [elim-15] 16 < 1/100 * 2219 = 22 considered unsuccessful
c [bca-18] limit of 10000000 steps and 25151 added (scaled 2)
c [bca-18] 272 out of 4408 literals actually usable 6%
c [bca-18] added 2 blocked clauses in 128696 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 340 pos 43.2% + 447 neg 56.8% = 787 sched 35.7% ret 1416
c [sweep-18-1] 15254327 steps 146 queries 8.77 avg class size
c [sweep-18-1] 5493 decisions 152 SAT calls 108.45 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-84] removed 7 variables
c [sweep-18-1] removed 7 vars (0 failed, 9 eqs, 1 impls)
c [sweep-18-2] 925 pos 42.1% + 1271 neg 57.9% = 2196 sched 100.0% ret 0
c [sweep-18-2] 21126012 steps 165 queries 27.13 avg class size
c [sweep-18-2] 6625 decisions 169 SAT calls 132.29 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-85] removed 13 variables
c [sweep-18-2] removed 13 vars (0 failed, 13 eqs, 4 impls)
c [sweep-18-3] 923 pos 42.3% + 1260 neg 57.7% = 2183 sched 100.0% ret 0
c [sweep-18-3] 21254433 steps 171 queries 22.57 avg class size
c [sweep-18-3] 6651 decisions 170 SAT calls 115.65 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-86] removed 9 variables
c [sweep-18-3] removed 9 vars (0 failed, 11 eqs, 9 impls)
c [sweep-18] removed 29 vars in TOTAL (3 rounds, 479 queries)
c [sort-queue-20] sorted 375 enqueued variables after 1706413 conflicts
c [score-dist-20] active 1799 (83%), one 375 (17%), zero 0 (0%)
c [score-dist-20] max exp 912, different 289 (32%)
c [score-dist-20] median active exp 842, avg 743.4
c [simplification-20] removed 48 variables 2.2% (2174 remain 7%)
c [simplification-20] removed 185 irredundant clauses 1.5% (12150 remain 14%)
c [simplification-20] maximum reduction of 2% = max (2%, 1%)
c [simplification-20] geometric conflict interval increment 129988 = 389966 / 3
c [simplification-20] new conflict interval 519954
c [simplification-20] penalized conflict interval 519954 = 1 * 519954
c [simplification-20] hard conflict limit 2486344 (soft 2226367 + delta 259977)
c [simplification-20] new conflict limit 2226367 (hard 2486344)
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 -  378.3    2174    12147   1741459  112962   6025  4572   10    31   18  32%   1011   -2    9   11   81%
c -  389.4    2174    12147   1794920  114849   6036  4576   11    22   27  50%   1018   -8   10   11   98%
c -  401.7    2174    12147   1849177  116853   6052  4578    9    22   27  43%   1021   -7   11   11  104%
c -  414.4    2174    12147   1902388  116258   6065  4580   12    33   27  38%   1023    2   14   11  128%
c -  428.0    2174    12147   1959636  119670   6074  4584   11    33   28  35%   1024    4   15   11  137%
c -  439.1    2174    12147   2015020  122880   6086  4585    9    13   25  68%   1024  -12    7   10   69%
c -  452.1    2174    12147   2068932  122722   6099  4585   11    32   25  34%   1024    6   13   11  120%
c -  464.4    2174    12147   2125338  123974   6116  4585   11    33   25  34%   1024    6   13   11  123%
c -  479.6    2174    12147   2181573  123188   6124  4586   12    34   27  35%   1024    5   11   11   96%
c 
c [simplification-21] limit 2226367 conflicts (hard 2486344) hit after 2234412 conflicts
c [quatres-19] found 8316 quaternary clauses 9% in total
c [quatres-19-1] removed 15 duplicate quaternary clauses
c [quatres-19-1] added 6 double-self-subsuming ternary resolvents
c [quatres-19-2] added 44 single-self-subsuming ternary resolvents
c [quatres-19-2] added 91 quaternary resolvents
c [ternres-19] limit 170658259 with penalty 0 = 0 + 0
c [ternres-19] all 2174 free variables schedulable
c [ternres-19] 372 ternary resolvents (23 bin, 349 trn)
c [ternres-19] fully completed ternary resolution
c [card-6] limit 5333070 penalty 4 = 4 + 0
c [card-6] found 217 at-most-one constraints of average size 3.0
c [card-6] found 76 at-most-two constraints of average size 4.0
c [card-6] using previous limit 5333070 for elimination
c [card-6] 293 out of 293 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-87] removed 4 variables
c [simpleprobe-8] all 2170 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-88] removed 13 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 13 variables, found 839 hbrs, 2 units
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 515 transitive binary clauses
c [bca-19] limit of 10000000 steps and 24962 added (scaled 2)
c [bca-19] 240 out of 4316 literals actually usable 6%
c [bca-19] added 1 blocked clauses in 173555 steps
c [sweep-19] limit 51197477 penalty 0 = 0 + 0
c [sweep-19-1] 857 pos 39.7% + 1300 neg 60.3% = 2157 sched 100.0% ret 0
c [sweep-19-1] 35266314 steps 196 queries 19.40 avg class size
c [sweep-19-1] 8317 decisions 193 SAT calls 137.65 avg env size
c [sweep-19-1] fully completed sweeping round
c [decomp-89] removed 33 variables
c [sweep-19-1] removed 33 vars (0 failed, 36 eqs, 26 impls)
c [sweep-19-2] 846 pos 39.8% + 1278 neg 60.2% = 2124 sched 100.0% ret 0
c [sweep-19-2] 16769007 steps 67 queries 52.81 avg class size
c [sweep-19-2] 4236 decisions 67 SAT calls 184.15 avg env size
c [sweep-19-2] 435 variables remain 20% (1689 retained 80%)
c [decomp-90] removed 2 variables
c [sweep-19-2] removed 2 vars (0 failed, 2 eqs, 2 impls)
c [sweep-19] removed 35 vars in TOTAL (2 rounds, 261 queries)
c [sort-queue-21] sorted 427 enqueued variables after 2234412 conflicts
c [score-dist-21] active 1695 (80%), one 427 (20%), zero 0 (0%)
c [score-dist-21] max exp 656, different 219 (33%)
c [score-dist-21] median active exp 606, avg 547.6
c [simplification-21] removed 52 variables 2.4% (2122 remain 7%)
c [simplification-21] removed 71 irredundant clauses 0.6% (12076 remain 13%)
c [simplification-21] maximum reduction of 2% = max (2%, 1%)
c [simplification-21] geometric conflict interval increment 173318 = 519954 / 3
c [simplification-21] new conflict interval 693272
c [simplification-21] penalized conflict interval 693272 = 1 * 693272
c [simplification-21] hard conflict limit 3274320 (soft 2927684 + delta 346636)
c [simplification-21] new conflict limit 2927684 (hard 3274320)
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 -  494.6    2122    12076   2237962  126541   6097  4796   11    29   20  39%   1024    2    9   11   78%
c i  494.7    2121    12076   2238504  127067   6097  4796   12    30   26  40%   1024    3   13   11  121%
c -  510.6    2121    12074   2296531  128118   6113  4797   12    31   29  38%  -4562    4   12   11  107%
c -  525.9    2121    12074   2356124  129027   6140  4799   12    31   29  39%  -1226    3   13   11  119%
c -  542.3    2121    12073   2414741  129164   6148  4801   13    29   29  44%    104    1    9   11   82%
c i  545.4    2120    12073   2436964  150247   6164  4807   11    31   39  36%    369    3    8   11   74%
c -  552.5    2119    12072   2476607  134250   6173  4810   11    16   30  68%  -1054   -8   14   11  133%
c -  568.8    2119    12072   2534278  131764   6185  4810   12    26   30  46%    162    1   11   11   92%
c -  581.2    2119    12072   2596351  135012   6190  4810   12    21   31  57%    690   -5   12   11  101%
c i  591.4    2118    12072   2652666  188045   6202  4815   11    24   49  48%    882    1    7   11   62%
c -  593.2    2118    12072   2657000  137205   6202  4815   13    28   31  45%  -2264    5   14   11  129%
c -  610.2    2118    12071   2718953  136647   6223  4818   14    28   30  50%   -273    5   13   11  120%
c i  619.2    2117    12071   2757547  173223   6244  4822   10    19   42  53%    304   -5    6   11   53%
c -  625.6    2113    12071   2782141  139273   6248  4822   11    19   31  58%   -614   -5   11   11  100%
c i  633.5    2112    12071   2825227  180459   6254  4824   12    19   45  61%    175   -3   15   11  133%
c i  633.6    2111    12071   2825286  180512   6255  4824   12    19   45  61%    117   -3   14   11  127%
c i  633.8    2107    12071   2825672  180867   6255  4824   12    20   45  60%   -191   -2   14   11  124%
c -  639.4    2107    12071   2843951  141077   6258  4824   10    26   31  40%   -427    3   11   11   99%
c i  643.2    2106    12071   2864594  159506   6261  4824   11    17   39  64%    -35   -6   14   11  126%
c -  652.4    2106    12070   2906723  142041   6262  4824   10    20   31  50%    143   -2    8   11   75%
c 
c [simplification-22] limit 2927684 conflicts (hard 3274320) hit after 2927685 conflicts
c [quatres-20] found 8020 quaternary clauses 9% in total
c [quatres-20-1] removed 9 duplicate quaternary clauses
c [quatres-20-1] added 1 double-self-subsuming ternary resolvents
c [quatres-20-2] added 64 single-self-subsuming ternary resolvents
c [quatres-20-2] added 86 quaternary resolvents
c [ternres-20] limit 200000000 with penalty 0 = 0 + 0
c [ternres-20] all 2106 free variables schedulable
c [ternres-20] 499 ternary resolvents (28 bin, 471 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-91] removed 28 variables
c [treelook-8] limit 24078940 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 4188 literals 100%
c [treelook-8] scheduling used 504931 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 24078940 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 1942419 steps
c [treelook-8] fully completed tree based probing
c [decomp-92] removed 5 variables
c [treelook-8] removed 7 variables, found 787 hbrs
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 382 transitive binary clauses
c [block-9] scheduling all variables this time
c [block-9] scheduled 2087 variables 100%
c [block-9] limit of 100000000 steps penalty 3 = 3 + 0
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 109 blocked clauses
c [block-9] 109 < 1/100 * 11820 = 118 considered unsuccessful
c [cce-13] boosting limit by 10
c [cce-13] limit of 6019735055 steps penalty 1 = 1 + 0
c [cce-13-1] eliminated 2 clauses out of 76 (3%) of length 8
c [cce-13-1] eliminated 7 clauses out of 157 (4%) of length 7
c [cce-13-1] eliminated 13 clauses out of 272 (5%) of length 6
c [cce-13-1] eliminated 40 clauses out of 831 (5%) of length 5
c [cce-13-1] eliminated 73 clauses out of 2785 (3%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 135 large clauses in 3842109 steps
c [cce-13-1] allowing another 1921054 steps for small clauses
c [cce-13-1] scheduling 5422 clauses = 1698 binary + 3724 ternary
c [cce-13-1] tried to eliminate 5422 small clauses 100%
c [cce-13-1] eliminated 44 binary clauses 3%
c [cce-13-1] eliminated 139 ternary clauses 4%
c [cce-13-1] eliminated 183 small clauses 3%
c [cce-13-1] eliminated 183 small clauses in 5037753 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 318 covered clauses in round 1
c [cce-13-2] eliminated 7 clauses out of 791 (1%) of length 5
c [cce-13-2] eliminated 8 clauses out of 2712 (0%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 15 large clauses in 3628405 steps
c [cce-13-2] allowing another 1814202 steps for small clauses
c [cce-13-2] scheduling 5239 clauses = 1654 binary + 3585 ternary
c [cce-13-2] tried to eliminate 5239 small clauses 100%
c [cce-13-2] eliminated 4 binary clauses 0%
c [cce-13-2] eliminated 6 ternary clauses 0%
c [cce-13-2] eliminated 10 small clauses 0%
c [cce-13-2] eliminated 10 small clauses in 4740614 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 25 covered clauses in round 2
c [cce-13-3] eliminated 1 clauses out of 2704 (0%) of length 4
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] eliminated 1 large clauses in 3606109 steps
c [cce-13-3] allowing another 1803054 steps for small clauses
c [cce-13-3] scheduling 5229 clauses = 1650 binary + 3579 ternary
c [cce-13-3] tried to eliminate 5229 small clauses 100%
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 1 covered clauses in round 3
c [cce-13] eliminated 344 covered clauses in TOTAL during 3 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 2074 variables 100%
c [elim-16] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 87 variables 4% in round 1 in 1743421 steps
c [elim-16-1] backward subsumption/strengthening limit 1743400
c [elim-16-1-1] backward checking 515 touched variables 25%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 1 and strengthened 17 clauses in 120800 steps
c [elim-16-1] rescheduled 40 variables 2% by backward subsumption
c [elim-16-2] no variable eliminated in round 2 in 191898 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 87 = 4% variables out of 2074 scheduled
c [bca-20] limit of 10000000 steps and 23080 added (scaled 2)
c [bca-20] 233 out of 3976 literals actually usable 6%
c [bca-20] added 4 blocked clauses in 147125 steps
c [sweep-20] limit 72236820 penalty 0 = 0 + 0
c [sweep-20-1] 169 pos 42.4% + 230 neg 57.6% = 399 sched 20.1% ret 1588
c [sweep-20-1] 12121579 steps 122 queries 10.78 avg class size
c [sweep-20-1] 3432 decisions 123 SAT calls 85.39 avg env size
c [sweep-20-1] fully completed sweeping round
c [decomp-93] removed 28 variables
c [sweep-20-1] removed 28 vars (0 failed, 29 eqs, 16 impls)
c [sweep-20-2] 737 pos 37.6% + 1222 neg 62.4% = 1959 sched 100.0% ret 0
c [sweep-20-2] 32729756 steps 166 queries 19.75 avg class size
c [sweep-20-2] 7978 decisions 169 SAT calls 111.40 avg env size
c [sweep-20-2] fully completed sweeping round
c [decomp-94] removed 20 variables
c [sweep-20-2] removed 20 vars (0 failed, 24 eqs, 7 impls)
c [sweep-20-3] 727 pos 37.5% + 1212 neg 62.5% = 1939 sched 100.0% ret 0
c [sweep-20-3] 27547232 steps 145 queries 21.94 avg class size
c [sweep-20-3] 6630 decisions 152 SAT calls 120.07 avg env size
c [sweep-20-3] 54 variables remain 3% (1883 retained 97%)
c [decomp-95] removed 20 variables
c [sweep-20-3] removed 20 vars (0 failed, 20 eqs, 6 impls)
c [sweep-20] removed 68 vars in TOTAL (3 rounds, 430 queries)
c [sort-queue-22] sorted 441 enqueued variables after 2927685 conflicts
c [score-dist-22] active 1478 (77%), one 441 (23%), zero 0 (0%)
c [score-dist-22] max exp 899, different 245 (27%)
c [score-dist-22] median active exp 828, avg 740.9
c [simplification-22] removed 187 variables 8.9% (1919 remain 6%)
c [simplification-22] removed 981 irredundant clauses 8.1% (11089 remain 12%)
c [simplification-22] maximum reduction of 9% = max (9%, 8%)
c [simplification-22] large reduction 9% >= 5% limit
c [simplification-22] next conflict interval 29276 = min (2927685/100, 693272)
c [simplification-22] penalized conflict interval 29276 = 1 * 29276
c [simplification-22] hard conflict limit 2971599 (soft 2956961 + delta 14638)
c [simplification-22] new conflict limit 2956961 (hard 2971599)
c 
c [simplification-23] limit 2956961 conflicts (hard 2971599) hit after 2961989 conflicts
c [quatres-21] found 8091 quaternary clauses 9% in total
c [quatres-21-1] removed 46 duplicate quaternary clauses
c [quatres-21-1] added 2 double-self-subsuming ternary resolvents
c [quatres-21-2] added 51 single-self-subsuming ternary resolvents
c [quatres-21-2] added 132 quaternary resolvents
c [ternres-21] limit 200000000 with penalty 0 = 0 + 0
c [ternres-21] all 1919 free variables schedulable
c [ternres-21] 547 ternary resolvents (18 bin, 529 trn)
c [ternres-21] fully completed ternary resolution
c [decomp-96] removed 2 variables
c [basicprobe-8] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 1021 sched 53%, 4 failed, 0 lifted, 116 hbrs
c [decomp-97] removed 7 variables
c [basicprobe-8-1] 1019 sched 53%, 0 failed, 0 lifted, 27 hbrs
c [basicprobe-8-2] 1019 sched 53%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-8-3] 1019 sched 53%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-8-4] 1019 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-8-4] fully completed probing
c [basicprobe-8-4] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-8-4] removed 7 variables, found 149 hbrs
c [bate-7] eliminated 9 asymmetric tautologies during probing
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 229 transitive binary clauses
c [cce-14] limit of 1222182323 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 2 clauses out of 32 (6%) of length 9
c [cce-14-1] eliminated 3 clauses out of 83 (4%) of length 8
c [cce-14-1] eliminated 6 clauses out of 155 (4%) of length 7
c [cce-14-1] eliminated 21 clauses out of 275 (8%) of length 6
c [cce-14-1] eliminated 60 clauses out of 819 (7%) of length 5
c [cce-14-1] eliminated 85 clauses out of 2660 (3%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 177 large clauses in 2323583 steps
c [cce-14-1] allowing another 1161791 steps for small clauses
c [cce-14-1] scheduling 4922 clauses = 1528 binary + 3394 ternary
c [cce-14-1] tried to eliminate 4922 small clauses 100%
c [cce-14-1] eliminated 16 binary clauses 1%
c [cce-14-1] eliminated 23 ternary clauses 1%
c [cce-14-1] eliminated 39 small clauses 1%
c [cce-14-1] eliminated 39 small clauses in 3225364 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 216 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 1115943 steps for small clauses
c [cce-14-2] scheduling 4883 clauses = 1512 binary + 3371 ternary
c [cce-14-2] tried to eliminate 4883 small clauses 100%
c [cce-14-2] completed small round (ATE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 216 covered clauses in TOTAL during 2 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 1910 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 36 variables 2% in round 1 in 1601127 steps
c [elim-17-1] backward subsumption/strengthening limit 1601100
c [elim-17-1-1] backward checking 201 touched variables 11%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 1 clauses in 64446 steps
c [elim-17-1] rescheduled 5 variables 0% by backward subsumption
c [elim-17-2] eliminated 1 variables 0% in round 2 in 2025 steps
c [elim-17-2] backward subsumption/strengthening limit 2000
c [elim-17-2-1] backward checking 0 touched variables 0%
c [elim-17-2-1] incomplete backward checking 0 remain 0%
c [elim-17-2] subsumed 0 and strengthened 0 clauses in 2001 steps
c [elim-17-2] fully rescheduled 1873 variables 98%
c [elim-17-3] eliminated 13 variables 1% in round 3 in 1570493 steps
c [elim-17-3] backward subsumption/strengthening limit 1570400
c [elim-17-3-1] backward checking 40 touched variables 2%
c [elim-17-3-1] fully completed backward checking in 1 rounds
c [elim-17-3] subsumed 0 and strengthened 0 clauses in 9565 steps
c [elim-17] fully completed in 3 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 50 = 3% variables out of 1910 scheduled
c [bca-21] limit of 10000000 steps and 21662 added (scaled 2)
c [bca-21] 210 out of 3722 literals actually usable 6%
c [bca-21] added 1 blocked clauses in 173734 steps
c [sweep-21] limit 73330939 penalty 0 = 0 + 0
c [sweep-21-1] 18 pos 33.3% + 36 neg 66.7% = 54 sched 2.9% ret 1806
c [sweep-21-1] 3582728 steps 30 queries 4.47 avg class size
c [sweep-21-1] 926 decisions 30 SAT calls 93.33 avg env size
c [sweep-21-1] fully completed sweeping round
c [decomp-101] removed 3 variables
c [sweep-21-1] removed 3 vars (0 failed, 4 eqs, 0 impls)
c [sweep-21-2] 716 pos 38.6% + 1141 neg 61.4% = 1857 sched 100.0% ret 0
c [sweep-21-2] 36815135 steps 160 queries 22.81 avg class size
c [sweep-21-2] 7082 decisions 166 SAT calls 115.04 avg env size
c [sweep-21-2] fully completed sweeping round
c [decomp-102] removed 12 variables
c [sweep-21-2] removed 12 vars (0 failed, 14 eqs, 9 impls)
c [sweep-21-3] 715 pos 38.8% + 1130 neg 61.2% = 1845 sched 100.0% ret 0
c [sweep-21-3] 33649382 steps 124 queries 25.19 avg class size
c [sweep-21-3] 6454 decisions 126 SAT calls 147.02 avg env size
c [sweep-21-3] 109 variables remain 6% (1736 retained 94%)
c [decomp-103] removed 12 variables
c [sweep-21-3] removed 12 vars (0 failed, 14 eqs, 8 impls)
c [sweep-21] removed 27 vars in TOTAL (3 rounds, 311 queries)
c [sort-queue-23] sorted 446 enqueued variables after 2961989 conflicts
c [score-dist-23] active 1387 (76%), one 446 (24%), zero 0 (0%)
c [score-dist-23] max exp 933, different 278 (30%)
c [score-dist-23] median active exp 868, avg 730.7
c [simplification-23] removed 86 variables 4.5% (1833 remain 6%)
c [simplification-23] removed 668 irredundant clauses 6.0% (10419 remain 12%)
c [simplification-23] maximum reduction of 6% = max (4%, 6%)
c [simplification-23] large reduction 6% >= 5% limit
c [simplification-23] next conflict interval 29619 = min (2961989/100, 693272)
c [simplification-23] penalized conflict interval 29619 = 1 * 29619
c [simplification-23] hard conflict limit 3006417 (soft 2991608 + delta 14809)
c [simplification-23] new conflict limit 2991608 (hard 3006417)
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  674.7    1832    10418   2971015  183623   5900  3820   10    18   46  57%    694   -5    7   11   68%
c -  676.5    1831    10417   2979410  133066   5904  3820   10    18   29  56%   -752   -5   10   10   96%
c i  680.8    1830    10417   2998340  150827   5908  3828   13    23   37  56%   -307    1   14   11  135%
c 
c [simplification-24] limit 2991608 conflicts (hard 3006417) hit after 3006417 conflicts
c [quatres-22] found 7711 quaternary clauses 9% in total
c [quatres-22-1] removed 39 duplicate quaternary clauses
c [quatres-22-2] added 41 single-self-subsuming ternary resolvents
c [quatres-22-2] added 63 quaternary resolvents
c [ternres-22] limit 200000000 with penalty 0 = 0 + 0
c [ternres-22] all 1830 free variables schedulable
c [ternres-22] 436 ternary resolvents (21 bin, 415 trn)
c [ternres-22] fully completed ternary resolution
c [decomp-104] removed 5 variables
c [simpleprobe-9] all 1828 free variables schedulable
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-105] removed 4 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 4 variables, found 664 hbrs, 1 units
c [unhide-8] limit 1250000 with penalty 4 = 4 + 0
c [unhide-8-8] 0 units, 0 failed, 3705 tauts, 0 hbrs, 74378 literals
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 254 transitive binary clauses
c [cce-15] limit of 1246809042 steps penalty 0 = 0 + 0
c [cce-15-1] eliminated 1 clauses out of 5 (20%) of length 13
c [cce-15-1] eliminated 2 clauses out of 28 (7%) of length 9
c [cce-15-1] eliminated 3 clauses out of 80 (4%) of length 8
c [cce-15-1] eliminated 2 clauses out of 136 (1%) of length 7
c [cce-15-1] eliminated 20 clauses out of 241 (8%) of length 6
c [cce-15-1] eliminated 49 clauses out of 740 (7%) of length 5
c [cce-15-1] eliminated 89 clauses out of 2478 (4%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 166 large clauses in 2774302 steps
c [cce-15-1] allowing another 1387151 steps for small clauses
c [cce-15-1] scheduling 3393 clauses = 1433 binary + 1960 ternary
c [cce-15-1] tried to eliminate 3393 small clauses 100%
c [cce-15-1] eliminated 31 binary clauses 2%
c [cce-15-1] eliminated 77 ternary clauses 4%
c [cce-15-1] eliminated 108 small clauses 3%
c [cce-15-1] eliminated 108 small clauses in 3039775 steps
c [cce-15-1] completed small round (ACCE)
c [cce-15-1] eliminated 274 covered clauses in round 1
c [cce-15-2] eliminated 1 clauses out of 691 (0%) of length 5
c [cce-15-2] eliminated 11 clauses out of 2389 (0%) of length 4
c [cce-15-2] completed large round (ACCE)
c [cce-15-2] eliminated 12 large clauses in 2614958 steps
c [cce-15-2] allowing another 1307479 steps for small clauses
c [cce-15-2] scheduling 3286 clauses = 1402 binary + 1884 ternary
c [cce-15-2] tried to eliminate 3286 small clauses 100%
c [cce-15-2] eliminated 1 binary clauses 0%
c [cce-15-2] eliminated 9 ternary clauses 0%
c [cce-15-2] eliminated 10 small clauses 0%
c [cce-15-2] eliminated 10 small clauses in 2895014 steps
c [cce-15-2] completed small round (ACCE)
c [cce-15-2] eliminated 22 covered clauses in round 2
c [cce-15-3] eliminated 2 clauses out of 2378 (0%) of length 4
c [cce-15-3] completed large round (ACCE)
c [cce-15-3] eliminated 2 large clauses in 2612048 steps
c [cce-15-3] allowing another 1306024 steps for small clauses
c [cce-15-3] scheduling 3276 clauses = 1401 binary + 1875 ternary
c [cce-15-3] tried to eliminate 3276 small clauses 100%
c [cce-15-3] eliminated 1 ternary clauses 0%
c [cce-15-3] eliminated 1 small clauses 0%
c [cce-15-3] eliminated 1 small clauses in 2890733 steps
c [cce-15-3] completed small round (ACCE)
c [cce-15-3] eliminated 3 covered clauses in round 3
c [cce-15] eliminated 299 covered clauses in TOTAL during 3 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 1824 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 16000000000 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 46 variables 3% in round 1 in 1483887 steps
c [elim-18-1] backward subsumption/strengthening limit 1483800
c [elim-18-1-1] backward checking 183 touched variables 10%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 0 and strengthened 0 clauses in 56975 steps
c [elim-18] fully completed in 1 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 46 = 3% variables out of 1824 scheduled
c [bca-22] limit of 10000000 steps and 20653 added (scaled 2)
c [bca-22] 207 out of 3558 literals actually usable 6%
c [bca-22] added 0 blocked clauses in 150004 steps
c [sweep-22] limit 74808542 penalty 0 = 0 + 0
c [sweep-22-1] 48 pos 45.7% + 57 neg 54.3% = 105 sched 5.9% ret 1673
c [sweep-22-1] 4314198 steps 50 queries 7.28 avg class size
c [sweep-22-1] 1149 decisions 52 SAT calls 72.19 avg env size
c [sweep-22-1] fully completed sweeping round
c [decomp-106] removed 4 variables
c [sweep-22-1] removed 4 vars (0 failed, 4 eqs, 2 impls)
c [sweep-22-2] 717 pos 40.4% + 1057 neg 59.6% = 1774 sched 100.0% ret 0
c [sweep-22-2] 33657944 steps 141 queries 19.87 avg class size
c [sweep-22-2] 6975 decisions 140 SAT calls 111.52 avg env size
c [sweep-22-2] fully completed sweeping round
c [decomp-107] removed 3 variables
c [sweep-22-2] removed 3 vars (0 failed, 4 eqs, 3 impls)
c [sweep-22-3] 715 pos 40.4% + 1056 neg 59.6% = 1771 sched 100.0% ret 0
c [sweep-22-3] 29187215 steps 154 queries 18.11 avg class size
c [sweep-22-3] 6124 decisions 159 SAT calls 105.38 avg env size
c [sweep-22-3] fully completed sweeping round
c [decomp-108] removed 10 variables
c [sweep-22-3] removed 10 vars (0 failed, 10 eqs, 3 impls)
c [sweep-22] removed 17 vars in TOTAL (3 rounds, 342 queries)
c [sort-queue-24] sorted 462 enqueued variables after 3006417 conflicts
c [score-dist-24] active 1299 (74%), one 462 (26%), zero 0 (0%)
c [score-dist-24] max exp 927, different 223 (24%)
c [score-dist-24] median active exp 840, avg 758.9
c [simplification-24] removed 69 variables 3.8% (1761 remain 6%)
c [simplification-24] removed 501 irredundant clauses 4.8% (9916 remain 11%)
c [simplification-24] maximum reduction of 5% = max (4%, 5%)
c [simplification-24] large reduction 5% >= 5% limit
c [simplification-24] next conflict interval 30064 = min (3006417/100, 693272)
c [simplification-24] penalized conflict interval 30064 = 1 * 30064
c [simplification-24] hard conflict limit 3051513 (soft 3036481 + delta 15032)
c [simplification-24] new conflict limit 3036481 (hard 3051513)
c 
c [simplification-25] limit 3036481 conflicts (hard 3051513) hit after 3036485 conflicts
c [quatres-23] found 7503 quaternary clauses 9% in total
c [quatres-23-1] removed 30 duplicate quaternary clauses
c [quatres-23-2] added 52 single-self-subsuming ternary resolvents
c [quatres-23-2] added 94 quaternary resolvents
c [ternres-23] limit 200000000 with penalty 0 = 0 + 0
c [ternres-23] all 1761 free variables schedulable
c [ternres-23] 572 ternary resolvents (16 bin, 556 trn)
c [ternres-23] fully completed ternary resolution
c [treelook-9] limit 25314874 penalty 0 = 0 + 0 boost 1
c [treelook-9] scheduled 3522 literals 100%
c [treelook-9] scheduling used 565148 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 25314874 penalty 0 = 0 + 0 boost 1
c [treelook-9] used 1819733 steps
c [treelook-9] fully completed tree based probing
c [treelook-9] removed 1 variables, found 424 hbrs
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 169 transitive binary clauses
c [cce-16] limit of 1265743747 steps penalty 0 = 0 + 0
c [cce-16-1] eliminated 1 clauses out of 134 (1%) of length 7
c [cce-16-1] eliminated 8 clauses out of 726 (1%) of length 5
c [cce-16-1] eliminated 13 clauses out of 2377 (1%) of length 4
c [cce-16-1] completed large round (ATE)
c [cce-16-1] eliminated 22 large clauses in 2069804 steps
c [cce-16-1] allowing another 1034902 steps for small clauses
c [cce-16-1] scheduling 4417 clauses = 1362 binary + 3055 ternary
c [cce-16-1] tried to eliminate 4417 small clauses 100%
c [cce-16-1] eliminated 5 binary clauses 0%
c [cce-16-1] eliminated 39 ternary clauses 1%
c [cce-16-1] eliminated 44 small clauses 1%
c [cce-16-1] eliminated 44 small clauses in 2848812 steps
c [cce-16-1] completed small round (ATE)
c [cce-16-1] eliminated 66 covered clauses in round 1
c [cce-16-2] completed large round (ATE)
c [cce-16-2] allowing another 1026129 steps for small clauses
c [cce-16-2] scheduling 4373 clauses = 1357 binary + 3016 ternary
c [cce-16-2] tried to eliminate 4373 small clauses 100%
c [cce-16-2] completed small round (ATE)
c [cce-16-2] eliminated 0 covered clauses in round 2
c [cce-16] eliminated 66 covered clauses in TOTAL during 2 rounds
c [cce-16] 66 < 1/100 * 9906 = 99 considered unsuccessful
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 1760 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 29 variables 2% in round 1 in 1447530 steps
c [elim-19-1] backward subsumption/strengthening limit 1447500
c [elim-19-1-1] backward checking 106 touched variables 6%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 0 and strengthened 5 clauses in 39044 steps
c [elim-19-1] rescheduled 23 variables 1% by backward subsumption
c [elim-19-2] eliminated 1 variables 0% in round 2 in 92595 steps
c [elim-19-2] backward subsumption/strengthening limit 92500
c [elim-19-2-1] backward checking 0 touched variables 0%
c [elim-19-2-1] fully completed backward checking in 1 rounds
c [elim-19-2] subsumed 0 and strengthened 0 clauses in 4608 steps
c [elim-19] fully completed in 2 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 30 = 2% variables out of 1760 scheduled
c [sweep-23] limit 75944624 penalty 0 = 0 + 0
c [sweep-23-1] 658 pos 38.0% + 1072 neg 62.0% = 1730 sched 100.0% ret 0
c [sweep-23-1] 53909183 steps 164 queries 17.37 avg class size
c [sweep-23-1] 8430 decisions 166 SAT calls 125.24 avg env size
c [sweep-23-1] fully completed sweeping round
c [decomp-111] removed 32 variables
c [sweep-23-1] removed 32 vars (0 failed, 30 eqs, 20 impls)
c [sweep-23-2] 646 pos 38.0% + 1052 neg 62.0% = 1698 sched 100.0% ret 0
c [sweep-23-2] 22429500 steps 29 queries 83.41 avg class size
c [sweep-23-2] 2627 decisions 28 SAT calls 189.71 avg env size
c [sweep-23-2] 854 variables remain 50% (844 retained 50%)
c [decomp-112] removed 2 variables
c [sweep-23-2] removed 2 vars (0 failed, 2 eqs, 1 impls)
c [sweep-23] removed 34 vars in TOTAL (2 rounds, 191 queries)
c [sort-queue-25] sorted 632 enqueued variables after 3036485 conflicts
c [score-dist-25] active 1064 (63%), one 632 (37%), zero 0 (0%)
c [score-dist-25] max exp 667, different 197 (29%)
c [score-dist-25] median active exp 590, avg 502.9
c [simplification-25] removed 65 variables 3.7% (1696 remain 6%)
c [simplification-25] removed 213 irredundant clauses 2.1% (9702 remain 11%)
c [simplification-25] maximum reduction of 4% = max (4%, 2%)
c [simplification-25] geometric conflict interval increment 138654 = 693272 / 5
c [simplification-25] new conflict interval 831926
c [simplification-25] penalized conflict interval 831926 = 1 * 831926
c [simplification-25] hard conflict limit 4284374 (soft 3868411 + delta 415963)
c [simplification-25] new conflict limit 3868411 (hard 4284374)
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 -  703.6    1696     9702   3047716  125963   5541  3117   10    18   28  57%    193   -2   10   11   91%
c i  713.5    1695     9702   3097657  172233   5558  3126   11    17   40  66%    636   -2    9   10   84%
c -  719.4    1695     9702   3117768  129818   5558  3127   10    12   29  86%   -421   -6    8   10   76%
c i  723.4    1694     9702   3143213  145937   5613  3138    7     8   36  89%     44   -7    5   10   52%
c i  725.9    1674     9702   3156387  154468   5643  3142    7     8   36  88%   -369   -6    6    9   60%
c i  726.3    1627     9702   3158295  155829   5671  3150    7     8   38  85%   -500   -6    5    9   51%
c i  726.9    1624     9702   3161296  157866   5702  3160    7     8   38  84%   -488   -6    5    9   54%
c i  727.0    1619     9702   3162114  158331   5720  3163    6     8   38  84%   -497   -6    5    9   56%
c i  727.0    1616     9702   3162319  158412   5738  3171    6     8   38  84%   -498   -6    4    9   49%
c i  727.0    1612     9702   3162320  158412   5738  3171    6     8   38  84%   -498   -6    4    9   49%
c i  727.1    1604     9702   3162718  158633   5750  3175    6     7   38  84%   -500   -6    5    9   50%
c i  727.1    1598     9702   3162791  158655   5759  3179    6     7   38  84%   -500   -6    4    9   46%
c i  727.2    1597     9702   3162913  158719   5772  3185    6     7   38  84%   -500   -6    4    9   44%
c 0  727.2    1578     9702   3162913  158719   5772  3185    6     7   38  84%   -500   -6    4    9   44%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 300 basic ate = 190 trn 63% + 110 lrg 37% in 7 updates
c bcas: 22 count, 614 added (117 skipped), 1926220 steps
c bkwd: tried 75246 clauses, 150307 lits, 2.00 lits/clause
c bkwd: checked 16120059 occs, 214.23 occs/clause, 107.25 occs/lit
c bkwd: subsumed 7 binary, 24 ternary, 35 large
c bkwd: strengthened 0 binary, 2 ternary (100% self), 282 large (0% self)
c blkd: 9 bces, 3115 removed, 1450947 resolutions, 3663752 steps
c blkd: 2249 blocking literals 4%, 219 pure
c bump: 3200355 bumped seen, 202690390 lits 63.3 on average
c card: 6 count, 0 units, 2 am1, 15295735 steps
c card: 17 rescheduled, 145 eliminated, 7359 resolved, 5334 subsumed
c card: 1361 at-most-one constraints found, average size 3.27
c card: 1361 at-most-one constraints used 100%, average size 3.27
c card: 108 at-most-two constraints found, average size 4.03
c card: 108 at-most-two constraints used 100%, average size 4.03
c cces: 16 cces, 8314 eliminated, 6723 ate 81%, 1591 abce 19%
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: 176 gcs, 0 rescored clauses, 1683 rescored vars
c dcps: 112 decompositions, 2815 equivalent 9%
c deco: 2 decision-only clauses 0%, 59% reduction
c decs: 9292507 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 19 elims, 24390 eliminated 79%, 262 pure 1%
c elms: 53 rounds, 2.8 rounds/bve
c elms: 22692 small 93%, 1217 large 5%
c elms: 47693 tried small, 22692 succeeded 48%, 25001 failed 52%
c elms: 2363 subsumed, 3298 strengthened, 392 blocked
c elms: 2871654 copies, 3803089 resolutions, 1635217 ipos
c elms: 1053991 subchks, 715499 strchks
c gaus: 8 extractions, 25951 extracted, 3.0 size, 4 max
c gaus: exported 1 units, 0 binary and 18 ternary equations
c gaus: 0 gc, 17223958 steps, 8611979 extr 50%, 1136577 elim 7%
c glue: 10.1 orig avg, 10.1 real avg, 2.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 45929 = 10382 simple 23% + 31076 trn 68% + 4471 lrg 10%, 939 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3200355 clauses, 28.6 length
c lrnd: 91680142 lits = 133444776 orig - 41764634 removed 31%
c lrnd: 601536 uips 19%, 2341518 flips 73%
c mins: 3179255 mins 99%, 553 bin 0%, 20545 size 1%
c mins: 158024113 poisoned searches, 22676236 hits, 14% hit rate
c mins: 265483545 used twice searches, 12656469 hits, 5% hit rate
c move: moved 5390, 1779 bin 33%, 3611 trn 67%
c otfs: 11294 driving 30%, 26452 restarting 70%
c otfs: str 37746, 37389 red 99%, 357 irr 1%
c otfs: str 37746, 0 bin 0%, 714 trn 2%, 37032 lrg 98%
c otfs: sub 701, 640 red 91%, 61 irr 9%
c otfs: sub 701, 0 bin 0%, 77 trn 11%, 624 lrg 89%
c phas: 1 computed, 8137 set, 2231 pos (27%), 5906 neg (73%)
c prbs: 8 basic, 147497 probed, 104 failed, 4 lifted
c prbs: 9 simple, 126956 probed, 129 failed, 2026 eqs
c prbs: 9 treelook, 14808 probed, 22 failed, 0 lifted
c prom: 1070008 locked 13% out of 7988543 tried
c prps: 483692506 props, 50 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c quat: 23 count, 3635 quat, 1286 self1, 65 self2, 696 dup
c queu: 25 sorted, 9292507 next (3917108 steps 0.42)
c queu: 205740467 enq (210723534 steps 1.02), 202690390 deq 99%
c redc: 87334 clauses 14%, 636885 tried 20%, 10 sat 0%
c redc: 118301 lits 1%, 10320955 tried 8%, 10 sat 0%
c redc: 1108 times jump level reduced, 4.5 levels on average
c reds: 60 count, 52715.2 conflicts per reduce
c reds: 0 memlim 0%, 60 arith 100%
c reds: 2385138 collected 88%, 331175 retired 12%
c rmbd: 1896 removed, 1588 red 84%
c rsts: 85621 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 25 count, 24 confs 96%, 0 vars 0%
c simp: 1 its 4%, 0 bin 0%, 0 trns 0%
c subl: 3200355 count (1528495 tried 0.5), 204862 sub out of 3193391 (6.4%)
c swps: 23 count, 41 rounds, 6791 queries (165.6/round)
c swps: 6584 sat calls, 761 unsat (7.4% success rate)
c swps: 197653 decisions 30.0, 48736 conflicts 7.4
c swps; 57.5 avg class size, 83.2 avg environment size
c swps: 0 failed, 787 impls, 956 equivs
c swp0: 2251 type 0 queries, 613 unsat (27.2%), 2050 sat (91.1%)
c swp1: 4540 type 1 queries, 2137 unsat (47.1%), 3785 sat (83.4%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 24989731 calls to obtain time
c tops: 2037 fixed 7%, 69 its, 45839.32 confs/it
c trds: 23 transitive reductions, 9963 removed, 27 failed
c trds: 173720 nodes, 184024 edges, 19573474 steps
c trim: 1310362 words, 5.0 MB
c trnr: 23 count, 715 bin, 19094 trn, 187296138 steps
c unhd: 8 count, 8 rounds, 7826494 steps
c unhd: 26 non-trivial sccs of average size 2.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 3 failed, 3 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 9621 tauts, 136 bin 1%, 2290 trn 24%, 3873 lrg 40%
c unhd: 9621 tauts, 3322 stamp 35%, 9569 red 99%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 197439 str, 0 bin 0%, 398 trn 0%, 197041 lrg 100%, 195792 red 99%
c vars: 1581 remaining 5% and 29242 removed 95% out of 30823
c vars: 2037 fixed 7%, 24390 eliminated 79%, 2815 equivalent 9%
c vsts: 27458134330 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 57.6 search visits per propagation, 8473.9 per conflict
c wchs: 9717975295 pushed, 9688541 enlarged, 331 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3197026       2385138        331175     123036142      34742314       2023679
c 
c  0 0        257804   8    113438   5         0   0  83995274  68  18362686  53    812195  40     4.2
c  1 5        220898   7    160507   7     30181   9  15929586  13<  4911082  14<   274257  14<    0.9
c  2 6        874758  27    683577  29     82112  25  16406737  13   6930956  20    513417  25     3.3
c  3 9       1199268  38<   952517  40<   107998  33<  5417661   4   3576602  10    342275  17     5.5
c  4 14       541651  17    410753  17     80233  24   1151671   1    873347   3     76768   4     2.6
c  5 21        90057   3     57524   2     25693   8    119870   0     79174   0      4368   0     0.6
c  6 30        11364   0      6193   0      4464   1     13865   0      7684   0       358   0     0.1
c  7 41         1096   0       579   0       441   0      1320   0       713   0        39   0     0.0
c  8 54          101   0        44   0        44   0       121   0        57   0         1   0     0.0
c  9 69           25   0         6   0         7   0        33   0        13   0         1   0     0.0
c 10 86            4   0         0   0         2   0         4   0         0   0         0   0     0.0
c 
c avg                  2.6           2.7           3.0           0.6           1.0           1.3
c std                  1.2           1.1           1.1           1.0           1.2           1.3
c 
c   22.515   3% sweep
c   16.621   2% bump
c   14.927   2% cce
c    8.115   1% probe
c    6.041   1% decide
c    4.328   1% elim
c 
c    7.855 < 1% rest (below)
c 
c    1.431   0% transred
c    1.422   0% quatres
c    1.192   0% ternres
c    1.041   0% unhide
c    0.865   0% bca
c    0.620   0% gauss
c    0.595   0% rescore
c    0.499   0% block
c    0.191   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.862   0% preprocessing     1%
c   58.773   8% inprocessing     99%
c ==================================
c   59.635   8% simplifying
c  667.517  92% search
c ==================================
c  727.152 100% all
c 
c       3162913 conflicts,        4349.7 confs/sec
c          3765 ternaries,         840.1 confs/ternary
c           549 binaries,         5761.2 confs/binary
c            69 iterations,      45839.3 confs/iteration
c 
c            60 reductions,          0.1 redus/sec,  52715.2 confs/reduction
c         85621 restarts,          117.7 rests/sec,     36.9 confs/restart
c       9292507 decisions,       12779.3 decis/sec,      2.9 decis/conflict
c     483692506 propagations,   665187.8 props/sec,     52.1 props/decision
c 
c 727.2 seconds, 55.7 MB
c launch: done
