c launch: /data/cnf/sc2014/app/hwmcc10-timeframe-expansion-k50-pdtpmsns2-tseitin.cnf.bz2
c host: atom31
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/hwmcc10-timeframe-expansion-k50-pdtpmsns2-tseitin.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/hwmcc10-timeframe-expansion-k50-pdtpmsns2-tseitin.cnf.bz2
c no embedded options
c found 'p cnf 88352 262658' header
c read 88352 variables, 262658 clauses, 612866 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=2
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 88350 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] VMTF (--score=2)
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   88350   262656         0       0      0     0    0     0   17   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 215 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 215 out of 215 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 117 at-most-one constraints, 117 used 100%
c [card-1] exported 117 binary clauses, 1.0 per/constraint
c [decomp-1] removed 2 variables
c [simpleprobe-1] all 88350 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 1733 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 1733 variables, found 1908 hbrs, 209 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 1 units, 39 failed, 127 tauts, 0 hbrs, 121 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 86592 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 68439 variables 79% in round 1 in 16274126 steps
c [elim-1-1] backward subsumption/strengthening limit 3725874
c [elim-1-1-1] backward checking 62330 touched variables 72%
c [elim-1-1-1] incomplete backward checking 61242 remain 98%
c [elim-1-1] subsumed 19 and strengthened 1869 clauses in 3725881 steps
c [elim-1] incomplete 2110 not tried 2% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 68439 = 79% variables out of 86592 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 106091 negative 95.5% of 111071 except 4980 4.5%
c [phase-count-1] 98172 positive 88.4% of 111071 except 12899 11.6%
c [phase-count-1] less non-negative clauses 4980 than limit 11100 (10.0%)
c [phase-count-1] non-pos/non-neg = 12899/4980 = 2.59 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 18153 negative 100%
c [sort-queue-1] sorted 18153 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 18153 (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 70197 variables 79.5% (18153 remain 21%)
c [simplification-1] removed 151585 irredundant clauses 57.7% (111071 remain 42%)
c [simplification-1] maximum reduction of 79% = max (79%, 58%)
c [simplification-1] large reduction 79% >= 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  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    2.3   18152   111071       106      53     43   265    0     3   13   2%      0    3    1    0 20395%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 14 variables
c [simpleprobe-2] all 18139 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 12 variables
c [simpleprobe-2] 10405 variables remain 57% (7722 retained 43%)
c [simpleprobe-2] removed 12 variables, found 454 hbrs, 5 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 28295 literals 78%
c [treelook-1] scheduling used 300005 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300950 steps
c [treelook-1] 28017 literals remain 77%
c [treelook-1] 17134 variables remain to probed next time 95%
c [treelook-1] removed 0 variables, found 1192 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 6756 probes remain 37% after last round
c [basicprobe-1-0] 25 units = 25 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 54 variables, found 3509 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 13 units, 11 failed, 253 tauts, 0 hbrs, 11557 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 18054 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 79 not tried 0% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 707 = 4% variables out of 18054 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 103851 negative 95.6% of 108678 except 4827 4.4%
c [phase-count-2] 95771 positive 88.1% of 108678 except 12907 11.9%
c [phase-count-2] less non-negative clauses 4827 than limit 10800 (10.0%)
c [phase-count-2] non-pos/non-neg = 12907/4827 = 2.67 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 515 negative 100%
c [sort-queue-2] sorted 17347 enqueued variables after 1000 conflicts
c [score-dist-2] active 0 (0%), one 3419 (20%), zero 13928 (80%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 803 variables 4.4% (17347 remain 20%)
c [simplification-2] removed 2393 irredundant clauses 2.2% (108678 remain 41%)
c [simplification-2] maximum reduction of 4% = max (4%, 2%)
c [simplification-2] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-2] new conflict interval 4000
c [simplification-2] penalized conflict interval 4000 = 1 * 4000
c [simplification-2] hard conflict limit 15000 (soft 5000 + delta 10000)
c [simplification-2] new conflict limit 5000 (hard 15000)
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    3.5   17346   108677      1528     967    307  3787    1    20   13   5%     10   20    3    0 4499%
c i    3.5   17342   108677      1927    1264    371  3797    1    23   13   5%      8   22    3    0 3692%
c 
c [simplification-3] limit of 171 binary hit after 171 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 162 at-most-one constraints of average size 3.0
c [card-2] found 16 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 178 out of 178 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 51 variables
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 4 units, 25 failed, 892 tauts, 0 hbrs, 3911 literals
c [elim-3] 79 variables 0% will be scheduled this time
c [elim-3] scheduled 79 variables 0%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] no variable eliminated in round 1 in 4190577 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 0 = 0% variables out of 79 scheduled
c [phase-count-3] 102947 negative 95.6% of 107702 except 4755 4.4%
c [phase-count-3] 94714 positive 87.9% of 107702 except 12988 12.1%
c [phase-count-3] less non-negative clauses 4755 than limit 10700 (10.0%)
c [phase-count-3] non-pos/non-neg = 12988/4755 = 2.73 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 358 negative 100%
c [sort-queue-3] sorted 17284 enqueued variables after 3696 conflicts
c [score-dist-3] active 0 (0%), one 7508 (43%), zero 9776 (57%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 58 variables 0.3% (17284 remain 20%)
c [simplification-3] removed 975 irredundant clauses 0.9% (107702 remain 41%)
c [simplification-3] maximum reduction of 1% = max (0%, 1%)
c [simplification-3] forced so keeping old conflict interval 4000
c [simplification-3] conflict limit remains at 5000 (hard 15000)
c [simplification-3] new binary interval 1000
c 
c [simplification-4] limit 5000 conflicts (hard 15000) hit after 5001 conflicts
c [decomp-7] removed 21 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 15552 literals 45%
c [treelook-2] scheduling used 150048 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 179773 steps
c [treelook-2] 15427 literals remain 45%
c [treelook-2] 12102 variables remain to probed next time 70%
c [decomp-8] removed 1 variables
c [treelook-2] removed 4 variables, found 963 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 6 units, 9 failed, 222 tauts, 0 hbrs, 2845 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 17248 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 1021 blocked clauses
c [block-1] 1021 < 1/100 * 107603 = 1076 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 6 (33%) of length 11
c [cce-1-1] eliminated 3 clauses out of 32 (9%) of length 10
c [cce-1-1] eliminated 15 clauses out of 140 (11%) of length 9
c [cce-1-1] eliminated 87 clauses out of 885 (10%) of length 8
c [cce-1-1] eliminated 176 clauses out of 1638 (11%) of length 7
c [cce-1-1] eliminated 830 clauses out of 4917 (17%) of length 6
c [cce-1-1] eliminated 3297 clauses out of 12248 (27%) of length 5
c [cce-1-1] eliminated 98 clauses out of 25745 (0%) of length 4
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 4508 large clauses in 30000090 steps
c [cce-1-1] allowing another 15000045 steps for small clauses
c [cce-1-1] scheduling 44772 clauses = 19219 binary + 25553 ternary
c [cce-1-1] tried to eliminate 17667 small clauses 39%
c [cce-1-1] eliminated 428 binary clauses 2%
c [cce-1-1] eliminated 951 ternary clauses 4%
c [cce-1-1] eliminated 1379 small clauses 3%
c [cce-1-1] eliminated 1379 small clauses in 30000002 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 5887 covered clauses in round 1
c [cce-1] eliminated 5887 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 201786 added (scaled 2)
c [bca-1] 28202 out of 34498 literals actually usable 82%
c [bca-1] added 8 blocked clauses in 76286 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 4008 pos 23.2% + 13240 neg 76.8% = 17248 sched 100.0% ret 0
c [sweep-1-1] 1000971 steps 182 queries 1867.77 avg class size
c [sweep-1-1] 2372 decisions 180 SAT calls 30.62 avg env size
c [sweep-1-1] 14977 variables remain 87% (2269 retained 13%)
c [decomp-9] removed 16 variables
c [sweep-1-1] removed 16 vars (0 failed, 3 eqs, 8 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 16 vars in TOTAL (1 rounds, 181 queries)
c [phase-count-4] 96052 negative 95.5% of 100581 except 4529 4.5%
c [phase-count-4] 88007 positive 87.5% of 100581 except 12574 12.5%
c [phase-count-4] less non-negative clauses 4529 than limit 10000 (10.0%)
c [phase-count-4] non-pos/non-neg = 12574/4529 = 2.78 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 288 negative 100%
c [sort-queue-4] sorted 17232 enqueued variables after 5001 conflicts
c [score-dist-4] active 0 (0%), one 8132 (47%), zero 9100 (53%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 52 variables 0.3% (17232 remain 20%)
c [simplification-4] removed 7121 irredundant clauses 6.6% (100581 remain 38%)
c [simplification-4] maximum reduction of 7% = max (0%, 7%)
c [simplification-4] large reduction 7% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 17001 (soft 7001 + delta 10000)
c [simplification-4] new conflict limit 7001 (hard 17001)
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    5.6   17231   100581      5082    3523   2413  5848    2    41   13   6%     34   39    4    0 1419%
c 
c [simplification-5] limit 7001 conflicts (hard 17001) hit after 7001 conflicts
c [quatres-1] found 27012 quaternary clauses 60% in total
c [quatres-1-2] added 201 single-self-subsuming ternary resolvents
c [quatres-1-2] added 3044 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 17231 free variables schedulable
c [ternres-1] 8259 ternary resolvents (26 bin, 8233 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 742 xors of average arity 3.0
c [gauss-1] connected 2203 occurrences of 174 variables (average 12.7)
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-10] removed 5 variables
c [basicprobe-2] limit 1591975 penalty 0 = 0 + 0
c [basicprobe-2-0] 3591 probes remain 21% after last round
c [basicprobe-2-0] 37 units = 37 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 42 variables, found 4651 hbrs
c [bate-1] eliminated 81 asymmetric tautologies during probing
c [unhide-5] limit 100000 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 3 failed, 661 tauts, 0 hbrs, 2207 literals
c [transred-1] limit 318395 with penalty 0 = 0 + 0
c [transred-1] removed 294 transitive binary clauses
c [transred-1] found 3 units
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 740 (0%) of length 8
c [cce-2-1] eliminated 5 clauses out of 1380 (0%) of length 7
c [cce-2-1] eliminated 17 clauses out of 4075 (0%) of length 6
c [cce-2-1] eliminated 44 clauses out of 8661 (1%) of length 5
c [cce-2-1] eliminated 250 clauses out of 25389 (1%) of length 4
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 317 large clauses in 30000036 steps
c [cce-2-1] allowing another 15000018 steps for small clauses
c [cce-2-1] scheduling 43528 clauses = 18957 binary + 24571 ternary
c [cce-2-1] tried to eliminate 17693 small clauses 41%
c [cce-2-1] eliminated 232 binary clauses 1%
c [cce-2-1] eliminated 608 ternary clauses 2%
c [cce-2-1] eliminated 840 small clauses 2%
c [cce-2-1] eliminated 865 small clauses in 30000026 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1182 covered clauses in round 1
c [cce-2] eliminated 1182 covered clauses in TOTAL during 1 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 17178 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 200000000 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 1099 variables 6% in round 1 in 18698327 steps
c [elim-4-1] backward subsumption/strengthening limit 18698300
c [elim-4-1-1] backward checking 6189 touched variables 36%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 1 and strengthened 23 clauses in 1557121 steps
c [elim-4-1] rescheduled 86 variables 1% by backward subsumption
c [elim-4-2] eliminated 4 variables 0% in round 2 in 234385 steps
c [elim-4-2] backward subsumption/strengthening limit 234300
c [elim-4-2-1] backward checking 39 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 1 and strengthened 8 clauses in 118901 steps
c [elim-4-2] rescheduled 27 variables 0% by backward subsumption
c [elim-4-3] no variable eliminated in round 3 in 116097 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 1103 = 6% variables out of 17178 scheduled
c [bca-2] limit of 10000000 steps and 194706 added (scaled 2)
c [bca-2] 20349 out of 32152 literals actually usable 63%
c [bca-2] added 168 blocked clauses in 59792 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2661 pos 19.0% + 11309 neg 81.0% = 13970 sched 86.9% ret 2105
c [sweep-2-1] 1001289 steps 185 queries 1705.47 avg class size
c [sweep-2-1] 2837 decisions 178 SAT calls 33.28 avg env size
c [sweep-2-1] 11959 variables remain 74% (4116 retained 26%)
c [decomp-11] removed 30 variables
c [sweep-2-1] removed 30 vars (0 failed, 8 eqs, 11 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 30 vars in TOTAL (1 rounds, 184 queries)
c [phase-count-5] 93107 negative 95.9% of 97043 except 3936 4.1%
c [phase-count-5] 85408 positive 88.0% of 97043 except 11635 12.0%
c [phase-count-5] less non-negative clauses 3936 than limit 9700 (10.0%)
c [phase-count-5] non-pos/non-neg = 11635/3936 = 2.96 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 209 negative 100%
c [sort-queue-5] sorted 16045 enqueued variables after 7001 conflicts
c [score-dist-5] active 0 (0%), one 8227 (51%), zero 7818 (49%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 1186 variables 6.9% (16045 remain 18%)
c [simplification-5] removed 3538 irredundant clauses 3.5% (97043 remain 37%)
c [simplification-5] maximum reduction of 7% = max (7%, 4%)
c [simplification-5] large reduction 7% >= 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 19001 (soft 9001 + delta 10000)
c [simplification-5] new conflict limit 9001 (hard 19001)
c 
c [simplification-6] limit 9001 conflicts (hard 19001) hit after 9001 conflicts
c [quatres-2] found 28754 quaternary clauses 59% in total
c [quatres-2-1] removed 3 duplicate quaternary clauses
c [quatres-2-2] added 115 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1326 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 16045 free variables schedulable
c [ternres-2] 1489 ternary resolvents (12 bin, 1477 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 273 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 273 out of 273 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 6 variables
c [simpleprobe-3] 9163 schedulable variables 57%
c [simpleprobe-3] limit 2000000 penalty 0 = 0 + 0
c [decomp-13] removed 6 variables
c [simpleprobe-3] 6045 variables remain 38% (9988 retained 62%)
c [simpleprobe-3] removed 6 variables, found 624 hbrs, 1 units
c [unhide-6] limit 100000 with penalty 0 = 0 + 0
c [unhide-6-6] 3 units, 6 failed, 1201 tauts, 0 hbrs, 3121 literals
c [transred-2] limit 430616 with penalty 0 = 0 + 0
c [transred-2] removed 285 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 16028 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 16 blocked clauses
c [block-2] 16 < 1/100 * 96946 = 969 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 2 clauses out of 18 (11%) of length 11
c [cce-3-1] eliminated 3 clauses out of 51 (6%) of length 10
c [cce-3-1] eliminated 8 clauses out of 168 (5%) of length 9
c [cce-3-1] eliminated 41 clauses out of 993 (4%) of length 8
c [cce-3-1] eliminated 109 clauses out of 1605 (7%) of length 7
c [cce-3-1] eliminated 66 clauses out of 4931 (1%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 229 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3-1] scheduling 32491 clauses = 17090 binary + 15401 ternary
c [cce-3-1] tried to eliminate 6367 small clauses 20%
c [cce-3-1] eliminated 225 binary clauses 1%
c [cce-3-1] eliminated 496 ternary clauses 3%
c [cce-3-1] eliminated 721 small clauses 2%
c [cce-3-1] eliminated 721 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 950 covered clauses in round 1
c [cce-3] eliminated 950 covered clauses in TOTAL during 1 rounds
c [cce-3] 950 < 1/100 * 96917 = 969 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 16028 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 146 variables 1% in round 1 in 17642475 steps
c [elim-5-1] backward subsumption/strengthening limit 2357525
c [elim-5-1-1] backward checking 1389 touched variables 9%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 3 and strengthened 4 clauses in 625300 steps
c [elim-5-1] rescheduled 24 variables 0% by backward subsumption
c [elim-5-2] no variable eliminated in round 2 in 37543 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 146 = 1% variables out of 16028 scheduled
c [elim-5] 146 < 1/100 * 16028 = 160 considered unsuccessful
c [bca-3] limit of 10000000 steps and 191722 added (scaled 2)
c [bca-3] 18216 out of 31766 literals actually usable 57%
c [bca-3] added 27 blocked clauses in 56184 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2593 pos 21.9% + 9253 neg 78.1% = 11846 sched 74.6% ret 4036
c [sweep-3-1] 1002232 steps 175 queries 1442.33 avg class size
c [sweep-3-1] 2763 decisions 174 SAT calls 34.57 avg env size
c [sweep-3-1] 9909 variables remain 62% (5973 retained 38%)
c [decomp-14] removed 21 variables
c [sweep-3-1] removed 21 vars (0 failed, 2 eqs, 3 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 21 vars in TOTAL (1 rounds, 174 queries)
c [phase-count-6] 91735 negative 96.0% of 95518 except 3783 4.0%
c [phase-count-6] 84020 positive 88.0% of 95518 except 11498 12.0%
c [phase-count-6] less non-negative clauses 3783 than limit 9500 (10.0%)
c [phase-count-6] non-pos/non-neg = 11498/3783 = 3.04 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 152 negative 100%
c [sort-queue-6] sorted 15861 enqueued variables after 9001 conflicts
c [score-dist-6] active 0 (0%), one 9062 (57%), zero 6799 (43%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 184 variables 1.1% (15861 remain 18%)
c [simplification-6] removed 1525 irredundant clauses 1.6% (95518 remain 36%)
c [simplification-6] maximum reduction of 2% = max (1%, 2%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 10666
c [simplification-6] penalized conflict interval 10666 = 1 * 10666
c [simplification-6] hard conflict limit 29667 (soft 19667 + delta 10000)
c [simplification-6] new conflict limit 19667 (hard 29667)
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   11.9   15860    95518     11668   11868  10909  9179    4    51   14   7%     82   44    4    1  676%
c 
c [simplification-7] limit of 2435 ternary hit after 2435 ternaries
c [quatres-3] found 30861 quaternary clauses 58% in total
c [quatres-3-1] removed 2 duplicate quaternary clauses
c [quatres-3-2] added 113 single-self-subsuming ternary resolvents
c [quatres-3-2] added 565 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 15857 free variables schedulable
c [ternres-3] 2077 ternary resolvents (22 bin, 2055 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 294 xors of average arity 2.9
c [gauss-2] connected 858 occurrences of 129 variables (average 6.7)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 12 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 20207 literals 64%
c [treelook-3] scheduling used 300010 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 300247 steps
c [treelook-3] 20123 literals remain 63%
c [treelook-3] 10402 variables remain to probed next time 66%
c [treelook-3] removed 0 variables, found 1501 hbrs
c [unhide-7] limit 189855 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 2 failed, 594 tauts, 0 hbrs, 4264 literals
c [transred-3] limit 949279 with penalty 0 = 0 + 0
c [transred-3] removed 530 transitive binary clauses
c [transred-3] found 1 units
c [bca-4] limit of 10000000 steps and 191041 added (scaled 2)
c [bca-4] 15148 out of 31688 literals actually usable 48%
c [bca-4] added 5 blocked clauses in 55529 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 2193 pos 22.2% + 7696 neg 77.8% = 9889 sched 62.4% ret 5954
c [sweep-4-1] 1002071 steps 131 queries 1412.34 avg class size
c [sweep-4-1] 2410 decisions 127 SAT calls 37.17 avg env size
c [sweep-4-1] 8619 variables remain 54% (7224 retained 46%)
c [decomp-17] removed 12 variables
c [sweep-4-1] removed 12 vars (0 failed, 4 eqs, 8 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 12 vars in TOTAL (1 rounds, 130 queries)
c [phase-count-7] 91428 negative 96.0% of 95189 except 3761 4.0%
c [phase-count-7] 83703 positive 87.9% of 95189 except 11486 12.1%
c [phase-count-7] less non-negative clauses 3761 than limit 9500 (10.0%)
c [phase-count-7] non-pos/non-neg = 11486/3761 = 3.05 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 60 negative 100%
c [sort-queue-7] sorted 15831 enqueued variables after 17543 conflicts
c [score-dist-7] active 0 (0%), one 11564 (73%), zero 4267 (27%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 26 variables 0.2% (15831 remain 18%)
c [simplification-7] removed 329 irredundant clauses 0.3% (95189 remain 36%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] forced so keeping old conflict interval 10666
c [simplification-7] conflict limit remains at 19667 (hard 29667)
c [simplification-7] new ternary interval 10000
c 
c [simplification-8] limit 19667 conflicts (hard 29667) hit after 19667 conflicts
c [quatres-4] found 31487 quaternary clauses 58% in total
c [quatres-4-1] removed 3 duplicate quaternary clauses
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 108 single-self-subsuming ternary resolvents
c [quatres-4-2] added 182 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 15831 free variables schedulable
c [ternres-4] 808 ternary resolvents (11 bin, 797 trn)
c [ternres-4] fully completed ternary resolution
c [basicprobe-3] limit 5532372 penalty 0 = 0 + 0
c [basicprobe-3-0] 3166 sched 20%, 39 failed, 1 lifted, 12838 hbrs
c [decomp-19] removed 53 variables
c [basicprobe-3-1] 4627 probes remain 29% after last round
c [basicprobe-3-1] 45 units = 44 failed (98%) + 1 lifted (2%)
c [basicprobe-3-1] removed 58 variables, found 15765 hbrs
c [bate-2] eliminated 97 asymmetric tautologies during probing
c [unhide-8] limit 221294 with penalty 0 = 0 + 0
c [unhide-8-8] 0 units, 4 failed, 2268 tauts, 0 hbrs, 5411 literals
c [transred-4] limit 1106474 with penalty 0 = 0 + 0
c [transred-4] removed 291 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 150000000 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 2 clauses out of 842 (0%) of length 8
c [cce-4-1] eliminated 16 clauses out of 1393 (1%) of length 7
c [cce-4-1] eliminated 239 clauses out of 4840 (5%) of length 6
c [cce-4-1] eliminated 428 clauses out of 8752 (5%) of length 5
c [cce-4-1] eliminated 3833 clauses out of 23656 (16%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 4518 large clauses in 51916213 steps
c [cce-4-1] allowing another 25958106 steps for small clauses
c [cce-4-1] scheduling 31751 clauses = 16903 binary + 14848 ternary
c [cce-4-1] tried to eliminate 31751 small clauses 100%
c [cce-4-1] eliminated 331 binary clauses 2%
c [cce-4-1] eliminated 1400 ternary clauses 9%
c [cce-4-1] eliminated 1731 small clauses 5%
c [cce-4-1] eliminated 1746 small clauses in 51604878 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 6264 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 22561948 steps for small clauses
c [cce-4-2] scheduling 30020 clauses = 16572 binary + 13448 ternary
c [cce-4-2] tried to eliminate 30020 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 6264 covered clauses in TOTAL during 2 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 15770 variables 100%
c [elim-6] limit of 11064744 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 152 not tried 1% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 609 = 4% variables out of 15770 scheduled
c [bca-5] limit of 10000000 steps and 175582 added (scaled 2)
c [bca-5] 14711 out of 30324 literals actually usable 49%
c [bca-5] added 38 blocked clauses in 54033 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 1582 pos 19.0% + 6739 neg 81.0% = 8321 sched 54.9% ret 6840
c [sweep-5-1] 7949076 steps 1643 queries 174.07 avg class size
c [sweep-5-1] 22710 decisions 1614 SAT calls 26.42 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-20] removed 42 variables
c [sweep-5-1] removed 42 vars (0 failed, 37 eqs, 46 impls)
c [sweep-5-2] 3382 pos 22.4% + 11737 neg 77.6% = 15119 sched 100.0% ret 0
c [sweep-5-2] 2092729 steps 156 queries 1125.58 avg class size
c [sweep-5-2] 3489 decisions 155 SAT calls 47.77 avg env size
c [sweep-5-2] 11643 variables remain 77% (3476 retained 23%)
c [decomp-21] removed 7 variables
c [sweep-5-2] removed 7 vars (0 failed, 1 eqs, 1 impls)
c [sweep-5] removed 49 vars in TOTAL (2 rounds, 1797 queries)
c [phase-count-8] 84092 negative 96.2% of 87396 except 3304 3.8%
c [phase-count-8] 76524 positive 87.6% of 87396 except 10872 12.4%
c [phase-count-8] less non-negative clauses 3304 than limit 8700 (10.0%)
c [phase-count-8] non-pos/non-neg = 10872/3304 = 3.29 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 2 negative 100%
c [sort-queue-8] sorted 15112 enqueued variables after 19667 conflicts
c [score-dist-8] active 0 (0%), one 11450 (76%), zero 3662 (24%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 719 variables 4.5% (15112 remain 17%)
c [simplification-8] removed 7793 irredundant clauses 8.2% (87396 remain 33%)
c [simplification-8] maximum reduction of 8% = max (5%, 8%)
c [simplification-8] large reduction 8% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 31667 (soft 21667 + delta 10000)
c [simplification-8] new conflict limit 21667 (hard 31667)
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   18.6   15111    87396     21487   18618  13591 22881    5    53   15   9%    123   40    5    1  469%
c 
c [simplification-9] limit 21667 conflicts (hard 31667) hit after 21667 conflicts
c [quatres-5] found 26894 quaternary clauses 54% in total
c [quatres-5-1] removed 6 duplicate quaternary clauses
c [quatres-5-1] added 1 double-self-subsuming ternary resolvents
c [quatres-5-2] added 84 single-self-subsuming ternary resolvents
c [quatres-5-2] added 315 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 15111 free variables schedulable
c [ternres-5] 1212 ternary resolvents (13 bin, 1199 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-22] removed 3 variables
c [simpleprobe-4] 5687 schedulable variables 38%
c [simpleprobe-4] limit 4950585 penalty 0 = 0 + 0
c [decomp-23] removed 7 variables
c [simpleprobe-4] 2185 variables remain 14% (12917 retained 86%)
c [simpleprobe-4] removed 7 variables, found 1711 hbrs, 1 units
c [unhide-9] limit 247529 with penalty 0 = 0 + 0
c [unhide-9-9] 0 units, 0 failed, 576 tauts, 0 hbrs, 2824 literals
c [transred-5] limit 1237646 with penalty 0 = 0 + 0
c [transred-5] removed 715 transitive binary clauses
c [transred-5] found 1 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 15101 variables 100%
c [block-3] limit of 12500000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 6 blocked clauses
c [block-3] 6 < 1/100 * 87248 = 872 considered unsuccessful
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 7 clauses out of 235 (3%) of length 9
c [cce-5-1] eliminated 28 clauses out of 940 (3%) of length 8
c [cce-5-1] eliminated 46 clauses out of 1413 (3%) of length 7
c [cce-5-1] eliminated 144 clauses out of 4849 (3%) of length 6
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 225 large clauses in 30000003 steps
c [cce-5-1] allowing another 15000001 steps for small clauses
c [cce-5-1] scheduling 28562 clauses = 15607 binary + 12955 ternary
c [cce-5-1] tried to eliminate 7401 small clauses 26%
c [cce-5-1] eliminated 171 binary clauses 1%
c [cce-5-1] eliminated 173 ternary clauses 1%
c [cce-5-1] eliminated 344 small clauses 1%
c [cce-5-1] eliminated 344 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 569 covered clauses in round 1
c [cce-5] eliminated 569 covered clauses in TOTAL during 1 rounds
c [cce-5] 569 < 1/100 * 87239 = 872 considered unsuccessful
c [elim-7] 152 variables 1% will be scheduled this time
c [elim-7] scheduled 152 variables 1%
c [elim-7] limit of 24752929 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] no variable eliminated in round 1 in 4332505 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 0 = 0% variables out of 152 scheduled
c [bca-6] limit of 10000000 steps and 173959 added (scaled 2)
c [bca-6] 13908 out of 30202 literals actually usable 46%
c [bca-6] added 6 blocked clauses in 53948 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 3306 pos 28.4% + 8321 neg 71.6% = 11627 sched 77.0% ret 3473
c [sweep-6-1] 1000622 steps 73 queries 1854.75 avg class size
c [sweep-6-1] 1428 decisions 72 SAT calls 43.44 avg env size
c [sweep-6-1] 10940 variables remain 72% (4160 retained 28%)
c [decomp-24] removed 1 variables
c [sweep-6-1] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-6] 1 < 1/1000 * 15100 = 15 considered unsuccessful
c [sweep-6] removed 1 vars in TOTAL (1 rounds, 72 queries)
c [phase-count-9] 83402 negative 96.2% of 86666 except 3264 3.8%
c [phase-count-9] 75853 positive 87.5% of 86666 except 10813 12.5%
c [phase-count-9] less non-negative clauses 3264 than limit 8600 (10.0%)
c [phase-count-9] non-pos/non-neg = 10813/3264 = 3.31 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-9] sorted 15099 enqueued variables after 21667 conflicts
c [score-dist-9] active 0 (0%), one 11566 (77%), zero 3533 (23%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 12 variables 0.1% (15099 remain 17%)
c [simplification-9] removed 730 irredundant clauses 0.8% (86666 remain 33%)
c [simplification-9] maximum reduction of 1% = max (0%, 1%)
c [simplification-9] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-9] new conflict interval 20666
c [simplification-9] penalized conflict interval 20666 = 1 * 20666
c [simplification-9] hard conflict limit 52666 (soft 42333 + delta 10333)
c [simplification-9] new conflict limit 42333 (hard 52666)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   22.1   15098    86666     23681   20744  14958 23997    4    51   15   9%     20   37    5    1  385%
c i   22.4   15097    86666     25082   21954  15089 24019    5    52   15   9%      3   37    5    1  404%
c i   25.4   15096    86666     36111   31707  15973 24168    6    53   16  11%    131   32    7    2  368%
c i   26.0   15095    86666     38307   33641  16138 24200    6    54   16  11%     12   32    5    2  251%
c 
c [simplification-10] limit 42333 conflicts (hard 52666) hit after 42333 conflicts
c [quatres-6] found 29220 quaternary clauses 49% in total
c [quatres-6-1] added 3 double-self-subsuming ternary resolvents
c [quatres-6-2] added 138 single-self-subsuming ternary resolvents
c [quatres-6-2] added 182 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 15095 free variables schedulable
c [ternres-6] 1189 ternary resolvents (8 bin, 1181 trn)
c [ternres-6] 80 variables remain 1% (15015 retained 99%)
c [card-4] limit 250000 penalty 3 = 3 + 0
c [card-4] found 87 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 250000 for elimination
c [card-4] 87 out of 87 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 92 xors of average arity 2.9
c [gauss-3] connected 271 occurrences of 85 variables (average 3.2)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-25] removed 9 variables
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 863 transitive binary clauses
c [transred-6] found 4 units
c [bca-7] limit of 10000000 steps and 173810 added (scaled 2)
c [bca-7] 10373 out of 30166 literals actually usable 34%
c [bca-7] added 6 blocked clauses in 63389 steps
c [phase-count-10] 83331 negative 96.2% of 86592 except 3261 3.8%
c [phase-count-10] 75798 positive 87.5% of 86592 except 10794 12.5%
c [phase-count-10] less non-negative clauses 3261 than limit 8600 (10.0%)
c [phase-count-10] non-pos/non-neg = 10794/3261 = 3.31 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-10] sorted 15082 enqueued variables after 42333 conflicts
c [score-dist-10] active 0 (0%), one 12974 (86%), zero 2108 (14%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 13 variables 0.1% (15082 remain 17%)
c [simplification-10] removed 74 irredundant clauses 0.1% (86592 remain 33%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 20666
c [simplification-10] new conflict interval 41332
c [simplification-10] penalized conflict interval 41332 = 1 * 41332
c [simplification-10] hard conflict limit 104331 (soft 83665 + delta 20666)
c [simplification-10] new conflict limit 83665 (hard 104331)
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   27.9   15081    86592     42512   37451  17644 23320    6    56   19  11%     23   32    7    2  282%
c i   28.5   15080    86592     44430   39159  17787 23338    7    58   19  11%     -3   33    8    3  325%
c i   28.5   15079    86592     44431   39159  17787 23338    7    58   19  11%     -3   33    8    3  323%
c i   32.0   15076    86592     55019   48654  18476 23474    7    57   19  12%    115   27    7    3  222%
c i   32.2   15075    86592     55560   49133  18514 23481    7    56   19  12%     55   27    6    3  188%
c i   32.3   15074    86592     55801   49353  18526 23483    6    56   19  12%     37   26    6    3  190%
c i   33.7   15073    86592     59949   53128  18749 23541    7    55   20  13%     15   23    7    3  208%
c i   34.5   15072    86592     62305   55299  18854 23570    7    57   21  13%     -7   24    8    4  228%
c i   35.2   15070    86592     63979   56839  18938 23587    7    57   21  13%    -16   24    7    4  198%
c i   35.8   15068    86592     65499   58212  19016 23606    7    57   21  13%    -18   23    7    4  175%
c i   35.8   15067    86592     65693   58385  19026 23609    8    57   21  13%    -21   23    7    4  191%
c i   37.0   15066    86592     68706   61120  19190 23638    7    55   22  14%     -0   20    7    4  176%
c i   37.9   15065    86592     70958   63180  19313 23655    8    55   22  14%     -8   20    7    4  173%
c i   39.0   15064    86592     73547   65566  19425 23681    8    56   22  14%     -4   20    6    4  154%
c i   39.1   15063    86592     73860   65851  19445 23682    8    56   22  14%    -11   20    7    4  156%
c i   40.2   15062    86592     76586   68328  19586 23708    8    55   23  14%     -2   18    8    4  186%
c i   40.2   15061    86592     76587   68328  19586 23708    8    55   23  14%     -2   18    8    4  186%
c 
c [simplification-11] limit of 20 iterations hit after 27 iterations
c [quatres-7] found 31647 quaternary clauses 44% in total
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 96 single-self-subsuming ternary resolvents
c [quatres-7-2] added 248 quaternary resolvents
c [ternres-7] limit 7075815 with penalty 0 = 0 + 0
c [ternres-7] 79 schedulable variables 1%
c [ternres-7] 953 ternary resolvents (9 bin, 944 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-26] removed 38 variables
c [treelook-4] limit 353790 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 17284 literals 57%
c [treelook-4] scheduling used 353796 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 353790 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 394265 steps
c [treelook-4] 17158 literals remain 57%
c [treelook-4] 9300 variables remain to probed next time 62%
c [treelook-4] removed 0 variables, found 1287 hbrs
c [unhide-10] limit 707581 with penalty 1 = 1 + 0
c [unhide-10-10] 2 units, 12 failed, 2083 tauts, 0 hbrs, 88258 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 462 transitive binary clauses
c [transred-7] found 7 units
c [cce-6] limit of 17689539 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 1 clauses out of 5 (20%) of length 12
c [cce-6-1] eliminated 2 clauses out of 916 (0%) of length 8
c [cce-6-1] eliminated 8 clauses out of 1326 (1%) of length 7
c [cce-6-1] eliminated 101 clauses out of 4615 (2%) of length 6
c [cce-6-1] eliminated 93 clauses out of 8316 (1%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 205 large clauses in 17689596 steps
c [cce-6-1] allowing another 8844798 steps for small clauses
c [cce-6-1] scheduling 28319 clauses = 15500 binary + 12819 ternary
c [cce-6-1] tried to eliminate 11182 small clauses 39%
c [cce-6-1] eliminated 33 binary clauses 0%
c [cce-6-1] eliminated 58 ternary clauses 0%
c [cce-6-1] eliminated 91 small clauses 0%
c [cce-6-1] eliminated 144 small clauses in 17689541 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 349 covered clauses in round 1
c [cce-6] eliminated 349 covered clauses in TOTAL during 1 rounds
c [cce-6] 349 < 1/100 * 86404 = 864 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 15031 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1415163150 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 170 variables 1% in round 1 in 14695838 steps
c [elim-8-1] backward subsumption/strengthening limit 14695800
c [elim-8-1-1] backward checking 1504 touched variables 10%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 6 and strengthened 5 clauses in 529045 steps
c [elim-8-1] rescheduled 36 variables 0% by backward subsumption
c [elim-8-2] eliminated 1 variables 0% in round 2 in 99376 steps
c [elim-8-2] backward subsumption/strengthening limit 99300
c [elim-8-2-1] backward checking 17 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 3 clauses in 55889 steps
c [elim-8-2] rescheduled 6 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 45523 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 171 = 1% variables out of 15031 scheduled
c [bca-8] limit of 10000000 steps and 171957 added (scaled 2)
c [bca-8] 7882 out of 29722 literals actually usable 27%
c [bca-8] added 7 blocked clauses in 84505 steps
c [sweep-7] limit 1061372 penalty 1 = 1 + 0
c [sweep-7-1] 2436 pos 22.6% + 8366 neg 77.4% = 10802 sched 72.7% ret 4058
c [sweep-7-1] 1256057 steps 45 queries 865.84 avg class size
c [sweep-7-1] 1579 decisions 44 SAT calls 84.34 avg env size
c [sweep-7-1] 10085 variables remain 68% (4775 retained 32%)
c [decomp-28] removed 5 variables
c [sweep-7-1] removed 5 vars (0 failed, 1 eqs, 1 impls)
c [sweep-7] 5 < 1/1000 * 14860 = 14 considered unsuccessful
c [sweep-7] removed 5 vars in TOTAL (1 rounds, 44 queries)
c [sort-queue-11] sorted 14855 enqueued variables after 79419 conflicts
c [score-dist-11] active 0 (0%), one 13691 (92%), zero 1164 (8%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 206 variables 1.4% (14855 remain 17%)
c [simplification-11] removed 932 irredundant clauses 1.1% (85660 remain 33%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] forced so keeping old conflict interval 41332
c [simplification-11] conflict limit remains at 83685 (hard 104331)
c [simplification-11] new iteration interval 100
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   43.4   14854    85660     79516   64673  19843 22185    8    56   23  14%      1   18    8    4  175%
c i   44.9   14853    85660     83443   68285  20050 22219    8    58   23  14%     16   19    8    5  169%
c 
c [simplification-12] limit 83685 conflicts (hard 104331) hit after 83686 conflicts
c [quatres-8] found 31782 quaternary clauses 44% in total
c [quatres-8-1] removed 8 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 47 single-self-subsuming ternary resolvents
c [quatres-8-2] added 165 quaternary resolvents
c [ternres-8] limit 7576413 with penalty 0 = 0 + 0
c [ternres-8] all 14853 free variables schedulable
c [ternres-8] 1884 ternary resolvents (15 bin, 1869 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-29] removed 3 variables
c [basicprobe-4] limit 37882068 penalty 0 = 0 + 0
c [basicprobe-4-0] 4321 sched 29%, 38 failed, 1 lifted, 17873 hbrs
c [decomp-30] removed 51 variables
c [basicprobe-4-1] 5031 sched 34%, 23 failed, 0 lifted, 8619 hbrs
c [decomp-31] removed 30 variables
c [basicprobe-4-2] 4882 sched 33%, 11 failed, 1 lifted, 3672 hbrs
c [decomp-32] removed 14 variables
c [basicprobe-4-3] 4512 probes remain 31% after last round
c [basicprobe-4-3] 74 units = 72 failed (97%) + 2 lifted (3%)
c [basicprobe-4-3] removed 95 variables, found 30347 hbrs
c [bate-3] eliminated 88 asymmetric tautologies during probing
c [unhide-11] limit 1515282 with penalty 0 = 0 + 0
c [unhide-11-11] 0 units, 0 failed, 575 tauts, 0 hbrs, 18766 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 646 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 14757 variables 100%
c [elim-9] limit of 151528275 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 86 variables 1% in round 1 in 14414294 steps
c [elim-9-1] backward subsumption/strengthening limit 14414200
c [elim-9-1-1] backward checking 652 touched variables 4%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 3 and strengthened 2 clauses in 260496 steps
c [elim-9-1] rescheduled 12 variables 0% by backward subsumption
c [elim-9-2] eliminated 1 variables 0% in round 2 in 50105 steps
c [elim-9-2] backward subsumption/strengthening limit 50100
c [elim-9-2-1] backward checking 9 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 3 clauses in 48321 steps
c [elim-9-2] rescheduled 6 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 48001 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 87 = 1% variables out of 14757 scheduled
c [elim-9] 87 < 1/100 * 14757 = 147 considered unsuccessful
c [bca-9] limit of 10000000 steps and 170172 added (scaled 2)
c [bca-9] 7738 out of 29342 literals actually usable 26%
c [bca-9] added 0 blocked clauses in 83757 steps
c [sort-queue-12] sorted 14670 enqueued variables after 83686 conflicts
c [score-dist-12] active 0 (0%), one 13564 (92%), zero 1106 (8%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 183 variables 1.2% (14670 remain 17%)
c [simplification-12] removed 890 irredundant clauses 1.0% (84770 remain 32%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 20666 = 41332 / 2
c [simplification-12] new conflict interval 61998
c [simplification-12] penalized conflict interval 61998 = 1 * 61998
c [simplification-12] hard conflict limit 176683 (soft 145684 + delta 30999)
c [simplification-12] new conflict limit 145684 (hard 176683)
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   50.9   14669    84770     90922   70908  21285 45558    8    54   23  14%     68   14    6    5  126%
c i   58.5   14668    84770    107629   86473  21956 45650    9    54   25  16%    191   10    8    6  138%
c i   61.0   14667    84770    113199   91685  22124 45683    8    55   27  15%     16   10    7    6  113%
c -   64.5   14667    84770    120619   57523  22373 45715    8    53   20  16%     44    7    7    6  109%
c i   64.6   14666    84770    120779   57670  22376 45716    8    52   23  16%     47    5    6    6  101%
c i   66.3   14665    84770    124658   61332  22475 45750    9    53   23  16%     -8    7    7    6  106%
c i   66.5   14664    84770    125537   62163  22498 45755    8    52   23  16%    -30    5    7    6  109%
c i   70.0   14660    84770    135614   71643  22789 45800    8    52   24  15%     85    5    8    7  122%
c i   70.5   14659    84770    136969   72912  22824 45805    8    50   24  17%    -10    3   10    7  141%
c i   70.6   14658    84770    136975   72915  22826 45805    8    50   24  17%    -11    3    9    7  138%
c i   70.6   14657    84770    136978   72917  22826 45805    8    50   24  17%    -11    3    9    7  137%
c i   71.4   14655    84770    138687   74524  22888 45808    9    53   25  17%    -34    5    9    7  138%
c 
c [simplification-13] limit 145688 conflicts (hard 176683) hit after 145689 conflicts
c [quatres-9] found 34436 quaternary clauses 39% in total
c [quatres-9-1] removed 5 duplicate quaternary clauses
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 128 single-self-subsuming ternary resolvents
c [quatres-9-2] added 266 quaternary resolvents
c [ternres-9] limit 15319582 with penalty 0 = 0 + 0
c [ternres-9] all 14655 free variables schedulable
c [ternres-9] 1740 ternary resolvents (4 bin, 1736 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-33] removed 26 variables
c [simpleprobe-5] 2073 schedulable variables 14%
c [simpleprobe-5] limit 61278328 penalty 0 = 0 + 0
c [decomp-34] removed 27 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 27 variables, found 14648 hbrs, 6 units
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1469 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 14617 variables 100%
c [block-4] limit of 19149477 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 4 blocked clauses
c [block-4] 4 < 1/100 * 84440 = 844 considered unsuccessful
c [sort-queue-13] sorted 14617 enqueued variables after 145689 conflicts
c [score-dist-13] active 0 (0%), one 14185 (97%), zero 432 (3%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 38 variables 0.3% (14617 remain 17%)
c [simplification-13] removed 334 irredundant clauses 0.4% (84436 remain 32%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 61998
c [simplification-13] new conflict interval 123996
c [simplification-13] penalized conflict interval 123996 = 1 * 123996
c [simplification-13] hard conflict limit 331683 (soft 269685 + delta 61998)
c [simplification-13] new conflict limit 269685 (hard 331683)
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   75.8   14616    84435    146278   81634  24829 58673    9    52   28  17%     47    4   10    7  136%
c i   77.0   14615    84435    149023   84207  24911 58690   10    52   28  19%    -20    4    9    7  127%
c i   77.2   14614    84435    149680   84843  24923 58691    9    49   28  19%    -34    1   10    7  144%
c i   79.6   14613    84435    155558   90370  25080 58709    9    49   28  18%     22    1    7    7   90%
c i   80.0   14612    84435    156280   91043  25096 58716    9    50   28  19%    -13    2    9    7  125%
c i   80.5   14611    84435    157282   91978  25130 58724   10    51   28  19%    -32    2   11    7  152%
c i   83.0   14607    84435    162912   97263  25276 58748   10    53   29  18%     20    4    9    8  118%
c i   86.4   14606    84435    171715  105571  25503 58779    9    52   33  17%     68    3    8    8   98%
c i   86.4   14605    84435    171716  105571  25503 58779    9    52   33  17%     68    3    8    8   97%
c i   87.5   14601    84435    175016  108657  25609 58791    9    49   33  18%    -12   -0    8    8   99%
c i   88.3   14600    84435    176534  110092  25651 58799    9    52   33  18%    -32    3   10    8  125%
c i   89.8   14599    84435    180499  113827  25748 58809   10    48   35  20%     -4   -2   11    8  142%
c -   90.1   14599    84434    180989   76613  25783 58817   10    48   23  20%    -20   -2   10    8  130%
c i   90.6   14598    84434    182753   78271  25847 58826    9    48   26  20%    -24   -1   10    8  121%
c i   92.2   14596    84434    188260   83478  25980 58843    9    55   27  17%     21    6   10    8  118%
c i   92.6   14595    84434    189320   84480  26005 58845    9    57   27  16%    -18    7    9    8  113%
c i   93.9   14589    84434    194152   89086  26095 58861    9    45   27  20%     12   -5    9    8  105%
c i   93.9   14587    84434    194201   89133  26095 58861    9    45   28  21%     10   -5   10    8  126%
c i   94.6   14586    84434    196488   91256  26175 58880    9    41   29  22%    -19   -9    8    8  102%
c i   97.7   14585    84434    205262   99581  26376 58901    9    45   31  21%     73   -4    9    8  110%
c i   98.2   14584    84434    206729  100990  26401 58906   10    51   31  19%     -9    1   11    9  135%
c i   98.9   14583    84434    208721  102890  26443 58916   10    47   31  20%    -25   -2    8    9   99%
c i   99.9   14582    84434    211572  105612  26481 58923   10    47   31  21%    -16   -2   11    9  133%
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  103.9   14581    84434    222911  116356  26748 58949   10    40   36  24%    109  -10   10    9  115%
c i  105.5   14580    84434    226600  119848  26820 58961   10    49   38  21%     -6   -1   11    9  123%
c i  107.3   14579    84434    230705  123776  26895 58977   10    47   38  22%     -2   -3   12    9  129%
c -  107.8   14579    84434    231689   90403  26910 58980   10    46   24  22%    -27   -3   11    9  117%
c i  109.4   14578    84434    237137   95477  27017 58995    9    40   29  22%     34   -9    9    9  104%
c i  110.1   14577    84434    239462   97671  27086 58997    9    43   28  22%    -20   -6   10    9  114%
c i  110.6   14575    84434    241226   99302  27112 59003    9    41   29  23%    -30   -8   10    9  109%
c i  112.3   14574    84434    244809  102708  27208 59018   11    51   30  21%     -7    3   15    9  167%
c i  112.4   14573    84434    245171  103056  27211 59021   11    51   30  21%    -18    2   11    9  125%
c i  113.9   14571    84434    250435  107975  27414 59036   10    52   30  18%     20    3    8    9   88%
c i  113.9   14569    84434    250436  107975  27414 59036   10    52   30  18%     19    3    8    9   88%
c 
c [simplification-14] limit 269705 conflicts (hard 331683) hit after 271479 conflicts
c [quatres-10] found 38035 quaternary clauses 34% in total
c [quatres-10-1] removed 4 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 156 single-self-subsuming ternary resolvents
c [quatres-10-2] added 305 quaternary resolvents
c [ternres-10] limit 29117896 with penalty 0 = 0 + 0
c [ternres-10] all 14565 free variables schedulable
c [ternres-10] 1869 ternary resolvents (15 bin, 1854 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 727947 penalty 3 = 3 + 0
c [gauss-4] extracted 116 xors of average arity 2.9
c [gauss-4] connected 338 occurrences of 113 variables (average 3.0)
c [gauss-4] limit 727947 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-35] removed 15 variables
c [unhide-12] limit 2911789 with penalty 1 = 1 + 0
c [unhide-12-13] 4 units, 20 failed, 13453 tauts, 0 hbrs, 267360 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 737 transitive binary clauses
c [transred-10] found 1 units
c [cce-7] limit of 36397370 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 17
c [cce-7-1] eliminated 1 clauses out of 13 (8%) of length 16
c [cce-7-1] eliminated 1 clauses out of 31 (3%) of length 10
c [cce-7-1] eliminated 1 clauses out of 149 (1%) of length 9
c [cce-7-1] eliminated 4 clauses out of 867 (0%) of length 8
c [cce-7-1] eliminated 18 clauses out of 1327 (1%) of length 7
c [cce-7-1] eliminated 183 clauses out of 4409 (4%) of length 6
c [cce-7-1] eliminated 198 clauses out of 7892 (3%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 407 large clauses in 36397371 steps
c [cce-7-1] allowing another 18198685 steps for small clauses
c [cce-7-1] scheduling 27934 clauses = 15260 binary + 12674 ternary
c [cce-7-1] tried to eliminate 12411 small clauses 44%
c [cce-7-1] eliminated 254 binary clauses 2%
c [cce-7-1] eliminated 278 ternary clauses 2%
c [cce-7-1] eliminated 532 small clauses 2%
c [cce-7-1] eliminated 545 small clauses in 36397384 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 952 covered clauses in round 1
c [cce-7] eliminated 952 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 14539 variables 100%
c [elim-10] limit of 291178965 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 149 variables 1% in round 1 in 13845250 steps
c [elim-10-1] backward subsumption/strengthening limit 13845200
c [elim-10-1-1] backward checking 1385 touched variables 10%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 5 and strengthened 3 clauses in 447954 steps
c [elim-10-1] rescheduled 22 variables 0% by backward subsumption
c [elim-10-2] no variable eliminated in round 2 in 128697 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 149 = 1% variables out of 14539 scheduled
c [bca-10] limit of 10000000 steps and 165742 added (scaled 2)
c [bca-10] 5049 out of 28782 literals actually usable 18%
c [bca-10] added 8 blocked clauses in 129063 steps
c [sweep-8] limit 2183842 penalty 2 = 2 + 0
c [sweep-8-1] 2803 pos 28.5% + 7036 neg 71.5% = 9839 sched 68.4% ret 4551
c [sweep-8-1] 2234237 steps 29 queries 2613.00 avg class size
c [sweep-8-1] 929 decisions 27 SAT calls 116.89 avg env size
c [sweep-8-1] 9617 variables remain 67% (4773 retained 33%)
c [decomp-36] removed 5 variables
c [sweep-8-1] removed 5 vars (0 failed, 3 eqs, 3 impls)
c [sweep-8] 5 < 1/1000 * 14390 = 14 considered unsuccessful
c [sweep-8] removed 5 vars in TOTAL (1 rounds, 28 queries)
c [sort-queue-14] sorted 14385 enqueued variables after 271479 conflicts
c [score-dist-14] active 0 (0%), one 14265 (99%), zero 120 (1%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 180 variables 1.2% (14385 remain 16%)
c [simplification-14] removed 1881 irredundant clauses 2.2% (82553 remain 31%)
c [simplification-14] maximum reduction of 2% = max (1%, 2%)
c [simplification-14] geometric conflict interval increment 41332 = 123996 / 3
c [simplification-14] new conflict interval 165328
c [simplification-14] penalized conflict interval 165328 = 1 * 165328
c [simplification-14] hard conflict limit 519471 (soft 436807 + delta 82664)
c [simplification-14] new conflict limit 436807 (hard 519471)
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  127.7   14384    82553    274373  119489  28705 44501   10    45   33  23%    269   -3   11    9  120%
c i  128.1   14383    82553    275433  120479  28728 44511   10    47   33  22%     42   -1   10    9  110%
c i  128.4   14381    82553    276503  121426  28751 44523   10    41   33  23%    -38   -7    5    9   53%
c -  133.0   14381    82553    288731   99236  29038 44552   10    49   24  21%     84    2   11   10  116%
c i  134.2   14380    82553    293525  103813  29137 44558   10    47   28  20%    151   -0    6   10   67%
c i  136.3   14379    82553    300518  110391  29388 44566   10    55   30  18%     -4    7   10   10  109%
c i  136.6   14375    82553    301275  111065  29426 44571   10    52   31  19%    -49    4   10   10  103%
c i  136.8   14374    82553    302068  111838  29430 44572   10    55   31  19%    -70    7   14   10  149%
c i  139.2   14373    82553    308259  117640  29620 44593   10    50   34  21%    -10    1   11   10  112%
c i  139.4   14372    82553    308634  117990  29627 44595   10    47   34  21%    -34   -2    8   10   82%
c i  139.4   14371    82553    308635  117990  29627 44595   10    47   34  21%    -34   -2    8   10   82%
c i  139.6   14367    82553    309111  118452  29630 44595   10    47   34  22%    -53   -2   13   10  131%
c i  145.3   14366    82553    323591  132277  29897 44624   11    49   37  23%    117    2   10   10  100%
c i  148.5   14365    82553    332430  140632  30152 44649   11    50   39  22%     31    1   12   10  123%
c -  148.8   14365    82553    332774  107077  30159 44650   11    50   26  22%     -4    1   13   10  128%
c i  149.0   14364    82553    333139  107379  30180 44658   11    49   30  22%    -27    1    8   10   85%
c i  154.4   14363    82553    349679  123065  30431 44690   10    42   33  24%    144   -6   11   10  111%
c i  154.4   14362    82553    349680  123065  30431 44690   10    42   33  24%    144   -6   11   10  111%
c i  157.6   14361    82553    358159  131127  30532 44710   11    42   36  26%     20   -6   13   10  126%
c i  158.2   14360    82553    359450  132297  30565 44715   11    42   36  26%    -54   -7    7   10   69%
c i  158.9   14358    82553    360493  133292  30591 44722   12    45   36  26%    -74   -3   13   10  128%
c i  158.9   14357    82553    360494  133292  30591 44722   12    45   36  26%    -74   -3   13   10  128%
c i  160.4   14354    82553    363863  136473  30652 44733   11    44   39  26%    -53   -4   12   10  121%
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  161.9   14353    82553    366875  139354  30709 44741   11    42   39  27%    -54   -5    9   10   86%
c i  161.9   14352    82553    366876  139354  30707 44743   11    42   39  27%    -54   -6    9   10   86%
c i  165.4   14351    82553    375958  147861  30877 44766   10    39   42  27%     41   -8   12   10  114%
c -  165.9   14351    82553    377746  115551  30914 44769   10    36   26  28%    -48  -10   11   10  103%
c i  171.3   14350    82553    392947  130079  31137 44801   11    48   35  23%    154    2   12   10  116%
c i  175.6   14349    82553    402595  139311  31291 44824   12    41   36  29%     41   -4   11   11  105%
c i  176.6   14348    82553    404821  141453  31334 44826   12    42   38  28%    -57   -3   12   11  110%
c i  176.6   14333    82553    404875  141505  31335 44826   12    42   38  28%    -59   -3   11   11  106%
c i  177.8   14332    82553    407472  144016  31352 44830   12    42   40  29%    -62   -4   12   11  114%
c i  177.9   14331    82553    407783  144297  31360 44830   12    41   43  29%    -68   -5    9   11   85%
c -  182.3   14331    82553    419445  120974  31511 44849   11    35   26  31%     78  -10    8   11   72%
c i  184.4   14330    82553    426261  127588  31585 44861   12    50   33  23%    171    5   12   11  110%
c i  185.3   14327    82553    429615  130764  31649 44869   11    44   35  24%    -54   -1   12   11  114%
c i  186.9   14325    82553    434500  135451  31742 44878   11    44   36  25%    -36   -1    9   11   87%
c i  190.9   14324    82553    443761  144314  31845 44893   12    39   41  31%     36   -5   14   11  129%
c i  193.1   14321    82553    448429  148667  31936 44910   10    33   41  31%    -31  -10    7   11   63%
c 
c [simplification-15] limit 436847 conflicts (hard 519471) hit after 456929 conflicts
c [quatres-11] found 41495 quaternary clauses 31% in total
c [quatres-11-1] removed 21 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 184 single-self-subsuming ternary resolvents
c [quatres-11-2] added 348 quaternary resolvents
c [ternres-11] limit 50197811 with penalty 0 = 0 + 0
c [ternres-11] all 14321 free variables schedulable
c [ternres-11] 2963 ternary resolvents (21 bin, 2942 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1568681 penalty 4 = 4 + 0
c [card-5] found 208 at-most-one constraints of average size 3.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1568681 for elimination
c [card-5] 208 out of 208 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-37] removed 77 variables
c [unhide-13] limit 10039562 with penalty 0 = 0 + 0
c [unhide-13-17] 0 units, 30 failed, 7482 tauts, 0 hbrs, 499381 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 409 transitive binary clauses
c [transred-11] found 1 units
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 14302 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 105 variables 1% in round 1 in 13493973 steps
c [elim-11-1] backward subsumption/strengthening limit 13493900
c [elim-11-1-1] backward checking 907 touched variables 6%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 4 clauses in 286914 steps
c [elim-11-1] rescheduled 10 variables 0% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 24699 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 105 = 1% variables out of 14302 scheduled
c [elim-11] 105 < 1/100 * 14302 = 143 considered unsuccessful
c [bca-11] limit of 10000000 steps and 163686 added (scaled 2)
c [bca-11] 3702 out of 28396 literals actually usable 13%
c [bca-11] added 2 blocked clauses in 150344 steps
c [sort-queue-15] sorted 14197 enqueued variables after 456929 conflicts
c [score-dist-15] active 0 (0%), one 14114 (99%), zero 83 (1%)
c [score-dist-15] max exp 1, different 2 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 124 variables 0.9% (14197 remain 16%)
c [simplification-15] removed 1028 irredundant clauses 1.2% (81525 remain 31%)
c [simplification-15] maximum reduction of 1% = max (1%, 1%)
c [simplification-15] geometric conflict interval increment 82664 = 165328 / 2
c [simplification-15] new conflict interval 247992
c [simplification-15] penalized conflict interval 247992 = 1 * 247992
c [simplification-15] hard conflict limit 828917 (soft 704921 + delta 123996)
c [simplification-15] new conflict limit 704921 (hard 828917)
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  202.1   14196    81525    460596  144919  33568 38109   12    50   38  24%     85    8   13   11  117%
c i  203.6   14195    81525    464545  148683  33640 38115   11    46   39  25%    -38    3   10   11   95%
c i  204.8   14193    81525    467962  151863  33736 38131   11    39   40  28%    -45   -3    6   11   58%
c -  207.2   14193    81525    475246  124196  33863 38149   10    38   26  27%     17   -4    8   11   75%
c i  207.5   14192    81525    476555  125413  33889 38153   10    32   31  29%     37  -10    7   11   60%
c i  207.9   14191    81525    478119  126910  33923 38156   10    47   31  22%    -44    5   12   11  108%
c i  210.6   14190    81525    487194  135502  34044 38178    9    28   33  31%     47  -14    6   11   56%
c i  214.6   14189    81525    499186  146771  34285 38218    8    28   37  29%     90  -14    6   11   55%
c i  217.2   14187    81525    505665  152999  34340 38228   10    33   39  31%      6   -9   11   11  108%
c i  217.2   14169    81525    505667  152999  34340 38229   10    33   39  31%      6   -9   11   11  107%
c i  219.6   14168    81525    511625  158742  34398 38250   11    37   40  30%      1   -3    9   11   87%
c i  219.6   14166    81525    511626  158742  34398 38250   11    37   40  30%      1   -3    9   11   87%
c -  222.8   14165    81525    518855  130944  34472 38263   11    34   27  32%     23   -6    9   11   84%
c i  224.1   14164    81525    522840  134659  34497 38270    9    21   32  43%     82  -19    7   11   66%
c i  229.7   14162    81525    537802  149109  34675 38292   12    41   37  28%    132    1   13   11  117%
c i  229.7   14161    81525    537805  149105  34675 38294   12    41   37  28%    132    1   12   11  116%
c i  233.4   14160    81525    545657  156527  34822 38315   10    33   42  32%     23   -7    9   11   84%
c i  238.6   14158    81525    557732  168160  34968 38329   12    39   45  30%     87   -0   11   11   98%
c -  240.7   14158    81525    562775  137792  35033 38332    9    34   28  28%    -19   -5    7   11   62%
c i  242.8   14157    81525    569076  143761  35144 38347    9    32   35  30%     75   -6   11   11  108%
c i  244.7   14155    81525    572909  147482  35193 38348   12    40   36  29%    -37    2   15   11  142%
c i  253.2   14149    81525    591139  164945  35430 38368   13    43   41  29%    172    4   14   11  123%
c i  253.6   14141    81525    591948  165734  35436 38368   13    46   41  28%     27    7   14   11  130%
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 -  259.6   14141    81525    604830  141182  35658 38402   12    40   29  30%     87   -0   18   11  164%
c i  260.8   14140    81525    607955  144073  35685 38409   10    30   35  34%    131  -10    7   11   63%
c i  263.4   14119    81525    614808  150666  35759 38426   11    45   37  26%     -9    5    9   11   79%
c i  263.4   14118    81525    614842  150678  35766 38432   11    44   37  26%    -12    5    8   11   72%
c i  276.5   14116    81525    642373  176930  36107 38480   13    44   48  31%    274    3   14   12  124%
c -  279.8   14112    81525    650430  147116  36256 38498   12    36   29  32%    -26   -4   14   11  118%
c i  280.9   14111    81525    652644  149266  36285 38501   12    42   36  29%      9    2   13   11  115%
c i  281.6   14106    81525    654933  151440  36295 38502   11    32   37  34%    -96   -8    8   11   73%
c i  281.7   14105    81525    654934  151440  36295 38502   11    32   37  34%    -96   -8    8   11   73%
c i  284.1   14104    81525    661017  157218  36383 38511   13    38   39  33%    -46   -1   14   12  119%
c i  290.6   14103    81525    674104  169699  36539 38539   13    43   42  30%     69    4   15   12  126%
c i  296.4   14102    81525    684150  179356  36662 38564   13    41   50  33%     26    1   11   12   89%
c i  297.3   14101    81525    686889  181981  36681 38568   13    42   50  31%    -75    3   14   12  121%
c i  300.6   14100    81525    692575  187475  36730 38577   14    45   51  31%    -33    5   15   12  121%
c -  301.6   14099    81525    693841  151064  36748 38578   14    44   31  32%    -76    4   12   12   97%
c 
c [simplification-16] limit 704949 conflicts (hard 828917) hit after 704949 conflicts
c [quatres-12] found 44906 quaternary clauses 29% in total
c [quatres-12-1] removed 25 duplicate quaternary clauses
c [quatres-12-1] added 2 double-self-subsuming ternary resolvents
c [quatres-12-2] added 165 single-self-subsuming ternary resolvents
c [quatres-12-2] added 341 quaternary resolvents
c [ternres-12] limit 81663770 with penalty 0 = 0 + 0
c [ternres-12] all 14099 free variables schedulable
c [ternres-12] 3523 ternary resolvents (25 bin, 3498 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-38] removed 126 variables
c [treelook-5] limit 2041594 penalty 2 = 2 + 0 boost 1
c [treelook-5] scheduled 21056 literals 75%
c [treelook-5] scheduling used 791574 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2041594 penalty 2 = 2 + 0 boost 1
c [treelook-5] used 2044535 steps
c [treelook-5] 20766 literals remain 74%
c [treelook-5] 8696 variables remain to probed next time 62%
c [decomp-39] removed 2 variables
c [treelook-5] removed 3 variables, found 5439 hbrs
c [unhide-14] limit 16332754 with penalty 0 = 0 + 0
c [unhide-14-24] 4 units, 16 failed, 7397 tauts, 0 hbrs, 235070 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 280 transitive binary clauses
c [transred-12] found 1 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 2041594255 steps penalty 1 = 1 + 0
c [cce-8-1] eliminated 1 clauses out of 9 (11%) of length 15
c [cce-8-1] eliminated 2 clauses out of 12 (17%) of length 11
c [cce-8-1] eliminated 1 clauses out of 105 (1%) of length 9
c [cce-8-1] eliminated 1 clauses out of 669 (0%) of length 8
c [cce-8-1] eliminated 14 clauses out of 1098 (1%) of length 7
c [cce-8-1] eliminated 122 clauses out of 4237 (3%) of length 6
c [cce-8-1] eliminated 411 clauses out of 7136 (6%) of length 5
c [cce-8-1] eliminated 747 clauses out of 17786 (4%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 1299 large clauses in 34825534 steps
c [cce-8-1] allowing another 17412767 steps for small clauses
c [cce-8-1] scheduling 27120 clauses = 14915 binary + 12205 ternary
c [cce-8-1] tried to eliminate 27120 small clauses 100%
c [cce-8-1] eliminated 153 binary clauses 1%
c [cce-8-1] eliminated 193 ternary clauses 2%
c [cce-8-1] eliminated 346 small clauses 1%
c [cce-8-1] eliminated 440 small clauses in 36825060 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 1739 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 16627005 steps for small clauses
c [cce-8-2] scheduling 26774 clauses = 14762 binary + 12012 ternary
c [cce-8-2] tried to eliminate 26774 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 1739 covered clauses in TOTAL during 2 rounds
c [bca-12] limit of 10000000 steps and 157711 added (scaled 2)
c [bca-12] 3355 out of 28064 literals actually usable 12%
c [bca-12] added 10 blocked clauses in 164911 steps
c [sort-queue-16] sorted 14031 enqueued variables after 704949 conflicts
c [score-dist-16] active 0 (0%), one 13957 (99%), zero 74 (1%)
c [score-dist-16] max exp 1, different 2 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 68 variables 0.5% (14031 remain 16%)
c [simplification-16] removed 2988 irredundant clauses 3.7% (78537 remain 30%)
c [simplification-16] maximum reduction of 4% = max (0%, 4%)
c [simplification-16] geometric conflict interval increment 49598 = 247992 / 5
c [simplification-16] new conflict interval 297590
c [simplification-16] penalized conflict interval 297590 = 1 * 297590
c [simplification-16] hard conflict limit 1151334 (soft 1002539 + delta 148795)
c [simplification-16] new conflict limit 1002539 (hard 1151334)
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  312.7   14030    78537    705501  157406  39014 37906   12    42   38  29%     82    1   11   12   88%
c i  314.5   14029    78537    711124  162868  39071 37911   12    38   38  31%    -28   -4   11   12   91%
c i  314.5   14028    78537    711130  162871  39073 37911   12    37   38  31%    -29   -4   11   12   89%
c i  320.7   14027    78537    725642  176839  39187 37931   12    40   45  30%    108   -0    6   12   53%
c i  321.0   14022    78537    726449  177602  39189 37931   12    37   45  33%     -3   -3   11   12   89%
c -  326.8   14016    78537    737976  151776  39275 37937   14    40   29  36%     64    0   19   12  151%
c i  330.2   14015    78537    746017  159470  39356 37948   12    39   37  32%    175   -1   10   12   80%
c i  338.8   14014    78537    763565  176409  39509 37975   14    37   43  37%    137   -2   15   13  116%
c i  340.1   14013    78537    765582  178351  39527 37981   14    40   44  36%    -68    1   15   13  117%
c -  346.0   14013    78537    782006  156585  39660 38000   11    31   30  37%    119   -8   10   13   78%
c i  353.1   14012    78537    799318  173100  39765 38018   11    25   44  43%    329  -11    8   12   65%
c i  353.1   14001    78537    799328  173109  39765 38018   11    25   44  43%    324  -11    8   12   63%
c i  361.6   14000    78537    816262  189378  39876 38046   12    32   66  38%     74   -4   16   12  127%
c i  361.6   13999    78537    816263  189378  39876 38046   12    32   66  38%     74   -4   16   12  126%
c -  366.4   13999    78537    825769  160607  39937 38054   12    25   44  48%    -30  -10   11   12   90%
c i  381.0   13998    78537    859408  193034  40108 38088   14    37   56  37%    393    2   15   13  117%
c i  381.0   13997    78537    859410  193035  40108 38088   14    37   56  37%    392    2   15   13  116%
c i  385.1   13996    78537    868723  201890  40199 38106   11    30   56  38%   -117   -4   10   12   80%
c -  385.4   13996    78537    869321  164535  40200 38106   12    31   31  38%   -171   -3   13   12  103%
c i  387.1   13995    78537    872429  167554  40216 38109   13    33   39  39%   -191   -1   14   12  116%
c i  389.1   13994    78537    877540  172496  40241 38115   13    31   41  41%   -157   -3   14   12  114%
c i  390.8   13993    78537    880336  175144  40266 38121   13    32   41  41%   -181   -1   11   12   90%
c i  390.9   13961    78537    880507  175286  40274 38124   13    31   41  41%   -185   -2    9   12   72%
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  398.0   13642    78537    896563  190550  40371 38142   13    29   48  46%     43   -5   13   13  103%
c i  400.2   13641    78537    902704  196537  40386 38145   13    26   50  51%   -101   -7   16   13  128%
c i  400.5   13635    78537    903213  197021  40389 38148   13    27   50  49%   -130   -5   15   13  123%
c -  404.9   13634    78537    912449  167470  40456 38160   13    28   31  47%    -37   -4   11   13   90%
c i  413.0   13633    78537    933798  187738  40640 38180   12    22   44  55%    258   -7   14   12  112%
c i  413.0   13632    78537    933919  187855  40642 38180   12    23   44  54%    206   -6   14   12  111%
c i  418.2   13631    78537    945842  199172  40708 38195   11    19   53  56%    -19   -9    9   12   72%
c i  422.2   13630    78537    951995  205020  40747 38204   13    22   68  60%    -97   -6    9   12   76%
c i  423.9   13625    78537    954963  207761  40771 38210   12    21   73  59%   -136   -6    9   12   71%
c -  425.0   13621    78537    956968  171365  40786 38213   12    21   46  58%   -145   -6   10   12   85%
c i  426.3   13620    78537    959705  173872  40800 38218   11    19   54  59%   -103   -7    9   12   70%
c 0  426.3    5407    78537    959705  173872  40800 38218   11    19   54  59%   -104   -7    9   12   70%
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 UNSATISFIABLE
c
c bate: 266 basic ate = 208 trn 78% + 58 lrg 22% in 3 updates
c bcas: 12 count, 285 added (120 skipped), 1031741 steps
c bkwd: tried 86894 clauses, 172486 lits, 1.99 lits/clause
c bkwd: checked 3963228 occs, 45.61 occs/clause, 22.98 occs/lit
c bkwd: subsumed 0 binary, 13 ternary, 26 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 1924 large (0% self)
c blkd: 4 bces, 1047 removed, 1963935 resolutions, 4980863 steps
c blkd: 1886 blocking literals 1%, 1 pure
c bump: 956751 bumped seen, 154896852 lits 161.9 on average
c card: 5 count, 0 units, 117 am1, 29339630 steps
c card: 53 rescheduled, 523 eliminated, 7780 resolved, 2562 subsumed
c card: 945 at-most-one constraints found, average size 3.08
c card: 945 at-most-one constraints used 100%, average size 3.08
c card: 16 at-most-two constraints found, average size 4.00
c card: 16 at-most-two constraints used 100%, average size 4.00
c cces: 8 cces, 17692 eliminated, 16757 ate 95%, 935 abce 5%
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: 875524 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 107 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 39 decompositions, 1459 equivalent 2%
c deco: 311 decision-only clauses 0%, 65% reduction
c decs: 4488654 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 11 elims, 71517 eliminated 81%, 33 pure 0%
c elms: 21 rounds, 1.9 rounds/bve
c elms: 69568 small 97%, 1915 large 3%
c elms: 78677 tried small, 69568 succeeded 88%, 9109 failed 12%
c elms: 5050 subsumed, 15106 strengthened, 363 blocked
c elms: 4233023 copies, 5643966 resolutions, 1301246 ipos
c elms: 873088 subchks, 762889 strchks
c gaus: 4 extractions, 1244 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8460878 steps, 4230439 extr 50%, 19077 elim 0%
c glue: 10.7 orig avg, 10.7 real avg, 2.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 88620 = 19345 simple 22% + 67689 trn 76% + 1586 lrg 2%, 2012 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 956751 clauses, 58.5 length
c lrnd: 55956262 lits = 93685907 orig - 37729645 removed 40%
c lrnd: 276736 uips 29%, 556534 flips 58%
c mins: 927012 mins 97%, 2001 bin 0%, 27426 size 3%
c mins: 273859330 poisoned searches, 32249252 hits, 12% hit rate
c mins: 333844418 used twice searches, 3772571 hits, 1% hit rate
c move: moved 7580, 2128 bin 28%, 5452 trn 72%
c otfs: 4080 driving 28%, 10705 restarting 72%
c otfs: str 14785, 14020 red 95%, 765 irr 5%
c otfs: str 14785, 0 bin 0%, 706 trn 5%, 14079 lrg 95%
c otfs: sub 73, 70 red 96%, 3 irr 4%
c otfs: sub 73, 0 bin 0%, 30 trn 41%, 43 lrg 59%
c phas: 10 computed, 19739 set, 0 pos (0%), 19739 neg (100%)
c prbs: 4 basic, 45721 probed, 178 failed, 3 lifted
c prbs: 5 simple, 237512 probed, 222 failed, 3155 eqs
c prbs: 5 treelook, 898 probed, 4 failed, 0 lifted
c prom: 351582 locked 8% out of 4334122 tried
c prps: 681755855 props, 151 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 12 count, 7287 quat, 1535 self1, 12 self2, 102 dup
c queu: 16 sorted, 4488654 next (17 steps 0.00)
c queu: 155235005 enq (155234972 steps 1.00), 154896852 deq 100%
c redc: 56710 clauses 21%, 274835 tried 29%, 66 sat 0%
c redc: 86072 lits 3%, 3004904 tried 3%, 66 sat 0%
c redc: 2645 times jump level reduced, 4.7 levels on average
c reds: 19 count, 50510.8 conflicts per reduce
c reds: 0 memlim 0%, 19 arith 100%
c reds: 559486 collected 81%, 132939 retired 19%
c rmbd: 2061 removed, 1836 red 89%
c rsts: 34944 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: 16 count, 13 confs 81%, 0 vars 0%
c simp: 1 its 6%, 1 bin 6%, 1 trns 6%
c subl: 956751 count (1187965 tried 1.2), 24606 sub out of 933013 (2.6%)
c swps: 8 count, 9 rounds, 2610 queries (290.0/round)
c swps: 2571 sat calls, 23 unsat (0.4% success rate)
c swps: 40517 decisions 15.8, 1126 conflicts 0.4
c swps; 691.4 avg class size, 32.0 avg environment size
c swps: 0 failed, 83 impls, 60 equivs
c swp0: 867 type 0 queries, 88 unsat (10.1%), 857 sat (98.8%)
c swp1: 1743 type 1 queries, 431 unsat (24.7%), 1693 sat (97.1%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 10891285 calls to obtain time
c tops: 9969 fixed 11%, 167 its, 5746.74 confs/it
c trds: 12 transitive reductions, 6981 removed, 19 failed
c trds: 207199 nodes, 250278 edges, 18043723 steps
c trim: 378638 words, 1.4 MB
c trnr: 12 count, 181 bin, 27785 trn, 87752291 steps
c unhd: 14 count, 24 rounds, 45334290 steps
c unhd: 292 non-trivial sccs of average size 2.0
c unhd: 37 units, 36 bin, 1 trn, 0 lrg
c unhd: 177 failed, 168 stamp, 0 lits, 4 bin, 4 trn, 0 lrg
c unhd: 37784 tauts, 733 bin 2%, 8493 trn 22%, 4136 lrg 11%
c unhd: 37784 tauts, 24422 stamp 65%, 35930 red 95%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1145096 str, 36 bin 0%, 3231 trn 0%, 1141829 lrg 100%, 1116782 red 98%
c vars: 5407 remaining 6% and 82945 removed 94% out of 88352
c vars: 9969 fixed 11%, 71517 eliminated 81%, 1459 equivalent 2%
c vsts: 11402900698 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 16.8 search visits per propagation, 11824.4 per conflict
c wchs: 2423510362 pushed, 14444445 enlarged, 173 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         940300        559486        132939     129278681      20608145        529842
c 
c  0 0        188807  20     22656   4         0   0 101101127  78< 14142868  69    259766  49     5.0
c  1 5         69944   7     44232   8     12743  10  11356762   9   2133838  10<    46880   9<    0.8
c  2 6        191110  20<   136244  24     31857  24  11534637   9   2566901  12     85547  16     2.7
c  3 9        241127  26    179565  32<    37422  28<  4036856   3   1220887   6     80226  15     6.5
c  4 14       160852  17    119544  21     28187  21    916358   1    390321   2     37545   7     5.7
c  5 21        58719   6     39895   7     13650  10    226486   0    104294   1     12108   2     3.0
c  6 30        18153   2     11196   2      5230   4     77461   0     31552   0      4408   1     1.0
c  7 41         6844   1      3831   1      2225   2     18165   0     10981   0      2117   0     0.4
c  8 54         2700   0      1432   0       913   1      6513   0      3890   0       788   0     0.1
c  9 69         1185   0       593   0       416   0      2795   0      1680   0       292   0     0.1
c 10 86          623   0       261   0       218   0      1247   0       804   0       159   0     0.1
c 11 126         234   0        37   0        76   0       272   0       129   0         6   0     0.0
c 12 230           2   0         0   0         2   0         2   0         0   0         0   0     0.0
c 
c avg                  2.5           2.9           3.2           0.4           0.6           1.4
c std                  1.7           1.4           1.5           0.9           1.1           1.6
c 
c   17.237   4% bump
c   13.378   3% cce
c    7.279   2% unhide
c    5.011   1% elim
c    3.901   1% probe
c    2.915   1% decide
c    1.619   0% sweep
c 
c    5.225 < 1% rest (below)
c 
c    1.377   0% quatres
c    1.247   0% transred
c    0.714   0% bca
c    0.689   0% ternres
c    0.507   0% block
c    0.457   0% gauss
c    0.235   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    2.268   1% preprocessing     6%
c   36.739   9% inprocessing     94%
c ==================================
c   39.007   9% simplifying
c  387.259  91% search
c ==================================
c  426.268 100% all
c 
c        959705 conflicts,        2251.4 confs/sec
c         20211 ternaries,          47.5 confs/ternary
c          3015 binaries,          318.3 confs/binary
c           167 iterations,       5746.7 confs/iteration
c 
c            19 reductions,          0.0 redus/sec,  50510.8 confs/reduction
c         34944 restarts,           82.0 rests/sec,     27.5 confs/restart
c       4488654 decisions,       10530.1 decis/sec,      4.7 decis/conflict
c     681755855 propagations,  1599358.7 props/sec,    151.9 props/decision
c 
c 426.3 seconds, 73.5 MB
c launch: done
