c launch: /data/cnf/sc2014/app/atco_enc1_opt1_04_32.cnf.bz2
c host: atom19
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/atco_enc1_opt1_04_32.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc1_opt1_04_32.cnf.bz2
c no embedded options
c found 'p cnf 57220 582308' header
c read 57220 variables, 582308 clauses, 2299758 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 56935 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   56935   558589         0       0      0     0    0     0   28   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 11073 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 11073 out of 11073 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 12662 variables
c [simpleprobe-1] all 44558 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 1193 variables
c [simpleprobe-1] 40972 variables remain 94% (2393 retained 6%)
c [simpleprobe-1] removed 1193 variables, found 2439 hbrs, 72 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 1 units, 1962 failed, 1011 tauts, 0 hbrs, 2491 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 41348 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 4237 not tried 10% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 16178 = 39% variables out of 41348 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 441871 negative 90.9% of 486166 except 44295 9.1%
c [phase-count-1] 439494 positive 90.4% of 486166 except 46672 9.6%
c [phase-1] phase bias: 11954 positive 47%, 13216 negative 53%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 25170 zero 100.00%
c [score-distribution-1] 1 different 0.00% out of total 25170 variables
c [simplification-1] removed 31330 variables 55.5% (25170 remain 44%)
c [simplification-1] removed 72423 irredundant clauses 13.0% (486166 remain 87%)
c [simplification-1] maximum reduction of 55% = max (55%, 13%)
c [simplification-1] large reduction 55% >= 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 of 100 binary hit after 100 binaries
c [decomp-3] removed 2 variables
c [simpleprobe-2] 23927 schedulable variables 95%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 23940 variables remain 95% (1228 retained 5%)
c [simpleprobe-2] removed 0 variables, found 156 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 12333 literals 25%
c [treelook-1] scheduling used 306749 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 321146 steps
c [treelook-1] 12314 literals remain 24%
c [treelook-1] 11275 variables remain to probed next time 45%
c [treelook-1] removed 0 variables, found 70 hbrs
c [basicprobe-1] limit 3889312 based on 486164 irredundant clauses
c [basicprobe-1-0] 5229 probes remain 21% after last round
c [basicprobe-1-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 4 variables, found 4760 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 1340 tauts, 0 hbrs, 480 literals
c [elim-2] 4236 variables 17% will be scheduled this time
c [elim-2] scheduled 4236 variables 17%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 2590 not tried 10% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 87 = 2% variables out of 4236 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 444528 negative 91.6% of 485071 except 40543 8.4%
c [phase-count-2] 437890 positive 90.3% of 485071 except 47181 9.7%
c [phase-2] phase bias: 8 positive 67%, 4 negative 33%
c [score-distribution-2] 2697 pos 10.75%, 0 min 0.00%, 22380 zero 89.25%
c [score-distribution-2] 859 different 3.43% out of total 25077 variables
c [simplification-2] removed 93 variables 0.4% (25077 remain 44%)
c [simplification-2] removed 1095 irredundant clauses 0.2% (485071 remain 87%)
c [simplification-2] maximum reduction of 0% = max (0%, 0%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1000 (hard 11000)
c [simplification-2] new binary interval 1000
c 
c [simplification-3] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3444 at-most-one constraints of average size 3.6
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3444 out of 3444 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 133 variables
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 24944 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 4076 not tried 16% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1505 = 6% variables out of 24944 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 441882 negative 91.5% of 483125 except 41243 8.5%
c [phase-count-3] 435613 positive 90.2% of 483125 except 47512 9.8%
c [phase-3] phase bias: 13 positive 68%, 6 negative 32%
c [score-distribution-3] 3170 pos 13.52%, 0 min 0.00%, 20269 zero 86.48%
c [score-distribution-3] 1178 different 5.03% out of total 23439 variables
c [simplification-3] removed 1638 variables 6.5% (23439 remain 41%)
c [simplification-3] removed 1946 irredundant clauses 0.4% (483125 remain 86%)
c [simplification-3] maximum reduction of 7% = max (7%, 0%)
c [simplification-3] large reduction 7% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-3] new conflict limit 3000 (hard 13000)
c 
c [simplification-4] limit 3000 conflicts (hard 13000) hit after 3001 conflicts
c [decomp-7] removed 13 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 6539 literals 14%
c [treelook-2] scheduling used 153575 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 152571 steps
c [treelook-2] 6528 literals remain 14%
c [treelook-2] 3958 variables remain to probed next time 17%
c [treelook-2] removed 0 variables, found 15 hbrs
c [unhide-3] limit 69935 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 2886 tauts, 0 hbrs, 533 literals
c [elim-4] 2451 variables 10% will be scheduled this time
c [elim-4] scheduled 2451 variables 10%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 501 not tried 2% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 9 = 0% variables out of 2451 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 439170 negative 91.5% of 480190 except 41020 8.5%
c [phase-count-4] 433908 positive 90.4% of 480190 except 46282 9.6%
c [phase-4] phase bias: 42 positive 91%, 4 negative 9%
c [score-distribution-4] 4674 pos 19.96%, 1 min 0.00%, 18742 zero 80.04%
c [score-distribution-4] 1920 different 8.20% out of total 23417 variables
c [simplification-4] removed 22 variables 0.1% (23417 remain 41%)
c [simplification-4] removed 2935 irredundant clauses 0.6% (480190 remain 86%)
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 10000
c [simplification-4] penalized conflict interval 10000 = 1 * 10000
c [simplification-4] hard conflict limit 23001 (soft 13001 + delta 10000)
c [simplification-4] new conflict limit 13001 (hard 23001)
c 
c [simplification-5] limit of 1676 ternary hit after 1676 ternaries
c [quatres-1] found 73930 quaternary clauses 25% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 89 single-self-subsuming ternary resolvents
c [quatres-1-2] added 37 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 23417 free variables schedulable
c [ternres-1] 5981 ternary resolvents (0 bin, 5981 trn)
c [ternres-1] 132 variables remain 1% (23285 retained 99%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 315 xors of average arity 2.9
c [gauss-1] connected 903 occurrences of 790 variables (average 1.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 66 variables
c [basicprobe-2] limit 11679678 penalty 0 = 0 + 0
c [basicprobe-2-0] 4841 sched 21%, 2 failed, 0 lifted, 9909 hbrs
c [decomp-10] removed 665 variables
c [basicprobe-2-1] 2994 probes remain 13% after last round
c [basicprobe-2-1] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-2-1] removed 665 variables, found 12281 hbrs
c [bate-1] eliminated 148 asymmetric tautologies during probing
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 3127 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 22686 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 22621 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 10 clauses out of 23 (43%) of length 18
c [cce-1-1] eliminated 2 clauses out of 14 (14%) of length 17
c [cce-1-1] eliminated 8 clauses out of 129 (6%) of length 15
c [cce-1-1] eliminated 4 clauses out of 188 (2%) of length 14
c [cce-1-1] eliminated 5 clauses out of 3933 (0%) of length 12
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 29 large clauses in 30000366 steps
c [cce-1-1] allowing another 15000183 steps for small clauses
c [cce-1-1] scheduling 157293 clauses = 44518 binary + 112775 ternary
c [cce-1-1] tried to eliminate 1684 small clauses 1%
c [cce-1-1] eliminated 47 binary clauses 0%
c [cce-1-1] eliminated 108 ternary clauses 0%
c [cce-1-1] eliminated 155 small clauses 0%
c [cce-1-1] eliminated 155 small clauses in 30000024 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 184 covered clauses in round 1
c [cce-1] eliminated 184 covered clauses in TOTAL during 1 rounds
c [cce-1] 184 < 1/100 * 456426 = 4564 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 22686 variables 100%
c [elim-5] limit of 46718712 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 1869 not tried 8% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1725 = 8% variables out of 22686 scheduled
c [bca-1] limit of 10000000 steps and 902320 added (scaled 2)
c [bca-1] 36652 out of 41924 literals actually usable 87%
c [bca-1] added 1584 blocked clauses in 126947 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 8559 pos 40.8% + 12402 neg 59.2% = 20961 sched 100.0% ret 0
c [sweep-1-1] 1006318 steps 54 queries 3441.81 avg class size
c [sweep-1-1] 1519 decisions 51 SAT calls 74.35 avg env size
c [sweep-1-1] 20570 variables remain 98% (391 retained 2%)
c [decomp-11] removed 166 variables
c [sweep-1-1] removed 166 vars (0 failed, 6 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 166 vars in TOTAL (1 rounds, 53 queries)
c [phase-count-5] 410223 negative 91.0% of 450909 except 40686 9.0%
c [phase-count-5] 414337 positive 91.9% of 450909 except 36572 8.1%
c [phase-5] phase bias: 30 positive 94%, 2 negative 6%
c [score-distribution-5] 3947 pos 18.98%, 2422 min 11.65%, 14426 zero 69.37%
c [score-distribution-5] 1836 different 8.83% out of total 20795 variables
c [simplification-5] removed 2622 variables 11.2% (20795 remain 37%)
c [simplification-5] removed 29281 irredundant clauses 6.1% (450909 remain 81%)
c [simplification-5] maximum reduction of 11% = max (11%, 6%)
c [simplification-5] forced so keeping old conflict interval 10000
c [simplification-5] conflict limit remains at 13001 (hard 23001)
c [simplification-5] new ternary interval 10000
c 
c [simplification-6] limit 13001 conflicts (hard 23001) hit after 13001 conflicts
c [quatres-2] found 71139 quaternary clauses 24% in total
c [quatres-2-1] removed 7 duplicate quaternary clauses
c [quatres-2-2] added 13 single-self-subsuming ternary resolvents
c [quatres-2-2] added 3 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 128 schedulable variables 1%
c [ternres-2] 383 ternary resolvents (0 bin, 383 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 1576 at-most-one constraints of average size 3.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 1576 out of 1576 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 46 variables
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 1471 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 20749 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 216 blocked clauses
c [block-2] 216 < 1/100 * 450311 = 4503 considered unsuccessful
c [elim-6] 374 variables 2% will be scheduled this time
c [elim-6] scheduled 374 variables 2%
c [elim-6] limit of 58578798 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 323 not tried 2% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 374 scheduled
c [bca-2] limit of 10000000 steps and 901482 added (scaled 2)
c [bca-2] 35112 out of 41500 literals actually usable 85%
c [bca-2] added 468 blocked clauses in 124356 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 8244 pos 40.5% + 12117 neg 59.5% = 20361 sched 98.1% ret 388
c [sweep-2-1] 1001802 steps 67 queries 4131.81 avg class size
c [sweep-2-1] 1648 decisions 65 SAT calls 61.82 avg env size
c [sweep-2-1] 19972 variables remain 96% (777 retained 4%)
c [decomp-13] removed 8 variables
c [sweep-2-1] removed 8 vars (0 failed, 2 eqs, 2 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 8 vars in TOTAL (1 rounds, 66 queries)
c [phase-count-6] 409414 negative 91.0% of 450095 except 40681 9.0%
c [phase-count-6] 413663 positive 91.9% of 450095 except 36432 8.1%
c [phase-6] phase bias: 4 positive 100%, 0 negative 0%
c [score-distribution-6] 4408 pos 21.25%, 2271 min 10.95%, 14062 zero 67.80%
c [score-distribution-6] 2093 different 10.09% out of total 20741 variables
c [simplification-6] removed 54 variables 0.3% (20741 remain 36%)
c [simplification-6] removed 814 irredundant clauses 0.2% (450095 remain 81%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 20000
c [simplification-6] new conflict interval 30000
c [simplification-6] penalized conflict interval 30000 = 1 * 30000
c [simplification-6] hard conflict limit 58001 (soft 43001 + delta 15000)
c [simplification-6] new conflict limit 43001 (hard 58001)
c 
c [simplification-7] limit 43001 conflicts (hard 58001) hit after 43001 conflicts
c [quatres-3] found 72386 quaternary clauses 24% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 5 single-self-subsuming ternary resolvents
c [quatres-3-2] added 38 quaternary resolvents
c [ternres-3] limit 9977896 with penalty 0 = 0 + 0
c [ternres-3] all 20741 free variables schedulable
c [ternres-3] 304 ternary resolvents (0 bin, 304 trn)
c [ternres-3] 10549 variables remain 51% (10192 retained 49%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 122 xors of average arity 2.6
c [gauss-2] connected 315 occurrences of 274 variables (average 1.1)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 133 variables
c [simpleprobe-3] 19574 schedulable variables 95%
c [simpleprobe-3] limit 19955793 penalty 1 = 1 + 0
c [decomp-15] removed 26 variables
c [simpleprobe-3] 17535 variables remain 85% (3047 retained 15%)
c [simpleprobe-3] removed 26 variables, found 1399 hbrs, 0 units
c [unhide-4] limit 498894 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 1772 tauts, 0 hbrs, 32955 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 1375 transitive binary clauses
c [cce-2] limit of 24944741 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 12472597 steps for small clauses
c [cce-2-1] scheduling 48377 clauses = 39704 binary + 8673 ternary
c [cce-2-1] tried to eliminate 1131 small clauses 2%
c [cce-2-1] eliminated 113 binary clauses 0%
c [cce-2-1] eliminated 2 ternary clauses 0%
c [cce-2-1] eliminated 115 small clauses 0%
c [cce-2-1] eliminated 115 small clauses in 24944752 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 115 covered clauses in round 1
c [cce-2] eliminated 115 covered clauses in TOTAL during 1 rounds
c [cce-2] 115 < 1/100 * 449077 = 4490 considered unsuccessful
c [bca-3] limit of 10000000 steps and 899450 added (scaled 2)
c [bca-3] 31458 out of 41166 literals actually usable 76%
c [bca-3] added 311 blocked clauses in 136055 steps
c [sweep-3] limit 2993369 penalty 0 = 0 + 0
c [sweep-3-1] 8292 pos 41.9% + 11516 neg 58.1% = 19808 sched 96.2% ret 774
c [sweep-3-1] 3237858 steps 109 queries 1524.87 avg class size
c [sweep-3-1] 3460 decisions 103 SAT calls 95.83 avg env size
c [sweep-3-1] 18431 variables remain 90% (2151 retained 10%)
c [decomp-16] removed 125 variables
c [sweep-3-1] removed 125 vars (0 failed, 8 eqs, 9 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 125 vars in TOTAL (1 rounds, 108 queries)
c [phase-count-7] 407672 negative 90.8% of 448955 except 41283 9.2%
c [phase-count-7] 412195 positive 91.8% of 448955 except 36760 8.2%
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [score-distribution-7] 3875 pos 18.94%, 5051 min 24.69%, 11531 zero 56.37%
c [score-distribution-7] 1773 different 8.67% out of total 20457 variables
c [simplification-7] removed 284 variables 1.4% (20457 remain 36%)
c [simplification-7] removed 1140 irredundant clauses 0.3% (448955 remain 80%)
c [simplification-7] maximum reduction of 1% = max (1%, 0%)
c [simplification-7] geometric conflict interval increment 15000 = 30000 / 2
c [simplification-7] new conflict interval 45000
c [simplification-7] penalized conflict interval 45000 = 1 * 45000
c [simplification-7] hard conflict limit 110501 (soft 88001 + delta 22500)
c [simplification-7] new conflict limit 88001 (hard 110501)
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 -   65.9   20457   448955     74524   19364   8806 13581   11    51   35  21%    690    2   11    6  176%
c 
c [simplification-8] limit 88001 conflicts (hard 110501) hit after 88072 conflicts
c [quatres-4] found 73630 quaternary clauses 24% in total
c [quatres-4-1] removed 13 duplicate quaternary clauses
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 14 single-self-subsuming ternary resolvents
c [quatres-4-2] added 8 quaternary resolvents
c [ternres-4] limit 22073138 with penalty 0 = 0 + 0
c [ternres-4] 10391 schedulable variables 51%
c [ternres-4] 479 ternary resolvents (0 bin, 479 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 26 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 800 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 20431 variables 100%
c [block-3] limit of 110365692 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 318 blocked clauses
c [block-3] 318 < 1/100 * 448557 = 4485 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 20431 variables 100%
c [elim-7] limit of 220731384 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 874 not tried 4% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 178 = 1% variables out of 20431 scheduled
c [elim-7] 178 < 1/100 * 20431 = 204 considered unsuccessful
c [bca-4] limit of 10000000 steps and 894725 added (scaled 2)
c [bca-4] 33371 out of 40508 literals actually usable 82%
c [bca-4] added 786 blocked clauses in 148621 steps
c [sweep-4] limit 6621941 penalty 0 = 0 + 0
c [sweep-4-1] 7676 pos 42.4% + 10443 neg 57.6% = 18119 sched 89.5% ret 2134
c [sweep-4-1] 6622416 steps 442 queries 651.57 avg class size
c [sweep-4-1] 9219 decisions 415 SAT calls 56.97 avg env size
c [sweep-4-1] 14558 variables remain 72% (5695 retained 28%)
c [decomp-18] removed 107 variables
c [sweep-4-1] removed 107 vars (0 failed, 40 eqs, 40 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 107 vars in TOTAL (1 rounds, 441 queries)
c [phase-count-8] 404508 negative 90.6% of 446511 except 42003 9.4%
c [phase-count-8] 409209 positive 91.6% of 446511 except 37302 8.4%
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [score-distribution-8] 4018 pos 19.94%, 5555 min 27.57%, 10573 zero 52.48%
c [score-distribution-8] 1839 different 9.13% out of total 20146 variables
c [simplification-8] removed 311 variables 1.5% (20146 remain 35%)
c [simplification-8] removed 2444 irredundant clauses 0.5% (446511 remain 80%)
c [simplification-8] maximum reduction of 2% = max (2%, 1%)
c [simplification-8] geometric conflict interval increment 15000 = 45000 / 3
c [simplification-8] new conflict interval 60000
c [simplification-8] penalized conflict interval 60000 = 1 * 60000
c [simplification-8] hard conflict limit 178072 (soft 148072 + delta 30000)
c [simplification-8] new conflict limit 148072 (hard 178072)
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 -  108.4   20146   446511    126834   27415   9076 13790   12    47   36  25%    874   -2   13    9  145%
c -  143.2   20146   446511    175737   33919   9282 13826   12    45   36  27%    953   -2   13   11  124%
c 
c [simplification-9] limit 148072 conflicts (hard 178072) hit after 177828 conflicts
c [quatres-5] found 74758 quaternary clauses 24% in total
c [quatres-5-1] removed 2 duplicate quaternary clauses
c [quatres-5-2] added 6 single-self-subsuming ternary resolvents
c [quatres-5-2] added 10 quaternary resolvents
c [ternres-5] limit 46436110 with penalty 0 = 0 + 0
c [ternres-5] all 20146 free variables schedulable
c [ternres-5] 300 ternary resolvents (0 bin, 300 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-19] removed 14 variables
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 718 transitive binary clauses
c [bca-5] limit of 10000000 steps and 894474 added (scaled 2)
c [bca-5] 33306 out of 40266 literals actually usable 83%
c [bca-5] added 229 blocked clauses in 154293 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 139308330 penalty 0 = 0 + 0
c [sweep-5-1] 6209 pos 42.9% + 8258 neg 57.1% = 14467 sched 71.9% ret 5665
c [sweep-5-1] 37808849 steps 4120 queries 100.58 avg class size
c [sweep-5-1] 72916 decisions 3289 SAT calls 56.89 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-20] removed 834 variables
c [sweep-5-1] removed 834 vars (0 failed, 845 eqs, 762 impls)
c [sweep-5-2] 8547 pos 44.3% + 10751 neg 55.7% = 19298 sched 100.0% ret 0
c [sweep-5-2] 45087475 steps 3957 queries 92.15 avg class size
c [sweep-5-2] 79155 decisions 3578 SAT calls 56.54 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-21] removed 219 variables
c [sweep-5-2] removed 219 vars (0 failed, 416 eqs, 285 impls)
c [sweep-5-3] 8506 pos 44.6% + 10573 neg 55.4% = 19079 sched 100.0% ret 0
c [sweep-5-3] 44521981 steps 3784 queries 43.49 avg class size
c [sweep-5-3] 75120 decisions 3451 SAT calls 55.57 avg env size
c [sweep-5-3] fully completed sweeping round
c [decomp-22] removed 123 variables
c [sweep-5-3] removed 123 vars (0 failed, 361 eqs, 165 impls)
c [sweep-5] removed 1176 vars in TOTAL (3 rounds, 11858 queries)
c [score-distribution-9] 3932 pos 20.74%, 6320 min 33.34%, 8704 zero 45.92%
c [score-distribution-9] 1753 different 9.25% out of total 18956 variables
c [simplification-9] removed 1190 variables 5.9% (18956 remain 33%)
c [simplification-9] removed 354 irredundant clauses 0.1% (446157 remain 80%)
c [simplification-9] maximum reduction of 6% = max (6%, 0%)
c [simplification-9] large reduction 6% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 189828 (soft 179828 + delta 10000)
c [simplification-9] new conflict limit 179828 (hard 189828)
c 
c [simplification-10] limit 179828 conflicts (hard 189828) hit after 179830 conflicts
c [quatres-6] found 74889 quaternary clauses 24% in total
c [quatres-6-1] removed 48 duplicate quaternary clauses
c [quatres-6-2] added 23 single-self-subsuming ternary resolvents
c [quatres-6-2] added 8 quaternary resolvents
c [ternres-6] limit 46873147 with penalty 0 = 0 + 0
c [ternres-6] all 18956 free variables schedulable
c [ternres-6] 69 ternary resolvents (0 bin, 69 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 2929571 penalty 3 = 3 + 0
c [card-4] found 3550 at-most-one constraints of average size 3.2
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2929571 for elimination
c [card-4] 3550 out of 3550 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 2343657 penalty 2 = 2 + 0
c [gauss-3] extracted 265 xors of average arity 2.4
c [gauss-3] connected 630 occurrences of 478 variables (average 1.3)
c [gauss-3] limit 2343657 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 3 variables
c [treelook-3] limit 1171828 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 25542 literals 67%
c [treelook-3] scheduling used 982070 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1171828 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 1179818 steps
c [treelook-3] 25526 literals remain 67%
c [treelook-3] 3160 variables remain to probed next time 17%
c [treelook-3] removed 0 variables, found 226 hbrs
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 2077 transitive binary clauses
c [cce-3] limit of 58591434 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 20
c [cce-3-1] eliminated 3 clauses out of 16 (19%) of length 18
c [cce-3-1] eliminated 7 clauses out of 17 (41%) of length 17
c [cce-3-1] eliminated 4 clauses out of 15 (27%) of length 16
c [cce-3-1] eliminated 26 clauses out of 95 (27%) of length 15
c [cce-3-1] eliminated 11 clauses out of 185 (6%) of length 14
c [cce-3-1] eliminated 20 clauses out of 190 (11%) of length 13
c [cce-3-1] eliminated 104 clauses out of 4454 (2%) of length 12
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 176 large clauses in 58591436 steps
c [cce-3-1] allowing another 29295718 steps for small clauses
c [cce-3-1] scheduling 144740 clauses = 37570 binary + 107170 ternary
c [cce-3-1] tried to eliminate 2852 small clauses 2%
c [cce-3-1] eliminated 106 binary clauses 0%
c [cce-3-1] eliminated 485 ternary clauses 0%
c [cce-3-1] eliminated 591 small clauses 0%
c [cce-3-1] eliminated 591 small clauses in 58591629 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 767 covered clauses in round 1
c [cce-3] eliminated 767 covered clauses in TOTAL during 1 rounds
c [cce-3] 767 < 1/100 * 444914 = 4449 considered unsuccessful
c [bca-6] limit of 10000000 steps and 890483 added (scaled 2)
c [bca-6] 29829 out of 37908 literals actually usable 79%
c [bca-6] added 1633 blocked clauses in 154264 steps
c [sweep-6] limit 14061944 penalty 0 = 0 + 0
c [sweep-6-1] 8421 pos 44.4% + 10532 neg 55.6% = 18953 sched 100.0% ret 0
c [sweep-6-1] 14401021 steps 759 queries 190.04 avg class size
c [sweep-6-1] 17693 decisions 738 SAT calls 62.66 avg env size
c [sweep-6-1] 11144 variables remain 59% (7809 retained 41%)
c [decomp-25] removed 52 variables
c [sweep-6-1] removed 52 vars (0 failed, 70 eqs, 30 impls)
c [sweep-6] removed 52 vars in TOTAL (1 rounds, 758 queries)
c [score-distribution-10] 3239 pos 17.14%, 7198 min 38.08%, 8464 zero 44.78%
c [score-distribution-10] 1531 different 8.10% out of total 18901 variables
c [simplification-10] removed 55 variables 0.3% (18901 remain 33%)
c [simplification-10] removed 2012 irredundant clauses 0.5% (444145 remain 80%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 60000
c [simplification-10] new conflict interval 120000
c [simplification-10] penalized conflict interval 120000 = 1 * 120000
c [simplification-10] hard conflict limit 359830 (soft 299830 + delta 60000)
c [simplification-10] new conflict limit 299830 (hard 359830)
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 -  178.0   18901   444145    220848   43451   8349 15152   13    38   36  33%    988   -8   13   12  112%
c -  197.8   18901   444145    262778   50306   8437 15174   13    37   37  34%   1005   -6   11   12   89%
c 
c [simplification-11] limit 299830 conflicts (hard 359830) hit after 299830 conflicts
c [quatres-7] found 75460 quaternary clauses 23% in total
c [quatres-7-1] removed 5 duplicate quaternary clauses
c [quatres-7-2] added 18 single-self-subsuming ternary resolvents
c [quatres-7-2] added 5 quaternary resolvents
c [ternres-7] limit 74259409 with penalty 0 = 0 + 0
c [ternres-7] all 18901 free variables schedulable
c [ternres-7] 75 ternary resolvents (0 bin, 75 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-26] removed 7 variables
c [basicprobe-3] limit 371297049 penalty 0 = 0 + 0
c [basicprobe-3-0] 3919 sched 21%, 2 failed, 0 lifted, 457 hbrs
c [decomp-27] removed 36 variables
c [basicprobe-3-1] 8789 sched 47%, 2 failed, 0 lifted, 334 hbrs
c [decomp-28] removed 11 variables
c [basicprobe-3-2] 8797 sched 47%, 0 failed, 0 lifted, 10 hbrs
c [basicprobe-3-3] 8797 sched 47%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-3-4] 8796 sched 47%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-5] 8796 sched 47%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-3-6] 8796 sched 47%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-6] fully completed probing
c [basicprobe-3-6] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-3-6] removed 47 variables, found 816 hbrs
c [bate-2] eliminated 126 asymmetric tautologies during probing
c [unhide-5] limit 1856485 with penalty 3 = 3 + 0
c [unhide-5-5] 0 units, 0 failed, 485 tauts, 0 hbrs, 17682 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 765 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 18847 variables 100%
c [block-4] limit of 185648524 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 295 blocked clauses
c [block-4] 295 < 1/100 * 441127 = 4411 considered unsuccessful
c [elim-8] 323 variables 2% will be scheduled this time
c [elim-8] scheduled 323 variables 2%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4000000000 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 683876389 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 323 scheduled
c [bca-7] limit of 10000000 steps and 880549 added (scaled 2)
c [bca-7] 29762 out of 37696 literals actually usable 79%
c [bca-7] added 337 blocked clauses in 200417 steps
c [sweep-7] limit 22277822 penalty 0 = 0 + 0
c [sweep-7-1] 5118 pos 46.1% + 5988 neg 53.9% = 11106 sched 58.9% ret 7741
c [sweep-7-1] 22281834 steps 1905 queries 113.62 avg class size
c [sweep-7-1] 35281 decisions 1738 SAT calls 50.56 avg env size
c [sweep-7-1] 2714 variables remain 14% (16133 retained 86%)
c [decomp-33] removed 67 variables
c [sweep-7-1] removed 67 vars (0 failed, 187 eqs, 47 impls)
c [sweep-7] removed 67 vars in TOTAL (1 rounds, 1904 queries)
c [score-distribution-11] 2909 pos 15.49%, 7709 min 41.05%, 8162 zero 43.46%
c [score-distribution-11] 1391 different 7.41% out of total 18780 variables
c [simplification-11] removed 121 variables 0.6% (18780 remain 33%)
c [simplification-11] removed 5387 irredundant clauses 1.2% (438758 remain 79%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 60000 = 120000 / 2
c [simplification-11] new conflict interval 180000
c [simplification-11] penalized conflict interval 180000 = 1 * 180000
c [simplification-11] hard conflict limit 569830 (soft 479830 + delta 90000)
c [simplification-11] new conflict limit 479830 (hard 569830)
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 -  229.9   18780   438758    300750   53967   8502 15359   14    45   38  32%   1013    2   15   13  117%
c -  246.3   18780   438758    338012   57257   8524 15361   15    37   39  40%   1018   -4   15   14  114%
c -  262.6   18780   438758    375044   59757   8560 15363   15    41   39  36%   1021    1   15   14  105%
c -  277.7   18780   438758    412667   63096   8596 15366   15    41   39  37%   1022    2   16   14  115%
c -  290.4   18780   438758    451270   67025   8655 15368   12    44   40  26%   1023    4   12   14   89%
c -  307.0   18780   438758    488287   68353   8672 15368   15    31   40  50%   1023   -8   15   15  100%
c 
c [simplification-12] limit 479830 conflicts (hard 569830) hit after 495388 conflicts
c [quatres-8] found 76263 quaternary clauses 23% in total
c [quatres-8-1] removed 18 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 9 single-self-subsuming ternary resolvents
c [quatres-8-2] added 5 quaternary resolvents
c [ternres-8] limit 117364949 with penalty 0 = 0 + 0
c [ternres-8] all 18780 free variables schedulable
c [ternres-8] 51 ternary resolvents (0 bin, 51 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-34] removed 2 variables
c [simpleprobe-4] 15944 schedulable variables 85%
c [simpleprobe-4] limit 200000000 penalty 0 = 0 + 0
c [decomp-35] removed 173 variables
c [simpleprobe-4] 8011 variables remain 43% (10594 retained 57%)
c [simpleprobe-4] removed 173 variables, found 3925 hbrs, 0 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2455 transitive binary clauses
c [bca-8] limit of 10000000 steps and 878716 added (scaled 2)
c [bca-8] 29770 out of 37212 literals actually usable 80%
c [bca-8] added 98 blocked clauses in 190092 steps
c [sweep-8] limit 35209484 penalty 0 = 0 + 0
c [sweep-8-1] 1495 pos 56.0% + 1175 neg 44.0% = 2670 sched 14.4% ret 15935
c [sweep-8-1] 12254343 steps 1261 queries 33.11 avg class size
c [sweep-8-1] 33587 decisions 1221 SAT calls 73.43 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-36] removed 34 variables
c [sweep-8-1] removed 34 vars (0 failed, 47 eqs, 26 impls)
c [sweep-8-2] 8247 pos 44.4% + 10324 neg 55.6% = 18571 sched 100.0% ret 0
c [sweep-8-2] 23063169 steps 1090 queries 124.20 avg class size
c [sweep-8-2] 24943 decisions 1073 SAT calls 60.48 avg env size
c [sweep-8-2] 8794 variables remain 47% (9777 retained 53%)
c [decomp-37] removed 50 variables
c [sweep-8-2] removed 50 vars (0 failed, 63 eqs, 33 impls)
c [sweep-8] removed 84 vars in TOTAL (2 rounds, 2349 queries)
c [score-distribution-12] 2871 pos 15.50%, 7751 min 41.85%, 7899 zero 42.65%
c [score-distribution-12] 1482 different 8.00% out of total 18521 variables
c [simplification-12] removed 259 variables 1.4% (18521 remain 33%)
c [simplification-12] removed 1003 irredundant clauses 0.2% (437755 remain 78%)
c [simplification-12] maximum reduction of 1% = max (1%, 0%)
c [simplification-12] geometric conflict interval increment 90000 = 180000 / 2
c [simplification-12] new conflict interval 270000
c [simplification-12] penalized conflict interval 270000 = 1 * 270000
c [simplification-12] hard conflict limit 900388 (soft 765388 + delta 135000)
c [simplification-12] new conflict limit 765388 (hard 900388)
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 -  327.2   18521   437755    525377   70241   8692 16977   16    35   39  46%   1024   -3   17   15  112%
c -  342.6   18521   437755    564862   73455   8720 16977   16    43   39  37%   1024    4   18   15  117%
c -  359.1   18521   437755    603491   75749   8731 16977   17    37   39  44%   1024    1   17   15  110%
c -  374.9   18521   437755    642803   77233   8750 16977   16    40   39  41%   1024    2   15   15   96%
c -  392.5   18521   437755    683360   79679   8769 16977   16    37   40  44%   1024   -1   16   16   99%
c -  410.2   18521   437755    723768   81985   8785 16977   16    33   40  48%   1024   -5   15   16   93%
c 1  418.9   18521   437755    744786  102322   8799 16981   17    55   47  30%   1024   17   11   16   67%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s SATISFIABLE
c
c bate: 274 basic ate = 24 trn 9% + 250 lrg 91% in 2 updates
c bcas: 8 count, 5446 added (170 skipped), 1235045 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, 23450 removed, 8670645 resolutions, 27982844 steps
c blkd: 9433 blocking literals 8%, 0 pure
c bump: 748194 bumped seen, 39992005 lits 53.5 on average
c card: 4 count, 0 units, 0 am1, 14780613 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 44080 subsumed
c card: 19643 at-most-one constraints found, average size 3.16
c card: 19643 at-most-one constraints used 100%, average size 3.16
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: 3 cces, 1066 eliminated, 562 ate 53%, 504 abce 47%
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: 2882066 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 51 gcs, 0 rescored clauses, 393 rescored vars
c dcps: 37 decompositions, 16126 equivalent 28%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 3139670 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 9499956 push, 9461256 pop (9461256 dec 100%)
c dsch: 198062585 swaps, 0 down, 68982309 up
c elms: 8 elims, 19682 eliminated 34%, 427 pure 2%
c elms: 8 rounds, 1.0 rounds/bve
c elms: 14259 small 72%, 4996 large 25%
c elms: 20892 tried small, 14259 succeeded 68%, 6633 failed 32%
c elms: 9369 subsumed, 10646 strengthened, 0 blocked
c elms: 4228831 copies, 5366515 resolutions, 398418 ipos
c elms: 11420492 subchks, 2626413 strchks
c gaus: 3 extractions, 702 extracted, 2.6 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10692200 steps, 5346100 extr 50%, 7446 elim 0%
c glue: 13.6 orig avg, 13.6 real avg, 3.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 30124 = 7919 simple 26% + 22086 trn 73% + 119 lrg 0%, 1940 sub 6%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 748194 clauses, 28.0 length
c lrnd: 20970085 lits = 25952102 orig - 4982017 removed 19%
c lrnd: 273153 uips 37%, 396965 flips 53%
c mins: 734206 mins 98%, 765 bin 0%, 13223 size 2%
c mins: 22195090 poisoned searches, 2950948 hits, 13% hit rate
c mins: 44365672 used twice searches, 5937630 hits, 13% hit rate
c move: moved 21019, 9338 bin 44%, 11681 trn 56%
c otfs: 4854 driving 43%, 6446 restarting 57%
c otfs: str 11300, 10594 red 94%, 706 irr 6%
c otfs: str 11300, 0 bin 0%, 446 trn 4%, 10854 lrg 96%
c otfs: sub 60, 60 red 100%, 0 irr 0%
c otfs: sub 60, 0 bin 0%, 2 trn 3%, 58 lrg 97%
c phas: 8 computed, 25283 set, 12051 pos (48%), 13232 neg (52%)
c prbs: 3 basic, 145554 probed, 7 failed, 0 lifted
c prbs: 4 simple, 95533 probed, 72 failed, 1244 eqs
c prbs: 3 treelook, 46 probed, 0 failed, 0 lifted
c prom: 181396 locked 17% out of 1077113 tried
c prps: 712832107 props, 224 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 8 count, 114 quat, 177 self1, 2 self2, 557 dup
c redc: 14873 clauses 11%, 141409 tried 19%, 253 sat 0%
c redc: 19959 lits 1%, 1353184 tried 5%, 253 sat 0%
c redc: 630 times jump level reduced, 8.6 levels on average
c reds: 17 count, 43810.9 conflicts per reduce
c reds: 0 memlim 0%, 17 arith 100%
c reds: 492001 collected 80%, 120102 retired 20%
c rmbd: 8880 removed, 943 red 11%
c rsts: 22986 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: 12 count, 10 confs 83%, 0 vars 0%
c simp: 0 its 0%, 1 bin 8%, 1 trns 8%
c subl: 748194 count (372329 tried 0.5), 21863 sub out of 740167 (3.0%)
c swps: 8 count, 11 rounds, 17537 queries (1594.3/round)
c swps: 15722 sat calls, 230 unsat (0.5% success rate)
c swps: 354541 decisions 22.6, 8262 conflicts 0.5
c swps; 136.8 avg class size, 58.0 avg environment size
c swps: 0 failed, 1402 impls, 2045 equivs
c swp0: 5843 type 0 queries, 2240 unsat (38.3%), 5312 sat (90.9%)
c swp1: 11694 type 1 queries, 6008 unsat (51.4%), 10180 sat (87.1%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 7776734 calls to obtain time
c tops: 2891 fixed 5%, 0 its, 0.00 confs/it
c trds: 8 transitive reductions, 12788 removed, 0 failed
c trds: 302032 nodes, 386863 edges, 15040875 steps
c trim: 167227 words, 0.6 MB
c trnr: 8 count, 0 bin, 7642 trn, 144974073 steps
c unhd: 5 count, 5 rounds, 20691269 steps
c unhd: 360 non-trivial sccs of average size 2.0
c unhd: 1 units, 1 bin, 0 trn, 0 lrg
c unhd: 1962 failed, 1962 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 7494 tauts, 287 bin 4%, 560 trn 7%, 645 lrg 9%
c unhd: 7494 tauts, 6002 stamp 80%, 3618 red 48%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 54141 str, 1 bin 0%, 3311 trn 6%, 50829 lrg 94%, 49822 red 92%
c vars: 18521 remaining 32% and 38699 removed 68% out of 57220
c vars: 2891 fixed 5%, 19682 eliminated 34%, 16126 equivalent 28%
c vsts: 17771695462 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 24.9 search visits per propagation, 23532.8 per conflict
c wchs: 4032808686 pushed, 38220631 enlarged, 100 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         740281        492001        120102      19324101       5082187        356281
c 
c  0 0         59594   8      2945   1         0   0  12426595  64   2299850  45    151173  42     1.9
c  1 5         40447   5     18437   4      9604   8   2644280  14<   863366  17<    59861  17<    0.5
c  2 6        129761  18     83090  17     24416  20   2992349  15   1128668  22     91924  26     1.0
c  3 9        180966  24<   138764  28<    31732  26<   708027   4    406242   8     31714   9     1.2
c  4 14       183045  25    144287  29     28011  23    341094   2    235387   5     14270   4     2.1
c  5 21       116001  16     85411  17     19007  16    169137   1    120953   2      5865   2     2.0
c  6 30        27781   4     17601   4      6487   5     38952   0     25565   1      1333   0     0.7
c  7 41         2546   0      1389   0       802   1      3473   0      2038   0       126   0     0.1
c  8 54          114   0        60   0        39   0       158   0        93   0        12   0     0.0
c  9 69           26   0        17   0         4   0        36   0        25   0         3   0     0.0
c 
c avg                  3.2           3.5           3.4           0.7           1.2           1.2
c std                  1.5           1.2           1.4           1.1           1.4           1.3
c 
c   15.388   4% elim
c   11.897   3% sweep
c    7.962   2% probe
c    2.782   1% quatres
c    2.671   1% decide
c    2.084   0% block
c    1.936   0% cce
c    1.545   0% unhide
c    1.422   0% transred
c 
c    4.560 < 1% rest (below)
c 
c    1.352   0% bump
c    1.301   0% bca
c    0.889   0% ternres
c    0.518   0% gauss
c    0.251   0% card
c    0.248   0% rescore
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    1.981   0% preprocessing     4%
c   49.580  12% inprocessing     96%
c ==================================
c   51.561  12% simplifying
c  367.315  88% search
c ==================================
c  418.876 100% all
c 
c        744786 conflicts,        1778.1 confs/sec
c          4845 ternaries,         153.7 confs/ternary
c          1933 binaries,          385.3 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            17 reductions,          0.0 redus/sec,  43810.9 confs/reduction
c         22986 restarts,           54.9 rests/sec,     32.4 confs/restart
c       3139670 decisions,        7495.5 decis/sec,      4.2 decis/conflict
c     712832107 propagations,  1701773.7 props/sec,    227.0 props/decision
c 
c 418.9 seconds, 85.4 MB
c launch: done
