c launch: /data/cnf/sc2014/app/atco_enc2_opt2_10_21.cnf.bz2
c host: atom18
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_enc2_opt2_10_21.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc2_opt2_10_21.cnf.bz2
c no embedded options
c found 'p cnf 9824 160531' header
c read 9824 variables, 160531 clauses, 675925 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=4
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 9423 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] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
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    9423   150535         0       0      0     0    0     0    7   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 1791 at-most-one constraints of average size 3.0
c [card-1] found 24 at-most-two constraints of average size 7.4
c [card-1] using previous limit 2000000 for elimination
c [card-1] 1815 out of 1815 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1189 variables
c [simpleprobe-1] all 8635 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 266 variables
c [simpleprobe-1] 5288 variables remain 63% (3081 retained 37%)
c [simpleprobe-1] removed 266 variables, found 2701 hbrs, 19 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 1 units, 3 failed, 1067 tauts, 0 hbrs, 9 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 8363 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 2209 variables 26% in round 1 in 8530403 steps
c [elim-1-1] backward subsumption/strengthening limit 8530400
c [elim-1-1-1] backward checking 5623 touched variables 67%
c [elim-1-1-1] incomplete backward checking 2691 remain 48%
c [elim-1-1] subsumed 285 and strengthened 732 clauses in 8530584 steps
c [elim-1-1] rescheduled 418 variables 5% by backward subsumption
c [elim-1-2] eliminated 14 variables 0% in round 2 in 227257 steps
c [elim-1-2] backward subsumption/strengthening limit 227200
c [elim-1-2-1] backward checking 2830 touched variables 34%
c [elim-1-2-1] incomplete backward checking 2804 remain 99%
c [elim-1-2] subsumed 6 and strengthened 9 clauses in 227857 steps
c [elim-1-2] rescheduled 23 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 2578 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 2223 = 27% variables out of 8363 scheduled
c [phase-count-1] 129929 negative 91.7% of 141730 except 11801 8.3%
c [phase-count-1] 132209 positive 93.3% of 141730 except 9521 6.7%
c [phase-1] phase bias: 3453 positive 56%, 2687 negative 44%
c [sort-queue-1] sorted 6140 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 6140 (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 3116 variables 33.7% (6140 remain 65%)
c [simplification-1] removed 8805 irredundant clauses 5.8% (141730 remain 94%)
c [simplification-1] maximum reduction of 34% = max (34%, 6%)
c [simplification-1] large reduction 34% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [decomp-3] removed 4 variables
c [simpleprobe-2] 4084 schedulable variables 67%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 5 variables
c [simpleprobe-2] 3574 variables remain 58% (2557 retained 42%)
c [simpleprobe-2] removed 5 variables, found 362 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 9952 literals 81%
c [treelook-1] scheduling used 301192 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 302017 steps
c [treelook-1] 9923 literals remain 81%
c [treelook-1] 5917 variables remain to probed next time 97%
c [decomp-5] removed 4 variables
c [treelook-1] removed 4 variables, found 173 hbrs
c [basicprobe-1] limit 1133656 based on 141707 irredundant clauses
c [basicprobe-1-0] 519 probes remain 8% after last round
c [basicprobe-1-0] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 5 variables, found 1872 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 1041 tauts, 0 hbrs, 492 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 6122 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 1532 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 22
c [cce-1-1] eliminated 15 clauses out of 15 (100%) of length 21
c [cce-1-1] eliminated 332 clauses out of 544 (61%) of length 13
c [cce-1-1] eliminated 80 clauses out of 880 (9%) of length 12
c [cce-1-1] eliminated 77 clauses out of 177 (44%) of length 11
c [cce-1-1] eliminated 8 clauses out of 229 (3%) of length 10
c [cce-1-1] eliminated 11 clauses out of 1144 (1%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 528 large clauses in 30000518 steps
c [cce-1-1] allowing another 15000259 steps for small clauses
c [cce-1-1] scheduling 14634 clauses = 12743 binary + 1891 ternary
c [cce-1-1] tried to eliminate 3282 small clauses 22%
c [cce-1-1] eliminated 358 binary clauses 3%
c [cce-1-1] eliminated 15 ternary clauses 1%
c [cce-1-1] eliminated 373 small clauses 3%
c [cce-1-1] eliminated 373 small clauses in 30000068 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 901 covered clauses in round 1
c [cce-1] eliminated 901 covered clauses in TOTAL during 1 rounds
c [cce-1] 901 < 1/100 * 140155 = 1401 considered unsuccessful
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 6122 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 789 not tried 13% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 81 = 1% variables out of 6122 scheduled
c [bca-1] limit of 10000000 steps and 278196 added (scaled 2)
c [bca-1] 11496 out of 12084 literals actually usable 95%
c [bca-1] added 95 blocked clauses in 29101 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2859 pos 47.3% + 3182 neg 52.7% = 6041 sched 100.0% ret 0
c [sweep-1-1] 1006239 steps 136 queries 387.67 avg class size
c [sweep-1-1] 2842 decisions 118 SAT calls 54.74 avg env size
c [sweep-1-1] 4856 variables remain 80% (1184 retained 20%)
c [decomp-6] removed 283 variables
c [sweep-1-1] removed 283 vars (0 failed, 33 eqs, 7 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 283 vars in TOTAL (1 rounds, 135 queries)
c [phase-count-2] 124959 negative 90.2% of 138477 except 13518 9.8%
c [phase-count-2] 128601 positive 92.9% of 138477 except 9876 7.1%
c [phase-2] phase bias: 2 positive 20%, 8 negative 80%
c [sort-queue-2] sorted 4886 enqueued variables after 1001 conflicts
c [score-dist-2] active 872 (15%), one 0 (0%), zero 4886 (85%)
c [score-dist-2] max exp 510, different 13 (3%)
c [score-dist-2] median active exp 503, avg 503.3
c [simplification-2] removed 382 variables 6.2% (5758 remain 61%)
c [simplification-2] removed 3253 irredundant clauses 2.3% (138477 remain 92%)
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 13001 (soft 3001 + delta 10000)
c [simplification-2] new conflict limit 3001 (hard 13001)
c 
c [simplification-3] limit 3001 conflicts (hard 13001) hit after 3001 conflicts
c [quatres-1] found 25528 quaternary clauses 28% in total
c [quatres-1-1] removed 2 duplicate quaternary clauses
c [quatres-1-2] added 2 single-self-subsuming ternary resolvents
c [quatres-1-2] added 23 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 5758 free variables schedulable
c [ternres-1] 22 ternary resolvents (0 bin, 22 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 867 at-most-one constraints of average size 3.1
c [card-2] found 43 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 910 out of 910 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 429 xors of average arity 3.0
c [gauss-1] connected 1275 occurrences of 603 variables (average 2.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-7] removed 5 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 9879 literals 86%
c [treelook-2] scheduling used 300545 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 305659 steps
c [treelook-2] 9811 literals remain 85%
c [treelook-2] 5498 variables remain to probed next time 96%
c [decomp-8] removed 1 variables
c [treelook-2] removed 1 variables, found 67 hbrs
c [transred-1] limit 138463 based on 138463 irredundant clauses
c [transred-1] removed 370 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5752 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 0 blocked clauses
c [elim-3] 616 variables 11% will be scheduled this time
c [elim-3] scheduled 616 variables 11%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 435 not tried 8% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 616 scheduled
c [bca-2] limit of 10000000 steps and 277079 added (scaled 2)
c [bca-2] 10596 out of 11506 literals actually usable 92%
c [bca-2] added 4 blocked clauses in 29111 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2288 pos 49.4% + 2339 neg 50.6% = 4627 sched 80.4% ret 1125
c [sweep-2-1] 1034423 steps 91 queries 412.10 avg class size
c [sweep-2-1] 2114 decisions 86 SAT calls 53.57 avg env size
c [sweep-2-1] 4120 variables remain 72% (1632 retained 28%)
c [decomp-9] removed 21 variables
c [sweep-2-1] removed 21 vars (0 failed, 9 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 21 vars in TOTAL (1 rounds, 90 queries)
c [phase-count-3] 124660 negative 90.2% of 138248 except 13588 9.8%
c [phase-count-3] 128307 positive 92.8% of 138248 except 9941 7.2%
c [phase-3] phase bias: 3 positive 100%, 0 negative 0%
c [sort-queue-3] sorted 4584 enqueued variables after 3001 conflicts
c [score-dist-3] active 1147 (20%), one 0 (0%), zero 4584 (80%)
c [score-dist-3] max exp 510, different 21 (4%)
c [score-dist-3] median active exp 502, avg 500.7
c [simplification-3] removed 27 variables 0.5% (5731 remain 61%)
c [simplification-3] removed 229 irredundant clauses 0.2% (138248 remain 92%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 20000
c [simplification-3] penalized conflict interval 20000 = 1 * 20000
c [simplification-3] hard conflict limit 33001 (soft 23001 + delta 10000)
c [simplification-3] new conflict limit 23001 (hard 33001)
c 
c [simplification-4] limit 23001 conflicts (hard 33001) hit after 23002 conflicts
c [quatres-2] found 25664 quaternary clauses 28% in total
c [quatres-2-2] added 6 single-self-subsuming ternary resolvents
c [quatres-2-2] added 17 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 5731 free variables schedulable
c [ternres-2] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-2] 636 variables remain 11% (5095 retained 89%)
c [decomp-10] removed 5 variables
c [basicprobe-2] limit 5281337 penalty 0 = 0 + 0
c [basicprobe-2-0] 407 sched 7%, 8 failed, 0 lifted, 912 hbrs
c [decomp-11] removed 91 variables
c [basicprobe-2-1] 1077 sched 19%, 1 failed, 0 lifted, 666 hbrs
c [decomp-12] removed 13 variables
c [basicprobe-2-2] 1058 sched 19%, 1 failed, 0 lifted, 98 hbrs
c [decomp-13] removed 2 variables
c [basicprobe-2-3] 473 probes remain 8% after last round
c [basicprobe-2-3] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-2-3] removed 106 variables, found 1678 hbrs
c [bate-1] eliminated 289 asymmetric tautologies during probing
c [unhide-3] limit 105626 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 691 tauts, 0 hbrs, 3829 literals
c [transred-2] limit 1056267 with penalty 0 = 0 + 0
c [transred-2] removed 791 transitive binary clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 14 clauses out of 14 (100%) of length 22
c [cce-2-1] eliminated 1 clauses out of 712 (0%) of length 12
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 15 large clauses in 15000636 steps
c [cce-2-1] allowing another 7500318 steps for small clauses
c [cce-2-1] scheduling 14575 clauses = 11155 binary + 3420 ternary
c [cce-2-1] tried to eliminate 1368 small clauses 9%
c [cce-2-1] eliminated 65 binary clauses 1%
c [cce-2-1] eliminated 23 ternary clauses 1%
c [cce-2-1] eliminated 88 small clauses 1%
c [cce-2-1] eliminated 88 small clauses in 15000116 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 103 covered clauses in round 1
c [cce-2] eliminated 103 covered clauses in TOTAL during 1 rounds
c [cce-2] 103 < 1/100 * 136822 = 1368 considered unsuccessful
c [bca-3] limit of 10000000 steps and 273987 added (scaled 2)
c [bca-3] 10039 out of 11242 literals actually usable 89%
c [bca-3] added 22 blocked clauses in 44801 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2017 pos 49.9% + 2028 neg 50.1% = 4045 sched 72.0% ret 1575
c [sweep-3-1] 1006846 steps 43 queries 575.60 avg class size
c [sweep-3-1] 1182 decisions 42 SAT calls 53.81 avg env size
c [sweep-3-1] 3814 variables remain 68% (1806 retained 32%)
c [decomp-14] removed 6 variables
c [sweep-3-1] removed 6 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 6 vars in TOTAL (1 rounds, 42 queries)
c [phase-count-4] 122643 negative 89.7% of 136716 except 14073 10.3%
c [phase-count-4] 126254 positive 92.3% of 136716 except 10462 7.7%
c [phase-4] phase bias: 2 positive 25%, 6 negative 75%
c [sort-queue-4] sorted 4339 enqueued variables after 23002 conflicts
c [score-dist-4] active 1275 (23%), one 0 (0%), zero 4339 (77%)
c [score-dist-4] max exp 510, different 66 (13%)
c [score-dist-4] median active exp 444, avg 461.5
c [simplification-4] removed 117 variables 2.0% (5614 remain 60%)
c [simplification-4] removed 1532 irredundant clauses 1.1% (136716 remain 91%)
c [simplification-4] maximum reduction of 2% = max (2%, 1%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 26666
c [simplification-4] penalized conflict interval 26666 = 1 * 26666
c [simplification-4] hard conflict limit 63001 (soft 49668 + delta 13333)
c [simplification-4] new conflict limit 49668 (hard 63001)
c 
c [simplification-5] limit 49668 conflicts (hard 63001) hit after 49670 conflicts
c [quatres-3] found 25725 quaternary clauses 28% in total
c [quatres-3-2] added 2 single-self-subsuming ternary resolvents
c [quatres-3-2] added 6 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 625 schedulable variables 11%
c [ternres-3] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 222 xors of average arity 3.0
c [gauss-2] connected 666 occurrences of 424 variables (average 1.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 [simpleprobe-3] 3296 schedulable variables 59%
c [simpleprobe-3] limit 11718675 penalty 0 = 0 + 0
c [decomp-16] removed 19 variables
c [simpleprobe-3] 3148 variables remain 56% (2447 retained 44%)
c [simpleprobe-3] removed 19 variables, found 896 hbrs, 0 units
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 715 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5595 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 9 blocked clauses
c [block-3] 9 < 1/100 * 136665 = 1366 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 5595 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 585933790 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 31 variables 1% in round 1 in 158036815 steps
c [elim-4-1] backward subsumption/strengthening limit 158036800
c [elim-4-1-1] backward checking 386 touched variables 7%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 55 clauses in 5655301 steps
c [elim-4-1] rescheduled 78 variables 1% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 4372132 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 31 = 1% variables out of 5595 scheduled
c [elim-4] 31 < 1/100 * 5595 = 55 considered unsuccessful
c [bca-4] limit of 10000000 steps and 272184 added (scaled 2)
c [bca-4] 9752 out of 11130 literals actually usable 88%
c [bca-4] added 15 blocked clauses in 67917 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1898 pos 50.3% + 1879 neg 49.7% = 3777 sched 67.9% ret 1787
c [sweep-4-1] 1135081 steps 91 queries 342.55 avg class size
c [sweep-4-1] 2394 decisions 92 SAT calls 63.72 avg env size
c [sweep-4-1] 3278 variables remain 59% (2284 retained 41%)
c [decomp-17] removed 15 variables
c [sweep-4-1] removed 15 vars (0 failed, 11 eqs, 5 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 15 vars in TOTAL (1 rounds, 90 queries)
c [phase-count-5] 121476 negative 89.5% of 135746 except 14270 10.5%
c [phase-count-5] 125137 positive 92.2% of 135746 except 10609 7.8%
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-5] sorted 4159 enqueued variables after 49670 conflicts
c [score-dist-5] active 1390 (25%), one 0 (0%), zero 4159 (75%)
c [score-dist-5] max exp 510, different 95 (19%)
c [score-dist-5] median active exp 403, avg 415.9
c [simplification-5] removed 65 variables 1.2% (5549 remain 59%)
c [simplification-5] removed 970 irredundant clauses 0.7% (135746 remain 90%)
c [simplification-5] maximum reduction of 1% = max (1%, 1%)
c [simplification-5] geometric conflict interval increment 13333 = 26666 / 2
c [simplification-5] new conflict interval 39999
c [simplification-5] penalized conflict interval 39999 = 1 * 39999
c [simplification-5] hard conflict limit 109668 (soft 89669 + delta 19999)
c [simplification-5] new conflict limit 89669 (hard 109668)
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 -   11.9    5549   135746     58936   25420   1075  3033   15    19   14  79%    601    8   15    9  174%
c 
c [simplification-6] limit 89669 conflicts (hard 109668) hit after 89671 conflicts
c [quatres-4] found 25747 quaternary clauses 28% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-2] added 2 single-self-subsuming ternary resolvents
c [quatres-4-2] added 8 quaternary resolvents
c [card-3] limit 766768 penalty 2 = 2 + 0
c [card-3] found 679 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 766768 for elimination
c [card-3] 679 out of 679 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-18] removed 2 variables
c [treelook-3] limit 613414 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 11003 literals 99%
c [treelook-3] scheduling used 455306 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 613414 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 618087 steps
c [treelook-3] 10934 literals remain 99%
c [treelook-3] 5293 variables remain to probed next time 95%
c [decomp-19] removed 2 variables
c [treelook-3] removed 2 variables, found 109 hbrs
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 377 transitive binary clauses
c [bca-5] limit of 10000000 steps and 271856 added (scaled 2)
c [bca-5] 9700 out of 11092 literals actually usable 87%
c [bca-5] added 0 blocked clauses in 77193 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 18402440 penalty 0 = 0 + 0
c [sweep-5-1] 1611 pos 49.2% + 1661 neg 50.8% = 3272 sched 59.0% ret 2273
c [sweep-5-1] 18035477 steps 926 queries 34.36 avg class size
c [sweep-5-1] 20798 decisions 872 SAT calls 54.55 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-20] removed 65 variables
c [sweep-5-1] removed 65 vars (0 failed, 67 eqs, 25 impls)
c [sweep-5-2] 2879 pos 52.5% + 2601 neg 47.5% = 5480 sched 100.0% ret 0
c [sweep-5-2] 838974 steps 41 queries 994.83 avg class size
c [sweep-5-2] 1289 decisions 42 SAT calls 60.21 avg env size
c [sweep-5-2] 5217 variables remain 95% (263 retained 5%)
c [decomp-21] removed 1 variables
c [sweep-5-2] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-5] removed 66 vars in TOTAL (2 rounds, 965 queries)
c [phase-count-6] 121258 negative 89.4% of 135583 except 14325 10.6%
c [phase-count-6] 124958 positive 92.2% of 135583 except 10625 7.8%
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-6] sorted 3378 enqueued variables after 89671 conflicts
c [score-dist-6] active 2101 (38%), one 0 (0%), zero 3378 (62%)
c [score-dist-6] max exp 511, different 76 (15%)
c [score-dist-6] median active exp 504, avg 450.9
c [simplification-6] removed 70 variables 1.3% (5479 remain 58%)
c [simplification-6] removed 163 irredundant clauses 0.1% (135583 remain 90%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 19999 = 39999 / 2
c [simplification-6] new conflict interval 59998
c [simplification-6] penalized conflict interval 59998 = 1 * 59998
c [simplification-6] hard conflict limit 179668 (soft 149669 + delta 29999)
c [simplification-6] new conflict limit 149669 (hard 179668)
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 -   16.1    5479   135583     89671   27489   1122  2969   15    19   10  78%    759    5   16   11  143%
c -   18.8    5479   135583    119687   28028   1143  2969   14    17   15  78%    857    1   12   12  101%
c 
c [simplification-7] limit 149669 conflicts (hard 179668) hit after 150519 conflicts
c [quatres-5] found 25972 quaternary clauses 28% in total
c [quatres-5-2] added 3 single-self-subsuming ternary resolvents
c [quatres-5-2] added 8 quaternary resolvents
c [ternres-4] limit 5277941 with penalty 1 = 1 + 0
c [ternres-4] all 5479 free variables schedulable
c [ternres-4] 12 ternary resolvents (0 bin, 12 trn)
c [ternres-4] 790 variables remain 14% (4689 retained 86%)
c [basicprobe-3] limit 52779411 penalty 0 = 0 + 0
c [basicprobe-3-0] 460 sched 8%, 4 failed, 0 lifted, 215 hbrs
c [decomp-23] removed 4 variables
c [basicprobe-3-1] 1009 sched 18%, 4 failed, 0 lifted, 133 hbrs
c [decomp-24] removed 4 variables
c [basicprobe-3-2] 1012 sched 19%, 3 failed, 0 lifted, 96 hbrs
c [decomp-25] removed 3 variables
c [basicprobe-3-3] 1012 sched 19%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-3-4] 1012 sched 19%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-3-5] 1012 sched 19%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-6] 1012 sched 19%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-3-7] 1012 sched 19%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-7] fully completed probing
c [basicprobe-3-7] 11 units = 11 failed (100%) + 0 lifted (0%)
c [basicprobe-3-7] removed 11 variables, found 458 hbrs
c [bate-2] eliminated 130 asymmetric tautologies during probing
c [unhide-4] limit 527794 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 406 tauts, 0 hbrs, 8133 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 246 transitive binary clauses
c [cce-3] limit of 13194852 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 42 clauses out of 265 (16%) of length 13
c [cce-3-1] eliminated 36 clauses out of 707 (5%) of length 12
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 78 large clauses in 13194852 steps
c [cce-3-1] allowing another 6597426 steps for small clauses
c [cce-3-1] scheduling 14491 clauses = 10866 binary + 3625 ternary
c [cce-3-1] tried to eliminate 1114 small clauses 8%
c [cce-3-1] eliminated 88 binary clauses 1%
c [cce-3-1] eliminated 150 ternary clauses 4%
c [cce-3-1] eliminated 238 small clauses 2%
c [cce-3-1] eliminated 238 small clauses in 13194853 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 316 covered clauses in round 1
c [cce-3] eliminated 316 covered clauses in TOTAL during 1 rounds
c [cce-3] 316 < 1/100 * 135194 = 1351 considered unsuccessful
c [sweep-6] limit 3166764 penalty 0 = 0 + 0
c [sweep-6-1] 2712 pos 52.1% + 2495 neg 47.9% = 5207 sched 95.2% ret 261
c [sweep-6-1] 3466604 steps 44 queries 737.07 avg class size
c [sweep-6-1] 1663 decisions 42 SAT calls 87.43 avg env size
c [sweep-6-1] 4788 variables remain 88% (680 retained 12%)
c [decomp-30] removed 3 variables
c [sweep-6-1] removed 3 vars (0 failed, 1 eqs, 0 impls)
c [sweep-6] 3 < 1/1000 * 5468 = 5 considered unsuccessful
c [sweep-6] removed 3 vars in TOTAL (1 rounds, 43 queries)
c [phase-count-7] 120599 negative 89.4% of 134876 except 14277 10.6%
c [phase-count-7] 124372 positive 92.2% of 134876 except 10504 7.8%
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-7] sorted 3572 enqueued variables after 150519 conflicts
c [score-dist-7] active 1893 (35%), one 247 (5%), zero 3325 (61%)
c [score-dist-7] max exp 511, different 109 (21%)
c [score-dist-7] median active exp 268, avg 336.2
c [simplification-7] removed 14 variables 0.3% (5465 remain 58%)
c [simplification-7] removed 707 irredundant clauses 0.5% (134876 remain 90%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 29999 = 59998 / 2
c [simplification-7] new conflict interval 89997
c [simplification-7] penalized conflict interval 89997 = 1 * 89997
c [simplification-7] hard conflict limit 285514 (soft 240516 + delta 44998)
c [simplification-7] new conflict limit 240516 (hard 285514)
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 -   23.4    5465   134876    151617   27933   1243  2776   13    16   15  78%    921    1   14   12  117%
c -   26.6    5465   134876    187281   30293   1261  2777   11    14   15  81%    964   -1   12   12  100%
c -   29.6    5465   134876    221669   31081   1290  2777   11    14   15  78%    989   -0   12   11  101%
c 
c [simplification-8] limit 240516 conflicts (hard 285514) hit after 240518 conflicts
c [quatres-6] found 26257 quaternary clauses 27% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 1 single-self-subsuming ternary resolvents
c [quatres-6-2] added 16 quaternary resolvents
c [ternres-5] limit 16902505 with penalty 0 = 0 + 0
c [ternres-5] 786 schedulable variables 14%
c [ternres-5] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-3] limit 845125 penalty 2 = 2 + 0
c [gauss-3] extracted 167 xors of average arity 3.0
c [gauss-3] connected 501 occurrences of 306 variables (average 1.6)
c [gauss-3] limit 845125 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-4] 3079 schedulable variables 56%
c [simpleprobe-4] limit 67610021 penalty 0 = 0 + 0
c [decomp-32] removed 58 variables
c [simpleprobe-4] 2127 variables remain 39% (3280 retained 61%)
c [simpleprobe-4] removed 58 variables, found 2758 hbrs, 0 units
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 1374 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 5407 variables 100%
c [block-4] limit of 42256263 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 441 blocked clauses
c [block-4] 441 < 1/100 * 134711 = 1347 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 5391 variables 100%
c [elim-5] limit of 84512527 steps penalty 2 = 2 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 251 not tried 5% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 15 = 0% variables out of 5391 scheduled
c [elim-5] 15 < 1/100 * 5391 = 53 considered unsuccessful
c [bca-6] limit of 10000000 steps and 267592 added (scaled 2)
c [bca-6] 8968 out of 10754 literals actually usable 83%
c [bca-6] added 0 blocked clauses in 69646 steps
c [phase-count-8] 118739 negative 88.9% of 133512 except 14773 11.1%
c [phase-count-8] 122256 positive 91.6% of 133512 except 11256 8.4%
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-8] sorted 4723 enqueued variables after 240518 conflicts
c [score-dist-8] active 653 (12%), one 1453 (27%), zero 3270 (61%)
c [score-dist-8] max exp 510, different 92 (18%)
c [score-dist-8] median active exp 500, avg 394.5
c [simplification-8] removed 89 variables 1.6% (5376 remain 57%)
c [simplification-8] removed 1364 irredundant clauses 1.0% (133512 remain 89%)
c [simplification-8] maximum reduction of 2% = max (2%, 1%)
c [simplification-8] geometric conflict interval increment 29999 = 89997 / 3
c [simplification-8] new conflict interval 119996
c [simplification-8] penalized conflict interval 119996 = 1 * 119996
c [simplification-8] hard conflict limit 420512 (soft 360514 + delta 59998)
c [simplification-8] new conflict limit 360514 (hard 420512)
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 -   34.5    5376   133512    257772   32512   1238  4020   15    19   14  79%   1004    4   15   12  125%
c -   38.0    5376   133512    296483   33625   1254  4020   12    15   14  81%   1013   -1   14   12  112%
c -   41.4    5376   133512    335469   35594   1266  4022   11    14   14  83%   1018   -1   11   12   93%
c 
c [simplification-9] limit 360514 conflicts (hard 420512) hit after 360515 conflicts
c [quatres-7] found 26117 quaternary clauses 26% in total
c [quatres-7-2] added 6 quaternary resolvents
c [treelook-4] limit 2628926 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 10683 literals 99%
c [treelook-4] scheduling used 458867 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 2628926 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 2653451 steps
c [treelook-4] 10281 literals remain 96%
c [treelook-4] 5122 variables remain to probed next time 95%
c [decomp-34] removed 2 variables
c [treelook-4] removed 3 variables, found 682 hbrs
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 853 transitive binary clauses
c [sweep-7] limit 3943390 penalty 1 = 1 + 0
c [sweep-7-1] 2430 pos 51.7% + 2274 neg 48.3% = 4704 sched 87.5% ret 669
c [sweep-7-1] 4156403 steps 60 queries 532.90 avg class size
c [sweep-7-1] 1989 decisions 59 SAT calls 79.51 avg env size
c [sweep-7-1] 4358 variables remain 81% (1014 retained 19%)
c [decomp-35] removed 4 variables
c [sweep-7-1] removed 4 vars (0 failed, 4 eqs, 1 impls)
c [sweep-7] 4 < 1/1000 * 5373 = 5 considered unsuccessful
c [sweep-7] removed 4 vars in TOTAL (1 rounds, 59 queries)
c [phase-count-9] 118685 negative 88.9% of 133493 except 14808 11.1%
c [phase-count-9] 122213 positive 91.6% of 133493 except 11280 8.4%
c [phase-9] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-9] sorted 4773 enqueued variables after 360515 conflicts
c [score-dist-9] active 596 (11%), one 1539 (29%), zero 3234 (60%)
c [score-dist-9] max exp 510, different 73 (14%)
c [score-dist-9] median active exp 505, avg 488.9
c [simplification-9] removed 7 variables 0.1% (5369 remain 57%)
c [simplification-9] removed 19 irredundant clauses 0.0% (133493 remain 89%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 119996
c [simplification-9] new conflict interval 239992
c [simplification-9] penalized conflict interval 239992 = 1 * 239992
c [simplification-9] hard conflict limit 720503 (soft 600507 + delta 119996)
c [simplification-9] new conflict limit 600507 (hard 720503)
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 -   45.7    5369   133493    375129   37539   1270  3759   13    15   15  81%   1021    1   12   12  104%
c -   49.1    5369   133493    413794   37520   1292  3759   13    18   15  75%   1022    1   13   12  108%
c -   52.7    5369   133493    453623   39221   1299  3759   11    14   15  80%   1023   -2   12   12   97%
c -   56.5    5369   133493    494394   40556   1315  3759   13    21   24  62%   1023    4   11   12   92%
c -   60.1    5369   133493    535081   41980   1326  3761   12    16   24  75%   1024   -0   12   12  101%
c -   63.9    5369   133493    575499   42874   1378  3765   12    16   24  78%   1024   -5   12   13   93%
c 
c [simplification-10] limit 600507 conflicts (hard 720503) hit after 602480 conflicts
c [quatres-8] found 26612 quaternary clauses 26% in total
c [quatres-8-2] added 1 single-self-subsuming ternary resolvents
c [quatres-8-2] added 37 quaternary resolvents
c [ternres-6] limit 22745450 with penalty 1 = 1 + 0
c [ternres-6] all 5369 free variables schedulable
c [ternres-6] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 2843181 penalty 3 = 3 + 0
c [card-4] found 631 at-most-one constraints of average size 3.2
c [card-4] found 43 at-most-two constraints of average size 4.0
c [card-4] using previous limit 2843181 for elimination
c [card-4] 674 out of 674 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-36] removed 1 variables
c [basicprobe-4] limit 227454504 penalty 0 = 0 + 0
c [basicprobe-4-0] 932 sched 17%, 2 failed, 0 lifted, 192 hbrs
c [decomp-37] removed 2 variables
c [basicprobe-4-1] 934 sched 17%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-4-2] 934 sched 17%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-3] 934 sched 17%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-4] 934 sched 17%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-4] fully completed probing
c [basicprobe-4-4] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-4-4] removed 2 variables, found 205 hbrs
c [bate-3] eliminated 6 asymmetric tautologies during probing
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 498 transitive binary clauses
c [phase-count-10] 118586 negative 88.9% of 133437 except 14851 11.1%
c [phase-count-10] 122102 positive 91.5% of 133437 except 11335 8.5%
c [phase-10] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-10] sorted 3884 enqueued variables after 602480 conflicts
c [score-dist-10] active 1482 (28%), one 1160 (22%), zero 2724 (51%)
c [score-dist-10] max exp 509, different 128 (25%)
c [score-dist-10] median active exp 502, avg 424.2
c [simplification-10] removed 3 variables 0.1% (5366 remain 57%)
c [simplification-10] removed 56 irredundant clauses 0.0% (133437 remain 89%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 239992
c [simplification-10] new conflict interval 479984
c [simplification-10] penalized conflict interval 479984 = 1 * 479984
c [simplification-10] hard conflict limit 1322456 (soft 1082464 + delta 239992)
c [simplification-10] new conflict limit 1082464 (hard 1322456)
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 -   68.8    5366   133437    617350   44128   1390  3496   13    17   16  77%   1024   -3   13   13   97%
c -   72.6    5366   133437    660017   45425   1398  3496   12    15   16  81%   1024   -3   13   13   97%
c -   76.8    5366   133437    703519   46746   1407  3496   12    15   16  80%   1024   -2   11   13   84%
c -   81.2    5366   133437    748464   48423   1422  3496   13    19   16  70%   1024    3   14   12  112%
c -   85.5    5366   133437    791557   49987   1430  3496   14    18   25  76%   1024    2   14   12  114%
c -   89.8    5366   133437    835450   50847   1436  3496   11    15   25  75%   1024   -1   12   12   96%
c -   94.2    5366   133437    879731   52034   1439  3496   12    14   25  81%   1024   -1   13   12  111%
c -   99.1    5366   133437    927642   53630   1449  3497   10    13   25  81%   1024   -2    8   11   75%
c -  104.2    5366   133437    976527   54225   1465  3498   11    14   25  80%   1024   -0   11   11  102%
c -  109.4    5366   133437   1026726   56351   1473  3498   11    13   26  81%   1024   -0   14   11  128%
c -  114.2    5366   133437   1073710   57651   1477  3498   11    13   26  83%   1024   -1   13   11  112%
c 
c [simplification-11] limit 1082464 conflicts (hard 1322456) hit after 1082465 conflicts
c [quatres-9] found 27047 quaternary clauses 24% in total
c [quatres-9-2] added 3 single-self-subsuming ternary resolvents
c [quatres-9-2] added 11 quaternary resolvents
c [ternres-7] limit 90842876 with penalty 0 = 0 + 0
c [ternres-7] all 5366 free variables schedulable
c [ternres-7] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-7] fully completed ternary resolution
c [simpleprobe-5] 2116 schedulable variables 39%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-42] removed 21 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 21 variables, found 3237 hbrs, 0 units
c [unhide-5] limit 2271071 with penalty 3 = 3 + 0
c [unhide-5-6] 0 units, 0 failed, 2590 tauts, 0 hbrs, 13269 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 778 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 567767975 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 67 clauses out of 468 (14%) of length 13
c [cce-4-1] eliminated 15 clauses out of 674 (2%) of length 12
c [cce-4-1] eliminated 13 clauses out of 125 (10%) of length 11
c [cce-4-1] eliminated 5 clauses out of 226 (2%) of length 10
c [cce-4-1] eliminated 14 clauses out of 1578 (1%) of length 9
c [cce-4-1] eliminated 132 clauses out of 3489 (4%) of length 8
c [cce-4-1] eliminated 142 clauses out of 7895 (2%) of length 7
c [cce-4-1] eliminated 440 clauses out of 18363 (2%) of length 6
c [cce-4-1] eliminated 1669 clauses out of 30808 (5%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 2497 large clauses in 567768033 steps
c [cce-4-1] allowing another 283884016 steps for small clauses
c [cce-4-1] scheduling 41572 clauses = 10549 binary + 31023 ternary
c [cce-4-1] tried to eliminate 41572 small clauses 100%
c [cce-4-1] eliminated 301 binary clauses 3%
c [cce-4-1] eliminated 1826 ternary clauses 6%
c [cce-4-1] eliminated 2127 small clauses 5%
c [cce-4-1] eliminated 2127 small clauses in 446517113 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 4624 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 60625760 steps for small clauses
c [cce-4-2] scheduling 39445 clauses = 10248 binary + 29197 ternary
c [cce-4-2] tried to eliminate 15711 small clauses 40%
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 4624 covered clauses in TOTAL during 2 rounds
c [bca-7] limit of 10000000 steps and 257992 added (scaled 2)
c [bca-7] 8222 out of 10692 literals actually usable 77%
c [bca-7] added 0 blocked clauses in 83754 steps
c [phase-count-11] 114501 negative 89.0% of 128712 except 14211 11.0%
c [phase-count-11] 117490 positive 91.3% of 128712 except 11222 8.7%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-11] sorted 4844 enqueued variables after 1082465 conflicts
c [score-dist-11] active 501 (9%), one 2134 (40%), zero 2710 (51%)
c [score-dist-11] max exp 510, different 91 (18%)
c [score-dist-11] median active exp 504, avg 482.8
c [simplification-11] removed 21 variables 0.4% (5345 remain 57%)
c [simplification-11] removed 4725 irredundant clauses 3.5% (128712 remain 86%)
c [simplification-11] maximum reduction of 4% = max (0%, 4%)
c [simplification-11] geometric conflict interval increment 95996 = 479984 / 5
c [simplification-11] new conflict interval 575980
c [simplification-11] penalized conflict interval 575980 = 1 * 575980
c [simplification-11] hard conflict limit 1946435 (soft 1658445 + delta 287990)
c [simplification-11] new conflict limit 1658445 (hard 1946435)
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 -  127.2    5345   128712   1120646   58306   3311  3603   12    15   16  81%   1024   -0   11   12   91%
c -  132.6    5345   128712   1170525   58064   3323  3603   12    14   25  84%   1024   -2   11   13   89%
c -  138.0    5345   128712   1222985   59450   3327  3604   12    15   25  78%   1024   -0   12   12  104%
c -  143.5    5345   128712   1272442   61313   3338  3604   13    23   25  56%   1024    8   11   12   92%
c -  150.1    5345   128712   1325353   62779   3342  3604   11    13   26  81%   1024   -1   10   11   94%
c -  155.9    5345   128712   1375805   63416   3349  3605   13    19   26  68%   1024    3   12   12  108%
c -  162.4    5345   128712   1430690   64950   3354  3605   10    12   26  82%   1024   -3    9   11   82%
c -  168.3    5345   128712   1485312   65880   3358  3605   16    32   26  50%   1024   16   13   12  104%
c -  174.2    5345   128712   1538640   67468   3373  3605   11    13   26  81%   1024   -3   11   12   89%
c -  180.3    5345   128712   1593309   68190   3381  3605   11    14   26  79%   1024   -1   11   12   96%
c -  186.9    5345   128712   1649527   69225   3385  3605   12    14   26  83%   1024   -0   12   12  103%
c 
c [simplification-12] limit 1658445 conflicts (hard 1946435) hit after 1681948 conflicts
c [quatres-10] found 27539 quaternary clauses 24% in total
c [quatres-10-1] removed 4 duplicate quaternary clauses
c [quatres-10-2] added 1 single-self-subsuming ternary resolvents
c [quatres-10-2] added 14 quaternary resolvents
c [ternres-8] limit 155746525 with penalty 0 = 0 + 0
c [ternres-8] all 5345 free variables schedulable
c [ternres-8] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-4] limit 3893663 penalty 3 = 3 + 0
c [gauss-4] extracted 518 xors of average arity 3.0
c [gauss-4] connected 1554 occurrences of 481 variables (average 3.2)
c [gauss-4] limit 3893663 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-43] removed 2 variables
c [treelook-5] limit 15574652 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 10632 literals 99%
c [treelook-5] scheduling used 532807 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 15574652 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 15575706 steps
c [treelook-5] 6260 literals remain 59%
c [treelook-5] 4326 variables remain to probed next time 81%
c [decomp-44] removed 7 variables
c [treelook-5] removed 7 variables, found 1268 hbrs
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 673 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 5336 variables 100%
c [block-5] limit of 100000000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 209 blocked clauses
c [block-5] 209 < 1/100 * 128704 = 1287 considered unsuccessful
c [elim-6] 249 variables 5% will be scheduled this time
c [elim-6] scheduled 249 variables 5%
c [elim-6] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 123 not tried 2% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 249 scheduled
c [sweep-8] limit 11680989 penalty 2 = 2 + 0
c [sweep-8-1] 2287 pos 52.8% + 2042 neg 47.2% = 4329 sched 81.2% ret 1004
c [sweep-8-1] 11743253 steps 579 queries 43.92 avg class size
c [sweep-8-1] 13967 decisions 598 SAT calls 54.07 avg env size
c [sweep-8-1] 553 variables remain 10% (4780 retained 90%)
c [decomp-45] removed 17 variables
c [sweep-8-1] removed 17 vars (0 failed, 19 eqs, 0 impls)
c [sweep-8] removed 17 vars in TOTAL (1 rounds, 578 queries)
c [phase-count-12] 114279 negative 89.0% of 128474 except 14195 11.0%
c [phase-count-12] 117225 positive 91.2% of 128474 except 11249 8.8%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 3597 enqueued variables after 1681948 conflicts
c [score-dist-12] active 1719 (32%), one 1128 (21%), zero 2469 (46%)
c [score-dist-12] max exp 510, different 65 (13%)
c [score-dist-12] median active exp 504, avg 500.2
c [simplification-12] removed 29 variables 0.5% (5316 remain 56%)
c [simplification-12] removed 238 irredundant clauses 0.2% (128474 remain 85%)
c [simplification-12] maximum reduction of 1% = max (1%, 0%)
c [simplification-12] geometric conflict interval increment 287990 = 575980 / 2
c [simplification-12] new conflict interval 863970
c [simplification-12] penalized conflict interval 863970 = 1 * 863970
c [simplification-12] hard conflict limit 2977903 (soft 2545918 + delta 431985)
c [simplification-12] new conflict limit 2545918 (hard 2977903)
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 -  196.5    5316   128474   1705980   70685   3508  4201   13    16   18  79%   1024    1   12   12  102%
c -  202.5    5316   128474   1760118   71649   3509  4201   12    15   18  78%   1024    0   12   12   98%
c -  208.8    5316   128474   1815462   73465   3515  4201   11    14   29  80%   1024   -0   10   11   88%
c -  215.3    5316   128474   1872624   74423   3523  4201   10    13   29  79%   1024   -1   10   12   84%
c -  223.0    5316   128474   1930726   75698   3551  4201   11    38   29  28%   1024   11   10   13   78%
c -  230.3    5316   128474   1992050   79721   3567  4203   11    15   29  76%   1024   -7   13   12  103%
c -  237.4    5316   128474   2050485   80563   3571  4203   10    13   29  82%   1024   -4   11   11  101%
c -  244.9    5316   128474   2109042   81235   3608  4203   16    27   29  58%   1024    7   15   13  116%
c -  253.3    5316   128474   2169106   83243   3656  4203   12    38   29  31%   1024    9   12   14   83%
c -  261.4    5316   128474   2232363   86055   3666  4203   11    16   29  71%   1024  -10   13   13  101%
c -  271.2    5316   128474   2292875   87496   3733  4203   14    19   30  75%   1024  -15   12   18   65%
c -  278.8    5316   128474   2357128   90414   3741  4204   12    33   30  36%   1024    6   13   14   88%
c -  287.9    5316   128474   2423720   91942   3756  4204   11    13   30  83%   1024   -7   12   12   94%
c -  297.8    5316   128474   2491927   94412   3776  4205   12    16   30  75%   1024   -4   11   13   80%
c 
c [simplification-13] limit 2545918 conflicts (hard 2977903) hit after 2545919 conflicts
c [quatres-11] found 28848 quaternary clauses 21% in total
c [quatres-11-1] removed 3 duplicate quaternary clauses
c [quatres-11-2] added 8 single-self-subsuming ternary resolvents
c [quatres-11-2] added 17 quaternary resolvents
c [ternres-9] limit 200000000 with penalty 0 = 0 + 0
c [ternres-9] all 5316 free variables schedulable
c [ternres-9] 12 ternary resolvents (0 bin, 12 trn)
c [ternres-9] fully completed ternary resolution
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 852 sched 16%, 1 failed, 0 lifted, 52 hbrs
c [decomp-47] removed 1 variables
c [basicprobe-5-1] 853 sched 16%, 0 failed, 0 lifted, 18 hbrs
c [basicprobe-5-2] 853 sched 16%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-2] fully completed probing
c [basicprobe-5-2] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-5-2] removed 1 variables, found 70 hbrs
c [bate-4] eliminated 8 asymmetric tautologies during probing
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 329 transitive binary clauses
c [cce-5] limit of 318176447 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 182 clauses out of 401 (45%) of length 13
c [cce-5-1] eliminated 10 clauses out of 659 (2%) of length 12
c [cce-5-1] eliminated 16 clauses out of 112 (14%) of length 11
c [cce-5-1] eliminated 50 clauses out of 221 (23%) of length 10
c [cce-5-1] eliminated 212 clauses out of 1548 (14%) of length 9
c [cce-5-1] eliminated 459 clauses out of 3348 (14%) of length 8
c [cce-5-1] eliminated 1001 clauses out of 7749 (13%) of length 7
c [cce-5-1] eliminated 5788 clauses out of 17872 (32%) of length 6
c [cce-5-1] eliminated 164 clauses out of 29144 (1%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 7882 large clauses in 318176566 steps
c [cce-5-1] allowing another 159088283 steps for small clauses
c [cce-5-1] scheduling 39250 clauses = 10203 binary + 29047 ternary
c [cce-5-1] tried to eliminate 39250 small clauses 100%
c [cce-5-1] eliminated 574 binary clauses 6%
c [cce-5-1] eliminated 3475 ternary clauses 12%
c [cce-5-1] eliminated 4049 small clauses 10%
c [cce-5-1] eliminated 4049 small clauses in 300787773 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 11931 covered clauses in round 1
c [cce-5-2] incomplete large round (ACCE)
c [cce-5-2] allowing another 8694531 steps for small clauses
c [cce-5-2] scheduling 35201 clauses = 9629 binary + 25572 ternary
c [cce-5-2] tried to eliminate 2775 small clauses 8%
c [cce-5-2] eliminated 1 binary clauses 0%
c [cce-5-2] eliminated 5 ternary clauses 0%
c [cce-5-2] eliminated 6 small clauses 0%
c [cce-5-2] eliminated 6 small clauses in 17388683 steps
c [cce-5-2] incomplete small round (ACCE)
c [cce-5-2] eliminated 6 covered clauses in round 2
c [cce-5] eliminated 11937 covered clauses in TOTAL during 2 rounds
c [phase-count-13] 102993 negative 88.5% of 116397 except 13404 11.5%
c [phase-count-13] 106799 positive 91.8% of 116397 except 9598 8.2%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 3279 enqueued variables after 2545919 conflicts
c [score-dist-13] active 2036 (38%), one 996 (19%), zero 2283 (43%)
c [score-dist-13] max exp 510, different 169 (33%)
c [score-dist-13] median active exp 476, avg 442.1
c [simplification-13] removed 1 variables 0.0% (5315 remain 56%)
c [simplification-13] removed 12077 irredundant clauses 9.4% (116397 remain 77%)
c [simplification-13] maximum reduction of 9% = max (0%, 9%)
c [simplification-13] large reduction 9% >= 5% limit
c [simplification-13] next conflict interval 25459 = min (2545919/100, 863970)
c [simplification-13] penalized conflict interval 25459 = 1 * 25459
c [simplification-13] hard conflict limit 2584107 (soft 2571378 + delta 12729)
c [simplification-13] new conflict limit 2571378 (hard 2584107)
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 -  311.1    5315   116397   2553998   95640   7280  4545   13    19   21  67%   1024   -4   12   14   90%
c 
c [simplification-14] limit 2571378 conflicts (hard 2584107) hit after 2575426 conflicts
c [quatres-12] found 28763 quaternary clauses 22% in total
c [quatres-12-2] added 1 single-self-subsuming ternary resolvents
c [quatres-12-2] added 4 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 5315 free variables schedulable
c [ternres-10] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-10] fully completed ternary resolution
c [simpleprobe-6] all 5315 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-50] removed 1 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 1 variables, found 3489 hbrs, 0 units
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 1769 transitive binary clauses
c [cce-6] limit of 644504947 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 48 clauses out of 28980 (0%) of length 5
c [cce-6-1] eliminated 878 clauses out of 24801 (4%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 926 large clauses in 574286588 steps
c [cce-6-1] allowing another 287143294 steps for small clauses
c [cce-6-1] scheduling 35196 clauses = 9628 binary + 25568 ternary
c [cce-6-1] tried to eliminate 35196 small clauses 100%
c [cce-6-1] completed small round (ATE)
c [cce-6-1] completed small and large (ATE)
c [cce-6-1] eliminated 926 covered clauses in round 1
c [cce-6-2] incomplete large round (ATE)
c [cce-6-2] allowing another 126151047 steps for small clauses
c [cce-6-2] scheduling 35196 clauses = 9628 binary + 25568 ternary
c [cce-6-2] tried to eliminate 35196 small clauses 100%
c [cce-6-2] completed small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 926 covered clauses in TOTAL during 2 rounds
c [cce-6] 926 < 1/100 * 116397 = 1163 considered unsuccessful
c [sweep-9] limit 38670296 penalty 1 = 1 + 0
c [sweep-9-1] 260 pos 47.0% + 293 neg 53.0% = 553 sched 10.4% ret 4761
c [sweep-9-1] 4549753 steps 318 queries 14.83 avg class size
c [sweep-9-1] 7475 decisions 317 SAT calls 60.62 avg env size
c [sweep-9-1] fully completed sweeping round
c [sweep-9-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-9-2] 2933 pos 55.2% + 2381 neg 44.8% = 5314 sched 100.0% ret 0
c [sweep-9-2] 21426306 steps 869 queries 28.73 avg class size
c [sweep-9-2] 22016 decisions 878 SAT calls 61.75 avg env size
c [sweep-9-2] fully completed sweeping round
c [decomp-52] removed 10 variables
c [sweep-9-2] removed 10 vars (0 failed, 11 eqs, 5 impls)
c [sweep-9-3] 2928 pos 55.2% + 2376 neg 44.8% = 5304 sched 100.0% ret 0
c [sweep-9-3] 13131646 steps 364 queries 66.55 avg class size
c [sweep-9-3] 9495 decisions 365 SAT calls 65.37 avg env size
c [sweep-9-3] 1404 variables remain 26% (3900 retained 74%)
c [decomp-53] removed 2 variables
c [sweep-9-3] removed 2 vars (0 failed, 5 eqs, 1 impls)
c [sweep-9] removed 12 vars in TOTAL (3 rounds, 1548 queries)
c [phase-count-14] 102168 negative 88.5% of 115469 except 13301 11.5%
c [phase-count-14] 105910 positive 91.7% of 115469 except 9559 8.3%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-14] sorted 2779 enqueued variables after 2575426 conflicts
c [score-dist-14] active 2523 (48%), one 699 (13%), zero 2080 (39%)
c [score-dist-14] max exp 512, different 138 (27%)
c [score-dist-14] median active exp 504, avg 464.7
c [simplification-14] removed 13 variables 0.2% (5302 remain 56%)
c [simplification-14] removed 928 irredundant clauses 0.8% (115469 remain 77%)
c [simplification-14] maximum reduction of 1% = max (0%, 1%)
c [simplification-14] geometric conflict interval increment 431985 = 863970 / 2
c [simplification-14] conflict interval soft limit 1000000 reached
c [simplification-14] new conflict interval 1000000
c [simplification-14] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-14] hard conflict limit 4075426 (soft 3575426 + delta 500000)
c [simplification-14] new conflict limit 3575426 (hard 4075426)
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 -  331.0    5302   115469   2616884   97682   7284  6325   13    29   21  44%   1024    4   14   15   95%
c -  341.7    5302   115469   2682642  100091   7348  6325   18    33   33  55%   1024    3   18   17  105%
c -  353.9    5302   115469   2748734  102592   7377  6327   18    27   33  67%   1024   -2   16   18   91%
c -  368.7    5302   115469   2818673  104269   7386  6327   17    25   33  68%   1024   -0   19   18  102%
c -  383.6    5302   115469   2887423  105822   7392  6327   16    21   34  74%   1024   -3   17   18   95%
c -  396.2    5302   115469   2952981  107250   7432  6330   21    39   34  54%   1024    8   21   19  112%
c -  404.2    5302   115469   3023872  110854   7451  6330   11    15   33  77%   1024   -9   11   14   79%
c -  414.2    5302   115469   3095879  113393   7464  6331   23    36   33  63%   1024   18   25   13  191%
c -  423.9    5302   115469   3162857  114202   7485  6332   14    26   33  52%   1024    6   14   14  101%
c -  435.3    5302   115469   3231696  115102   7504  6332   15    24   34  64%   1024   -2   16   15  104%
c -  447.7    5302   115469   3301157  115742   7539  6332   21    29   34  73%   1024    2   21   17  127%
c -  461.5    5302   115469   3370826  116524   7579  6332   26    39   34  66%   1024    7   28   19  145%
c -  476.4    5302   115469   3444290  118232   7599  6333   17    22   34  77%   1024   -3   18   18  101%
c -  491.4    5302   115469   3515743  118762   7638  6335   22    37   34  60%   1024    6   22   19  116%
c 
c [simplification-15] limit 3575426 conflicts (hard 4075426) hit after 3576614 conflicts
c [quatres-13] found 29301 quaternary clauses 20% in total
c [quatres-13-2] added 8 single-self-subsuming ternary resolvents
c [quatres-13-2] added 9 quaternary resolvents
c [card-5] limit 11491479 penalty 4 = 4 + 0
c [card-5] found 652 at-most-one constraints of average size 3.2
c [card-5] found 40 at-most-two constraints of average size 4.0
c [card-5] using previous limit 11491479 for elimination
c [card-5] 692 out of 692 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [treelook-6] limit 36772734 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 10203 literals 96%
c [treelook-6] scheduling used 666745 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 36772734 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 17930016 steps
c [treelook-6] fully completed tree based probing
c [decomp-55] removed 1 variables
c [treelook-6] removed 1 variables, found 264 hbrs
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 915 transitive binary clauses
c [bca-8] limit of 10000000 steps and 231366 added (scaled 2)
c [bca-8] 6431 out of 10604 literals actually usable 61%
c [bca-8] added 0 blocked clauses in 188759 steps
c [sweep-10] limit 110318203 penalty 0 = 0 + 0
c [sweep-10-1] 720 pos 51.3% + 683 neg 48.7% = 1403 sched 26.5% ret 3898
c [sweep-10-1] 11337194 steps 538 queries 16.44 avg class size
c [sweep-10-1] 14135 decisions 541 SAT calls 65.19 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-56] removed 7 variables
c [sweep-10-1] removed 7 vars (0 failed, 4 eqs, 0 impls)
c [sweep-10-2] 2943 pos 55.6% + 2351 neg 44.4% = 5294 sched 100.0% ret 0
c [sweep-10-2] 17683102 steps 784 queries 29.68 avg class size
c [sweep-10-2] 21840 decisions 795 SAT calls 69.53 avg env size
c [sweep-10-2] fully completed sweeping round
c [decomp-57] removed 7 variables
c [sweep-10-2] removed 7 vars (0 failed, 10 eqs, 1 impls)
c [sweep-10-3] 2940 pos 55.6% + 2347 neg 44.4% = 5287 sched 100.0% ret 0
c [sweep-10-3] 20027379 steps 742 queries 31.63 avg class size
c [sweep-10-3] 20641 decisions 762 SAT calls 69.73 avg env size
c [sweep-10-3] fully completed sweeping round
c [decomp-58] removed 11 variables
c [sweep-10-3] removed 11 vars (0 failed, 14 eqs, 0 impls)
c [sweep-10] removed 25 vars in TOTAL (3 rounds, 2061 queries)
c [sort-queue-15] sorted 2430 enqueued variables after 3576614 conflicts
c [score-dist-15] active 2846 (54%), one 688 (13%), zero 1742 (33%)
c [score-dist-15] max exp 512, different 186 (36%)
c [score-dist-15] median active exp 505, avg 477.0
c [simplification-15] removed 26 variables 0.5% (5276 remain 56%)
c [simplification-15] removed 81 irredundant clauses 0.1% (115388 remain 77%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 1000000
c [simplification-15] conflict interval soft limit 1000000 reached
c [simplification-15] new conflict interval 1000000
c [simplification-15] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-15] hard conflict limit 5076614 (soft 4576614 + delta 500000)
c [simplification-15] new conflict limit 4576614 (hard 5076614)
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 -  507.8    5276   115388   3585492  121329   7612  5784   22    37   25  58%   1024    5   18   19   94%
c -  520.7    5276   115388   3660671  125898   7652  5784   11    23   26  45%   1024   -7   13   16   83%
c -  534.8    5276   115388   3732742  127281   7667  5784   19    34   40  55%   1024    8   24   16  146%
c -  550.8    5276   115388   3807428  128020   7679  5784   19    26   40  75%   1024   -1   20   18  110%
c -  565.6    5276   115388   3881499  129429   7692  5785   13    19   40  68%   1024   -7   13   17   75%
c -  579.8    5276   115388   3957316  131227   7712  5785   18    23   40  80%   1024   -3   17   18   97%
c -  597.1    5276   115388   4031774  132384   7727  5786   23    38   40  61%   1024   10   20   18  109%
c -  611.9    5276   115388   4104511  133121   7743  5786   18    33   40  54%   1024    0   17   19   92%
c -  626.8    5276   115388   4177086  134627   7749  5786   20    44   40  46%   1024    9   24   19  126%
c -  645.2    5276   115388   4254831  135374   7768  5787   20    35   40  58%   1024   -0   22   21  101%
c -  658.2    5276   115388   4331970  138190   7775  5788   18    33   40  53%   1024   -1   19   19  102%
c -  675.4    5276   115388   4407658  139250   7781  5788   25    32   40  78%   1024   -2   24   21  111%
c -  699.8    5276   115388   4488932  140121   7785  5788   22    25   41  86%   1024   -5   21   22   93%
c -  723.8    5276   115388   4570185  139828   7798  5788   22    25   41  86%   1024   -2   21   23   91%
c 
c [simplification-16] limit 4576614 conflicts (hard 5076614) hit after 4578897 conflicts
c [quatres-14] found 29989 quaternary clauses 19% in total
c [quatres-14-1] removed 2 duplicate quaternary clauses
c [quatres-14-2] added 21 single-self-subsuming ternary resolvents
c [quatres-14-2] added 26 quaternary resolvents
c [ternres-11] limit 100000000 with penalty 1 = 1 + 0
c [ternres-11] all 5276 free variables schedulable
c [ternres-11] 56 ternary resolvents (0 bin, 56 trn)
c [ternres-11] fully completed ternary resolution
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 850 sched 16%, 1 failed, 0 lifted, 37 hbrs
c [decomp-60] removed 1 variables
c [basicprobe-6-1] 850 sched 16%, 1 failed, 0 lifted, 2 hbrs
c [decomp-61] removed 1 variables
c [basicprobe-6-2] 850 sched 16%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-6-3] 850 sched 16%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-3] fully completed probing
c [basicprobe-6-3] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-6-3] removed 2 variables, found 41 hbrs
c [bate-5] eliminated 3 asymmetric tautologies during probing
c [unhide-6] limit 1250000 with penalty 4 = 4 + 0
c [unhide-6-7] 0 units, 0 failed, 1440 tauts, 0 hbrs, 18905 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 344 transitive binary clauses
c [cce-7] limit of 536870911 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 6 clauses out of 2897 (0%) of length 8
c [cce-7-1] eliminated 97 clauses out of 12066 (1%) of length 6
c [cce-7-1] eliminated 11317 clauses out of 28944 (39%) of length 5
c [cce-7-1] eliminated 9886 clauses out of 23767 (42%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 21306 large clauses in 536054597 steps
c [cce-7-1] allowing another 268027298 steps for small clauses
c [cce-7-1] scheduling 35056 clauses = 9621 binary + 25435 ternary
c [cce-7-1] tried to eliminate 35056 small clauses 100%
c [cce-7-1] eliminated 46 binary clauses 0%
c [cce-7-1] eliminated 330 ternary clauses 1%
c [cce-7-1] eliminated 376 small clauses 1%
c [cce-7-1] eliminated 376 small clauses in 357905836 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 21682 covered clauses in round 1
c [cce-7-2] eliminated 16 clauses out of 11969 (0%) of length 6
c [cce-7-2] incomplete large round (ACCE)
c [cce-7-2] eliminated 16 large clauses in 178965092 steps
c [cce-7-2] allowing another 89482546 steps for small clauses
c [cce-7-2] scheduling 34680 clauses = 9575 binary + 25105 ternary
c [cce-7-2] tried to eliminate 34680 small clauses 100%
c [cce-7-2] eliminated 6 binary clauses 0%
c [cce-7-2] eliminated 5 ternary clauses 0%
c [cce-7-2] eliminated 11 small clauses 0%
c [cce-7-2] eliminated 11 small clauses in 175706046 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 27 covered clauses in round 2
c [cce-7-3] incomplete large round (ACCE)
c [cce-7-3] allowing another 1629671 steps for small clauses
c [cce-7-3] scheduling 34669 clauses = 9569 binary + 25100 ternary
c [cce-7-3] tried to eliminate 569 small clauses 2%
c [cce-7-3] incomplete small round (ACCE)
c [cce-7-3] eliminated 0 covered clauses in round 3
c [cce-7] eliminated 21709 covered clauses in TOTAL during 3 rounds
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 1485274380 penalty 0 = 0 + 0
c [sweep-11-1] 2939 pos 55.7% + 2335 neg 44.3% = 5274 sched 100.0% ret 0
c [sweep-11-1] 16675713 steps 844 queries 21.59 avg class size
c [sweep-11-1] 21048 decisions 841 SAT calls 60.56 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-63] removed 4 variables
c [sweep-11-1] removed 4 vars (0 failed, 5 eqs, 2 impls)
c [sweep-11-2] 2938 pos 55.7% + 2332 neg 44.3% = 5270 sched 100.0% ret 0
c [sweep-11-2] 20641008 steps 858 queries 33.81 avg class size
c [sweep-11-2] 22583 decisions 859 SAT calls 62.08 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-64] removed 4 variables
c [sweep-11-2] removed 4 vars (0 failed, 5 eqs, 1 impls)
c [sweep-11-3] 2936 pos 55.8% + 2330 neg 44.2% = 5266 sched 100.0% ret 0
c [sweep-11-3] 17931646 steps 872 queries 34.48 avg class size
c [sweep-11-3] 22165 decisions 867 SAT calls 59.86 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-65] removed 3 variables
c [sweep-11-3] removed 3 vars (0 failed, 6 eqs, 2 impls)
c [sweep-11] removed 11 vars in TOTAL (3 rounds, 2571 queries)
c [sort-queue-16] sorted 2675 enqueued variables after 4578897 conflicts
c [score-dist-16] active 2588 (49%), one 1155 (22%), zero 1520 (29%)
c [score-dist-16] max exp 512, different 115 (22%)
c [score-dist-16] median active exp 504, avg 489.8
c [simplification-16] removed 13 variables 0.2% (5263 remain 56%)
c [simplification-16] removed 21848 irredundant clauses 18.9% (93540 remain 62%)
c [simplification-16] maximum reduction of 19% = max (0%, 19%)
c [simplification-16] large reduction 19% >= 5% limit
c [simplification-16] next conflict interval 45788 = min (4578897/100, 1000000)
c [simplification-16] penalized conflict interval 45788 = 1 * 45788
c [simplification-16] hard conflict limit 4647579 (soft 4624685 + delta 22894)
c [simplification-16] new conflict limit 4624685 (hard 4647579)
c 
c [simplification-17] limit 4624685 conflicts (hard 4647579) hit after 4624685 conflicts
c [quatres-15] found 20222 quaternary clauses 15% in total
c [quatres-15-1] removed 12 duplicate quaternary clauses
c [quatres-15-2] added 11 single-self-subsuming ternary resolvents
c [quatres-15-2] added 41 quaternary resolvents
c [ternres-12] limit 200000000 with penalty 0 = 0 + 0
c [ternres-12] all 5263 free variables schedulable
c [ternres-12] 30 ternary resolvents (1 bin, 29 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-5] limit 3125000 penalty 4 = 4 + 0
c [gauss-5] extracted 526 xors of average arity 3.0
c [gauss-5] connected 1566 occurrences of 489 variables (average 3.2)
c [gauss-5] limit 3125000 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-7] all 5263 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-67] removed 3 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 3 variables, found 2725 hbrs, 0 units
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 1525 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 5260 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 32 blocked clauses
c [block-6] 32 < 1/100 * 93533 = 935 considered unsuccessful
c [cce-8] boosting limit by 10
c [cce-8] limit of 10737418235 steps penalty 1 = 1 + 0
c [cce-8-1] eliminated 5 clauses out of 11948 (0%) of length 6
c [cce-8-1] eliminated 12 clauses out of 17598 (0%) of length 5
c [cce-8-1] eliminated 10 clauses out of 13857 (0%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 27 large clauses in 327420114 steps
c [cce-8-1] allowing another 163710057 steps for small clauses
c [cce-8-1] scheduling 12946 clauses = 9562 binary + 3384 ternary
c [cce-8-1] tried to eliminate 12946 small clauses 100%
c [cce-8-1] eliminated 2 binary clauses 0%
c [cce-8-1] eliminated 133 ternary clauses 4%
c [cce-8-1] eliminated 135 small clauses 1%
c [cce-8-1] eliminated 135 small clauses in 202509579 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 162 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 163581668 steps for small clauses
c [cce-8-2] scheduling 12811 clauses = 9560 binary + 3251 ternary
c [cce-8-2] tried to eliminate 12811 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 162 covered clauses in TOTAL during 2 rounds
c [cce-8] 162 < 1/100 * 93501 = 935 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 5252 variables 100%
c [elim-7] limit of 50000000 steps penalty 4 = 4 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 188 not tried 4% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 72 = 1% variables out of 5252 scheduled
c [sweep-12] limit 150304395 penalty 0 = 0 + 0
c [sweep-12-1] 2884 pos 55.7% + 2296 neg 44.3% = 5180 sched 100.0% ret 0
c [sweep-12-1] 19448120 steps 832 queries 37.78 avg class size
c [sweep-12-1] 21656 decisions 836 SAT calls 62.14 avg env size
c [sweep-12-1] fully completed sweeping round
c [sweep-12-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-12-2] 2884 pos 55.7% + 2296 neg 44.3% = 5180 sched 100.0% ret 0
c [sweep-12-2] 22021368 steps 837 queries 21.07 avg class size
c [sweep-12-2] 22241 decisions 837 SAT calls 63.92 avg env size
c [sweep-12-2] fully completed sweeping round
c [decomp-69] removed 2 variables
c [sweep-12-2] removed 2 vars (0 failed, 1 eqs, 0 impls)
c [sweep-12-3] 2882 pos 55.7% + 2296 neg 44.3% = 5178 sched 100.0% ret 0
c [sweep-12-3] 21750546 steps 853 queries 27.88 avg class size
c [sweep-12-3] 22155 decisions 855 SAT calls 62.96 avg env size
c [sweep-12-3] fully completed sweeping round
c [decomp-70] removed 1 variables
c [sweep-12-3] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-12] 3 < 1/1000 * 5180 = 5 considered unsuccessful
c [sweep-12] removed 3 vars in TOTAL (3 rounds, 2519 queries)
c [sort-queue-17] sorted 2346 enqueued variables after 4624685 conflicts
c [score-dist-17] active 2831 (55%), one 920 (18%), zero 1426 (28%)
c [score-dist-17] max exp 513, different 95 (18%)
c [score-dist-17] median active exp 504, avg 472.6
c [simplification-17] removed 86 variables 1.6% (5177 remain 55%)
c [simplification-17] removed 361 irredundant clauses 0.4% (93179 remain 62%)
c [simplification-17] maximum reduction of 2% = max (2%, 0%)
c [simplification-17] geometric conflict interval increment 333333 = 1000000 / 3
c [simplification-17] conflict interval soft limit 1000000 reached
c [simplification-17] new conflict interval 1000000
c [simplification-17] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-17] hard conflict limit 6124685 (soft 5624685 + delta 500000)
c [simplification-17] new conflict limit 5624685 (hard 6124685)
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 -  767.5    5177    93179   4678132  134757   7767  5648   24    35   37  68%   1024    3   22   21  107%
c -  786.8    5177    93179   4759344  137508   7807  5648   20    32   37  63%   1024   -0   24   21  116%
c -  809.3    5177    93179   4843444  139820   7822  5648   21    27   38  76%   1024   -2   20   21   97%
c -  831.0    5177    93179   4924005  139595   7844  5649   22    29   38  78%   1024   -0   22   22  100%
c -  855.1    5177    93179   5006501  142069   7853  5650   22    27   38  81%   1024    0   21   22   95%
c -  878.2    5177    93179   5087787  141938   7861  5650   22    25   38  87%   1024   -2   22   22  100%
c -  902.5    5177    93179   5175112  143531   7866  5650   22    26   38  85%   1024   -2   21   22   96%
c -  927.5    5177    93179   5260822  143331   7870  5650   19    25   38  77%   1024   -2   20   22   91%
c -  948.7    5177    93179   5344625  145078   7878  5650   20    27   38  72%   1024    0   20   20   98%
c -  971.9    5177    93179   5432040  146723   7881  5650   18    23   38  79%   1024   -2   18   20   94%
c -  993.9    5177    93179   5518114  148707   7887  5650   21    25   38  85%   1024   -1   21   21  100%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 436 basic ate = 29 trn 7% + 407 lrg 93% in 5 updates
c bcas: 8 count, 136 added (109 skipped), 590282 steps
c bkwd: tried 39161 clauses, 77559 lits, 1.98 lits/clause
c bkwd: checked 7343635 occs, 187.52 occs/clause, 94.68 occs/lit
c bkwd: subsumed 0 binary, 12 ternary, 279 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 796 large (0% self)
c blkd: 6 bces, 2223 removed, 3715182 resolutions, 11825454 steps
c blkd: 3494 blocking literals 18%, 27 pure
c bump: 5557806 bumped seen, 314011996 lits 56.5 on average
c card: 5 count, 0 units, 0 am1, 28113174 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 11112 subsumed
c card: 4620 at-most-one constraints found, average size 3.08
c card: 4620 at-most-one constraints used 100%, average size 3.08
c card: 150 at-most-two constraints found, average size 4.56
c card: 150 at-most-two constraints used 100%, average size 4.56
c cces: 8 cces, 40678 eliminated, 7940 ate 20%, 32738 abce 80%
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: 836456 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 89 gcs, 0 rescored clauses, 21620 rescored vars
c dcps: 70 decompositions, 1553 equivalent 16%
c deco: 20 decision-only clauses 0%, 44% reduction
c decs: 7528156 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 7 elims, 2449 eliminated 25%, 424 pure 17%
c elms: 10 rounds, 1.4 rounds/bve
c elms: 1543 small 63%, 455 large 19%
c elms: 3092 tried small, 1543 succeeded 50%, 1549 failed 50%
c elms: 2325 subsumed, 624 strengthened, 186 blocked
c elms: 1861964 copies, 2700636 resolutions, 109104 ipos
c elms: 4125184 subchks, 783510 strchks
c gaus: 5 extractions, 1862 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 21734068 steps, 10867034 extr 50%, 133997 elim 1%
c glue: 16.0 orig avg, 16.0 real avg, 3.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 24038 = 16168 simple 67% + 6540 trn 27% + 1330 lrg 6%, 457 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 5557805 clauses, 26.0 length
c lrnd: 144688564 lits = 202952243 orig - 58263679 removed 29%
c lrnd: 1642143 uips 30%, 3552091 flips 64%
c mins: 5534400 mins 100%, 170 bin 0%, 23215 size 0%
c mins: 101155794 poisoned searches, 13217399 hits, 13% hit rate
c mins: 285167821 used twice searches, 54832590 hits, 19% hit rate
c move: moved 8852, 1598 bin 18%, 7254 trn 82%
c otfs: 8179 driving 30%, 18866 restarting 70%
c otfs: str 27045, 26647 red 99%, 398 irr 1%
c otfs: str 27045, 0 bin 0%, 123 trn 0%, 26922 lrg 100%
c otfs: sub 294, 294 red 100%, 0 irr 0%
c otfs: sub 294, 0 bin 0%, 3 trn 1%, 291 lrg 99%
c phas: 14 computed, 6161 set, 3460 pos (56%), 2701 neg (44%)
c prbs: 6 basic, 44549 probed, 31 failed, 0 lifted
c prbs: 7 simple, 54319 probed, 19 failed, 367 eqs
c prbs: 6 treelook, 15127 probed, 1 failed, 0 lifted
c prom: 552474 locked 11% out of 4849793 tried
c prps: 1146454170 props, 151 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 15 count, 243 quat, 70 self1, 0 self2, 389 dup
c queu: 17 sorted, 7528156 next (763421 steps 0.10)
c queu: 352454859 enq (387880134 steps 1.10), 314011996 deq 89%
c redc: 12339 clauses 4%, 313587 tried 6%, 3 sat 0%
c redc: 14178 lits 0%, 3363671 tried 2%, 3 sat 0%
c redc: 323 times jump level reduced, 3.1 levels on average
c reds: 91 count, 60933.3 conflicts per reduce
c reds: 0 memlim 0%, 91 arith 100%
c reds: 4323295 collected 92%, 400437 retired 8%
c rmbd: 700 removed, 283 red 40%
c rsts: 21449 restarts 100%, 6 skipped 0%
c rsts: 6 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: 17 count, 17 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 5557805 count (2805229 tried 0.5), 614432 sub out of 5555303 (11.1%)
c swps: 12 count, 21 rounds, 10701 queries (509.6/round)
c swps: 10704 sat calls, 213 unsat (2.0% success rate)
c swps: 275688 decisions 25.8, 21057 conflicts 2.0
c swps; 53.1 avg class size, 62.3 avg environment size
c swps: 0 failed, 53 impls, 207 equivs
c swp0: 3562 type 0 queries, 1491 unsat (41.9%), 3521 sat (98.8%)
c swp1: 7139 type 1 queries, 3531 unsat (49.5%), 6973 sat (97.7%)
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: 26215557 calls to obtain time
c tops: 645 fixed 7%, 0 its, 0.00 confs/it
c trds: 15 transitive reductions, 11557 removed, 0 failed
c trds: 154034 nodes, 201819 edges, 6134972 steps
c trim: 2619001 words, 10.0 MB
c trnr: 12 count, 1 bin, 145 trn, 74353173 steps
c unhd: 6 count, 7 rounds, 12229455 steps
c unhd: 440 non-trivial sccs of average size 2.0
c unhd: 1 units, 1 bin, 0 trn, 0 lrg
c unhd: 3 failed, 3 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 7235 tauts, 1071 bin 15%, 416 trn 6%, 771 lrg 11%
c unhd: 7235 tauts, 4977 stamp 69%, 6060 red 84%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 44637 str, 1 bin 0%, 173 trn 0%, 44463 lrg 100%, 44419 red 100%
c vars: 5177 remaining 53% and 4647 removed 47% out of 9824
c vars: 645 fixed 7%, 2449 eliminated 25%, 1553 equivalent 16%
c vsts: 64224806485 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 56.1 search visits per propagation, 11530.1 per conflict
c wchs: 9793115022 pushed, 9118123 enlarged, 176 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        5555546       4323295        400437     133206586      45254357       2623631
c 
c  0 0         96425   2      4371   0         0   0  65883471  49  17494519  39    959202  37     3.1
c  1 5         93070   2     31533   1     53943  13  13394310  10<  4417419  10    267402  10     0.5
c  2 6        556119  10    357366   8    161596  40  26507491  20   8996808  20<   566095  22<    2.0
c  3 9       1800703  32   1496546  35     89557  22< 16585621  12   7496753  17    430012  16     4.0
c  4 14      1608210  29<  1315431  30<    42797  11   7710498   6   4558170  10    270189  10     5.7
c  5 21      1104358  20    878155  20     37645   9   2584883   2   1899610   4    108227   4     9.9
c  6 30       249981   4    201915   5     11457   3    456169   0    333351   1     18890   1     2.6
c  7 41        36721   1     29955   1      2528   1     66978   0     46145   0      2929   0     1.3
c  8 54         7747   0      6269   0       708   0     13476   0      9073   0       544   0     0.6
c  9 69         2053   0      1645   0       175   0      3426   0      2353   0       138   0     0.3
c 10 86          158   0       109   0        30   0       262   0       156   0         3   0     0.0
c 11 126           1   0         0   0         1   0         1   0         0   0         0   0     0.0
c 
c avg                  3.7           3.8           2.7           1.2           1.7           1.7
c std                  1.2           1.1           1.3           1.4           1.6           1.6
c 
c   32.473   3% cce
c   23.991   2% bump
c   11.138   1% sweep
c    7.711   1% probe
c    6.575   1% rescore
c    5.175   1% elim
c 
c   11.144 < 1% rest (below)
c 
c    4.597   0% decide
c    2.187   0% quatres
c    1.262   0% unhide
c    0.856   0% block
c    0.594   0% transred
c    0.486   0% bca
c    0.445   0% gauss
c    0.412   0% ternres
c    0.305   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.881   0% preprocessing     1%
c   64.692   6% inprocessing     99%
c ==================================
c   65.573   7% simplifying
c  934.386  93% search
c ==================================
c  999.960 100% all
c 
c       5544928 conflicts,        5545.2 confs/sec
c          1490 ternaries,        3721.4 confs/ternary
c            70 binaries,        79213.3 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            91 reductions,          0.1 redus/sec,  60933.3 confs/reduction
c         21449 restarts,           21.4 rests/sec,    258.5 confs/restart
c       7528156 decisions,        7528.5 decis/sec,      1.4 decis/conflict
c    1146454170 propagations,  1146500.5 props/sec,    152.3 props/decision
c 
c 1000.0 seconds, 64.1 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
