c launch: /data/cnf/sc2014/app/IBM_FV_2004_rule_batch_1_31_1_SAT_dat.k40.debugged.cnf.bz2
c host: atom02
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/IBM_FV_2004_rule_batch_1_31_1_SAT_dat.k40.debugged.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/IBM_FV_2004_rule_batch_1_31_1_SAT_dat.k40.debugged.cnf.bz2
c no embedded options
c found 'p cnf 52444 217642' header
c read 52444 variables, 217642 clauses, 547043 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=0
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 50629 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] STATIC (--score=0)
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   50629   210196         0       0      0     0    0     0   10   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 2338 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] 2338 out of 2338 constraints (100%) meet size limits
c [card-1] found 9 units
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 16385 variables
c [simpleprobe-1] all 36059 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 5612 variables
c [simpleprobe-1] 130 variables remain 0% (30317 retained 100%)
c [simpleprobe-1] removed 5612 variables, found 35460 hbrs, 747 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 9 units, 7 failed, 349 tauts, 0 hbrs, 644 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 30420 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 18857 variables 62% in round 1 in 12327619 steps
c [elim-1-1] backward subsumption/strengthening limit 7672381
c [elim-1-1-1] backward checking 21884 touched variables 72%
c [elim-1-1-1] incomplete backward checking 21619 remain 99%
c [elim-1-1] subsumed 5 and strengthened 111 clauses in 7675938 steps
c [elim-1] incomplete 385 not tried 1% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 18859 = 62% variables out of 30420 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 75533 negative 93.8% of 80551 except 5018 6.2%
c [phase-count-1] 69933 positive 86.8% of 80551 except 10618 13.2%
c [phase-count-1] less non-negative clauses 5018 than limit 8000 (10.0%)
c [phase-count-1] non-pos/non-neg = 10618/5018 = 2.12 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 11561 negative 100%
c [sort-queue-1] sorted 11561 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 11561 (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 34588 variables 74.9% (11561 remain 23%)
c [simplification-1] removed 129645 irredundant clauses 61.7% (80551 remain 38%)
c [simplification-1] maximum reduction of 75% = max (75%, 62%)
c [simplification-1] large reduction 75% >= 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    1.6   11560    80551       113      82     15  7651    0     8    7   1%      0    8    1    0 21034%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [decomp-3] removed 12 variables
c [simpleprobe-2] 40 schedulable variables 0%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 38 variables
c [simpleprobe-2] 564 variables remain 5% (10947 retained 95%)
c [simpleprobe-2] removed 38 variables, found 764 hbrs, 2 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 23022 literals 100%
c [treelook-1] scheduling used 263724 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 350335 steps
c [treelook-1] 22925 literals remain 100%
c [treelook-1] 11511 variables remain to probed next time 100%
c [decomp-5] removed 2 variables
c [treelook-1] removed 2 variables, found 723 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 6903 probes remain 60% after last round
c [basicprobe-1-0] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 25 variables, found 1394 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 1 units, 25 failed, 596 tauts, 0 hbrs, 4881 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 11409 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 298 variables 3% in round 1 in 14372366 steps
c [elim-2-1] backward subsumption/strengthening limit 5627634
c [elim-2-1-1] backward checking 3304 touched variables 29%
c [elim-2-1-1] incomplete backward checking 3247 remain 98%
c [elim-2-1] subsumed 0 and strengthened 19 clauses in 5627704 steps
c [elim-2] incomplete 70 not tried 1% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 298 = 3% variables out of 11409 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 11111 enqueued variables after 1001 conflicts
c [score-dist-2] active 0 (0%), one 0 (0%), zero 11111 (100%)
c [score-dist-2] max exp 0, different 1 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 449 variables 3.9% (11111 remain 22%)
c [simplification-2] removed 3325 irredundant clauses 4.1% (77226 remain 37%)
c [simplification-2] maximum reduction of 4% = max (4%, 4%)
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 15001 (soft 5001 + delta 10000)
c [simplification-2] new conflict limit 5001 (hard 15001)
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.6   11110    77226      1865    1345    250  8749    2   107    7   2%     14  106    4    0 3434%
c i    2.7   11053    77226      2115    1536    284  8765    2   117    7   2%     11  114    5    0 3097%
c i    2.8   11048    77226      2539    1874    334  8784    2   133    7   2%      9  130    5    0 2588%
c i    2.8   11047    77226      2573    1901    340  8784    2   136    7   2%      8  133    4    0 2515%
c i    2.9   11046    77226      2856    2141    366  8795    2   147    7   2%      7  143    5    0 2434%
c 
c [simplification-3] limit of 161 binary hit after 161 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 681 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 681 out of 681 constraints (100%) meet size limits
c [card-2] found 1 units
c [card-2] no units found
c [card-2] generated 6 at-most-one constraints, 4 used 67%
c [card-2] exported 4 binary clauses, 1.0 per/constraint
c [decomp-6] removed 93 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 22036 literals 100%
c [treelook-2] scheduling used 256487 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 302737 steps
c [treelook-2] 21843 literals remain 99%
c [treelook-2] 11018 variables remain to probed next time 100%
c [treelook-2] removed 0 variables, found 294 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 17 units, 10 failed, 444 tauts, 0 hbrs, 900 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 10969 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 143 variables 1% in round 1 in 13485213 steps
c [elim-3-1] backward subsumption/strengthening limit 6514787
c [elim-3-1-1] backward checking 846 touched variables 8%
c [elim-3-1-1] incomplete backward checking 841 remain 99%
c [elim-3-1] subsumed 1 and strengthened 16 clauses in 6515692 steps
c [elim-3] incomplete 75 not tried 1% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 143 = 1% variables out of 10969 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 10826 enqueued variables after 3283 conflicts
c [score-dist-3] active 0 (0%), one 0 (0%), zero 10826 (100%)
c [score-dist-3] max exp 0, different 1 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 220 variables 2.0% (10826 remain 21%)
c [simplification-3] removed 2194 irredundant clauses 2.8% (75032 remain 36%)
c [simplification-3] maximum reduction of 3% = max (2%, 3%)
c [simplification-3] forced so keeping old conflict interval 4000
c [simplification-3] conflict limit remains at 5001 (hard 15001)
c [simplification-3] new binary interval 1000
c 
c [simplification-4] limit 5001 conflicts (hard 15001) hit after 5001 conflicts
c [decomp-8] removed 12 variables
c [basicprobe-2] limit 1138842 penalty 0 = 0 + 0
c [basicprobe-2-0] 5437 probes remain 50% after last round
c [basicprobe-2-0] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 10 variables, found 1273 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 1 units, 13 failed, 451 tauts, 0 hbrs, 1598 literals
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 10790 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 95 variables 1% in round 1 in 13360839 steps
c [elim-4-1] backward subsumption/strengthening limit 13360800
c [elim-4-1-1] backward checking 659 touched variables 6%
c [elim-4-1-1] incomplete backward checking 560 remain 85%
c [elim-4-1] subsumed 1 and strengthened 22 clauses in 13360890 steps
c [elim-4-1] rescheduled 65 variables 1% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 77447 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 98 = 1% variables out of 10790 scheduled
c [elim-4] 98 < 1/100 * 10790 = 107 considered unsuccessful
c [sort-queue-4] sorted 10692 enqueued variables after 5001 conflicts
c [score-dist-4] active 0 (0%), one 0 (0%), zero 10692 (100%)
c [score-dist-4] max exp 0, different 1 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 134 variables 1.2% (10692 remain 21%)
c [simplification-4] removed 748 irredundant clauses 1.0% (74284 remain 35%)
c [simplification-4] maximum reduction of 1% = max (1%, 1%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 14000
c [simplification-4] penalized conflict interval 14000 = 1 * 14000
c [simplification-4] hard conflict limit 29001 (soft 19001 + delta 10000)
c [simplification-4] new conflict limit 19001 (hard 29001)
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    4.8   10691    74284      5996    4425    689  8880    4   222    7   2%     33  209    5    0 1188%
c i    5.0   10689    74284      6691    5013    757  8904    4   235    7   2%     19  221    5    0 1118%
c i    5.4   10688    74284      8274    6346    909  8966    5   245    7   2%     15  225    6    1  996%
c i    5.7   10655    74284      9555    7445   1008  9018    5   255    7   2%     11  231    5    1  728%
c i    6.0   10653    74284     10842    8551   1120  9049    5   258    8   2%     10  229    6    1  745%
c i    6.0   10652    74284     10939    8637   1126  9052    5   259    8   2%      9  230    6    1  705%
c i    6.1   10651    74284     11076    8755   1134  9058    5   262    8   2%      8  232    6    1  707%
c i    6.3   10642    74284     12016    9568   1214  9087    5   267    8   2%      7  234    6    1  715%
c i    6.5   10641    74284     12697   10137   1289  9108    5   274    8   2%      5  239    6    1  666%
c 
c [simplification-5] limit of 1620 ternary hit after 1620 ternaries
c [quatres-1] found 9317 quaternary clauses 31% in total
c [quatres-1-1] removed 6 duplicate quaternary clauses
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 48 single-self-subsuming ternary resolvents
c [quatres-1-2] added 420 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 10639 free variables schedulable
c [ternres-1] 4192 ternary resolvents (246 bin, 3946 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 4096 xors of average arity 2.9
c [gauss-1] connected 11694 occurrences of 620 variables (average 18.9)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 127 variables
c [gauss-1] exported 0 unary, 3 binary and 3 ternary equations
c [simpleprobe-3] 504 schedulable variables 5%
c [simpleprobe-3] limit 3338661 penalty 0 = 0 + 0
c [decomp-11] removed 225 variables
c [simpleprobe-3] 527 variables remain 5% (9760 retained 95%)
c [simpleprobe-3] removed 225 variables, found 1064 hbrs, 11 units
c [unhide-5] limit 166933 with penalty 0 = 0 + 0
c [unhide-5-5] 2 units, 1 failed, 285 tauts, 0 hbrs, 3652 literals
c [transred-1] limit 834665 with penalty 0 = 0 + 0
c [transred-1] removed 382 transitive binary clauses
c [transred-1] found 2 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 10280 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 94 blocked clauses
c [block-1] 94 < 1/100 * 71481 = 714 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 13
c [cce-1-1] eliminated 23 clauses out of 114 (20%) of length 12
c [cce-1-1] eliminated 49 clauses out of 446 (11%) of length 11
c [cce-1-1] eliminated 6 clauses out of 263 (2%) of length 10
c [cce-1-1] eliminated 103 clauses out of 1017 (10%) of length 9
c [cce-1-1] eliminated 103 clauses out of 1477 (7%) of length 8
c [cce-1-1] eliminated 64 clauses out of 2837 (2%) of length 7
c [cce-1-1] eliminated 443 clauses out of 4098 (11%) of length 6
c [cce-1-1] eliminated 63 clauses out of 5553 (1%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 856 large clauses in 30000020 steps
c [cce-1-1] allowing another 15000010 steps for small clauses
c [cce-1-1] scheduling 41563 clauses = 35403 binary + 6160 ternary
c [cce-1-1] tried to eliminate 6342 small clauses 15%
c [cce-1-1] eliminated 614 binary clauses 2%
c [cce-1-1] eliminated 93 ternary clauses 2%
c [cce-1-1] eliminated 707 small clauses 2%
c [cce-1-1] eliminated 707 small clauses in 30000013 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1563 covered clauses in round 1
c [cce-1] eliminated 1563 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 140052 added (scaled 2)
c [bca-1] 7563 out of 20560 literals actually usable 37%
c [bca-1] added 1 blocked clauses in 33412 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3474 pos 33.8% + 6805 neg 66.2% = 10279 sched 100.0% ret 0
c [sweep-1-1] 1010910 steps 53 queries 631.09 avg class size
c [sweep-1-1] 1460 decisions 52 SAT calls 97.65 avg env size
c [sweep-1-1] 9421 variables remain 92% (858 retained 8%)
c [decomp-12] removed 8 variables
c [sweep-1-1] removed 8 vars (0 failed, 3 eqs, 4 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 8 vars in TOTAL (1 rounds, 52 queries)
c [sort-queue-5] sorted 10271 enqueued variables after 16418 conflicts
c [score-dist-5] active 0 (0%), one 0 (0%), zero 10271 (100%)
c [score-dist-5] max exp 0, different 1 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 368 variables 3.5% (10271 remain 20%)
c [simplification-5] removed 4528 irredundant clauses 6.1% (69756 remain 33%)
c [simplification-5] maximum reduction of 6% = max (3%, 6%)
c [simplification-5] forced so keeping old conflict interval 14000
c [simplification-5] conflict limit remains at 19001 (hard 29001)
c [simplification-5] new ternary interval 10000
c 
c [simplification-6] limit 19001 conflicts (hard 29001) hit after 19002 conflicts
c [quatres-2] found 9641 quaternary clauses 32% in total
c [quatres-2-1] removed 3 duplicate quaternary clauses
c [quatres-2-2] added 16 single-self-subsuming ternary resolvents
c [quatres-2-2] added 409 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 10271 free variables schedulable
c [ternres-2] 225 ternary resolvents (6 bin, 219 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 364 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 364 out of 364 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 3551 xors of average arity 3.0
c [gauss-2] connected 10561 occurrences of 457 variables (average 23.1)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [decomp-13] removed 3 variables
c [gauss-2] exported 0 unary, 1 binary and 0 ternary equations
c [unhide-6] limit 197143 with penalty 0 = 0 + 0
c [unhide-6-6] 3 units, 6 failed, 920 tauts, 0 hbrs, 6309 literals
c [transred-2] limit 985716 with penalty 0 = 0 + 0
c [transred-2] removed 374 transitive binary clauses
c [transred-2] found 1 units
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 4 clauses out of 2725 (0%) of length 7
c [cce-2-1] eliminated 19 clauses out of 3693 (1%) of length 6
c [cce-2-1] eliminated 163 clauses out of 5362 (3%) of length 5
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 186 large clauses in 30000010 steps
c [cce-2-1] allowing another 15000005 steps for small clauses
c [cce-2-1] scheduling 41680 clauses = 34752 binary + 6928 ternary
c [cce-2-1] tried to eliminate 6055 small clauses 15%
c [cce-2-1] eliminated 461 binary clauses 1%
c [cce-2-1] eliminated 116 ternary clauses 2%
c [cce-2-1] eliminated 577 small clauses 1%
c [cce-2-1] eliminated 652 small clauses in 30000010 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 838 covered clauses in round 1
c [cce-2] eliminated 838 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 10258 variables 100%
c [elim-5] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 52 not tried 1% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 242 = 2% variables out of 10258 scheduled
c [bca-2] limit of 10000000 steps and 135234 added (scaled 2)
c [bca-2] 6969 out of 20034 literals actually usable 35%
c [bca-2] added 8 blocked clauses in 32860 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 3133 pos 34.2% + 6037 neg 65.8% = 9170 sched 91.6% ret 846
c [sweep-2-1] 1085938 steps 89 queries 602.82 avg class size
c [sweep-2-1] 1518 decisions 76 SAT calls 41.59 avg env size
c [sweep-2-1] 8030 variables remain 80% (1986 retained 20%)
c [decomp-15] removed 38 variables
c [sweep-2-1] removed 38 vars (0 failed, 12 eqs, 19 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 38 vars in TOTAL (1 rounds, 88 queries)
c [sort-queue-6] sorted 9978 enqueued variables after 19002 conflicts
c [score-dist-6] active 0 (0%), one 0 (0%), zero 9978 (100%)
c [score-dist-6] max exp 0, different 1 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 293 variables 2.9% (9978 remain 20%)
c [simplification-6] removed 2431 irredundant clauses 3.5% (67325 remain 32%)
c [simplification-6] maximum reduction of 3% = max (3%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 19000
c [simplification-6] penalized conflict interval 19000 = 1 * 19000
c [simplification-6] hard conflict limit 48002 (soft 38002 + delta 10000)
c [simplification-6] new conflict limit 38002 (hard 48002)
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   10.8    9977    67325     20367   16031   4844  9233    6   270    9   2%     97  208    6    2  400%
c i   12.0    9972    67325     24857   19955   5176  9361    6   266    9   2%     46  191    7    2  366%
c i   13.7    9971    67325     31223   25650   5558  9504    7   261   10   3%     70  169    7    2  315%
c i   13.9    9970    67325     32074   26396   5619  9528    7   261   10   3%     27  167    6    2  278%
c i   14.5    9965    67325     34048   28171   5733  9570    7   261   10   3%      9  162    7    2  271%
c i   14.5    9964    67325     34163   28272   5742  9572    7   260   10   3%      7  161    6    2  259%
c i   14.9    9963    67325     35588   29560   5814  9604    7   262   10   3%      1  159    7    3  278%
c 
c [simplification-7] limit 38002 conflicts (hard 48002) hit after 38002 conflicts
c [quatres-3] found 11534 quaternary clauses 33% in total
c [quatres-3-1] removed 3 duplicate quaternary clauses
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 44 single-self-subsuming ternary resolvents
c [quatres-3-2] added 329 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 9947 free variables schedulable
c [ternres-3] 421 ternary resolvents (1 bin, 420 trn)
c [ternres-3] 3 variables remain 0% (9944 retained 100%)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 2573 xors of average arity 2.9
c [gauss-3] connected 7495 occurrences of 513 variables (average 14.6)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-16] removed 44 variables
c [treelook-3] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 11612 literals 59%
c [treelook-3] scheduling used 150119 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 151929 steps
c [treelook-3] 11540 literals remain 58%
c [treelook-3] 8942 variables remain to probed next time 90%
c [decomp-17] removed 4 variables
c [treelook-3] removed 4 variables, found 203 hbrs
c [unhide-7] limit 431454 with penalty 0 = 0 + 0
c [unhide-7-7] 4 units, 5 failed, 210 tauts, 0 hbrs, 8862 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 589 transitive binary clauses
c [transred-3] found 3 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 9887 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 36 blocked clauses
c [block-2] 36 < 1/100 * 66578 = 665 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 2 clauses out of 84 (2%) of length 12
c [cce-3-1] eliminated 4 clauses out of 381 (1%) of length 11
c [cce-3-1] eliminated 1 clauses out of 255 (0%) of length 10
c [cce-3-1] eliminated 7 clauses out of 606 (1%) of length 9
c [cce-3-1] eliminated 9 clauses out of 1463 (1%) of length 8
c [cce-3-1] eliminated 100 clauses out of 2804 (4%) of length 7
c [cce-3-1] eliminated 147 clauses out of 3755 (4%) of length 6
c [cce-3-1] eliminated 76 clauses out of 5005 (2%) of length 5
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 346 large clauses in 30000004 steps
c [cce-3-1] allowing another 15000002 steps for small clauses
c [cce-3-1] scheduling 38661 clauses = 32957 binary + 5704 ternary
c [cce-3-1] tried to eliminate 6147 small clauses 16%
c [cce-3-1] eliminated 892 binary clauses 3%
c [cce-3-1] eliminated 85 ternary clauses 1%
c [cce-3-1] eliminated 977 small clauses 3%
c [cce-3-1] eliminated 977 small clauses in 30000007 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1323 covered clauses in round 1
c [cce-3] eliminated 1323 covered clauses in TOTAL during 1 rounds
c [elim-6] 52 variables 1% will be scheduled this time
c [elim-6] scheduled 52 variables 1%
c [elim-6] limit of 43145477 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 5721863 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 52 scheduled
c [bca-3] limit of 10000000 steps and 130788 added (scaled 2)
c [bca-3] 4776 out of 19774 literals actually usable 24%
c [bca-3] added 48 blocked clauses in 43518 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2803 pos 35.4% + 5114 neg 64.6% = 7917 sched 80.1% ret 1969
c [sweep-3-1] 1042377 steps 40 queries 660.12 avg class size
c [sweep-3-1] 1073 decisions 32 SAT calls 78.28 avg env size
c [sweep-3-1] 7498 variables remain 76% (2387 retained 24%)
c [decomp-18] removed 13 variables
c [sweep-3-1] removed 13 vars (0 failed, 7 eqs, 9 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 13 vars in TOTAL (1 rounds, 39 queries)
c [sort-queue-7] sorted 9873 enqueued variables after 38002 conflicts
c [score-dist-7] active 0 (0%), one 0 (0%), zero 9873 (100%)
c [score-dist-7] max exp 0, different 1 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 74 variables 0.7% (9873 remain 20%)
c [simplification-7] removed 2201 irredundant clauses 3.3% (65124 remain 31%)
c [simplification-7] maximum reduction of 3% = max (1%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 24000
c [simplification-7] penalized conflict interval 24000 = 1 * 24000
c [simplification-7] hard conflict limit 74002 (soft 62002 + delta 12000)
c [simplification-7] new conflict limit 62002 (hard 74002)
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.7    9872    65124     43773   37055   6639 10351    8   254   12   3%     93  133    7    3  218%
c i   19.8    9869    65124     47111   40105   6810 10402    8   250   12   3%     21  122    8    3  232%
c i   23.7    9868    65124     58479   50512   7351 10584    8   247   13   3%    132  101    8    4  201%
c i   23.7    9867    65124     58519   50550   7351 10585    8   247   13   3%    126  100    9    4  208%
c 
c [simplification-8] limit 62002 conflicts (hard 74002) hit after 62003 conflicts
c [quatres-4] found 13393 quaternary clauses 32% in total
c [quatres-4-1] removed 4 duplicate quaternary clauses
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 40 single-self-subsuming ternary resolvents
c [quatres-4-2] added 171 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 3 schedulable variables 0%
c [ternres-4] 56 ternary resolvents (0 bin, 56 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-19] removed 32 variables
c [basicprobe-3] limit 19714115 penalty 0 = 0 + 0
c [basicprobe-3-0] 4594 sched 47%, 58 failed, 1 lifted, 7113 hbrs
c [decomp-20] removed 111 variables
c [basicprobe-3-1] 5626 sched 58%, 24 failed, 0 lifted, 1726 hbrs
c [decomp-21] removed 33 variables
c [basicprobe-3-2] 4508 probes remain 46% after last round
c [basicprobe-3-2] 83 units = 82 failed (99%) + 1 lifted (1%)
c [basicprobe-3-2] removed 144 variables, found 8917 hbrs
c [bate-1] eliminated 137 asymmetric tautologies during probing
c [unhide-8] limit 788564 with penalty 0 = 0 + 0
c [unhide-8-8] 0 units, 0 failed, 1529 tauts, 0 hbrs, 36482 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 933 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 3 clauses out of 253 (1%) of length 10
c [cce-4-1] eliminated 11 clauses out of 582 (2%) of length 9
c [cce-4-1] eliminated 15 clauses out of 1349 (1%) of length 8
c [cce-4-1] eliminated 31 clauses out of 2643 (1%) of length 7
c [cce-4-1] eliminated 38 clauses out of 3648 (1%) of length 6
c [cce-4-1] eliminated 338 clauses out of 4743 (7%) of length 5
c [cce-4-1] eliminated 843 clauses out of 6870 (12%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 1279 large clauses in 39107785 steps
c [cce-4-1] allowing another 19553892 steps for small clauses
c [cce-4-1] scheduling 37406 clauses = 32016 binary + 5390 ternary
c [cce-4-1] tried to eliminate 37406 small clauses 100%
c [cce-4-1] eliminated 1787 binary clauses 6%
c [cce-4-1] eliminated 295 ternary clauses 5%
c [cce-4-1] eliminated 2082 small clauses 6%
c [cce-4-1] eliminated 2082 small clauses in 96803393 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 3361 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 16773401 steps for small clauses
c [cce-4-2] scheduling 35324 clauses = 30229 binary + 5095 ternary
c [cce-4-2] tried to eliminate 35324 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 3361 covered clauses in TOTAL during 2 rounds
c [bca-4] limit of 10000000 steps and 121468 added (scaled 2)
c [bca-4] 3476 out of 19396 literals actually usable 18%
c [bca-4] added 2 blocked clauses in 61521 steps
c [sweep-4] limit 1182846 penalty 0 = 0 + 0
c [sweep-4-1] 2455 pos 33.4% + 4888 neg 66.6% = 7343 sched 75.7% ret 2354
c [sweep-4-1] 1192343 steps 40 queries 525.42 avg class size
c [sweep-4-1] 1046 decisions 28 SAT calls 120.43 avg env size
c [sweep-4-1] 6878 variables remain 71% (2819 retained 29%)
c [decomp-22] removed 12 variables
c [sweep-4-1] removed 12 vars (0 failed, 12 eqs, 9 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 12 vars in TOTAL (1 rounds, 39 queries)
c [sort-queue-8] sorted 9685 enqueued variables after 62003 conflicts
c [score-dist-8] active 0 (0%), one 0 (0%), zero 9685 (100%)
c [score-dist-8] max exp 0, different 1 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 182 variables 1.8% (9685 remain 19%)
c [simplification-8] removed 4655 irredundant clauses 7.1% (60469 remain 29%)
c [simplification-8] maximum reduction of 7% = max (2%, 7%)
c [simplification-8] large reduction 7% >= 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 74003 (soft 64003 + delta 10000)
c [simplification-8] new conflict limit 64003 (hard 74003)
c 
c [simplification-9] limit 64003 conflicts (hard 74003) hit after 64003 conflicts
c [quatres-5] found 12723 quaternary clauses 31% in total
c [quatres-5-1] removed 15 duplicate quaternary clauses
c [quatres-5-1] added 1 double-self-subsuming ternary resolvents
c [quatres-5-2] added 21 single-self-subsuming ternary resolvents
c [quatres-5-2] added 82 quaternary resolvents
c [ternres-5] limit 4107164 with penalty 0 = 0 + 0
c [ternres-5] all 9685 free variables schedulable
c [ternres-5] 579 ternary resolvents (2 bin, 577 trn)
c [ternres-5] 40 variables remain 0% (9645 retained 100%)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] extracted 1415 xors of average arity 3.0
c [gauss-4] connected 4226 occurrences of 459 variables (average 9.2)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 2 variables
c [simpleprobe-4] 448 schedulable variables 5%
c [simpleprobe-4] limit 16428656 penalty 0 = 0 + 0
c [decomp-24] removed 331 variables
c [simpleprobe-4] 324 variables remain 3% (9028 retained 97%)
c [simpleprobe-4] removed 331 variables, found 3782 hbrs, 0 units
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 2299 transitive binary clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 2 clauses out of 1263 (0%) of length 8
c [cce-5-1] eliminated 15 clauses out of 2553 (1%) of length 7
c [cce-5-1] eliminated 23 clauses out of 3596 (1%) of length 6
c [cce-5-1] eliminated 49 clauses out of 4307 (1%) of length 5
c [cce-5-1] eliminated 51 clauses out of 5991 (1%) of length 4
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 140 large clauses in 30000182 steps
c [cce-5-1] allowing another 15000091 steps for small clauses
c [cce-5-1] scheduling 34493 clauses = 28735 binary + 5758 ternary
c [cce-5-1] tried to eliminate 7483 small clauses 22%
c [cce-5-1] eliminated 579 binary clauses 2%
c [cce-5-1] eliminated 97 ternary clauses 2%
c [cce-5-1] eliminated 676 small clauses 2%
c [cce-5-1] eliminated 676 small clauses in 30000008 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 816 covered clauses in round 1
c [cce-5] eliminated 816 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 9352 variables 100%
c [elim-7] limit of 41071640 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 516 variables 6% in round 1 in 12480618 steps
c [elim-7-1] backward subsumption/strengthening limit 12480600
c [elim-7-1-1] backward checking 3181 touched variables 34%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 3 and strengthened 26 clauses in 2043562 steps
c [elim-7-1] rescheduled 90 variables 1% by backward subsumption
c [elim-7-2] eliminated 6 variables 0% in round 2 in 81261 steps
c [elim-7-2] backward subsumption/strengthening limit 81200
c [elim-7-2-1] backward checking 12 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 2 and strengthened 4 clauses in 43743 steps
c [elim-7-2] rescheduled 10 variables 0% by backward subsumption
c [elim-7-3] eliminated 1 variables 0% in round 3 in 6450 steps
c [elim-7-3] backward subsumption/strengthening limit 6400
c [elim-7-3-1] backward checking 9 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 0 and strengthened 0 clauses in 6401 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 523 = 6% variables out of 9352 scheduled
c [bca-5] limit of 10000000 steps and 113303 added (scaled 2)
c [bca-5] 3091 out of 17660 literals actually usable 18%
c [bca-5] added 11 blocked clauses in 48785 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 12321490 penalty 0 = 0 + 0
c [sweep-5-1] 1993 pos 32.2% + 4195 neg 67.8% = 6188 sched 70.1% ret 2641
c [sweep-5-1] 11302196 steps 690 queries 46.38 avg class size
c [sweep-5-1] 14047 decisions 631 SAT calls 54.79 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-25] removed 65 variables
c [sweep-5-1] removed 65 vars (0 failed, 72 eqs, 89 impls)
c [sweep-5-2] 2802 pos 32.0% + 5962 neg 68.0% = 8764 sched 100.0% ret 0
c [sweep-5-2] 1022408 steps 29 queries 959.38 avg class size
c [sweep-5-2] 1319 decisions 29 SAT calls 162.00 avg env size
c [sweep-5-2] 8048 variables remain 92% (714 retained 8%)
c [decomp-26] removed 2 variables
c [sweep-5-2] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 67 vars in TOTAL (2 rounds, 717 queries)
c [sort-queue-9] sorted 8762 enqueued variables after 64003 conflicts
c [score-dist-9] active 0 (0%), one 0 (0%), zero 8762 (100%)
c [score-dist-9] max exp 0, different 1 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 923 variables 9.5% (8762 remain 17%)
c [simplification-9] removed 4162 irredundant clauses 6.9% (56307 remain 27%)
c [simplification-9] maximum reduction of 10% = max (10%, 7%)
c [simplification-9] large reduction 10% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 76003 (soft 66003 + delta 10000)
c [simplification-9] new conflict limit 66003 (hard 76003)
c 
c [simplification-10] limit 66003 conflicts (hard 76003) hit after 66003 conflicts
c [quatres-6] found 12373 quaternary clauses 32% in total
c [quatres-6-1] removed 36 duplicate quaternary clauses
c [quatres-6-2] added 32 single-self-subsuming ternary resolvents
c [quatres-6-2] added 328 quaternary resolvents
c [ternres-6] limit 4248204 with penalty 0 = 0 + 0
c [ternres-6] 39 schedulable variables 0%
c [ternres-6] 736 ternary resolvents (9 bin, 727 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 265512 penalty 3 = 3 + 0
c [card-4] found 147 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 265512 for elimination
c [card-4] 147 out of 147 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-27] removed 1 variables
c [treelook-4] limit 424820 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 16929 literals 97%
c [treelook-4] scheduling used 325905 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 424820 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 445270 steps
c [treelook-4] 16743 literals remain 96%
c [treelook-4] 7848 variables remain to probed next time 90%
c [decomp-28] removed 1 variables
c [treelook-4] removed 1 variables, found 87 hbrs
c [unhide-9] limit 424820 with penalty 1 = 1 + 0
c [unhide-9-9] 0 units, 2 failed, 134 tauts, 0 hbrs, 6847 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 1447 transitive binary clauses
c [transred-6] found 3 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 8751 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 23 blocked clauses
c [block-3] 23 < 1/100 * 56034 = 560 considered unsuccessful
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 6 clauses out of 294 (2%) of length 10
c [cce-6-1] eliminated 15 clauses out of 559 (3%) of length 9
c [cce-6-1] eliminated 15 clauses out of 927 (2%) of length 8
c [cce-6-1] eliminated 13 clauses out of 2811 (0%) of length 7
c [cce-6-1] eliminated 87 clauses out of 3648 (2%) of length 6
c [cce-6-1] eliminated 111 clauses out of 4258 (3%) of length 5
c [cce-6-1] eliminated 125 clauses out of 6133 (2%) of length 4
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 372 large clauses in 30000016 steps
c [cce-6-1] allowing another 15000008 steps for small clauses
c [cce-6-1] scheduling 31777 clauses = 26333 binary + 5444 ternary
c [cce-6-1] tried to eliminate 7930 small clauses 25%
c [cce-6-1] eliminated 74 binary clauses 0%
c [cce-6-1] eliminated 60 ternary clauses 1%
c [cce-6-1] eliminated 134 small clauses 0%
c [cce-6-1] eliminated 134 small clauses in 30000084 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 506 covered clauses in round 1
c [cce-6] eliminated 506 covered clauses in TOTAL during 1 rounds
c [cce-6] 506 < 1/100 * 55932 = 559 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 8750 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1699281920 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 110 variables 1% in round 1 in 11867373 steps
c [elim-8-1] backward subsumption/strengthening limit 11867300
c [elim-8-1-1] backward checking 891 touched variables 10%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 6 and strengthened 7 clauses in 1133944 steps
c [elim-8-1] rescheduled 51 variables 1% by backward subsumption
c [elim-8-2] eliminated 3 variables 0% in round 2 in 51427 steps
c [elim-8-2] backward subsumption/strengthening limit 51400
c [elim-8-2-1] backward checking 22 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 2 and strengthened 2 clauses in 27376 steps
c [elim-8-2] rescheduled 11 variables 0% by backward subsumption
c [elim-8-3] eliminated 1 variables 0% in round 3 in 8332 steps
c [elim-8-3] backward subsumption/strengthening limit 8300
c [elim-8-3-1] backward checking 11 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 0 and strengthened 0 clauses in 8301 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 114 = 1% variables out of 8750 scheduled
c [bca-6] limit of 10000000 steps and 110839 added (scaled 2)
c [bca-6] 2885 out of 17274 literals actually usable 17%
c [bca-6] added 4 blocked clauses in 48196 steps
c [sweep-6] limit 1274461 penalty 0 = 0 + 0
c [sweep-6-1] 2627 pos 33.1% + 5298 neg 66.9% = 7925 sched 91.8% ret 711
c [sweep-6-1] 1363105 steps 65 queries 461.12 avg class size
c [sweep-6-1] 1866 decisions 62 SAT calls 75.53 avg env size
c [sweep-6-1] 6353 variables remain 74% (2283 retained 26%)
c [decomp-29] removed 6 variables
c [sweep-6-1] removed 6 vars (0 failed, 2 eqs, 2 impls)
c [sweep-6] 6 < 1/1000 * 8636 = 8 considered unsuccessful
c [sweep-6] removed 6 vars in TOTAL (1 rounds, 64 queries)
c [sort-queue-10] sorted 8630 enqueued variables after 66003 conflicts
c [score-dist-10] active 0 (0%), one 0 (0%), zero 8630 (100%)
c [score-dist-10] max exp 0, different 1 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 132 variables 1.5% (8630 remain 17%)
c [simplification-10] removed 1158 irredundant clauses 2.1% (55149 remain 26%)
c [simplification-10] maximum reduction of 2% = max (2%, 2%)
c [simplification-10] geometric conflict interval increment 8000 = 24000 / 3
c [simplification-10] new conflict interval 32000
c [simplification-10] penalized conflict interval 32000 = 1 * 32000
c [simplification-10] hard conflict limit 114003 (soft 98003 + delta 16000)
c [simplification-10] new conflict limit 98003 (hard 114003)
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   36.6    8629    55149     73716   48908   8109 14131    8   230   13   4%    174   65    8    5  160%
c i   40.1    8617    55149     83890   58361   8568 14234    9   225   14   4%     89   50    9    6  157%
c i   43.7    8615    55149     93339   67225   8917 14326    9   226   15   4%     75   44    8    6  134%
c i   44.5    8613    55149     95238   68998   9001 14341    9   226   16   4%    -20   43   10    6  160%
c i   45.4    8612    55149     97165   70814   9061 14356    9   223   16   4%    -34   39   10    6  160%
c 
c [simplification-11] limit 98003 conflicts (hard 114003) hit after 101621 conflicts
c [quatres-7] found 13995 quaternary clauses 30% in total
c [quatres-7-1] removed 9 duplicate quaternary clauses
c [quatres-7-2] added 61 single-self-subsuming ternary resolvents
c [quatres-7-2] added 290 quaternary resolvents
c [ternres-7] limit 7150848 with penalty 0 = 0 + 0
c [ternres-7] all 8610 free variables schedulable
c [ternres-7] 990 ternary resolvents (10 bin, 980 trn)
c [ternres-7] 2 variables remain 0% (8608 retained 100%)
c [decomp-30] removed 36 variables
c [basicprobe-4] limit 35754241 penalty 0 = 0 + 0
c [basicprobe-4-0] 3852 sched 45%, 20 failed, 0 lifted, 2335 hbrs
c [decomp-31] removed 20 variables
c [basicprobe-4-1] 4598 sched 54%, 14 failed, 0 lifted, 913 hbrs
c [decomp-32] removed 15 variables
c [basicprobe-4-2] 4573 sched 53%, 4 failed, 0 lifted, 365 hbrs
c [decomp-33] removed 4 variables
c [basicprobe-4-3] 4566 sched 53%, 4 failed, 0 lifted, 192 hbrs
c [decomp-34] removed 5 variables
c [basicprobe-4-4] 3108 probes remain 36% after last round
c [basicprobe-4-4] 42 units = 42 failed (100%) + 0 lifted (0%)
c [basicprobe-4-4] removed 44 variables, found 3837 hbrs
c [bate-2] eliminated 21 asymmetric tautologies during probing
c [unhide-10] limit 1430169 with penalty 0 = 0 + 0
c [unhide-10-11] 0 units, 0 failed, 2063 tauts, 0 hbrs, 73394 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 888 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 8550 variables 100%
c [elim-9] limit of 143016964 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 185 variables 2% in round 1 in 11715865 steps
c [elim-9-1] backward subsumption/strengthening limit 11715800
c [elim-9-1-1] backward checking 1328 touched variables 16%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 3 and strengthened 14 clauses in 1400590 steps
c [elim-9-1] rescheduled 57 variables 1% by backward subsumption
c [elim-9-2] eliminated 4 variables 0% in round 2 in 111193 steps
c [elim-9-2] backward subsumption/strengthening limit 111100
c [elim-9-2-1] backward checking 33 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 2 clauses in 37238 steps
c [elim-9-2] rescheduled 8 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 5173 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 189 = 2% variables out of 8550 scheduled
c [bca-7] limit of 10000000 steps and 108529 added (scaled 2)
c [bca-7] 2044 out of 16724 literals actually usable 12%
c [bca-7] added 0 blocked clauses in 68960 steps
c [sort-queue-11] sorted 8361 enqueued variables after 101621 conflicts
c [score-dist-11] active 0 (0%), one 0 (0%), zero 8361 (100%)
c [score-dist-11] max exp 0, different 1 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 249 variables 2.9% (8361 remain 17%)
c [simplification-11] removed 1153 irredundant clauses 2.1% (53996 remain 26%)
c [simplification-11] maximum reduction of 3% = max (3%, 2%)
c [simplification-11] geometric conflict interval increment 8000 = 32000 / 4
c [simplification-11] new conflict interval 40000
c [simplification-11] penalized conflict interval 40000 = 1 * 40000
c [simplification-11] hard conflict limit 161621 (soft 141621 + delta 20000)
c [simplification-11] new conflict limit 141621 (hard 161621)
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.8    8360    53996    103407   66147   9564 14250   10   226   16   4%     27   38    9    7  141%
c i   51.9    8359    53996    106032   68599   9677 14272    9   223   17   4%    -21   33    9    7  138%
c i   51.9    8358    53996    106044   68608   9678 14273    9   223   17   4%    -22   33    9    7  135%
c i   52.5    8351    53996    107450   69929   9732 14286    9   221   17   4%    -35   31   10    7  148%
c i   52.5    8338    53996    107545   70021   9732 14286    9   220   17   4%    -36   30   10    7  149%
c -   56.9    8338    53996    117675   35966  10084 14342   10   218   11   4%     87   24   10    7  141%
c 
c [simplification-12] limit 141621 conflicts (hard 161621) hit after 141621 conflicts
c [quatres-8] found 15568 quaternary clauses 30% in total
c [quatres-8-1] removed 21 duplicate quaternary clauses
c [quatres-8-1] added 3 double-self-subsuming ternary resolvents
c [quatres-8-2] added 76 single-self-subsuming ternary resolvents
c [quatres-8-2] added 380 quaternary resolvents
c [ternres-8] limit 10563783 with penalty 0 = 0 + 0
c [ternres-8] 2 schedulable variables 0%
c [ternres-8] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-5] limit 528189 penalty 2 = 2 + 0
c [gauss-5] extracted 675 xors of average arity 3.0
c [gauss-5] connected 2002 occurrences of 398 variables (average 5.0)
c [gauss-5] limit 528189 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-35] removed 11 variables
c [simpleprobe-5] 272 schedulable variables 3%
c [simpleprobe-5] limit 42255133 penalty 0 = 0 + 0
c [decomp-36] removed 18 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 18 variables, found 3664 hbrs, 0 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1304 transitive binary clauses
c [cce-7] limit of 26409458 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 4 clauses out of 35 (11%) of length 12
c [cce-7-1] eliminated 18 clauses out of 321 (6%) of length 11
c [cce-7-1] eliminated 20 clauses out of 267 (7%) of length 10
c [cce-7-1] eliminated 23 clauses out of 537 (4%) of length 9
c [cce-7-1] eliminated 29 clauses out of 781 (4%) of length 8
c [cce-7-1] eliminated 32 clauses out of 2599 (1%) of length 7
c [cce-7-1] eliminated 93 clauses out of 3664 (3%) of length 6
c [cce-7-1] eliminated 106 clauses out of 4162 (3%) of length 5
c [cce-7-1] eliminated 58 clauses out of 6158 (1%) of length 4
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 383 large clauses in 26409462 steps
c [cce-7-1] allowing another 13204731 steps for small clauses
c [cce-7-1] scheduling 30174 clauses = 24930 binary + 5244 ternary
c [cce-7-1] tried to eliminate 7083 small clauses 23%
c [cce-7-1] eliminated 544 binary clauses 2%
c [cce-7-1] eliminated 78 ternary clauses 1%
c [cce-7-1] eliminated 622 small clauses 2%
c [cce-7-1] eliminated 622 small clauses in 26409460 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1005 covered clauses in round 1
c [cce-7] eliminated 1005 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 8309 variables 100%
c [elim-10] limit of 211275666 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 126 variables 2% in round 1 in 10982214 steps
c [elim-10-1] backward subsumption/strengthening limit 10982200
c [elim-10-1-1] backward checking 962 touched variables 12%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 1 and strengthened 7 clauses in 1117770 steps
c [elim-10-1] rescheduled 32 variables 0% by backward subsumption
c [elim-10-2] no variable eliminated in round 2 in 49816 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 126 = 2% variables out of 8309 scheduled
c [sweep-7] limit 1584567 penalty 1 = 1 + 0
c [sweep-7-1] 1931 pos 32.1% + 4081 neg 67.9% = 6012 sched 73.5% ret 2171
c [sweep-7-1] 1598273 steps 90 queries 259.10 avg class size
c [sweep-7-1] 2396 decisions 88 SAT calls 72.61 avg env size
c [sweep-7-1] 4315 variables remain 53% (3868 retained 47%)
c [decomp-37] removed 1 variables
c [sweep-7-1] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-7] 1 < 1/1000 * 8183 = 8 considered unsuccessful
c [sweep-7] removed 1 vars in TOTAL (1 rounds, 89 queries)
c [sort-queue-12] sorted 8182 enqueued variables after 141621 conflicts
c [score-dist-12] active 0 (0%), one 0 (0%), zero 8182 (100%)
c [score-dist-12] max exp 0, different 1 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 156 variables 1.9% (8182 remain 16%)
c [simplification-12] removed 1616 irredundant clauses 3.0% (52380 remain 25%)
c [simplification-12] maximum reduction of 3% = max (2%, 3%)
c [simplification-12] geometric conflict interval increment 10000 = 40000 / 4
c [simplification-12] new conflict interval 50000
c [simplification-12] penalized conflict interval 50000 = 1 * 50000
c [simplification-12] hard conflict limit 216621 (soft 191621 + delta 25000)
c [simplification-12] new conflict limit 191621 (hard 216621)
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   69.6    8181    52380    151444   63385  10777 16809   11   219   15   5%    464   16   12    8  138%
c i   79.8    8180    52380    176329   87282  11332 16906   11   222   21   5%    164   15   11    9  117%
c -   82.1    8180    52380    180820   50728  11425 16922   11   212   13   5%   -143    5   12    9  125%
c 
c [simplification-13] limit 191621 conflicts (hard 216621) hit after 191621 conflicts
c [quatres-9] found 17321 quaternary clauses 29% in total
c [quatres-9-1] removed 11 duplicate quaternary clauses
c [quatres-9-1] added 2 double-self-subsuming ternary resolvents
c [quatres-9-2] added 59 single-self-subsuming ternary resolvents
c [quatres-9-2] added 189 quaternary resolvents
c [decomp-38] removed 6 variables
c [treelook-5] limit 1505980 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 15818 literals 97%
c [treelook-5] scheduling used 364431 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 1505980 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1506258 steps
c [treelook-5] 15094 literals remain 92%
c [treelook-5] 7326 variables remain to probed next time 90%
c [decomp-39] removed 6 variables
c [treelook-5] removed 6 variables, found 1289 hbrs
c [unhide-11] limit 1505980 with penalty 1 = 1 + 0
c [unhide-11-13] 0 units, 1 failed, 2220 tauts, 0 hbrs, 41581 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 888 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 752990280 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 4 clauses out of 35 (11%) of length 12
c [cce-8-1] eliminated 11 clauses out of 307 (4%) of length 11
c [cce-8-1] eliminated 2 clauses out of 238 (1%) of length 10
c [cce-8-1] eliminated 4 clauses out of 542 (1%) of length 9
c [cce-8-1] eliminated 8 clauses out of 746 (1%) of length 8
c [cce-8-1] eliminated 13 clauses out of 2534 (1%) of length 7
c [cce-8-1] eliminated 15 clauses out of 3573 (0%) of length 6
c [cce-8-1] eliminated 32 clauses out of 4023 (1%) of length 5
c [cce-8-1] eliminated 221 clauses out of 6136 (4%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 310 large clauses in 25736617 steps
c [cce-8-1] allowing another 12868308 steps for small clauses
c [cce-8-1] scheduling 29021 clauses = 24032 binary + 4989 ternary
c [cce-8-1] tried to eliminate 29021 small clauses 100%
c [cce-8-1] eliminated 310 binary clauses 1%
c [cce-8-1] eliminated 142 ternary clauses 3%
c [cce-8-1] eliminated 452 small clauses 2%
c [cce-8-1] eliminated 463 small clauses in 57686601 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 773 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 12601563 steps for small clauses
c [cce-8-2] scheduling 28569 clauses = 23722 binary + 4847 ternary
c [cce-8-2] tried to eliminate 28569 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 773 covered clauses in TOTAL during 2 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 8166 variables 100%
c [elim-11] limit of 301196113 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 110 variables 1% in round 1 in 10670083 steps
c [elim-11-1] backward subsumption/strengthening limit 10670000
c [elim-11-1-1] backward checking 874 touched variables 11%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 0 and strengthened 5 clauses in 1024730 steps
c [elim-11-1] rescheduled 29 variables 0% by backward subsumption
c [elim-11-2] eliminated 3 variables 0% in round 2 in 104051 steps
c [elim-11-2] backward subsumption/strengthening limit 104000
c [elim-11-2-1] backward checking 20 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 4 clauses in 39161 steps
c [elim-11-2] rescheduled 10 variables 0% by backward subsumption
c [elim-11-3] eliminated 1 variables 0% in round 3 in 40508 steps
c [elim-11-3] backward subsumption/strengthening limit 40500
c [elim-11-3-1] backward checking 11 touched variables 0%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 0 and strengthened 0 clauses in 27353 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 114 = 1% variables out of 8166 scheduled
c [bca-8] limit of 10000000 steps and 103019 added (scaled 2)
c [bca-8] 1890 out of 16106 literals actually usable 12%
c [bca-8] added 7 blocked clauses in 61538 steps
c [sort-queue-13] sorted 8052 enqueued variables after 191621 conflicts
c [score-dist-13] active 0 (0%), one 0 (0%), zero 8052 (100%)
c [score-dist-13] max exp 0, different 1 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 128 variables 1.6% (8052 remain 16%)
c [simplification-13] removed 1139 irredundant clauses 2.2% (51241 remain 24%)
c [simplification-13] maximum reduction of 2% = max (2%, 2%)
c [simplification-13] geometric conflict interval increment 16666 = 50000 / 3
c [simplification-13] new conflict interval 66666
c [simplification-13] penalized conflict interval 66666 = 1 * 66666
c [simplification-13] hard conflict limit 291620 (soft 258287 + delta 33333)
c [simplification-13] new conflict limit 258287 (hard 291620)
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 -  102.3    8052    51241    235949   59653  12342 15329   12   238   13   5%    519   24   11   10  101%
c 
c [simplification-14] limit 258287 conflicts (hard 291620) hit after 258288 conflicts
c [quatres-10] found 18926 quaternary clauses 28% in total
c [quatres-10-1] removed 14 duplicate quaternary clauses
c [quatres-10-2] added 75 single-self-subsuming ternary resolvents
c [quatres-10-2] added 271 quaternary resolvents
c [ternres-9] limit 10187654 with penalty 1 = 1 + 0
c [ternres-9] all 8052 free variables schedulable
c [ternres-9] 5053 ternary resolvents (24 bin, 5029 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-40] removed 7 variables
c [basicprobe-5] limit 101876547 penalty 0 = 0 + 0
c [basicprobe-5-0] 2940 sched 37%, 12 failed, 0 lifted, 2019 hbrs
c [decomp-41] removed 30 variables
c [basicprobe-5-1] 4238 sched 53%, 7 failed, 0 lifted, 1159 hbrs
c [decomp-42] removed 7 variables
c [basicprobe-5-2] 4218 sched 53%, 1 failed, 0 lifted, 300 hbrs
c [decomp-43] removed 1 variables
c [basicprobe-5-3] 4211 sched 53%, 0 failed, 0 lifted, 128 hbrs
c [basicprobe-5-4] 4209 sched 53%, 0 failed, 0 lifted, 43 hbrs
c [basicprobe-5-5] 4208 sched 53%, 0 failed, 0 lifted, 28 hbrs
c [basicprobe-5-6] 4209 sched 53%, 0 failed, 0 lifted, 22 hbrs
c [basicprobe-5-7] 4209 sched 53%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-5-8] 4209 sched 53%, 0 failed, 0 lifted, 16 hbrs
c [basicprobe-5-8] round limit 8 hit
c [basicprobe-5-8] 20 units = 20 failed (100%) + 0 lifted (0%)
c [basicprobe-5-8] removed 38 variables, found 3729 hbrs
c [bate-3] eliminated 27 asymmetric tautologies during probing
c [unhide-12] limit 4075061 with penalty 0 = 0 + 0
c [unhide-12-16] 0 units, 0 failed, 3231 tauts, 0 hbrs, 103961 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 747 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 8007 variables 100%
c [block-4] limit of 25469136 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 22 blocked clauses
c [block-4] 22 < 1/100 * 50929 = 509 considered unsuccessful
c [cce-9] limit of 101876547 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 7 clauses out of 283 (2%) of length 11
c [cce-9-1] eliminated 3 clauses out of 218 (1%) of length 10
c [cce-9-1] eliminated 16 clauses out of 529 (3%) of length 9
c [cce-9-1] eliminated 21 clauses out of 747 (3%) of length 8
c [cce-9-1] eliminated 15 clauses out of 2454 (1%) of length 7
c [cce-9-1] eliminated 25 clauses out of 3489 (1%) of length 6
c [cce-9-1] eliminated 34 clauses out of 4038 (1%) of length 5
c [cce-9-1] eliminated 190 clauses out of 5974 (3%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 311 large clauses in 26253807 steps
c [cce-9-1] allowing another 13126903 steps for small clauses
c [cce-9-1] scheduling 28338 clauses = 23289 binary + 5049 ternary
c [cce-9-1] tried to eliminate 28338 small clauses 100%
c [cce-9-1] eliminated 1223 binary clauses 5%
c [cce-9-1] eliminated 239 ternary clauses 5%
c [cce-9-1] eliminated 1462 small clauses 5%
c [cce-9-1] eliminated 1462 small clauses in 60158017 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] completed small and large (ACCE)
c [cce-9-1] eliminated 1773 covered clauses in round 1
c [cce-9-2] eliminated 3 clauses out of 513 (1%) of length 9
c [cce-9-2] eliminated 1 clauses out of 726 (0%) of length 8
c [cce-9-2] eliminated 6 clauses out of 2439 (0%) of length 7
c [cce-9-2] eliminated 3 clauses out of 3464 (0%) of length 6
c [cce-9-2] eliminated 2 clauses out of 4004 (0%) of length 5
c [cce-9-2] eliminated 6 clauses out of 5784 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 21 large clauses in 24686001 steps
c [cce-9-2] allowing another 12343000 steps for small clauses
c [cce-9-2] scheduling 26876 clauses = 22066 binary + 4810 ternary
c [cce-9-2] tried to eliminate 17964 small clauses 67%
c [cce-9-2] eliminated 5 binary clauses 0%
c [cce-9-2] eliminated 5 ternary clauses 0%
c [cce-9-2] eliminated 10 small clauses 0%
c [cce-9-2] eliminated 10 small clauses in 41718534 steps
c [cce-9-2] incomplete small round (ACCE)
c [cce-9-2] eliminated 31 covered clauses in round 2
c [cce-9] eliminated 1804 covered clauses in TOTAL during 2 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 8004 variables 100%
c [elim-12] limit of 407506190 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 265 variables 3% in round 1 in 10183227 steps
c [elim-12-1] backward subsumption/strengthening limit 10183200
c [elim-12-1-1] backward checking 1779 touched variables 22%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 3 and strengthened 16 clauses in 1272240 steps
c [elim-12-1] rescheduled 64 variables 1% by backward subsumption
c [elim-12-2] eliminated 2 variables 0% in round 2 in 172216 steps
c [elim-12-2] backward subsumption/strengthening limit 172200
c [elim-12-2-1] backward checking 21 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 1 and strengthened 0 clauses in 33675 steps
c [elim-12-2] rescheduled 4 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 2360 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 267 = 3% variables out of 8004 scheduled
c [bca-9] limit of 10000000 steps and 97910 added (scaled 2)
c [bca-9] 1385 out of 15476 literals actually usable 9%
c [bca-9] added 0 blocked clauses in 71110 steps
c [sort-queue-14] sorted 7737 enqueued variables after 258288 conflicts
c [score-dist-14] active 0 (0%), one 0 (0%), zero 7737 (100%)
c [score-dist-14] max exp 0, different 1 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 315 variables 3.9% (7737 remain 15%)
c [simplification-14] removed 2556 irredundant clauses 5.0% (48685 remain 23%)
c [simplification-14] maximum reduction of 5% = max (4%, 5%)
c [simplification-14] large reduction 5% >= 5% limit
c [simplification-14] next conflict interval 2582 = min (258288/100, 66666)
c [simplification-14] penalized conflict interval 2582 = 1 * 2582
c [simplification-14] hard conflict limit 270870 (soft 260870 + delta 10000)
c [simplification-14] new conflict limit 260870 (hard 270870)
c 
c [simplification-15] limit 260870 conflicts (hard 270870) hit after 263774 conflicts
c [quatres-11] found 18349 quaternary clauses 28% in total
c [quatres-11-1] removed 24 duplicate quaternary clauses
c [quatres-11-2] added 94 single-self-subsuming ternary resolvents
c [quatres-11-2] added 370 quaternary resolvents
c [ternres-10] limit 20771889 with penalty 0 = 0 + 0
c [ternres-10] all 7737 free variables schedulable
c [ternres-10] 1699 ternary resolvents (18 bin, 1681 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 649121 penalty 4 = 4 + 0
c [card-5] found 258 at-most-one constraints of average size 3.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 649121 for elimination
c [card-5] 258 out of 258 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-49] removed 3 variables
c [simpleprobe-6] all 7734 free variables schedulable
c [simpleprobe-6] limit 83087557 penalty 0 = 0 + 0
c [decomp-50] removed 18 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 18 variables, found 7303 hbrs, 0 units
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 2583 transitive binary clauses
c [cce-10] limit of 103859447 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 31 (3%) of length 12
c [cce-10-1] eliminated 2 clauses out of 281 (1%) of length 11
c [cce-10-1] eliminated 6 clauses out of 221 (3%) of length 10
c [cce-10-1] eliminated 3 clauses out of 532 (1%) of length 9
c [cce-10-1] eliminated 7 clauses out of 799 (1%) of length 8
c [cce-10-1] eliminated 1 clauses out of 2395 (0%) of length 7
c [cce-10-1] eliminated 10 clauses out of 3443 (0%) of length 6
c [cce-10-1] eliminated 57 clauses out of 4008 (1%) of length 5
c [cce-10-1] eliminated 82 clauses out of 5994 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 169 large clauses in 23086572 steps
c [cce-10-1] allowing another 11543286 steps for small clauses
c [cce-10-1] scheduling 26157 clauses = 21469 binary + 4688 ternary
c [cce-10-1] tried to eliminate 26157 small clauses 100%
c [cce-10-1] eliminated 37 binary clauses 0%
c [cce-10-1] eliminated 26 ternary clauses 1%
c [cce-10-1] eliminated 63 small clauses 0%
c [cce-10-1] eliminated 63 small clauses in 49833803 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 232 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 11495617 steps for small clauses
c [cce-10-2] scheduling 26094 clauses = 21432 binary + 4662 ternary
c [cce-10-2] tried to eliminate 26094 small clauses 100%
c [cce-10-2] completed small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 232 covered clauses in TOTAL during 2 rounds
c [cce-10] 232 < 1/100 * 48647 = 486 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 7716 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 29 variables 0% in round 1 in 10063577 steps
c [elim-13-1] backward subsumption/strengthening limit 10063500
c [elim-13-1-1] backward checking 264 touched variables 3%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 1 clauses in 250942 steps
c [elim-13-1] rescheduled 6 variables 0% by backward subsumption
c [elim-13-2] eliminated 1 variables 0% in round 2 in 35764 steps
c [elim-13-2] backward subsumption/strengthening limit 35700
c [elim-13-2-1] backward checking 9 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 0 and strengthened 0 clauses in 23863 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 30 = 0% variables out of 7716 scheduled
c [elim-13] 30 < 1/100 * 7716 = 77 considered unsuccessful
c [sweep-8] limit 1557891 penalty 2 = 2 + 0
c [sweep-8-1] 1349 pos 33.7% + 2659 neg 66.3% = 4008 sched 52.1% ret 3678
c [sweep-8-1] 2074575 steps 68 queries 196.12 avg class size
c [sweep-8-1] 2244 decisions 67 SAT calls 91.25 avg env size
c [sweep-8-1] 2767 variables remain 36% (4919 retained 64%)
c [decomp-51] removed 1 variables
c [sweep-8-1] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-8] 1 < 1/1000 * 7686 = 7 considered unsuccessful
c [sweep-8] removed 1 vars in TOTAL (1 rounds, 67 queries)
c [sort-queue-15] sorted 7685 enqueued variables after 263774 conflicts
c [score-dist-15] active 0 (0%), one 0 (0%), zero 7685 (100%)
c [score-dist-15] max exp 0, different 1 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 52 variables 0.7% (7685 remain 15%)
c [simplification-15] removed 305 irredundant clauses 0.6% (48380 remain 23%)
c [simplification-15] maximum reduction of 1% = max (1%, 1%)
c [simplification-15] geometric conflict interval increment 33333 = 66666 / 2
c [simplification-15] new conflict interval 99999
c [simplification-15] penalized conflict interval 99999 = 1 * 99999
c [simplification-15] hard conflict limit 413772 (soft 363773 + delta 49999)
c [simplification-15] new conflict limit 363773 (hard 413772)
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.6    7684    48380    292335   99574  17679 20452   12   199   23   6%    810  -15   12   11  109%
c -  129.3    7684    48380    297419   62337  17745 20462   12   196   14   6%   -865  -16   14   11  121%
c -  144.7    7684    48380    348784   70937  18493 20559   13   241   15   5%    156   25   14   12  116%
c 
c [simplification-16] limit 363773 conflicts (hard 413772) hit after 388077 conflicts
c [quatres-12] found 21128 quaternary clauses 26% in total
c [quatres-12-1] removed 7 duplicate quaternary clauses
c [quatres-12-1] added 1 double-self-subsuming ternary resolvents
c [quatres-12-2] added 80 single-self-subsuming ternary resolvents
c [quatres-12-2] added 218 quaternary resolvents
c [ternres-11] limit 31356254 with penalty 0 = 0 + 0
c [ternres-11] all 7684 free variables schedulable
c [ternres-11] 2440 ternary resolvents (27 bin, 2413 trn)
c [ternres-11] fully completed ternary resolution
c [gauss-6] limit 783906 penalty 3 = 3 + 0
c [gauss-6] extracted 581 xors of average arity 3.0
c [gauss-6] connected 1724 occurrences of 292 variables (average 5.9)
c [gauss-6] limit 783906 penalty 3 = 3 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-52] removed 9 variables
c [treelook-6] limit 3135625 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 14872 literals 97%
c [treelook-6] scheduling used 495634 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3135625 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 3149805 steps
c [treelook-6] 13975 literals remain 91%
c [treelook-6] 6852 variables remain to probed next time 89%
c [decomp-53] removed 2 variables
c [treelook-6] removed 5 variables, found 2211 hbrs
c [unhide-13] limit 3135625 with penalty 1 = 1 + 0
c [unhide-13-18] 1 units, 0 failed, 3760 tauts, 0 hbrs, 202523 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 1348 transitive binary clauses
c [bca-10] limit of 10000000 steps and 97158 added (scaled 2)
c [bca-10] 1019 out of 15340 literals actually usable 7%
c [bca-10] added 0 blocked clauses in 110738 steps
c [sort-queue-16] sorted 7669 enqueued variables after 388077 conflicts
c [score-dist-16] active 0 (0%), one 0 (0%), zero 7669 (100%)
c [score-dist-16] max exp 0, different 1 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 15 variables 0.2% (7669 remain 15%)
c [simplification-16] removed 71 irredundant clauses 0.1% (48309 remain 23%)
c [simplification-16] maximum reduction of 0% = max (0%, 0%)
c [simplification-16] full geometric conflict interval increment 99999
c [simplification-16] new conflict interval 199998
c [simplification-16] penalized conflict interval 199998 = 1 * 199998
c [simplification-16] hard conflict limit 688074 (soft 588075 + delta 99999)
c [simplification-16] new conflict limit 588075 (hard 688074)
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 -  161.8    7669    48309    397813   75668  21002 18684   12   151   15   8%    613  -55    9   13   75%
c -  177.1    7669    48309    448324   82294  21554 18762   14   202   16   7%    834    9   13   13  100%
c -  193.2    7669    48309    498005   87705  21958 18817   14   221   17   6%    935   19   14   14  101%
c -  209.4    7669    48309    548175   93370  22349 18874   15   224   18   7%    983   26   13   14   88%
c 
c [simplification-17] limit 588075 conflicts (hard 688074) hit after 589911 conflicts
c [quatres-13] found 24484 quaternary clauses 24% in total
c [quatres-13-1] removed 14 duplicate quaternary clauses
c [quatres-13-1] added 1 double-self-subsuming ternary resolvents
c [quatres-13-2] added 156 single-self-subsuming ternary resolvents
c [quatres-13-2] added 231 quaternary resolvents
c [ternres-12] limit 50492558 with penalty 0 = 0 + 0
c [ternres-12] all 7669 free variables schedulable
c [ternres-12] 5285 ternary resolvents (46 bin, 5239 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-54] removed 8 variables
c [basicprobe-6] limit 252462792 penalty 0 = 0 + 0
c [basicprobe-6-0] 3993 sched 52%, 12 failed, 0 lifted, 2569 hbrs
c [decomp-55] removed 13 variables
c [basicprobe-6-1] 3951 sched 52%, 4 failed, 0 lifted, 453 hbrs
c [decomp-56] removed 4 variables
c [basicprobe-6-2] 3939 sched 52%, 0 failed, 0 lifted, 199 hbrs
c [decomp-57] removed 1 variables
c [basicprobe-6-3] 3935 sched 51%, 0 failed, 0 lifted, 84 hbrs
c [basicprobe-6-4] 3935 sched 51%, 0 failed, 0 lifted, 68 hbrs
c [basicprobe-6-5] 3935 sched 51%, 0 failed, 0 lifted, 39 hbrs
c [basicprobe-6-6] 3935 sched 51%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-6-7] 3935 sched 51%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-6-8] 3935 sched 51%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-6-8] round limit 8 hit
c [basicprobe-6-8] 16 units = 16 failed (100%) + 0 lifted (0%)
c [basicprobe-6-8] removed 18 variables, found 3449 hbrs
c [bate-4] eliminated 8 asymmetric tautologies during probing
c [unhide-14] limit 10098511 with penalty 0 = 0 + 0
c [unhide-14-23] 0 units, 0 failed, 5758 tauts, 0 hbrs, 355636 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 734 transitive binary clauses
c [cce-11] limit of 126231396 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 13 clauses out of 255 (5%) of length 11
c [cce-11-1] eliminated 16 clauses out of 207 (8%) of length 10
c [cce-11-1] eliminated 13 clauses out of 534 (2%) of length 9
c [cce-11-1] eliminated 4 clauses out of 760 (1%) of length 8
c [cce-11-1] eliminated 26 clauses out of 2086 (1%) of length 7
c [cce-11-1] eliminated 20 clauses out of 3533 (1%) of length 6
c [cce-11-1] eliminated 31 clauses out of 3958 (1%) of length 5
c [cce-11-1] eliminated 58 clauses out of 5956 (1%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 181 large clauses in 23806096 steps
c [cce-11-1] allowing another 11903048 steps for small clauses
c [cce-11-1] scheduling 26086 clauses = 21398 binary + 4688 ternary
c [cce-11-1] tried to eliminate 26086 small clauses 100%
c [cce-11-1] eliminated 334 binary clauses 2%
c [cce-11-1] eliminated 57 ternary clauses 1%
c [cce-11-1] eliminated 391 small clauses 1%
c [cce-11-1] eliminated 391 small clauses in 51657054 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 572 covered clauses in round 1
c [cce-11-2] eliminated 2 clauses out of 2060 (0%) of length 7
c [cce-11-2] eliminated 1 clauses out of 3513 (0%) of length 6
c [cce-11-2] eliminated 3 clauses out of 3927 (0%) of length 5
c [cce-11-2] eliminated 2 clauses out of 5898 (0%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 8 large clauses in 23269619 steps
c [cce-11-2] allowing another 11634809 steps for small clauses
c [cce-11-2] scheduling 25695 clauses = 21064 binary + 4631 ternary
c [cce-11-2] tried to eliminate 25695 small clauses 100%
c [cce-11-2] eliminated 4 binary clauses 0%
c [cce-11-2] eliminated 4 small clauses 0%
c [cce-11-2] eliminated 4 small clauses in 50248498 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 12 covered clauses in round 2
c [cce-11-3] eliminated 3 clauses out of 3512 (0%) of length 6
c [cce-11-3] eliminated 6 clauses out of 5896 (0%) of length 4
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] eliminated 9 large clauses in 23269953 steps
c [cce-11-3] allowing another 11634976 steps for small clauses
c [cce-11-3] scheduling 25691 clauses = 21060 binary + 4631 ternary
c [cce-11-3] tried to eliminate 8867 small clauses 35%
c [cce-11-3] eliminated 1 binary clauses 0%
c [cce-11-3] eliminated 1 small clauses 0%
c [cce-11-3] eliminated 1 small clauses in 24325847 steps
c [cce-11-3] incomplete small round (ACCE)
c [cce-11-3] eliminated 10 covered clauses in round 3
c [cce-11] eliminated 594 covered clauses in TOTAL during 3 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 7643 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 150 variables 2% in round 1 in 9789760 steps
c [elim-14-1] backward subsumption/strengthening limit 9789700
c [elim-14-1-1] backward checking 1074 touched variables 14%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 5 and strengthened 15 clauses in 1013690 steps
c [elim-14-1] rescheduled 61 variables 1% by backward subsumption
c [elim-14-2] eliminated 4 variables 0% in round 2 in 158768 steps
c [elim-14-2] backward subsumption/strengthening limit 158700
c [elim-14-2-1] backward checking 28 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 0 and strengthened 0 clauses in 41426 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 154 = 2% variables out of 7643 scheduled
c [sort-queue-17] sorted 7489 enqueued variables after 589911 conflicts
c [score-dist-17] active 0 (0%), one 0 (0%), zero 7489 (100%)
c [score-dist-17] max exp 0, different 1 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 180 variables 2.3% (7489 remain 15%)
c [simplification-17] removed 1011 irredundant clauses 2.1% (47298 remain 23%)
c [simplification-17] maximum reduction of 2% = max (2%, 2%)
c [simplification-17] geometric conflict interval increment 66666 = 199998 / 3
c [simplification-17] new conflict interval 266664
c [simplification-17] penalized conflict interval 266664 = 1 * 266664
c [simplification-17] hard conflict limit 989907 (soft 856575 + delta 133332)
c [simplification-17] new conflict limit 856575 (hard 989907)
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 -  242.2    7489    47298    616079   94146  25477 17710   15   191   17   8%   1009   -4   17   15  116%
c -  259.4    7489    47298    667633   99821  25860 17751   16   207   18   8%   1017   15   15   15  100%
c -  277.1    7489    47298    718376  104099  26210 17783   17   195   19   9%   1021    2   18   16  117%
c -  295.1    7489    47298    770045  108978  26552 17813   15   175   19   9%   1023   -9   16   16  103%
c -  313.6    7489    47298    821728  113301  26864 17857   16   191   20   8%   1023   11   17   16  102%
c 
c [simplification-18] limit 856575 conflicts (hard 989907) hit after 856575 conflicts
c [quatres-14] found 27111 quaternary clauses 23% in total
c [quatres-14-1] removed 29 duplicate quaternary clauses
c [quatres-14-2] added 158 single-self-subsuming ternary resolvents
c [quatres-14-2] added 384 quaternary resolvents
c [ternres-13] limit 79027493 with penalty 0 = 0 + 0
c [ternres-13] all 7489 free variables schedulable
c [ternres-13] 6625 ternary resolvents (41 bin, 6584 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-63] removed 6 variables
c [simpleprobe-7] all 7483 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-64] removed 6 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 6 variables, found 10556 hbrs, 0 units
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 2572 transitive binary clauses
c [cce-12] limit of 395137468 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 5 clauses out of 192 (3%) of length 10
c [cce-12-1] eliminated 5 clauses out of 525 (1%) of length 9
c [cce-12-1] eliminated 2 clauses out of 769 (0%) of length 8
c [cce-12-1] eliminated 6 clauses out of 2072 (0%) of length 7
c [cce-12-1] eliminated 6 clauses out of 3533 (0%) of length 6
c [cce-12-1] eliminated 17 clauses out of 3964 (0%) of length 5
c [cce-12-1] eliminated 39 clauses out of 6019 (1%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 80 large clauses in 21951198 steps
c [cce-12-1] allowing another 10975599 steps for small clauses
c [cce-12-1] scheduling 25181 clauses = 20581 binary + 4600 ternary
c [cce-12-1] tried to eliminate 25181 small clauses 100%
c [cce-12-1] eliminated 20 binary clauses 0%
c [cce-12-1] eliminated 12 ternary clauses 0%
c [cce-12-1] eliminated 32 small clauses 0%
c [cce-12-1] eliminated 32 small clauses in 46130790 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 112 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 10959398 steps for small clauses
c [cce-12-2] scheduling 25149 clauses = 20561 binary + 4588 ternary
c [cce-12-2] tried to eliminate 25149 small clauses 100%
c [cce-12-2] completed small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 112 covered clauses in TOTAL during 2 rounds
c [cce-12] 112 < 1/100 * 47283 = 472 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 7477 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 6 variables 0% in round 1 in 9685407 steps
c [elim-15-1] backward subsumption/strengthening limit 9685400
c [elim-15-1-1] backward checking 76 touched variables 1%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 1 and strengthened 2 clauses in 501633 steps
c [elim-15-1] rescheduled 10 variables 0% by backward subsumption
c [elim-15-2] eliminated 1 variables 0% in round 2 in 12870 steps
c [elim-15-2] backward subsumption/strengthening limit 12800
c [elim-15-2-1] backward checking 7 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 0 and strengthened 0 clauses in 12801 steps
c [elim-15-2] fully rescheduled 7470 variables 100%
c [elim-15-3] no variable eliminated in round 3 in 9682617 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 7 = 0% variables out of 7477 scheduled
c [elim-15] 7 < 1/100 * 7477 = 74 considered unsuccessful
c [sort-queue-18] sorted 7470 enqueued variables after 856575 conflicts
c [score-dist-18] active 0 (0%), one 0 (0%), zero 7470 (100%)
c [score-dist-18] max exp 0, different 1 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 19 variables 0.3% (7470 remain 15%)
c [simplification-18] removed 138 irredundant clauses 0.3% (47160 remain 22%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] full geometric conflict interval increment 266664
c [simplification-18] new conflict interval 533328
c [simplification-18] penalized conflict interval 533328 = 1 * 533328
c [simplification-18] hard conflict limit 1656567 (soft 1389903 + delta 266664)
c [simplification-18] new conflict limit 1389903 (hard 1656567)
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 -  337.7    7470    47160    876836  117696  33657 25809   17   205   20   8%   1024    8   19   17  115%
c -  356.5    7470    47160    929311  121932  33942 25842   17   189   21   9%   1024   -2   18   17  106%
c -  376.6    7470    47160    982100  126003  34210 25875   15   148   21  10%   1024  -40   15   17   87%
c -  398.0    7470    47160   1035431  130457  34526 25910   15   133   22  11%   1024  -47   18   17  110%
c -  420.2    7470    47160   1088644  133483  34780 25940   18   199   22   9%   1024   12   17   17  101%
c -  443.3    7470    47160   1143396  137467  35014 25977   18   220   22   8%   1024   34   20   17  117%
c -  465.8    7470    47160   1198423  141302  35286 26000   18   169   23  11%   1024   -8   19   18  107%
c -  487.7    7470    47160   1253707  145331  35514 26027   19   184   23  10%   1024    2   20   18  111%
c -  511.0    7470    47160   1308960  149102  35710 26052   16   137   23  12%   1024  -46   18   18  101%
c -  536.8    7470    47160   1365193  152590  35942 26085   17   158   24  11%   1024  -24   18   17  105%
c 
c [simplification-19] limit 1389903 conflicts (hard 1656567) hit after 1390934 conflicts
c [quatres-15] found 31752 quaternary clauses 21% in total
c [quatres-15-1] removed 1 duplicate quaternary clauses
c [quatres-15-1] added 1 double-self-subsuming ternary resolvents
c [quatres-15-2] added 137 single-self-subsuming ternary resolvents
c [quatres-15-2] added 208 quaternary resolvents
c [ternres-14] limit 148924581 with penalty 0 = 0 + 0
c [ternres-14] all 7470 free variables schedulable
c [ternres-14] 6034 ternary resolvents (31 bin, 6003 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-65] removed 3 variables
c [treelook-7] limit 14892458 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 14488 literals 97%
c [treelook-7] scheduling used 712365 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 14892458 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 14894883 steps
c [treelook-7] 10095 literals remain 68%
c [treelook-7] 6480 variables remain to probed next time 87%
c [decomp-66] removed 8 variables
c [treelook-7] removed 10 variables, found 10744 hbrs
c [unhide-15] limit 10000000 with penalty 1 = 1 + 0
c [unhide-15-27] 0 units, 0 failed, 12155 tauts, 0 hbrs, 312814 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 1212 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 7457 variables 100%
c [block-5] limit of 50000000 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 5 blocked clauses
c [block-5] 5 < 1/100 * 47126 = 471 considered unsuccessful
c [bca-11] limit of 10000000 steps and 94782 added (scaled 2)
c [bca-11] 577 out of 14916 literals actually usable 4%
c [bca-11] added 0 blocked clauses in 177690 steps
c [sweep-9] limit 5584671 penalty 3 = 3 + 0
c [sweep-9-1] 837 pos 31.4% + 1831 neg 68.6% = 2668 sched 35.8% ret 4789
c [sweep-9-1] 5773697 steps 55 queries 134.78 avg class size
c [sweep-9-1] 2849 decisions 54 SAT calls 212.57 avg env size
c [sweep-9-1] 1586 variables remain 21% (5871 retained 79%)
c [decomp-67] removed 1 variables
c [sweep-9-1] removed 1 vars (0 failed, 0 eqs, 2 impls)
c [sweep-9] 1 < 1/1000 * 7457 = 7 considered unsuccessful
c [sweep-9] removed 1 vars in TOTAL (1 rounds, 54 queries)
c [sort-queue-19] sorted 7456 enqueued variables after 1390934 conflicts
c [score-dist-19] active 0 (0%), one 0 (0%), zero 7456 (100%)
c [score-dist-19] max exp 0, different 1 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 14 variables 0.2% (7456 remain 15%)
c [simplification-19] removed 41 irredundant clauses 0.1% (47119 remain 22%)
c [simplification-19] maximum reduction of 0% = max (0%, 0%)
c [simplification-19] full geometric conflict interval increment 533328
c [simplification-19] conflict interval soft limit 1000000 reached
c [simplification-19] new conflict interval 1000000
c [simplification-19] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-19] hard conflict limit 2890934 (soft 2390934 + delta 500000)
c [simplification-19] new conflict limit 2390934 (hard 2890934)
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 -  567.5    7456    47119   1422022  154625  40087 26452   18   180   23  10%   1024    5   20   17  114%
c -  593.5    7456    47119   1479933  157761  40297 26467   18   163   24  11%   1024  -17   20   18  114%
c i  608.7    7455    47119   1515592  192943  40437 26480   18   162   41  11%   1024  -16   21   18  116%
c -  620.1    7455    47119   1538777  161645  40517 26492   19   156   25  12% -12607  -19   21   18  114%
c i  621.9    7454    47119   1543380  166136  40529 26496   17   131   32  13% -11683  -43   15   18   82%
c -  648.6    7449    47119   1597998  165461  40713 26520   18   181   25  10%  -4689    7   19   18  106%
c -  676.2    7449    47119   1657279  168730  40904 26544   18   208   25   9%  -1288   36   16   18   88%
c -  703.8    7449    47119   1717080  171981  41056 26560   19   158   26  12%     96   -8   19   19  102%
c -  732.3    7449    47119   1777829  175628  41220 26579   20   173   26  11%    657    0   20   19  105%
c -  762.4    7449    47119   1838690  178621  41382 26593   19   140   27  14%    879  -33   17   19   86%
c -  791.9    7449    47119   1900703  181999  41562 26609   20   165   26  12%    968  -15   21   19  110%
c i  798.7    7448    47119   1915451  196597  41608 26614   20   161   38  13%    979  -18   22   20  114%
c -  822.7    7440    47119   1963378  185612  41751 26622   20   195   28  10%  -1840   21   21   19  106%
c -  854.5    7440    47119   2026314  189266  41934 26642   18   141   29  13%    -72  -34   19   19  100%
c i  878.1    7439    47119   2075321  237725  42051 26658   19   156   60  12%    505   -7   20   19  109%
c -  886.1    7439    47119   2089557  192653  42088 26661   20   155   29  13%  -1436  -11   22   19  117%
c -  918.0    7439    47119   2152928  194932  42257 26673   21   211   29  10%     89   36   22   19  112%
c -  951.8    7439    47119   2218029  198880  42418 26700   19   148   29  13%    678  -11   22   19  117%
c -  987.2    7439    47119   2282929  201617  42597 26725   19   164   30  11%    895   -4   17   20   88%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 193 basic ate = 66 trn 34% + 127 lrg 66% in 4 updates
c bcas: 11 count, 81 added (74 skipped), 758328 steps
c bkwd: tried 116616 clauses, 233097 lits, 2.00 lits/clause
c bkwd: checked 29623222 occs, 254.02 occs/clause, 127.09 occs/lit
c bkwd: subsumed 1 binary, 10 ternary, 23 large
c bkwd: strengthened 0 binary, 4 ternary (100% self), 269 large (0% self)
c blkd: 5 bces, 180 removed, 1333684 resolutions, 3521885 steps
c blkd: 2316 blocking literals 2%, 6 pure
c bump: 0 bumped seen, 0 lits 0.0 on average
c card: 5 count, 10 units, 4 am1, 23845440 steps
c card: 106 rescheduled, 904 eliminated, 10500 resolved, 9567 subsumed
c card: 3788 at-most-one constraints found, average size 3.00
c card: 3788 at-most-one constraints used 100%, average size 3.00
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 12 cces, 12841 eliminated, 9970 ate 78%, 2871 abce 22%
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: 764685 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 124 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 67 decompositions, 15398 equivalent 29%
c deco: 324 decision-only clauses 0%, 61% reduction
c decs: 35952301 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 21165 eliminated 40%, 154 pure 1%
c elms: 39 rounds, 2.6 rounds/bve
c elms: 18745 small 89%, 2260 large 11%
c elms: 24953 tried small, 18745 succeeded 75%, 6208 failed 25%
c elms: 6559 subsumed, 19628 strengthened, 282 blocked
c elms: 3897471 copies, 4925310 resolutions, 512355 ipos
c elms: 2643051 subchks, 3366277 strchks
c gaus: 6 extractions, 12891 extracted, 2.9 size, 3 max
c gaus: exported 0 units, 4 binary and 3 ternary equations
c gaus: 0 gc, 16625124 steps, 8312562 extr 50%, 409860 elim 2%
c glue: 16.4 orig avg, 16.4 real avg, 3.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 102120 = 62593 simple 61% + 33541 trn 33% + 5986 lrg 6%, 2480 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2305127 clauses, 55.4 length
c lrnd: 127728884 lits = 182434549 orig - 54705665 removed 30%
c lrnd: 1149564 uips 50%, 397193 flips 17%
c mins: 2252055 mins 98%, 2099 bin 0%, 50630 size 2%
c mins: 238492382 poisoned searches, 46840030 hits, 20% hit rate
c mins: 371344322 used twice searches, 18650273 hits, 5% hit rate
c move: moved 8494, 6957 bin 82%, 1537 trn 18%
c otfs: 5746 driving 21%, 21246 restarting 79%
c otfs: str 26992, 26295 red 97%, 697 irr 3%
c otfs: str 26992, 0 bin 0%, 346 trn 1%, 26646 lrg 99%
c otfs: sub 52, 52 red 100%, 0 irr 0%
c otfs: sub 52, 0 bin 0%, 24 trn 46%, 28 lrg 54%
c phas: 1 computed, 11561 set, 0 pos (0%), 11561 neg (100%)
c prbs: 6 basic, 208172 probed, 174 failed, 1 lifted
c prbs: 7 simple, 159110 probed, 760 failed, 13352 eqs
c prbs: 7 treelook, 6554 probed, 3 failed, 0 lifted
c prom: 701507 locked 9% out of 7612976 tried
c prps: 1138762670 props, 31 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 15 count, 4280 quat, 1097 self1, 12 self2, 295 dup
c queu: 19 sorted, 35952301 next (0 steps 0.00)
c queu: 223934 enq (223914 steps 1.00), 0 deq 0%
c redc: 100488 clauses 26%, 388518 tried 17%, 127 sat 0%
c redc: 184263 lits 4%, 4210863 tried 2%, 127 sat 0%
c redc: 5727 times jump level reduced, 34.6 levels on average
c reds: 39 count, 59198.1 conflicts per reduce
c reds: 0 memlim 0%, 39 arith 100%
c reds: 1327885 collected 68%, 628413 retired 32%
c rmbd: 10235 removed, 9325 red 91%
c rsts: 33207 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: 19 count, 17 confs 89%, 0 vars 0%
c simp: 0 its 0%, 1 bin 5%, 1 trns 5%
c subl: 2305127 count (2992061 tried 1.3), 19542 sub out of 2282029 (0.9%)
c swps: 9 count, 10 rounds, 1209 queries (120.9/round)
c swps: 1119 sat calls, 22 unsat (1.9% success rate)
c swps: 29818 decisions 26.6, 2146 conflicts 1.9
c swps; 222.0 avg class size, 73.3 avg environment size
c swps: 0 failed, 137 impls, 110 equivs
c swp0: 400 type 0 queries, 85 unsat (21.2%), 380 sat (95.0%)
c swp1: 809 type 1 queries, 315 unsat (38.9%), 719 sat (88.9%)
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: 71905045 calls to obtain time
c tops: 8442 fixed 16%, 43 its, 53691.33 confs/it
c trds: 15 transitive reductions, 18300 removed, 9 failed
c trds: 201139 nodes, 468719 edges, 27673580 steps
c trim: 179102 words, 0.7 MB
c trnr: 14 count, 461 bin, 33874 trn, 267758203 steps
c unhd: 15 count, 27 rounds, 42716101 steps
c unhd: 115 non-trivial sccs of average size 2.1
c unhd: 38 units, 38 bin, 0 trn, 0 lrg
c unhd: 70 failed, 69 stamp, 0 lits, 0 bin, 1 trn, 0 lrg
c unhd: 34105 tauts, 289 bin 1%, 7339 trn 22%, 3483 lrg 10%
c unhd: 34105 tauts, 22994 stamp 67%, 32819 red 96%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1160084 str, 38 bin 0%, 2600 trn 0%, 1157446 lrg 100%, 1148085 red 99%
c vars: 7439 remaining 14% and 45005 removed 86% out of 52444
c vars: 8442 fixed 16%, 21165 eliminated 40%, 15398 equivalent 29%
c vsts: 29729980591 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 26.3 search visits per propagation, 12767.5 per conflict
c wchs: 10499449705 pushed, 37889155 enlarged, 380 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2286309       1327885        628413     296039200      36851063       1433848
c 
c  0 0        222044  10     18414   1         0   0 223734703  76< 24021745  65    771550  54     6.0
c  1 5        114443   5     71563   5     28707   5  28004845   9   4053221  11<   149826  10<    0.5
c  2 6        342285  15    221760  17     92234  15  32109032  11   5418912  15    252726  18     1.6
c  3 9        497818  22<   324822  24    143099  23   9722638   3   2163047   6    149492  10     3.2
c  4 14       470127  21    306139  23<   141211  22<  1355983   0    608806   2     58731   4     4.0
c  5 21       334503  15    210336  16    107492  17    615662   0    334367   1     30490   2     4.3
c  6 30       183144   8    109078   8     65061  10    307241   0    160468   0     13666   1     3.8
c  7 41        82483   4     46316   3     32402   5    131086   0     64636   0      5318   0     2.6
c  8 54        28921   1     14943   1     12781   2     43144   0     19822   0      1547   0     1.2
c  9 69         8180   0      3693   0      4087   1     11737   0      4920   0       420   0     0.4
c 10 86         1983   0       782   0      1102   0      2670   0      1004   0        81   0     0.1
c 11 126         219   0        32   0       133   0       266   0        75   0         1   0     0.0
c 12 230         159   0         7   0       104   0       193   0        40   0         0   0     0.0
c 
c avg                  3.4           3.7           4.0           0.4           0.7           1.1
c std                  1.9           1.6           1.7           0.9           1.2           1.5
c 
c   21.907   2% decide
c   15.458   2% cce
c   13.864   1% probe
c    7.138   1% unhide
c 
c   13.583 < 1% rest (below)
c 
c    5.032   1% elim
c    2.115   0% ternres
c    1.703   0% transred
c    1.614   0% sweep
c    1.528   0% quatres
c    0.558   0% gauss
c    0.450   0% bca
c    0.430   0% block
c    0.152   0% card
c    0.000   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.542   0% preprocessing     3%
c   50.353   5% inprocessing     97%
c ==================================
c   51.895   5% simplifying
c  948.006  95% search
c ==================================
c  999.905 100% all
c 
c       2308727 conflicts,        2308.9 confs/sec
c         19285 ternaries,         119.7 confs/ternary
c          3512 binaries,          657.4 confs/binary
c            43 iterations,      53691.3 confs/iteration
c 
c            39 reductions,          0.0 redus/sec,  59198.1 confs/reduction
c         33207 restarts,           33.2 rests/sec,     69.5 confs/restart
c      35952301 decisions,       35955.7 decis/sec,     15.6 decis/conflict
c    1138762670 propagations,  1138870.7 props/sec,     31.7 props/decision
c 
c 999.9 seconds, 93.5 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
