c launch: /data/cnf/sc2014/app/E02F20.cnf.bz2
c host: atom26
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 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 fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/E02F20.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/E02F20.cnf.bz2
c no embedded options
c found 'p cnf 10420 395383' header
c read 10420 variables, 395383 clauses, 2821910 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --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 10398 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 
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   10398   394921         0       0      0     0    0     0   29   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 20 at-most-one constraints of average size 5.0
c [card-1] found 129 at-most-two constraints of average size 5.3
c [card-1] using previous limit 2000000 for elimination
c [card-1] 149 out of 149 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 564 variables
c [simpleprobe-1] all 9856 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [simpleprobe-1] 4969 variables remain 50% (4887 retained 50%)
c [simpleprobe-1] removed 0 variables, found 7669 hbrs, 0 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 9856 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 868 variables 9% in round 1 in 1852274 steps
c [elim-1-1] backward subsumption/strengthening limit 1852200
c [elim-1-1-1] backward checking 9026 touched variables 92%
c [elim-1-1-1] incomplete backward checking 8962 remain 99%
c [elim-1-1] subsumed 0 and strengthened 0 clauses in 1861318 steps
c [elim-1-1] fully rescheduled 8988 variables 91%
c [elim-1-2] no variable eliminated in round 2 in 1029912 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 868 = 9% variables out of 9856 scheduled
c [phase-count-1] 374674 negative 95.7% of 391613 except 16939 4.3%
c [phase-count-1] 54937 positive 14.0% of 391613 except 336676 86.0%
c [phase-count-1] less non-negative clauses 16939 than limit 39100 (10.0%)
c [phase-count-1] non-pos/non-neg = 336676/16939 = 19.88 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 8988 negative 100%
c [sort-queue-1] sorted 8988 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 8988 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 948 variables 9.5% (8988 remain 86%)
c [simplification-1] removed 3308 irredundant clauses 0.8% (391613 remain 99%)
c [simplification-1] maximum reduction of 10% = max (10%, 1%)
c [simplification-1] large reduction 10% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6140 literals 34%
c [treelook-1] scheduling used 300100 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 303425 steps
c [treelook-1] 6101 literals remain 34%
c [treelook-1] 5875 variables remain to probed next time 65%
c [treelook-1] removed 2 variables, found 76 hbrs
c [basicprobe-1] limit 3132568 based on 391571 irredundant clauses
c [basicprobe-1-0] 6464 probes remain 72% after last round
c [basicprobe-1-0] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 3 variables, found 3225 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 8983 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 1763 blocked clauses
c [block-1] 1763 < 1/100 * 391571 = 3915 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] allowing another 15000064 steps for small clauses
c [cce-1-1] scheduling 31694 clauses = 23081 binary + 8613 ternary
c [cce-1-1] tried to eliminate 2170 small clauses 7%
c [cce-1-1] eliminated 1 binary clauses 0%
c [cce-1-1] eliminated 197 ternary clauses 2%
c [cce-1-1] eliminated 198 small clauses 1%
c [cce-1-1] eliminated 198 small clauses in 30000278 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 198 covered clauses in round 1
c [cce-1] eliminated 198 covered clauses in TOTAL during 1 rounds
c [cce-1] 198 < 1/100 * 389802 = 3898 considered unsuccessful
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 8983 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 1 variables 0% in round 1 in 2869302 steps
c [elim-2-1] backward subsumption/strengthening limit 2869300
c [elim-2-1-1] backward checking 23 touched variables 0%
c [elim-2-1-1] incomplete backward checking 23 remain 100%
c [elim-2-1] subsumed 18 and strengthened 46 clauses in 2879615 steps
c [elim-2-1] rescheduled 39 variables 0% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 812 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 1 = 0% variables out of 8983 scheduled
c [elim-2] 1 < 1/100 * 8983 = 89 considered unsuccessful
c [bca-1] limit of 10000000 steps and 779646 added (scaled 2)
c [bca-1] 15364 out of 17966 literals actually usable 86%
c [bca-1] added 0 blocked clauses in 37868 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 182 pos 2.0% + 8800 neg 98.0% = 8982 sched 100.0% ret 0
c [sweep-1-1] 1007858 steps 114 queries 446.39 avg class size
c [sweep-1-1] 1523 decisions 113 SAT calls 29.86 avg env size
c [sweep-1-1] 3954 variables remain 44% (5028 retained 56%)
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, 113 queries)
c [phase-count-2] 372637 negative 95.7% of 389573 except 16936 4.3%
c [phase-count-2] 53137 positive 13.6% of 389573 except 336436 86.4%
c [phase-count-2] less non-negative clauses 16936 than limit 38900 (10.0%)
c [phase-count-2] non-pos/non-neg = 336436/16936 = 19.87 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 1082 negative 100%
c [sort-queue-2] sorted 8982 enqueued variables after 1001 conflicts
c [score-dist-2] active 0 (0%), one 3805 (42%), zero 5177 (58%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 6 variables 0.1% (8982 remain 86%)
c [simplification-2] removed 2040 irredundant clauses 0.5% (389573 remain 99%)
c [simplification-2] maximum reduction of 1% = max (0%, 1%)
c [simplification-2] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-2] new conflict interval 10000
c [simplification-2] penalized conflict interval 10000 = 1 * 10000
c [simplification-2] hard conflict limit 21001 (soft 11001 + delta 10000)
c [simplification-2] new conflict limit 11001 (hard 21001)
c 
c [simplification-3] limit 11001 conflicts (hard 21001) hit after 11001 conflicts
c [quatres-1] found 13009 quaternary clauses 4% in total
c [quatres-1-2] added 1 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 8982 free variables schedulable
c [ternres-1] 13269 ternary resolvents (0 bin, 13269 trn)
c [ternres-1] 232 variables remain 3% (8750 retained 97%)
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 40 at-most-one constraints of average size 4.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 40 out of 40 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-2] 4538 schedulable variables 51%
c [simpleprobe-2] limit 1000000 penalty 1 = 1 + 0
c [simpleprobe-2] 4549 variables remain 51% (4433 retained 49%)
c [simpleprobe-2] removed 0 variables, found 30 hbrs, 0 units
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 1 units, 4 failed, 40 tauts, 0 hbrs, 6132 literals
c [transred-1] limit 445761 with penalty 0 = 0 + 0
c [transred-1] removed 4 transitive binary clauses
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 162 pos 4.1% + 3789 neg 95.9% = 3951 sched 44.0% ret 5027
c [sweep-2-1] 1100899 steps 78 queries 178.71 avg class size
c [sweep-2-1] 1664 decisions 77 SAT calls 55.23 avg env size
c [sweep-2-1] 1947 variables remain 22% (7031 retained 78%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 77 queries)
c [phase-count-3] 372625 negative 95.7% of 389561 except 16936 4.3%
c [phase-count-3] 53130 positive 13.6% of 389561 except 336431 86.4%
c [phase-count-3] less non-negative clauses 16936 than limit 38900 (10.0%)
c [phase-count-3] non-pos/non-neg = 336431/16936 = 19.86 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 554 negative 100%
c [sort-queue-3] sorted 8978 enqueued variables after 11001 conflicts
c [score-dist-3] active 0 (0%), one 5386 (60%), zero 3592 (40%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 4 variables 0.0% (8978 remain 86%)
c [simplification-3] removed 12 irredundant clauses 0.0% (389561 remain 99%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 30000
c [simplification-3] penalized conflict interval 30000 = 1 * 30000
c [simplification-3] hard conflict limit 56001 (soft 41001 + delta 15000)
c [simplification-3] new conflict limit 41001 (hard 56001)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    9.5    8977   389561     14279   13241  15836 10614   13    49   35  26%    187   42   14    3  534%
c i   12.3    8976   389561     25286   23743  16029 10622   14    50   38  28%    125   36   14    4  318%
c 
c [simplification-4] limit 41001 conflicts (hard 56001) hit after 41001 conflicts
c [quatres-2] found 13303 quaternary clauses 4% in total
c [quatres-2-2] added 5 single-self-subsuming ternary resolvents
c [quatres-2-2] added 2 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 232 schedulable variables 3%
c [ternres-2] 7925 ternary resolvents (0 bin, 7925 trn)
c [ternres-2] 152 variables remain 2% (8824 retained 98%)
c [decomp-9] removed 2 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 7599 literals 42%
c [treelook-2] scheduling used 300289 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 320639 steps
c [treelook-2] 7590 literals remain 42%
c [treelook-2] 5025 variables remain to probed next time 56%
c [unhide-3] limit 464686 with penalty 0 = 0 + 0
c [unhide-3-3] 5 units, 0 failed, 721 tauts, 0 hbrs, 29940 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 17 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 8971 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 4 blocked clauses
c [block-2] 4 < 1/100 * 389153 = 3891 considered unsuccessful
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 7500894 steps for small clauses
c [cce-2-1] scheduling 32687 clauses = 23053 binary + 9634 ternary
c [cce-2-1] tried to eliminate 959 small clauses 3%
c [cce-2-1] eliminated 2 binary clauses 0%
c [cce-2-1] eliminated 57 ternary clauses 1%
c [cce-2-1] eliminated 59 small clauses 0%
c [cce-2-1] eliminated 59 small clauses in 15000239 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 59 covered clauses in round 1
c [cce-2] eliminated 59 covered clauses in TOTAL during 1 rounds
c [cce-2] 59 < 1/100 * 389139 = 3891 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 8970 variables 100%
c [elim-3] limit of 23234306 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 67 variables 1% in round 1 in 13054347 steps
c [elim-3-1] backward subsumption/strengthening limit 10179959
c [elim-3-1-1] backward checking 1358 touched variables 15%
c [elim-3-1-1] incomplete backward checking 1031 remain 76%
c [elim-3-1] subsumed 0 and strengthened 4 clauses in 10180643 steps
c [elim-3] incomplete 59 not tried 1% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 67 = 1% variables out of 8970 scheduled
c [elim-3] 67 < 1/100 * 8970 = 89 considered unsuccessful
c [bca-2] limit of 10000000 steps and 778486 added (scaled 2)
c [bca-2] 11604 out of 17808 literals actually usable 65%
c [bca-2] added 0 blocked clauses in 51607 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 54 pos 2.8% + 1887 neg 97.2% = 1941 sched 21.8% ret 6962
c [sweep-3-1] 1001824 steps 47 queries 173.26 avg class size
c [sweep-3-1] 1549 decisions 46 SAT calls 95.22 avg env size
c [sweep-3-1] 1433 variables remain 16% (7469 retained 84%)
c [decomp-10] removed 1 variables
c [sweep-3-1] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 1 vars in TOTAL (1 rounds, 46 queries)
c [phase-count-4] 372054 negative 95.6% of 388991 except 16937 4.4%
c [phase-count-4] 52895 positive 13.6% of 388991 except 336096 86.4%
c [phase-count-4] less non-negative clauses 16937 than limit 38800 (10.0%)
c [phase-count-4] non-pos/non-neg = 336096/16937 = 19.84 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 434 negative 100%
c [sort-queue-4] sorted 8902 enqueued variables after 41001 conflicts
c [score-dist-4] active 0 (0%), one 5935 (67%), zero 2967 (33%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 74 variables 0.8% (8902 remain 86%)
c [simplification-4] removed 570 irredundant clauses 0.1% (388991 remain 98%)
c [simplification-4] maximum reduction of 1% = max (1%, 0%)
c [simplification-4] geometric conflict interval increment 15000 = 30000 / 2
c [simplification-4] new conflict interval 45000
c [simplification-4] penalized conflict interval 45000 = 1 * 45000
c [simplification-4] hard conflict limit 108501 (soft 86001 + delta 22500)
c [simplification-4] new conflict limit 86001 (hard 108501)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   22.4    8901   388991     43896   27114  24165 10750   15    51   39  29%    216   28   14    7  206%
c -   33.8    8901   388991     73702   14147  24446 10795   16    52   34  31%    324   18   16   10  153%
c 
c [simplification-5] limit 86001 conflicts (hard 108501) hit after 86003 conflicts
c [quatres-3] found 13635 quaternary clauses 4% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 7 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1 quaternary resolvents
c [ternres-3] limit 5865596 with penalty 0 = 0 + 0
c [ternres-3] 152 schedulable variables 2%
c [ternres-3] 6900 ternary resolvents (0 bin, 6900 trn)
c [ternres-3] 87 variables remain 1% (8814 retained 99%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-2] limit 29327982 penalty 0 = 0 + 0
c [basicprobe-2-0] 6381 sched 72%, 24 failed, 0 lifted, 14715 hbrs
c [decomp-12] removed 24 variables
c [basicprobe-2-1] 4454 probes remain 50% after last round
c [basicprobe-2-1] 27 units = 27 failed (100%) + 0 lifted (0%)
c [basicprobe-2-1] removed 27 variables, found 14762 hbrs
c [unhide-4] limit 1173119 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 0 failed, 481 tauts, 0 hbrs, 25240 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 70 transitive binary clauses
c [sweep-4] limit 1759678 penalty 0 = 0 + 0
c [sweep-4-1] 34 pos 2.4% + 1396 neg 97.6% = 1430 sched 16.1% ret 7444
c [sweep-4-1] 1833637 steps 47 queries 122.74 avg class size
c [sweep-4-1] 1235 decisions 46 SAT calls 95.28 avg env size
c [sweep-4-1] 901 variables remain 10% (7973 retained 90%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 46 queries)
c [phase-count-5] 371950 negative 95.6% of 388887 except 16937 4.4%
c [phase-count-5] 52827 positive 13.6% of 388887 except 336060 86.4%
c [phase-count-5] less non-negative clauses 16937 than limit 38800 (10.0%)
c [phase-count-5] non-pos/non-neg = 336060/16937 = 19.84 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 368 negative 100%
c [sort-queue-5] sorted 8874 enqueued variables after 86003 conflicts
c [score-dist-5] active 0 (0%), one 5951 (67%), zero 2923 (33%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 27 variables 0.3% (8874 remain 85%)
c [simplification-5] removed 104 irredundant clauses 0.0% (388887 remain 98%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 45000
c [simplification-5] new conflict interval 90000
c [simplification-5] penalized conflict interval 90000 = 1 * 90000
c [simplification-5] hard conflict limit 221003 (soft 176003 + delta 45000)
c [simplification-5] new conflict limit 176003 (hard 221003)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   52.5    8873   388887    111600   50707  31538 24836   16    52   45  31%    631   11   15   13  116%
c -   55.8    8856   388887    119404   17796  31564 24840   16    46   35  35%   -278    4   17   13  128%
c i   65.7    8855   388887    153599   50650  31703 24849   15    42   48  37%    251   -0   18   14  129%
c -   68.3    8855   388887    163706   24769  31729 24850   15    35   37  42%   -210   -6   12   14   83%
c 
c [simplification-6] limit 176003 conflicts (hard 221003) hit after 176003 conflicts
c [quatres-4] found 14200 quaternary clauses 4% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 16 single-self-subsuming ternary resolvents
c [quatres-4-2] added 8 quaternary resolvents
c [ternres-4] limit 13489203 with penalty 0 = 0 + 0
c [ternres-4] 87 schedulable variables 1%
c [ternres-4] 10059 ternary resolvents (0 bin, 10059 trn)
c [ternres-4] 32 variables remain 0% (8823 retained 100%)
c [card-3] limit 1686150 penalty 2 = 2 + 0
c [card-3] found 28 at-most-one constraints of average size 4.5
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1686150 for elimination
c [card-3] 28 out of 28 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-14] removed 21 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 37 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 40467610 penalty 0 = 0 + 0
c [sweep-5-1] 26 pos 2.9% + 873 neg 97.1% = 899 sched 10.2% ret 7954
c [sweep-5-1] 7178886 steps 175 queries 16.36 avg class size
c [sweep-5-1] 7694 decisions 170 SAT calls 188.51 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-15] removed 6 variables
c [sweep-5-1] removed 6 vars (0 failed, 5 eqs, 3 impls)
c [sweep-5-2] 287 pos 3.2% + 8560 neg 96.8% = 8847 sched 100.0% ret 0
c [sweep-5-2] 12577725 steps 282 queries 75.77 avg class size
c [sweep-5-2] 9254 decisions 277 SAT calls 133.30 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-16] removed 4 variables
c [sweep-5-2] removed 4 vars (0 failed, 4 eqs, 5 impls)
c [sweep-5-3] 287 pos 3.2% + 8556 neg 96.8% = 8843 sched 100.0% ret 0
c [sweep-5-3] 11791045 steps 284 queries 67.76 avg class size
c [sweep-5-3] 9898 decisions 283 SAT calls 159.69 avg env size
c [sweep-5-3] fully completed sweeping round
c [decomp-17] removed 17 variables
c [sweep-5-3] removed 17 vars (0 failed, 0 eqs, 3 impls)
c [sweep-5] removed 27 vars in TOTAL (3 rounds, 738 queries)
c [sort-queue-6] sorted 8826 enqueued variables after 176003 conflicts
c [score-dist-6] active 0 (0%), one 8493 (96%), zero 333 (4%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 29 variables 0.3% (8826 remain 85%)
c [simplification-6] removed 5976 irredundant clauses 1.5% (382911 remain 97%)
c [simplification-6] maximum reduction of 2% = max (0%, 2%)
c [simplification-6] geometric conflict interval increment 30000 = 90000 / 3
c [simplification-6] new conflict interval 120000
c [simplification-6] penalized conflict interval 120000 = 1 * 120000
c [simplification-6] hard conflict limit 356003 (soft 296003 + delta 60000)
c [simplification-6] new conflict limit 296003 (hard 356003)
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 -   83.5    8826   382911    201543   26766  41610 24818   16    46   37  36%    331    2   14   15   93%
c -   96.5    8826   382911    241318   29933  41718 24825   17    43   39  39%    646   -1   14   16   91%
c -  106.5    8826   382911    280740   34144  41793 24839   16    48   39  34%    817    6   15   16   97%
c i  109.8    8825   382911    295182   48028  41821 24842   16    48   47  32%    858    7   17   16  107%
c -  117.6    8825   382911    317686   34402  41870 24843   19    53   38  35%   -688   11   23   16  144%
c 
c [simplification-7] limit 296003 conflicts (hard 356003) hit after 351367 conflicts
c [quatres-5] found 14827 quaternary clauses 4% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 15 single-self-subsuming ternary resolvents
c [quatres-5-2] added 19 quaternary resolvents
c [ternres-5] limit 29339708 with penalty 0 = 0 + 0
c [ternres-5] 32 schedulable variables 0%
c [ternres-5] 5481 ternary resolvents (0 bin, 5481 trn)
c [ternres-5] 5 variables remain 0% (8820 retained 100%)
c [decomp-18] removed 2 variables
c [unhide-5] limit 1466985 with penalty 2 = 1 + 1
c [unhide-5-5] 2 units, 0 failed, 1725 tauts, 0 hbrs, 129486 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 38 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 8821 variables 100%
c [block-3] limit of 73349270 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 46 blocked clauses
c [block-3] 46 < 1/100 * 381494 = 3814 considered unsuccessful
c [cce-3] limit of 36674635 steps penalty 2 = 2 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 18337918 steps for small clauses
c [cce-3-1] scheduling 30897 clauses = 22598 binary + 8299 ternary
c [cce-3-1] tried to eliminate 2496 small clauses 8%
c [cce-3-1] eliminated 5 binary clauses 0%
c [cce-3-1] eliminated 184 ternary clauses 2%
c [cce-3-1] eliminated 189 small clauses 1%
c [cce-3-1] eliminated 189 small clauses in 36676717 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 189 covered clauses in round 1
c [cce-3] eliminated 189 covered clauses in TOTAL during 1 rounds
c [cce-3] 189 < 1/100 * 381440 = 3814 considered unsuccessful
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 8799 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 2933970835 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 24 variables 0% in round 1 in 14118185 steps
c [elim-4-1] backward subsumption/strengthening limit 14118100
c [elim-4-1-1] backward checking 504 touched variables 6%
c [elim-4-1-1] incomplete backward checking 323 remain 64%
c [elim-4-1] subsumed 69 and strengthened 492 clauses in 14122978 steps
c [elim-4-1] rescheduled 54 variables 1% by backward subsumption
c [elim-4-2] eliminated 1 variables 0% in round 2 in 601699 steps
c [elim-4-2] backward subsumption/strengthening limit 601600
c [elim-4-2-1] backward checking 340 touched variables 4%
c [elim-4-2-1] incomplete backward checking 340 remain 100%
c [elim-4-2] subsumed 0 and strengthened 1 clauses in 609518 steps
c [elim-4-2] rescheduled 16 variables 0% by backward subsumption
c [elim-4-3] no variable eliminated in round 3 in 2236 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 25 = 0% variables out of 8799 scheduled
c [elim-4] 25 < 1/100 * 8799 = 87 considered unsuccessful
c [bca-3] limit of 10000000 steps and 762182 added (scaled 2)
c [bca-3] 6078 out of 17550 literals actually usable 35%
c [bca-3] added 0 blocked clauses in 72722 steps
c [sweep-6] limit 8801912 penalty 0 = 0 + 0
c [sweep-6-1] 313 pos 3.6% + 8461 neg 96.4% = 8774 sched 100.0% ret 0
c [sweep-6-1] 8834463 steps 157 queries 170.79 avg class size
c [sweep-6-1] 6959 decisions 156 SAT calls 224.85 avg env size
c [sweep-6-1] 294 variables remain 3% (8480 retained 97%)
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 156 queries)
c [sort-queue-7] sorted 8774 enqueued variables after 351367 conflicts
c [score-dist-7] active 0 (0%), one 8751 (100%), zero 23 (0%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 51 variables 0.6% (8774 remain 84%)
c [simplification-7] removed 2070 irredundant clauses 0.5% (380841 remain 96%)
c [simplification-7] maximum reduction of 1% = max (1%, 1%)
c [simplification-7] geometric conflict interval increment 60000 = 120000 / 2
c [simplification-7] new conflict interval 180000
c [simplification-7] penalized conflict interval 180000 = 1 * 180000
c [simplification-7] hard conflict limit 621367 (soft 531367 + delta 90000)
c [simplification-7] new conflict limit 531367 (hard 621367)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  135.2    8773   380841    359217   67971  47319 24640   16    36   58  44%    116   -6   13   16   80%
c -  135.9    8773   380841    363192   36742  47327 24641   15    41   39  36%   -767   -1   13   16   79%
c -  145.9    8773   380841    401759   38808  47379 24647   17    38   39  43%     18   -2   19   16  115%
c -  156.3    8773   380841    440111   39637  47486 24661   17    53   40  32%    464   12   14   16   86%
c i  157.7    8772   380841    448632   47759  47525 24661   17    60   46  28%    532   18   18   16  112%
c -  165.7    8772   380841    480112   41209  47629 24667   17    40   39  41%   -158   -2   19   16  118%
c i  167.2    8771   380841    486333   47213  47642 24671   18    42   44  42%    -51    0   22   17  131%
c -  176.4    8771   380841    520616   42844  47705 24674   15    50   40  31%     32    9   15   17   88%
c i  179.1    8770   380841    528628   50657  47716 24677   17    43   45  41%    146    1   21   17  124%
c 
c [simplification-8] limit 531367 conflicts (hard 621367) hit after 555755 conflicts
c [quatres-6] found 15307 quaternary clauses 4% in total
c [quatres-6-1] removed 8 duplicate quaternary clauses
c [quatres-6-2] added 20 single-self-subsuming ternary resolvents
c [quatres-6-2] added 9 quaternary resolvents
c [ternres-6] limit 47409745 with penalty 0 = 0 + 0
c [ternres-6] 5 schedulable variables 0%
c [ternres-6] 2473 ternary resolvents (0 bin, 2473 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 2370487 penalty 2 = 2 + 0
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-20] removed 1 variables
c [simpleprobe-3] 4455 schedulable variables 51%
c [simpleprobe-3] limit 47409745 penalty 2 = 2 + 0
c [decomp-21] removed 4 variables
c [simpleprobe-3] 2310 variables remain 26% (6454 retained 74%)
c [simpleprobe-3] removed 4 variables, found 398 hbrs, 4 units
c [unhide-6] limit 4740974 with penalty 1 = 0 + 1
c [unhide-6-7] 0 units, 0 failed, 375 tauts, 0 hbrs, 230785 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 48 transitive binary clauses
c [transred-6] found 1 units
c [sort-queue-8] sorted 8763 enqueued variables after 555755 conflicts
c [score-dist-8] active 0 (0%), one 8763 (100%), zero 0 (0%)
c [score-dist-8] max exp 1, different 1 (50%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 6 variables 0.1% (8763 remain 84%)
c [simplification-8] removed 85 irredundant clauses 0.0% (380756 remain 96%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 180000
c [simplification-8] new conflict interval 360000
c [simplification-8] penalized conflict interval 360000 = 1 * 360000
c [simplification-8] hard conflict limit 1095755 (soft 915755 + delta 180000)
c [simplification-8] new conflict limit 915755 (hard 1095755)
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 -  194.7    8763   380756    561306   43584  50115 24701   18    41   39  43%     83   -3   16   17   96%
c -  205.6    8763   380756    603857   46588  50202 24707   17    48   40  34%    532    4   19   17  114%
c -  217.6    8763   380756    645190   47478  50278 24713   17    37   40  47%    762   -5   20   17  117%
c -  230.6    8763   380756    687452   48874  50354 24717   17    41   40  40%    887    0   17   17   99%
c i  244.2    8762   380756    729206   89607  50445 24722   19    53   61  35%    951   10   21   17  122%
c -  244.8    8762   380756    730472   49327  50450 24722   19    51   40  37%  -1247    8   19   17  109%
c -  258.9    8762   380756    775485   51273  50519 24731   18    44   41  42%   -583    1   20   17  115%
c -  272.7    8762   380756    820597   53617  50562 24735   17    45   41  37%    217    4   18   17  105%
c -  289.8    8762   380756    865253   53519  50644 24740   20    48   41  42%    616    5   21   18  120%
c -  304.5    8762   380756    912266   55672  50742 24743   19    52   42  36%    825    8   20   18  109%
c 
c [simplification-9] limit 915755 conflicts (hard 1095755) hit after 915760 conflicts
c [quatres-7] found 16463 quaternary clauses 4% in total
c [quatres-7-2] added 15 single-self-subsuming ternary resolvents
c [quatres-7-2] added 13 quaternary resolvents
c [ternres-7] limit 85513640 with penalty 0 = 0 + 0
c [ternres-7] all 8762 free variables schedulable
c [ternres-7] 1490 ternary resolvents (1 bin, 1489 trn)
c [ternres-7] 7 variables remain 0% (8755 retained 100%)
c [decomp-22] removed 2 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 39 transitive binary clauses
c [sweep-7] limit 12827046 penalty 1 = 1 + 0
c [sweep-7-1] 8 pos 2.7% + 286 neg 97.3% = 294 sched 3.4% ret 8467
c [sweep-7-1] 6861779 steps 94 queries 9.72 avg class size
c [sweep-7-1] 4678 decisions 93 SAT calls 192.38 avg env size
c [sweep-7-1] fully completed sweeping round
c [sweep-7-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7-2] 421 pos 4.8% + 8340 neg 95.2% = 8761 sched 100.0% ret 0
c [sweep-7-2] 5979169 steps 105 queries 212.88 avg class size
c [sweep-7-2] 3384 decisions 104 SAT calls 146.92 avg env size
c [sweep-7-2] 1339 variables remain 15% (7422 retained 85%)
c [sweep-7-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7] removed 0 vars in TOTAL (2 rounds, 197 queries)
c [sort-queue-9] sorted 8761 enqueued variables after 915760 conflicts
c [score-dist-9] active 0 (0%), one 8761 (100%), zero 0 (0%)
c [score-dist-9] max exp 1, different 1 (50%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 1 variables 0.0% (8761 remain 84%)
c [simplification-9] removed 7 irredundant clauses 0.0% (380749 remain 96%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 360000
c [simplification-9] new conflict interval 720000
c [simplification-9] penalized conflict interval 720000 = 1 * 720000
c [simplification-9] hard conflict limit 1995760 (soft 1635760 + delta 360000)
c [simplification-9] new conflict limit 1635760 (hard 1995760)
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 -  322.8    8761   380749    958377   57930  52295 24779   19    41   41  46%    925   -0   20   18  110%
c 1  327.9    8761   380749    980066   78813  52335 24781   17    61   55  28%    953   17   19   18  105%
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: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 3 count, 0 added (0 skipped), 162197 steps
c bkwd: tried 10629 clauses, 21163 lits, 1.99 lits/clause
c bkwd: checked 14581733 occs, 1371.88 occs/clause, 689.02 occs/lit
c bkwd: subsumed 0 binary, 36 ternary, 51 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 543 large (0% self)
c blkd: 3 bces, 1813 removed, 8477529 resolutions, 27946430 steps
c blkd: 1769 blocking literals 8%, 23 pure
c bump: 978427 bumped seen, 139260810 lits 142.3 on average
c card: 3 count, 0 units, 0 am1, 9049759 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 48 subsumed
c card: 88 at-most-one constraints found, average size 4.68
c card: 88 at-most-one constraints used 100%, average size 4.68
c card: 129 at-most-two constraints found, average size 5.26
c card: 129 at-most-two constraints used 100%, average size 5.26
c cces: 3 cces, 446 eliminated, 446 ate 100%, 0 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: 3217293 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 44 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 24 decompositions, 96 equivalent 1%
c deco: 269 decision-only clauses 0%, 56% reduction
c decs: 3501394 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 4 elims, 984 eliminated 9%, 0 pure 0%
c elms: 9 rounds, 2.2 rounds/bve
c elms: 0 small 0%, 961 large 98%
c elms: 0 tried small, 0 succeeded 0%, 0 failed 0%
c elms: 423 subsumed, 22 strengthened, 1 blocked
c elms: 455674 copies, 801325 resolutions, 0 ipos
c elms: 892774 subchks, 756080 strchks
c gaus: 3 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10755784 steps, 5377892 extr 50%, 0 elim 0%
c glue: 16.7 orig avg, 16.7 real avg, 3.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 27019 = 8097 simple 30% + 18913 trn 70% + 9 lrg 0%, 51 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 978427 clauses, 80.5 length
c lrnd: 78720575 lits = 110310700 orig - 31590125 removed 29%
c lrnd: 359617 uips 37%, 516226 flips 53%
c mins: 969040 mins 99%, 211 bin 0%, 8903 size 1%
c mins: 173938740 poisoned searches, 39615531 hits, 23% hit rate
c mins: 243497361 used twice searches, 7033429 hits, 3% hit rate
c move: moved 2425, 11 bin 0%, 2414 trn 100%
c otfs: 5003 driving 23%, 16364 restarting 77%
c otfs: str 21367, 21175 red 99%, 192 irr 1%
c otfs: str 21367, 0 bin 0%, 33 trn 0%, 21334 lrg 100%
c otfs: sub 17, 17 red 100%, 0 irr 0%
c otfs: sub 17, 0 bin 0%, 9 trn 53%, 8 lrg 47%
c phas: 5 computed, 11426 set, 0 pos (0%), 11426 neg (100%)
c prbs: 2 basic, 21826 probed, 30 failed, 0 lifted
c prbs: 3 simple, 22487 probed, 4 failed, 0 eqs
c prbs: 2 treelook, 47 probed, 1 failed, 0 lifted
c prom: 267383 locked 15% out of 1818188 tried
c prps: 396084065 props, 112 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 7 count, 53 quat, 79 self1, 0 self2, 13 dup
c queu: 9 sorted, 3501394 next (0 steps 0.00)
c queu: 139351078 enq (0 steps 0.00), 139260810 deq 100%
c redc: 14259 clauses 16%, 87326 tried 9%, 3 sat 0%
c redc: 42956 lits 3%, 1259879 tried 1%, 3 sat 0%
c redc: 1402 times jump level reduced, 6.6 levels on average
c reds: 22 count, 44548.5 conflicts per reduce
c reds: 0 memlim 0%, 22 arith 100%
c reds: 665605 collected 78%, 185097 retired 22%
c rmbd: 541 removed, 58 red 11%
c rsts: 24814 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 9 count, 9 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 978427 count (1145768 tried 1.2), 22961 sub out of 974729 (2.4%)
c swps: 7 count, 10 rounds, 1373 queries (137.3/round)
c swps: 1365 sat calls, 1 unsat (2.5% success rate)
c swps: 47838 decisions 35.0, 3364 conflicts 2.5
c swps; 125.5 avg class size, 145.6 avg environment size
c swps: 0 failed, 17 impls, 9 equivs
c swp0: 454 type 0 queries, 93 unsat (20.5%), 453 sat (99.8%)
c swp1: 919 type 1 queries, 241 unsat (26.2%), 911 sat (99.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: 8959830 calls to obtain time
c tops: 579 fixed 6%, 11 its, 89096.91 confs/it
c trds: 7 transitive reductions, 253 removed, 1 failed
c trds: 101799 nodes, 248846 edges, 11521978 steps
c trim: 361407 words, 1.4 MB
c trnr: 7 count, 1 bin, 47596 trn, 205617899 steps
c unhd: 6 count, 7 rounds, 32890682 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 8 units, 8 bin, 0 trn, 0 lrg
c unhd: 4 failed, 4 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 3342 tauts, 12 bin 0%, 962 trn 29%, 1935 lrg 58%
c unhd: 3342 tauts, 433 stamp 13%, 1515 red 45%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 421583 str, 8 bin 0%, 43 trn 0%, 421532 lrg 100%, 415515 red 99%
c vars: 8761 remaining 84% and 1659 removed 16% out of 10420
c vars: 579 fixed 6%, 984 eliminated 9%, 96 equivalent 1%
c vsts: 9331864492 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 23.6 search visits per propagation, 9437.5 per conflict
c wchs: 3682173487 pushed, 3677985 enlarged, 147 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         974782        665605        185097      23615584       6868189        497169
c 
c  0 0         43528   4     10863   2         0   0  11257559  48   2247744  33     87174  18     1.3
c  1 5         28999   3     16644   3      5598   3   2380744  10<   704882  10     40363   8     0.4
c  2 6        117642  12     79704  12     20494  11   4621541  20   1559940  23<   112133  23<    1.4
c  3 9        228361  23    165834  25     39957  22   3226250  14   1282133  19    127269  26     3.3
c  4 14       278858  29<   205604  31<    51092  28<  1540860   7    725515  11     86489  17     6.0
c  5 21       187751  19    132769  20     40361  22    436434   2    259346   4     32371   7     6.4
c  6 30        66489   7     42197   6     18731  10    116525   0     69216   1      8641   2     2.7
c  7 41        16553   2      9001   1      5986   3     26117   0     14359   0      1925   0     0.6
c  8 54         4181   0      2002   0      1810   1      6249   0      3450   0       628   0     0.2
c  9 69         1391   0       632   0       606   0      1960   0       958   0       118   0     0.1
c 10 86          792   0       301   0       356   0      1049   0       516   0        50   0     0.0
c 11 126         234   0        54   0       104   0       293   0       129   0         7   0     0.0
c 12 230           3   0         0   0         2   0         3   0         1   0         1   0     0.0
c 
c avg                  3.7           3.8           4.1           1.3           1.8           2.5
c std                  1.5           1.4           1.5           1.5           1.6           1.6
c 
c    7.795   2% bump
c    4.818   1% probe
c    4.747   1% unhide
c    4.318   1% sweep
c    2.740   1% block
c    2.672   1% elim
c    2.116   1% decide
c    1.874   1% ternres
c 
c    4.756 < 1% rest (below)
c 
c    1.789   1% cce
c    0.977   0% quatres
c    0.811   0% gauss
c    0.546   0% bca
c    0.520   0% transred
c    0.114   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.928   1% preprocessing     7%
c   27.103   8% inprocessing     93%
c ==================================
c   29.031   9% simplifying
c  298.902  91% search
c ==================================
c  327.933 100% all
c 
c        980066 conflicts,        2988.6 confs/sec
c          3378 ternaries,         290.1 confs/ternary
c           256 binaries,         3828.4 confs/binary
c            11 iterations,      89096.9 confs/iteration
c 
c            22 reductions,          0.1 redus/sec,  44548.5 confs/reduction
c         24814 restarts,           75.7 rests/sec,     39.5 confs/restart
c       3501394 decisions,       10677.1 decis/sec,      3.6 decis/conflict
c     396084065 propagations,  1207818.3 props/sec,    113.1 props/decision
c 
c 327.9 seconds, 114.7 MB
c launch: done
