c launch: /data/cnf/sc2014/app/atco_enc1_opt1_10_15.cnf.bz2
c host: atom24
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/atco_enc1_opt1_10_15.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc1_opt1_10_15.cnf.bz2
c no embedded options
c found 'p cnf 46759 261059' header
c read 46759 variables, 261059 clauses, 878724 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=6
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 46396 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] AVG (--score=6)
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   46396   251513         0       0      0     0    0     0   15   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 9362 at-most-one constraints of average size 3.0
c [card-1] found 74 at-most-two constraints of average size 4.8
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9436 out of 9436 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 11460 variables
c [simpleprobe-1] all 35299 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 4883 variables
c [simpleprobe-1] 19848 variables remain 65% (10568 retained 35%)
c [simpleprobe-1] removed 4883 variables, found 5817 hbrs, 696 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 505 failed, 983 tauts, 0 hbrs, 2271 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 29895 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 13214 variables 44% in round 1 in 12708796 steps
c [elim-1-1] backward subsumption/strengthening limit 7291204
c [elim-1-1-1] backward checking 22729 touched variables 76%
c [elim-1-1-1] incomplete backward checking 18356 remain 81%
c [elim-1-1] subsumed 183 and strengthened 138 clauses in 7291509 steps
c [elim-1] incomplete 652 not tried 2% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 13214 = 44% variables out of 29895 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 165775 negative 89.5% of 185253 except 19478 10.5%
c [phase-count-1] 159598 positive 86.2% of 185253 except 25655 13.8%
c [phase-1] phase bias: 8474 positive 51%, 8207 negative 49%
c [sort-queue-1] sorted 16681 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 16681 (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 29526 variables 63.9% (16681 remain 36%)
c [simplification-1] removed 66260 irredundant clauses 26.3% (185253 remain 74%)
c [simplification-1] maximum reduction of 64% = max (64%, 26%)
c [simplification-1] large reduction 64% >= 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 430 variables
c [simpleprobe-2] 11150 schedulable variables 69%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 4 variables
c [simpleprobe-2] 11230 variables remain 69% (5017 retained 31%)
c [simpleprobe-2] removed 4 variables, found 208 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 21759 literals 67%
c [treelook-1] scheduling used 300516 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 306880 steps
c [treelook-1] 21649 literals remain 67%
c [treelook-1] 15345 variables remain to probed next time 94%
c [decomp-5] removed 1 variables
c [treelook-1] removed 3 variables, found 139 hbrs
c [basicprobe-1] limit 1474952 based on 184369 irredundant clauses
c [basicprobe-1-0] 5798 probes remain 36% after last round
c [basicprobe-1-0] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 5 variables, found 4024 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 1065 tauts, 0 hbrs, 907 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 16239 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 778 not tried 5% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 522 = 3% variables out of 16239 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 163398 negative 89.7% of 182135 except 18737 10.3%
c [phase-count-2] 157022 positive 86.2% of 182135 except 25113 13.8%
c [phase-2] phase bias: 53 positive 69%, 24 negative 31%
c [sort-queue-2] sorted 15134 enqueued variables after 1000 conflicts
c [score-dist-2] active 583 (4%), one 0 (0%), zero 15134 (96%)
c [score-dist-2] max exp 511, different 10 (2%)
c [score-dist-2] median active exp 511, avg 509.7
c [simplification-2] removed 964 variables 5.8% (15717 remain 34%)
c [simplification-2] removed 3118 irredundant clauses 1.7% (182135 remain 72%)
c [simplification-2] maximum reduction of 6% = max (6%, 2%)
c [simplification-2] large reduction 6% >= 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 [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4979 at-most-one constraints of average size 3.6
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4979 out of 4979 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 336 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 21309 literals 69%
c [treelook-2] scheduling used 302292 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 307267 steps
c [treelook-2] 21247 literals remain 69%
c [treelook-2] 13965 variables remain to probed next time 91%
c [treelook-2] removed 0 variables, found 65 hbrs
c [elim-3] 662 variables 4% will be scheduled this time
c [elim-3] scheduled 662 variables 4%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 469 not tried 3% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 662 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 161963 negative 89.2% of 181656 except 19693 10.8%
c [phase-count-3] 156097 positive 85.9% of 181656 except 25559 14.1%
c [phase-3] phase bias: 1 positive 50%, 1 negative 50%
c [sort-queue-3] sorted 14794 enqueued variables after 3000 conflicts
c [score-dist-3] active 587 (4%), one 0 (0%), zero 14794 (96%)
c [score-dist-3] max exp 513, different 10 (2%)
c [score-dist-3] median active exp 513, avg 511.4
c [simplification-3] removed 336 variables 2.1% (15381 remain 33%)
c [simplification-3] removed 479 irredundant clauses 0.3% (181656 remain 72%)
c [simplification-3] maximum reduction of 2% = max (2%, 0%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 6666
c [simplification-3] penalized conflict interval 6666 = 1 * 6666
c [simplification-3] hard conflict limit 19666 (soft 9666 + delta 10000)
c [simplification-3] new conflict limit 9666 (hard 19666)
c 
c [simplification-4] limit 9666 conflicts (hard 19666) hit after 9668 conflicts
c [decomp-8] removed 18 variables
c [basicprobe-2] limit 2169066 penalty 0 = 0 + 0
c [basicprobe-2-0] 877 probes remain 6% after last round
c [basicprobe-2-0] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 10 variables, found 3778 hbrs
c [unhide-3] limit 50000 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 789 tauts, 0 hbrs, 2142 literals
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 15353 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 46 variables 0% in round 1 in 122835253 steps
c [elim-4-1] backward subsumption/strengthening limit 122835200
c [elim-4-1-1] backward checking 651 touched variables 4%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 192 clauses in 4632617 steps
c [elim-4-1] rescheduled 34 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 355474 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 46 = 0% variables out of 15353 scheduled
c [elim-4] 46 < 1/100 * 15353 = 153 considered unsuccessful
c [phase-count-4] 158719 negative 88.8% of 178689 except 19970 11.2%
c [phase-count-4] 153205 positive 85.7% of 178689 except 25484 14.3%
c [phase-4] phase bias: 10 positive 30%, 23 negative 70%
c [sort-queue-4] sorted 14725 enqueued variables after 9668 conflicts
c [score-dist-4] active 582 (4%), one 0 (0%), zero 14725 (96%)
c [score-dist-4] max exp 515, different 10 (2%)
c [score-dist-4] median active exp 515, avg 513.0
c [simplification-4] removed 74 variables 0.5% (15307 remain 33%)
c [simplification-4] removed 2967 irredundant clauses 1.6% (178689 remain 71%)
c [simplification-4] maximum reduction of 2% = max (0%, 2%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 13332
c [simplification-4] penalized conflict interval 13332 = 1 * 13332
c [simplification-4] hard conflict limit 33000 (soft 23000 + delta 10000)
c [simplification-4] new conflict limit 23000 (hard 33000)
c 
c [simplification-5] limit 23000 conflicts (hard 33000) hit after 23000 conflicts
c [quatres-1] found 31747 quaternary clauses 33% in total
c [quatres-1-1] removed 2 duplicate quaternary clauses
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 2 single-self-subsuming ternary resolvents
c [quatres-1-2] added 32 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 15307 free variables schedulable
c [ternres-1] 521 ternary resolvents (0 bin, 521 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 1104 xors of average arity 2.5
c [gauss-1] connected 2751 occurrences of 1125 variables (average 2.4)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 255 variables
c [gauss-1] exported 0 unary, 4 binary and 6 ternary equations
c [simpleprobe-3] 10463 schedulable variables 70%
c [simpleprobe-3] limit 4890134 penalty 0 = 0 + 0
c [decomp-11] removed 33 variables
c [simpleprobe-3] 10627 variables remain 71% (4392 retained 29%)
c [simpleprobe-3] removed 33 variables, found 657 hbrs, 0 units
c [transred-1] limit 1222533 with penalty 0 = 0 + 0
c [transred-1] removed 1595 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 15019 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 23992 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 20 clauses out of 20 (100%) of length 22
c [cce-1-1] eliminated 29 clauses out of 29 (100%) of length 21
c [cce-1-1] eliminated 5 clauses out of 6 (83%) of length 20
c [cce-1-1] eliminated 239 clauses out of 646 (37%) of length 13
c [cce-1-1] eliminated 69 clauses out of 908 (8%) of length 12
c [cce-1-1] eliminated 81 clauses out of 605 (13%) of length 11
c [cce-1-1] eliminated 5 clauses out of 255 (2%) of length 10
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 448 large clauses in 30000000 steps
c [cce-1-1] allowing another 15000000 steps for small clauses
c [cce-1-1] scheduling 30186 clauses = 27383 binary + 2803 ternary
c [cce-1-1] tried to eliminate 5577 small clauses 18%
c [cce-1-1] eliminated 230 binary clauses 1%
c [cce-1-1] eliminated 26 ternary clauses 1%
c [cce-1-1] eliminated 256 small clauses 1%
c [cce-1-1] eliminated 256 small clauses in 30000333 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 704 covered clauses in round 1
c [cce-1] eliminated 704 covered clauses in TOTAL during 1 rounds
c [cce-1] 704 < 1/100 * 153738 = 1537 considered unsuccessful
c [bca-1] limit of 10000000 steps and 306568 added (scaled 2)
c [bca-1] 27841 out of 30038 literals actually usable 93%
c [bca-1] added 4034 blocked clauses in 133598 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 6957 pos 46.3% + 8061 neg 53.7% = 15018 sched 100.0% ret 0
c [sweep-1-1] 1004141 steps 66 queries 2424.50 avg class size
c [sweep-1-1] 1383 decisions 68 SAT calls 45.66 avg env size
c [sweep-1-1] 14507 variables remain 97% (511 retained 3%)
c [decomp-12] removed 7 variables
c [sweep-1-1] removed 7 vars (0 failed, 4 eqs, 1 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 7 vars in TOTAL (1 rounds, 65 queries)
c [phase-count-5] 134588 negative 87.9% of 153033 except 18445 12.1%
c [phase-count-5] 138897 positive 90.8% of 153033 except 14136 9.2%
c [phase-5] phase bias: 2 positive 67%, 1 negative 33%
c [sort-queue-5] sorted 12572 enqueued variables after 23000 conflicts
c [score-dist-5] active 2439 (16%), one 0 (0%), zero 12572 (84%)
c [score-dist-5] max exp 516, different 7 (1%)
c [score-dist-5] median active exp 516, avg 515.5
c [simplification-5] removed 296 variables 1.9% (15011 remain 32%)
c [simplification-5] removed 25656 irredundant clauses 14.4% (153033 remain 61%)
c [simplification-5] maximum reduction of 14% = max (2%, 14%)
c [simplification-5] large reduction 14% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 35000 (soft 25000 + delta 10000)
c [simplification-5] new conflict limit 25000 (hard 35000)
c 
c [simplification-6] limit 25000 conflicts (hard 35000) hit after 25000 conflicts
c [quatres-2] found 28124 quaternary clauses 30% in total
c [quatres-2-1] removed 2 duplicate quaternary clauses
c [quatres-2-2] added 3 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] all 15011 free variables schedulable
c [ternres-2] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-2] 4351 variables remain 29% (10660 retained 71%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2727 at-most-one constraints of average size 3.4
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2727 out of 2727 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 655 xors of average arity 3.0
c [gauss-2] connected 1965 occurrences of 734 variables (average 2.7)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [transred-2] limit 1358877 with penalty 0 = 0 + 0
c [transred-2] removed 787 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 15010 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 99 blocked clauses
c [block-2] 99 < 1/100 * 152735 = 1527 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 15010 variables 100%
c [elim-5] limit of 13588775 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 700 not tried 5% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1580 = 11% variables out of 15010 scheduled
c [bca-2] limit of 10000000 steps and 303917 added (scaled 2)
c [bca-2] 24883 out of 26862 literals actually usable 93%
c [bca-2] added 19 blocked clauses in 137150 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 6038 pos 46.6% + 6910 neg 53.4% = 12948 sched 96.4% ret 482
c [sweep-2-1] 1086678 steps 106 queries 1846.03 avg class size
c [sweep-2-1] 2115 decisions 98 SAT calls 45.05 avg env size
c [sweep-2-1] 12230 variables remain 91% (1200 retained 9%)
c [decomp-14] removed 18 variables
c [sweep-2-1] removed 18 vars (0 failed, 8 eqs, 7 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 18 vars in TOTAL (1 rounds, 105 queries)
c [phase-count-6] 133343 negative 88.5% of 150691 except 17348 11.5%
c [phase-count-6] 136653 positive 90.7% of 150691 except 14038 9.3%
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-6] sorted 11010 enqueued variables after 25000 conflicts
c [score-dist-6] active 2402 (18%), one 0 (0%), zero 11010 (82%)
c [score-dist-6] max exp 516, different 7 (1%)
c [score-dist-6] median active exp 516, avg 515.5
c [simplification-6] removed 1599 variables 10.7% (13412 remain 29%)
c [simplification-6] removed 2342 irredundant clauses 1.5% (150691 remain 60%)
c [simplification-6] maximum reduction of 11% = max (11%, 2%)
c [simplification-6] large reduction 11% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 37000 (soft 27000 + delta 10000)
c [simplification-6] new conflict limit 27000 (hard 37000)
c 
c [simplification-7] limit 27000 conflicts (hard 37000) hit after 27001 conflicts
c [quatres-3] found 28026 quaternary clauses 30% in total
c [quatres-3-2] added 2 single-self-subsuming ternary resolvents
c [quatres-3-2] added 8 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 3908 schedulable variables 29%
c [ternres-3] 44 ternary resolvents (0 bin, 44 trn)
c [ternres-3] fully completed ternary resolution
c [treelook-3] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 10530 literals 39%
c [treelook-3] scheduling used 150056 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 192453 steps
c [treelook-3] 10480 literals remain 39%
c [treelook-3] 8591 variables remain to probed next time 64%
c [treelook-3] removed 0 variables, found 84 hbrs
c [unhide-4] limit 74682 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 7 failed, 347 tauts, 0 hbrs, 7389 literals
c [transred-3] limit 1493652 with penalty 0 = 0 + 0
c [transred-3] removed 293 transitive binary clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 105 (1%) of length 14
c [cce-2-1] eliminated 1 clauses out of 977 (0%) of length 12
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 2 large clauses in 15000281 steps
c [cce-2-1] allowing another 7500140 steps for small clauses
c [cce-2-1] scheduling 56702 clauses = 24678 binary + 32024 ternary
c [cce-2-1] tried to eliminate 2265 small clauses 4%
c [cce-2-1] eliminated 33 binary clauses 0%
c [cce-2-1] eliminated 55 ternary clauses 0%
c [cce-2-1] eliminated 88 small clauses 0%
c [cce-2-1] eliminated 98 small clauses in 15000001 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 100 covered clauses in round 1
c [cce-2] eliminated 100 covered clauses in TOTAL during 1 rounds
c [cce-2] 100 < 1/100 * 150595 = 1505 considered unsuccessful
c [elim-6] 696 variables 5% will be scheduled this time
c [elim-6] scheduled 696 variables 5%
c [elim-6] limit of 29873059 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 353 not tried 3% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 696 scheduled
c [bca-3] limit of 10000000 steps and 303474 added (scaled 2)
c [bca-3] 24763 out of 26820 literals actually usable 92%
c [bca-3] added 0 blocked clauses in 138332 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 5646 pos 46.2% + 6573 neg 53.8% = 12219 sched 91.1% ret 1190
c [sweep-3-1] 1402118 steps 86 queries 2185.14 avg class size
c [sweep-3-1] 1771 decisions 79 SAT calls 48.23 avg env size
c [sweep-3-1] 11796 variables remain 88% (1613 retained 12%)
c [decomp-17] removed 13 variables
c [sweep-3-1] removed 13 vars (0 failed, 6 eqs, 9 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 13 vars in TOTAL (1 rounds, 85 queries)
c [phase-count-7] 133134 negative 88.5% of 150473 except 17339 11.5%
c [phase-count-7] 136459 positive 90.7% of 150473 except 14014 9.3%
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-7] sorted 10948 enqueued variables after 27001 conflicts
c [score-dist-7] active 2448 (18%), one 0 (0%), zero 10948 (82%)
c [score-dist-7] max exp 516, different 7 (1%)
c [score-dist-7] median active exp 516, avg 515.5
c [simplification-7] removed 16 variables 0.1% (13396 remain 29%)
c [simplification-7] removed 218 irredundant clauses 0.1% (150473 remain 60%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 20000
c [simplification-7] new conflict interval 33332
c [simplification-7] penalized conflict interval 33332 = 1 * 33332
c [simplification-7] hard conflict limit 76999 (soft 60333 + delta 16666)
c [simplification-7] new conflict limit 60333 (hard 76999)
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 -   19.0   13396   150473     58081   17663   3320 12500   11    18   17  63%    595    7   11    6  166%
c i   19.1   13395   150473     58613   18177   3320 12500   11    18   18  63%    599    7   10    6  157%
c 
c [simplification-8] limit 60333 conflicts (hard 76999) hit after 76999 conflicts
c [quatres-4] found 28611 quaternary clauses 30% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-2] added 8 single-self-subsuming ternary resolvents
c [quatres-4-2] added 35 quaternary resolvents
c [ternres-4] limit 5665406 with penalty 0 = 0 + 0
c [ternres-4] all 13393 free variables schedulable
c [ternres-4] 42 ternary resolvents (0 bin, 42 trn)
c [ternres-4] 12 variables remain 0% (13381 retained 100%)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 207 xors of average arity 3.0
c [gauss-3] connected 618 occurrences of 388 variables (average 1.6)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-18] removed 2 variables
c [basicprobe-3] limit 28327034 penalty 0 = 0 + 0
c [basicprobe-3-0] 2137 sched 16%, 7 failed, 0 lifted, 1377 hbrs
c [decomp-19] removed 153 variables
c [basicprobe-3-1] 8108 sched 61%, 6 failed, 0 lifted, 819 hbrs
c [decomp-20] removed 39 variables
c [basicprobe-3-2] 8113 sched 61%, 0 failed, 0 lifted, 124 hbrs
c [basicprobe-3-3] 8113 sched 61%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-3-4] 8113 sched 61%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-4] fully completed probing
c [basicprobe-3-4] 13 units = 13 failed (100%) + 0 lifted (0%)
c [basicprobe-3-4] removed 192 variables, found 2332 hbrs
c [bate-1] eliminated 3 asymmetric tautologies during probing
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 661 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 13199 variables 100%
c [block-3] limit of 28327034 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 221 blocked clauses
c [block-3] 221 < 1/100 * 150132 = 1501 considered unsuccessful
c [sweep-4] limit 1699622 penalty 0 = 0 + 0
c [sweep-4-1] 5398 pos 46.5% + 6201 neg 53.5% = 11599 sched 87.9% ret 1600
c [sweep-4-1] 2247226 steps 50 queries 2391.66 avg class size
c [sweep-4-1] 980 decisions 46 SAT calls 50.50 avg env size
c [sweep-4-1] 11378 variables remain 86% (1821 retained 14%)
c [decomp-23] removed 7 variables
c [sweep-4-1] removed 7 vars (0 failed, 4 eqs, 3 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 7 vars in TOTAL (1 rounds, 49 queries)
c [phase-count-8] 132607 negative 88.5% of 149910 except 17303 11.5%
c [phase-count-8] 135929 positive 90.7% of 149910 except 13981 9.3%
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-8] sorted 9611 enqueued variables after 76999 conflicts
c [score-dist-8] active 3581 (27%), one 0 (0%), zero 9611 (73%)
c [score-dist-8] max exp 518, different 9 (2%)
c [score-dist-8] median active exp 516, avg 516.4
c [simplification-8] removed 201 variables 1.5% (13192 remain 28%)
c [simplification-8] removed 563 irredundant clauses 0.4% (149910 remain 60%)
c [simplification-8] maximum reduction of 2% = max (2%, 0%)
c [simplification-8] geometric conflict interval increment 11110 = 33332 / 3
c [simplification-8] new conflict interval 44442
c [simplification-8] penalized conflict interval 44442 = 1 * 44442
c [simplification-8] hard conflict limit 143662 (soft 121441 + delta 22221)
c [simplification-8] new conflict limit 121441 (hard 143662)
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 -   29.3   13192   149910    101163   23814   3398 13538   12    18   18  67%    316    4   12    9  132%
c 
c [simplification-9] limit 121441 conflicts (hard 143662) hit after 127964 conflicts
c [quatres-5] found 29111 quaternary clauses 29% in total
c [quatres-5-2] added 8 single-self-subsuming ternary resolvents
c [quatres-5-2] added 30 quaternary resolvents
c [ternres-5] limit 10048168 with penalty 0 = 0 + 0
c [ternres-5] 12 schedulable variables 0%
c [ternres-5] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-5] fully completed ternary resolution
c [simpleprobe-4] 9276 schedulable variables 70%
c [simpleprobe-4] limit 40192673 penalty 0 = 0 + 0
c [decomp-25] removed 44 variables
c [simpleprobe-4] 4168 variables remain 32% (8980 retained 68%)
c [simpleprobe-4] removed 44 variables, found 2377 hbrs, 0 units
c [unhide-5] limit 1004816 with penalty 1 = 1 + 0
c [unhide-5-5] 0 units, 0 failed, 392 tauts, 0 hbrs, 8804 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 1086 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 13148 variables 100%
c [elim-7] limit of 100481683 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 199 not tried 2% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 100 = 1% variables out of 13148 scheduled
c [elim-7] 100 < 1/100 * 13148 = 131 considered unsuccessful
c [bca-4] limit of 10000000 steps and 300152 added (scaled 2)
c [bca-4] 23417 out of 26098 literals actually usable 90%
c [bca-4] added 268 blocked clauses in 154662 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 30144500 penalty 0 = 0 + 0
c [sweep-5-1] 5236 pos 46.6% + 6011 neg 53.4% = 11247 sched 86.2% ret 1801
c [sweep-5-1] 24349302 steps 2394 queries 85.12 avg class size
c [sweep-5-1] 32617 decisions 2240 SAT calls 30.12 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-26] removed 170 variables
c [sweep-5-1] removed 170 vars (0 failed, 179 eqs, 187 impls)
c [sweep-5-2] 6165 pos 47.9% + 6713 neg 52.1% = 12878 sched 100.0% ret 0
c [sweep-5-2] 6165741 steps 173 queries 1284.23 avg class size
c [sweep-5-2] 3479 decisions 168 SAT calls 45.86 avg env size
c [sweep-5-2] 11180 variables remain 87% (1698 retained 13%)
c [decomp-27] removed 8 variables
c [sweep-5-2] removed 8 vars (0 failed, 8 eqs, 8 impls)
c [sweep-5] removed 178 vars in TOTAL (2 rounds, 2565 queries)
c [phase-count-9] 131546 negative 88.4% of 148772 except 17226 11.6%
c [phase-count-9] 134960 positive 90.7% of 148772 except 13812 9.3%
c [phase-9] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-9] sorted 8678 enqueued variables after 127964 conflicts
c [score-dist-9] active 4192 (33%), one 0 (0%), zero 8678 (67%)
c [score-dist-9] max exp 519, different 9 (2%)
c [score-dist-9] median active exp 517, avg 517.1
c [simplification-9] removed 322 variables 2.4% (12870 remain 28%)
c [simplification-9] removed 1138 irredundant clauses 0.8% (148772 remain 59%)
c [simplification-9] maximum reduction of 2% = max (2%, 1%)
c [simplification-9] geometric conflict interval increment 14814 = 44442 / 3
c [simplification-9] new conflict interval 59256
c [simplification-9] penalized conflict interval 59256 = 1 * 59256
c [simplification-9] hard conflict limit 216848 (soft 187220 + delta 29628)
c [simplification-9] new conflict limit 187220 (hard 216848)
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 -   39.3   12870   148772    142066   31922   3274 14406   10    18   18  56%    645    4   12    9  127%
c -   46.1   12870   148772    179275   32735   3351 14410   10    14   19  70%    809   -1    9   10   89%
c 
c [simplification-10] limit 187220 conflicts (hard 216848) hit after 216848 conflicts
c [quatres-6] found 29899 quaternary clauses 28% in total
c [quatres-6-1] removed 3 duplicate quaternary clauses
c [quatres-6-2] added 16 single-self-subsuming ternary resolvents
c [quatres-6-2] added 46 quaternary resolvents
c [ternres-6] limit 17682020 with penalty 0 = 0 + 0
c [ternres-6] all 12870 free variables schedulable
c [ternres-6] 151 ternary resolvents (0 bin, 151 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 1105126 penalty 3 = 3 + 0
c [card-4] found 3239 at-most-one constraints of average size 3.4
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1105126 for elimination
c [card-4] 3239 out of 3239 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 879 transitive binary clauses
c [transred-6] found 1 units
c [cce-3] limit of 22102525 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 19
c [cce-3-1] eliminated 5 clauses out of 7 (71%) of length 18
c [cce-3-1] eliminated 11 clauses out of 16 (69%) of length 17
c [cce-3-1] eliminated 9 clauses out of 20 (45%) of length 16
c [cce-3-1] eliminated 55 clauses out of 94 (59%) of length 15
c [cce-3-1] eliminated 41 clauses out of 112 (37%) of length 14
c [cce-3-1] eliminated 64 clauses out of 424 (15%) of length 13
c [cce-3-1] eliminated 52 clauses out of 952 (5%) of length 12
c [cce-3-1] eliminated 55 clauses out of 1029 (5%) of length 11
c [cce-3-1] eliminated 52 clauses out of 477 (11%) of length 10
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 345 large clauses in 22102546 steps
c [cce-3-1] allowing another 11051273 steps for small clauses
c [cce-3-1] scheduling 54665 clauses = 23646 binary + 31019 ternary
c [cce-3-1] tried to eliminate 3397 small clauses 6%
c [cce-3-1] eliminated 111 binary clauses 0%
c [cce-3-1] eliminated 363 ternary clauses 1%
c [cce-3-1] eliminated 474 small clauses 1%
c [cce-3-1] eliminated 490 small clauses in 22102552 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 835 covered clauses in round 1
c [cce-3] eliminated 835 covered clauses in TOTAL during 1 rounds
c [cce-3] 835 < 1/100 * 148408 = 1484 considered unsuccessful
c [bca-5] limit of 10000000 steps and 297806 added (scaled 2)
c [bca-5] 22372 out of 25740 literals actually usable 87%
c [bca-5] added 191 blocked clauses in 168455 steps
c [sweep-6] limit 5304606 penalty 0 = 0 + 0
c [sweep-6-1] 5368 pos 48.0% + 5811 neg 52.0% = 11179 sched 86.9% ret 1690
c [sweep-6-1] 5458935 steps 268 queries 685.53 avg class size
c [sweep-6-1] 4746 decisions 266 SAT calls 37.76 avg env size
c [sweep-6-1] 9112 variables remain 71% (3757 retained 29%)
c [decomp-29] removed 13 variables
c [sweep-6-1] removed 13 vars (0 failed, 8 eqs, 9 impls)
c [sweep-6] removed 13 vars in TOTAL (1 rounds, 267 queries)
c [sort-queue-10] sorted 7982 enqueued variables after 216848 conflicts
c [score-dist-10] active 4874 (38%), one 0 (0%), zero 7982 (62%)
c [score-dist-10] max exp 519, different 9 (2%)
c [score-dist-10] median active exp 518, avg 517.7
c [simplification-10] removed 14 variables 0.1% (12856 remain 28%)
c [simplification-10] removed 1199 irredundant clauses 0.8% (147573 remain 59%)
c [simplification-10] maximum reduction of 1% = max (0%, 1%)
c [simplification-10] geometric conflict interval increment 29628 = 59256 / 2
c [simplification-10] new conflict interval 88884
c [simplification-10] penalized conflict interval 88884 = 1 * 88884
c [simplification-10] hard conflict limit 350174 (soft 305732 + delta 44442)
c [simplification-10] new conflict limit 305732 (hard 350174)
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 -   53.7   12856   147573    220973   39109   3931 14166   10    14   19  71%    910    1   12    9  128%
c -   60.2   12856   147573    257129   39067   3962 14167   11    16   20  71%    958    2   12   10  123%
c i   64.1   12855   147573    285392   63095   4008 14175    8    10   23  79%    981   -4    7   10   67%
c -   66.4   12851   147573    299016   44641   4018 14175   10    13   20  74%  -1935   -0   10   10  100%
c -   72.0   12851   147573    336241   45734   4055 14180   10    14   20  72%   -652    1   11   10  116%
c 
c [simplification-11] limit 305732 conflicts (hard 350174) hit after 350175 conflicts
c [quatres-7] found 30105 quaternary clauses 28% in total
c [quatres-7-2] added 31 single-self-subsuming ternary resolvents
c [quatres-7-2] added 22 quaternary resolvents
c [ternres-7] limit 30020528 with penalty 0 = 0 + 0
c [ternres-7] all 12851 free variables schedulable
c [ternres-7] 78 ternary resolvents (0 bin, 78 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-4] limit 1501026 penalty 2 = 2 + 0
c [gauss-4] extracted 252 xors of average arity 3.0
c [gauss-4] connected 754 occurrences of 476 variables (average 1.6)
c [gauss-4] limit 1501026 penalty 2 = 2 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 519 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 12851 variables 100%
c [block-4] limit of 75051320 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 243 blocked clauses
c [block-4] 243 < 1/100 * 147311 = 1473 considered unsuccessful
c [bca-6] limit of 10000000 steps and 296892 added (scaled 2)
c [bca-6] 23275 out of 25688 literals actually usable 91%
c [bca-6] added 73 blocked clauses in 167265 steps
c [sweep-7] limit 9006158 penalty 0 = 0 + 0
c [sweep-7-1] 4379 pos 48.1% + 4725 neg 51.9% = 9104 sched 70.9% ret 3739
c [sweep-7-1] 9446004 steps 515 queries 351.40 avg class size
c [sweep-7-1] 8151 decisions 500 SAT calls 32.49 avg env size
c [sweep-7-1] 6242 variables remain 49% (6601 retained 51%)
c [decomp-31] removed 21 variables
c [sweep-7-1] removed 21 vars (0 failed, 24 eqs, 23 impls)
c [sweep-7] removed 21 vars in TOTAL (1 rounds, 514 queries)
c [sort-queue-11] sorted 7882 enqueued variables after 350175 conflicts
c [score-dist-11] active 4940 (39%), one 0 (0%), zero 7882 (61%)
c [score-dist-11] max exp 520, different 10 (2%)
c [score-dist-11] median active exp 518, avg 518.0
c [simplification-11] removed 29 variables 0.2% (12822 remain 28%)
c [simplification-11] removed 507 irredundant clauses 0.3% (147066 remain 58%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 88884
c [simplification-11] new conflict interval 177768
c [simplification-11] penalized conflict interval 177768 = 1 * 177768
c [simplification-11] hard conflict limit 616827 (soft 527943 + delta 88884)
c [simplification-11] new conflict limit 527943 (hard 616827)
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 -   78.9   12822   147066    375774   48405   4149 13783    9    11   19  78%    107   -2    9   10   95%
c -   85.0   12822   147066    416557   50717   4178 13788    9    12   20  79%    532   -1    8   10   85%
c i   87.8   12821   147066    437796   69031   4237 13797    8    10   23  78%    668   -2    5    9   58%
c i   87.8   12813   147066    437799   69030   4237 13799    8    10   23  78%    661   -2    5    9   58%
c -   91.3   12812   147066    457850   53683   4254 13800   10    13   29  75%  -1020    1   11    9  115%
c i   92.1   12811   147066    463146   57749   4282 13807    8    10   31  79%   -861   -3    5    9   59%
c -   98.9   12808   147066    502329   57046   4331 13810    8    11   29  75%   -234   -1    8    9   93%
c i  103.0   12807   147066    530606   80958   4412 13826    8    11   34  76%    207   -2    6    9   63%
c i  103.8   12772   147066    535152   84624   4437 13833    8    10   35  80%   -725   -3    6    9   69%
c i  103.9   12769   147066    535634   84958   4449 13837    7     9   35  80%   -743   -3    6    9   65%
c i  104.6   12718   147066    540286   89323   4523 13852    9    55   35  16%   -678   41    9    9  102%
c -  105.4   12672   147066    546622   60577   4562 13860    9    52   30  18%   -588   34   10    9  116%
c 
c [simplification-12] limit 527946 conflicts (hard 616827) hit after 576385 conflicts
c [quatres-8] found 28391 quaternary clauses 28% in total
c [quatres-8-1] removed 2 duplicate quaternary clauses
c [quatres-8-2] added 31 single-self-subsuming ternary resolvents
c [quatres-8-2] added 36 quaternary resolvents
c [ternres-8] limit 50688841 with penalty 0 = 0 + 0
c [ternres-8] all 12672 free variables schedulable
c [ternres-8] 190 ternary resolvents (1 bin, 189 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-32] removed 171 variables
c [treelook-4] limit 1267221 penalty 2 = 2 + 0 boost 1
c [treelook-4] scheduled 22067 literals 87%
c [treelook-4] scheduling used 499102 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1267221 penalty 2 = 2 + 0 boost 1
c [treelook-4] used 1273831 steps
c [treelook-4] 21775 literals remain 86%
c [treelook-4] 8005 variables remain to probed next time 63%
c [treelook-4] removed 0 variables, found 167 hbrs
c [unhide-6] limit 2534442 with penalty 2 = 2 + 0
c [unhide-6-7] 17 units, 29 failed, 11685 tauts, 0 hbrs, 47034 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 304 transitive binary clauses
c [transred-8] found 12 units
c [elim-8] 193 variables 2% will be scheduled this time
c [elim-8] scheduled 193 variables 2%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4000000000 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 206648693 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 193 scheduled
c [bca-7] limit of 10000000 steps and 277032 added (scaled 2)
c [bca-7] 18822 out of 25102 literals actually usable 75%
c [bca-7] added 13 blocked clauses in 119855 steps
c [sweep-8] limit 15206652 penalty 0 = 0 + 0
c [sweep-8-1] 3120 pos 50.6% + 3047 neg 49.4% = 6167 sched 49.1% ret 6383
c [sweep-8-1] 15310618 steps 1480 queries 35.55 avg class size
c [sweep-8-1] 27606 decisions 1423 SAT calls 38.45 avg env size
c [sweep-8-1] 139 variables remain 1% (12396 retained 99%)
c [decomp-34] removed 97 variables
c [sweep-8-1] removed 97 vars (0 failed, 78 eqs, 72 impls)
c [sweep-8] removed 97 vars in TOTAL (1 rounds, 1479 queries)
c [sort-queue-12] sorted 5656 enqueued variables after 576385 conflicts
c [score-dist-12] active 6797 (55%), one 0 (0%), zero 5656 (45%)
c [score-dist-12] max exp 521, different 10 (2%)
c [score-dist-12] median active exp 521, avg 520.4
c [simplification-12] removed 219 variables 1.7% (12453 remain 27%)
c [simplification-12] removed 10323 irredundant clauses 7.0% (136743 remain 54%)
c [simplification-12] maximum reduction of 7% = max (2%, 7%)
c [simplification-12] large reduction 7% >= 5% limit
c [simplification-12] next conflict interval 5763 = min (576385/100, 177768)
c [simplification-12] penalized conflict interval 5763 = 1 * 5763
c [simplification-12] hard conflict limit 592148 (soft 582148 + delta 10000)
c [simplification-12] new conflict limit 582148 (hard 592148)
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  115.3   12452   136743    578309   43695   3854 13067   10    30   23  33%     30    5   10    9  104%
c 
c [simplification-13] limit 582148 conflicts (hard 592148) hit after 592149 conflicts
c [quatres-9] found 27232 quaternary clauses 29% in total
c [quatres-9-1] removed 55 duplicate quaternary clauses
c [quatres-9-2] added 252 single-self-subsuming ternary resolvents
c [quatres-9-2] added 216 quaternary resolvents
c [ternres-9] limit 51930641 with penalty 0 = 0 + 0
c [ternres-9] all 12452 free variables schedulable
c [ternres-9] 4943 ternary resolvents (140 bin, 4803 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-35] removed 6 variables
c [basicprobe-4] limit 259653206 penalty 0 = 0 + 0
c [basicprobe-4-0] 7882 sched 66%, 72 failed, 52 lifted, 381 hbrs
c [decomp-36] removed 528 variables
c [basicprobe-4-1] 7530 sched 63%, 19 failed, 0 lifted, 603 hbrs
c [decomp-37] removed 26 variables
c [basicprobe-4-2] 7540 sched 63%, 7 failed, 0 lifted, 106 hbrs
c [decomp-38] removed 8 variables
c [basicprobe-4-3] 7547 sched 64%, 4 failed, 0 lifted, 54 hbrs
c [decomp-39] removed 4 variables
c [basicprobe-4-4] 7542 sched 63%, 2 failed, 0 lifted, 11 hbrs
c [decomp-40] removed 2 variables
c [basicprobe-4-5] 7544 sched 64%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-4-6] 7544 sched 64%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-7] 7544 sched 64%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-7] fully completed probing
c [basicprobe-4-7] 156 units = 104 failed (67%) + 52 lifted (33%)
c [basicprobe-4-7] removed 568 variables, found 1161 hbrs
c [bate-2] eliminated 412 asymmetric tautologies during probing
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 462 transitive binary clauses
c [bca-8] limit of 10000000 steps and 265681 added (scaled 2)
c [bca-8] 17439 out of 23760 literals actually usable 73%
c [bca-8] added 16 blocked clauses in 118673 steps
c [sweep-9] limit 15579192 penalty 0 = 0 + 0
c [sweep-9-1] 68 pos 53.1% + 60 neg 46.9% = 128 sched 1.1% ret 11751
c [sweep-9-1] 721946 steps 84 queries 12.07 avg class size
c [sweep-9-1] 1411 decisions 79 SAT calls 39.80 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-43] removed 3 variables
c [sweep-9-1] removed 3 vars (0 failed, 5 eqs, 2 impls)
c [sweep-9-2] 5686 pos 47.9% + 6190 neg 52.1% = 11876 sched 100.0% ret 0
c [sweep-9-2] 14860982 steps 905 queries 103.42 avg class size
c [sweep-9-2] 19628 decisions 899 SAT calls 44.87 avg env size
c [sweep-9-2] 4521 variables remain 38% (7353 retained 62%)
c [decomp-44] removed 51 variables
c [sweep-9-2] removed 51 vars (0 failed, 48 eqs, 36 impls)
c [sweep-9] removed 54 vars in TOTAL (2 rounds, 987 queries)
c [sort-queue-13] sorted 5323 enqueued variables after 592149 conflicts
c [score-dist-13] active 6502 (55%), one 0 (0%), zero 5323 (45%)
c [score-dist-13] max exp 521, different 9 (2%)
c [score-dist-13] median active exp 521, avg 520.5
c [simplification-13] removed 627 variables 5.0% (11825 remain 25%)
c [simplification-13] removed 5325 irredundant clauses 3.9% (131418 remain 52%)
c [simplification-13] maximum reduction of 5% = max (5%, 4%)
c [simplification-13] large reduction 5% >= 5% limit
c [simplification-13] next conflict interval 5921 = min (592149/100, 177768)
c [simplification-13] penalized conflict interval 5921 = 1 * 5921
c [simplification-13] hard conflict limit 608070 (soft 598070 + delta 10000)
c [simplification-13] new conflict limit 598070 (hard 608070)
c 
c [simplification-14] limit 598070 conflicts (hard 608070) hit after 608070 conflicts
c [quatres-10] found 25161 quaternary clauses 28% in total
c [quatres-10-1] removed 11 duplicate quaternary clauses
c [quatres-10-2] added 14 single-self-subsuming ternary resolvents
c [quatres-10-2] added 10 quaternary resolvents
c [ternres-10] limit 53153527 with penalty 0 = 0 + 0
c [ternres-10] all 11825 free variables schedulable
c [ternres-10] 32 ternary resolvents (3 bin, 29 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-45] removed 3 variables
c [simpleprobe-5] 3638 schedulable variables 31%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-46] removed 25 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 25 variables, found 3566 hbrs, 2 units
c [unhide-7] limit 5315352 with penalty 1 = 1 + 0
c [unhide-7-10] 0 units, 0 failed, 3006 tauts, 0 hbrs, 17772 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 767 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 332209545 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 24 (4%) of length 15
c [cce-4-1] eliminated 4 clauses out of 46 (9%) of length 14
c [cce-4-1] eliminated 7 clauses out of 309 (2%) of length 13
c [cce-4-1] eliminated 24 clauses out of 789 (3%) of length 12
c [cce-4-1] eliminated 48 clauses out of 651 (7%) of length 11
c [cce-4-1] eliminated 16 clauses out of 587 (3%) of length 10
c [cce-4-1] eliminated 55 clauses out of 2517 (2%) of length 9
c [cce-4-1] eliminated 75 clauses out of 3675 (2%) of length 8
c [cce-4-1] eliminated 89 clauses out of 7122 (1%) of length 7
c [cce-4-1] eliminated 471 clauses out of 15661 (3%) of length 6
c [cce-4-1] eliminated 250 clauses out of 23934 (1%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 1040 large clauses in 332209976 steps
c [cce-4-1] allowing another 166104988 steps for small clauses
c [cce-4-1] scheduling 48608 clauses = 21448 binary + 27160 ternary
c [cce-4-1] tried to eliminate 48608 small clauses 100%
c [cce-4-1] eliminated 374 binary clauses 2%
c [cce-4-1] eliminated 1446 ternary clauses 5%
c [cce-4-1] eliminated 1820 small clauses 4%
c [cce-4-1] eliminated 1820 small clauses in 306316979 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 2860 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 12946361 steps for small clauses
c [cce-4-2] scheduling 46789 clauses = 21074 binary + 25715 ternary
c [cce-4-2] tried to eliminate 5119 small clauses 11%
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 2860 covered clauses in TOTAL during 2 rounds
c [bca-9] limit of 10000000 steps and 258593 added (scaled 2)
c [bca-9] 17002 out of 23596 literals actually usable 72%
c [bca-9] added 15 blocked clauses in 131289 steps
c [sweep-10] limit 15946058 penalty 0 = 0 + 0
c [sweep-10-1] 2159 pos 47.9% + 2346 neg 52.1% = 4505 sched 38.2% ret 7292
c [sweep-10-1] 14229034 steps 1330 queries 66.02 avg class size
c [sweep-10-1] 23489 decisions 1306 SAT calls 36.33 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-47] removed 50 variables
c [sweep-10-1] removed 50 vars (0 failed, 41 eqs, 36 impls)
c [sweep-10-2] 5671 pos 48.3% + 6076 neg 51.7% = 11747 sched 100.0% ret 0
c [sweep-10-2] 1735692 steps 38 queries 534.05 avg class size
c [sweep-10-2] 1458 decisions 37 SAT calls 101.59 avg env size
c [sweep-10-2] 11066 variables remain 94% (681 retained 6%)
c [sweep-10-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-10] removed 50 vars in TOTAL (2 rounds, 1366 queries)
c [sort-queue-14] sorted 5178 enqueued variables after 608070 conflicts
c [score-dist-14] active 6569 (56%), one 0 (0%), zero 5178 (44%)
c [score-dist-14] max exp 521, different 9 (2%)
c [score-dist-14] median active exp 521, avg 520.6
c [simplification-14] removed 78 variables 0.7% (11747 remain 25%)
c [simplification-14] removed 3588 irredundant clauses 2.7% (127830 remain 51%)
c [simplification-14] maximum reduction of 3% = max (1%, 3%)
c [simplification-14] geometric conflict interval increment 44442 = 177768 / 4
c [simplification-14] new conflict interval 222210
c [simplification-14] penalized conflict interval 222210 = 1 * 222210
c [simplification-14] hard conflict limit 941385 (soft 830280 + delta 111105)
c [simplification-14] new conflict limit 830280 (hard 941385)
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 -  137.2   11747   127830    616903   33945   4696 13393   11    24   19  44%    137   -2   11   10  113%
c -  149.5   11747   127830    662392   40192   4759 13412   12    24   28  48%    581   -1   13   10  122%
c -  160.3   11747   127830    705626   44394   4794 13427   10    15   29  67%    795   -8   10   10  100%
c -  172.1   11747   127830    746923   43094   4822 13434   11    23   28  49%    902    1   13   11  121%
c -  183.7   11747   127830    791452   45579   4853 13443   12    20   29  57%    962   -1   11   11   98%
c 
c [simplification-15] limit 830280 conflicts (hard 941385) hit after 830280 conflicts
c [quatres-11] found 25502 quaternary clauses 26% in total
c [quatres-11-1] removed 3 duplicate quaternary clauses
c [quatres-11-2] added 3 single-self-subsuming ternary resolvents
c [quatres-11-2] added 31 quaternary resolvents
c [ternres-11] limit 73149716 with penalty 0 = 0 + 0
c [ternres-11] all 11747 free variables schedulable
c [ternres-11] 68 ternary resolvents (0 bin, 68 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 2285928 penalty 4 = 4 + 0
c [card-5] found 3162 at-most-one constraints of average size 3.4
c [card-5] found 94 at-most-two constraints of average size 4.4
c [card-5] using previous limit 2285928 for elimination
c [card-5] 3253 out of 3256 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-5] limit 1828742 penalty 3 = 3 + 0
c [gauss-5] extracted 290 xors of average arity 3.0
c [gauss-5] connected 869 occurrences of 454 variables (average 1.9)
c [gauss-5] limit 1828742 penalty 3 = 3 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 515 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 11747 variables 100%
c [block-5] limit of 91437145 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 406 blocked clauses
c [block-5] 406 < 1/100 * 127693 = 1276 considered unsuccessful
c [bca-10] limit of 10000000 steps and 257388 added (scaled 2)
c [bca-10] 17281 out of 23428 literals actually usable 74%
c [bca-10] added 7 blocked clauses in 149931 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 219449140 penalty 0 = 0 + 0
c [sweep-11-1] 5250 pos 47.6% + 5784 neg 52.4% = 11034 sched 94.2% ret 679
c [sweep-11-1] 22082766 steps 2144 queries 38.26 avg class size
c [sweep-11-1] 34807 decisions 2137 SAT calls 32.89 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-50] removed 43 variables
c [sweep-11-1] removed 43 vars (0 failed, 49 eqs, 32 impls)
c [sweep-11-2] 5608 pos 48.1% + 6062 neg 51.9% = 11670 sched 100.0% ret 0
c [sweep-11-2] 23044180 steps 2125 queries 38.37 avg class size
c [sweep-11-2] 34579 decisions 2124 SAT calls 34.27 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-51] removed 40 variables
c [sweep-11-2] removed 40 vars (0 failed, 48 eqs, 25 impls)
c [sweep-11-3] 5583 pos 48.0% + 6047 neg 52.0% = 11630 sched 100.0% ret 0
c [sweep-11-3] 19603783 steps 2117 queries 32.32 avg class size
c [sweep-11-3] 33628 decisions 2128 SAT calls 32.55 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-52] removed 30 variables
c [sweep-11-3] removed 30 vars (0 failed, 38 eqs, 1 impls)
c [sweep-11] removed 113 vars in TOTAL (3 rounds, 6383 queries)
c [sort-queue-15] sorted 4281 enqueued variables after 830280 conflicts
c [score-dist-15] active 7319 (63%), one 0 (0%), zero 4281 (37%)
c [score-dist-15] max exp 521, different 9 (2%)
c [score-dist-15] median active exp 521, avg 520.7
c [simplification-15] removed 147 variables 1.3% (11600 remain 25%)
c [simplification-15] removed 592 irredundant clauses 0.5% (127238 remain 51%)
c [simplification-15] maximum reduction of 1% = max (1%, 0%)
c [simplification-15] geometric conflict interval increment 111105 = 222210 / 2
c [simplification-15] new conflict interval 333315
c [simplification-15] penalized conflict interval 333315 = 1 * 333315
c [simplification-15] hard conflict limit 1330252 (soft 1163595 + delta 166657)
c [simplification-15] new conflict limit 1163595 (hard 1330252)
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  199.7   11599   127238    831373   86946   4883 13221   12    22   30  53%    990    1   10   12   86%
c 1  199.9   11599   127238    832513   88029   4884 13222   11    31   30  37%  -1639    9    8   12   68%
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: 415 basic ate = 232 trn 56% + 183 lrg 44% in 2 updates
c bcas: 10 count, 4636 added (1509 skipped), 1419210 steps
c bkwd: tried 50474 clauses, 100480 lits, 1.99 lits/clause
c bkwd: checked 6342100 occs, 125.65 occs/clause, 63.12 occs/lit
c bkwd: subsumed 8 binary, 4 ternary, 171 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 330 large (0% self)
c blkd: 5 bces, 24961 removed, 3640980 resolutions, 11672575 steps
c blkd: 9816 blocking literals 10%, 43 pure
c bump: 844534 bumped seen, 37397918 lits 44.3 on average
c card: 5 count, 0 units, 0 am1, 15261300 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 53741 subsumed
c card: 23469 at-most-one constraints found, average size 3.29
c card: 23469 at-most-one constraints used 100%, average size 3.29
c card: 168 at-most-two constraints found, average size 4.59
c card: 165 at-most-two constraints used 98%, average size 4.59
c cces: 4 cces, 4473 eliminated, 3957 ate 88%, 516 abce 12%
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: 1139783 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 83 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 52 decompositions, 16301 equivalent 35%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1587069 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 8 elims, 15505 eliminated 33%, 435 pure 3%
c elms: 10 rounds, 1.2 rounds/bve
c elms: 11049 small 71%, 3978 large 26%
c elms: 13293 tried small, 11049 succeeded 83%, 2244 failed 17%
c elms: 9789 subsumed, 6326 strengthened, 96 blocked
c elms: 2776785 copies, 3954321 resolutions, 210853 ipos
c elms: 4831252 subchks, 1306379 strchks
c gaus: 5 extractions, 2508 extracted, 2.8 size, 3 max
c gaus: exported 0 units, 4 binary and 6 ternary equations
c gaus: 0 gc, 16663900 steps, 8331950 extr 50%, 228991 elim 1%
c glue: 10.1 orig avg, 10.1 real avg, 2.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 25908 = 12625 simple 49% + 13110 trn 51% + 173 lrg 1%, 562 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 844534 clauses, 19.6 length
c lrnd: 16558720 lits = 22664247 orig - 6105527 removed 27%
c lrnd: 234220 uips 28%, 551618 flips 65%
c mins: 832641 mins 99%, 327 bin 0%, 11566 size 1%
c mins: 16522451 poisoned searches, 2862330 hits, 17% hit rate
c mins: 35415055 used twice searches, 4860257 hits, 14% hit rate
c move: moved 24074, 10920 bin 45%, 13154 trn 55%
c otfs: 2350 driving 36%, 4203 restarting 64%
c otfs: str 6553, 6404 red 98%, 149 irr 2%
c otfs: str 6553, 0 bin 0%, 196 trn 3%, 6357 lrg 97%
c otfs: sub 47, 47 red 100%, 0 irr 0%
c otfs: sub 47, 0 bin 0%, 16 trn 34%, 31 lrg 66%
c phas: 9 computed, 16796 set, 8540 pos (51%), 8256 neg (49%)
c prbs: 4 basic, 205904 probed, 131 failed, 52 lifted
c prbs: 5 simple, 81547 probed, 699 failed, 3606 eqs
c prbs: 4 treelook, 514 probed, 2 failed, 0 lifted
c prom: 147405 locked 15% out of 958971 tried
c prps: 270887960 props, 165 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c quat: 11 count, 468 quat, 370 self1, 1 self2, 905 dup
c queu: 15 sorted, 1587069 next (24421 steps 0.02)
c queu: 37595132 enq (231318789 steps 6.15), 37397918 deq 99%
c redc: 10660 clauses 7%, 163759 tried 20%, 9 sat 0%
c redc: 13177 lits 1%, 1874947 tried 8%, 9 sat 0%
c redc: 346 times jump level reduced, 2.8 levels on average
c reds: 18 count, 46250.7 conflicts per reduce
c reds: 0 memlim 0%, 18 arith 100%
c reds: 526518 collected 85%, 96162 retired 15%
c rmbd: 8574 removed, 2413 red 28%
c rsts: 22765 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 15 count, 15 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 844534 count (260219 tried 0.3), 70932 sub out of 841151 (8.4%)
c swps: 11 count, 16 rounds, 13865 queries (866.6/round)
c swps: 13598 sat calls, 290 unsat (1.1% success rate)
c swps: 231848 decisions 17.1, 14371 conflicts 1.1
c swps; 140.0 avg class size, 35.1 avg environment size
c swps: 0 failed, 451 impls, 548 equivs
c swp0: 4617 type 0 queries, 808 unsat (17.5%), 4491 sat (97.3%)
c swp1: 9248 type 1 queries, 2578 unsat (27.9%), 8826 sat (95.4%)
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: 4863498 calls to obtain time
c tops: 3354 fixed 7%, 11 its, 75683.00 confs/it
c trds: 11 transitive reductions, 7868 removed, 14 failed
c trds: 257564 nodes, 401396 edges, 10262907 steps
c trim: 375487 words, 1.4 MB
c trnr: 11 count, 144 bin, 5931 trn, 81957610 steps
c unhd: 7 count, 10 rounds, 17579630 steps
c unhd: 500 non-trivial sccs of average size 2.1
c unhd: 17 units, 17 bin, 0 trn, 0 lrg
c unhd: 541 failed, 540 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 18267 tauts, 1415 bin 8%, 2438 trn 13%, 9823 lrg 54%
c unhd: 18267 tauts, 4591 stamp 25%, 14871 red 81%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 86319 str, 17 bin 0%, 2724 trn 3%, 83578 lrg 97%, 81228 red 94%
c vars: 11599 remaining 25% and 35160 removed 75% out of 46759
c vars: 3354 fixed 7%, 15505 eliminated 33%, 16301 equivalent 35%
c vsts: 7525244194 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 28.1 search visits per propagation, 8809.8 per conflict
c wchs: 2370219271 pushed, 37117278 enlarged, 150 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         841619        526518         96162      13420567       5125681        403230
c 
c  0 0         59935   7      4654   1         0   0   7979054  59   2646559  52    190114  47     1.5
c  1 5         49384   6     21076   4      8391   9   2090838  16<   756900  15<    67091  17<    0.5
c  2 6        219912  26    143454  27     25332  26   2308990  17   1025354  20     98642  24     1.7
c  3 9        341731  41<   249113  47<    33607  35<   797450   6    524451  10     37705   9     2.5
c  4 14       152678  18     99069  19     24312  25    219723   2    157126   3      8724   2     1.7
c  5 21        16692   2      8520   2      4096   4     22764   0     14354   0       884   0     0.4
c  6 30         1161   0       573   0       379   0      1551   0       844   0        64   0     0.1
c  7 41          109   0        50   0        37   0       177   0        84   0         6   0     0.0
c  8 54           11   0         6   0         5   0        13   0         6   0         0   0     0.0
c  9 69            3   0         1   0         2   0         4   0         1   0         0   0     0.0
c 10 86            3   0         2   0         1   0         3   0         2   0         0   0     0.0
c 
c avg                  2.6           2.8           2.9           0.8           1.0           1.0
c std                  1.1           0.9           1.0           1.1           1.2           1.2
c 
c   10.104   5% sweep
c    6.473   3% elim
c    5.642   3% probe
c    5.216   3% cce
c    3.368   2% bump
c    2.138   1% unhide
c    1.418   1% quatres
c    0.968   0% decide
c    0.917   0% block
c    0.753   0% bca
c 
c    2.117 < 1% rest (below)
c 
c    0.674   0% transred
c    0.612   0% ternres
c    0.603   0% gauss
c    0.229   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.324   1% preprocessing     4%
c   35.635  18% inprocessing     96%
c ==================================
c   36.959  18% simplifying
c  162.949  82% search
c ==================================
c  199.912 100% all
c 
c        832513 conflicts,        4164.4 confs/sec
c          1765 ternaries,         471.7 confs/ternary
c           392 binaries,         2123.8 confs/binary
c            11 iterations,      75683.0 confs/iteration
c 
c            18 reductions,          0.1 redus/sec,  46250.7 confs/reduction
c         22765 restarts,          113.9 rests/sec,     36.6 confs/restart
c       1587069 decisions,        7938.8 decis/sec,      1.9 decis/conflict
c     270887960 propagations,  1355036.0 props/sec,    170.7 props/decision
c 
c 199.9 seconds, 49.2 MB
c launch: done
