c launch: /data/cnf/sc2014/app/minxor128.cnf.bz2
c host: atom24
c Lingeling SAT Solver
c 
c Version b7ztzud 55d9a3e9649fc56eacf3e72d8e2e2d5c615d5f18
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Fri May  1 11:44:04 CEST 2015
c compiled Fri May  1 11:44:04 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-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/minxor128.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/minxor128.cnf.bz2
c no embedded options
c found 'p cnf 54258 160469' header
c read 54258 variables, 160469 clauses, 374425 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 --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 54256 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 [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   54256   160467         0       0      0     0    0     0    9   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 18 variables
c [simpleprobe-1] all 54240 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 2 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 2 variables, found 0 hbrs, 1 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 47 tauts, 0 hbrs, 7 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 54238 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 2175 not tried 4% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 50357 = 93% variables out of 54238 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 58763 negative 98.2% of 59813 except 1050 1.8%
c [phase-count-1] 40342 positive 67.4% of 59813 except 19471 32.6%
c [phase-count-1] less non-negative clauses 1050 than limit 5900 (10.0%)
c [phase-count-1] non-pos/non-neg = 19471/1050 = 18.54 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 3881 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 3881 zero 100.00%
c [score-distribution-1] 1 different 0.03% out of total 3881 variables
c [simplification-1] removed 50359 variables 92.8% (3881 remain 7%)
c [simplification-1] removed 100654 irredundant clauses 62.7% (59813 remain 37%)
c [simplification-1] maximum reduction of 93% = max (93%, 63%)
c [simplification-1] large reduction 93% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 6 variables
c [simpleprobe-2] all 3875 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 2 variables
c [simpleprobe-2] 2411 variables remain 62% (1462 retained 38%)
c [simpleprobe-2] removed 2 variables, found 17 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 7746 literals 100%
c [treelook-1] scheduling used 170088 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 316662 steps
c [treelook-1] 7696 literals remain 99%
c [treelook-1] 3873 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 9 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 2229 sched 58%, 2 failed, 0 lifted, 1099 hbrs
c [decomp-6] removed 2 variables
c [basicprobe-1-1] 556 probes remain 14% after last round
c [basicprobe-1-1] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-1-1] removed 2 variables, found 1111 hbrs
c [elim-2] 2165 variables 56% will be scheduled this time
c [elim-2] scheduled 2165 variables 56%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 1279 not tried 33% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 776 = 36% variables out of 2165 scheduled
c [elim-2] considered successful since not run to completion yet
c [score-distribution-2] 1890 pos 61.07%, 0 min 0.00%, 1205 zero 38.93%
c [score-distribution-2] 698 different 22.55% out of total 3095 variables
c [simplification-2] removed 786 variables 20.3% (3095 remain 6%)
c [simplification-2] removed 1283 irredundant clauses 2.1% (58530 remain 36%)
c [simplification-2] maximum reduction of 20% = max (20%, 2%)
c [simplification-2] large reduction 20% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3000 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 149 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 149 out of 149 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-7] removed 6 variables
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 11 tauts, 0 hbrs, 9156 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 3089 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 102 variables 3% in round 1 in 7138253 steps
c [elim-3-1] backward subsumption/strengthening limit 7138200
c [elim-3-1-1] backward checking 962 touched variables 31%
c [elim-3-1-1] incomplete backward checking 920 remain 96%
c [elim-3-1] subsumed 30 and strengthened 343 clauses in 7138210 steps
c [elim-3-1] rescheduled 368 variables 12% by backward subsumption
c [elim-3-2] no variable eliminated in round 2 in 3281952 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 102 = 3% variables out of 3089 scheduled
c [score-distribution-3] 1984 pos 66.42%, 0 min 0.00%, 1003 zero 33.58%
c [score-distribution-3] 748 different 25.04% out of total 2987 variables
c [simplification-3] removed 108 variables 3.5% (2987 remain 6%)
c [simplification-3] removed 462 irredundant clauses 0.8% (58068 remain 36%)
c [simplification-3] maximum reduction of 3% = max (3%, 1%)
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 18000 (soft 8000 + delta 10000)
c [simplification-3] new conflict limit 8000 (hard 18000)
c 
c [simplification-4] limit 8000 conflicts (hard 18000) hit after 8000 conflicts
c [decomp-8] removed 6 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 5618 literals 94%
c [treelook-2] scheduling used 150006 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 238938 steps
c [treelook-2] 5602 literals remain 94%
c [treelook-2] 2978 variables remain to probed next time 100%
c [block-1] scheduling all variables this time
c [block-1] scheduled 2981 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 1573 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 6 (17%) of length 120
c [cce-1-1] eliminated 1 clauses out of 6 (17%) of length 119
c [cce-1-1] eliminated 1 clauses out of 9 (11%) of length 114
c [cce-1-1] eliminated 1 clauses out of 7 (14%) of length 113
c [cce-1-1] eliminated 1 clauses out of 5 (20%) of length 111
c [cce-1-1] eliminated 1 clauses out of 8 (12%) of length 97
c [cce-1-1] eliminated 1 clauses out of 10 (10%) of length 91
c [cce-1-1] eliminated 1 clauses out of 9 (11%) of length 90
c [cce-1-1] eliminated 1 clauses out of 8 (12%) of length 89
c [cce-1-1] eliminated 2 clauses out of 11 (18%) of length 88
c [cce-1-1] eliminated 1 clauses out of 7 (14%) of length 87
c [cce-1-1] eliminated 1 clauses out of 10 (10%) of length 86
c [cce-1-1] eliminated 1 clauses out of 15 (7%) of length 84
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 14 large clauses in 30000758 steps
c [cce-1-1] allowing another 15000379 steps for small clauses
c [cce-1-1] scheduling 21107 clauses = 19674 binary + 1433 ternary
c [cce-1-1] tried to eliminate 175 small clauses 1%
c [cce-1-1] eliminated 3 binary clauses 0%
c [cce-1-1] eliminated 2 ternary clauses 0%
c [cce-1-1] eliminated 5 small clauses 0%
c [cce-1-1] eliminated 5 small clauses in 30000386 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 19 covered clauses in round 1
c [cce-1] eliminated 19 covered clauses in TOTAL during 1 rounds
c [cce-1] 19 < 1/100 * 56483 = 564 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 2981 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 234 variables 8% in round 1 in 8461134 steps
c [elim-4-1] backward subsumption/strengthening limit 8461100
c [elim-4-1-1] backward checking 1548 touched variables 52%
c [elim-4-1-1] incomplete backward checking 1387 remain 90%
c [elim-4-1] subsumed 85 and strengthened 537 clauses in 8461203 steps
c [elim-4-1] rescheduled 483 variables 16% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 4336388 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 234 = 8% variables out of 2981 scheduled
c [bca-1] limit of 10000000 steps and 112576 added (scaled 2)
c [bca-1] 3469 out of 5496 literals actually usable 63%
c [bca-1] added 30 blocked clauses in 23010 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 695 pos 25.3% + 2052 neg 74.7% = 2747 sched 100.0% ret 0
c [sweep-1-1] 934039 steps 414 queries 66.19 avg class size
c [sweep-1-1] 21835 decisions 413 SAT calls 89.45 avg env size
c [sweep-1-1] fully completed sweeping round
c [decomp-9] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 2 eqs, 1 impls)
c [sweep-1-2] 695 pos 25.3% + 2051 neg 74.7% = 2746 sched 100.0% ret 0
c [sweep-1-2] 77428 steps 19 queries 388.42 avg class size
c [sweep-1-2] 937 decisions 18 SAT calls 128.50 avg env size
c [sweep-1-2] 2594 variables remain 94% (152 retained 6%)
c [sweep-1-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] 1 < 1/1000 * 2747 = 2 considered unsuccessful
c [sweep-1] removed 1 vars in TOTAL (2 rounds, 431 queries)
c [score-distribution-4] 1977 pos 72.00%, 345 min 12.56%, 424 zero 15.44%
c [score-distribution-4] 909 different 33.10% out of total 2746 variables
c [simplification-4] removed 241 variables 8.1% (2746 remain 5%)
c [simplification-4] removed 2035 irredundant clauses 3.5% (56033 remain 35%)
c [simplification-4] maximum reduction of 8% = max (8%, 4%)
c [simplification-4] large reduction 8% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 20000 (soft 10000 + delta 10000)
c [simplification-4] new conflict limit 10000 (hard 20000)
c 
c [simplification-5] limit 10000 conflicts (hard 20000) hit after 10000 conflicts
c [quatres-1] found 2274 quaternary clauses 7% in total
c [quatres-1-2] added 8 single-self-subsuming ternary resolvents
c [quatres-1-2] added 25 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 2746 free variables schedulable
c [ternres-1] 135 ternary resolvents (6 bin, 129 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 989 xors of average arity 3.0
c [gauss-1] connected 2964 occurrences of 352 variables (average 8.4)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-2] limit 2091450 penalty 0 = 0 + 0
c [basicprobe-2-0] 505 sched 18%, 1 failed, 0 lifted, 5 hbrs
c [decomp-12] removed 2 variables
c [basicprobe-2-1] 1539 sched 56%, 0 failed, 0 lifted, 148 hbrs
c [decomp-13] removed 1 variables
c [basicprobe-2-2] 1537 sched 56%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-2-3] 1537 sched 56%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-3] fully completed probing
c [basicprobe-2-3] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-2-3] removed 3 variables, found 157 hbrs
c [bate-1] eliminated 256 asymmetric tautologies during probing
c [transred-1] limit 418290 with penalty 0 = 0 + 0
c [transred-1] removed 27 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 2743 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 224 blocked clauses
c [block-2] 224 < 1/100 * 55737 = 557 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 2743 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 58 variables 2% in round 1 in 13569756 steps
c [elim-5-1] backward subsumption/strengthening limit 6430244
c [elim-5-1-1] backward checking 752 touched variables 27%
c [elim-5-1-1] incomplete backward checking 772 remain 103%
c [elim-5-1] subsumed 1 and strengthened 502 clauses in 6430347 steps
c [elim-5] incomplete 440 not tried 16% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 58 = 2% variables out of 2743 scheduled
c [bca-2] limit of 10000000 steps and 111303 added (scaled 2)
c [bca-2] 2981 out of 5372 literals actually usable 55%
c [bca-2] added 40 blocked clauses in 19927 steps
c [score-distribution-5] 1958 pos 72.92%, 364 min 13.56%, 363 zero 13.52%
c [score-distribution-5] 775 different 28.86% out of total 2685 variables
c [simplification-5] removed 61 variables 2.2% (2685 remain 5%)
c [simplification-5] removed 639 irredundant clauses 1.1% (55394 remain 35%)
c [simplification-5] maximum reduction of 2% = max (2%, 1%)
c [simplification-5] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-5] new conflict interval 11666
c [simplification-5] penalized conflict interval 11666 = 1 * 11666
c [simplification-5] hard conflict limit 31666 (soft 21666 + delta 10000)
c [simplification-5] new conflict limit 21666 (hard 31666)
c 
c [simplification-6] limit 21666 conflicts (hard 31666) hit after 21666 conflicts
c [quatres-2] found 2776 quaternary clauses 8% in total
c [quatres-2-1] added 1 double-self-subsuming ternary resolvents
c [quatres-2-2] added 6 single-self-subsuming ternary resolvents
c [quatres-2-2] added 20 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 2685 free variables schedulable
c [ternres-2] 65 ternary resolvents (1 bin, 64 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 75 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 75 out of 75 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [simpleprobe-3] 1645 schedulable variables 61%
c [simpleprobe-3] limit 3384112 penalty 0 = 0 + 0
c [simpleprobe-3] 1381 variables remain 51% (1304 retained 49%)
c [simpleprobe-3] removed 0 variables, found 34 hbrs, 0 units
c [unhide-3] limit 42301 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 238 tauts, 0 hbrs, 4998 literals
c [transred-2] limit 846028 with penalty 0 = 0 + 0
c [transred-2] removed 7 transitive binary clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 7500559 steps for small clauses
c [cce-2-1] scheduling 20190 clauses = 19046 binary + 1144 ternary
c [cce-2-1] tried to eliminate 164 small clauses 1%
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 0 covered clauses in round 1
c [cce-2] eliminated 0 covered clauses in TOTAL during 1 rounds
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 2685 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 29 variables 1% in round 1 in 13849265 steps
c [elim-6-1] backward subsumption/strengthening limit 6150735
c [elim-6-1-1] backward checking 573 touched variables 21%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 6 clauses in 4948383 steps
c [elim-6-1] rescheduled 191 variables 7% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 386063 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 29 = 1% variables out of 2685 scheduled
c [bca-3] limit of 10000000 steps and 110899 added (scaled 2)
c [bca-3] 2052 out of 5314 literals actually usable 39%
c [bca-3] added 40 blocked clauses in 26140 steps
c [sweep-2] limit 500000 penalty 1 = 1 + 0
c [sweep-2-1] 577 pos 23.0% + 1933 neg 77.0% = 2510 sched 94.5% ret 146
c [sweep-2-1] 501568 steps 104 queries 136.97 avg class size
c [sweep-2-1] 6966 decisions 103 SAT calls 126.83 avg env size
c [sweep-2-1] 1106 variables remain 42% (1550 retained 58%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 103 queries)
c [score-distribution-6] 2196 pos 82.68%, 263 min 9.90%, 197 zero 7.42%
c [score-distribution-6] 964 different 36.30% out of total 2656 variables
c [simplification-6] removed 29 variables 1.1% (2656 remain 5%)
c [simplification-6] removed 212 irredundant clauses 0.4% (55182 remain 34%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 21666
c [simplification-6] penalized conflict interval 21666 = 1 * 21666
c [simplification-6] hard conflict limit 54165 (soft 43332 + delta 10833)
c [simplification-6] new conflict limit 43332 (hard 54165)
c 
c [simplification-7] limit 43332 conflicts (hard 54165) hit after 43332 conflicts
c [quatres-3] found 3250 quaternary clauses 9% in total
c [quatres-3-2] added 7 single-self-subsuming ternary resolvents
c [quatres-3-2] added 13 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 2656 free variables schedulable
c [ternres-3] 164 ternary resolvents (7 bin, 157 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 804 xors of average arity 3.0
c [gauss-2] connected 2412 occurrences of 345 variables (average 7.0)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [transred-3] limit 1605060 with penalty 0 = 0 + 0
c [transred-3] removed 20 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 2656 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 8 blocked clauses
c [block-3] 8 < 1/100 * 55179 = 551 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 2656 variables 100%
c [elim-7] limit of 32101210 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] no variable eliminated in round 1 in 15062759 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 0 = 0% variables out of 2656 scheduled
c [bca-4] limit of 10000000 steps and 110897 added (scaled 2)
c [bca-4] 715 out of 5314 literals actually usable 13%
c [bca-4] added 0 blocked clauses in 35394 steps
c [score-distribution-7] 2562 pos 96.46%, 81 min 3.05%, 13 zero 0.49%
c [score-distribution-7] 1400 different 52.71% out of total 2656 variables
c [simplification-7] removed 0 variables 0.0% (2656 remain 5%)
c [simplification-7] removed 11 irredundant clauses 0.0% (55171 remain 34%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 21666
c [simplification-7] new conflict interval 43332
c [simplification-7] penalized conflict interval 43332 = 1 * 43332
c [simplification-7] hard conflict limit 108330 (soft 86664 + delta 21666)
c [simplification-7] new conflict limit 86664 (hard 108330)
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   17.7    2655    55171     53468   41712   2220   708   30   106   23  29%    564   64   21   13  158%
c -   19.6    2655    55171     68241   18579   2278   714   40   104   18  38%    -21   51   33   18  183%
c 
c [simplification-8] limit 86664 conflicts (hard 108330) hit after 86664 conflicts
c [quatres-4] found 3530 quaternary clauses 9% in total
c [quatres-4-2] added 10 single-self-subsuming ternary resolvents
c [quatres-4-2] added 19 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 2655 free variables schedulable
c [ternres-4] 77 ternary resolvents (1 bin, 76 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-19] removed 1 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 32 transitive binary clauses
c [score-distribution-8] 2355 pos 88.70%, 300 min 11.30%, 0 zero 0.00%
c [score-distribution-8] 1356 different 51.07% out of total 2655 variables
c [simplification-8] removed 0 variables 0.0% (2655 remain 5%)
c [simplification-8] removed 8 irredundant clauses 0.0% (55163 remain 34%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 43332
c [simplification-8] new conflict interval 86664
c [simplification-8] penalized conflict interval 86664 = 1 * 86664
c [simplification-8] hard conflict limit 216660 (soft 173328 + delta 43332)
c [simplification-8] new conflict limit 173328 (hard 216660)
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.3    2655    55163    112293   23037   2458   697   43   110   14  39%    491   24   30   31   96%
c i   28.9    2654    55163    146206   51719   2549   711   42    99   29  42%    706    1   14   37   37%
c -   29.7    2651    55163    153495   25836   2554   713   45   120   19  38%   -576   19   53   38  138%
c i   30.2    2650    55163    158096   29822   2558   717   44   112   22  39%   -469   11   34   39   87%
c 
c [simplification-9] limit 173328 conflicts (hard 216660) hit after 190607 conflicts
c [quatres-5] found 2890 quaternary clauses 9% in total
c [quatres-5-2] added 29 single-self-subsuming ternary resolvents
c [quatres-5-2] added 21 quaternary resolvents
c [ternres-5] limit 5339578 with penalty 0 = 0 + 0
c [ternres-5] all 2649 free variables schedulable
c [ternres-5] 170 ternary resolvents (2 bin, 168 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-20] removed 6 variables
c [treelook-3] limit 133489 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 2963 literals 56%
c [treelook-3] scheduling used 136136 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 133489 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 147435 steps
c [treelook-3] 2940 literals remain 55%
c [treelook-3] 2180 variables remain to probed next time 82%
c [treelook-3] removed 0 variables, found 3 hbrs
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 14 transitive binary clauses
c [cce-3] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 2 clauses out of 6 (33%) of length 172
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 118
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 109
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 108
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 107
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 103
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 9 large clauses in 7500260 steps
c [cce-3-1] allowing another 3750130 steps for small clauses
c [cce-3-1] scheduling 20557 clauses = 18991 binary + 1566 ternary
c [cce-3-1] tried to eliminate 57 small clauses 0%
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 9 covered clauses in round 1
c [cce-3] eliminated 9 covered clauses in TOTAL during 1 rounds
c [cce-3] 9 < 1/100 * 54884 = 548 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 2649 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1067915690 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 2 variables 0% in round 1 in 16040316 steps
c [elim-8-1] backward subsumption/strengthening limit 16040300
c [elim-8-1-1] backward checking 313 touched variables 12%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 2414147 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 2 = 0% variables out of 2649 scheduled
c [elim-8] 2 < 1/100 * 2649 = 26 considered unsuccessful
c [bca-5] limit of 10000000 steps and 110289 added (scaled 2)
c [bca-5] 293 out of 5296 literals actually usable 6%
c [bca-5] added 0 blocked clauses in 55026 steps
c [sweep-3] limit 400468 penalty 2 = 2 + 0
c [sweep-3-1] 349 pos 31.6% + 755 neg 68.4% = 1104 sched 41.7% ret 1543
c [sweep-3-1] 485567 steps 76 queries 112.05 avg class size
c [sweep-3-1] 6898 decisions 74 SAT calls 359.03 avg env size
c [sweep-3-1] 625 variables remain 24% (2022 retained 76%)
c [decomp-22] removed 1 variables
c [sweep-3-1] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-3] 1 < 1/1000 * 2647 = 2 considered unsuccessful
c [sweep-3] removed 1 vars in TOTAL (1 rounds, 75 queries)
c [score-distribution-9] 2451 pos 92.63%, 195 min 7.37%, 0 zero 0.00%
c [score-distribution-9] 1003 different 37.91% out of total 2646 variables
c [simplification-9] removed 3 variables 0.1% (2646 remain 5%)
c [simplification-9] removed 300 irredundant clauses 0.5% (54863 remain 34%)
c [simplification-9] maximum reduction of 1% = max (0%, 1%)
c [simplification-9] geometric conflict interval increment 43332 = 86664 / 2
c [simplification-9] new conflict interval 129996
c [simplification-9] penalized conflict interval 129996 = 1 * 129996
c [simplification-9] hard conflict limit 385601 (soft 320603 + delta 64998)
c [simplification-9] new conflict limit 320603 (hard 385601)
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 -   36.2    2646    54863    195493   23992   2581   731   72   141   15  51%     74   27  138   47  294%
c i   37.4    2645    54863    206308   32435   2670   736   86   140   25  62%    218   20   34   53   65%
c i   39.6    2640    54863    224997   48101   2747   736   72   137   44  53%   -157   13   31   55   57%
c -   41.1    2639    54863    238993   27160   2748   736   58   128   15  46%   -170    1   95   55  174%
c -   46.0    2639    54863    280675   28117   2963   749   82   153   16  54%    392   19   34   61   55%
c i   48.3    2638    54863    304094   48296   2986   757   54   126   31  43%    582   -3   30   57   51%
c -   50.0    2637    54863    321078   30178   2986   757   57   116   16  49%   -286   -8   68   55  123%
c 
c [simplification-10] limit 320603 conflicts (hard 385601) hit after 337221 conflicts
c [quatres-6] found 1857 quaternary clauses 8% in total
c [quatres-6-2] added 7 single-self-subsuming ternary resolvents
c [quatres-6-2] added 23 quaternary resolvents
c [ternres-6] limit 8376919 with penalty 0 = 0 + 0
c [ternres-6] all 2637 free variables schedulable
c [ternres-6] 26 ternary resolvents (2 bin, 24 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 523557 penalty 3 = 3 + 0
c [card-4] found 70 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 523557 for elimination
c [card-4] 70 out of 70 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 476 xors of average arity 3.0
c [gauss-3] connected 1428 occurrences of 201 variables (average 7.1)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 41884595 penalty 0 = 0 + 0
c [basicprobe-3-0] 1513 sched 57%, 4 failed, 0 lifted, 263 hbrs
c [decomp-24] removed 5 variables
c [basicprobe-3-1] 1514 sched 58%, 0 failed, 0 lifted, 138 hbrs
c [basicprobe-3-2] 1515 sched 58%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-2] fully completed probing
c [basicprobe-3-2] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-3-2] removed 5 variables, found 401 hbrs
c [unhide-4] limit 209422 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 0 failed, 230 tauts, 0 hbrs, 20195 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 11 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 2632 variables 100%
c [block-4] limit of 20942297 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 16 blocked clauses
c [block-4] 16 < 1/100 * 54058 = 540 considered unsuccessful
c [score-distribution-10] 2447 pos 92.97%, 185 min 7.03%, 0 zero 0.00%
c [score-distribution-10] 1414 different 53.72% out of total 2632 variables
c [simplification-10] removed 5 variables 0.2% (2632 remain 5%)
c [simplification-10] removed 821 irredundant clauses 1.5% (54042 remain 34%)
c [simplification-10] maximum reduction of 1% = max (0%, 1%)
c [simplification-10] geometric conflict interval increment 64998 = 129996 / 2
c [simplification-10] new conflict interval 194994
c [simplification-10] penalized conflict interval 194994 = 1 * 194994
c [simplification-10] hard conflict limit 629712 (soft 532215 + delta 97497)
c [simplification-10] new conflict limit 532215 (hard 629712)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   56.5    2632    54042    365281   26872   1913  1064   44    78   17  56%    357  -46   95   55  172%
c -   61.8    2632    54042    408841   28144   1987  1066   53   102   17  51%    681  -16   70   55  127%
c -   67.5    2632    54042    452408   27982   2105  1071  111   196   21  56%    847   62  120   66  182%
c i   73.0    2631    54042    495851   62708   2265  1082   91   139   43  66%    933    1   44   72   62%
c -   73.5    2629    54042    500261   30056   2265  1082   79   149   18  53%  -1866   11  113   71  158%
c i   76.9    2628    54042    527794   52659   2304  1086   61    98   40  62%   -901  -44   40   73   55%
c -   79.5    2626    54042    546083   30913   2322  1092   56    97   17  58%   -816  -44   26   73   35%
c 
c [simplification-11] limit 532215 conflicts (hard 629712) hit after 584496 conflicts
c [quatres-7] found 2264 quaternary clauses 10% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-2] added 22 single-self-subsuming ternary resolvents
c [quatres-7-2] added 46 quaternary resolvents
c [ternres-7] limit 13393303 with penalty 0 = 0 + 0
c [ternres-7] all 2626 free variables schedulable
c [ternres-7] 181 ternary resolvents (3 bin, 178 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-26] removed 7 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 16 transitive binary clauses
c [score-distribution-11] 2211 pos 84.23%, 414 min 15.77%, 0 zero 0.00%
c [score-distribution-11] 1149 different 43.77% out of total 2625 variables
c [simplification-11] removed 1 variables 0.0% (2625 remain 5%)
c [simplification-11] removed 642 irredundant clauses 1.2% (53400 remain 33%)
c [simplification-11] maximum reduction of 1% = max (0%, 1%)
c [simplification-11] geometric conflict interval increment 97497 = 194994 / 2
c [simplification-11] new conflict interval 292491
c [simplification-11] penalized conflict interval 292491 = 1 * 292491
c [simplification-11] hard conflict limit 1023232 (soft 876987 + delta 146245)
c [simplification-11] new conflict limit 876987 (hard 1023232)
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 -   85.9    2625    53400    594577   29273   1966  1049   51   126   15  41%    146  -23   36   77   47%
c -   91.9    2625    53400    642629   31350   2043  1053   97   200   18  48%    602   57  129   75  173%
c i   95.2    2624    53400    672053   54172   2095  1058   62   112   37  55%    755  -26   36   71   51%
c i   95.2    2623    53400    672054   54172   2095  1058   62   112   37  55%    753  -26   36   71   51%
c -   97.4    2622    53400    690687   31670   2116  1059   66   126   16  52%   -902  -17   60   73   81%
c i  101.4    2621    53400    727600   62208   2175  1066   75   116   40  64%    -72  -22   30   74   41%
c -  103.1    2616    53400    739513   32967   2222  1072   98   169   17  58%   -625   32   98   76  129%
c -  108.8    2616    53400    789509   33622   2319  1075   65   132   17  49%    255   -0   78   73  107%
c i  112.3    2615    53400    816405   55350   2425  1093   61    99   39  62%    514  -38   29   74   39%
c -  115.7    2613    53400    841556   34275   2529  1096   82   141   18  58%   -284    5  123   74  165%
c i  116.0    2612    53400    844004   36099   2564  1098   73   122   22  59%   -236  -14   24   74   32%
c i  121.3    2606    53400    884879   69319   2620  1106   70    99   55  71%    114  -40   33   77   43%
c -  123.0    2606    53400    893969   35333   2632  1106  121   203   17  60%   -333   61  163   83  195%
c 
c [simplification-12] limit 876997 conflicts (hard 1023232) hit after 912421 conflicts
c [quatres-8] found 2735 quaternary clauses 9% in total
c [quatres-8-2] added 66 single-self-subsuming ternary resolvents
c [quatres-8-2] added 55 quaternary resolvents
c [ternres-8] limit 19903156 with penalty 0 = 0 + 0
c [ternres-8] all 2606 free variables schedulable
c [ternres-8] 775 ternary resolvents (29 bin, 746 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-27] removed 23 variables
c [simpleprobe-4] 1329 schedulable variables 51%
c [simpleprobe-4] limit 39806312 penalty 1 = 1 + 0
c [simpleprobe-4] 107 variables remain 4% (2495 retained 96%)
c [simpleprobe-4] removed 0 variables, found 260 hbrs, 0 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 89 transitive binary clauses
c [transred-8] found 1 units
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 2600 variables 100%
c [elim-9] limit of 99515781 steps penalty 2 = 2 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 50 variables 2% in round 1 in 16906057 steps
c [elim-9-1] backward subsumption/strengthening limit 16906000
c [elim-9-1-1] backward checking 440 touched variables 17%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 1254277 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 50 = 2% variables out of 2600 scheduled
c [bca-6] limit of 10000000 steps and 104217 added (scaled 2)
c [bca-6] 519 out of 5102 literals actually usable 10%
c [bca-6] added 2 blocked clauses in 42853 steps
c [score-distribution-12] 1686 pos 66.12%, 864 min 33.88%, 0 zero 0.00%
c [score-distribution-12] 1001 different 39.25% out of total 2550 variables
c [simplification-12] removed 56 variables 2.1% (2550 remain 5%)
c [simplification-12] removed 1569 irredundant clauses 2.9% (51831 remain 32%)
c [simplification-12] maximum reduction of 3% = max (2%, 3%)
c [simplification-12] geometric conflict interval increment 73122 = 292491 / 4
c [simplification-12] new conflict interval 365613
c [simplification-12] penalized conflict interval 365613 = 1 * 365613
c [simplification-12] hard conflict limit 1460840 (soft 1278034 + delta 182806)
c [simplification-12] new conflict limit 1278034 (hard 1460840)
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 -  132.2    2550    51831    953841   33826   2607  1228   72   132   19  55%    480   -2   87   75  115%
c i  136.5    2549    51831    986036   60186   2629  1235   82   136   47  60%    691   -8   44   80   55%
c i  138.3    2548    51831    998414   69647   2647  1238   91   153   50  59%   -581   11   69   80   86%
c i  139.3    2547    51831   1003803   73909   2656  1245  105   179   59  59%   -634   34   56   83   67%
c -  139.7    2547    51831   1006026   33358   2656  1245  119   201   18  60%   -653   54  155   85  182%
c i  140.8    2546    51831   1013458   39379   2659  1245  118   193   27  61%   -482   42  145   88  165%
c i  143.4    2543    51831   1032515   53861   2703  1249  100   175   40  57%   -216   18  103   90  114%
c i  144.4    2542    51831   1040235   59486   2706  1256   85   131   46  64%   -347  -24  111   89  124%
c i  145.2    2541    51831   1044597   63042   2710  1259  115   191   49  60%   -372   35  143   92  156%
c i  145.7    2540    51831   1049024   66115   2721  1263   87   134   56  65%   -346  -23   27   91   30%
c -  147.9    2534    51831   1064488   34806   2741  1264   81   129   20  63%   -114  -22   65   89   73%
c i  148.7    2533    51831   1072314   41155   2792  1270   62   136   28  46%     14  -14   27   87   31%
c i  154.3    2530    51831   1109624   69125   2846  1280  119   181   59  66%    243   26   49   93   52%
c 
c [simplification-13] limit of 24 iterations hit after 24 iterations
c [quatres-9] found 2166 quaternary clauses 9% in total
c [quatres-9-2] added 35 single-self-subsuming ternary resolvents
c [quatres-9-2] added 35 quaternary resolvents
c [ternres-9] limit 24163099 with penalty 0 = 0 + 0
c [ternres-9] all 2527 free variables schedulable
c [ternres-9] 198 ternary resolvents (2 bin, 196 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-29] removed 27 variables
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 76 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 151019368 steps penalty 3 = 3 + 0
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] allowing another 75510629 steps for small clauses
c [cce-4-1] scheduling 20004 clauses = 18469 binary + 1535 ternary
c [cce-4-1] tried to eliminate 1460 small clauses 7%
c [cce-4-1] eliminated 61 ternary clauses 4%
c [cce-4-1] eliminated 61 small clauses 0%
c [cce-4-1] eliminated 61 small clauses in 151021500 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 61 covered clauses in round 1
c [cce-4] eliminated 61 covered clauses in TOTAL during 1 rounds
c [cce-4] 61 < 1/100 * 50319 = 503 considered unsuccessful
c [sweep-4] limit 906116 penalty 3 = 3 + 0
c [sweep-4-1] 200 pos 32.7% + 411 neg 67.3% = 611 sched 24.2% ret 1912
c [sweep-4-1] 909075 steps 130 queries 48.44 avg class size
c [sweep-4-1] 10925 decisions 131 SAT calls 390.31 avg env size
c [sweep-4-1] 89 variables remain 4% (2432 retained 96%)
c [decomp-30] removed 2 variables
c [sweep-4-1] removed 2 vars (0 failed, 1 eqs, 0 impls)
c [sweep-4] removed 2 vars in TOTAL (1 rounds, 129 queries)
c [score-distribution-13] 1729 pos 68.58%, 792 min 31.42%, 0 zero 0.00%
c [score-distribution-13] 765 different 30.35% out of total 2521 variables
c [simplification-13] removed 6 variables 0.2% (2521 remain 5%)
c [simplification-13] removed 1586 irredundant clauses 3.1% (50245 remain 31%)
c [simplification-13] maximum reduction of 3% = max (0%, 3%)
c [simplification-13] forced so keeping old conflict interval 365613
c [simplification-13] conflict limit remains at 1278034 (hard 1460840)
c [simplification-13] 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 -  159.5    2521    50245   1134211   34122   2429   941   70   112   20  62%     80  -42   85   87   98%
c i  163.3    2520    50245   1161337   54917   2432   944   68   105   42  64%    400  -45   31   87   36%
c i  164.4    2518    50245   1168276   60250   2432   945  104   168   52  61%   -275   22  114   88  130%
c i  164.4    2515    50245   1168427   60326   2439   946  100   164   52  61%   -287   17   71   87   81%
c i  166.4    2511    50245   1182649   70674   2470   952   63    95   56  66%   -110  -51   28   85   34%
c i  166.5    2510    50245   1183151   71055   2485   957   57    90   56  63%   -187  -56   12   84   14%
c i  168.2    2506    50245   1192186   77875   2581   968  139   211   68  66%   -158   67  172   90  191%
c -  168.4    2506    50245   1192734   34790   2581   968  143   218   22  66%   -207   72  195   91  215%
c i  169.5    2505    50245   1199585   39970   2707   980   79   118   32  66%   -160  -30   32   89   36%
c i  171.5    2504    50245   1215148   51477   2820   989   48    72   43  67%     -3  -70   29   83   35%
c i  174.2    2502    50245   1229919   63023   2829   994  154   250   55  61%      7  102  113   94  120%
c -  178.4    2501    50245   1253485   35865   2872   996  117   184   21  64%    151   22   96  101   95%
c 
c [simplification-14] limit 1278034 conflicts (hard 1460840) hit after 1279267 conflicts
c [quatres-10] found 1681 quaternary clauses 8% in total
c [quatres-10-2] added 11 single-self-subsuming ternary resolvents
c [quatres-10-2] added 12 quaternary resolvents
c [ternres-10] limit 28021230 with penalty 0 = 0 + 0
c [ternres-10] all 2501 free variables schedulable
c [ternres-10] 863 ternary resolvents (17 bin, 846 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 700530 penalty 3 = 3 + 0
c [gauss-4] extracted 575 xors of average arity 3.0
c [gauss-4] connected 1719 occurrences of 307 variables (average 5.6)
c [gauss-4] limit 700530 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-31] removed 4 variables
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 33 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 2497 variables 100%
c [block-5] limit of 35026537 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 58 blocked clauses
c [block-5] 58 < 1/100 * 48842 = 488 considered unsuccessful
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 2494 variables 100%
c [elim-10] limit of 280212302 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 46 variables 2% in round 1 in 18682836 steps
c [elim-10-1] backward subsumption/strengthening limit 18682800
c [elim-10-1-1] backward checking 342 touched variables 14%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 119 and strengthened 1 clauses in 839135 steps
c [elim-10-1] rescheduled 124 variables 5% by backward subsumption
c [elim-10-2] eliminated 1 variables 0% in round 2 in 2358950 steps
c [elim-10-2] backward subsumption/strengthening limit 2358900
c [elim-10-2-1] backward checking 10 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 0 clauses in 196413 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 47 = 2% variables out of 2494 scheduled
c [bca-7] limit of 10000000 steps and 97704 added (scaled 2)
c [bca-7] 453 out of 4896 literals actually usable 9%
c [bca-7] added 5 blocked clauses in 43480 steps
c [score-distribution-14] 1999 pos 81.69%, 448 min 18.31%, 0 zero 0.00%
c [score-distribution-14] 992 different 40.54% out of total 2447 variables
c [simplification-14] removed 54 variables 2.2% (2447 remain 5%)
c [simplification-14] removed 1671 irredundant clauses 3.3% (48574 remain 30%)
c [simplification-14] maximum reduction of 3% = max (2%, 3%)
c [simplification-14] geometric conflict interval increment 91403 = 365613 / 4
c [simplification-14] new conflict interval 457016
c [simplification-14] penalized conflict interval 457016 = 1 * 457016
c [simplification-14] hard conflict limit 1964791 (soft 1736283 + delta 228508)
c [simplification-14] new conflict limit 1736283 (hard 1964791)
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  185.7    2446    48574   1292842   52224   2250   711  108   157   48  69%    545  -11  127  104  122%
c i  186.0    2445    48574   1293871   53048   2251   712  123   186   45  66%    -65   18  151  105  143%
c i  186.3    2444    48574   1295704   54524   2253   712  129   196   45  66%   -343   28  135  106  128%
c i  187.2    2440    48574   1302092   59241   2256   717  125   194   51  64%   -300   26  153  107  143%
c i  187.2    2439    48574   1302094   59241   2256   718  125   194   51  64%   -300   26  152  107  142%
c -  191.7    2439    48574   1328832   33468   2290   726  149   221   21  68%     76   53  158  109  145%
c i  191.7    2438    48574   1328915   33521   2290   726  147   218   27  68%     77   51  130  109  120%
c i  191.7    2437    48574   1328970   33543   2293   728  146   216   28  68%     56   49  115  109  106%
c -  201.7    2436    48574   1393622   36139   2355   738   81   119   25  68%    512  -41  118  102  116%
c i  205.0    2435    48574   1421082   55656   2372   740   84   138   40  61%    688   -4   51   92   55%
c -  211.6    2435    48574   1457323   36398   2382   743  141   192   21  73%    -11   27  192  112  171%
c i  219.6    2434    48574   1507986   72682   2489   749   61    82   65  75%    546  -76   45  104   43%
c i  219.8    2433    48574   1509244   73502   2510   751   82   112   76  73%   -394  -45   62  105   59%
c i  220.9    2432    48574   1514295   77414   2515   753  150   216   77  70%   -678   58  199  110  181%
c i  221.0    2395    48574   1514491   77546   2516   755  149   212   77  70%   -687   55  153  110  139%
c -  223.2    2395    48574   1523892   38377   2517   755  165   230   22  72%   -521   59   98  120   82%
c i  223.7    2394    48574   1528031   41277   2550   763   97   138   29  70%   -426  -32   47  116   41%
c i  223.8    2393    48574   1528756   41677   2559   768   93   132   29  70%   -517  -37   56  115   49%
c i  225.5    2389    48574   1538423   47914   2564   770  122   175   37  70%   -407    8   47  116   41%
c i  227.5    2384    48574   1551242   56604   2631   772  119   176   42  67%   -279    8  171  116  148%
c i  228.1    2379    48574   1554253   58877   2664   774  142   212   52  67%   -404   42   72  118   61%
c i  233.8    2365    48574   1589574   83914   2824   793  100   136   80  74%    157  -28   46  111   41%
c -  234.8    2364    48574   1593292   40104   2843   794  157   214   23  73%   -310   50  247  115  214%
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  236.2    2363    48574   1602035   46130   2899   799   90   123   34  73%   -157  -43   33  114   29%
c i  236.3    2358    48574   1602331   46285   2899   800   88   119   34  73%   -200  -47   45  113   39%
c i  239.5    2357    48574   1618938   57125   2977   806   97   127   44  76%    -45  -40   37  115   32%
c i  246.1    2344    48574   1652761   80198   3154   813  127   169   68  75%    229    7   25  116   22%
c i  246.8    2339    48574   1655856   81830   3161   815   97   126   71  77%   -220  -36   32  114   28%
c i  248.3    2336    48574   1664162   87180   3212   817  108   148   93  73%   -139  -11   44  114   39%
c i  248.3    2333    48574   1664163   87180   3212   817  108   148   93  73%   -139  -11   44  114   39%
c i  248.5    2326    48574   1665156   87765   3245   825  106   145   95  73%   -201  -14   60  113   53%
c -  249.0    2322    48574   1667436   42340   3247   826   99   136   26  73%   -216  -23   62  113   55%
c 
c [simplification-15] limit of 418 binary hit after 419 binaries
c [quatres-11] found 1297 quaternary clauses 9% in total
c [quatres-11-2] added 13 single-self-subsuming ternary resolvents
c [quatres-11-2] added 16 quaternary resolvents
c [ternres-11] limit 38684250 with penalty 0 = 0 + 0
c [ternres-11] all 2322 free variables schedulable
c [ternres-11] 34 ternary resolvents (2 bin, 32 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1208882 penalty 4 = 4 + 0
c [card-5] found 93 at-most-one constraints of average size 3.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1208882 for elimination
c [card-5] 93 out of 93 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-32] removed 160 variables
c [unhide-5] limit 483553 with penalty 4 = 4 + 0
c [unhide-5-5] 0 units, 0 failed, 39 tauts, 0 hbrs, 14169 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 20 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 2287 variables 100%
c [elim-11] limit of 773685002 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 101 variables 4% in round 1 in 22404808 steps
c [elim-11-1] backward subsumption/strengthening limit 22404800
c [elim-11-1-1] backward checking 530 touched variables 23%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 6 and strengthened 1 clauses in 1680776 steps
c [elim-11-1] rescheduled 23 variables 1% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 75642 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 101 = 4% variables out of 2287 scheduled
c [bca-8] limit of 10000000 steps and 81106 added (scaled 2)
c [bca-8] 556 out of 4374 literals actually usable 13%
c [bca-8] added 5 blocked clauses in 30203 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 29013187 penalty 2 = 2 + 0
c [sweep-5-1] 18 pos 25.4% + 53 neg 74.6% = 71 sched 3.2% ret 2115
c [sweep-5-1] 192555 steps 40 queries 14.95 avg class size
c [sweep-5-1] 2130 decisions 38 SAT calls 107.95 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-33] removed 1 variables
c [sweep-5-1] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-5-2] 500 pos 22.9% + 1685 neg 77.1% = 2185 sched 100.0% ret 0
c [sweep-5-2] 2092104 steps 235 queries 32.80 avg class size
c [sweep-5-2] 15212 decisions 236 SAT calls 242.87 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-34] removed 14 variables
c [sweep-5-2] removed 14 vars (0 failed, 11 eqs, 5 impls)
c [sweep-5-3] 498 pos 22.9% + 1673 neg 77.1% = 2171 sched 100.0% ret 0
c [sweep-5-3] 2148299 steps 233 queries 33.66 avg class size
c [sweep-5-3] 16319 decisions 231 SAT calls 246.35 avg env size
c [sweep-5-3] fully completed sweeping round
c [decomp-35] removed 2 variables
c [sweep-5-3] removed 2 vars (0 failed, 1 eqs, 2 impls)
c [sweep-5] removed 17 vars in TOTAL (3 rounds, 505 queries)
c [score-distribution-15] 1893 pos 87.28%, 276 min 12.72%, 0 zero 0.00%
c [score-distribution-15] 1052 different 48.50% out of total 2169 variables
c [simplification-15] removed 153 variables 6.6% (2169 remain 4%)
c [simplification-15] removed 8338 irredundant clauses 17.2% (40236 remain 25%)
c [simplification-15] maximum reduction of 17% = max (7%, 17%)
c [simplification-15] forced so keeping old conflict interval 457016
c [simplification-15] conflict limit remains at 1736298 (hard 1964791)
c [simplification-15] new binary interval 1000
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  256.1    2168    40236   1688575   34797   1247  1057  165   225   37  74%    121   46   48  130   37%
c i  256.1    2167    40236   1688668   34847   1249  1060  162   220   37  74%     91   42   39  130   30%
c i  256.2    2166    40236   1688832   34974   1251  1062  157   217   37  72%     43   38   33  130   26%
c i  258.1    2164    40236   1698542   40751   1292  1090   91   123   42  74%    -74  -56   54  127   42%
c i  258.9    2162    40236   1702785   43384   1304  1104  111   146   45  77%   -147  -31   76  127   60%
c i  261.2    2161    40236   1719012   54556   1339  1163  113   154   62  73%     55  -11   40  119   34%
c 
c [simplification-16] limit 1736298 conflicts (hard 1964791) hit after 1742258 conflicts
c [quatres-12] found 2093 quaternary clauses 10% in total
c [quatres-12-1] removed 2 duplicate quaternary clauses
c [quatres-12-1] added 4 double-self-subsuming ternary resolvents
c [quatres-12-2] added 61 single-self-subsuming ternary resolvents
c [quatres-12-2] added 26 quaternary resolvents
c [ternres-12] limit 40441477 with penalty 0 = 0 + 0
c [ternres-12] all 2161 free variables schedulable
c [ternres-12] 397 ternary resolvents (4 bin, 393 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-36] removed 8 variables
c [treelook-4] limit 505518 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 3853 literals 89%
c [treelook-4] scheduling used 255218 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 505518 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 511224 steps
c [treelook-4] 3817 literals remain 88%
c [treelook-4] 1788 variables remain to probed next time 83%
c [treelook-4] removed 0 variables, found 14 hbrs
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 98 transitive binary clauses
c [transred-12] found 1 units
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 2160 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 38 variables 2% in round 1 in 29563112 steps
c [elim-12-1] backward subsumption/strengthening limit 29563100
c [elim-12-1-1] backward checking 332 touched variables 15%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 289 and strengthened 6 clauses in 2335114 steps
c [elim-12-1] rescheduled 222 variables 10% by backward subsumption
c [elim-12-2] eliminated 1 variables 0% in round 2 in 2624327 steps
c [elim-12-2] backward subsumption/strengthening limit 2624300
c [elim-12-2-1] backward checking 5 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 0 and strengthened 1 clauses in 49149 steps
c [elim-12-2] rescheduled 4 variables 0% by backward subsumption
c [elim-12-3] eliminated 1 variables 0% in round 3 in 26820 steps
c [elim-12-3] backward subsumption/strengthening limit 26800
c [elim-12-3-1] backward checking 6 touched variables 0%
c [elim-12-3-1] incomplete backward checking 4 remain 67%
c [elim-12-3] subsumed 0 and strengthened 1 clauses in 26875 steps
c [elim-12] incomplete 4 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 41 = 2% variables out of 2160 scheduled
c [bca-9] limit of 10000000 steps and 79431 added (scaled 2)
c [bca-9] 403 out of 4240 literals actually usable 10%
c [bca-9] added 2 blocked clauses in 64148 steps
c [sweep-6] limit 6066221 penalty 1 = 1 + 0
c [sweep-6-1] 544 pos 25.7% + 1575 neg 74.3% = 2119 sched 100.0% ret 0
c [sweep-6-1] 2885658 steps 264 queries 40.81 avg class size
c [sweep-6-1] 17955 decisions 253 SAT calls 354.61 avg env size
c [sweep-6-1] fully completed sweeping round
c [decomp-38] removed 35 variables
c [sweep-6-1] removed 35 vars (0 failed, 18 eqs, 14 impls)
c [sweep-6-2] 538 pos 25.8% + 1546 neg 74.2% = 2084 sched 100.0% ret 0
c [sweep-6-2] 2798182 steps 264 queries 23.10 avg class size
c [sweep-6-2] 16235 decisions 227 SAT calls 357.90 avg env size
c [sweep-6-2] fully completed sweeping round
c [decomp-39] removed 46 variables
c [sweep-6-2] removed 46 vars (0 failed, 39 eqs, 43 impls)
c [sweep-6-3] 513 pos 25.2% + 1525 neg 74.8% = 2038 sched 100.0% ret 0
c [sweep-6-3] 426983 steps 22 queries 300.41 avg class size
c [sweep-6-3] 1727 decisions 21 SAT calls 538.29 avg env size
c [sweep-6-3] 1797 variables remain 88% (240 retained 12%)
c [decomp-40] removed 3 variables
c [sweep-6-3] removed 3 vars (0 failed, 2 eqs, 2 impls)
c [sweep-6] removed 84 vars in TOTAL (3 rounds, 547 queries)
c [score-distribution-16] 1799 pos 88.40%, 236 min 11.60%, 0 zero 0.00%
c [score-distribution-16] 1170 different 57.49% out of total 2035 variables
c [simplification-16] removed 126 variables 5.8% (2035 remain 4%)
c [simplification-16] removed 2216 irredundant clauses 5.5% (38020 remain 24%)
c [simplification-16] maximum reduction of 6% = max (6%, 6%)
c [simplification-16] large reduction 6% >= 5% limit
c [simplification-16] next conflict interval 17422 = min (1742258/100, 457016)
c [simplification-16] penalized conflict interval 17422 = 1 * 17422
c [simplification-16] hard conflict limit 1769680 (soft 1759680 + delta 10000)
c [simplification-16] new conflict limit 1759680 (hard 1769680)
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  269.3    2034    38020   1742304   57803   1099  1031  126   154   59  82%    164    1  261  114  229%
c i  269.3    2033    38020   1742314   57812   1099  1031  126   155   67  82%    161    1  256  114  224%
c i  269.3    2032    38020   1742327   57824   1099  1031  126   155   68  81%    157    1  247  114  217%
c i  269.3    2031    38020   1742337   57831   1099  1031  126   155   68  81%    153    1  244  114  214%
c i  269.3    2030    38020   1742339   57832   1099  1031  126   155   68  81%    153    1  243  114  213%
c i  269.3    2029    38020   1742423   57895   1099  1031  128   158   68  81%    126    4  239  114  209%
c i  269.3    2028    38020   1742439   57905   1099  1031  128   158   68  81%    121    4  235  114  206%
c i  269.3    2027    38020   1742441   57906   1099  1031  128   158   68  81%    120    4  235  114  205%
c i  269.3    2026    38020   1742442   57906   1099  1031  128   158   68  81%    120    4  234  114  205%
c i  269.3    2025    38020   1742443   57906   1099  1031  128   158   68  81%    120    4  233  114  204%
c i  269.3    2024    38020   1742445   57906   1099  1031  128   158   68  81%    119    4  232  114  203%
c i  269.3    2023    38020   1742452   57910   1099  1031  128   158   68  81%    117    4  229  114  201%
c i  269.3    2022    38020   1742457   57912   1099  1031  128   158   68  81%    116    4  228  114  200%
c i  269.3    2021    38020   1742462   57913   1099  1031  128   158   68  81%    114    4  227  114  198%
c i  269.4    2020    38020   1742755   58131   1100  1031  129   160   69  80%     40    6  157  114  138%
c i  269.5    2019    38020   1743597   58629   1100  1032  122   152   70  80%    -81   -2   96  114   84%
c i  269.5    2018    38020   1743620   58647   1100  1033  121   151   70  80%    -83   -3   90  114   79%
c i  269.6    2017    38020   1744074   58862   1100  1035  119   149   70  80%   -117   -5   99  114   87%
c i  269.7    2016    38020   1744302   58998   1100  1035  123   154   70  80%   -130   -0  152  114  133%
c i  269.7    2015    38020   1744305   59000   1100  1035  123   154   70  80%   -130   -0  152  114  133%
c i  269.7    2014    38020   1744313   59007   1100  1035  123   154   70  80%   -130   -0  151  114  132%
c i  269.7    2013    38020   1744515   59140   1100  1036  128   160   70  80%   -139    6  195  114  170%
c i  269.9    2012    38020   1745091   59442   1102  1036  127   159   70  80%   -154    5  116  115  102%
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  270.0    2011    38020   1745559   59657   1102  1036  125   155   70  81%   -161    1  129  114  113%
c i  270.1    2010    38020   1745860   59836   1102  1036  131   162   70  81%   -165    8  173  115  151%
c i  270.2    2009    38020   1746545   60293   1103  1037  119   147   70  81%   -167   -7   60  114   52%
c i  270.3    2008    38020   1746821   60486   1103  1037  113   141   70  81%   -168  -13   42  114   37%
c i  270.3    2007    38020   1746848   60502   1103  1037  113   140   70  81%   -168  -14   42  114   37%
c i  270.6    2006    38020   1748586   61390   1104  1037  108   131   70  82%   -157  -22  119  113  105%
c i  270.6    2005    38020   1748592   61395   1104  1037  108   131   70  82%   -157  -22  118  113  104%
c i  270.8    2004    38020   1749717   62067   1112  1056  111   138   70  80%   -157  -15   70  114   62%
c i  271.1    2000    38020   1751498   63197   1114  1058   91   113   70  80%   -149  -39   56  112   50%
c i  271.8    1999    38020   1754808   65232   1125  1063   94   117   74  81%   -121  -34   52  111   47%
c i  271.9    1998    38020   1755173   65494   1128  1067   89   110   74  81%   -131  -41   32  111   29%
c i  272.6    1997    38020   1758346   67518   1131  1068  106   129   71  82%   -115  -21   69  111   62%
c i  273.3    1996    38020   1762612   70090   1149  1088   68    84   71  81%    -92  -63   39  108   36%
c i  273.3    1995    38020   1762640   70103   1151  1091   67    83   71  81%    -93  -63   36  107   33%
c i  273.5    1989    38020   1763403   70596   1157  1094   62    77   71  81%   -115  -69   29  107   27%
c i  273.5    1902    38020   1763515   70647   1158  1094   62    77   71  81%   -117  -69   35  107   33%
c i  273.5    1897    38020   1763547   70655   1159  1099   62    76   71  81%   -118  -69   32  107   30%
c 0  273.5    1791    38020   1763547   70655   1159  1099   62    76   71  81%   -118  -69   32  107   30%
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: 256 basic ate = 232 trn 91% + 24 lrg 9% in 1 updates
c bcas: 9 count, 124 added (16 skipped), 340181 steps
c bkwd: tried 111911 clauses, 222661 lits, 1.99 lits/clause
c bkwd: checked 22729221 occs, 203.10 occs/clause, 102.08 occs/lit
c bkwd: subsumed 0 binary, 211 ternary, 319 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 1398 large (0% self)
c blkd: 5 bces, 1879 removed, 6240848 resolutions, 15139424 steps
c blkd: 855 blocking literals 1%, 3 pure
c bump: 1702227 bumped seen, 347138516 lits 203.9 on average
c card: 5 count, 0 units, 0 am1, 8009578 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 807 subsumed
c card: 387 at-most-one constraints found, average size 3.04
c card: 387 at-most-one constraints used 100%, average size 3.04
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 4 cces, 89 eliminated, 82 ate 92%, 7 abce 8%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 534894 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 79 gcs, 0 rescored clauses, 895 rescored vars
c dcps: 40 decompositions, 141 equivalent 0%
c deco: 167618 decision-only clauses 10%, 52% reduction
c decs: 23086775 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 43622098 push, 43568001 pop (43568001 dec 100%)
c dsch: 687276892 swaps, 0 down, 206377817 up
c elms: 12 elims, 51799 eliminated 95%, 1 pure 0%
c elms: 24 rounds, 2.0 rounds/bve
c elms: 38956 small 75%, 12839 large 25%
c elms: 43945 tried small, 38956 succeeded 89%, 4989 failed 11%
c elms: 648 subsumed, 893 strengthened, 255 blocked
c elms: 1668230 copies, 7734364 resolutions, 617095 ipos
c elms: 7855066 subchks, 3498162 strchks
c gaus: 4 extractions, 2844 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8429036 steps, 4214518 extr 50%, 77162 elim 1%
c glue: 83.4 orig avg, 83.4 real avg, 7.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 3087 = 311 simple 10% + 2772 trn 90% + 4 lrg 0%, 1106 sub 36%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1702227 clauses, 133.3 length
c lrnd: 226984918 lits = 300927196 orig - 73942278 removed 25%
c lrnd: 806337 uips 47%, 730370 flips 43%
c mins: 1351096 mins 85%, 183 bin 0%, 78454 size 5%
c mins: 125444645 poisoned searches, 39875749 hits, 32% hit rate
c mins: 277231300 used twice searches, 69147946 hits, 25% hit rate
c move: moved 1254, 164 bin 13%, 1090 trn 87%
c otfs: 62669 driving 22%, 218773 restarting 78%
c otfs: str 281442, 281345 red 100%, 97 irr 0%
c otfs: str 281442, 0 bin 0%, 144 trn 0%, 281298 lrg 100%
c otfs: sub 303, 300 red 99%, 3 irr 1%
c otfs: sub 303, 0 bin 0%, 14 trn 5%, 289 lrg 95%
c phas: 1 computed, 3881 set, 0 pos (0%), 3881 neg (100%)
c prbs: 3 basic, 26592 probed, 7 failed, 0 lifted
c prbs: 4 simple, 118126 probed, 1 failed, 4 eqs
c prbs: 4 treelook, 125 probed, 0 failed, 0 lifted
c prom: 292481 locked 5% out of 6245730 tried
c prps: 218505286 props, 9 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 12 count, 311 quat, 275 self1, 5 self2, 9 dup
c redc: 5787 clauses 13%, 44907 tried 3%, 1 sat 0%
c redc: 9902 lits 3%, 361128 tried 0%, 1 sat 0%
c redc: 1867 times jump level reduced, 19.5 levels on average
c reds: 31 count, 56888.6 conflicts per reduce
c reds: 0 memlim 0%, 31 arith 100%
c reds: 1007842 collected 83%, 210527 retired 17%
c rmbd: 150 removed, 56 red 37%
c rsts: 34913 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: 16 count, 14 confs 88%, 0 vars 0%
c simp: 1 its 6%, 1 bin 6%, 0 trns 0%
c subl: 1702227 count (1961753 tried 1.2), 324972 sub out of 1696365 (19.2%)
c swps: 6 count, 11 rounds, 1790 queries (162.7/round)
c swps: 1745 sat calls, 32 unsat (0.8% success rate)
c swps: 117139 decisions 67.1, 1349 conflicts 0.8
c swps; 57.8 avg class size, 246.8 avg environment size
c swps: 0 failed, 70 impls, 76 equivs
c swp0: 594 type 0 queries, 37 unsat (6.2%), 582 sat (98.0%)
c swp1: 1196 type 1 queries, 201 unsat (16.8%), 1132 sat (94.6%)
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: 49580187 calls to obtain time
c tops: 527 fixed 1%, 105 its, 16795.69 confs/it
c trds: 12 transitive reductions, 443 removed, 2 failed
c trds: 30542 nodes, 116148 edges, 20870572 steps
c trim: 7806575 words, 29.8 MB
c trnr: 12 count, 76 bin, 3009 trn, 17509814 steps
c unhd: 5 count, 5 rounds, 3862025 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 565 tauts, 24 bin 4%, 225 trn 40%, 103 lrg 18%
c unhd: 565 tauts, 213 stamp 38%, 345 red 61%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 48525 str, 0 bin 0%, 76 trn 0%, 48449 lrg 100%, 35022 red 72%
c vars: 1791 remaining 3% and 52467 removed 97% out of 54258
c vars: 527 fixed 1%, 51799 eliminated 95%, 141 equivalent 0%
c vsts: 4128527582 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 18.9 search visits per propagation, 2331.4 per conflict
c wchs: 1225945359 pushed, 5815955 enlarged, 225 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1696676       1007842        210527      77806308      24797297       1428803
c 
c  0 0         32131   2      2212   0         0   0   9581519  12   1944647   8     57086   4     0.4
c  1 5         16099   1      6841   1      3735   2   2668572   3    665998   3     22600   2     0.2
c  2 6         49126   3     27129   3      9045   4   7589793  10   1881918   8     70062   5     0.5
c  3 9         84308   5     53007   5     11994   6   9329758  12   2466262  10    114719   8     1.3
c  4 14       118346   7     81251   8     13346   6   9662929  12   2630428  11    123525   9     2.0
c  5 21       149234   9    105563  10     15572   7   9320500  12<  2768602  11    127168   9     2.5
c  6 30       163777  10    114614  11     17048   8   7292887   9   2498404  10<   128411   9     3.8
c  7 41       169717  10    115794  11<    17579   8   6497156   8   2358002  10    125743   9<    5.0
c  8 54       168496  10<   111329  11     18053   9<  4535111   6   1915718   8    128107   9     5.1
c  9 69       157638   9    102942  10     17422   8   3940655   5   1770617   7    121658   9     5.4
c 10 86       222013  13    128257  13     27306  13   4180832   5   2018128   8    163348  11     7.5
c 11 126      258083  15    108994  11     38855  18   2644215   3   1480095   6    157836  11    11.9
c 12 230      107309   6     49671   5     20461  10    561580   1    397661   2     88239   6    16.0
c 13 534         399   0       238   0       111   0       801   0       817   0       301   0     0.2
c 
c avg                  7.6           7.4           7.9           4.8           5.7           6.9
c std                  3.0           2.8           3.1           3.1           3.2           3.3
c 
c   19.063   7% bump
c   18.609   7% decide
c    8.227   3% elim
c    3.306   1% block
c    2.250   1% sweep
c    1.883   1% probe
c    1.772   1% unhide
c    1.669   1% cce
c 
c    2.761 < 1% rest (below)
c 
c    1.199   0% transred
c    0.643   0% bca
c    0.378   0% gauss
c    0.253   0% quatres
c    0.109   0% rescore
c    0.106   0% ternres
c    0.074   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    1.386   1% preprocessing     6%
c   22.512   8% inprocessing     94%
c ==================================
c   23.898   9% simplifying
c  249.607  91% search
c ==================================
c  273.507 100% all
c 
c       1763547 conflicts,        6447.9 confs/sec
c          5000 ternaries,         352.7 confs/ternary
c           576 binaries,         3061.7 confs/binary
c           105 iterations,      16795.7 confs/iteration
c 
c            31 reductions,          0.1 redus/sec,  56888.6 confs/reduction
c         34913 restarts,          127.6 rests/sec,     50.5 confs/restart
c      23086775 decisions,       84410.3 decis/sec,     13.1 decis/conflict
c     218505286 propagations,   798903.3 props/sec,      9.5 props/decision
c 
c 273.5 seconds, 96.9 MB
c launch: done
