c launch: /data/cnf/sc2014/app/003-23-80.cnf.bz2
c host: atom20
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/003-23-80.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/003-23-80.cnf.bz2
c no embedded options
c found 'p cnf 4288 132592' header
c read 4288 variables, 132592 clauses, 873647 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=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 3829 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] INC (--score=1)
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    3829    76353         0       0      0     0    0     0    4   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 3 at-most-one constraints of average size 3.0
c [card-1] found 7 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 10 constraints (90%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 602 variables
c [simpleprobe-1] all 3686 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 138 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 138 variables, found 10 hbrs, 61 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 662 tauts, 0 hbrs, 22 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 3548 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 124 variables 3% in round 1 in 2047727 steps
c [elim-1-1] backward subsumption/strengthening limit 2047700
c [elim-1-1-1] backward checking 1179 touched variables 33%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 32 and strengthened 86 clauses in 745507 steps
c [elim-1-1] rescheduled 158 variables 4% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 121400 steps
c [elim-1-2] backward subsumption/strengthening limit 121400
c [elim-1-2-1] backward checking 39 touched variables 1%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 2 and strengthened 0 clauses in 103050 steps
c [elim-1-2] rescheduled 5 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 3260 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 127 = 4% variables out of 3548 scheduled
c [phase-count-1] 67777 negative 99.2% of 68317 except 540 0.8%
c [phase-count-1] 67500 positive 98.8% of 68317 except 817 1.2%
c [phase-1] phase bias: 1481 positive 43%, 1940 negative 57%
c [sort-queue-1] sorted 3421 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 3421 (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 393 variables 10.3% (3421 remain 89%)
c [simplification-1] removed 8036 irredundant clauses 10.5% (68317 remain 89%)
c [simplification-1] maximum reduction of 11% = max (10%, 11%)
c [simplification-1] large reduction 11% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 1 variables
c [simpleprobe-2] all 3420 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 1987 variables remain 58% (1433 retained 42%)
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6840 literals 100%
c [treelook-1] scheduling used 293771 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300064 steps
c [treelook-1] 5646 literals remain 83%
c [treelook-1] 3415 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 2 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 359 sched 10%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-1-1] 366 sched 11%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-1-2] 367 sched 11%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] removed 0 variables, found 16 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 3420 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 222 blocked clauses
c [block-1] 222 < 1/100 * 68315 = 683 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3542 clauses out of 21746 (16%) of length 7
c [cce-1-1] eliminated 427 clauses out of 20573 (2%) of length 6
c [cce-1-1] eliminated 2634 clauses out of 13613 (19%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 6603 large clauses in 30000097 steps
c [cce-1-1] allowing another 15000048 steps for small clauses
c [cce-1-1] scheduling 4500 clauses = 243 binary + 4257 ternary
c [cce-1-1] tried to eliminate 4500 small clauses 100%
c [cce-1-1] eliminated 4 binary clauses 2%
c [cce-1-1] eliminated 1062 ternary clauses 25%
c [cce-1-1] eliminated 1066 small clauses 24%
c [cce-1-1] eliminated 1066 small clauses in 16152749 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] eliminated 7669 covered clauses in round 1
c [cce-1-2] incomplete large round (ATE)
c [cce-1-2] allowing another 6923631 steps for small clauses
c [cce-1-2] scheduling 3434 clauses = 239 binary + 3195 ternary
c [cce-1-2] tried to eliminate 3434 small clauses 100%
c [cce-1-2] completed small round (ATE)
c [cce-1-2] eliminated 0 covered clauses in round 2
c [cce-1] eliminated 7669 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 3420 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 728 not tried 21% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 30 = 1% variables out of 3420 scheduled
c [elim-2] 30 < 1/100 * 3420 = 34 considered unsuccessful
c [bca-1] limit of 10000000 steps and 119504 added (scaled 2)
c [bca-1] 4497 out of 6782 literals actually usable 66%
c [bca-1] added 0 blocked clauses in 30629 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1615 pos 47.6% + 1775 neg 52.4% = 3390 sched 100.0% ret 0
c [sweep-1-1] 514256 steps 569 queries 175.31 avg class size
c [sweep-1-1] 9427 decisions 569 SAT calls 22.67 avg env size
c [sweep-1-1] fully completed sweeping round
c [decomp-8] removed 7 variables
c [sweep-1-1] removed 7 vars (0 failed, 6 eqs, 5 impls)
c [sweep-1-2] 1613 pos 47.7% + 1770 neg 52.3% = 3383 sched 100.0% ret 0
c [sweep-1-2] 469305 steps 541 queries 167.79 avg class size
c [sweep-1-2] 8686 decisions 542 SAT calls 22.58 avg env size
c [sweep-1-2] fully completed sweeping round
c [decomp-9] removed 1 variables
c [sweep-1-2] removed 1 vars (0 failed, 1 eqs, 3 impls)
c [sweep-1-3] 1612 pos 47.7% + 1770 neg 52.3% = 3382 sched 100.0% ret 0
c [sweep-1-3] 16565 steps 21 queries 927.67 avg class size
c [sweep-1-3] 279 decisions 21 SAT calls 20.48 avg env size
c [sweep-1-3] 3326 variables remain 98% (56 retained 2%)
c [sweep-1-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] removed 8 vars in TOTAL (3 rounds, 1128 queries)
c [sort-queue-2] sorted 296 enqueued variables after 1000 conflicts
c [score-dist-2] active 3086 (91%), one 0 (0%), zero 296 (9%)
c [score-dist-2] max exp 507, different 7 (1%)
c [score-dist-2] median active exp 504, avg 503.9
c [simplification-2] removed 39 variables 1.1% (3382 remain 88%)
c [simplification-2] removed 8844 irredundant clauses 12.9% (59473 remain 78%)
c [simplification-2] maximum reduction of 13% = max (1%, 13%)
c [simplification-2] large reduction 13% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3000 conflicts
c [quatres-1] found 7374 quaternary clauses 13% in total
c [quatres-1-1] added 31 double-self-subsuming ternary resolvents
c [quatres-1-2] added 78 single-self-subsuming ternary resolvents
c [quatres-1-2] added 257 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 3382 free variables schedulable
c [ternres-1] 209 ternary resolvents (14 bin, 195 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1 at-most-one constraints of average size 3.0
c [card-2] found 4 at-most-two constraints of average size 4.5
c [card-2] using previous limit 1000000 for elimination
c [card-2] 5 out of 5 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 3908 xors of average arity 4.9
c [gauss-1] connected 19022 occurrences of 818 variables (average 23.3)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] connected 1209 occurrences of 818 variables (average 1.5)
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 61 tauts, 0 hbrs, 135 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 14 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 2 clauses out of 16995 (0%) of length 7
c [cce-2-1] eliminated 163 clauses out of 20546 (1%) of length 6
c [cce-2-1] eliminated 62 clauses out of 11091 (1%) of length 5
c [cce-2-1] eliminated 311 clauses out of 6872 (5%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 538 large clauses in 29405972 steps
c [cce-2-1] allowing another 14702986 steps for small clauses
c [cce-2-1] scheduling 3455 clauses = 264 binary + 3191 ternary
c [cce-2-1] tried to eliminate 3455 small clauses 100%
c [cce-2-1] eliminated 1 binary clauses 0%
c [cce-2-1] eliminated 16 ternary clauses 1%
c [cce-2-1] eliminated 17 small clauses 0%
c [cce-2-1] eliminated 17 small clauses in 15587959 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] completed small and large (ATE)
c [cce-2-1] eliminated 555 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 7206039 steps for small clauses
c [cce-2-2] scheduling 3438 clauses = 263 binary + 3175 ternary
c [cce-2-2] tried to eliminate 3438 small clauses 100%
c [cce-2-2] completed small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 555 covered clauses in TOTAL during 2 rounds
c [cce-2] 555 < 1/100 * 59470 = 594 considered unsuccessful
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1663 pos 50.0% + 1663 neg 50.0% = 3326 sched 98.3% ret 56
c [sweep-2-1] 542877 steps 546 queries 167.49 avg class size
c [sweep-2-1] 10690 decisions 547 SAT calls 26.80 avg env size
c [sweep-2-1] fully completed sweeping round
c [decomp-12] removed 2 variables
c [sweep-2-1] removed 2 vars (0 failed, 1 eqs, 1 impls)
c [sweep-2-2] 1686 pos 49.9% + 1694 neg 50.1% = 3380 sched 100.0% ret 0
c [sweep-2-2] 458223 steps 447 queries 155.70 avg class size
c [sweep-2-2] 9172 decisions 446 SAT calls 28.44 avg env size
c [sweep-2-2] 274 variables remain 8% (3106 retained 92%)
c [decomp-13] removed 1 variables
c [sweep-2-2] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-2] removed 3 vars in TOTAL (2 rounds, 991 queries)
c [sort-queue-3] sorted 101 enqueued variables after 3000 conflicts
c [score-dist-3] active 3278 (97%), one 0 (0%), zero 101 (3%)
c [score-dist-3] max exp 508, different 8 (2%)
c [score-dist-3] median active exp 505, avg 505.2
c [simplification-3] removed 3 variables 0.1% (3379 remain 88%)
c [simplification-3] removed 564 irredundant clauses 0.9% (58909 remain 77%)
c [simplification-3] maximum reduction of 1% = max (0%, 1%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 23000 (soft 13000 + delta 10000)
c [simplification-3] new conflict limit 13000 (hard 23000)
c 
c [simplification-4] limit 13000 conflicts (hard 23000) hit after 13000 conflicts
c [quatres-2] found 7494 quaternary clauses 13% in total
c [quatres-2-1] added 13 double-self-subsuming ternary resolvents
c [quatres-2-2] added 95 single-self-subsuming ternary resolvents
c [quatres-2-2] added 193 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 3379 free variables schedulable
c [ternres-2] 184 ternary resolvents (15 bin, 169 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 3339 literals 49%
c [treelook-2] scheduling used 150019 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150271 steps
c [treelook-2] 2680 literals remain 40%
c [treelook-2] 2567 variables remain to probed next time 76%
c [treelook-2] removed 0 variables, found 11 hbrs
c [transred-2] limit 527111 with penalty 0 = 0 + 0
c [transred-2] removed 5 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 3378 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 1 blocked clauses
c [block-2] 1 < 1/100 * 58908 = 589 considered unsuccessful
c [elim-3] 728 variables 22% will be scheduled this time
c [elim-3] scheduled 728 variables 22%
c [elim-3] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 311 not tried 9% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 728 scheduled
c [bca-2] limit of 10000000 steps and 118286 added (scaled 2)
c [bca-2] 286 out of 6758 literals actually usable 4%
c [bca-2] added 0 blocked clauses in 15779 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 141 pos 51.5% + 133 neg 48.5% = 274 sched 8.1% ret 3104
c [sweep-3-1] 149063 steps 125 queries 26.86 avg class size
c [sweep-3-1] 6477 decisions 124 SAT calls 159.84 avg env size
c [sweep-3-1] fully completed sweeping round
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3-2] 1711 pos 50.7% + 1667 neg 49.3% = 3378 sched 100.0% ret 0
c [sweep-3-2] 598944 steps 383 queries 85.02 avg class size
c [sweep-3-2] 20405 decisions 383 SAT calls 136.77 avg env size
c [sweep-3-2] fully completed sweeping round
c [sweep-3-2] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-3-3] 1711 pos 50.7% + 1667 neg 49.3% = 3378 sched 100.0% ret 0
c [sweep-3-3] 253547 steps 135 queries 234.24 avg class size
c [sweep-3-3] 8607 decisions 134 SAT calls 201.07 avg env size
c [sweep-3-3] 1248 variables remain 37% (2130 retained 63%)
c [sweep-3-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (3 rounds, 640 queries)
c [sort-queue-4] sorted 9 enqueued variables after 13000 conflicts
c [score-dist-4] active 3369 (100%), one 0 (0%), zero 9 (0%)
c [score-dist-4] max exp 512, different 12 (2%)
c [score-dist-4] median active exp 509, avg 509.1
c [simplification-4] removed 1 variables 0.0% (3378 remain 88%)
c [simplification-4] removed 16 irredundant clauses 0.0% (58893 remain 77%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 30000
c [simplification-4] penalized conflict interval 30000 = 1 * 30000
c [simplification-4] hard conflict limit 58000 (soft 43000 + delta 15000)
c [simplification-4] new conflict limit 43000 (hard 58000)
c 
c [simplification-5] limit 43000 conflicts (hard 58000) hit after 43000 conflicts
c [quatres-3] found 7801 quaternary clauses 13% in total
c [quatres-3-1] added 13 double-self-subsuming ternary resolvents
c [quatres-3-2] added 70 single-self-subsuming ternary resolvents
c [quatres-3-2] added 163 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3378 free variables schedulable
c [ternres-3] 22 ternary resolvents (2 bin, 20 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 1684 xors of average arity 4.6
c [gauss-2] connected 7796 occurrences of 471 variables (average 16.6)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 3 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 2 clauses out of 16723 (0%) of length 7
c [cce-3-1] eliminated 20 clauses out of 20534 (0%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 22 large clauses in 15000042 steps
c [cce-3-1] allowing another 7500021 steps for small clauses
c [cce-3-1] scheduling 3463 clauses = 269 binary + 3194 ternary
c [cce-3-1] tried to eliminate 3463 small clauses 100%
c [cce-3-1] eliminated 10 ternary clauses 0%
c [cce-3-1] eliminated 10 small clauses 0%
c [cce-3-1] eliminated 10 small clauses in 8463899 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 32 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 3268071 steps for small clauses
c [cce-3-2] scheduling 3453 clauses = 269 binary + 3184 ternary
c [cce-3-2] tried to eliminate 3453 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 32 covered clauses in TOTAL during 2 rounds
c [cce-3] 32 < 1/100 * 58893 = 588 considered unsuccessful
c [sort-queue-5] sorted 2 enqueued variables after 43000 conflicts
c [score-dist-5] active 3376 (100%), one 0 (0%), zero 2 (0%)
c [score-dist-5] max exp 515, different 15 (3%)
c [score-dist-5] median active exp 512, avg 511.9
c [simplification-5] removed 0 variables 0.0% (3378 remain 88%)
c [simplification-5] removed 32 irredundant clauses 0.1% (58861 remain 77%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 30000
c [simplification-5] new conflict interval 60000
c [simplification-5] penalized conflict interval 60000 = 1 * 60000
c [simplification-5] hard conflict limit 133000 (soft 103000 + delta 30000)
c [simplification-5] new conflict limit 103000 (hard 133000)
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 -   18.6    3378    58861     58625   23870   2031   100  162   474   14  34%    599  228  125   75  167%
c -   27.2    3378    58861     92599   28735   2039   100  139   461   14  30%    771  129  152   98  155%
c 
c [simplification-6] limit 103000 conflicts (hard 133000) hit after 103000 conflicts
c [quatres-4] found 7918 quaternary clauses 13% in total
c [quatres-4-1] added 2 double-self-subsuming ternary resolvents
c [quatres-4-2] added 31 single-self-subsuming ternary resolvents
c [quatres-4-2] added 86 quaternary resolvents
c [ternres-4] limit 6770701 with penalty 0 = 0 + 0
c [ternres-4] all 3378 free variables schedulable
c [ternres-4] 18 ternary resolvents (2 bin, 16 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 846337 penalty 2 = 2 + 0
c [card-3] found 3 at-most-one constraints of average size 3.0
c [card-3] found 22 at-most-two constraints of average size 4.1
c [card-3] using previous limit 846337 for elimination
c [card-3] 25 out of 25 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 16926753 penalty 1 = 1 + 0
c [basicprobe-2-0] 458 sched 14%, 1 failed, 0 lifted, 2 hbrs
c [decomp-21] removed 1 variables
c [basicprobe-2-1] 458 sched 14%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-2-2] 458 sched 14%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-2] fully completed probing
c [basicprobe-2-2] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-2-2] removed 1 variables, found 3 hbrs
c [bate-1] eliminated 16 asymmetric tautologies during probing
c [unhide-3] limit 338535 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 35 tauts, 0 hbrs, 26308 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 13 transitive binary clauses
c [sweep-4] limit 1015605 penalty 1 = 1 + 0
c [sweep-4-1] 609 pos 48.8% + 638 neg 51.2% = 1247 sched 36.9% ret 2130
c [sweep-4-1] 605080 steps 302 queries 52.96 avg class size
c [sweep-4-1] 17072 decisions 301 SAT calls 165.62 avg env size
c [sweep-4-1] fully completed sweeping round
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4-2] 1657 pos 49.1% + 1720 neg 50.9% = 3377 sched 100.0% ret 0
c [sweep-4-2] 412234 steps 149 queries 195.17 avg class size
c [sweep-4-2] 11598 decisions 148 SAT calls 271.13 avg env size
c [sweep-4-2] 838 variables remain 25% (2539 retained 75%)
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (2 rounds, 449 queries)
c [sort-queue-6] sorted 2 enqueued variables after 103000 conflicts
c [score-dist-6] active 3375 (100%), one 0 (0%), zero 2 (0%)
c [score-dist-6] max exp 517, different 16 (3%)
c [score-dist-6] median active exp 514, avg 513.9
c [simplification-6] removed 1 variables 0.0% (3377 remain 88%)
c [simplification-6] removed 23 irredundant clauses 0.0% (58838 remain 77%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 60000
c [simplification-6] new conflict interval 120000
c [simplification-6] penalized conflict interval 120000 = 1 * 120000
c [simplification-6] hard conflict limit 283000 (soft 223000 + delta 60000)
c [simplification-6] new conflict limit 223000 (hard 283000)
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 -   42.7    3377    58838    141552   31017   2108   109  143   457   15  31%    904   83  132  154   86%
c -   54.0    3377    58838    172606   30234   2110   109  163   455   21  36%    949   50  156  161   96%
c -   64.8    3377    58838    204651   30534   2110   109  155   470   17  33%    978   43  122  165   74%
c 
c [simplification-7] limit 223000 conflicts (hard 283000) hit after 223001 conflicts
c [quatres-5] found 8087 quaternary clauses 13% in total
c [quatres-5-1] added 7 double-self-subsuming ternary resolvents
c [quatres-5-2] added 39 single-self-subsuming ternary resolvents
c [quatres-5-2] added 79 quaternary resolvents
c [ternres-5] limit 16373839 with penalty 0 = 0 + 0
c [ternres-5] all 3377 free variables schedulable
c [ternres-5] 12 ternary resolvents (0 bin, 12 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 3 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 3377 variables 100%
c [block-3] limit of 40934598 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 1 blocked clauses
c [block-3] 1 < 1/100 * 58838 = 588 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 3377 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1637383930 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 3 variables 0% in round 1 in 44698797 steps
c [elim-4-1] backward subsumption/strengthening limit 44698700
c [elim-4-1-1] backward checking 1123 touched variables 33%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 5 and strengthened 0 clauses in 528391 steps
c [elim-4-1] rescheduled 9 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 35845 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 3 = 0% variables out of 3377 scheduled
c [elim-4] 3 < 1/100 * 3377 = 33 considered unsuccessful
c [bca-3] limit of 10000000 steps and 118064 added (scaled 2)
c [bca-3] 170 out of 6750 literals actually usable 3%
c [bca-3] added 0 blocked clauses in 48804 steps
c [sort-queue-7] sorted 2 enqueued variables after 223001 conflicts
c [score-dist-7] active 3372 (100%), one 0 (0%), zero 2 (0%)
c [score-dist-7] max exp 518, different 18 (3%)
c [score-dist-7] median active exp 516, avg 515.3
c [simplification-7] removed 3 variables 0.1% (3374 remain 88%)
c [simplification-7] removed 56 irredundant clauses 0.1% (58782 remain 77%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 120000
c [simplification-7] new conflict interval 240000
c [simplification-7] penalized conflict interval 240000 = 1 * 240000
c [simplification-7] hard conflict limit 583001 (soft 463001 + delta 120000)
c [simplification-7] new conflict limit 463001 (hard 583001)
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 -   74.9    3374    58782    237571   30707   2154   101  160   463   17  35%    996   21  174  161  108%
c -   83.8    3374    58782    270679   31594   2156   101  177   469   16  38%   1007   17  187  160  117%
c -   97.3    3374    58782    313838   32516   2156   103  162   461   17  35%   1015    4  147  194   76%
c -  108.1    3374    58782    347706   33170   2156   104  161   460   19  35%   1019    1  152  177   86%
c -  120.0    3374    58782    382178   33922   2156   104  156   457   21  34%   1021   -2  161  168   96%
c -  131.0    3374    58782    419981   33116   2165   104  286   466   23  61%   1022    2  245  181  135%
c -  153.6    3374    58782    477207   34379   2170   104  304   449   22  68%   1023   -9  171  248   69%
c 
c [simplification-8] limit 463001 conflicts (hard 583001) hit after 495027 conflicts
c [quatres-6] found 8206 quaternary clauses 13% in total
c [quatres-6-1] removed 2 duplicate quaternary clauses
c [quatres-6-1] added 4 double-self-subsuming ternary resolvents
c [quatres-6-2] added 31 single-self-subsuming ternary resolvents
c [quatres-6-2] added 68 quaternary resolvents
c [ternres-6] limit 38628248 with penalty 0 = 0 + 0
c [ternres-6] all 3374 free variables schedulable
c [ternres-6] 9 ternary resolvents (2 bin, 7 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1931412 penalty 2 = 2 + 0
c [gauss-3] extracted 3906 xors of average arity 4.9
c [gauss-3] connected 19008 occurrences of 820 variables (average 23.2)
c [gauss-3] limit 1931412 penalty 2 = 2 + 0
c [gauss-3] connected 1215 occurrences of 820 variables (average 1.5)
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 1959 schedulable variables 58%
c [simpleprobe-3] limit 77256496 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 13 hbrs, 0 units
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 8 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 482853105 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 53 clauses out of 20759 (0%) of length 6
c [cce-4-1] eliminated 25 clauses out of 11127 (0%) of length 5
c [cce-4-1] eliminated 21 clauses out of 6516 (0%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 99 large clauses in 28968242 steps
c [cce-4-1] allowing another 14484121 steps for small clauses
c [cce-4-1] scheduling 3468 clauses = 272 binary + 3196 ternary
c [cce-4-1] tried to eliminate 3468 small clauses 100%
c [cce-4-1] eliminated 2 binary clauses 1%
c [cce-4-1] eliminated 1 ternary clauses 0%
c [cce-4-1] eliminated 3 small clauses 0%
c [cce-4-1] eliminated 3 small clauses in 15389569 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 102 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 14466186 steps for small clauses
c [cce-4-2] scheduling 3465 clauses = 270 binary + 3195 ternary
c [cce-4-2] tried to eliminate 3465 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 102 covered clauses in TOTAL during 2 rounds
c [cce-4] 102 < 1/100 * 58782 = 587 considered unsuccessful
c [score-dist-8] active 3374 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-8] max exp 519, different 17 (3%)
c [score-dist-8] median active exp 517, avg 516.6
c [simplification-8] removed 0 variables 0.0% (3374 remain 88%)
c [simplification-8] removed 102 irredundant clauses 0.2% (58680 remain 77%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 240000
c [simplification-8] new conflict interval 480000
c [simplification-8] penalized conflict interval 480000 = 1 * 480000
c [simplification-8] hard conflict limit 1215027 (soft 975027 + delta 240000)
c [simplification-8] new conflict limit 975027 (hard 1215027)
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 -  164.7    3374    58680    514635   36918   2213   113  121   462   18  26%   1024    4  133  204   65%
c -  175.2    3374    58680    549107   37847   2213   113  151   462   25  33%   1024    3  160  179   90%
c -  203.2    3374    58680    612967   36142   2216   114  349   452   25  77%   1024   -7  361  283  128%
c -  216.8    3374    58680    657117   37341   2219   114  143   463   21  31%   1024    4  142  238   60%
c -  228.3    3374    58680    694449   39030   2219   114  155   462   22  34%   1024    2  160  199   81%
c -  248.7    3374    58680    748967   37362   2221   114  342   466   29  73%   1024    4  343  255  135%
c -  277.9    3374    58680    813549   36732   2221   114  231   462   26  50%   1024    1  209  282   74%
c -  298.6    3374    58680    863170   40181   2222   114  225   464   32  48%   1024    1  257  255  101%
c -  332.6    3374    58680    940604   38877   2223   114  229   460   39  50%   1024   -1  274  300   92%
c 
c [simplification-9] limit 975027 conflicts (hard 1215027) hit after 975027 conflicts
c [quatres-7] found 8256 quaternary clauses 13% in total
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 12 single-self-subsuming ternary resolvents
c [quatres-7-2] added 52 quaternary resolvents
c [ternres-7] limit 86136022 with penalty 0 = 0 + 0
c [ternres-7] all 3374 free variables schedulable
c [ternres-7] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 64602015 penalty 2 = 2 + 0
c [sweep-5-1] 412 pos 49.3% + 424 neg 50.7% = 836 sched 24.8% ret 2538
c [sweep-5-1] 628066 steps 272 queries 45.84 avg class size
c [sweep-5-1] 16617 decisions 271 SAT calls 289.57 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-5-2] 1679 pos 49.8% + 1695 neg 50.2% = 3374 sched 100.0% ret 0
c [sweep-5-2] 983262 steps 402 queries 87.35 avg class size
c [sweep-5-2] 24966 decisions 402 SAT calls 324.50 avg env size
c [sweep-5-2] fully completed sweeping round
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-5-3] 1679 pos 49.8% + 1695 neg 50.2% = 3374 sched 100.0% ret 0
c [sweep-5-3] 966746 steps 395 queries 83.08 avg class size
c [sweep-5-3] 23732 decisions 394 SAT calls 334.66 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 1066 queries)
c [score-dist-9] active 3374 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-9] max exp 521, different 17 (3%)
c [score-dist-9] median active exp 518, avg 517.7
c [simplification-9] removed 0 variables 0.0% (3374 remain 88%)
c [simplification-9] removed 0 irredundant clauses 0.0% (58680 remain 77%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 480000
c [simplification-9] new conflict interval 960000
c [simplification-9] penalized conflict interval 960000 = 1 * 960000
c [simplification-9] hard conflict limit 2415027 (soft 1935027 + delta 480000)
c [simplification-9] new conflict limit 1935027 (hard 2415027)
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 -  362.3    3374    58680   1003892   41142   2361   125  351   460   35  76%   1024   -1  243  300   81%
c -  396.3    3374    58680   1081230   40317   2362   125  211   457   39  46%   1024   -2  216  299   72%
c 1  429.0    3374    58680   1155380   79668   2362   125  260   460  198  57%   1024    2  266  307   87%
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: 16 basic ate = 16 trn 100% + 0 lrg 0% in 1 updates
c bcas: 3 count, 0 added (0 skipped), 95212 steps
c bkwd: tried 4727 clauses, 9357 lits, 1.98 lits/clause
c bkwd: checked 452466 occs, 95.72 occs/clause, 48.36 occs/lit
c bkwd: subsumed 0 binary, 2 ternary, 37 large
c bkwd: strengthened 0 binary, 3 ternary (100% self), 83 large (0% self)
c blkd: 3 bces, 224 removed, 2440028 resolutions, 4914055 steps
c blkd: 29 blocking literals 0%, 0 pure
c bump: 1155622 bumped seen, 613006493 lits 530.5 on average
c card: 3 count, 0 units, 0 am1, 3980943 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 735 subsumed
c card: 7 at-most-one constraints found, average size 3.00
c card: 7 at-most-one constraints used 100%, average size 3.00
c card: 33 at-most-two constraints found, average size 4.15
c card: 32 at-most-two constraints used 97%, average size 4.16
c cces: 4 cces, 8358 eliminated, 8356 ate 100%, 2 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: 1006239 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 39 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 31 decompositions, 209 equivalent 5%
c deco: 324767 decision-only clauses 28%, 43% reduction
c decs: 7000774 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 4 elims, 159 eliminated 4%, 0 pure 0%
c elms: 7 rounds, 1.8 rounds/bve
c elms: 159 small 100%, 0 large 0%
c elms: 1049 tried small, 160 succeeded 15%, 889 failed 85%
c elms: 2094 subsumed, 3018 strengthened, 0 blocked
c elms: 755210 copies, 1942653 resolutions, 280708 ipos
c elms: 138756 subchks, 91603 strchks
c gaus: 3 extractions, 9498 extracted, 4.8 size, 7 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 2 gc, 9862948 steps, 4931474 extr 50%, 341562 elim 3%
c glue: 235.7 orig avg, 235.7 real avg, 10.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 79 = 23 simple 29% + 54 trn 68% + 2 lrg 3%, 31 sub 39%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1155622 clauses, 328.2 length
c lrnd: 379253152 lits = 498691030 orig - 119437878 removed 24%
c lrnd: 260965 uips 23%, 695626 flips 60%
c mins: 551089 mins 62%, 11 bin 0%, 8597 size 1%
c mins: 46741762 poisoned searches, 5034768 hits, 11% hit rate
c mins: 122264509 used twice searches, 45051766 hits, 37% hit rate
c move: moved 1322, 7 bin 1%, 1315 trn 99%
c otfs: 4821 driving 20%, 19248 restarting 80%
c otfs: str 24069, 23634 red 98%, 435 irr 2%
c otfs: str 24069, 0 bin 0%, 67 trn 0%, 24002 lrg 100%
c otfs: sub 210, 210 red 100%, 0 irr 0%
c otfs: sub 210, 0 bin 0%, 3 trn 1%, 207 lrg 99%
c phas: 1 computed, 3421 set, 1481 pos (43%), 1940 neg (57%)
c prbs: 2 basic, 4931 probed, 1 failed, 0 lifted
c prbs: 3 simple, 16230 probed, 61 failed, 119 eqs
c prbs: 2 treelook, 1853 probed, 0 failed, 0 lifted
c prom: 23666 locked 1% out of 3914459 tried
c prps: 347265808 props, 50 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 7 count, 898 quat, 356 self1, 71 self2, 2 dup
c queu: 7 sorted, 7000774 next (164603 steps 0.02)
c queu: 613014614 enq (1179094696 steps 1.92), 613006493 deq 100%
c redc: 11 clauses 0%, 11582 tried 1%, 0 sat 0%
c redc: 14 lits 0%, 83054 tried 0%, 0 sat 0%
c redc: 0 times jump level reduced, 0.0 levels on average
c reds: 23 count, 50233.9 conflicts per reduce
c reds: 0 memlim 0%, 23 arith 100%
c reds: 701827 collected 90%, 81517 retired 10%
c rmbd: 12 removed, 1 red 8%
c rsts: 9716 restarts 91%, 964 skipped 9%
c rsts: 964 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 9 count, 9 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 1155622 count (4340803 tried 3.8), 291625 sub out of 1154935 (25.3%)
c swps: 5 count, 13 rounds, 4274 queries (328.8/round)
c swps: 4282 sat calls, 17 unsat (1.2% success rate)
c swps: 167728 decisions 39.2, 5063 conflicts 1.2
c swps; 132.0 avg class size, 136.1 avg environment size
c swps: 0 failed, 16 impls, 9 equivs
c swp0: 1419 type 0 queries, 33 unsat (2.3%), 1417 sat (99.9%)
c swp1: 2855 type 1 queries, 162 unsat (5.7%), 2848 sat (99.8%)
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: 16312965 calls to obtain time
c tops: 546 fixed 13%, 0 its, 0.00 confs/it
c trds: 7 transitive reductions, 47 removed, 1 failed
c trds: 47059 nodes, 2578 edges, 3593 steps
c trim: 40566 words, 0.2 MB
c trnr: 7 count, 35 bin, 423 trn, 5035977 steps
c unhd: 3 count, 3 rounds, 732695 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 758 tauts, 0 bin 0%, 504 trn 66%, 254 lrg 34%
c unhd: 758 tauts, 0 stamp 0%, 302 red 40%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 26465 str, 0 bin 0%, 61 trn 0%, 26404 lrg 100%, 26416 red 100%
c vars: 3374 remaining 79% and 914 removed 21% out of 4288
c vars: 546 fixed 13%, 159 eliminated 4%, 209 equivalent 5%
c vsts: 10584019396 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 30.5 search visits per propagation, 9155.8 per conflict
c wchs: 2456963520 pushed, 3022072 enlarged, 92 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1155833        701827         81517     119780959      44326664        525252
c 
c  0 0         10056   1        15   0         0   0  43564167  36  11804157  27     89084  17     0.3
c  1 5          4827   0        39   0      3367   4  19012852  16   6278645  14     48522   9     0.1
c  2 6          6049   1       423   0      4030   5  13023257  11<  5013307  11     50908  10     0.1
c  3 9         12012   1      2574   0      6868   8  13846882  12   5082174  11<    48123   9     0.3
c  4 14        23608   2     10457   1      9021  11  12255811  10   5298400  12     50555  10     0.7
c  5 21        31694   3     20523   3      6943   9   6141861   5   2839886   6     31794   6<    0.9
c  6 30        36822   3     27777   4      5124   6   3248041   3   1746183   4     23165   4     1.0
c  7 41        39529   3     31946   5      4356   5   2305715   2   1306288   3     19118   4     1.2
c  8 54        42127   4     35448   5      3758   5<  1418036   1    893746   2     14005   3     1.4
c  9 69        44723   4     38638   6      3170   4    859883   1    605213   1     12050   2     1.7
c 10 86       101090   9<    89977  13<     5317   7   1078765   1    823796   2     17435   3     4.6
c 11 126      295749  26    270983  39     10183  12   1429256   1   1221080   3     39848   8    30.3
c 12 230      507547  44    173027  25     19380  24   1596433   1   1413789   3     80645  15   119.3
c 
c avg                 10.3          10.2           7.6           2.2           3.1           5.2
c std                  2.5           2.0           3.7           2.7           3.2           4.3
c 
c  114.907  27% bump
c    4.352   1% decide
c    2.042   0% cce
c 
c    3.451 < 1% rest (below)
c 
c    1.803   0% sweep
c    1.416   0% elim
c    0.799   0% probe
c    0.424   0% block
c    0.267   0% gauss
c    0.166   0% bca
c    0.142   0% quatres
c    0.118   0% unhide
c    0.075   0% card
c    0.034   0% ternres
c    0.009   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.414   0% preprocessing     5%
c    8.153   2% inprocessing     95%
c ==================================
c    8.567   2% simplifying
c  420.395  98% search
c ==================================
c  428.963 100% all
c 
c       1155380 conflicts,        2693.4 confs/sec
c           186 ternaries,        6211.7 confs/ternary
c            14 binaries,        82527.1 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            23 reductions,          0.1 redus/sec,  50233.9 confs/reduction
c          9716 restarts,           22.6 rests/sec,    118.9 confs/restart
c       7000774 decisions,       16320.2 decis/sec,      6.1 decis/conflict
c     347265808 propagations,   809547.1 props/sec,     49.6 props/decision
c 
c 429.0 seconds, 210.3 MB
c launch: done
