c launch: /data/cnf/sc2014/app/bob12s09-opt.cnf.bz2
c host: atom31
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 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 fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/bob12s09-opt.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/bob12s09-opt.cnf.bz2
c no embedded options
c found 'p cnf 51108 152338' header
c read 51108 variables, 152338 clauses, 355454 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 --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 51107 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 
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   51107   152337         0       0      0     0    0     0    9   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 86 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] 86 out of 86 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 77 at-most-one constraints, 77 used 100%
c [card-1] exported 77 binary clauses, 1.0 per/constraint
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 51107 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 1953 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 1953 variables, found 4381 hbrs, 80 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 78 units, 141 failed, 621 tauts, 0 hbrs, 79 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 49060 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 36701 variables 75% in round 1 in 10634745 steps
c [elim-1-1] backward subsumption/strengthening limit 9365255
c [elim-1-1-1] backward checking 36008 touched variables 73%
c [elim-1-1-1] incomplete backward checking 35861 remain 100%
c [elim-1-1] subsumed 35 and strengthened 72 clauses in 9366101 steps
c [elim-1] incomplete 271 not tried 1% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 36701 = 75% variables out of 49060 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 66509 negative 90.2% of 73754 except 7245 9.8%
c [phase-count-1] 61840 positive 83.8% of 73754 except 11914 16.2%
c [phase-1] phase bias: 3458 positive 28%, 8901 negative 72%
c [sort-queue-1] sorted 12359 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 12359 (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 38748 variables 75.8% (12359 remain 24%)
c [simplification-1] removed 78583 irredundant clauses 51.6% (73754 remain 48%)
c [simplification-1] maximum reduction of 76% = max (76%, 52%)
c [simplification-1] large reduction 76% >= 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   12358    73754       120      96      8   144    0     3    7   4%      0    3    2    0 20663%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 4 variables
c [simpleprobe-2] all 12355 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 6546 variables remain 53% (5809 retained 47%)
c [simpleprobe-2] removed 0 variables, found 543 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 24710 literals 100%
c [treelook-1] scheduling used 274498 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 305445 steps
c [treelook-1] 24669 literals remain 100%
c [treelook-1] 12355 variables remain to probed next time 100%
c [decomp-5] removed 2 variables
c [treelook-1] removed 2 variables, found 2174 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 7669 probes remain 62% after last round
c [basicprobe-1-0] removed 0 variables, found 9610 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 946 tauts, 0 hbrs, 1339 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 12353 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 199 variables 2% in round 1 in 10542441 steps
c [elim-2-1] backward subsumption/strengthening limit 9457559
c [elim-2-1-1] backward checking 1898 touched variables 15%
c [elim-2-1-1] incomplete backward checking 1084 remain 57%
c [elim-2-1] subsumed 17 and strengthened 350 clauses in 9457832 steps
c [elim-2] incomplete 542 not tried 4% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 199 = 2% variables out of 12353 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 12154 enqueued variables after 1000 conflicts
c [score-dist-2] active 0 (0%), one 4084 (34%), zero 8070 (66%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 204 variables 1.7% (12154 remain 24%)
c [simplification-2] removed 634 irredundant clauses 0.9% (73120 remain 48%)
c [simplification-2] maximum reduction of 2% = max (2%, 1%)
c [simplification-2] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-2] new conflict interval 6666
c [simplification-2] penalized conflict interval 6666 = 1 * 6666
c [simplification-2] hard conflict limit 17666 (soft 7666 + delta 10000)
c [simplification-2] new conflict limit 7666 (hard 17666)
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.9   12153    73120      1574    1181    114 10665    2    29    8   6%     11   29    5    0 4198%
c i    3.0   12152    73120      2316    1768    176 10679    2    34    8   7%      8   33    6    0 3290%
c i    3.9   12138    73120      5760    4565    390 10752    5    43    8  10%     38   40    7    0 1440%
c 
c [simplification-3] limit of 135 binary hit after 135 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 86 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] 86 out of 86 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 31 at-most-one constraints, 22 used 71%
c [card-2] exported 22 binary clauses, 1.0 per/constraint
c [decomp-6] removed 28 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 24252 literals 100%
c [treelook-2] scheduling used 291726 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 306373 steps
c [treelook-2] 24228 literals remain 100%
c [treelook-2] 12126 variables remain to probed next time 100%
c [treelook-2] removed 0 variables, found 1016 hbrs
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 12126 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 21 not tried 0% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 60 = 0% variables out of 12126 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 12066 enqueued variables after 5818 conflicts
c [score-dist-3] active 0 (0%), one 9051 (75%), zero 3015 (25%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 72 variables 0.6% (12066 remain 24%)
c [simplification-3] removed 249 irredundant clauses 0.3% (72871 remain 48%)
c [simplification-3] maximum reduction of 1% = max (1%, 0%)
c [simplification-3] forced so keeping old conflict interval 6666
c [simplification-3] conflict limit remains at 7666 (hard 17666)
c [simplification-3] new binary interval 1000
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.7   12065    72871      6636    5234    401 11754    5    44    8  11%     19   41    7    1 1261%
c 
c [simplification-4] limit 7666 conflicts (hard 17666) hit after 7666 conflicts
c [decomp-8] removed 3 variables
c [unhide-3] limit 69942 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 94 tauts, 0 hbrs, 2974 literals
c [elim-4] 21 variables 0% will be scheduled this time
c [elim-4] scheduled 21 variables 0%
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] no variable eliminated in round 1 in 9358347 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 21 scheduled
c [sort-queue-4] sorted 12063 enqueued variables after 7666 conflicts
c [score-dist-4] active 0 (0%), one 9957 (83%), zero 2106 (17%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 2 variables 0.0% (12063 remain 24%)
c [simplification-4] removed 77 irredundant clauses 0.1% (72794 remain 48%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 26666
c [simplification-4] penalized conflict interval 26666 = 1 * 26666
c [simplification-4] hard conflict limit 47665 (soft 34332 + delta 13333)
c [simplification-4] new conflict limit 34332 (hard 47665)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    5.4   12062    72794      8783    7081    494 11765    6    47    9  13%     20   42    8    1  998%
c i    5.7   12059    72794     10002    8127    555 11776    6    47    9  13%     12   41    7    1  766%
c i    5.7   12058    72794     10003    8127    555 11776    6    46    9  13%     12   41    7    1  763%
c i    5.7   12057    72794     10019    8135    558 11779    6    46    9  13%     12   41    7    1  738%
c i    5.7   12056    72794     10022    8135    559 11780    6    46    9  13%     12   41    7    1  731%
c i    5.7   12055    72794     10024    8135    558 11781    6    46    9  13%     12   41    7    1  728%
c i    6.7   12052    72794     14408   12034    733 11812    7    45    9  15%     49   37    7    1  526%
c i    6.7   12050    72794     14409   12034    733 11812    7    45    9  15%     49   37    7    1  524%
c i    6.9   12049    72794     14922   12489    753 11817    7    45    9  15%     30   37    8    1  603%
c i    6.9   12046    72794     15111   12663    760 11819    7    45    9  15%     24   37    8    1  599%
c 
c [simplification-5] limit of 15 iterations hit after 15 iterations
c [quatres-1] found 15891 quaternary clauses 48% in total
c [quatres-1-2] added 108 single-self-subsuming ternary resolvents
c [quatres-1-2] added 488 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 12046 free variables schedulable
c [ternres-1] 8610 ternary resolvents (50 bin, 8560 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 2626 xors of average arity 3.0
c [gauss-1] connected 7816 occurrences of 648 variables (average 12.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 14 variables
c [basicprobe-2] limit 3152873 penalty 1 = 1 + 0
c [basicprobe-2-0] 5262 probes remain 44% after last round
c [basicprobe-2-0] 17 units = 13 failed (76%) + 4 lifted (24%)
c [basicprobe-2-0] removed 15 variables, found 14697 hbrs
c [bate-1] eliminated 48 asymmetric tautologies during probing
c [transred-1] limit 1261149 with penalty 0 = 0 + 0
c [transred-1] removed 780 transitive binary clauses
c [transred-1] found 2 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 12015 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 840 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 28
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 27
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 26
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 25
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 24
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 23
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 22
c [cce-1-1] eliminated 1 clauses out of 8 (12%) of length 21
c [cce-1-1] eliminated 1 clauses out of 4 (25%) of length 20
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 17
c [cce-1-1] eliminated 1 clauses out of 6 (17%) of length 16
c [cce-1-1] eliminated 1 clauses out of 8 (12%) of length 15
c [cce-1-1] eliminated 1 clauses out of 24 (4%) of length 13
c [cce-1-1] eliminated 2 clauses out of 35 (6%) of length 12
c [cce-1-1] eliminated 8 clauses out of 40 (20%) of length 11
c [cce-1-1] eliminated 8 clauses out of 65 (12%) of length 10
c [cce-1-1] eliminated 33 clauses out of 240 (14%) of length 9
c [cce-1-1] eliminated 147 clauses out of 704 (21%) of length 8
c [cce-1-1] eliminated 224 clauses out of 1559 (14%) of length 7
c [cce-1-1] eliminated 3 clauses out of 3565 (0%) of length 6
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 438 large clauses in 30000005 steps
c [cce-1-1] allowing another 15000002 steps for small clauses
c [cce-1-1] scheduling 30165 clauses = 18020 binary + 12145 ternary
c [cce-1-1] tried to eliminate 4373 small clauses 14%
c [cce-1-1] eliminated 93 binary clauses 1%
c [cce-1-1] eliminated 96 ternary clauses 1%
c [cce-1-1] eliminated 189 small clauses 1%
c [cce-1-1] eliminated 189 small clauses in 30000005 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 627 covered clauses in round 1
c [cce-1] eliminated 627 covered clauses in TOTAL during 1 rounds
c [cce-1] 627 < 1/100 * 71643 = 716 considered unsuccessful
c [bca-1] limit of 10000000 steps and 142532 added (scaled 2)
c [bca-1] 11653 out of 24032 literals actually usable 48%
c [bca-1] added 1 blocked clauses in 41794 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 4716 pos 39.3% + 7299 neg 60.7% = 12015 sched 100.0% ret 0
c [sweep-1-1] 1021302 steps 26 queries 1848.65 avg class size
c [sweep-1-1] 394 decisions 25 SAT calls 68.88 avg env size
c [sweep-1-1] 10900 variables remain 91% (1113 retained 9%)
c [decomp-10] removed 15 variables
c [sweep-1-1] removed 15 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 15 vars in TOTAL (1 rounds, 25 queries)
c [sort-queue-5] sorted 12000 enqueued variables after 15111 conflicts
c [score-dist-5] active 0 (0%), one 11413 (95%), zero 587 (5%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 46 variables 0.4% (12000 remain 23%)
c [simplification-5] removed 1822 irredundant clauses 2.5% (70972 remain 47%)
c [simplification-5] maximum reduction of 3% = max (0%, 3%)
c [simplification-5] forced so keeping old conflict interval 26666
c [simplification-5] conflict limit remains at 34360 (hard 47665)
c [simplification-5] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    8.9   11999    70972     16953   14704   9770 26159    7    46   11  15%     16   36    6    2  412%
c i    9.0   11989    70972     17353   15042   9794 26172    7    45   11  16%     10   36    7    2  429%
c i    9.0   11987    70972     17534   15207   9801 26174    7    45   11  16%      8   35    8    2  483%
c i    9.0   11986    70972     17655   15321   9803 26175    7    45   11  16%      7   35    8    2  507%
c i    9.0   11983    70972     17694   15349   9804 26181    7    45   11  16%      6   35    8    2  492%
c i    9.3   11982    70972     18857   16409   9836 26188    7    45   11  16%      6   34    8    2  449%
c i   10.3   11981    70972     22771   20047   9923 26201    8    45   11  18%     40   33    9    2  449%
c i   10.4   11980    70972     23105   20341   9945 26206    8    46   11  18%     28   33    7    2  353%
c i   10.8   11979    70972     24757   21845  10002 26229    8    46   11  17%     13   33    7    2  303%
c i   10.8   11978    70972     24763   21847  10002 26232    8    46   11  17%     13   33    7    2  297%
c i   10.8   11975    70972     24764   21846  10002 26233    8    46   11  17%     13   33    7    2  296%
c i   10.8   11969    70972     24770   21847  10006 26233    8    46   11  17%     13   33    7    2  291%
c i   10.8   11965    70972     24771   21847  10006 26233    8    46   11  17%     13   33    7    2  290%
c i   11.4   11964    70972     27555   24411  10085 26257    8    47   12  18%     23   32    9    3  351%
c i   11.4   11960    70972     27556   24411  10084 26258    8    47   12  18%     23   32    9    3  350%
c i   11.5   11951    70972     27670   24520  10086 26259    8    47   12  18%     20   32    9    3  366%
c i   11.8   11950    70972     28989   25767  10128 26264    9    47   12  18%      9   31    9    3  320%
c i   11.8   11949    70972     28990   25767  10128 26264    9    47   12  18%      9   31    9    3  318%
c i   12.7   11946    70972     32243   28840  10195 26277    9    47   12  19%     29   30    8    3  284%
c i   12.7   11940    70972     32247   28840  10197 26277    9    47   12  19%     28   30    8    3  280%
c i   12.7   11936    70972     32253   28842  10198 26278    9    47   12  19%     28   30    8    3  275%
c i   13.0   11926    70972     33639   30153  10232 26283    9    48   14  18%     11   31    8    3  273%
c i   13.1   11925    70972     33798   30293  10237 26286    9    48   14  18%      9   30    7    3  239%
c 
c [simplification-6] limit 34405 conflicts (hard 47665) hit after 34406 conflicts
c [quatres-2] found 16568 quaternary clauses 46% in total
c [quatres-2-2] added 121 single-self-subsuming ternary resolvents
c [quatres-2-2] added 346 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 11873 free variables schedulable
c [ternres-2] 238 ternary resolvents (2 bin, 236 trn)
c [ternres-2] 3281 variables remain 28% (8592 retained 72%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 56 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] 56 out of 56 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 177 variables
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 906 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 11822 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 25 blocked clauses
c [block-2] 25 < 1/100 * 70066 = 700 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 11821 variables 100%
c [elim-5] limit of 28931954 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 9 not tried 0% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 308 = 3% variables out of 11821 scheduled
c [bca-2] limit of 10000000 steps and 139138 added (scaled 2)
c [bca-2] 7575 out of 23028 literals actually usable 33%
c [bca-2] added 0 blocked clauses in 45278 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 4103 pos 39.4% + 6317 neg 60.6% = 10420 sched 90.5% ret 1093
c [sweep-2-1] 1026748 steps 22 queries 1258.73 avg class size
c [sweep-2-1] 533 decisions 24 SAT calls 67.75 avg env size
c [sweep-2-1] 10270 variables remain 89% (1243 retained 11%)
c [decomp-12] removed 6 variables
c [sweep-2-1] removed 6 vars (0 failed, 3 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 6 vars in TOTAL (1 rounds, 21 queries)
c [sort-queue-6] sorted 11507 enqueued variables after 34406 conflicts
c [score-dist-6] active 0 (0%), one 11460 (100%), zero 47 (0%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 366 variables 3.1% (11507 remain 23%)
c [simplification-6] removed 1665 irredundant clauses 2.3% (69307 remain 45%)
c [simplification-6] maximum reduction of 3% = max (3%, 2%)
c [simplification-6] geometric conflict interval increment 6666 = 26666 / 4
c [simplification-6] new conflict interval 33332
c [simplification-6] penalized conflict interval 33332 = 1 * 33332
c [simplification-6] hard conflict limit 84404 (soft 67738 + delta 16666)
c [simplification-6] new conflict limit 67738 (hard 84404)
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   14.3   11506    69307     34656   27708   9857 25004    8    47   14  18%      3   29    8    3  251%
c i   14.7   11505    69307     36145   29084   9900 25015    9    46   14  19%      6   27    9    3  274%
c i   15.2   11504    69307     38303   31126   9945 25023    9    45   14  20%     13   25    9    3  261%
c i   15.3   11502    69307     38340   31155   9947 25024    9    45   14  20%     12   25    9    3  251%
c i   15.4   11501    69307     38739   31532   9953 25028    9    45   14  20%      7   25    9    4  270%
c i   15.4   11500    69307     38800   31590   9954 25028    9    45   14  20%      6   25   10    4  271%
c i   15.4   11495    69307     38802   31590   9955 25028    9    45   14  20%      6   25    9    4  269%
c i   15.4   11492    69307     39015   31791   9962 25029    9    45   14  20%      4   25    8    4  238%
c i   15.4   11474    69307     39023   31792   9964 25031    9    45   14  20%      3   25    8    4  233%
c i   15.6   11473    69307     39746   32475   9970 25035    9    45   14  19%      1   25    9    4  252%
c i   15.6   11468    69307     39748   32476   9970 25035    9    45   14  19%      1   25    9    4  250%
c i   15.7   11466    69307     39940   32654   9973 25035    9    45   14  20%     -1   25   10    4  264%
c i   15.7   11465    69307     39941   32654   9973 25035    9    45   14  20%     -1   25    9    4  263%
c i   15.8   11462    69307     40622   33303   9982 25042    9    45   14  20%     -1   25   10    4  276%
c i   16.1   11441    69307     41436   34079   9998 25045    9    46   14  20%     -1   25    9    4  234%
c i   16.2   11440    69307     42090   34707  10006 25047    9    47   14  19%     -2   26    9    4  244%
c i   16.2   11438    69307     42092   34707  10006 25047    9    47   14  19%     -2   26    9    4  243%
c i   16.4   11381    69307     42548   35139  10017 25050    9    46   14  20%     -3   25   10    4  256%
c i   16.4   11379    69307     42757   35328  10021 25051    9    47   14  20%     -3   25   10    4  248%
c i   16.4   11378    69307     42758   35328  10021 25051    9    47   14  20%     -3   25   10    4  247%
c i   16.4   11377    69307     42779   35342  10024 25053    9    46   14  20%     -4   25    9    4  235%
c i   16.4   11376    69307     42790   35348  10024 25053    9    46   14  20%     -4   25    9    4  229%
c i   16.6   11375    69307     43463   35966  10048 25060    9    47   14  19%     -3   25    9    4  241%
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   16.6   11368    69307     43466   35968  10048 25060    9    47   14  19%     -3   25    9    4  240%
c i   16.7   11367    69307     43950   36423  10061 25064    9    47   14  20%     -3   25   10    4  246%
c i   16.7   11362    69307     43959   36427  10062 25065    9    47   14  20%     -3   25   10    4  241%
c i   17.0   11361    69307     44908   37327  10078 25072    9    47   14  20%     -1   25    9    4  215%
c i   17.3   11343    69307     46094   38426  10110 25082    9    46   14  20%      2   24    9    4  227%
c i   17.4   11337    69307     46429   38742  10114 25085    9    46   14  20%     -0   23    9    4  217%
c i   17.5   11331    69307     46657   38964  10116 25087    9    46   14  20%     -1   23   10    4  232%
c i   17.8   11330    69307     47881   40134  10140 25089    9    46   14  21%      2   23   10    4  236%
c i   18.7   11328    69307     50861   42945  10201 25099    9    45   15  21%     24   20   10    5  212%
c i   18.7   11327    69307     50865   42946  10202 25100    9    44   15  21%     23   20    9    5  209%
c i   18.7   11320    69307     50866   42946  10202 25100    9    44   15  21%     23   20    9    5  208%
c i   18.8   11309    69307     51000   43074  10204 25100    9    44   15  21%     20   20   10    5  217%
c i   18.8   11307    69307     51007   43075  10206 25102    9    44   15  21%     19   20   10    5  213%
c i   18.8   11300    69307     51214   43270  10208 25103    9    44   15  22%     15   20    9    5  209%
c i   19.9   11298    69307     54636   46525  10255 25113    9    45   16  21%     30   20   10    5  208%
c i   19.9   11297    69307     54699   46567  10262 25114    9    45   16  21%     27   20    9    5  198%
c i   21.7   11296    69307     60286   51911  10318 25130   10    45   17  22%     60   18   11    5  213%
c i   21.9   11292    69307     60642   52253  10326 25131   10    45   17  21%     40   18    9    5  177%
c i   21.9   11289    69307     60689   52292  10328 25132   10    45   17  21%     37   18    9    5  180%
c i   22.5   11262    69307     62858   54371  10352 25140   10    44   18  22%     13   16   10    5  182%
c i   23.6   11260    69307     66019   57366  10398 25151   10    44   18  22%     22   16    9    6  162%
c 
c [simplification-7] limit 67791 conflicts (hard 84404) hit after 67792 conflicts
c [quatres-3] found 16842 quaternary clauses 41% in total
c [quatres-3-1] removed 5 duplicate quaternary clauses
c [quatres-3-2] added 88 single-self-subsuming ternary resolvents
c [quatres-3-2] added 238 quaternary resolvents
c [ternres-3] limit 5989279 with penalty 0 = 0 + 0
c [ternres-3] 3101 schedulable variables 27%
c [ternres-3] 855 ternary resolvents (6 bin, 849 trn)
c [ternres-3] 42 variables remain 0% (11218 retained 100%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 770 xors of average arity 2.8
c [gauss-2] connected 2142 occurrences of 422 variables (average 5.1)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [decomp-13] removed 82 variables
c [gauss-2] exported 1 unary, 26 binary and 3 ternary equations
c [simpleprobe-3] 5907 schedulable variables 53%
c [simpleprobe-3] limit 11978559 penalty 1 = 1 + 0
c [decomp-15] removed 30 variables
c [simpleprobe-3] 3625 variables remain 33% (7523 retained 67%)
c [simpleprobe-3] removed 30 variables, found 3204 hbrs, 9 units
c [unhide-4] limit 299463 with penalty 2 = 2 + 0
c [unhide-4-4] 4 units, 39 failed, 2163 tauts, 0 hbrs, 70594 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 438 transitive binary clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 30 (7%) of length 12
c [cce-2-1] eliminated 2 clauses out of 42 (5%) of length 11
c [cce-2-1] eliminated 6 clauses out of 77 (8%) of length 10
c [cce-2-1] eliminated 14 clauses out of 261 (5%) of length 9
c [cce-2-1] eliminated 23 clauses out of 625 (4%) of length 8
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 47 large clauses in 15000002 steps
c [cce-2-1] allowing another 7500001 steps for small clauses
c [cce-2-1] scheduling 27965 clauses = 16584 binary + 11381 ternary
c [cce-2-1] tried to eliminate 2156 small clauses 8%
c [cce-2-1] eliminated 45 binary clauses 0%
c [cce-2-1] eliminated 50 ternary clauses 0%
c [cce-2-1] eliminated 95 small clauses 0%
c [cce-2-1] eliminated 274 small clauses in 15000016 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 321 covered clauses in round 1
c [cce-2] eliminated 321 covered clauses in TOTAL during 1 rounds
c [cce-2] 321 < 1/100 * 67217 = 672 considered unsuccessful
c [elim-6] 9 variables 0% will be scheduled this time
c [elim-6] scheduled 9 variables 0%
c [elim-6] limit of 119785595 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 22710205 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 9 scheduled
c [sweep-3] limit 1796783 penalty 0 = 0 + 0
c [sweep-3-1] 3783 pos 38.3% + 6097 neg 61.7% = 9880 sched 88.8% ret 1240
c [sweep-3-1] 1834009 steps 27 queries 1003.93 avg class size
c [sweep-3-1] 1006 decisions 28 SAT calls 123.18 avg env size
c [sweep-3-1] 9564 variables remain 86% (1556 retained 14%)
c [decomp-16] removed 31 variables
c [sweep-3-1] removed 31 vars (0 failed, 1 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 31 vars in TOTAL (1 rounds, 26 queries)
c [sort-queue-7] sorted 11089 enqueued variables after 67792 conflicts
c [score-dist-7] active 0 (0%), one 11086 (100%), zero 3 (0%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 171 variables 1.5% (11089 remain 22%)
c [simplification-7] removed 2496 irredundant clauses 3.6% (66811 remain 44%)
c [simplification-7] maximum reduction of 4% = max (2%, 4%)
c [simplification-7] geometric conflict interval increment 6666 = 33332 / 5
c [simplification-7] new conflict interval 39998
c [simplification-7] penalized conflict interval 39998 = 1 * 39998
c [simplification-7] hard conflict limit 127789 (soft 107790 + delta 19999)
c [simplification-7] new conflict limit 107790 (hard 127789)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   27.0   11088    66811     70464   60759  10925 24611   10    44   20  23%     40   14   10    6  175%
c -   28.3   11087    66811     73814   26853  10958 24614   10    44   12  23%     24   14   10    6  160%
c i   30.9   11086    66811     83643   36289  11049 24640   10    44   13  22%    161   12    9    7  130%
c i   31.9   11085    66811     86966   39468  11081 24648   10    44   13  23%     13   11   10    7  154%
c i   34.8   11083    66811     96221   48286  11156 24666   10    44   16  23%     93   10   11    7  151%
c i   37.0   11082    66811    102948   54763  11200 24676   10    41   16  25%     52    6    9    8  124%
c 
c [simplification-8] limit 107790 conflicts (hard 127789) hit after 107790 conflicts
c [quatres-4] found 17640 quaternary clauses 39% in total
c [quatres-4-1] removed 5 duplicate quaternary clauses
c [quatres-4-1] added 2 double-self-subsuming ternary resolvents
c [quatres-4-2] added 95 single-self-subsuming ternary resolvents
c [quatres-4-2] added 192 quaternary resolvents
c [ternres-4] limit 9935142 with penalty 0 = 0 + 0
c [ternres-4] 41 schedulable variables 0%
c [ternres-4] 850 ternary resolvents (6 bin, 844 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 1292 xors of average arity 3.0
c [gauss-3] connected 3833 occurrences of 342 variables (average 11.2)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-17] removed 22 variables
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 392 transitive binary clauses
c [transred-4] found 4 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 11050 variables 100%
c [block-3] limit of 49675710 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 260 blocked clauses
c [block-3] 260 < 1/100 * 66678 = 666 considered unsuccessful
c [bca-3] limit of 10000000 steps and 133212 added (scaled 2)
c [bca-3] 5031 out of 22066 literals actually usable 23%
c [bca-3] added 1 blocked clauses in 70513 steps
c [sweep-4] limit 2980542 penalty 0 = 0 + 0
c [sweep-4-1] 3500 pos 36.9% + 5978 neg 63.1% = 9478 sched 85.9% ret 1554
c [sweep-4-1] 3403761 steps 71 queries 410.76 avg class size
c [sweep-4-1] 1290 decisions 75 SAT calls 80.53 avg env size
c [sweep-4-1] 5412 variables remain 49% (5620 retained 51%)
c [decomp-18] removed 17 variables
c [sweep-4-1] removed 17 vars (0 failed, 6 eqs, 4 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 17 vars in TOTAL (1 rounds, 70 queries)
c [sort-queue-8] sorted 11015 enqueued variables after 107790 conflicts
c [score-dist-8] active 0 (0%), one 11014 (100%), zero 1 (0%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 67 variables 0.6% (11015 remain 22%)
c [simplification-8] removed 473 irredundant clauses 0.7% (66338 remain 44%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 19999 = 39998 / 2
c [simplification-8] new conflict interval 59997
c [simplification-8] penalized conflict interval 59997 = 1 * 59997
c [simplification-8] hard conflict limit 197785 (soft 167787 + delta 29998)
c [simplification-8] new conflict limit 167787 (hard 197785)
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 -   43.8   11015    66337    119084   35212  12155 24997   11    42   13  25%    180    5   10    8  121%
c i   47.7   11014    66337    143084   56311  12275 25043    6    32   15  20%    439   -9    6    8   75%
c i   51.9   11013    66337    156433   68647  12350 25054   10    37   18  27%     27   -4   10    8  124%
c i   52.5   11012    66337    158194   70324  12361 25058   10    37   18  28%   -115   -4   11    8  128%
c -   55.1   11001    66337    165307   44918  12388 25064   11    39   14  28%    -57   -2   11    9  126%
c i   56.2   11000    66337    172098   50544  12410 25067    8    30   16  26%     50  -10    7    8   82%
c 
c [simplification-9] limit 167787 conflicts (hard 197785) hit after 193146 conflicts
c [quatres-5] found 18299 quaternary clauses 33% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-1] added 3 double-self-subsuming ternary resolvents
c [quatres-5-2] added 69 single-self-subsuming ternary resolvents
c [quatres-5-2] added 125 quaternary resolvents
c [ternres-5] limit 17082722 with penalty 0 = 0 + 0
c [ternres-5] all 11000 free variables schedulable
c [ternres-5] 1589 ternary resolvents (50 bin, 1539 trn)
c [ternres-5] 20 variables remain 0% (10980 retained 100%)
c [gauss-4] limit 3416544 penalty 0 = 0 + 0
c [gauss-4] extracted 1676 xors of average arity 3.1
c [gauss-4] connected 5160 occurrences of 443 variables (average 11.6)
c [gauss-4] limit 3416544 penalty 0 = 0 + 0
c [gauss-4] fully completed
c [decomp-19] removed 24 variables
c [gauss-4] exported 0 unary, 2 binary and 0 ternary equations
c [treelook-3] limit 854136 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 21952 literals 100%
c [treelook-3] scheduling used 480255 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 854136 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 854779 steps
c [treelook-3] 21906 literals remain 100%
c [treelook-3] 10976 variables remain to probed next time 100%
c [treelook-3] removed 0 variables, found 1689 hbrs
c [unhide-5] limit 1708272 with penalty 1 = 1 + 0
c [unhide-5-6] 5 units, 34 failed, 5248 tauts, 0 hbrs, 56530 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 314 transitive binary clauses
c [transred-5] found 5 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 10952 variables 100%
c [elim-7] limit of 170827223 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 258 variables 2% in round 1 in 54041259 steps
c [elim-7-1] backward subsumption/strengthening limit 54041200
c [elim-7-1-1] backward checking 1478 touched variables 13%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 21 and strengthened 38 clauses in 7728714 steps
c [elim-7-1] rescheduled 137 variables 1% by backward subsumption
c [elim-7-2] eliminated 14 variables 0% in round 2 in 11017920 steps
c [elim-7-2] backward subsumption/strengthening limit 11017900
c [elim-7-2-1] backward checking 88 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 5 and strengthened 1 clauses in 1116145 steps
c [elim-7-2] rescheduled 19 variables 0% by backward subsumption
c [elim-7-3] eliminated 3 variables 0% in round 3 in 3310720 steps
c [elim-7-3] backward subsumption/strengthening limit 3310700
c [elim-7-3-1] backward checking 14 touched variables 0%
c [elim-7-3-1] fully completed backward checking in 1 rounds
c [elim-7-3] subsumed 0 and strengthened 0 clauses in 36993 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 278 = 3% variables out of 10952 scheduled
c [bca-4] limit of 10000000 steps and 130049 added (scaled 2)
c [bca-4] 5073 out of 21350 literals actually usable 24%
c [bca-4] added 1 blocked clauses in 69421 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 51248160 penalty 0 = 0 + 0
c [sweep-5-1] 2099 pos 40.6% + 3076 neg 59.4% = 5175 sched 48.5% ret 5499
c [sweep-5-1] 29466515 steps 878 queries 28.47 avg class size
c [sweep-5-1] 10084 decisions 717 SAT calls 61.36 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-22] removed 509 variables
c [sweep-5-1] removed 509 vars (0 failed, 400 eqs, 303 impls)
c [sweep-5-2] 3672 pos 36.1% + 6493 neg 63.9% = 10165 sched 100.0% ret 0
c [sweep-5-2] 21782305 steps 504 queries 47.10 avg class size
c [sweep-5-2] 7657 decisions 450 SAT calls 76.72 avg env size
c [sweep-5-2] 685 variables remain 7% (9479 retained 93%)
c [decomp-23] removed 152 variables
c [sweep-5-2] removed 152 vars (0 failed, 138 eqs, 132 impls)
c [sweep-5] removed 661 vars in TOTAL (2 rounds, 1380 queries)
c [sort-queue-9] sorted 10013 enqueued variables after 193146 conflicts
c [score-dist-9] active 0 (0%), one 10013 (100%), zero 0 (0%)
c [score-dist-9] max exp 1, different 1 (50%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 987 variables 9.0% (10013 remain 20%)
c [simplification-9] removed 3032 irredundant clauses 4.6% (63305 remain 42%)
c [simplification-9] maximum reduction of 9% = max (9%, 5%)
c [simplification-9] large reduction 9% >= 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 205146 (soft 195146 + delta 10000)
c [simplification-9] new conflict limit 195146 (hard 205146)
c 
c [simplification-10] limit 195146 conflicts (hard 205146) hit after 195148 conflicts
c [quatres-6] found 17932 quaternary clauses 36% in total
c [quatres-6-1] removed 35 duplicate quaternary clauses
c [quatres-6-1] added 10 double-self-subsuming ternary resolvents
c [quatres-6-2] added 112 single-self-subsuming ternary resolvents
c [quatres-6-2] added 254 quaternary resolvents
c [ternres-6] limit 17256446 with penalty 0 = 0 + 0
c [ternres-6] 15 schedulable variables 0%
c [ternres-6] 2025 ternary resolvents (17 bin, 2008 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 1078527 penalty 3 = 3 + 0
c [card-4] found 103 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1078527 for elimination
c [card-4] 103 out of 103 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-5] limit 3451289 penalty 0 = 0 + 0
c [gauss-5] extracted 1564 xors of average arity 3.1
c [gauss-5] connected 4846 occurrences of 385 variables (average 12.6)
c [gauss-5] limit 3451289 penalty 0 = 0 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-24] removed 5 variables
c [basicprobe-3] limit 86282234 penalty 0 = 0 + 0
c [basicprobe-3-0] 3836 sched 38%, 23 failed, 0 lifted, 31120 hbrs
c [decomp-25] removed 66 variables
c [basicprobe-3-1] 4700 sched 47%, 13 failed, 0 lifted, 5235 hbrs
c [decomp-26] removed 26 variables
c [basicprobe-3-2] 4653 sched 47%, 1 failed, 0 lifted, 451 hbrs
c [decomp-27] removed 3 variables
c [basicprobe-3-3] 4648 sched 47%, 0 failed, 0 lifted, 70 hbrs
c [basicprobe-3-4] 4278 probes remain 43% after last round
c [basicprobe-3-4] 37 units = 37 failed (100%) + 0 lifted (0%)
c [basicprobe-3-4] removed 95 variables, found 36882 hbrs
c [bate-2] eliminated 118 asymmetric tautologies during probing
c [unhide-6] limit 3451289 with penalty 0 = 0 + 0
c [unhide-6-9] 0 units, 0 failed, 8592 tauts, 0 hbrs, 36611 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 469 transitive binary clauses
c [cce-3] limit of 21570558 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 2 clauses out of 11 (18%) of length 12
c [cce-3-1] eliminated 1 clauses out of 33 (3%) of length 11
c [cce-3-1] eliminated 8 clauses out of 68 (12%) of length 10
c [cce-3-1] eliminated 25 clauses out of 212 (12%) of length 9
c [cce-3-1] eliminated 63 clauses out of 583 (11%) of length 8
c [cce-3-1] eliminated 25 clauses out of 1270 (2%) of length 7
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 124 large clauses in 21570644 steps
c [cce-3-1] allowing another 10785322 steps for small clauses
c [cce-3-1] scheduling 25365 clauses = 14865 binary + 10500 ternary
c [cce-3-1] tried to eliminate 1936 small clauses 8%
c [cce-3-1] eliminated 72 binary clauses 0%
c [cce-3-1] eliminated 188 ternary clauses 2%
c [cce-3-1] eliminated 260 small clauses 1%
c [cce-3-1] eliminated 260 small clauses in 21570560 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 384 covered clauses in round 1
c [cce-3] eliminated 384 covered clauses in TOTAL during 1 rounds
c [cce-3] 384 < 1/100 * 62199 = 621 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 9913 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 6902578720 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 448 variables 5% in round 1 in 51427061 steps
c [elim-8-1] backward subsumption/strengthening limit 51427000
c [elim-8-1-1] backward checking 1593 touched variables 16%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 14 and strengthened 28 clauses in 6513740 steps
c [elim-8-1] rescheduled 110 variables 1% by backward subsumption
c [elim-8-2] eliminated 11 variables 0% in round 2 in 6399622 steps
c [elim-8-2] backward subsumption/strengthening limit 6399600
c [elim-8-2-1] backward checking 103 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 2 and strengthened 4 clauses in 250870 steps
c [elim-8-2] rescheduled 9 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 5454 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 459 = 5% variables out of 9913 scheduled
c [bca-5] limit of 10000000 steps and 119719 added (scaled 2)
c [bca-5] 4424 out of 18910 literals actually usable 23%
c [bca-5] added 25 blocked clauses in 65202 steps
c [sweep-6] limit 5176934 penalty 0 = 0 + 0
c [sweep-6-1] 207 pos 37.5% + 345 neg 62.5% = 552 sched 5.8% ret 8902
c [sweep-6-1] 5215545 steps 113 queries 17.82 avg class size
c [sweep-6-1] 1656 decisions 106 SAT calls 83.50 avg env size
c [sweep-6-1] 268 variables remain 3% (9185 retained 97%)
c [decomp-29] removed 47 variables
c [sweep-6-1] removed 47 vars (0 failed, 47 eqs, 29 impls)
c [sweep-6] removed 47 vars in TOTAL (1 rounds, 112 queries)
c [sort-queue-10] sorted 9407 enqueued variables after 195148 conflicts
c [score-dist-10] active 0 (0%), one 9407 (100%), zero 0 (0%)
c [score-dist-10] max exp 1, different 1 (50%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 606 variables 6.1% (9407 remain 18%)
c [simplification-10] removed 3698 irredundant clauses 5.8% (59604 remain 39%)
c [simplification-10] maximum reduction of 6% = max (6%, 6%)
c [simplification-10] large reduction 6% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 207148 (soft 197148 + delta 10000)
c [simplification-10] new conflict limit 197148 (hard 207148)
c 
c [simplification-11] limit 197148 conflicts (hard 207148) hit after 204134 conflicts
c [quatres-7] found 17322 quaternary clauses 36% in total
c [quatres-7-1] removed 9 duplicate quaternary clauses
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 69 single-self-subsuming ternary resolvents
c [quatres-7-2] added 212 quaternary resolvents
c [ternres-7] limit 17737257 with penalty 0 = 0 + 0
c [ternres-7] all 9407 free variables schedulable
c [ternres-7] 1351 ternary resolvents (14 bin, 1337 trn)
c [ternres-7] 5 variables remain 0% (9402 retained 100%)
c [decomp-30] removed 4 variables
c [simpleprobe-4] 3133 schedulable variables 33%
c [simpleprobe-4] limit 70949031 penalty 0 = 0 + 0
c [decomp-31] removed 24 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 24 variables, found 6559 hbrs, 0 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 735 transitive binary clauses
c [transred-7] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 9378 variables 100%
c [block-4] limit of 44343144 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 87 blocked clauses
c [block-4] 87 < 1/100 * 59460 = 594 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 9372 variables 100%
c [elim-9] limit of 354745157 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 66 variables 1% in round 1 in 51078437 steps
c [elim-9-1] backward subsumption/strengthening limit 51078400
c [elim-9-1-1] backward checking 458 touched variables 5%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 4 and strengthened 7 clauses in 1153771 steps
c [elim-9-1] rescheduled 36 variables 0% by backward subsumption
c [elim-9-2] no variable eliminated in round 2 in 1533542 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 66 = 1% variables out of 9372 scheduled
c [elim-9] 66 < 1/100 * 9372 = 93 considered unsuccessful
c [bca-6] limit of 10000000 steps and 118656 added (scaled 2)
c [bca-6] 4227 out of 18614 literals actually usable 23%
c [bca-6] added 34 blocked clauses in 71744 steps
c [sweep-7] limit 5321177 penalty 0 = 0 + 0
c [sweep-7-1] 85 pos 34.6% + 161 neg 65.4% = 246 sched 2.6% ret 9060
c [sweep-7-1] 5771176 steps 131 queries 8.69 avg class size
c [sweep-7-1] 1809 decisions 114 SAT calls 83.06 avg env size
c [sweep-7-1] 14 variables remain 0% (9292 retained 100%)
c [decomp-32] removed 35 variables
c [sweep-7-1] removed 35 vars (0 failed, 36 eqs, 35 impls)
c [sweep-7] removed 35 vars in TOTAL (1 rounds, 130 queries)
c [sort-queue-11] sorted 9271 enqueued variables after 204134 conflicts
c [score-dist-11] active 0 (0%), one 9271 (100%), zero 0 (0%)
c [score-dist-11] max exp 1, different 1 (50%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 136 variables 1.4% (9271 remain 18%)
c [simplification-11] removed 545 irredundant clauses 0.9% (59059 remain 39%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 29998 = 59997 / 2
c [simplification-11] new conflict interval 89995
c [simplification-11] penalized conflict interval 89995 = 1 * 89995
c [simplification-11] hard conflict limit 339126 (soft 294129 + delta 44997)
c [simplification-11] new conflict limit 294129 (hard 339126)
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   78.8    9270    59059    220022   77064  12780 53887    9    40   19  23%    449    3   10    9  118%
c i   78.9    9269    59059    220144   77178  12782 53887    9    40   19  23%    366    2   11    9  123%
c i   79.3    9268    59059    221243   78203  12795 53890   10    38   20  25%    -58    1   10    9  115%
c -   79.4    9268    59059    221488   46978  12796 53890   10    38   14  25%   -106    0   11    9  121%
c -   88.8    9268    59059    259714   51396  12929 53906   11    32   15  36%    284   -6   12    9  128%
c -   99.1    9268    59059    296094   54875  12967 53911   10    30   14  32%    599   -2   12    9  123%
c 
c [simplification-12] limit 294129 conflicts (hard 339126) hit after 325825 conflicts
c [quatres-8] found 17919 quaternary clauses 31% in total
c [quatres-8-1] removed 11 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 68 single-self-subsuming ternary resolvents
c [quatres-8-2] added 173 quaternary resolvents
c [ternres-8] limit 29410562 with penalty 0 = 0 + 0
c [ternres-8] 5 schedulable variables 0%
c [ternres-8] 564 ternary resolvents (4 bin, 560 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-6] limit 2941056 penalty 1 = 1 + 0
c [gauss-6] extracted 1066 xors of average arity 3.0
c [gauss-6] connected 3162 occurrences of 244 variables (average 13.0)
c [gauss-6] limit 2941056 penalty 1 = 1 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-33] removed 7 variables
c [unhide-7] limit 2941056 with penalty 1 = 1 + 0
c [unhide-7-11] 0 units, 2 failed, 3903 tauts, 0 hbrs, 46521 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 458 transitive binary clauses
c [bca-7] limit of 10000000 steps and 118259 added (scaled 2)
c [bca-7] 4019 out of 18520 literals actually usable 22%
c [bca-7] added 28 blocked clauses in 90639 steps
c [sweep-8] limit 8823168 penalty 0 = 0 + 0
c [sweep-8-1] 1 pos 7.7% + 12 neg 92.3% = 13 sched 0.1% ret 9246
c [sweep-8-1] 364835 steps 9 queries 4.56 avg class size
c [sweep-8-1] 78 decisions 7 SAT calls 49.86 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-34] removed 3 variables
c [sweep-8-1] removed 3 vars (0 failed, 1 eqs, 1 impls)
c [sweep-8-2] 3391 pos 36.6% + 5865 neg 63.4% = 9256 sched 100.0% ret 0
c [sweep-8-2] 8638529 steps 37 queries 489.05 avg class size
c [sweep-8-2] 1115 decisions 37 SAT calls 159.22 avg env size
c [sweep-8-2] 6178 variables remain 67% (3078 retained 33%)
c [decomp-35] removed 7 variables
c [sweep-8-2] removed 7 vars (0 failed, 2 eqs, 1 impls)
c [sweep-8] removed 10 vars in TOTAL (2 rounds, 44 queries)
c [sort-queue-12] sorted 9249 enqueued variables after 325825 conflicts
c [score-dist-12] active 0 (0%), one 9249 (100%), zero 0 (0%)
c [score-dist-12] max exp 1, different 1 (50%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 19 variables 0.2% (9249 remain 18%)
c [simplification-12] removed 195 irredundant clauses 0.3% (58864 remain 39%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 89995
c [simplification-12] new conflict interval 179990
c [simplification-12] penalized conflict interval 179990 = 1 * 179990
c [simplification-12] hard conflict limit 595810 (soft 505815 + delta 89995)
c [simplification-12] new conflict limit 505815 (hard 595810)
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 -  109.2    9249    58864    331972   55720  13249 50051   10    29   15  36%    778   -2    9   10   90%
c -  115.6    9249    58864    370912   59721  13267 50051    8    29   24  28%    888   -2    7    9   80%
c i  120.5    9248    58864    400345   86354  13288 50053    9    21   31  42%    937   -7   11    9  123%
c -  123.6    9248    58864    407463   60616  13292 50057   11    27   24  41%  -1601   -2   12    9  129%
c -  134.2    9248    58864    446258   61032  13338 50061   12    29   24  40%   -430    0   12   10  125%
c -  143.7    9248    58864    487128   64601  13368 50062   11    30   24  36%    245    0   11   10  119%
c -  153.9    9248    58864    527208   68889  13384 50066    8    23   16  32%    601   -3    6    9   69%
c i  158.3    9247    58864    553136   91316  13399 50066    7    14   22  48%    739   -9    6    9   64%
c -  162.6    9210    58864    568811   71829  13405 50067    8    10   17  82%  -1109  -11    8    9   93%
c i  169.0    9209    58864    589321   87779  13477 50082    6     8   21  82%   -536  -10    5    8   54%
c 
c [simplification-13] limit 505815 conflicts (hard 595810) hit after 595810 conflicts
c [quatres-9] found 16742 quaternary clauses 28% in total
c [quatres-9-1] removed 10 duplicate quaternary clauses
c [quatres-9-2] added 59 single-self-subsuming ternary resolvents
c [quatres-9-2] added 145 quaternary resolvents
c [ternres-9] limit 58815063 with penalty 0 = 0 + 0
c [ternres-9] all 9097 free variables schedulable
c [ternres-9] 1433 ternary resolvents (16 bin, 1417 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-7] limit 11763012 penalty 0 = 0 + 0
c [gauss-7] extracted 1736 xors of average arity 2.9
c [gauss-7] connected 4974 occurrences of 482 variables (average 10.3)
c [gauss-7] limit 11763012 penalty 0 = 0 + 0
c [gauss-7] fully completed
c [decomp-36] removed 112 variables
c [gauss-7] exported 0 unary, 4 binary and 0 ternary equations
c [unhide-8] limit 11763012 with penalty 0 = 0 + 0
c [unhide-8-20] 8 units, 196 failed, 9459 tauts, 0 hbrs, 33509 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 551 transitive binary clauses
c [transred-9] found 1 units
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 8901 variables 100%
c [elim-10] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 1139 variables 13% in round 1 in 47089037 steps
c [elim-10-1] backward subsumption/strengthening limit 47089000
c [elim-10-1-1] backward checking 2683 touched variables 30%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 13 and strengthened 26 clauses in 9621621 steps
c [elim-10-1] rescheduled 128 variables 1% by backward subsumption
c [elim-10-2] eliminated 18 variables 0% in round 2 in 21706836 steps
c [elim-10-2] backward subsumption/strengthening limit 21706800
c [elim-10-2-1] backward checking 92 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 2 and strengthened 4 clauses in 3312956 steps
c [elim-10-2] rescheduled 18 variables 0% by backward subsumption
c [elim-10-3] eliminated 2 variables 0% in round 3 in 6172784 steps
c [elim-10-3] backward subsumption/strengthening limit 6172700
c [elim-10-3-1] backward checking 0 touched variables 0%
c [elim-10-3-1] fully completed backward checking in 1 rounds
c [elim-10-3] subsumed 0 and strengthened 0 clauses in 56246 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 1159 = 13% variables out of 8901 scheduled
c [bca-8] limit of 10000000 steps and 98705 added (scaled 2)
c [bca-8] 4172 out of 15486 literals actually usable 27%
c [bca-8] added 24 blocked clauses in 61228 steps
c [sweep-9] limit 17644519 penalty 0 = 0 + 0
c [sweep-9-1] 1812 pos 34.8% + 3394 neg 65.2% = 5206 sched 67.2% ret 2536
c [sweep-9-1] 17670655 steps 411 queries 23.22 avg class size
c [sweep-9-1] 4275 decisions 303 SAT calls 73.66 avg env size
c [sweep-9-1] 636 variables remain 8% (7026 retained 92%)
c [decomp-38] removed 382 variables
c [sweep-9-1] removed 382 vars (0 failed, 155 eqs, 169 impls)
c [sweep-9] removed 382 vars in TOTAL (1 rounds, 410 queries)
c [sort-queue-13] sorted 7360 enqueued variables after 595810 conflicts
c [score-dist-13] active 0 (0%), one 7360 (100%), zero 0 (0%)
c [score-dist-13] max exp 1, different 1 (50%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 1737 variables 19.1% (7360 remain 14%)
c [simplification-13] removed 10946 irredundant clauses 18.6% (47918 remain 31%)
c [simplification-13] maximum reduction of 19% = max (19%, 19%)
c [simplification-13] large reduction 19% >= 5% limit
c [simplification-13] next conflict interval 5958 = min (595810/100, 179990)
c [simplification-13] penalized conflict interval 5958 = 1 * 5958
c [simplification-13] hard conflict limit 611768 (soft 601768 + delta 10000)
c [simplification-13] new conflict limit 601768 (hard 611768)
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  179.3    7359    47918    610212   62850   9646 33192    9    14   15  63%   -528   -3   10    8  124%
c 
c [simplification-14] limit 601768 conflicts (hard 611768) hit after 611768 conflicts
c [quatres-10] found 14585 quaternary clauses 28% in total
c [quatres-10-1] removed 41 duplicate quaternary clauses
c [quatres-10-2] added 64 single-self-subsuming ternary resolvents
c [quatres-10-2] added 305 quaternary resolvents
c [ternres-10] limit 60790308 with penalty 0 = 0 + 0
c [ternres-10] all 7359 free variables schedulable
c [ternres-10] 7104 ternary resolvents (8 bin, 7096 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-8] limit 12158061 penalty 0 = 0 + 0
c [gauss-8] extracted 1273 xors of average arity 3.1
c [gauss-8] connected 3963 occurrences of 329 variables (average 12.0)
c [gauss-8] limit 12158061 penalty 0 = 0 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-39] removed 12 variables
c [treelook-4] limit 1519757 penalty 2 = 2 + 0 boost 1
c [treelook-4] scheduled 14694 literals 100%
c [treelook-4] scheduling used 432352 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1519757 penalty 2 = 2 + 0 boost 1
c [treelook-4] used 1530402 steps
c [treelook-4] 14607 literals remain 99%
c [treelook-4] 7346 variables remain to probed next time 100%
c [treelook-4] removed 1 variables, found 1901 hbrs
c [unhide-9] limit 12158061 with penalty 0 = 0 + 0
c [unhide-9-30] 0 units, 8 failed, 3468 tauts, 0 hbrs, 21407 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 511 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 379939426 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 13
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 12
c [cce-4-1] eliminated 3 clauses out of 18 (17%) of length 11
c [cce-4-1] eliminated 8 clauses out of 45 (18%) of length 10
c [cce-4-1] eliminated 26 clauses out of 133 (20%) of length 9
c [cce-4-1] eliminated 56 clauses out of 400 (14%) of length 8
c [cce-4-1] eliminated 131 clauses out of 970 (14%) of length 7
c [cce-4-1] eliminated 616 clauses out of 2505 (25%) of length 6
c [cce-4-1] eliminated 1088 clauses out of 5478 (20%) of length 5
c [cce-4-1] eliminated 2043 clauses out of 10321 (20%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 3973 large clauses in 147823481 steps
c [cce-4-1] allowing another 73911740 steps for small clauses
c [cce-4-1] scheduling 19088 clauses = 11207 binary + 7881 ternary
c [cce-4-1] tried to eliminate 19088 small clauses 100%
c [cce-4-1] eliminated 303 binary clauses 3%
c [cce-4-1] eliminated 1370 ternary clauses 17%
c [cce-4-1] eliminated 1673 small clauses 9%
c [cce-4-1] eliminated 1674 small clauses in 143469005 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 5647 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 58973232 steps for small clauses
c [cce-4-2] scheduling 17419 clauses = 10904 binary + 6515 ternary
c [cce-4-2] tried to eliminate 17419 small clauses 100%
c [cce-4-2] eliminated 4 ternary clauses 0%
c [cce-4-2] eliminated 4 small clauses 0%
c [cce-4-2] eliminated 4 small clauses in 121690667 steps
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 4 covered clauses in round 2
c [cce-4-3] incomplete large round (ATE)
c [cce-4-3] allowing another 57389877 steps for small clauses
c [cce-4-3] scheduling 17415 clauses = 10904 binary + 6511 ternary
c [cce-4-3] tried to eliminate 15538 small clauses 89%
c [cce-4-3] incomplete small round (ATE)
c [cce-4-3] eliminated 0 covered clauses in round 3
c [cce-4] eliminated 5651 covered clauses in TOTAL during 3 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 7344 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 1321 variables 18% in round 1 in 41610987 steps
c [elim-11-1] backward subsumption/strengthening limit 41610900
c [elim-11-1-1] backward checking 3214 touched variables 44%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 12 and strengthened 25 clauses in 9396029 steps
c [elim-11-1] rescheduled 89 variables 1% by backward subsumption
c [elim-11-2] eliminated 10 variables 0% in round 2 in 16719794 steps
c [elim-11-2] backward subsumption/strengthening limit 16719700
c [elim-11-2-1] backward checking 75 touched variables 1%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 3 and strengthened 2 clauses in 3383696 steps
c [elim-11-2] rescheduled 18 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 13330266 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 1331 = 18% variables out of 7344 scheduled
c [bca-9] limit of 10000000 steps and 76177 added (scaled 2)
c [bca-9] 2595 out of 12028 literals actually usable 22%
c [bca-9] added 24 blocked clauses in 53774 steps
c [sweep-10] limit 18237092 penalty 0 = 0 + 0
c [sweep-10-1] 139 pos 32.0% + 295 neg 68.0% = 434 sched 7.2% ret 5579
c [sweep-10-1] 6399997 steps 217 queries 9.97 avg class size
c [sweep-10-1] 1959 decisions 152 SAT calls 61.67 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-41] removed 102 variables
c [sweep-10-1] removed 102 vars (0 failed, 101 eqs, 105 impls)
c [sweep-10-2] 2253 pos 38.1% + 3658 neg 61.9% = 5911 sched 100.0% ret 0
c [sweep-10-2] 12000416 steps 127 queries 138.60 avg class size
c [sweep-10-2] 2200 decisions 123 SAT calls 75.47 avg env size
c [sweep-10-2] 1729 variables remain 29% (4182 retained 71%)
c [decomp-42] removed 17 variables
c [sweep-10-2] removed 17 vars (0 failed, 16 eqs, 12 impls)
c [sweep-10] removed 119 vars in TOTAL (2 rounds, 342 queries)
c [sort-queue-14] sorted 5894 enqueued variables after 611768 conflicts
c [score-dist-14] active 0 (0%), one 5894 (100%), zero 0 (0%)
c [score-dist-14] max exp 1, different 1 (50%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 1465 variables 19.9% (5894 remain 12%)
c [simplification-14] removed 10125 irredundant clauses 21.1% (37793 remain 25%)
c [simplification-14] maximum reduction of 21% = max (20%, 21%)
c [simplification-14] large reduction 21% >= 5% limit
c [simplification-14] next conflict interval 6117 = min (611768/100, 179990)
c [simplification-14] penalized conflict interval 6117 = 1 * 6117
c [simplification-14] hard conflict limit 627885 (soft 617885 + delta 10000)
c [simplification-14] new conflict limit 617885 (hard 627885)
c 
c [simplification-15] limit 617885 conflicts (hard 627885) hit after 627886 conflicts
c [quatres-11] found 11260 quaternary clauses 28% in total
c [quatres-11-1] removed 21 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 51 single-self-subsuming ternary resolvents
c [quatres-11-2] added 240 quaternary resolvents
c [ternres-11] limit 63075699 with penalty 0 = 0 + 0
c [ternres-11] all 5894 free variables schedulable
c [ternres-11] 3098 ternary resolvents (8 bin, 3090 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1971115 penalty 4 = 4 + 0
c [card-5] found 197 at-most-one constraints of average size 3.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1971115 for elimination
c [card-5] 197 out of 197 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-43] removed 1 variables
c [basicprobe-4] limit 315378499 penalty 0 = 0 + 0
c [basicprobe-4-0] 2804 sched 48%, 5 failed, 0 lifted, 13890 hbrs
c [decomp-44] removed 50 variables
c [basicprobe-4-1] 2800 sched 48%, 0 failed, 0 lifted, 1602 hbrs
c [decomp-45] removed 3 variables
c [basicprobe-4-2] 2780 sched 48%, 0 failed, 0 lifted, 138 hbrs
c [basicprobe-4-3] 2779 sched 48%, 0 failed, 0 lifted, 31 hbrs
c [basicprobe-4-4] 2778 sched 48%, 0 failed, 0 lifted, 17 hbrs
c [basicprobe-4-5] 2778 sched 48%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-4-6] 2777 sched 48%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-4-7] 2777 sched 48%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-4-8] 2777 sched 48%, 0 failed, 0 lifted, 19 hbrs
c [basicprobe-4-8] round limit 8 hit
c [basicprobe-4-8] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-4-8] removed 53 variables, found 15721 hbrs
c [bate-3] eliminated 31 asymmetric tautologies during probing
c [unhide-10] limit 12615139 with penalty 0 = 0 + 0
c [unhide-10-41] 0 units, 0 failed, 4307 tauts, 0 hbrs, 25540 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 500 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 5840 variables 100%
c [block-5] limit of 78844624 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 423 blocked clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 5792 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 161 variables 3% in round 1 in 39602243 steps
c [elim-12-1] backward subsumption/strengthening limit 39602200
c [elim-12-1-1] backward checking 699 touched variables 12%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 5 and strengthened 8 clauses in 4098317 steps
c [elim-12-1] rescheduled 38 variables 1% by backward subsumption
c [elim-12-2] eliminated 6 variables 0% in round 2 in 535412 steps
c [elim-12-2] backward subsumption/strengthening limit 535400
c [elim-12-2-1] backward checking 14 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 3 and strengthened 1 clauses in 33447 steps
c [elim-12-2] rescheduled 7 variables 0% by backward subsumption
c [elim-12-3] eliminated 3 variables 0% in round 3 in 59841 steps
c [elim-12-3] backward subsumption/strengthening limit 59800
c [elim-12-3-1] backward checking 138 touched variables 2%
c [elim-12-3-1] incomplete backward checking 123 remain 89%
c [elim-12-3] subsumed 0 and strengthened 0 clauses in 59893 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 170 = 3% variables out of 5792 scheduled
c [bca-10] limit of 10000000 steps and 73351 added (scaled 2)
c [bca-10] 2105 out of 11246 literals actually usable 19%
c [bca-10] added 20 blocked clauses in 65189 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 189227090 penalty 0 = 0 + 0
c [sweep-11-1] 587 pos 37.3% + 986 neg 62.7% = 1573 sched 28.0% ret 4049
c [sweep-11-1] 24204905 steps 297 queries 22.68 avg class size
c [sweep-11-1] 4311 decisions 297 SAT calls 77.51 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-52] removed 65 variables
c [sweep-11-1] removed 65 vars (0 failed, 73 eqs, 39 impls)
c [sweep-11-2] 2124 pos 38.2% + 3433 neg 61.8% = 5557 sched 100.0% ret 0
c [sweep-11-2] 42476662 steps 347 queries 36.63 avg class size
c [sweep-11-2] 6701 decisions 347 SAT calls 85.12 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-53] removed 27 variables
c [sweep-11-2] removed 27 vars (0 failed, 39 eqs, 17 impls)
c [sweep-11-3] 2116 pos 38.3% + 3414 neg 61.7% = 5530 sched 100.0% ret 0
c [sweep-11-3] 41665026 steps 333 queries 53.78 avg class size
c [sweep-11-3] 5864 decisions 333 SAT calls 76.61 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-54] removed 17 variables
c [sweep-11-3] removed 17 vars (0 failed, 33 eqs, 12 impls)
c [sweep-11] removed 109 vars in TOTAL (3 rounds, 974 queries)
c [sort-queue-15] sorted 5513 enqueued variables after 627886 conflicts
c [score-dist-15] active 0 (0%), one 5513 (100%), zero 0 (0%)
c [score-dist-15] max exp 1, different 1 (50%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 381 variables 6.5% (5513 remain 11%)
c [simplification-15] removed 1449 irredundant clauses 3.8% (36344 remain 24%)
c [simplification-15] maximum reduction of 6% = max (6%, 4%)
c [simplification-15] large reduction 6% >= 5% limit
c [simplification-15] next conflict interval 6278 = min (627886/100, 179990)
c [simplification-15] penalized conflict interval 6278 = 1 * 6278
c [simplification-15] hard conflict limit 644164 (soft 634164 + delta 10000)
c [simplification-15] new conflict limit 634164 (hard 644164)
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  212.2    5512    36344    634874   69003  15005 30497    7     8   18  84%   -269   -7    4    8   53%
c i  213.4    5387    36344    638115   71003  15051 30506    6     8   18  83%   -562   -7    5    8   63%
c i  214.0    5182    36344    639728   72154  15077 30515    6     7   18  83%   -576   -7    5    8   59%
c i  214.7    4999    36344    641948   73800  15122 30524    6     7   18  81%   -557   -7    5    8   58%
c i  214.7    4922    36344    641959   73798  15124 30526    6     7   18  81%   -557   -7    5    8   57%
c i  214.7    4583    36344    641963   73798  15125 30527    6     7   18  81%   -557   -7    5    8   57%
c i  214.7    4326    36344    641965   73799  15125 30527    6     7   18  81%   -557   -7    5    8   56%
c 0  214.7    4184    36344    641965   73799  15125 30527    6     7   18  81%   -557   -7    5    8   56%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 197 basic ate = 135 trn 69% + 62 lrg 31% in 3 updates
c bcas: 10 count, 158 added (172 skipped), 634782 steps
c bkwd: tried 195938 clauses, 391337 lits, 2.00 lits/clause
c bkwd: checked 40410776 occs, 206.24 occs/clause, 103.26 occs/lit
c bkwd: subsumed 1 binary, 42 ternary, 93 large
c bkwd: strengthened 1 binary, 2 ternary (100% self), 563 large (0% self)
c blkd: 5 bces, 1635 removed, 1624235 resolutions, 4110707 steps
c blkd: 1000 blocking literals 1%, 73 pure
c bump: 655515 bumped seen, 56793655 lits 86.6 on average
c card: 5 count, 0 units, 99 am1, 13577024 steps
c card: 32 rescheduled, 299 eliminated, 10530 resolved, 5908 subsumed
c card: 528 at-most-one constraints found, average size 3.01
c card: 528 at-most-one constraints used 100%, average size 3.01
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: 4 cces, 6803 eliminated, 6724 ate 99%, 79 abce 1%
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: 507792 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 104 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 54 decompositions, 3594 equivalent 7%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 2172986 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 12 elims, 40799 eliminated 80%, 120 pure 0%
c elms: 28 rounds, 2.3 rounds/bve
c elms: 38709 small 95%, 1897 large 5%
c elms: 50712 tried small, 38709 succeeded 76%, 12003 failed 24%
c elms: 4275 subsumed, 5634 strengthened, 1198 blocked
c elms: 2979509 copies, 3888868 resolutions, 1021258 ipos
c elms: 5513594 subchks, 5510857 strchks
c gaus: 8 extractions, 12003 extracted, 3.0 size, 4 max
c gaus: exported 1 units, 32 binary and 6 ternary equations
c gaus: 0 gc, 38912376 steps, 19456188 extr 50%, 357378 elim 1%
c glue: 8.9 orig avg, 8.9 real avg, 2.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 115007 = 14687 simple 13% + 96671 trn 84% + 3649 lrg 3%, 901 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 655515 clauses, 21.8 length
c lrnd: 14308260 lits = 29980159 orig - 15671899 removed 52%
c lrnd: 123004 uips 19%, 489886 flips 75%
c mins: 646625 mins 99%, 847 bin 0%, 8043 size 1%
c mins: 44104209 poisoned searches, 3345464 hits, 8% hit rate
c mins: 70050841 used twice searches, 2269105 hits, 3% hit rate
c move: moved 4407, 865 bin 20%, 3542 trn 80%
c otfs: 1991 driving 30%, 4613 restarting 70%
c otfs: str 6604, 6394 red 97%, 210 irr 3%
c otfs: str 6604, 0 bin 0%, 398 trn 6%, 6206 lrg 94%
c otfs: sub 146, 131 red 90%, 15 irr 10%
c otfs: sub 146, 0 bin 0%, 38 trn 26%, 108 lrg 74%
c phas: 1 computed, 12359 set, 3458 pos (28%), 8901 neg (72%)
c prbs: 4 basic, 90605 probed, 55 failed, 4 lifted
c prbs: 4 simple, 144757 probed, 89 failed, 3846 eqs
c prbs: 4 treelook, 197 probed, 1 failed, 0 lifted
c prom: 141438 locked 9% out of 1661509 tried
c prps: 357480766 props, 155 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 11 count, 2718 quat, 904 self1, 18 self2, 257 dup
c queu: 15 sorted, 2172986 next (173 steps 0.00)
c queu: 56995723 enq (0 steps 0.00), 56793655 deq 100%
c redc: 20883 clauses 12%, 173968 tried 27%, 9 sat 0%
c redc: 27939 lits 1%, 2073642 tried 7%, 9 sat 0%
c redc: 773 times jump level reduced, 2.9 levels on average
c reds: 13 count, 49381.9 conflicts per reduce
c reds: 0 memlim 0%, 13 arith 100%
c reds: 364015 collected 85%, 63120 retired 15%
c rmbd: 18835 removed, 17686 red 94%
c rsts: 22547 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 15 count, 13 confs 87%, 0 vars 0%
c simp: 1 its 7%, 1 bin 7%, 0 trns 0%
c subl: 655515 count (243732 tried 0.4), 59308 sub out of 649484 (9.1%)
c swps: 11 count, 16 rounds, 3534 queries (220.9/round)
c swps: 3138 sat calls, 665 unsat (5.0% success rate)
c swps: 50932 decisions 16.2, 15541 conflicts 5.0
c swps; 76.0 avg class size, 74.9 avg environment size
c swps: 0 failed, 859 impls, 1051 equivs
c swp0: 1172 type 0 queries, 672 unsat (57.3%), 894 sat (76.3%)
c swp1: 2362 type 1 queries, 1921 unsat (81.3%), 1589 sat (67.3%)
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: 5657404 calls to obtain time
c tops: 2531 fixed 5%, 105 its, 6113.95 confs/it
c trds: 11 transitive reductions, 6054 removed, 14 failed
c trds: 71089 nodes, 134436 edges, 21264900 steps
c trim: 340435 words, 1.3 MB
c trnr: 11 count, 181 bin, 27536 trn, 281146172 steps
c unhd: 10 count, 41 rounds, 51186698 steps
c unhd: 782 non-trivial sccs of average size 2.3
c unhd: 95 units, 95 bin, 0 trn, 0 lrg
c unhd: 420 failed, 418 stamp, 0 lits, 1 bin, 0 trn, 0 lrg
c unhd: 38801 tauts, 688 bin 2%, 5712 trn 15%, 9203 lrg 24%
c unhd: 38801 tauts, 23198 stamp 60%, 36748 red 95%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 295104 str, 95 bin 0%, 1026 trn 0%, 293983 lrg 100%, 289361 red 98%
c vars: 4184 remaining 8% and 46924 removed 92% out of 51108
c vars: 2531 fixed 5%, 40799 eliminated 80%, 3594 equivalent 7%
c vsts: 6913526810 visits, 95% srch, 5% simp, 0% lkhd
c vsts: 19.5 search visits per propagation, 10224.9 per conflict
c wchs: 1989373309 pushed, 16063154 enlarged, 191 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         652202        364015         63120      24241979       7564207        325107
c 
c  0 0         74569  11      6355   2         0   0  16727727  69   4469142  59    150087  46     1.7
c  1 5         52404   8     22302   6      6493  10   3181401  13<  1107418  15<    45511  14<    0.6
c  2 6        212157  33<   125163  34     16028  25   3463612  14   1437433  19     80536  25     2.3
c  3 9        229539  35    155523  43<    21990  35<   744578   3    466090   6     40817  13     2.2
c  4 14        71568  11     47784  13     14841  24    108946   0     75054   1      7393   2     1.4
c  5 21        11111   2      6424   2      3475   6     14578   0      8464   0       702   0     0.5
c  6 30          815   0       446   0       278   0      1087   0       579   0        57   0     0.1
c  7 41           39   0        18   0        15   0        50   0        27   0         4   0     0.0
c 
c avg                  2.3           2.7           2.9           0.5           0.8           1.1
c std                  1.2           0.9           1.1           0.9           1.0           1.2
c 
c   12.074   6% cce
c    8.221   4% elim
c    7.868   4% sweep
c    7.374   3% probe
c    6.504   3% unhide
c    2.481   1% bump
c    1.742   1% ternres
c    1.409   1% transred
c    1.405   1% decide
c 
c    3.105 < 1% rest (below)
c 
c    1.159   1% gauss
c    0.850   0% quatres
c    0.501   0% block
c    0.415   0% bca
c    0.180   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.560   1% preprocessing     3%
c   48.141  22% inprocessing     97%
c ==================================
c   49.702  23% simplifying
c  165.006  77% search
c ==================================
c  214.708 100% all
c 
c        641965 conflicts,        2989.9 confs/sec
c          3397 ternaries,         189.0 confs/ternary
c           693 binaries,          926.4 confs/binary
c           105 iterations,       6114.0 confs/iteration
c 
c            13 reductions,          0.1 redus/sec,  49381.9 confs/reduction
c         22547 restarts,          105.0 rests/sec,     28.5 confs/restart
c       2172986 decisions,       10120.6 decis/sec,      3.4 decis/conflict
c     357480766 propagations,  1664960.0 props/sec,    164.5 props/decision
c 
c 214.7 seconds, 39.1 MB
c launch: done
