c launch: /data/cnf/sc2014/app/MD5-32-2.cnf.bz2
c host: atom11
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/MD5-32-2.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/MD5-32-2.cnf.bz2
c no embedded options
c found 'p cnf 9524 73623' header
c read 9524 variables, 73623 clauses, 288325 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 9513 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    9513    73358         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 1 at-most-one constraints of average size 3.0
c [card-1] found 120 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 121 out of 121 constraints (100%) meet size limits
c [card-1] found 1 units
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 28 variables
c [simpleprobe-1] all 9496 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 4 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 4 variables, found 341 hbrs, 0 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 84 tauts, 0 hbrs, 64 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 9492 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 2745 variables 29% in round 1 in 9827717 steps
c [elim-1-1] backward subsumption/strengthening limit 9827700
c [elim-1-1-1] backward checking 6654 touched variables 70%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 20 and strengthened 25 clauses in 1348640 steps
c [elim-1-1] rescheduled 59 variables 1% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 150878 steps
c [elim-1-2] backward subsumption/strengthening limit 150800
c [elim-1-2-1] backward checking 40 touched variables 0%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 0 and strengthened 7 clauses in 145200 steps
c [elim-1-2] rescheduled 12 variables 0% by backward subsumption
c [elim-1-3] eliminated 1 variables 0% in round 3 in 14770 steps
c [elim-1-3] backward subsumption/strengthening limit 14700
c [elim-1-3-1] backward checking 7 touched variables 0%
c [elim-1-3-1] incomplete backward checking 0 remain 0%
c [elim-1-3] subsumed 1 and strengthened 1 clauses in 14701 steps
c [elim-1] incomplete 3 not tried 0% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 2748 = 29% variables out of 9492 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 71881 negative 99.1% of 72524 except 643 0.9%
c [phase-count-1] 69832 positive 96.3% of 72524 except 2692 3.7%
c [phase-count-1] less non-negative clauses 643 than limit 7200 (10.0%)
c [phase-count-1] non-pos/non-neg = 2692/643 = 4.19 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 6744 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 6744 zero 100.00%
c [score-distribution-1] 1 different 0.01% out of total 6744 variables
c [simplification-1] removed 2769 variables 29.1% (6744 remain 71%)
c [simplification-1] removed 834 irredundant clauses 1.1% (72524 remain 99%)
c [simplification-1] maximum reduction of 29% = max (29%, 1%)
c [simplification-1] large reduction 29% >= 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] all 6744 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 3007 variables remain 45% (3737 retained 55%)
c [simpleprobe-2] removed 0 variables, found 17 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 12345 literals 92%
c [treelook-1] scheduling used 300031 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300087 steps
c [treelook-1] 9565 literals remain 71%
c [treelook-1] 6649 variables remain to probed next time 99%
c [treelook-1] removed 0 variables, found 55 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 761 sched 11%, 0 failed, 0 lifted, 38 hbrs
c [basicprobe-1-1] 770 sched 11%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-1-2] 769 sched 11%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] removed 0 variables, found 39 hbrs
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 6744 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 313 not tried 5% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 33 = 0% variables out of 6744 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 71756 negative 99.1% of 72395 except 639 0.9%
c [phase-count-2] 69699 positive 96.3% of 72395 except 2696 3.7%
c [phase-count-2] less non-negative clauses 639 than limit 7200 (10.0%)
c [phase-count-2] non-pos/non-neg = 2696/639 = 4.22 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 3225 negative 100%
c [score-distribution-2] 1807 pos 26.93%, 0 min 0.00%, 4904 zero 73.07%
c [score-distribution-2] 921 different 13.72% out of total 6711 variables
c [simplification-2] removed 33 variables 0.5% (6711 remain 71%)
c [simplification-2] removed 129 irredundant clauses 0.2% (72395 remain 99%)
c [simplification-2] maximum reduction of 0% = max (0%, 0%)
c [simplification-2] full geometric conflict interval increment 20000
c [simplification-2] new conflict interval 20000
c [simplification-2] penalized conflict interval 20000 = 1 * 20000
c [simplification-2] hard conflict limit 31000 (soft 21000 + delta 10000)
c [simplification-2] new conflict limit 21000 (hard 31000)
c 
c [simplification-3] limit of 1272 ternary hit after 1272 ternaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3 at-most-one constraints of average size 3.0
c [card-2] found 30 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 33 out of 33 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 99 tauts, 0 hbrs, 159 literals
c [elim-3] 313 variables 5% will be scheduled this time
c [elim-3] scheduled 313 variables 5%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] no variable eliminated in round 1 in 3849539 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 313 scheduled
c [phase-count-3] 71746 negative 99.1% of 72391 except 645 0.9%
c [phase-count-3] 69677 positive 96.3% of 72391 except 2714 3.7%
c [phase-count-3] less non-negative clauses 645 than limit 7200 (10.0%)
c [phase-count-3] non-pos/non-neg = 2714/645 = 4.21 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 1128 negative 100%
c [score-distribution-3] 2893 pos 43.11%, 923 min 13.75%, 2895 zero 43.14%
c [score-distribution-3] 1406 different 20.95% out of total 6711 variables
c [simplification-3] removed 0 variables 0.0% (6711 remain 71%)
c [simplification-3] removed 4 irredundant clauses 0.0% (72391 remain 99%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] forced so keeping old conflict interval 20000
c [simplification-3] conflict limit remains at 21000 (hard 31000)
c [simplification-3] new ternary interval 10000
c 
c [simplification-4] limit 21000 conflicts (hard 31000) hit after 21001 conflicts
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 5083 literals 38%
c [treelook-2] scheduling used 150018 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150169 steps
c [treelook-2] 3808 literals remain 28%
c [treelook-2] 2864 variables remain to probed next time 43%
c [treelook-2] removed 0 variables, found 23 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 6711 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] eliminated 50 clauses out of 890 (6%) of length 6
c [cce-1-1] eliminated 9266 clauses out of 28914 (32%) of length 5
c [cce-1-1] eliminated 523 clauses out of 24915 (2%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 9839 large clauses in 12655424 steps
c [cce-1-1] allowing another 6327712 steps for small clauses
c [cce-1-1] scheduling 15482 clauses = 644 binary + 14838 ternary
c [cce-1-1] tried to eliminate 15482 small clauses 100%
c [cce-1-1] eliminated 20 binary clauses 3%
c [cce-1-1] eliminated 206 ternary clauses 1%
c [cce-1-1] eliminated 226 small clauses 1%
c [cce-1-1] eliminated 226 small clauses in 8599676 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 10065 covered clauses in round 1
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] allowing another 5639605 steps for small clauses
c [cce-1-2] scheduling 15256 clauses = 624 binary + 14632 ternary
c [cce-1-2] tried to eliminate 15256 small clauses 100%
c [cce-1-2] eliminated 1 binary clauses 0%
c [cce-1-2] eliminated 1 small clauses 0%
c [cce-1-2] eliminated 1 small clauses in 7972706 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 1 covered clauses in round 2
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] allowing another 6380395 steps for small clauses
c [cce-1-3] scheduling 15255 clauses = 623 binary + 14632 ternary
c [cce-1-3] tried to eliminate 15255 small clauses 100%
c [cce-1-3] eliminated 1 binary clauses 0%
c [cce-1-3] eliminated 1 ternary clauses 0%
c [cce-1-3] eliminated 2 small clauses 0%
c [cce-1-3] eliminated 2 small clauses in 8938876 steps
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 2 covered clauses in round 3
c [cce-1] eliminated 10068 covered clauses in TOTAL during 3 rounds
c [bca-1] limit of 10000000 steps and 125146 added (scaled 2)
c [bca-1] 5003 out of 13424 literals actually usable 37%
c [bca-1] added 0 blocked clauses in 35423 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2996 pos 44.6% + 3715 neg 55.4% = 6711 sched 100.0% ret 0
c [sweep-1-1] 1000508 steps 659 queries 433.19 avg class size
c [sweep-1-1] 12049 decisions 658 SAT calls 28.15 avg env size
c [sweep-1-1] 1128 variables remain 17% (5583 retained 83%)
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 0 vars in TOTAL (1 rounds, 658 queries)
c [phase-count-4] 61713 negative 99.0% of 62323 except 610 1.0%
c [phase-count-4] 59620 positive 95.7% of 62323 except 2703 4.3%
c [phase-count-4] less non-negative clauses 610 than limit 6200 (10.0%)
c [phase-count-4] non-pos/non-neg = 2703/610 = 4.43 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 100 negative 100%
c [score-distribution-4] 3790 pos 56.47%, 1411 min 21.03%, 1510 zero 22.50%
c [score-distribution-4] 1649 different 24.57% out of total 6711 variables
c [simplification-4] removed 0 variables 0.0% (6711 remain 71%)
c [simplification-4] removed 10068 irredundant clauses 13.9% (62323 remain 85%)
c [simplification-4] maximum reduction of 14% = max (0%, 14%)
c [simplification-4] geometric conflict interval increment 1333 = 20000 / 15
c [simplification-4] new conflict interval 21333
c [simplification-4] penalized conflict interval 21333 = 1 * 21333
c [simplification-4] hard conflict limit 53000 (soft 42334 + delta 10666)
c [simplification-4] new conflict limit 42334 (hard 53000)
c 
c [simplification-5] limit 42334 conflicts (hard 53000) hit after 42335 conflicts
c [quatres-1] found 29961 quaternary clauses 47% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-1] added 4 double-self-subsuming ternary resolvents
c [quatres-1-2] added 1245 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1006 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 6711 free variables schedulable
c [ternres-1] 5258 ternary resolvents (28 bin, 5230 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 6468 xors of average arity 3.0
c [gauss-1] connected 19404 occurrences of 1547 variables (average 12.5)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] connected 2178 occurrences of 1547 variables (average 1.4)
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [transred-1] limit 1549558 with penalty 0 = 0 + 0
c [transred-1] removed 25 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 71 clauses out of 19563 (0%) of length 5
c [cce-2-1] eliminated 148 clauses out of 24397 (1%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 219 large clauses in 10580323 steps
c [cce-2-1] allowing another 5290161 steps for small clauses
c [cce-2-1] scheduling 15297 clauses = 637 binary + 14660 ternary
c [cce-2-1] tried to eliminate 15297 small clauses 100%
c [cce-2-1] eliminated 5 binary clauses 1%
c [cce-2-1] eliminated 8 ternary clauses 0%
c [cce-2-1] eliminated 13 small clauses 0%
c [cce-2-1] eliminated 13 small clauses in 7535641 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 232 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 5255570 steps for small clauses
c [cce-2-2] scheduling 15284 clauses = 632 binary + 14652 ternary
c [cce-2-2] tried to eliminate 15284 small clauses 100%
c [cce-2-2] completed small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 232 covered clauses in TOTAL during 2 rounds
c [cce-2] 232 < 1/100 * 62322 = 623 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 6711 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 309911640 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 20 variables 0% in round 1 in 16395530 steps
c [elim-4-1] backward subsumption/strengthening limit 16395500
c [elim-4-1-1] backward checking 118 touched variables 2%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 2 and strengthened 2 clauses in 66744 steps
c [elim-4-1] rescheduled 9 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 8367 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 20 = 0% variables out of 6711 scheduled
c [elim-4] 20 < 1/100 * 6711 = 67 considered unsuccessful
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 522 pos 46.4% + 603 neg 53.6% = 1125 sched 16.8% ret 5566
c [sweep-2-1] 398080 steps 401 queries 85.38 avg class size
c [sweep-2-1] 7653 decisions 401 SAT calls 28.91 avg env size
c [sweep-2-1] fully completed sweeping round
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2-2] 3126 pos 46.7% + 3565 neg 53.3% = 6691 sched 100.0% ret 0
c [sweep-2-2] 603256 steps 198 queries 652.51 avg class size
c [sweep-2-2] 7477 decisions 197 SAT calls 55.79 avg env size
c [sweep-2-2] 3385 variables remain 51% (3306 retained 49%)
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 0 vars in TOTAL (2 rounds, 597 queries)
c [phase-count-5] 61452 negative 99.0% of 62062 except 610 1.0%
c [phase-count-5] 59353 positive 95.6% of 62062 except 2709 4.4%
c [phase-count-5] less non-negative clauses 610 than limit 6200 (10.0%)
c [phase-count-5] non-pos/non-neg = 2709/610 = 4.44 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 3 negative 100%
c [score-distribution-5] 3810 pos 56.94%, 2234 min 33.39%, 647 zero 9.67%
c [score-distribution-5] 1604 different 23.97% out of total 6691 variables
c [simplification-5] removed 20 variables 0.3% (6691 remain 70%)
c [simplification-5] removed 261 irredundant clauses 0.4% (62062 remain 85%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 21333
c [simplification-5] new conflict interval 42666
c [simplification-5] penalized conflict interval 42666 = 1 * 42666
c [simplification-5] hard conflict limit 106334 (soft 85001 + delta 21333)
c [simplification-5] new conflict limit 85001 (hard 106334)
c 
c [simplification-6] limit 85001 conflicts (hard 106334) hit after 85001 conflicts
c [quatres-2] found 33071 quaternary clauses 43% in total
c [quatres-2-1] added 7 double-self-subsuming ternary resolvents
c [quatres-2-2] added 669 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1180 quaternary resolvents
c [ternres-2] limit 4509760 with penalty 0 = 0 + 0
c [ternres-2] all 6691 free variables schedulable
c [ternres-2] 731 ternary resolvents (9 bin, 722 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 563720 penalty 2 = 2 + 0
c [card-3] found 5 at-most-one constraints of average size 3.0
c [card-3] found 11 at-most-two constraints of average size 4.0
c [card-3] using previous limit 563720 for elimination
c [card-3] 16 out of 16 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 11274400 penalty 1 = 1 + 0
c [basicprobe-2-0] 1300 sched 19%, 0 failed, 0 lifted, 27 hbrs
c [basicprobe-2-1] 1310 sched 20%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-2-2] 1310 sched 20%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-2] fully completed probing
c [basicprobe-2-2] removed 0 variables, found 28 hbrs
c [bate-1] eliminated 1 asymmetric tautologies during probing
c [unhide-3] limit 225488 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 27 tauts, 0 hbrs, 1294 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 13 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 6691 variables 100%
c [block-2] limit of 25000000 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 [bca-2] limit of 10000000 steps and 124618 added (scaled 2)
c [bca-2] 1458 out of 13384 literals actually usable 11%
c [bca-2] added 0 blocked clauses in 77654 steps
c [phase-count-6] 61447 negative 99.0% of 62059 except 612 1.0%
c [phase-count-6] 59342 positive 95.6% of 62059 except 2717 4.4%
c [phase-count-6] less non-negative clauses 612 than limit 6200 (10.0%)
c [phase-count-6] non-pos/non-neg = 2717/612 = 4.44 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 3 negative 100%
c [score-distribution-6] 4031 pos 60.25%, 2159 min 32.27%, 501 zero 7.49%
c [score-distribution-6] 1956 different 29.23% out of total 6691 variables
c [simplification-6] removed 0 variables 0.0% (6691 remain 70%)
c [simplification-6] removed 3 irredundant clauses 0.0% (62059 remain 85%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 42666
c [simplification-6] new conflict interval 85332
c [simplification-6] penalized conflict interval 85332 = 1 * 85332
c [simplification-6] hard conflict limit 212999 (soft 170333 + delta 42666)
c [simplification-6] new conflict limit 170333 (hard 212999)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   28.5    6691    62059     99098   37257  16330   653    9   404   11   2%    795  126   10    6  177%
c -   50.4    6691    62059    166291   56318  17269   658   10   398   12   2%    942   42   10    8  119%
c 
c [simplification-7] limit 170333 conflicts (hard 212999) hit after 170333 conflicts
c [quatres-3] found 37543 quaternary clauses 38% in total
c [quatres-3-1] removed 5 duplicate quaternary clauses
c [quatres-3-1] added 11 double-self-subsuming ternary resolvents
c [quatres-3-2] added 429 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1045 quaternary resolvents
c [ternres-3] limit 12080426 with penalty 0 = 0 + 0
c [ternres-3] all 6691 free variables schedulable
c [ternres-3] 369 ternary resolvents (0 bin, 369 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1208042 penalty 1 = 1 + 0
c [gauss-2] extracted 3586 xors of average arity 3.0
c [gauss-2] connected 10758 occurrences of 1506 variables (average 7.1)
c [gauss-2] limit 1208042 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 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 3 transitive binary clauses
c [cce-3] limit of 30201065 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 84 clauses out of 19409 (0%) of length 5
c [cce-3-1] eliminated 235 clauses out of 24236 (1%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 319 large clauses in 12496156 steps
c [cce-3-1] allowing another 6248078 steps for small clauses
c [cce-3-1] scheduling 15276 clauses = 626 binary + 14650 ternary
c [cce-3-1] tried to eliminate 15276 small clauses 100%
c [cce-3-1] eliminated 5 binary clauses 1%
c [cce-3-1] eliminated 2 ternary clauses 0%
c [cce-3-1] eliminated 7 small clauses 0%
c [cce-3-1] eliminated 7 small clauses in 8815792 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 326 covered clauses in round 1
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] allowing another 6186507 steps for small clauses
c [cce-3-2] scheduling 15269 clauses = 621 binary + 14648 ternary
c [cce-3-2] tried to eliminate 15269 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 326 covered clauses in TOTAL during 2 rounds
c [cce-3] 326 < 1/100 * 62059 = 620 considered unsuccessful
c [sweep-3] limit 1812063 penalty 1 = 1 + 0
c [sweep-3-1] 1592 pos 47.0% + 1793 neg 53.0% = 3385 sched 50.6% ret 3306
c [sweep-3-1] 1031276 steps 646 queries 156.89 avg class size
c [sweep-3-1] 12412 decisions 646 SAT calls 32.49 avg env size
c [sweep-3-1] fully completed sweeping round
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-3-2] 3174 pos 47.4% + 3517 neg 52.6% = 6691 sched 100.0% ret 0
c [sweep-3-2] 785321 steps 245 queries 680.91 avg class size
c [sweep-3-2] 7121 decisions 244 SAT calls 49.87 avg env size
c [sweep-3-2] 3162 variables remain 47% (3529 retained 53%)
c [sweep-3-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (2 rounds, 889 queries)
c [phase-count-7] 61123 negative 99.0% of 61733 except 610 1.0%
c [phase-count-7] 59017 positive 95.6% of 61733 except 2716 4.4%
c [phase-count-7] less non-negative clauses 610 than limit 6100 (10.0%)
c [phase-count-7] non-pos/non-neg = 2716/610 = 4.45 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 2 negative 100%
c [score-distribution-7] 4665 pos 69.72%, 1612 min 24.09%, 414 zero 6.19%
c [score-distribution-7] 2075 different 31.01% out of total 6691 variables
c [simplification-7] removed 0 variables 0.0% (6691 remain 70%)
c [simplification-7] removed 326 irredundant clauses 0.5% (61733 remain 84%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 42666 = 85332 / 2
c [simplification-7] new conflict interval 127998
c [simplification-7] penalized conflict interval 127998 = 1 * 127998
c [simplification-7] hard conflict limit 362330 (soft 298331 + delta 63999)
c [simplification-7] new conflict limit 298331 (hard 362330)
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 -   70.9    6691    61733    227455   70529  18600   672   11   421   13   3%    992   30   11   10  120%
c -   87.5    6691    61733    286838   81621  18979   685   13   424   14   3%   1011   12   13   11  122%
c 
c [simplification-8] limit 298331 conflicts (hard 362330) hit after 298331 conflicts
c [quatres-4] found 41617 quaternary clauses 34% in total
c [quatres-4-1] removed 5 duplicate quaternary clauses
c [quatres-4-1] added 13 double-self-subsuming ternary resolvents
c [quatres-4-2] added 375 single-self-subsuming ternary resolvents
c [quatres-4-2] added 892 quaternary resolvents
c [ternres-4] limit 22064675 with penalty 0 = 0 + 0
c [ternres-4] all 6691 free variables schedulable
c [ternres-4] 254 ternary resolvents (2 bin, 252 trn)
c [ternres-4] fully completed ternary resolution
c [simpleprobe-3] 2985 schedulable variables 45%
c [simpleprobe-3] limit 44129350 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 63 hbrs, 0 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 44 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 6691 variables 100%
c [elim-5] limit of 110323377 steps penalty 2 = 2 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 2 variables 0% in round 1 in 16141591 steps
c [elim-5-1] backward subsumption/strengthening limit 16141500
c [elim-5-1-1] backward checking 26 touched variables 0%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 51325 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 2 = 0% variables out of 6691 scheduled
c [elim-5] 2 < 1/100 * 6691 = 66 considered unsuccessful
c [score-distribution-8] 5034 pos 75.26%, 1337 min 19.99%, 318 zero 4.75%
c [score-distribution-8] 2542 different 38.00% out of total 6689 variables
c [simplification-8] removed 2 variables 0.0% (6689 remain 70%)
c [simplification-8] removed 41 irredundant clauses 0.1% (61692 remain 84%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 127998
c [simplification-8] new conflict interval 255996
c [simplification-8] penalized conflict interval 255996 = 1 * 255996
c [simplification-8] hard conflict limit 682325 (soft 554327 + delta 127998)
c [simplification-8] new conflict limit 554327 (hard 682325)
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 -  103.0    6689    61692    346023   91376  19851   706   13   440   15   3%   1019   12   14   12  116%
c -  116.3    6689    61692    406139  100970  20114   709   14   446   16   3%   1022    5   15   13  115%
c -  129.7    6689    61692    466222  109608  20371   713   15   473   17   3%   1023   25   17   14  121%
c -  142.3    6689    61692    526971  117955  20587   715   16   454   17   4%   1024   -0   15   15  101%
c 
c [simplification-9] limit 554327 conflicts (hard 682325) hit after 554327 conflicts
c [quatres-5] found 46588 quaternary clauses 29% in total
c [quatres-5-1] removed 18 duplicate quaternary clauses
c [quatres-5-1] added 8 double-self-subsuming ternary resolvents
c [quatres-5-2] added 392 single-self-subsuming ternary resolvents
c [quatres-5-2] added 833 quaternary resolvents
c [ternres-5] limit 37730379 with penalty 0 = 0 + 0
c [ternres-5] all 6689 free variables schedulable
c [ternres-5] 258 ternary resolvents (8 bin, 250 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 14 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 6689 variables 100%
c [block-3] limit of 94325947 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 [bca-3] limit of 10000000 steps and 123884 added (scaled 2)
c [bca-3] 1170 out of 13380 literals actually usable 9%
c [bca-3] added 0 blocked clauses in 150154 steps
c [score-distribution-9] 5425 pos 81.10%, 963 min 14.40%, 301 zero 4.50%
c [score-distribution-9] 3308 different 49.45% out of total 6689 variables
c [simplification-9] removed 0 variables 0.0% (6689 remain 70%)
c [simplification-9] removed 0 irredundant clauses 0.0% (61692 remain 84%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 255996
c [simplification-9] new conflict interval 511992
c [simplification-9] penalized conflict interval 511992 = 1 * 511992
c [simplification-9] hard conflict limit 1322315 (soft 1066319 + delta 255996)
c [simplification-9] new conflict limit 1066319 (hard 1322315)
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 -  155.5    6689    61692    588313  126814  21357   711   17   480   18   3%   1024   20   15   16   94%
c -  168.5    6689    61692    650014  135408  21518   711   18   460   19   4%   1024   -6   19   17  116%
c -  181.6    6689    61692    711118  143408  21613   712   18   482   20   4%   1024   17   17   17  100%
c -  195.4    6689    61692    772164  150499  21709   713   19   461   20   4%   1024   -4   22   18  119%
c -  209.2    6689    61692    833922  158222  21813   714   19   479   21   4%   1024    9   19   19  104%
c -  222.9    6689    61692    895899  165776  21947   717   20   481   21   4%   1024    9   21   19  110%
c -  237.0    6689    61692    958259  173512  22082   717   20   481   22   4%   1024   10   22   19  115%
c -  251.5    6689    61692   1020063  180235  22184   718   20   474   22   4%   1024    1   19   19  100%
c 
c [simplification-10] limit 1066319 conflicts (hard 1322315) hit after 1073445 conflicts
c [quatres-6] found 52398 quaternary clauses 24% in total
c [quatres-6-1] removed 28 duplicate quaternary clauses
c [quatres-6-1] added 3 double-self-subsuming ternary resolvents
c [quatres-6-2] added 376 single-self-subsuming ternary resolvents
c [quatres-6-2] added 919 quaternary resolvents
c [ternres-6] limit 71819812 with penalty 0 = 0 + 0
c [ternres-6] all 6689 free variables schedulable
c [ternres-6] 279 ternary resolvents (4 bin, 275 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 4488738 penalty 3 = 3 + 0
c [card-4] found 3 at-most-one constraints of average size 3.0
c [card-4] found 21 at-most-two constraints of average size 4.0
c [card-4] using previous limit 4488738 for elimination
c [card-4] 24 out of 24 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 3590990 penalty 2 = 2 + 0
c [gauss-3] extracted 10441 xors of average arity 3.4
c [gauss-3] connected 35470 occurrences of 3066 variables (average 11.6)
c [gauss-3] limit 3590990 penalty 2 = 2 + 0
c [gauss-3] connected 9837 occurrences of 3066 variables (average 3.2)
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-4] limit 1795495 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 0 failed, 777 tauts, 0 hbrs, 31668 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 8 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 897747657 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 60 clauses out of 19203 (0%) of length 5
c [cce-4-1] eliminated 224 clauses out of 23971 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 284 large clauses in 10233194 steps
c [cce-4-1] allowing another 5116597 steps for small clauses
c [cce-4-1] scheduling 15329 clauses = 618 binary + 14711 ternary
c [cce-4-1] tried to eliminate 15329 small clauses 100%
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 284 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 5069250 steps for small clauses
c [cce-4-2] scheduling 15329 clauses = 618 binary + 14711 ternary
c [cce-4-2] tried to eliminate 15329 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 284 covered clauses in TOTAL during 2 rounds
c [cce-4] 284 < 1/100 * 61692 = 616 considered unsuccessful
c [sweep-4] limit 5386485 penalty 2 = 2 + 0
c [sweep-4-1] 1576 pos 49.8% + 1586 neg 50.2% = 3162 sched 47.3% ret 3527
c [sweep-4-1] 2535481 steps 363 queries 92.90 avg class size
c [sweep-4-1] 22856 decisions 363 SAT calls 225.92 avg env size
c [sweep-4-1] fully completed sweeping round
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4-2] 3273 pos 48.9% + 3416 neg 51.1% = 6689 sched 100.0% ret 0
c [sweep-4-2] 2862985 steps 339 queries 201.12 avg class size
c [sweep-4-2] 23057 decisions 338 SAT calls 281.48 avg env size
c [sweep-4-2] 210 variables remain 3% (6479 retained 97%)
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (2 rounds, 700 queries)
c [score-distribution-10] 5694 pos 85.12%, 979 min 14.64%, 16 zero 0.24%
c [score-distribution-10] 2919 different 43.64% out of total 6689 variables
c [simplification-10] removed 0 variables 0.0% (6689 remain 70%)
c [simplification-10] removed 284 irredundant clauses 0.5% (61408 remain 84%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 511992
c [simplification-10] conflict interval soft limit 1000000 reached
c [simplification-10] new conflict interval 1000000
c [simplification-10] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-10] hard conflict limit 2573445 (soft 2073445 + delta 500000)
c [simplification-10] new conflict limit 2073445 (hard 2573445)
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 -  268.3    6689    61408   1082994  188314  22385   717   20   466   23   4%   1024   -7   22   20  112%
c -  283.6    6689    61408   1145235  194254  22460   718   20   465   24   4%   1024   -6   20   20  100%
c -  299.2    6689    61408   1208422  200510  22503   718   21   471   24   4%   1024   -1   19   20   94%
c -  314.9    6689    61408   1272142  207179  22563   718   21   476   25   4%   1024    3   20   21   96%
c -  330.9    6689    61408   1336531  213889  22631   720   21   477   25   4%   1024    3   18   21   86%
c -  347.3    6689    61408   1401076  220326  22724   720   21   489   26   4%   1024    9   22   21  105%
c -  363.0    6689    61408   1466319  227239  22818   721   22   483   26   4%   1024    5   27   21  127%
c -  379.8    6689    61408   1531638  233086  22911   721   21   489   27   4%   1024    8   20   21   96%
c -  396.9    6689    61408   1598170  239672  23002   721   21   486   27   4%   1024    8   22   21  102%
c -  414.7    6689    61408   1665103  245232  23074   723   21   486   28   4%   1024    4   19   21   89%
c -  433.4    6689    61408   1733431  251474  23151   723   22   490   28   5%   1024    8   32   21  148%
c -  452.7    6689    61408   1802421  257058  23211   726   21   491   29   4%   1024    9   20   21   95%
c -  472.7    6689    61408   1873018  263386  23314   726   22   486   29   5%   1024    6   24   22  113%
c -  493.5    6689    61408   1944526  269945  23416   726   23   477   30   5%   1024   -4   25   22  117%
c -  514.6    6689    61408   2016515  276508  23485   727   22   484   30   5%   1024    2   23   22  105%
c 
c [simplification-11] limit 2073445 conflicts (hard 2573445) hit after 2073663 conflicts
c [quatres-7] found 59557 quaternary clauses 19% in total
c [quatres-7-1] removed 52 duplicate quaternary clauses
c [quatres-7-1] added 14 double-self-subsuming ternary resolvents
c [quatres-7-2] added 496 single-self-subsuming ternary resolvents
c [quatres-7-2] added 1068 quaternary resolvents
c [ternres-7] limit 152396480 with penalty 0 = 0 + 0
c [ternres-7] all 6689 free variables schedulable
c [ternres-7] 303 ternary resolvents (5 bin, 298 trn)
c [ternres-7] fully completed ternary resolution
c [treelook-3] limit 3809912 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 6067 literals 45%
c [treelook-3] scheduling used 1159771 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 3809912 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 683053 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 5 hbrs
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 3 transitive binary clauses
c [score-distribution-11] 5929 pos 88.64%, 760 min 11.36%, 0 zero 0.00%
c [score-distribution-11] 3451 different 51.59% out of total 6689 variables
c [simplification-11] removed 0 variables 0.0% (6689 remain 70%)
c [simplification-11] removed 0 irredundant clauses 0.0% (61408 remain 84%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1000000
c [simplification-11] new conflict interval 2000000
c [simplification-11] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-11] hard conflict limit 5073663 (soft 4073663 + delta 1000000)
c [simplification-11] new conflict limit 4073663 (hard 5073663)
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 -  537.3    6689    61408   2089254  283291  24382   735   22   478   31   5%   1024   -3   26   22  119%
c -  560.4    6689    61408   2162497  289071  24432   735   22   466   31   5%   1024  -12   19   22   85%
c -  583.5    6689    61408   2236928  295420  24480   735   23   486   32   5%   1024    9   25   22  112%
c -  607.4    6689    61408   2312113  301589  24540   736   24   475   32   5%   1024   -3   26   22  118%
c -  631.8    6689    61408   2387957  308080  24604   739   24   470   33   5%   1024   -7   27   22  118%
c -  657.4    6689    61408   2464373  314188  24683   740   22   480   34   5%   1024    2   18   23   80%
c -  682.6    6689    61408   2541494  320462  24741   740   22   471   34   5%   1024   -7   25   22  112%
c -  708.2    6689    61408   2619648  326932  24813   740   22   468   35   5%   1024  -10   27   22  121%
c -  735.0    6689    61408   2698718  333694  24897   742   21   506   35   4%   1024   27   25   22  111%
c -  762.5    6689    61408   2777898  339259  24962   745   23   458   36   5%   1024  -22   22   22  101%
c -  790.9    6689    61408   2858774  345145  25045   745   22   485   36   4%   1024    5   26   22  116%
c -  820.5    6689    61408   2940737  351517  25088   746   23   474   37   5%   1024   -6   24   23  108%
c -  850.2    6689    61408   3023338  357899  25129   747   23   478   37   5%   1024   -3   24   22  107%
c -  880.6    6689    61408   3107129  364438  25217   747   22   487   38   4%   1024   14   19   22   85%
c -  912.4    6689    61408   3191482  370851  25273   747   23   476   38   5%   1024   -2   22   23   99%
c -  944.4    6689    61408   3276576  378134  25326   748   23   488   39   5%   1024    8   26   23  112%
c -  976.5    6689    61408   3361316  384004  25389   749   23   471   40   5%   1024   -8   24   23  103%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 1 basic ate = 1 trn 100% + 0 lrg 0% in 1 updates
c bcas: 3 count, 0 added (0 skipped), 263231 steps
c bkwd: tried 16055 clauses, 32066 lits, 2.00 lits/clause
c bkwd: checked 545957 occs, 34.01 occs/clause, 17.03 occs/lit
c bkwd: subsumed 0 binary, 19 ternary, 4 large
c bkwd: strengthened 0 binary, 17 ternary (100% self), 18 large (0% self)
c blkd: 3 bces, 0 removed, 1755314 resolutions, 3703422 steps
c blkd: 5 blocking literals 0%, 0 pure
c bump: 3405702 bumped seen, 197850650 lits 58.1 on average
c card: 4 count, 1 units, 0 am1, 8919000 steps
c card: 42 rescheduled, 218 eliminated, 22546 resolved, 1967 subsumed
c card: 12 at-most-one constraints found, average size 3.00
c card: 12 at-most-one constraints used 100%, average size 3.00
c card: 182 at-most-two constraints found, average size 4.00
c card: 182 at-most-two constraints used 100%, average size 4.00
c cces: 4 cces, 10910 eliminated, 10907 ate 100%, 3 abce 0%
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: 361948 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 41 gcs, 0 rescored clauses, 1791 rescored vars
c dcps: 28 decompositions, 20 equivalent 0%
c deco: 341 decision-only clauses 0%, 40% reduction
c decs: 37746137 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 126197692 push, 126188198 pop (126188198 dec 100%)
c dsch: 2028671675 swaps, 0 down, 501578422 up
c elms: 5 elims, 2803 eliminated 29%, 0 pure 0%
c elms: 10 rounds, 2.0 rounds/bve
c elms: 2803 small 100%, 0 large 0%
c elms: 18565 tried small, 2803 succeeded 15%, 15762 failed 85%
c elms: 227 subsumed, 195 strengthened, 0 blocked
c elms: 1496964 copies, 2868975 resolutions, 1801437 ipos
c elms: 53902 subchks, 48779 strchks
c gaus: 3 extractions, 20495 extracted, 3.2 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 2 gc, 13598118 steps, 6799059 extr 50%, 2517803 elim 19%
c glue: 19.8 orig avg, 19.8 real avg, 3.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 608 = 421 simple 69% + 180 trn 30% + 7 lrg 1%, 16 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3405702 clauses, 38.5 length
c lrnd: 131271752 lits = 138324089 orig - 7052337 removed 5%
c lrnd: 1579417 uips 46%, 1345401 flips 40%
c mins: 3119159 mins 92%, 90 bin 0%, 284811 size 8%
c mins: 111892336 poisoned searches, 8230463 hits, 7% hit rate
c mins: 225706460 used twice searches, 42405007 hits, 19% hit rate
c move: moved 294, 32 bin 11%, 262 trn 89%
c otfs: 19569 driving 47%, 22482 restarting 53%
c otfs: str 42051, 41217 red 98%, 834 irr 2%
c otfs: str 42051, 0 bin 0%, 406 trn 1%, 41645 lrg 99%
c otfs: sub 534, 534 red 100%, 0 irr 0%
c otfs: sub 534, 0 bin 0%, 102 trn 19%, 432 lrg 81%
c phas: 7 computed, 11205 set, 0 pos (0%), 11205 neg (100%)
c prbs: 2 basic, 12440 probed, 0 failed, 0 lifted
c prbs: 3 simple, 35202 probed, 0 failed, 19 eqs
c prbs: 3 treelook, 10122 probed, 0 failed, 0 lifted
c prom: 335887 locked 28% out of 1185871 tried
c prps: 660714498 props, 17 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 7 count, 6943 quat, 3982 self1, 60 self2, 111 dup
c redc: 3368 clauses 0%, 706528 tried 21%, 0 sat 0%
c redc: 3456 lits 0%, 5737114 tried 4%, 0 sat 0%
c redc: 130 times jump level reduced, 15.9 levels on average
c reds: 48 count, 71336.0 conflicts per reduce
c reds: 0 memlim 0%, 48 arith 100%
c reds: 1722517 collected 59%, 1208131 retired 41%
c rmbd: 65 removed, 65 red 100%
c rsts: 36988 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: 11 count, 10 confs 91%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 1 trns 9%
c subl: 3405702 count (3352106 tried 1.0), 14967 sub out of 3393302 (0.4%)
c swps: 4 count, 7 rounds, 2844 queries (406.3/round)
c swps: 2847 sat calls, 3 unsat (0.4% success rate)
c swps: 92625 decisions 32.5, 1141 conflicts 0.4
c swps; 288.0 avg class size, 88.3 avg environment size
c swps: 0 failed, 3 impls, 0 equivs
c swp0: 945 type 0 queries, 6 unsat (0.6%), 945 sat (100.0%)
c swp1: 1899 type 1 queries, 90 unsat (4.7%), 1899 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: 82307469 calls to obtain time
c tops: 12 fixed 0%, 0 its, 0.00 confs/it
c trds: 7 transitive reductions, 110 removed, 0 failed
c trds: 93569 nodes, 9177 edges, 14347 steps
c trim: 121417 words, 0.5 MB
c trnr: 7 count, 56 bin, 7396 trn, 35945825 steps
c unhd: 4 count, 4 rounds, 2668840 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: 987 tauts, 1 bin 0%, 812 trn 82%, 162 lrg 16%
c unhd: 987 tauts, 12 stamp 1%, 943 red 96%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 33185 str, 0 bin 0%, 95 trn 0%, 33090 lrg 100%, 33070 red 100%
c vars: 6689 remaining 70% and 2835 removed 30% out of 9524
c vars: 12 fixed 0%, 2803 eliminated 29%, 20 equivalent 0%
c vsts: 29105117076 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 44.1 search visits per propagation, 8497.5 per conflict
c wchs: 9587382727 pushed, 16163016 enlarged, 1026 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3400245       1722517       1208131     188094572      26002753       1622245
c 
c  0 0        378746  11       505   0         0   0 171862656  91< 21794659  84<  1361351  84<   11.6
c  1 5        262785   8    130776   8    115278  10   8761837   5   1423007   5     96351   6     0.6
c  2 6        692127  20    360445  21    311562  26   3848427   2    971236   4     61132   4     1.0
c  3 9        658375  19<   365748  21    276627  23   1431046   1    623956   2     33350   2     1.3
c  4 14       466598  14    277656  16<   177294  15<   835147   0    424206   2     22934   1     1.4
c  5 21       309674   9    190398  11    111008   9    492023   0    268380   1     14857   1     1.5
c  6 30       210425   6    131857   8     72840   6    306274   0    173297   1      9912   1     1.6
c  7 41       146081   4     93285   5     48853   4    200515   0    117089   0      7246   0     1.6
c  8 54       102062   3     65408   4     33535   3    135269   0     79772   0      5086   0     1.6
c  9 69        69738   2     44699   3     22799   2     90538   0     53538   0      3650   0     1.5
c 10 86        75659   2     46844   3     26294   2     96323   0     55848   0      4545   0     2.6
c 11 126       27173   1     14632   1     11609   1     33516   0     17345   0      1778   0     1.6
c 12 230         789   0       260   0       424   0       984   0       416   0        53   0     0.1
c 13 534          13   0         4   0         8   0        17   0         4   0         0   0     0.0
c 
c avg                  3.5           4.1           3.7           0.2           0.5           0.5
c std                  2.5           2.3           2.2           0.8           1.4           1.4
c 
c   40.458   4% decide
c   11.443   1% bump
c    2.432   0% elim
c 
c    5.262 < 1% rest (below)
c 
c    2.372   0% cce
c    1.220   0% sweep
c    1.179   0% quatres
c    0.919   0% probe
c    0.380   0% gauss
c    0.362   0% rescore
c    0.302   0% block
c    0.293   0% unhide
c    0.265   0% ternres
c    0.182   0% card
c    0.141   0% bca
c    0.018   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.761   0% preprocessing     7%
c   10.161   1% inprocessing     93%
c ==================================
c   10.922   1% simplifying
c  989.117  99% search
c ==================================
c 1000.040 100% all
c 
c       3424130 conflicts,        3424.0 confs/sec
c         12134 ternaries,         282.2 confs/ternary
c           119 binaries,        28774.2 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            48 reductions,          0.0 redus/sec,  71336.0 confs/reduction
c         36988 restarts,           37.0 rests/sec,     92.6 confs/restart
c      37746137 decisions,       37744.6 decis/sec,     11.0 decis/conflict
c     660714498 propagations,   660688.3 props/sec,     17.5 props/decision
c 
c 1000.0 seconds, 95.7 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
