c launch: /data/cnf/sc2014/app/grieu-vmpc-31.cnf.bz2
c host: atom14
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/grieu-vmpc-31.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/grieu-vmpc-31.cnf.bz2
c no embedded options
c found 'p cnf 961 146909' header
c read 961 variables, 146909 clauses, 384710 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=3
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 961 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] SUM (--score=3)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0     961   146909         0       0      0     0    0     0    4   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 10 at-most-one constraints of average size 31.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 10 out of 10 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [simpleprobe-1] all 961 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 1 variables
c [simpleprobe-1] 466 variables remain 49% (494 retained 51%)
c [simpleprobe-1] removed 1 variables, found 228 hbrs, 1 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-3] 0 units, 0 failed, 1310 tauts, 0 hbrs, 1009 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 960 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] no variable eliminated in round 1 in 0 steps
c [elim-1] fully completed in 1 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 0 = 0% variables out of 960 scheduled
c [phase-count-1] 116749 negative 99.9% of 116811 except 62 0.1%
c [phase-count-1] 87555 positive 75.0% of 116811 except 29256 25.0%
c [phase-count-1] less non-negative clauses 62 than limit 11600 (10.0%)
c [phase-count-1] non-pos/non-neg = 29256/62 = 471.87 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 960 negative 100%
c [sort-queue-1] sorted 960 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 960 (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 1 variables 0.1% (960 remain 100%)
c [simplification-1] removed 30098 irredundant clauses 20.5% (116811 remain 80%)
c [simplification-1] maximum reduction of 20% = max (0%, 20%)
c [simplification-1] large reduction 20% >= 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 [simpleprobe-2] 466 schedulable variables 49%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 470 variables remain 49% (490 retained 51%)
c [simpleprobe-2] removed 0 variables, found 11 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 1601 literals 83%
c [treelook-1] scheduling used 300154 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 327478 steps
c [treelook-1] 1585 literals remain 83%
c [treelook-1] 958 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 78 hbrs
c [basicprobe-1] limit 1037727 penalty 0 = 0 + 0
c [basicprobe-1-0] 735 probes remain 77% after last round
c [basicprobe-1-0] removed 0 variables, found 655 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 960 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 0 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] completed large round (ATE)
c [cce-1-1] allowing another 96626 steps for small clauses
c [cce-1-1] scheduling 29998 clauses = 29998 binary + 0 ternary
c [cce-1-1] tried to eliminate 3049 small clauses 10%
c [cce-1-1] eliminated 615 binary clauses 2%
c [cce-1-1] eliminated 615 small clauses 2%
c [cce-1-1] eliminated 615 small clauses in 30000007 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 615 covered clauses in round 1
c [cce-1] eliminated 615 covered clauses in TOTAL during 1 rounds
c [cce-1] 615 < 1/100 * 116811 = 1168 considered unsuccessful
c [bca-1] limit of 10000000 steps and 232892 added (scaled 2)
c [bca-1] 708 out of 1922 literals actually usable 37%
c [bca-1] added 0 blocked clauses in 2216 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 13 pos 1.4% + 947 neg 98.6% = 960 sched 100.0% ret 0
c [sweep-1-1] 1268590 steps 9 queries 140.78 avg class size
c [sweep-1-1] 774 decisions 8 SAT calls 421.00 avg env size
c [sweep-1-1] 877 variables remain 91% (83 retained 9%)
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 0 vars in TOTAL (1 rounds, 8 queries)
c [score-dist-2] active 960 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-2] max exp 520, different 8 (2%)
c [score-dist-2] median active exp 517, avg 516.8
c [simplification-2] removed 0 variables 0.0% (960 remain 100%)
c [simplification-2] removed 615 irredundant clauses 0.5% (116196 remain 79%)
c [simplification-2] maximum reduction of 1% = max (0%, 1%)
c [simplification-2] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-2] new conflict interval 10000
c [simplification-2] penalized conflict interval 10000 = 1 * 10000
c [simplification-2] hard conflict limit 21000 (soft 11000 + delta 10000)
c [simplification-2] new conflict limit 11000 (hard 21000)
c 
c [simplification-3] limit 11000 conflicts (hard 21000) hit after 11000 conflicts
c [quatres-1] found 421 quaternary clauses 31% in total
c [quatres-1-2] added 4 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1 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 960 free variables schedulable
c [ternres-1] 5626 ternary resolvents (0 bin, 5626 trn)
c [ternres-1] 524 variables remain 55% (436 retained 45%)
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 31 at-most-one constraints of average size 27.5
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 31 out of 31 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-2] limit 229190 with penalty 1 = 1 + 0
c [unhide-2-5] 0 units, 0 failed, 706 tauts, 0 hbrs, 5372 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 159 transitive binary clauses
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 960 variables 100%
c [elim-2] limit of 22919058 steps penalty 1 = 1 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 723 not tried 75% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 0 = 0% variables out of 960 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 7 pos 0.8% + 870 neg 99.2% = 877 sched 91.4% ret 83
c [sweep-2-1] 1271245 steps 7 queries 151.00 avg class size
c [sweep-2-1] 600 decisions 6 SAT calls 499.17 avg env size
c [sweep-2-1] 842 variables remain 88% (118 retained 12%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 6 queries)
c [score-dist-3] active 960 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-3] max exp 527, different 6 (1%)
c [score-dist-3] median active exp 524, avg 523.8
c [simplification-3] removed 0 variables 0.0% (960 remain 100%)
c [simplification-3] removed 5305 irredundant clauses 4.6% (110891 remain 75%)
c [simplification-3] maximum reduction of 5% = max (0%, 5%)
c [simplification-3] geometric conflict interval increment 3333 = 20000 / 6
c [simplification-3] new conflict interval 13333
c [simplification-3] penalized conflict interval 13333 = 1 * 13333
c [simplification-3] hard conflict limit 34333 (soft 24333 + delta 10000)
c [simplification-3] new conflict limit 24333 (hard 34333)
c 
c [simplification-4] limit 24333 conflicts (hard 34333) hit after 24339 conflicts
c [quatres-2] found 896 quaternary clauses 33% in total
c [quatres-2-2] added 10 single-self-subsuming ternary resolvents
c [quatres-2-2] added 3 quaternary resolvents
c [ternres-2] limit 5053763 with penalty 0 = 0 + 0
c [ternres-2] 524 schedulable variables 55%
c [ternres-2] 1305 ternary resolvents (0 bin, 1305 trn)
c [ternres-2] 399 variables remain 42% (561 retained 58%)
c [treelook-2] limit 252688 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 1394 literals 73%
c [treelook-2] scheduling used 253009 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 252688 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 257050 steps
c [treelook-2] 1380 literals remain 72%
c [treelook-2] 954 variables remain to probed next time 99%
c [treelook-2] removed 0 variables, found 6 hbrs
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 677 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 960 variables 100%
c [block-2] limit of 25268815 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] completed large round (ATE)
c [cce-2-1] allowing another 83321 steps for small clauses
c [cce-2-1] scheduling 110182 clauses = 32282 binary + 77900 ternary
c [cce-2-1] tried to eliminate 1172 small clauses 1%
c [cce-2-1] eliminated 122 binary clauses 0%
c [cce-2-1] eliminated 540 ternary clauses 1%
c [cce-2-1] eliminated 662 small clauses 1%
c [cce-2-1] eliminated 662 small clauses in 15000001 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 662 covered clauses in round 1
c [cce-2] eliminated 662 covered clauses in TOTAL during 1 rounds
c [cce-2] 662 < 1/100 * 110244 = 1102 considered unsuccessful
c [bca-2] limit of 10000000 steps and 219664 added (scaled 2)
c [bca-2] 124 out of 1922 literals actually usable 6%
c [bca-2] added 0 blocked clauses in 20842 steps
c [sweep-3] limit 1516128 penalty 0 = 0 + 0
c [sweep-3-1] 15 pos 1.8% + 827 neg 98.2% = 842 sched 87.7% ret 118
c [sweep-3-1] 1630218 steps 9 queries 114.67 avg class size
c [sweep-3-1] 800 decisions 8 SAT calls 606.62 avg env size
c [sweep-3-1] 751 variables remain 78% (209 retained 22%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 8 queries)
c [score-dist-4] active 960 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-4] max exp 529, different 7 (1%)
c [score-dist-4] median active exp 526, avg 526.1
c [simplification-4] removed 0 variables 0.0% (960 remain 100%)
c [simplification-4] removed 1309 irredundant clauses 1.2% (109582 remain 75%)
c [simplification-4] maximum reduction of 1% = max (0%, 1%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 23333
c [simplification-4] penalized conflict interval 23333 = 1 * 23333
c [simplification-4] hard conflict limit 59338 (soft 47672 + delta 11666)
c [simplification-4] new conflict limit 47672 (hard 59338)
c 
c [simplification-5] limit 47672 conflicts (hard 59338) hit after 47674 conflicts
c [quatres-3] found 1646 quaternary clauses 33% in total
c [quatres-3-2] added 20 single-self-subsuming ternary resolvents
c [quatres-3-2] added 3 quaternary resolvents
c [ternres-3] limit 10336641 with penalty 0 = 0 + 0
c [ternres-3] 399 schedulable variables 42%
c [ternres-3] 1931 ternary resolvents (0 bin, 1931 trn)
c [ternres-3] 224 variables remain 23% (736 retained 77%)
c [gauss-2] limit 1033664 penalty 1 = 1 + 0
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 519 transitive binary clauses
c [sweep-4] limit 3100992 penalty 0 = 0 + 0
c [sweep-4-1] 13 pos 1.7% + 738 neg 98.3% = 751 sched 78.2% ret 209
c [sweep-4-1] 3310603 steps 11 queries 85.82 avg class size
c [sweep-4-1] 1000 decisions 10 SAT calls 682.30 avg env size
c [sweep-4-1] 554 variables remain 58% (406 retained 42%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 10 queries)
c [score-dist-5] active 960 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-5] max exp 531, different 6 (1%)
c [score-dist-5] median active exp 528, avg 528.1
c [simplification-5] removed 0 variables 0.0% (960 remain 100%)
c [simplification-5] removed 494 irredundant clauses 0.5% (109088 remain 74%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 23333
c [simplification-5] new conflict interval 46666
c [simplification-5] penalized conflict interval 46666 = 1 * 46666
c [simplification-5] hard conflict limit 117673 (soft 94340 + delta 23333)
c [simplification-5] new conflict limit 94340 (hard 117673)
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 -   22.6     960   109088     64869   29864   9866   871   16    24   14  66%    637   11   10    9  102%
c 
c [simplification-6] limit 94340 conflicts (hard 117673) hit after 94342 conflicts
c [quatres-4] found 2844 quaternary clauses 33% in total
c [quatres-4-2] added 24 single-self-subsuming ternary resolvents
c [quatres-4-2] added 4 quaternary resolvents
c [ternres-4] limit 21600130 with penalty 0 = 0 + 0
c [ternres-4] 224 schedulable variables 23%
c [ternres-4] 2596 ternary resolvents (0 bin, 2596 trn)
c [ternres-4] 117 variables remain 12% (843 retained 88%)
c [card-3] limit 2700016 penalty 2 = 2 + 0
c [card-3] found 51 at-most-one constraints of average size 22.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 2700016 for elimination
c [card-3] 51 out of 51 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 54000326 penalty 1 = 1 + 0
c [basicprobe-2-0] 735 sched 77%, 0 failed, 0 lifted, 354 hbrs
c [basicprobe-2-1] 874 sched 91%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-2-2] 874 sched 91%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-2-3] 874 sched 91%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-3] fully completed probing
c [basicprobe-2-3] removed 0 variables, found 364 hbrs
c [unhide-3] limit 1080006 with penalty 2 = 2 + 0
c [unhide-3-7] 0 units, 0 failed, 2931 tauts, 0 hbrs, 24389 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 184 transitive binary clauses
c [elim-3] 723 variables 75% will be scheduled this time
c [elim-3] scheduled 723 variables 75%
c [elim-3] limit of 108000653 steps penalty 2 = 2 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] no variable eliminated in round 1 in 74570345 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 0 = 0% variables out of 723 scheduled
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 64800390 penalty 0 = 0 + 0
c [sweep-5-1] 6 pos 1.1% + 548 neg 98.9% = 554 sched 57.7% ret 406
c [sweep-5-1] 10032830 steps 39 queries 27.10 avg class size
c [sweep-5-1] 3789 decisions 38 SAT calls 564.87 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-2] 10 pos 1.0% + 950 neg 99.0% = 960 sched 100.0% ret 0
c [sweep-5-2] 7354562 steps 39 queries 41.56 avg class size
c [sweep-5-2] 3683 decisions 38 SAT calls 557.29 avg env size
c [sweep-5-2] fully completed sweeping round
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-3] 10 pos 1.0% + 950 neg 99.0% = 960 sched 100.0% ret 0
c [sweep-5-3] 9454735 steps 41 queries 38.71 avg class size
c [sweep-5-3] 3903 decisions 40 SAT calls 567.90 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 116 queries)
c [score-dist-6] active 960 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-6] max exp 533, different 6 (1%)
c [score-dist-6] median active exp 530, avg 530.2
c [simplification-6] removed 0 variables 0.0% (960 remain 100%)
c [simplification-6] removed 1816 irredundant clauses 1.7% (107272 remain 73%)
c [simplification-6] maximum reduction of 2% = max (0%, 2%)
c [simplification-6] geometric conflict interval increment 15555 = 46666 / 3
c [simplification-6] new conflict interval 62221
c [simplification-6] penalized conflict interval 62221 = 1 * 62221
c [simplification-6] hard conflict limit 187673 (soft 156563 + delta 31110)
c [simplification-6] new conflict limit 156563 (hard 187673)
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.8     960   107272    100427   33617  12301   786   14    21   14  70%    799    4   14   12  122%
c -   47.4     960   107272    136277   36791  12438   801   12    18   15  69%    894    0   12   12   94%
c 
c [simplification-7] limit 156563 conflicts (hard 187673) hit after 157604 conflicts
c [quatres-5] found 4076 quaternary clauses 31% in total
c [quatres-5-2] added 69 single-self-subsuming ternary resolvents
c [quatres-5-2] added 7 quaternary resolvents
c [ternres-5] limit 35328595 with penalty 0 = 0 + 0
c [ternres-5] 117 schedulable variables 12%
c [ternres-5] 3936 ternary resolvents (0 bin, 3936 trn)
c [ternres-5] 40 variables remain 4% (920 retained 96%)
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 612 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 960 variables 100%
c [block-3] limit of 88321488 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [cce-3] limit of 44160744 steps penalty 2 = 2 + 0
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] allowing another 85677 steps for small clauses
c [cce-3-1] scheduling 34543 clauses = 34543 binary + 0 ternary
c [cce-3-1] tried to eliminate 4662 small clauses 13%
c [cce-3-1] eliminated 1215 binary clauses 4%
c [cce-3-1] eliminated 1215 small clauses 4%
c [cce-3-1] eliminated 1215 small clauses in 44160779 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1215 covered clauses in round 1
c [cce-3] eliminated 1215 covered clauses in TOTAL during 1 rounds
c [bca-3] limit of 10000000 steps and 211440 added (scaled 2)
c [bca-3] 79 out of 1922 literals actually usable 4%
c [bca-3] not enough literals usable
c [bca-3] added 0 blocked clauses in 54660 steps
c [score-dist-7] active 960 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-7] max exp 535, different 5 (1%)
c [score-dist-7] median active exp 531, avg 531.6
c [simplification-7] removed 0 variables 0.0% (960 remain 100%)
c [simplification-7] removed 1802 irredundant clauses 1.7% (105470 remain 72%)
c [simplification-7] maximum reduction of 2% = max (0%, 2%)
c [simplification-7] geometric conflict interval increment 20740 = 62221 / 3
c [simplification-7] new conflict interval 82961
c [simplification-7] penalized conflict interval 82961 = 1 * 82961
c [simplification-7] hard conflict limit 282045 (soft 240565 + delta 41480)
c [simplification-7] new conflict limit 240565 (hard 282045)
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   59.1     959   105470    168610   64281  16520  2002   14    19   23  74%    945    1    8   13   62%
c -   59.9     959   105470    171572   35809  16533  2002   14    19   14  72%  -1462    1   14   13  107%
c -   70.6     959   105470    208565   39257  16622  2004   21    30   15  68%   -474    8   18   16  117%
c -   81.0     959   105470    245783   42360  16709  2007   15    20   16  72%    175   -3   15   16   94%
c 
c [simplification-8] limit 240565 conflicts (hard 282045) hit after 248648 conflicts
c [quatres-6] found 4439 quaternary clauses 39% in total
c [quatres-6-2] added 21 single-self-subsuming ternary resolvents
c [quatres-6-2] added 2 quaternary resolvents
c [ternres-6] limit 55543065 with penalty 0 = 0 + 0
c [ternres-6] 39 schedulable variables 4%
c [ternres-6] 5269 ternary resolvents (0 bin, 5269 trn)
c [ternres-6] 15 variables remain 2% (944 retained 98%)
c [gauss-3] limit 2777153 penalty 2 = 2 + 0
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 470 schedulable variables 49%
c [simpleprobe-3] limit 100000000 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 314 hbrs, 0 units
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 524 transitive binary clauses
c [sweep-6] limit 8331459 penalty 1 = 1 + 0
c [sweep-6-1] 10 pos 1.0% + 949 neg 99.0% = 959 sched 100.0% ret 0
c [sweep-6-1] 8478284 steps 40 queries 30.07 avg class size
c [sweep-6-1] 3881 decisions 39 SAT calls 579.95 avg env size
c [sweep-6-1] 15 variables remain 2% (944 retained 98%)
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 39 queries)
c [score-dist-8] active 959 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-8] max exp 536, different 6 (1%)
c [score-dist-8] median active exp 533, avg 532.9
c [simplification-8] removed 0 variables 0.0% (959 remain 100%)
c [simplification-8] removed 610 irredundant clauses 0.6% (104860 remain 71%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 41480 = 82961 / 2
c [simplification-8] new conflict interval 124441
c [simplification-8] penalized conflict interval 124441 = 1 * 124441
c [simplification-8] hard conflict limit 435309 (soft 373089 + delta 62220)
c [simplification-8] new conflict limit 373089 (hard 435309)
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 -   94.0     959   104860    284864   39540  21455  2140   16    26   16  62%    556    1   14   17   86%
c -  105.5     959   104860    321406   41642  21510  2144   21    32   16  67%    756    7   20   17  115%
c -  117.3     959   104860    358941   42967  21575  2149   17    24   16  72%    873   -1   13   17   75%
c 
c [simplification-9] limit 373089 conflicts (hard 435309) hit after 375817 conflicts
c [quatres-7] found 6348 quaternary clauses 36% in total
c [quatres-7-2] added 47 single-self-subsuming ternary resolvents
c [quatres-7-2] added 7 quaternary resolvents
c [ternres-7] limit 83459678 with penalty 0 = 0 + 0
c [ternres-7] 15 schedulable variables 2%
c [ternres-7] 9808 ternary resolvents (2 bin, 9806 trn)
c [ternres-7] 5 variables remain 1% (954 retained 99%)
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 391 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 2086491970 steps penalty 1 = 1 + 0
c [cce-4-1] completed large round (ATE)
c [cce-4-1] allowing another 76705 steps for small clauses
c [cce-4-1] scheduling 32652 clauses = 32652 binary + 0 ternary
c [cce-4-1] tried to eliminate 32652 small clauses 100%
c [cce-4-1] eliminated 6101 binary clauses 19%
c [cce-4-1] eliminated 6101 small clauses 19%
c [cce-4-1] eliminated 6101 small clauses in 319387593 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 6101 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 76718 steps for small clauses
c [cce-4-2] scheduling 26551 clauses = 26551 binary + 0 ternary
c [cce-4-2] tried to eliminate 26551 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 6101 covered clauses in TOTAL during 2 rounds
c [score-dist-9] active 959 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-9] max exp 537, different 6 (1%)
c [score-dist-9] median active exp 534, avg 534.2
c [simplification-9] removed 0 variables 0.0% (959 remain 100%)
c [simplification-9] removed 6385 irredundant clauses 6.1% (98475 remain 67%)
c [simplification-9] maximum reduction of 6% = max (0%, 6%)
c [simplification-9] geometric conflict interval increment 17777 = 124441 / 7
c [simplification-9] new conflict interval 142218
c [simplification-9] penalized conflict interval 142218 = 1 * 142218
c [simplification-9] hard conflict limit 589144 (soft 518035 + delta 71109)
c [simplification-9] new conflict limit 518035 (hard 589144)
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 -  140.2     959    98475    399805   45517  31516  8127   14    19   17  73%    943   -4   13   16   79%
c -  153.5     959    98475    438648   47219  31542  8127   17    24   17  70%    979    2   20   16  121%
c -  167.7     959    98475    475736   48605  31559  8127   20    28   18  73%    999    2   20   18  111%
c i  175.2     958    98475    496668   67192  31581  8132   16    22   24  73%   1006   -3   10   18   55%
c -  180.3     958    98475    515489   50086  31641  8133   18    32   18  56%  -2897    6   15   18   82%
c -  192.6     958    98475    558221   53983  31724  8138   16    23   19  70%  -1019   -2   14   17   82%
c 
c [simplification-10] limit 518035 conflicts (hard 589144) hit after 589144 conflicts
c [quatres-8] found 8483 quaternary clauses 40% in total
c [quatres-8-2] added 23 single-self-subsuming ternary resolvents
c [quatres-8-2] added 10 quaternary resolvents
c [ternres-8] limit 134385332 with penalty 0 = 0 + 0
c [ternres-8] 5 schedulable variables 1%
c [ternres-8] 15219 ternary resolvents (71 bin, 15148 trn)
c [ternres-8] 3 variables remain 0% (955 retained 100%)
c [card-4] limit 8399083 penalty 3 = 3 + 0
c [card-4] found 80 at-most-one constraints of average size 24.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 8399083 for elimination
c [card-4] 80 out of 80 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-26] removed 1 variables
c [unhide-4] limit 2500000 with penalty 3 = 3 + 0
c [unhide-4-10] 0 units, 0 failed, 3685 tauts, 0 hbrs, 30836 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 130 transitive binary clauses
c [cce-5] limit of 671926660 steps penalty 0 = 0 + 0
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] allowing another 88284 steps for small clauses
c [cce-5-1] scheduling 98177 clauses = 26599 binary + 71578 ternary
c [cce-5-1] tried to eliminate 45283 small clauses 46%
c [cce-5-1] eliminated 32 binary clauses 0%
c [cce-5-1] eliminated 9254 ternary clauses 13%
c [cce-5-1] eliminated 9286 small clauses 9%
c [cce-5-1] eliminated 9286 small clauses in 671926736 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 9286 covered clauses in round 1
c [cce-5] eliminated 9286 covered clauses in TOTAL during 1 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 958 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 2000000000 steps penalty 3 = 3 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 64876210 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 958 scheduled
c [score-dist-10] active 958 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-10] max exp 538, different 5 (1%)
c [score-dist-10] median active exp 535, avg 535.5
c [simplification-10] removed 0 variables 0.0% (958 remain 100%)
c [simplification-10] removed 9529 irredundant clauses 9.7% (88946 remain 61%)
c [simplification-10] maximum reduction of 10% = max (0%, 10%)
c [simplification-10] geometric conflict interval increment 12928 = 142218 / 11
c [simplification-10] new conflict interval 155146
c [simplification-10] penalized conflict interval 155146 = 1 * 155146
c [simplification-10] hard conflict limit 821863 (soft 744290 + delta 77573)
c [simplification-10] new conflict limit 744290 (hard 821863)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  219.4     958    88946    603347   51481  54708  5308   17    24   19  71%     -2   -1   15   17   89%
c -  232.8     958    88946    645043   53172  54752  5310   19    26   19  74%    481    1   24   18  135%
c -  246.8     958    88946    687978   54283  54799  5311   18    23   19  76%    742   -2   22   18  125%
c -  262.1     958    88946    732920   56076  54837  5311   16    21   19  77%    882   -2   15   17   87%
c 
c [simplification-11] limit 744290 conflicts (hard 821863) hit after 746939 conflicts
c [quatres-9] found 10372 quaternary clauses 39% in total
c [quatres-9-2] added 29 single-self-subsuming ternary resolvents
c [quatres-9-2] added 19 quaternary resolvents
c [ternres-9] limit 173318295 with penalty 0 = 0 + 0
c [ternres-9] 3 schedulable variables 0%
c [ternres-9] 19763 ternary resolvents (135 bin, 19628 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-3] limit 4332957 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 1910 literals 100%
c [treelook-3] scheduling used 740594 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 4332957 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 4334936 steps
c [treelook-3] 1761 literals remain 92%
c [treelook-3] 951 variables remain to probed next time 99%
c [treelook-3] removed 0 variables, found 4 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 94 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 958 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [cce-6] limit of 866591477 steps penalty 0 = 0 + 0
c [cce-6-1] completed large round (ATE)
c [cce-6-1] allowing another 66613 steps for small clauses
c [cce-6-1] scheduling 88877 clauses = 26576 binary + 62301 ternary
c [cce-6-1] tried to eliminate 72721 small clauses 82%
c [cce-6-1] eliminated 20 binary clauses 0%
c [cce-6-1] eliminated 5051 ternary clauses 8%
c [cce-6-1] eliminated 5071 small clauses 6%
c [cce-6-1] eliminated 5071 small clauses in 866591505 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 5071 covered clauses in round 1
c [cce-6] eliminated 5071 covered clauses in TOTAL during 1 rounds
c [bca-4] limit of 10000000 steps and 168236 added (scaled 2)
c [bca-4] 41 out of 1918 literals actually usable 2%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 68341 steps
c [sweep-7] limit 12998872 penalty 2 = 2 + 0
c [sweep-7-1] 0 pos 0.0% + 15 neg 100.0% = 15 sched 1.6% ret 943
c [sweep-7-1] 4024359 steps 12 queries 6.50 avg class size
c [sweep-7-1] 1100 decisions 11 SAT calls 534.82 avg env size
c [sweep-7-1] fully completed sweeping round
c [sweep-7-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7-2] 16 pos 1.7% + 942 neg 98.3% = 958 sched 100.0% ret 0
c [sweep-7-2] 9249656 steps 26 queries 48.65 avg class size
c [sweep-7-2] 2500 decisions 25 SAT calls 683.88 avg env size
c [sweep-7-2] 20 variables remain 2% (938 retained 98%)
c [sweep-7-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7] removed 0 vars in TOTAL (2 rounds, 36 queries)
c [score-dist-11] active 958 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-11] max exp 539, different 6 (1%)
c [score-dist-11] median active exp 536, avg 536.2
c [simplification-11] removed 0 variables 0.0% (958 remain 100%)
c [simplification-11] removed 5078 irredundant clauses 5.7% (83868 remain 57%)
c [simplification-11] maximum reduction of 6% = max (0%, 6%)
c [simplification-11] geometric conflict interval increment 22163 = 155146 / 7
c [simplification-11] new conflict interval 177309
c [simplification-11] penalized conflict interval 177309 = 1 * 177309
c [simplification-11] hard conflict limit 1012902 (soft 924248 + delta 88654)
c [simplification-11] new conflict limit 924248 (hard 1012902)
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 -  293.8     958    83868    777339   58587  79571  5386   23    32   21  71%    952    9   26   17  148%
c -  310.6     958    83868    821096   60478  79602  5386   14    18   21  79%    987   -8   10   19   53%
c i  311.9     957    83868    824866   63866  79627  5389   13    20   26  67%    989   -6    8   18   45%
c -  325.6     957    83868    866661   64008  79754  5390   18    28   21  65%  -1748    0   25   18  139%
c -  341.7     957    83868    912008   68638  79848  5390   21    33   22  66%   -363    3   24   19  128%
c 
c [simplification-12] limit 924248 conflicts (hard 1012902) hit after 931914 conflicts
c [quatres-10] found 12473 quaternary clauses 42% in total
c [quatres-10-2] added 14 single-self-subsuming ternary resolvents
c [quatres-10-2] added 24 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 957 free variables schedulable
c [ternres-10] 16092 ternary resolvents (78 bin, 16014 trn)
c [ternres-10] 148 variables remain 15% (809 retained 85%)
c [gauss-4] limit 5564692 penalty 3 = 3 + 0
c [gauss-4] extracted 0 xors of average arity 0.0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 86 transitive binary clauses
c [cce-7] limit of 1112938403 steps penalty 0 = 0 + 0
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] allowing another 72864 steps for small clauses
c [cce-7-1] scheduling 26564 clauses = 26564 binary + 0 ternary
c [cce-7-1] tried to eliminate 26564 small clauses 100%
c [cce-7-1] eliminated 42 binary clauses 0%
c [cce-7-1] eliminated 42 small clauses 0%
c [cce-7-1] eliminated 42 small clauses in 198424776 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 42 covered clauses in round 1
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] allowing another 72884 steps for small clauses
c [cce-7-2] scheduling 26522 clauses = 26522 binary + 0 ternary
c [cce-7-2] tried to eliminate 26522 small clauses 100%
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 0 covered clauses in round 2
c [cce-7] eliminated 42 covered clauses in TOTAL during 2 rounds
c [cce-7] 42 < 1/100 * 83700 = 837 considered unsuccessful
c [score-dist-12] active 957 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-12] max exp 539, different 5 (1%)
c [score-dist-12] median active exp 537, avg 536.8
c [simplification-12] removed 0 variables 0.0% (957 remain 100%)
c [simplification-12] removed 210 irredundant clauses 0.3% (83658 remain 57%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 177309
c [simplification-12] new conflict interval 354618
c [simplification-12] penalized conflict interval 354618 = 1 * 354618
c [simplification-12] hard conflict limit 1463841 (soft 1286532 + delta 177309)
c [simplification-12] new conflict limit 1286532 (hard 1463841)
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 -  368.4     957    83658    958131   65573  95290  5482   26    41   23  63%    338    5   26   23  112%
c -  384.4     957    83658   1001311   65905  95345  5482   18    26   23  68%    669   -9   22   22  100%
c i  389.7     956    83658   1018029   81451  95413  5491   14    24   30  60%    749   -9    9   21   44%
c -  401.2     955    83658   1048737   69332  95469  5493   26    45   23  58%  -1067   12   34   21  160%
c -  418.3     955    83658   1095746   74019  95564  5494   18    28   24  63%      3   -8   13   21   64%
c i  422.2     954    83658   1107981   85210  95619  5499   16    25   32  64%    177   -9   10   20   50%
c -  433.8     954    83658   1143000   77297  95688  5500   20    32   24  61%   -309    1   16   19   81%
c -  449.1     954    83658   1188772   79487  95792  5500   24    39   24  63%    361    4   23   21  109%
c -  466.4     954    83658   1234360   81013  95856  5500   31    50   25  63%    693    6   28   28  101%
c -  484.0     954    83658   1281580   82416  95910  5500   24    35   25  69%    863   -7   22   26   85%
c i  498.0     953    83658   1318813  116428  95973  5505   19    27   38  71%    933  -10   12   24   50%
c -  503.0     952    83658   1333051   85479  96005  5506   29    44   25  67%  -1742    8   35   24  144%
c -  523.0     952    83658   1386551   88694  96086  5509   20    27   25  74%   -199   -7   23   24   97%
c 
c [simplification-13] limit 1286532 conflicts (hard 1463841) hit after 1398181 conflicts
c [quatres-11] found 18630 quaternary clauses 44% in total
c [quatres-11-2] added 40 single-self-subsuming ternary resolvents
c [quatres-11-2] added 45 quaternary resolvents
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] 146 schedulable variables 15%
c [ternres-11] 15756 ternary resolvents (54 bin, 15702 trn)
c [ternres-11] 57 variables remain 6% (895 retained 94%)
c [decomp-32] removed 5 variables
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 155 transitive binary clauses
c [score-dist-13] active 952 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-13] max exp 540, different 5 (1%)
c [score-dist-13] median active exp 538, avg 538.2
c [simplification-13] removed 0 variables 0.0% (952 remain 99%)
c [simplification-13] removed 683 irredundant clauses 0.8% (82975 remain 56%)
c [simplification-13] maximum reduction of 1% = max (0%, 1%)
c [simplification-13] geometric conflict interval increment 177309 = 354618 / 2
c [simplification-13] new conflict interval 531927
c [simplification-13] penalized conflict interval 531927 = 1 * 531927
c [simplification-13] hard conflict limit 2196071 (soft 1930108 + delta 265963)
c [simplification-13] new conflict limit 1930108 (hard 2196071)
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 -  548.7     952    82975   1441914   83034 109430  5917   23    33   26  70%    499    2   34   23  153%
c -  569.6     952    82975   1494251   85249 109473  5919   19    26   26  76%    788   -4   23   22  109%
c -  591.4     952    82975   1548676   86716 109514  5919   18    24   26  77%    921   -5   18   21   89%
c -  614.5     952    82975   1603431   87726 109541  5922   19    24   26  79%    979   -3   16   20   78%
c -  637.8     952    82975   1658542   89525 109566  5923   23    32   27  73%   1005    4   28   21  130%
c -  662.6     952    82975   1711535   90702 109578  5924   24    32   27  75%   1015   -2   20   25   79%
c -  688.4     952    82975   1767643   91756 109596  5927   17    22   27  75%   1020   -7   19   22   88%
c i  694.4     951    82975   1782168  104387 109633  5934   19    25   34  76%   1021   -4   11   22   52%
c -  711.1     951    82975   1825766   95759 109695  5939   18    24   28  73%  -2759   -4   13   21   62%
c -  733.8     951    82975   1881274   98995 109752  5939   21    31   27  69%   -598    1   21   21   96%
c 
c [simplification-14] limit 1930108 conflicts (hard 2196071) hit after 1930108 conflicts
c [quatres-12] found 21878 quaternary clauses 43% in total
c [quatres-12-2] added 45 single-self-subsuming ternary resolvents
c [quatres-12-2] added 52 quaternary resolvents
c [ternres-12] limit 200000000 with penalty 0 = 0 + 0
c [ternres-12] 57 schedulable variables 6%
c [ternres-12] 10493 ternary resolvents (5 bin, 10488 trn)
c [ternres-12] 25 variables remain 3% (926 retained 97%)
c [decomp-33] removed 1 variables
c [basicprobe-3] limit 100000000 penalty 2 = 2 + 0
c [basicprobe-3-0] 867 sched 91%, 0 failed, 0 lifted, 20 hbrs
c [basicprobe-3-1] 867 sched 91%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-1] fully completed probing
c [basicprobe-3-1] removed 0 variables, found 20 hbrs
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 104 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 10737418235 steps penalty 1 = 1 + 0
c [cce-8-1] completed large round (ATE)
c [cce-8-1] allowing another 60171 steps for small clauses
c [cce-8-1] scheduling 82739 clauses = 26493 binary + 56246 ternary
c [cce-8-1] tried to eliminate 82739 small clauses 100%
c [cce-8-1] eliminated 38 binary clauses 0%
c [cce-8-1] eliminated 1105 ternary clauses 2%
c [cce-8-1] eliminated 1143 small clauses 1%
c [cce-8-1] eliminated 1143 small clauses in 854664808 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 1143 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 59022 steps for small clauses
c [cce-8-2] scheduling 81596 clauses = 26455 binary + 55141 ternary
c [cce-8-2] tried to eliminate 81596 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 1143 covered clauses in TOTAL during 2 rounds
c [score-dist-14] active 951 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-14] max exp 541, different 5 (1%)
c [score-dist-14] median active exp 539, avg 539.1
c [simplification-14] removed 0 variables 0.0% (951 remain 99%)
c [simplification-14] removed 1317 irredundant clauses 1.6% (81658 remain 56%)
c [simplification-14] maximum reduction of 2% = max (0%, 2%)
c [simplification-14] geometric conflict interval increment 177309 = 531927 / 3
c [simplification-14] new conflict interval 709236
c [simplification-14] penalized conflict interval 709236 = 1 * 709236
c [simplification-14] hard conflict limit 2993962 (soft 2639344 + delta 354618)
c [simplification-14] new conflict limit 2639344 (hard 2993962)
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 -  788.4     951    81658   1939415   95083 120869  5885   31    44   28  69%    356   10   33   25  132%
c -  812.9     951    81658   1992820   95603 120888  5885   23    31   28  76%    728   -6   19   26   73%
c i  828.4     950    81658   2029667  128705 120930  5888   15    21   42  71%    855  -12    9   23   39%
c -  835.1     950    81658   2050142   97697 120974  5888   22    36   29  60%  -1974    4   18   23   79%
c -  854.8     950    81658   2105685  102298 121087  5888   31    57   29  53%   -260   17   30   25  122%
c -  876.1     950    81658   2160517  105308 121167  5888   21    34   29  62%    468   -8   27   24  110%
c i  883.8     949    81658   2183548  127062 121224  5899   16    25   43  62%    633  -14   10   23   44%
c -  898.5     948    81658   2220229  107339 121261  5902   20    28   29  72%   -595   -7   25   22  111%
c -  924.6     948    81658   2281192  110805 121294  5904   23    31   30  75%    385   -1   30   22  139%
c -  950.9     948    81658   2340185  112703 121325  5904   25    36   30  70%    764    4   24   23  103%
c -  977.9     948    81658   2397193  113345 121350  5904   36    51   30  71%    915   12   36   28  125%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 4 count, 0 added (0 skipped), 146059 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 4 bces, 0 removed, 1187681 resolutions, 3491317 steps
c blkd: 58 blocking literals 3%, 0 pure
c bump: 2440405 bumped seen, 304906972 lits 124.9 on average
c card: 4 count, 0 units, 0 am1, 33410899 steps
c card: 21 rescheduled, 48 eliminated, 31542 resolved, 311 subsumed
c card: 172 at-most-one constraints found, average size 24.73
c card: 172 at-most-one constraints used 100%, average size 24.73
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: 8 cces, 24135 eliminated, 23992 ate 99%, 143 abce 1%
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: 531619 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 50 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 34 decompositions, 0 equivalent 0%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 4605900 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 4 elims, 0 eliminated 0%, 0 pure 0%
c elms: 4 rounds, 1.0 rounds/bve
c elms: 0 small 0%, 0 large 0%
c elms: 0 tried small, 0 succeeded 0%, 0 failed 0%
c elms: 4892 subsumed, 7965 strengthened, 0 blocked
c elms: 555451 copies, 541596 resolutions, 0 ipos
c elms: 5093904 subchks, 1921265 strchks
c gaus: 4 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 22776650 steps, 11388325 extr 50%, 0 elim 0%
c glue: 21.2 orig avg, 21.2 real avg, 4.2 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1870 = 553 simple 30% + 1317 trn 70% + 0 lrg 0%, 1185 sub 63%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2440405 clauses, 47.3 length
c lrnd: 115316797 lits = 233553327 orig - 118236530 removed 51%
c lrnd: 733143 uips 30%, 1490284 flips 61%
c mins: 2415383 mins 99%, 3 bin 0%, 25019 size 1%
c mins: 126767376 poisoned searches, 20604627 hits, 16% hit rate
c mins: 337191299 used twice searches, 25043006 hits, 7% hit rate
c move: moved 24861, 8185 bin 33%, 16676 trn 67%
c otfs: 4541 driving 18%, 20936 restarting 82%
c otfs: str 25477, 25421 red 100%, 56 irr 0%
c otfs: str 25477, 0 bin 0%, 79 trn 0%, 25398 lrg 100%
c otfs: sub 23, 23 red 100%, 0 irr 0%
c otfs: sub 23, 0 bin 0%, 0 trn 0%, 23 lrg 100%
c phas: 1 computed, 960 set, 0 pos (0%), 960 neg (100%)
c prbs: 3 basic, 10460 probed, 0 failed, 0 lifted
c prbs: 3 simple, 2897 probed, 1 failed, 0 eqs
c prbs: 3 treelook, 179 probed, 0 failed, 0 lifted
c prom: 335753 locked 33% out of 1009459 tried
c prps: 376596617 props, 82 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 12 count, 177 quat, 346 self1, 0 self2, 0 dup
c queu: 1 sorted, 4605900 next (188325 steps 0.04)
c queu: 304908893 enq (530960916 steps 1.74), 304906972 deq 100%
c redc: 28184 clauses 21%, 134674 tried 6%, 1 sat 0%
c redc: 41070 lits 3%, 1482326 tried 1%, 1 sat 0%
c redc: 1162 times jump level reduced, 2.1 levels on average
c reds: 50 count, 48852.5 conflicts per reduce
c reds: 0 memlim 0%, 50 arith 100%
c reds: 1862608 collected 93%, 142862 retired 7%
c rmbd: 30578 removed, 672 red 2%
c rsts: 29346 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 14 count, 14 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 2440405 count (2233560 tried 0.9), 225483 sub out of 2436395 (9.3%)
c swps: 7 count, 10 rounds, 223 queries (22.3/round)
c swps: 223 sat calls, 0 unsat (10.4% success rate)
c swps: 22030 decisions 98.8, 2320 conflicts 10.4
c swps; 49.8 avg class size, 578.5 avg environment size
c swps: 0 failed, 0 impls, 0 equivs
c swp0: 70 type 0 queries, 5 unsat (7.1%), 70 sat (100.0%)
c swp1: 153 type 1 queries, 17 unsat (11.1%), 153 sat (100.0%)
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: 14092891 calls to obtain time
c tops: 13 fixed 1%, 9 its, 271402.89 confs/it
c trds: 12 transitive reductions, 3635 removed, 0 failed
c trds: 20917 nodes, 334001 edges, 23891238 steps
c trim: 1986624 words, 7.6 MB
c trnr: 12 count, 345 bin, 107449 trn, 1139025506 steps
c unhd: 4 count, 10 rounds, 4741662 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: 8632 tauts, 9 bin 0%, 2212 trn 26%, 2243 lrg 26%
c unhd: 8632 tauts, 4168 stamp 48%, 6766 red 78%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 61606 str, 0 bin 0%, 2741 trn 4%, 58865 lrg 96%, 59584 red 97%
c vars: 948 remaining 99% and 13 removed 1% out of 961
c vars: 13 fixed 1%, 0 eliminated 0%, 0 equivalent 0%
c vsts: 64476862584 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 171.3 search visits per propagation, 26349.7 per conflict
c wchs: 7185543024 pushed, 886486 enlarged, 362 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2436572       1862608        142862      29529302      10479998       1262160
c 
c  0 0        112395   5     10944   1         0   0   5004920  17   1506367  14     71071   6     2.0
c  1 5         36729   2     23115   1      8705   6   1368774   5    376513   4     68216   5     0.3
c  2 6        178030   7    117121   6     35065  25   6603823  22   1874428  18    342716  27     2.0
c  3 9        377753  16    285704  15     42280  30<  7841714  27<  2576660  25<   382925  30<    4.0
c  4 14       581823  24<   480771  26<    28973  20   5716688  19   2316862  22    235584  19     4.2
c  5 21       603674  25    505940  27     18529  13   1897275   6   1101971  11    107256   8     4.5
c  6 30       380761  16    312779  17      7451   5    805132   3    526922   5     41315   3     4.7
c  7 41       135415   6    106385   6      1644   1    238402   1    164569   2     10777   1     3.4
c  8 54        26051   1     18093   1       202   0     45787   0     31005   0      2020   0     2.0
c  9 69         3713   0      1711   0        11   0      6363   0      4423   0       262   0     0.6
c 10 86          228   0        45   0         2   0       424   0       278   0        18   0     0.1
c 
c avg                  4.2           4.5           3.3           2.6           3.0           2.9
c std                  1.7           1.4           1.3           1.6           1.7           1.4
c 
c   60.138   6% cce
c   43.716   4% bump
c   14.807   1% ternres
c    5.383   1% transred
c 
c   12.317 < 1% rest (below)
c 
c    2.766   0% decide
c    2.697   0% probe
c    1.808   0% sweep
c    1.506   0% unhide
c    1.426   0% elim
c    1.260   0% quatres
c    0.302   0% card
c    0.285   0% gauss
c    0.213   0% block
c    0.055   0% bca
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.340   0% preprocessing     0%
c   91.262   9% inprocessing    100%
c ==================================
c   91.602   9% simplifying
c  908.360  91% search
c ==================================
c  999.962 100% all
c 
c       2442626 conflicts,        2442.7 confs/sec
c          3821 ternaries,         639.3 confs/ternary
c           146 binaries,        16730.3 confs/binary
c             9 iterations,     271402.9 confs/iteration
c 
c            50 reductions,          0.1 redus/sec,  48852.5 confs/reduction
c         29346 restarts,           29.3 rests/sec,     83.2 confs/restart
c       4605900 decisions,        4606.1 decis/sec,      1.9 decis/conflict
c     376596617 propagations,   376611.1 props/sec,     81.8 props/decision
c 
c 1000.0 seconds, 65.8 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
