c launch: /data/cnf/sc2014/app/manol-pipe-g10bid_i.cnf.bz2
c host: atom04
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/manol-pipe-g10bid_i.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/manol-pipe-g10bid_i.cnf.bz2
c no embedded options
c found 'p cnf 266405 792175' header
c read 266405 variables, 792175 clauses, 1848407 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=6
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 266404 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] AVG (--score=6)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  266404   792174         0       0      0     0    0     0   44   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 1 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] 1 out of 1 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 1 at-most-one constraints, 1 used 100%
c [card-1] exported 1 binary clauses, 1.0 per/constraint
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 266404 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 7402 variables
c [simpleprobe-1] 91801 variables remain 35% (167201 retained 65%)
c [simpleprobe-1] removed 7402 variables, found 953 hbrs, 86 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 83 failed, 201 tauts, 0 hbrs, 171 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 257663 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 64530 not tried 25% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 193123 = 75% variables out of 257663 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 313684 negative 95.8% of 327495 except 13811 4.2%
c [phase-count-1] 311324 positive 95.1% of 327495 except 16171 4.9%
c [phase-1] phase bias: 23065 positive 36%, 41475 negative 64%
c [sort-queue-1] sorted 64540 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 64540 (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 201864 variables 75.8% (64540 remain 24%)
c [simplification-1] removed 464679 irredundant clauses 58.7% (327495 remain 41%)
c [simplification-1] maximum reduction of 76% = max (76%, 59%)
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    5.2   64539   327495        20      13      1    55    0     0   38   4%      0    0    0    0 24521%
c i    5.2   64527   327495        24      14      2    56    0     0   38   5%      0    0    0    0 24217%
c i    5.3   64524   327495       227     161     22    69    0     4   38   6%      0    4    3    0 18093%
c i    5.3   64512   327495       238     167     25    70    0     5   38   6%      0    5    3    0 17524%
c i    5.5   64494   327495       676     499     57    71    1    22   39   5%      1   21    8    0 11599%
c i    5.6   64424   327495       799     593     68    72    1    28   39   5%      1   28   11    0 10973%
c i    5.6   64401   327495       897     666     71    73    2    29   39   6%      1   29   13    0 10615%
c 
c [simplification-2] limit 1002 conflicts (hard 11000) hit after 1002 conflicts
c [decomp-3] removed 335 variables
c [simpleprobe-2] 22499 schedulable variables 35%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 99 variables
c [simpleprobe-2] 22566 variables remain 35% (41540 retained 65%)
c [simpleprobe-2] removed 99 variables, found 77 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 37205 literals 29%
c [treelook-1] scheduling used 300002 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300492 steps
c [treelook-1] 37123 literals remain 29%
c [treelook-1] 32448 variables remain to probed next time 51%
c [decomp-5] removed 1 variables
c [treelook-1] removed 1 variables, found 1738 hbrs
c [basicprobe-1] limit 2596856 based on 324607 irredundant clauses
c [basicprobe-1-0] 34591 probes remain 55% after last round
c [basicprobe-1-0] 562 units = 336 failed (60%) + 226 lifted (40%)
c [basicprobe-1-0] removed 1583 variables, found 3465 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 32 units, 85 failed, 495 tauts, 0 hbrs, 2300 literals
c [elim-2] 62199 variables 100% will be scheduled this time
c [elim-2] scheduled 62199 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 15181 not tried 24% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 26936 = 43% variables out of 62199 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 250728 negative 97.1% of 258203 except 7475 2.9%
c [phase-count-2] 249273 positive 96.5% of 258203 except 8930 3.5%
c [phase-2] phase bias: 17 positive 19%, 73 negative 81%
c [sort-queue-2] sorted 30710 enqueued variables after 1002 conflicts
c [score-dist-2] active 4566 (13%), one 0 (0%), zero 30710 (87%)
c [score-dist-2] max exp 511, different 12 (2%)
c [score-dist-2] median active exp 510, avg 509.8
c [simplification-2] removed 29119 variables 45.2% (35276 remain 13%)
c [simplification-2] removed 69292 irredundant clauses 21.2% (258203 remain 33%)
c [simplification-2] maximum reduction of 45% = max (45%, 21%)
c [simplification-2] large reduction 45% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13002 (soft 3002 + delta 10000)
c [simplification-2] new conflict limit 3002 (hard 13002)
c 
c [simplification-3] limit 3002 conflicts (hard 13002) hit after 3002 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 41 at-most-one constraints of average size 3.0
c [card-2] found 2 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 43 out of 43 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 90 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 20178 literals 29%
c [treelook-2] scheduling used 300007 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 319019 steps
c [treelook-2] 20043 literals remain 29%
c [treelook-2] 12340 variables remain to probed next time 35%
c [decomp-7] removed 14 variables
c [treelook-2] removed 62 variables, found 80 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 4 units, 20 failed, 1046 tauts, 0 hbrs, 4388 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 35063 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 4034 not tried 12% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1481 = 4% variables out of 35063 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 243921 negative 97.1% of 251140 except 7219 2.9%
c [phase-count-3] 243035 positive 96.8% of 251140 except 8105 3.2%
c [phase-3] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-3] sorted 25795 enqueued variables after 3002 conflicts
c [score-dist-3] active 7787 (23%), one 0 (0%), zero 25795 (77%)
c [score-dist-3] max exp 513, different 13 (3%)
c [score-dist-3] median active exp 512, avg 511.6
c [simplification-3] removed 1694 variables 4.8% (33582 remain 13%)
c [simplification-3] removed 7062 irredundant clauses 2.7% (251140 remain 32%)
c [simplification-3] maximum reduction of 5% = max (5%, 3%)
c [simplification-3] large reduction 5% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 15002 (soft 5002 + delta 10000)
c [simplification-3] new conflict limit 5002 (hard 15002)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   11.1   33581   251140      3837    2152    136  1204    6    90   38   7%     30   87   12    1 2247%
c 
c [simplification-4] limit 5002 conflicts (hard 15002) hit after 5003 conflicts
c [decomp-8] removed 15 variables
c [basicprobe-2] limit 2056989 penalty 0 = 0 + 0
c [basicprobe-2-0] 2201 probes remain 7% after last round
c [basicprobe-2-0] 146 units = 141 failed (97%) + 5 lifted (3%)
c [basicprobe-2-0] removed 458 variables, found 1609 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 17 failed, 117 tauts, 0 hbrs, 3687 literals
c [elim-4] 3882 variables 12% will be scheduled this time
c [elim-4] scheduled 3882 variables 12%
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 101173525 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 3 = 0% variables out of 3882 scheduled
c [elim-4] 3 < 1/100 * 3882 = 38 considered unsuccessful
c [sort-queue-4] sorted 23299 enqueued variables after 5003 conflicts
c [score-dist-4] active 9784 (30%), one 0 (0%), zero 23299 (70%)
c [score-dist-4] max exp 514, different 14 (3%)
c [score-dist-4] median active exp 513, avg 512.4
c [simplification-4] removed 498 variables 1.5% (33083 remain 12%)
c [simplification-4] removed 9517 irredundant clauses 3.8% (241623 remain 31%)
c [simplification-4] maximum reduction of 4% = max (1%, 4%)
c [simplification-4] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-4] new conflict interval 4000
c [simplification-4] penalized conflict interval 4000 = 1 * 4000
c [simplification-4] hard conflict limit 19003 (soft 9003 + delta 10000)
c [simplification-4] new conflict limit 9003 (hard 19003)
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   13.4   33082   241623      5221    3042    212  1873    7   117   37   6%     17  112    7    1 1003%
c i   14.0   33081   241622      8316    5277    333  1894    8   130   37   6%     32  120   11    1  977%
c 
c [simplification-5] limit 9003 conflicts (hard 19003) hit after 9003 conflicts
c [quatres-1] found 28581 quaternary clauses 24% in total
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 289 single-self-subsuming ternary resolvents
c [quatres-1-2] added 8369 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 33079 free variables schedulable
c [ternres-1] 10790 ternary resolvents (181 bin, 10609 trn)
c [ternres-1] 2 variables remain 0% (33077 retained 100%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 18633 xors of average arity 3.0
c [gauss-1] connected 55721 occurrences of 5516 variables (average 10.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 159 variables
c [simpleprobe-3] 11539 schedulable variables 35%
c [simpleprobe-3] limit 2615078 penalty 0 = 0 + 0
c [simpleprobe-3] 11252 variables remain 34% (21668 retained 66%)
c [simpleprobe-3] removed 0 variables, found 58 hbrs, 0 units
c [unhide-5] limit 130753 with penalty 0 = 0 + 0
c [unhide-5-5] 4 units, 11 failed, 206 tauts, 0 hbrs, 1933 literals
c [transred-1] limit 653769 with penalty 0 = 0 + 0
c [transred-1] removed 189 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 32851 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 6158 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 31
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 27
c [cce-1-1] eliminated 3 clauses out of 56 (5%) of length 23
c [cce-1-1] eliminated 4 clauses out of 72 (6%) of length 22
c [cce-1-1] eliminated 9 clauses out of 95 (9%) of length 21
c [cce-1-1] eliminated 19 clauses out of 158 (12%) of length 20
c [cce-1-1] eliminated 23 clauses out of 179 (13%) of length 19
c [cce-1-1] eliminated 25 clauses out of 253 (10%) of length 18
c [cce-1-1] eliminated 19 clauses out of 360 (5%) of length 17
c [cce-1-1] eliminated 49 clauses out of 425 (12%) of length 16
c [cce-1-1] eliminated 46 clauses out of 394 (12%) of length 15
c [cce-1-1] eliminated 88 clauses out of 588 (15%) of length 14
c [cce-1-1] eliminated 88 clauses out of 671 (13%) of length 13
c [cce-1-1] eliminated 135 clauses out of 1025 (13%) of length 12
c [cce-1-1] eliminated 304 clauses out of 1964 (15%) of length 11
c [cce-1-1] eliminated 338 clauses out of 2435 (14%) of length 10
c [cce-1-1] eliminated 728 clauses out of 4346 (17%) of length 9
c [cce-1-1] eliminated 51 clauses out of 7806 (1%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1931 large clauses in 30000050 steps
c [cce-1-1] allowing another 15000025 steps for small clauses
c [cce-1-1] scheduling 104603 clauses = 28318 binary + 76285 ternary
c [cce-1-1] tried to eliminate 8491 small clauses 8%
c [cce-1-1] eliminated 91 binary clauses 0%
c [cce-1-1] eliminated 106 ternary clauses 0%
c [cce-1-1] eliminated 197 small clauses 0%
c [cce-1-1] eliminated 197 small clauses in 30000036 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2128 covered clauses in round 1
c [cce-1] eliminated 2128 covered clauses in TOTAL during 1 rounds
c [cce-1] 2128 < 1/100 * 233243 = 2332 considered unsuccessful
c [bca-1] limit of 10000000 steps and 462730 added (scaled 2)
c [bca-1] 49395 out of 65238 literals actually usable 76%
c [bca-1] added 114 blocked clauses in 160448 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 12619 pos 38.7% + 19999 neg 61.3% = 32618 sched 100.0% ret 0
c [sweep-1-1] 1003984 steps 109 queries 6460.66 avg class size
c [sweep-1-1] 3518 decisions 108 SAT calls 54.74 avg env size
c [sweep-1-1] 30899 variables remain 95% (1683 retained 5%)
c [decomp-11] removed 71 variables
c [sweep-1-1] removed 71 vars (0 failed, 1 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 71 vars in TOTAL (1 rounds, 108 queries)
c [sort-queue-5] sorted 20705 enqueued variables after 9003 conflicts
c [score-dist-5] active 11842 (36%), one 0 (0%), zero 20705 (64%)
c [score-dist-5] max exp 514, different 14 (3%)
c [score-dist-5] median active exp 514, avg 513.2
c [simplification-5] removed 532 variables 1.6% (32547 remain 12%)
c [simplification-5] removed 11048 irredundant clauses 4.6% (230574 remain 29%)
c [simplification-5] maximum reduction of 5% = max (2%, 5%)
c [simplification-5] large reduction 5% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 21003 (soft 11003 + delta 10000)
c [simplification-5] new conflict limit 11003 (hard 21003)
c 
c [simplification-6] limit 11003 conflicts (hard 21003) hit after 11004 conflicts
c [quatres-2] found 36197 quaternary clauses 29% in total
c [quatres-2-2] added 154 single-self-subsuming ternary resolvents
c [quatres-2-2] added 4635 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 1 schedulable variables 0%
c [ternres-2] 889 ternary resolvents (63 bin, 826 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 96 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 96 out of 96 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 2 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 15891 literals 24%
c [treelook-3] scheduling used 300062 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 309779 steps
c [treelook-3] 15844 literals remain 24%
c [treelook-3] 8754 variables remain to probed next time 27%
c [treelook-3] removed 3 variables, found 86 hbrs
c [unhide-6] limit 175063 with penalty 0 = 0 + 0
c [unhide-6-6] 6 units, 22 failed, 973 tauts, 0 hbrs, 2216 literals
c [transred-2] limit 875316 with penalty 0 = 0 + 0
c [transred-2] removed 223 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 32500 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 1419 blocked clauses
c [block-2] 1419 < 1/100 * 230340 = 2303 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 32185 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 6345 not tried 20% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1616 = 5% variables out of 32185 scheduled
c [bca-2] limit of 10000000 steps and 452207 added (scaled 2)
c [bca-2] 44984 out of 61140 literals actually usable 74%
c [bca-2] added 39 blocked clauses in 153820 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 10968 pos 37.9% + 17974 neg 62.1% = 28942 sched 94.7% ret 1627
c [sweep-2-1] 1002221 steps 126 queries 6379.22 avg class size
c [sweep-2-1] 3756 decisions 123 SAT calls 46.46 avg env size
c [sweep-2-1] 27422 variables remain 90% (3036 retained 10%)
c [decomp-14] removed 141 variables
c [sweep-2-1] removed 141 vars (0 failed, 6 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 141 vars in TOTAL (1 rounds, 125 queries)
c [sort-queue-6] sorted 17409 enqueued variables after 11004 conflicts
c [score-dist-6] active 13019 (43%), one 0 (0%), zero 17409 (57%)
c [score-dist-6] max exp 515, different 13 (3%)
c [score-dist-6] median active exp 514, avg 513.8
c [simplification-6] removed 2119 variables 6.5% (30428 remain 11%)
c [simplification-6] removed 7386 irredundant clauses 3.2% (223188 remain 28%)
c [simplification-6] maximum reduction of 7% = max (7%, 3%)
c [simplification-6] large reduction 7% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 23004 (soft 13004 + delta 10000)
c [simplification-6] new conflict limit 13004 (hard 23004)
c 
c [simplification-7] limit 13004 conflicts (hard 23004) hit after 13006 conflicts
c [quatres-3] found 36975 quaternary clauses 29% in total
c [quatres-3-1] added 3 double-self-subsuming ternary resolvents
c [quatres-3-2] added 88 single-self-subsuming ternary resolvents
c [quatres-3-2] added 2850 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 30428 free variables schedulable
c [ternres-3] 526 ternary resolvents (20 bin, 506 trn)
c [ternres-3] 18320 variables remain 60% (12108 retained 40%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 8182 xors of average arity 3.0
c [gauss-2] connected 24543 occurrences of 4665 variables (average 5.3)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 5 variables
c [basicprobe-3] limit 5213960 penalty 0 = 0 + 0
c [basicprobe-3-0] 2525 sched 8%, 37 failed, 0 lifted, 448 hbrs
c [decomp-16] removed 96 variables
c [basicprobe-3-1] 16136 sched 54%, 83 failed, 22 lifted, 686 hbrs
c [decomp-17] removed 217 variables
c [basicprobe-3-2] 15909 sched 53%, 4 failed, 0 lifted, 105 hbrs
c [decomp-18] removed 14 variables
c [basicprobe-3-3] 12565 probes remain 42% after last round
c [basicprobe-3-3] 146 units = 124 failed (85%) + 22 lifted (15%)
c [basicprobe-3-3] removed 327 variables, found 1239 hbrs
c [bate-1] eliminated 683 asymmetric tautologies during probing
c [unhide-7] limit 208558 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 0 failed, 314 tauts, 0 hbrs, 1470 literals
c [transred-3] limit 1042792 with penalty 0 = 0 + 0
c [transred-3] removed 164 transitive binary clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 29
c [cce-2-1] eliminated 1 clauses out of 4 (25%) of length 27
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 26
c [cce-2-1] eliminated 1 clauses out of 31 (3%) of length 23
c [cce-2-1] eliminated 2 clauses out of 58 (3%) of length 22
c [cce-2-1] eliminated 1 clauses out of 55 (2%) of length 21
c [cce-2-1] eliminated 6 clauses out of 167 (4%) of length 19
c [cce-2-1] eliminated 8 clauses out of 266 (3%) of length 18
c [cce-2-1] eliminated 8 clauses out of 348 (2%) of length 17
c [cce-2-1] eliminated 32 clauses out of 393 (8%) of length 16
c [cce-2-1] eliminated 31 clauses out of 456 (7%) of length 15
c [cce-2-1] eliminated 34 clauses out of 623 (5%) of length 14
c [cce-2-1] eliminated 84 clauses out of 713 (12%) of length 13
c [cce-2-1] eliminated 117 clauses out of 1210 (10%) of length 12
c [cce-2-1] eliminated 96 clauses out of 1845 (5%) of length 11
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 423 large clauses in 15000349 steps
c [cce-2-1] allowing another 7500174 steps for small clauses
c [cce-2-1] scheduling 96973 clauses = 25138 binary + 71835 ternary
c [cce-2-1] tried to eliminate 10311 small clauses 11%
c [cce-2-1] eliminated 30 binary clauses 0%
c [cce-2-1] eliminated 74 ternary clauses 0%
c [cce-2-1] eliminated 104 small clauses 0%
c [cce-2-1] eliminated 104 small clauses in 15001183 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 527 covered clauses in round 1
c [cce-2] eliminated 527 covered clauses in TOTAL during 1 rounds
c [cce-2] 527 < 1/100 * 218198 = 2181 considered unsuccessful
c [elim-6] 6131 variables 20% will be scheduled this time
c [elim-6] scheduled 6131 variables 20%
c [elim-6] limit of 20855840 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 2182 not tried 7% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 8 = 0% variables out of 6131 scheduled
c [elim-6] 8 < 1/100 * 6131 = 61 considered unsuccessful
c [bca-3] limit of 10000000 steps and 435334 added (scaled 2)
c [bca-3] 42618 out of 60178 literals actually usable 71%
c [bca-3] added 11 blocked clauses in 148523 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 11415 pos 42.0% + 15738 neg 58.0% = 27153 sched 90.2% ret 2935
c [sweep-3-1] 1004859 steps 145 queries 4815.17 avg class size
c [sweep-3-1] 3453 decisions 144 SAT calls 40.47 avg env size
c [sweep-3-1] 25875 variables remain 86% (4213 retained 14%)
c [decomp-19] removed 4 variables
c [sweep-3-1] removed 4 vars (0 failed, 2 eqs, 1 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 4 vars in TOTAL (1 rounds, 144 queries)
c [sort-queue-7] sorted 16606 enqueued variables after 13006 conflicts
c [score-dist-7] active 13478 (45%), one 0 (0%), zero 16606 (55%)
c [score-dist-7] max exp 515, different 13 (3%)
c [score-dist-7] median active exp 514, avg 514.0
c [simplification-7] removed 344 variables 1.1% (30084 remain 11%)
c [simplification-7] removed 5814 irredundant clauses 2.6% (217374 remain 27%)
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 9000
c [simplification-7] penalized conflict interval 9000 = 1 * 9000
c [simplification-7] hard conflict limit 32006 (soft 22006 + delta 10000)
c [simplification-7] new conflict limit 22006 (hard 32006)
c 
c [simplification-8] limit 22006 conflicts (hard 32006) hit after 22006 conflicts
c [quatres-4] found 39253 quaternary clauses 31% in total
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 57 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1649 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 18096 schedulable variables 60%
c [ternres-4] 644 ternary resolvents (22 bin, 622 trn)
c [ternres-4] 6615 variables remain 22% (23469 retained 78%)
c [decomp-20] removed 10 variables
c [transred-4] limit 1749086 with penalty 0 = 0 + 0
c [transred-4] removed 121 transitive binary clauses
c [transred-4] found 1 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 30073 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 1650 blocked clauses
c [block-3] 1650 < 1/100 * 217301 = 2173 considered unsuccessful
c [bca-4] limit of 10000000 steps and 431874 added (scaled 2)
c [bca-4] 39796 out of 59640 literals actually usable 67%
c [bca-4] added 1 blocked clauses in 148104 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 10705 pos 41.7% + 14946 neg 58.3% = 25651 sched 86.0% ret 4168
c [sweep-4-1] 1062931 steps 95 queries 5352.46 avg class size
c [sweep-4-1] 2828 decisions 93 SAT calls 50.51 avg env size
c [sweep-4-1] 24653 variables remain 83% (5166 retained 17%)
c [decomp-21] removed 3 variables
c [sweep-4-1] removed 3 vars (0 failed, 5 eqs, 2 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 3 vars in TOTAL (1 rounds, 94 queries)
c [sort-queue-8] sorted 14942 enqueued variables after 22006 conflicts
c [score-dist-8] active 14874 (50%), one 0 (0%), zero 14942 (50%)
c [score-dist-8] max exp 516, different 14 (3%)
c [score-dist-8] median active exp 515, avg 514.8
c [simplification-8] removed 268 variables 0.9% (29816 remain 11%)
c [simplification-8] removed 1744 irredundant clauses 0.8% (215630 remain 27%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-8] new conflict interval 19000
c [simplification-8] penalized conflict interval 19000 = 1 * 19000
c [simplification-8] hard conflict limit 51006 (soft 41006 + delta 10000)
c [simplification-8] new conflict limit 41006 (hard 51006)
c 
c [simplification-9] limit 41006 conflicts (hard 51006) hit after 41007 conflicts
c [quatres-5] found 41367 quaternary clauses 31% in total
c [quatres-5-1] removed 15 duplicate quaternary clauses
c [quatres-5-1] added 3 double-self-subsuming ternary resolvents
c [quatres-5-2] added 28 single-self-subsuming ternary resolvents
c [quatres-5-2] added 644 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] 6557 schedulable variables 22%
c [ternres-5] 1325 ternary resolvents (76 bin, 1249 trn)
c [ternres-5] 20 variables remain 0% (29796 retained 100%)
c [decomp-22] removed 16 variables
c [simpleprobe-4] 10173 schedulable variables 34%
c [simpleprobe-4] limit 6388954 penalty 1 = 1 + 0
c [simpleprobe-4] 9954 variables remain 33% (19846 retained 67%)
c [simpleprobe-4] removed 0 variables, found 53 hbrs, 0 units
c [unhide-8] limit 319447 with penalty 1 = 1 + 0
c [unhide-8-8] 0 units, 1 failed, 1128 tauts, 0 hbrs, 15241 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 125 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 29799 variables 100%
c [elim-7] limit of 31944774 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 2037 not tried 7% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 716 = 2% variables out of 29799 scheduled
c [bca-5] limit of 10000000 steps and 428688 added (scaled 2)
c [bca-5] 36345 out of 58168 literals actually usable 62%
c [bca-5] added 5 blocked clauses in 151215 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 10957 pos 45.6% + 13050 neg 54.4% = 24007 sched 82.5% ret 5076
c [sweep-5-1] 10002389 steps 1454 queries 1135.36 avg class size
c [sweep-5-1] 31438 decisions 1443 SAT calls 32.50 avg env size
c [sweep-5-1] 10455 variables remain 36% (18622 retained 64%)
c [decomp-24] removed 30 variables
c [sweep-5-1] removed 30 vars (0 failed, 19 eqs, 12 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 30 vars in TOTAL (1 rounds, 1453 queries)
c [sort-queue-9] sorted 12389 enqueued variables after 41007 conflicts
c [score-dist-9] active 16664 (57%), one 0 (0%), zero 12389 (43%)
c [score-dist-9] max exp 517, different 12 (2%)
c [score-dist-9] median active exp 516, avg 515.7
c [simplification-9] removed 763 variables 2.6% (29053 remain 11%)
c [simplification-9] removed 1845 irredundant clauses 0.9% (213785 remain 27%)
c [simplification-9] maximum reduction of 3% = max (3%, 1%)
c [simplification-9] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-9] new conflict interval 24000
c [simplification-9] penalized conflict interval 24000 = 1 * 24000
c [simplification-9] hard conflict limit 77007 (soft 65007 + delta 12000)
c [simplification-9] new conflict limit 65007 (hard 77007)
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.0   29052   213785     44845   44833  11478  2400   10   120   42   8%    427   62    9    5  206%
c 
c [simplification-10] limit 65007 conflicts (hard 77007) hit after 65007 conflicts
c [quatres-6] found 40715 quaternary clauses 30% in total
c [quatres-6-1] removed 3 duplicate quaternary clauses
c [quatres-6-1] added 1 double-self-subsuming ternary resolvents
c [quatres-6-2] added 75 single-self-subsuming ternary resolvents
c [quatres-6-2] added 647 quaternary resolvents
c [ternres-6] limit 5255345 with penalty 0 = 0 + 0
c [ternres-6] 20 schedulable variables 0%
c [ternres-6] 962 ternary resolvents (37 bin, 925 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 328459 penalty 3 = 3 + 0
c [card-4] found 84 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 328459 for elimination
c [card-4] 84 out of 84 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 3963 xors of average arity 3.0
c [gauss-3] connected 11888 occurrences of 2691 variables (average 4.4)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-25] removed 4 variables
c [treelook-4] limit 525534 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 18682 literals 32%
c [treelook-4] scheduling used 525545 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 525534 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 540257 steps
c [treelook-4] 18345 literals remain 32%
c [treelook-4] 7458 variables remain to probed next time 26%
c [decomp-26] removed 1 variables
c [treelook-4] removed 1 variables, found 271 hbrs
c [unhide-9] limit 1051069 with penalty 0 = 0 + 0
c [unhide-9-9] 0 units, 1 failed, 373 tauts, 0 hbrs, 9832 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 151 transitive binary clauses
c [cce-3] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 31
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 28
c [cce-3-1] eliminated 3 clauses out of 9 (33%) of length 27
c [cce-3-1] eliminated 1 clauses out of 13 (8%) of length 25
c [cce-3-1] eliminated 9 clauses out of 35 (26%) of length 23
c [cce-3-1] eliminated 1 clauses out of 63 (2%) of length 22
c [cce-3-1] eliminated 2 clauses out of 64 (3%) of length 21
c [cce-3-1] eliminated 1 clauses out of 147 (1%) of length 20
c [cce-3-1] eliminated 11 clauses out of 193 (6%) of length 19
c [cce-3-1] eliminated 7 clauses out of 290 (2%) of length 18
c [cce-3-1] eliminated 16 clauses out of 381 (4%) of length 17
c [cce-3-1] eliminated 30 clauses out of 418 (7%) of length 16
c [cce-3-1] eliminated 14 clauses out of 495 (3%) of length 15
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 99 large clauses in 7500001 steps
c [cce-3-1] allowing another 3750000 steps for small clauses
c [cce-3-1] scheduling 94174 clauses = 24350 binary + 69824 ternary
c [cce-3-1] tried to eliminate 3602 small clauses 4%
c [cce-3-1] eliminated 21 binary clauses 0%
c [cce-3-1] eliminated 47 ternary clauses 0%
c [cce-3-1] eliminated 68 small clauses 0%
c [cce-3-1] eliminated 103 small clauses in 7500006 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 202 covered clauses in round 1
c [cce-3] eliminated 202 covered clauses in TOTAL during 1 rounds
c [cce-3] 202 < 1/100 * 213461 = 2134 considered unsuccessful
c [elim-8] 1989 variables 7% will be scheduled this time
c [elim-8] scheduled 1989 variables 7%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2102138180 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 92245343 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 1989 scheduled
c [bca-6] limit of 10000000 steps and 423971 added (scaled 2)
c [bca-6] 34113 out of 58088 literals actually usable 59%
c [bca-6] added 2 blocked clauses in 163669 steps
c [sweep-6] limit 1576603 penalty 0 = 0 + 0
c [sweep-6-1] 4951 pos 47.4% + 5503 neg 52.6% = 10454 sched 36.0% ret 18589
c [sweep-6-1] 1578107 steps 247 queries 2608.58 avg class size
c [sweep-6-1] 5355 decisions 240 SAT calls 33.30 avg env size
c [sweep-6-1] 9853 variables remain 34% (19190 retained 66%)
c [decomp-27] removed 11 variables
c [sweep-6-1] removed 11 vars (0 failed, 9 eqs, 9 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 11 vars in TOTAL (1 rounds, 246 queries)
c [sort-queue-10] sorted 11643 enqueued variables after 65007 conflicts
c [score-dist-10] active 17389 (60%), one 0 (0%), zero 11643 (40%)
c [score-dist-10] max exp 517, different 12 (2%)
c [score-dist-10] median active exp 517, avg 516.2
c [simplification-10] removed 17 variables 0.1% (29032 remain 11%)
c [simplification-10] removed 2131 irredundant clauses 1.0% (211654 remain 27%)
c [simplification-10] maximum reduction of 1% = max (0%, 1%)
c [simplification-10] geometric conflict interval increment 12000 = 24000 / 2
c [simplification-10] new conflict interval 36000
c [simplification-10] penalized conflict interval 36000 = 1 * 36000
c [simplification-10] hard conflict limit 119007 (soft 101007 + delta 18000)
c [simplification-10] new conflict limit 101007 (hard 119007)
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   52.5   29031   211654     88677   80169  13404  2631   10   109   46   9%    421   24    8    7  122%
c i   52.5   29019   211654     88679   80169  13404  2631   10   109   46   9%    420   24    8    7  122%
c -   53.0   29018   211654     90318   37028  13442  2633    9    99   40  10%   -103   14    9    7  134%
c 
c [simplification-11] limit 101012 conflicts (hard 119007) hit after 104252 conflicts
c [quatres-7] found 42558 quaternary clauses 30% in total
c [quatres-7-1] removed 38 duplicate quaternary clauses
c [quatres-7-2] added 320 single-self-subsuming ternary resolvents
c [quatres-7-2] added 344 quaternary resolvents
c [ternres-7] limit 8558339 with penalty 0 = 0 + 0
c [ternres-7] all 29018 free variables schedulable
c [ternres-7] 691 ternary resolvents (20 bin, 671 trn)
c [ternres-7] 2254 variables remain 8% (26764 retained 92%)
c [decomp-28] removed 22 variables
c [basicprobe-4] limit 42791696 penalty 0 = 0 + 0
c [basicprobe-4-0] 12156 sched 42%, 19 failed, 0 lifted, 619 hbrs
c [decomp-29] removed 38 variables
c [basicprobe-4-1] 15275 sched 53%, 6 failed, 0 lifted, 183 hbrs
c [decomp-30] removed 10 variables
c [basicprobe-4-2] 15260 sched 53%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-4-3] 15260 sched 53%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-3] fully completed probing
c [basicprobe-4-3] 25 units = 25 failed (100%) + 0 lifted (0%)
c [basicprobe-4-3] removed 48 variables, found 810 hbrs
c [bate-2] eliminated 963 asymmetric tautologies during probing
c [unhide-10] limit 1711667 with penalty 0 = 0 + 0
c [unhide-10-10] 0 units, 0 failed, 947 tauts, 0 hbrs, 10387 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 130 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 28962 variables 100%
c [block-4] limit of 21395848 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 1802 blocked clauses
c [block-4] 1802 < 1/100 * 209680 = 2096 considered unsuccessful
c [bca-7] limit of 10000000 steps and 416342 added (scaled 2)
c [bca-7] 36903 out of 57510 literals actually usable 64%
c [bca-7] added 9 blocked clauses in 160790 steps
c [sweep-7] limit 2567501 penalty 0 = 0 + 0
c [sweep-7-1] 4300 pos 44.3% + 5408 neg 55.7% = 9708 sched 33.8% ret 19046
c [sweep-7-1] 2573318 steps 736 queries 1898.40 avg class size
c [sweep-7-1] 11671 decisions 726 SAT calls 22.02 avg env size
c [sweep-7-1] 7818 variables remain 27% (20936 retained 73%)
c [decomp-32] removed 13 variables
c [sweep-7-1] removed 13 vars (0 failed, 14 eqs, 16 impls)
c [sweep-7] 13 < 1/1000 * 28754 = 28 considered unsuccessful
c [sweep-7] removed 13 vars in TOTAL (1 rounds, 735 queries)
c [sort-queue-11] sorted 10532 enqueued variables after 104252 conflicts
c [score-dist-11] active 18209 (63%), one 0 (0%), zero 10532 (37%)
c [score-dist-11] max exp 518, different 13 (3%)
c [score-dist-11] median active exp 518, avg 517.1
c [simplification-11] removed 277 variables 1.0% (28741 remain 11%)
c [simplification-11] removed 3792 irredundant clauses 1.8% (207862 remain 26%)
c [simplification-11] maximum reduction of 2% = max (1%, 2%)
c [simplification-11] geometric conflict interval increment 12000 = 36000 / 3
c [simplification-11] new conflict interval 48000
c [simplification-11] penalized conflict interval 48000 = 1 * 48000
c [simplification-11] hard conflict limit 176252 (soft 152252 + delta 24000)
c [simplification-11] new conflict limit 152252 (hard 176252)
c 
c [simplification-12] limit 152252 conflicts (hard 176252) hit after 152253 conflicts
c [quatres-8] found 42619 quaternary clauses 29% in total
c [quatres-8-1] removed 41 duplicate quaternary clauses
c [quatres-8-1] added 4 double-self-subsuming ternary resolvents
c [quatres-8-2] added 110 single-self-subsuming ternary resolvents
c [quatres-8-2] added 197 quaternary resolvents
c [ternres-8] limit 11554715 with penalty 0 = 0 + 0
c [ternres-8] 2229 schedulable variables 8%
c [ternres-8] 3115 ternary resolvents (68 bin, 3047 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-33] removed 5 variables
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 116 transitive binary clauses
c [transred-8] found 1 units
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 28735 variables 100%
c [elim-9] limit of 115547157 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 5 not tried 0% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 519 = 2% variables out of 28735 scheduled
c [bca-8] limit of 10000000 steps and 413986 added (scaled 2)
c [bca-8] 33440 out of 56434 literals actually usable 59%
c [bca-8] added 19 blocked clauses in 187036 steps
c [sort-queue-12] sorted 9838 enqueued variables after 152253 conflicts
c [score-dist-12] active 18378 (65%), one 0 (0%), zero 9838 (35%)
c [score-dist-12] max exp 519, different 14 (3%)
c [score-dist-12] median active exp 518, avg 517.6
c [simplification-12] removed 525 variables 1.8% (28216 remain 11%)
c [simplification-12] removed 1164 irredundant clauses 0.6% (206698 remain 26%)
c [simplification-12] maximum reduction of 2% = max (2%, 1%)
c [simplification-12] geometric conflict interval increment 16000 = 48000 / 3
c [simplification-12] new conflict interval 64000
c [simplification-12] penalized conflict interval 64000 = 1 * 64000
c [simplification-12] hard conflict limit 248253 (soft 216253 + delta 32000)
c [simplification-12] new conflict limit 216253 (hard 248253)
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   71.8   28215   206698    152983   85383  16613  2429    8   205   49   4%    537  112    7    8   81%
c i   73.0   28188   206698    160137   91414  16704  2446    8   144   49   6%   -327   45    8    8   96%
c i   73.7   28124   206698    162220   93091  16754  2452    9   153   49   6%   -380   53   10    8  123%
c -   74.3   28124   206698    165032   57660  16823  2455    9   157   42   6%   -364   55    9    8  116%
c i   75.7   28123   206698    176307   66955  17063  2472    8   160   45   5%   -147   51    6    8   78%
c i   76.5   28118   206698    181221   71013  17171  2488    8   102   45   7%   -268  -10    7    8   90%
c i   76.5   28109   206698    181222   71013  17169  2490    8   102   45   7%   -269  -10    7    8   90%
c i   78.6   28108   206698    190269   78051  17361  2515    9   147   46   6%   -171   32    9    8  106%
c i   78.6   28107   206698    190270   78051  17361  2515    9   147   46   6%   -171   32    9    8  106%
c i   79.6   28103   206698    193944   81035  17435  2518    9   224   46   4%   -238  106   12    8  138%
c i   81.5   28100   206698    204406   89748  17610  2536    8   191   47   4%   -105   60   10    8  118%
c i   81.5   28094   206698    204407   89748  17610  2536    8   191   47   4%   -105   60   10    8  117%
c i   81.9   28090   206698    205993   91028  17661  2545    9   166   47   5%   -205   34   10    8  115%
c i   83.8   28079   206698    215210   98383  17855  2563    9   209   47   4%    -96   70   10    8  116%
c i   84.9   28076   206698    222671  104362  18020  2579    8   117   48   7%   -106  -24    8    8   96%
c i   85.0   28075   206698    225006  106068  18028  2581    8   235   50   3%   -169   93   12    8  147%
c -   86.2   28073   206698    230268   76542  18187  2593    8   140   43   6%   -122   -6    7    8   79%
c i   87.5   28072   206698    239671   84452  18434  2605    7    84   46   9%     31  -55    5    8   64%
c 
c [simplification-13] limit 216283 conflicts (hard 248253) hit after 248254 conflicts
c [quatres-9] found 41730 quaternary clauses 27% in total
c [quatres-9-1] removed 14 duplicate quaternary clauses
c [quatres-9-1] added 6 double-self-subsuming ternary resolvents
c [quatres-9-2] added 247 single-self-subsuming ternary resolvents
c [quatres-9-2] added 498 quaternary resolvents
c [ternres-9] limit 16711315 with penalty 0 = 0 + 0
c [ternres-9] all 28064 free variables schedulable
c [ternres-9] 1325 ternary resolvents (42 bin, 1283 trn)
c [ternres-9] 2 variables remain 0% (28062 retained 100%)
c [decomp-34] removed 557 variables
c [unhide-11] limit 1671131 with penalty 1 = 1 + 0
c [unhide-11-11] 2 units, 4 failed, 1154 tauts, 0 hbrs, 25305 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 177 transitive binary clauses
c [elim-10] 5 variables 0% will be scheduled this time
c [elim-10] scheduled 5 variables 0%
c [elim-10] limit of 334226306 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] no variable eliminated in round 1 in 82663454 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 0 = 0% variables out of 5 scheduled
c [bca-9] limit of 10000000 steps and 399740 added (scaled 2)
c [bca-9] 31948 out of 55306 literals actually usable 58%
c [bca-9] added 9 blocked clauses in 182048 steps
c [sweep-8] limit 2506697 penalty 1 = 1 + 0
c [sweep-8-1] 3790 pos 49.7% + 3834 neg 50.3% = 7624 sched 27.6% ret 20028
c [sweep-8-1] 2513622 steps 520 queries 1627.18 avg class size
c [sweep-8-1] 8856 decisions 521 SAT calls 23.24 avg env size
c [sweep-8-1] 6301 variables remain 23% (21345 retained 77%)
c [decomp-35] removed 68 variables
c [sweep-8-1] removed 68 vars (0 failed, 7 eqs, 4 impls)
c [sweep-8] removed 68 vars in TOTAL (1 rounds, 519 queries)
c [sort-queue-13] sorted 9346 enqueued variables after 248254 conflicts
c [score-dist-13] active 18238 (66%), one 0 (0%), zero 9346 (34%)
c [score-dist-13] max exp 519, different 14 (3%)
c [score-dist-13] median active exp 519, avg 518.1
c [simplification-13] removed 480 variables 1.7% (27584 remain 10%)
c [simplification-13] removed 7412 irredundant clauses 3.6% (199286 remain 25%)
c [simplification-13] maximum reduction of 4% = max (2%, 4%)
c [simplification-13] geometric conflict interval increment 12800 = 64000 / 5
c [simplification-13] new conflict interval 76800
c [simplification-13] penalized conflict interval 76800 = 1 * 76800
c [simplification-13] hard conflict limit 363454 (soft 325054 + delta 38400)
c [simplification-13] new conflict limit 325054 (hard 363454)
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   92.1   27583   199286    250133   84571  17097  2738    9   145   46   6%    -21    6    9    8  103%
c i   94.0   27582   199286    257577   90702  17294  2770    9   147   46   6%    -57    9   10    8  118%
c i   94.2   27581   199286    259000   91909  17317  2774    9   139   46   7%   -120    1   11    8  125%
c i   94.9   27580   199286    261798   94213  17398  2778    9   175   47   5%   -118   37   10    8  119%
c i   95.1   27573   199286    262640   94829  17443  2788    9   166   47   6%   -130   27    9    9  111%
c i   95.1   27572   199286    262641   94829  17443  2788    9   166   47   6%   -130   27    9    9  111%
c i   95.1   27571   199286    262644   94830  17443  2788    9   166   47   6%   -130   27    9    9  110%
c i   95.2   27569   199286    263189   95297  17450  2788    9   166   47   6%   -134   27   10    9  123%
c i   98.1   27566   199286    274616  104641  17715  2810    9   137   48   7%     27   -4    7    9   80%
c i  100.8   27564   199286    289360  116573  18040  2829    9   186   50   5%     83   44   12    9  135%
c 
c [simplification-14] limit of 39 iterations hit after 39 iterations
c [quatres-10] found 44516 quaternary clauses 27% in total
c [quatres-10-1] removed 72 duplicate quaternary clauses
c [quatres-10-1] added 4 double-self-subsuming ternary resolvents
c [quatres-10-2] added 253 single-self-subsuming ternary resolvents
c [quatres-10-2] added 563 quaternary resolvents
c [ternres-10] limit 19347782 with penalty 0 = 0 + 0
c [ternres-10] 2 schedulable variables 0%
c [ternres-10] 7162 ternary resolvents (695 bin, 6467 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 483694 penalty 3 = 3 + 0
c [gauss-4] extracted 3628 xors of average arity 3.0
c [gauss-4] connected 10858 occurrences of 2802 variables (average 3.9)
c [gauss-4] limit 483694 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-36] removed 96 variables
c [simpleprobe-5] 9143 schedulable variables 33%
c [simpleprobe-5] limit 19347782 penalty 2 = 2 + 0
c [decomp-37] removed 15 variables
c [simpleprobe-5] 6023 variables remain 22% (21430 retained 78%)
c [simpleprobe-5] removed 15 variables, found 260 hbrs, 1 units
c [unhide-12] limit 3869556 with penalty 0 = 0 + 0
c [unhide-12-13] 4 units, 7 failed, 4676 tauts, 0 hbrs, 55785 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 213 transitive binary clauses
c [transred-10] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 120923642 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 2 clauses out of 141 (1%) of length 20
c [cce-4-1] eliminated 6 clauses out of 170 (4%) of length 19
c [cce-4-1] eliminated 6 clauses out of 250 (2%) of length 18
c [cce-4-1] eliminated 12 clauses out of 287 (4%) of length 17
c [cce-4-1] eliminated 21 clauses out of 308 (7%) of length 16
c [cce-4-1] eliminated 22 clauses out of 357 (6%) of length 15
c [cce-4-1] eliminated 38 clauses out of 493 (8%) of length 14
c [cce-4-1] eliminated 29 clauses out of 541 (5%) of length 13
c [cce-4-1] eliminated 57 clauses out of 923 (6%) of length 12
c [cce-4-1] eliminated 64 clauses out of 1539 (4%) of length 11
c [cce-4-1] eliminated 177 clauses out of 2017 (9%) of length 10
c [cce-4-1] eliminated 235 clauses out of 3360 (7%) of length 9
c [cce-4-1] eliminated 870 clauses out of 6339 (14%) of length 8
c [cce-4-1] eliminated 1332 clauses out of 13304 (10%) of length 7
c [cce-4-1] eliminated 1275 clauses out of 28195 (5%) of length 6
c [cce-4-1] eliminated 1147 clauses out of 17625 (7%) of length 5
c [cce-4-1] eliminated 1194 clauses out of 20131 (6%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 6487 large clauses in 112832873 steps
c [cce-4-1] allowing another 56416436 steps for small clauses
c [cce-4-1] scheduling 37638 clauses = 23259 binary + 14379 ternary
c [cce-4-1] tried to eliminate 37638 small clauses 100%
c [cce-4-1] eliminated 233 binary clauses 1%
c [cce-4-1] eliminated 355 ternary clauses 2%
c [cce-4-1] eliminated 588 small clauses 2%
c [cce-4-1] eliminated 621 small clauses in 89216069 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 7108 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 15853837 steps for small clauses
c [cce-4-2] scheduling 37052 clauses = 23026 binary + 14026 ternary
c [cce-4-2] tried to eliminate 18802 small clauses 51%
c [cce-4-2] eliminated 1 ternary clauses 0%
c [cce-4-2] eliminated 1 small clauses 0%
c [cce-4-2] eliminated 1 small clauses in 31708102 steps
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 1 covered clauses in round 2
c [cce-4] eliminated 7109 covered clauses in TOTAL during 2 rounds
c [bca-10] limit of 10000000 steps and 381122 added (scaled 2)
c [bca-10] 29643 out of 54862 literals actually usable 54%
c [bca-10] added 2 blocked clauses in 205259 steps
c [sweep-9] limit 5804334 penalty 0 = 0 + 0
c [sweep-9-1] 3408 pos 54.2% + 2875 neg 45.8% = 6283 sched 22.9% ret 21147
c [sweep-9-1] 5811503 steps 1212 queries 880.94 avg class size
c [sweep-9-1] 20375 decisions 1217 SAT calls 23.78 avg env size
c [sweep-9-1] 3324 variables remain 12% (24103 retained 88%)
c [decomp-38] removed 75 variables
c [sweep-9-1] removed 75 vars (0 failed, 15 eqs, 7 impls)
c [sweep-9] removed 75 vars in TOTAL (1 rounds, 1211 queries)
c [sort-queue-14] sorted 9127 enqueued variables after 289360 conflicts
c [score-dist-14] active 18228 (67%), one 0 (0%), zero 9127 (33%)
c [score-dist-14] max exp 520, different 15 (3%)
c [score-dist-14] median active exp 519, avg 518.5
c [simplification-14] removed 209 variables 0.8% (27355 remain 10%)
c [simplification-14] removed 9148 irredundant clauses 4.6% (190138 remain 24%)
c [simplification-14] maximum reduction of 5% = max (1%, 5%)
c [simplification-14] forced so keeping old conflict interval 76800
c [simplification-14] conflict limit remains at 325067 (hard 363454)
c [simplification-14] 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  106.0   27354   190137    289827  114850  21429  3618    9   184   52   5%      5   42    9    9  103%
c -  106.7   27354   190137    293333   82866  21504  3627    9   154   43   6%    -84   11    9    9  103%
c i  106.8   27353   190137    294166   83541  21543  3627    9   139   46   6%    -73   -5    7    9   86%
c i  107.1   27349   190137    295543   84698  21589  3634    9   122   46   7%   -101  -21    7    9   80%
c i  107.7   27348   190137    299109   87744  21632  3639    9   202   46   4%    -79   55   11    9  123%
c i  108.3   27344   190137    301559   89778  21721  3653    9   151   46   6%    -89    3    6    9   72%
c i  109.3   27341   190137    306008   93440  21798  3663    9   225   47   4%    -56   72    8    9   98%
c i  113.1   27337   190137    321816  106855  22175  3711    9   101   48   9%    119  -48    7    9   81%
c 
c [simplification-15] limit 325067 conflicts (hard 363454) hit after 329729 conflicts
c [quatres-11] found 42837 quaternary clauses 27% in total
c [quatres-11-1] removed 33 duplicate quaternary clauses
c [quatres-11-1] added 10 double-self-subsuming ternary resolvents
c [quatres-11-2] added 3376 single-self-subsuming ternary resolvents
c [quatres-11-2] added 276 quaternary resolvents
c [ternres-11] limit 21988984 with penalty 0 = 0 + 0
c [ternres-11] all 27331 free variables schedulable
c [ternres-11] 8725 ternary resolvents (652 bin, 8073 trn)
c [ternres-11] 37 variables remain 0% (27294 retained 100%)
c [card-5] limit 687155 penalty 4 = 4 + 0
c [card-5] found 121 at-most-one constraints of average size 3.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 687155 for elimination
c [card-5] 121 out of 121 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-39] removed 144 variables
c [treelook-5] limit 2198898 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 22318 literals 41%
c [treelook-5] scheduling used 804134 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2198898 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2200698 steps
c [treelook-5] 21081 literals remain 39%
c [treelook-5] 6909 variables remain to probed next time 25%
c [decomp-40] removed 10 variables
c [treelook-5] removed 18 variables, found 1700 hbrs
c [unhide-13] limit 4397796 with penalty 0 = 0 + 0
c [unhide-13-15] 0 units, 1 failed, 4247 tauts, 0 hbrs, 45965 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 290 transitive binary clauses
c [transred-11] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 27190 variables 100%
c [block-5] limit of 27486230 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 17146 blocked clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 25007 variables 100%
c [elim-11] limit of 219889846 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 2597 variables 10% in round 1 in 106381855 steps
c [elim-11-1] backward subsumption/strengthening limit 106381800
c [elim-11-1-1] backward checking 6720 touched variables 27%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 19 and strengthened 29 clauses in 5792259 steps
c [elim-11-1] rescheduled 95 variables 0% by backward subsumption
c [elim-11-2] eliminated 3 variables 0% in round 2 in 7102208 steps
c [elim-11-2] backward subsumption/strengthening limit 7102200
c [elim-11-2-1] backward checking 10 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 0 clauses in 224122 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 2600 = 10% variables out of 25007 scheduled
c [bca-11] limit of 10000000 steps and 330617 added (scaled 2)
c [bca-11] 25164 out of 44816 literals actually usable 56%
c [bca-11] added 29 blocked clauses in 166752 steps
c [sweep-10] limit 6596695 penalty 0 = 0 + 0
c [sweep-10-1] 1309 pos 48.5% + 1392 neg 51.5% = 2701 sched 12.1% ret 19706
c [sweep-10-1] 2726018 steps 1517 queries 347.39 avg class size
c [sweep-10-1] 22376 decisions 1519 SAT calls 19.31 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-41] removed 30 variables
c [sweep-10-1] removed 30 vars (0 failed, 2 eqs, 0 impls)
c [sweep-10-2] 9455 pos 42.3% + 12922 neg 57.7% = 22377 sched 100.0% ret 0
c [sweep-10-2] 3893842 steps 315 queries 1333.02 avg class size
c [sweep-10-2] 10320 decisions 313 SAT calls 56.98 avg env size
c [sweep-10-2] 14575 variables remain 65% (7798 retained 35%)
c [decomp-42] removed 22 variables
c [sweep-10-2] removed 22 vars (0 failed, 11 eqs, 6 impls)
c [sweep-10] removed 52 vars in TOTAL (2 rounds, 1830 queries)
c [sort-queue-15] sorted 7244 enqueued variables after 329729 conflicts
c [score-dist-15] active 15111 (68%), one 0 (0%), zero 7244 (32%)
c [score-dist-15] max exp 520, different 15 (3%)
c [score-dist-15] median active exp 520, avg 519.0
c [simplification-15] removed 4976 variables 18.2% (22355 remain 8%)
c [simplification-15] removed 25227 irredundant clauses 13.3% (164910 remain 21%)
c [simplification-15] maximum reduction of 18% = max (18%, 13%)
c [simplification-15] large reduction 18% >= 5% limit
c [simplification-15] next conflict interval 3297 = min (329729/100, 76800)
c [simplification-15] penalized conflict interval 3297 = 1 * 3297
c [simplification-15] hard conflict limit 343026 (soft 333026 + delta 10000)
c [simplification-15] new conflict limit 333026 (hard 343026)
c 
c [simplification-16] limit 333026 conflicts (hard 343026) hit after 333026 conflicts
c [quatres-12] found 29256 quaternary clauses 22% in total
c [quatres-12-1] removed 47 duplicate quaternary clauses
c [quatres-12-1] added 3 double-self-subsuming ternary resolvents
c [quatres-12-2] added 168 single-self-subsuming ternary resolvents
c [quatres-12-2] added 345 quaternary resolvents
c [ternres-12] limit 22216646 with penalty 0 = 0 + 0
c [ternres-12] 37 schedulable variables 0%
c [ternres-12] 5988 ternary resolvents (358 bin, 5630 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-43] removed 29 variables
c [basicprobe-5] limit 111083231 penalty 0 = 0 + 0
c [basicprobe-5-0] 11607 sched 52%, 19 failed, 0 lifted, 845 hbrs
c [decomp-44] removed 67 variables
c [basicprobe-5-1] 11534 sched 52%, 0 failed, 0 lifted, 72 hbrs
c [decomp-45] removed 1 variables
c [basicprobe-5-2] 11537 sched 52%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-2] fully completed probing
c [basicprobe-5-2] 19 units = 19 failed (100%) + 0 lifted (0%)
c [basicprobe-5-2] removed 68 variables, found 917 hbrs
c [bate-3] eliminated 88 asymmetric tautologies during probing
c [unhide-14] limit 4443329 with penalty 0 = 0 + 0
c [unhide-14-17] 0 units, 0 failed, 2688 tauts, 0 hbrs, 11093 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 243 transitive binary clauses
c [cce-5] limit of 27770807 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 34
c [cce-5-1] eliminated 1 clauses out of 4 (25%) of length 30
c [cce-5-1] eliminated 2 clauses out of 5 (40%) of length 26
c [cce-5-1] eliminated 2 clauses out of 15 (13%) of length 25
c [cce-5-1] eliminated 3 clauses out of 22 (14%) of length 24
c [cce-5-1] eliminated 10 clauses out of 72 (14%) of length 22
c [cce-5-1] eliminated 3 clauses out of 62 (5%) of length 21
c [cce-5-1] eliminated 10 clauses out of 158 (6%) of length 20
c [cce-5-1] eliminated 10 clauses out of 198 (5%) of length 19
c [cce-5-1] eliminated 26 clauses out of 294 (9%) of length 18
c [cce-5-1] eliminated 22 clauses out of 291 (8%) of length 17
c [cce-5-1] eliminated 16 clauses out of 314 (5%) of length 16
c [cce-5-1] eliminated 32 clauses out of 375 (9%) of length 15
c [cce-5-1] eliminated 26 clauses out of 488 (5%) of length 14
c [cce-5-1] eliminated 16 clauses out of 612 (3%) of length 13
c [cce-5-1] eliminated 45 clauses out of 915 (5%) of length 12
c [cce-5-1] eliminated 51 clauses out of 1450 (4%) of length 11
c [cce-5-1] eliminated 87 clauses out of 1992 (4%) of length 10
c [cce-5-1] eliminated 189 clauses out of 3337 (6%) of length 9
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 552 large clauses in 27770810 steps
c [cce-5-1] allowing another 13885405 steps for small clauses
c [cce-5-1] scheduling 29015 clauses = 18517 binary + 10498 ternary
c [cce-5-1] tried to eliminate 14884 small clauses 51%
c [cce-5-1] eliminated 248 binary clauses 1%
c [cce-5-1] eliminated 361 ternary clauses 3%
c [cce-5-1] eliminated 609 small clauses 2%
c [cce-5-1] eliminated 609 small clauses in 27770815 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1161 covered clauses in round 1
c [cce-5] eliminated 1161 covered clauses in TOTAL during 1 rounds
c [cce-5] 1161 < 1/100 * 164105 = 1641 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 22258 variables 100%
c [elim-12] limit of 444332926 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 801 variables 4% in round 1 in 94839779 steps
c [elim-12-1] backward subsumption/strengthening limit 94839700
c [elim-12-1-1] backward checking 1866 touched variables 8%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 5 and strengthened 3 clauses in 3363808 steps
c [elim-12-1] rescheduled 32 variables 0% by backward subsumption
c [elim-12-2] eliminated 1 variables 0% in round 2 in 416757 steps
c [elim-12-2] backward subsumption/strengthening limit 416700
c [elim-12-2-1] backward checking 11 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 0 and strengthened 0 clauses in 113891 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 802 = 4% variables out of 22258 scheduled
c [bca-12] limit of 10000000 steps and 317522 added (scaled 2)
c [bca-12] 23639 out of 42914 literals actually usable 55%
c [bca-12] added 102 blocked clauses in 161972 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 66649930 penalty 0 = 0 + 0
c [sweep-11-1] 6694 pos 48.1% + 7230 neg 51.9% = 13924 sched 64.9% ret 7532
c [sweep-11-1] 15604713 steps 2932 queries 252.98 avg class size
c [sweep-11-1] 61693 decisions 2903 SAT calls 30.44 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-46] removed 124 variables
c [sweep-11-1] removed 124 vars (4 failed, 130 eqs, 75 impls)
c [sweep-11-2] 10077 pos 47.2% + 11255 neg 52.8% = 21332 sched 100.0% ret 0
c [sweep-11-2] 16997062 steps 2893 queries 251.71 avg class size
c [sweep-11-2] 61320 decisions 2881 SAT calls 31.71 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-47] removed 72 variables
c [sweep-11-2] removed 72 vars (0 failed, 97 eqs, 37 impls)
c [sweep-11-3] 10047 pos 47.3% + 11213 neg 52.7% = 21260 sched 100.0% ret 0
c [sweep-11-3] 17182886 steps 2984 queries 195.98 avg class size
c [sweep-11-3] 62469 decisions 2970 SAT calls 30.82 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-48] removed 36 variables
c [sweep-11-3] removed 36 vars (0 failed, 58 eqs, 13 impls)
c [sweep-11] removed 232 vars in TOTAL (3 rounds, 8806 queries)
c [sort-queue-16] sorted 6454 enqueued variables after 333026 conflicts
c [score-dist-16] active 14770 (70%), one 0 (0%), zero 6454 (30%)
c [score-dist-16] max exp 520, different 15 (3%)
c [score-dist-16] median active exp 520, avg 519.2
c [simplification-16] removed 1131 variables 5.1% (21224 remain 8%)
c [simplification-16] removed 6623 irredundant clauses 4.0% (158287 remain 20%)
c [simplification-16] maximum reduction of 5% = max (5%, 4%)
c [simplification-16] large reduction 5% >= 5% limit
c [simplification-16] next conflict interval 3330 = min (333026/100, 76800)
c [simplification-16] penalized conflict interval 3330 = 1 * 3330
c [simplification-16] hard conflict limit 346356 (soft 336356 + delta 10000)
c [simplification-16] new conflict limit 336356 (hard 346356)
c 
c [simplification-17] limit 336356 conflicts (hard 346356) hit after 336356 conflicts
c [quatres-13] found 28476 quaternary clauses 22% in total
c [quatres-13-1] removed 58 duplicate quaternary clauses
c [quatres-13-1] added 1 double-self-subsuming ternary resolvents
c [quatres-13-2] added 168 single-self-subsuming ternary resolvents
c [quatres-13-2] added 158 quaternary resolvents
c [ternres-13] limit 22375296 with penalty 0 = 0 + 0
c [ternres-13] all 21224 free variables schedulable
c [ternres-13] 2598 ternary resolvents (226 bin, 2372 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-49] removed 4 variables
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 466 transitive binary clauses
c [transred-13] found 1 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 21219 variables 100%
c [block-6] limit of 55938241 steps penalty 2 = 2 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 634 blocked clauses
c [block-6] 634 < 1/100 * 158023 = 1580 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 21158 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 149 variables 1% in round 1 in 93444946 steps
c [elim-13-1] backward subsumption/strengthening limit 93444900
c [elim-13-1-1] backward checking 887 touched variables 4%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 0 clauses in 2382076 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 149 = 1% variables out of 21158 scheduled
c [elim-13] 149 < 1/100 * 21158 = 211 considered unsuccessful
c [bca-13] limit of 10000000 steps and 312911 added (scaled 2)
c [bca-13] 22355 out of 42020 literals actually usable 53%
c [bca-13] added 9 blocked clauses in 157883 steps
c [sweep-12] limit 6712589 penalty 0 = 0 + 0
c [sweep-12-1] 10237 pos 48.7% + 10772 neg 51.3% = 21009 sched 100.0% ret 0
c [sweep-12-1] 6718866 steps 485 queries 910.64 avg class size
c [sweep-12-1] 16159 decisions 486 SAT calls 55.43 avg env size
c [sweep-12-1] 9544 variables remain 45% (11465 retained 55%)
c [decomp-50] removed 13 variables
c [sweep-12-1] removed 13 vars (0 failed, 12 eqs, 2 impls)
c [sweep-12] 13 < 1/1000 * 21009 = 21 considered unsuccessful
c [sweep-12] removed 13 vars in TOTAL (1 rounds, 484 queries)
c [sort-queue-17] sorted 6326 enqueued variables after 336356 conflicts
c [score-dist-17] active 14670 (70%), one 0 (0%), zero 6326 (30%)
c [score-dist-17] max exp 520, different 15 (3%)
c [score-dist-17] median active exp 520, avg 519.2
c [simplification-17] removed 228 variables 1.1% (20996 remain 8%)
c [simplification-17] removed 2172 irredundant clauses 1.4% (156115 remain 20%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] geometric conflict interval increment 38400 = 76800 / 2
c [simplification-17] new conflict interval 115200
c [simplification-17] penalized conflict interval 115200 = 1 * 115200
c [simplification-17] hard conflict limit 509156 (soft 451556 + delta 57600)
c [simplification-17] new conflict limit 451556 (hard 509156)
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 -  138.7   20996   156115    366583   75053  22095  3832    9   102   40   9%    440  -36    7    9   79%
c -  148.3   20996   156115    423634   88795  23166  3875    8    58   54  13%    780  -77    7    9   77%
c 
c [simplification-18] limit 451556 conflicts (hard 509156) hit after 453252 conflicts
c [quatres-14] found 31142 quaternary clauses 20% in total
c [quatres-14-1] removed 2 duplicate quaternary clauses
c [quatres-14-2] added 127 single-self-subsuming ternary resolvents
c [quatres-14-2] added 196 quaternary resolvents
c [ternres-14] limit 28938024 with penalty 0 = 0 + 0
c [ternres-14] all 20996 free variables schedulable
c [ternres-14] 2794 ternary resolvents (107 bin, 2687 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-51] removed 21 variables
c [simpleprobe-6] 4549 schedulable variables 22%
c [simpleprobe-6] limit 57876049 penalty 1 = 1 + 0
c [decomp-52] removed 34 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 34 variables, found 1410 hbrs, 8 units
c [unhide-15] limit 2893802 with penalty 1 = 1 + 0
c [unhide-15-19] 0 units, 0 failed, 7373 tauts, 0 hbrs, 52788 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 427 transitive binary clauses
c [bca-14] limit of 10000000 steps and 311963 added (scaled 2)
c [bca-14] 21864 out of 41884 literals actually usable 52%
c [bca-14] added 6 blocked clauses in 179967 steps
c [sort-queue-18] sorted 6221 enqueued variables after 453252 conflicts
c [score-dist-18] active 14720 (70%), one 0 (0%), zero 6221 (30%)
c [score-dist-18] max exp 520, different 15 (3%)
c [score-dist-18] median active exp 520, avg 519.3
c [simplification-18] removed 55 variables 0.3% (20941 remain 8%)
c [simplification-18] removed 471 irredundant clauses 0.3% (155644 remain 20%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] full geometric conflict interval increment 115200
c [simplification-18] new conflict interval 230400
c [simplification-18] penalized conflict interval 230400 = 1 * 230400
c [simplification-18] hard conflict limit 798852 (soft 683652 + delta 115200)
c [simplification-18] new conflict limit 683652 (hard 798852)
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 -  162.5   20941   155644    482797   97333  25315  4040   10   131   42   7%    925   11    8    9   94%
c -  171.7   20941   155644    536185  108289  25927  4066    9   127   57   7%    980    5   11    9  124%
c -  182.0   20941   155644    587565  116757  26762  4115    9    66   57  14%   1004  -34   10    9  115%
c -  194.6   20941   155644    638377  124225  27436  4150   10    50   58  19%   1015  -30   11    9  116%
c i  204.0   20940   155644    672667  155635  27776  4164   10    35   67  28%   1019  -28    7    9   79%
c -  208.7   20763   155644    688548  133044  27939  4194   10    25   58  38%  -3351  -30   12    9  125%
c i  209.8   20762   155644    692555  136542  27977  4205    9    21   63  42%  -3091  -32    7    9   72%
c i  211.9   20757   155644    701021  144162  28015  4213    9    19   65  50%  -2870  -31    9    9  100%
c i  213.2   20725   155644    705757  148210  28045  4225    8    14   65  61%  -2722  -33    6    9   65%
c i  213.2   20582   155644    706020  148377  28056  4231    8    13   65  62%  -2724  -33    5    9   60%
c i  213.3   20298   155644    706064  148397  28061  4233    8    13   65  62%  -2724  -33    5    9   56%
c 0  213.3   19874   155644    706064  148397  28061  4233    8    13   65  62%  -2724  -33    5    9   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: 1734 basic ate = 147 trn 8% + 1587 lrg 92% in 3 updates
c bcas: 14 count, 357 added (1568 skipped), 2327486 steps
c bkwd: tried 83048 clauses, 166058 lits, 2.00 lits/clause
c bkwd: checked 6663654 occs, 80.24 occs/clause, 40.13 occs/lit
c bkwd: subsumed 0 binary, 1 ternary, 23 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 32 large (0% self)
c blkd: 6 bces, 28809 removed, 8503330 resolutions, 22930889 steps
c blkd: 8792 blocking literals 2%, 3254 pure
c bump: 674981 bumped seen, 28331438 lits 42.0 on average
c card: 5 count, 0 units, 1 am1, 10226897 steps
c card: 1 rescheduled, 2 eliminated, 8 resolved, 2402 subsumed
c card: 343 at-most-one constraints found, average size 3.05
c card: 343 at-most-one constraints used 100%, average size 3.05
c card: 2 at-most-two constraints found, average size 4.00
c card: 2 at-most-two constraints used 100%, average size 4.00
c cces: 5 cces, 11059 eliminated, 10551 ate 95%, 508 abce 5%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 2640582 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 113 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 52 decompositions, 6211 equivalent 2%
c deco: 24 decision-only clauses 0%, 48% reduction
c decs: 8821206 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 13 elims, 231151 eliminated 87%, 108 pure 0%
c elms: 18 rounds, 1.4 rounds/bve
c elms: 216890 small 94%, 10899 large 5%
c elms: 299052 tried small, 216890 succeeded 73%, 82162 failed 27%
c elms: 9821 subsumed, 5892 strengthened, 1012 blocked
c elms: 8949540 copies, 15501003 resolutions, 5938823 ipos
c elms: 6619746 subchks, 5933735 strchks
c gaus: 4 extractions, 34406 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 7976520 steps, 3988260 extr 50%, 4026242 elim 50%
c glue: 9.0 orig avg, 9.0 real avg, 2.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 16251 = 2811 simple 17% + 11948 trn 74% + 1492 lrg 9%, 1269 sub 8%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 674981 clauses, 20.6 length
c lrnd: 13875723 lits = 18626897 orig - 4751174 removed 26%
c lrnd: 218621 uips 32%, 276398 flips 41%
c mins: 649849 mins 96%, 535 bin 0%, 24558 size 4%
c mins: 17955079 poisoned searches, 2655665 hits, 15% hit rate
c mins: 33085907 used twice searches, 2822518 hits, 9% hit rate
c move: moved 18720, 4364 bin 23%, 14356 trn 77%
c otfs: 37220 driving 51%, 36389 restarting 49%
c otfs: str 73609, 73374 red 100%, 235 irr 0%
c otfs: str 73609, 0 bin 0%, 545 trn 1%, 73064 lrg 99%
c otfs: sub 944, 940 red 100%, 4 irr 0%
c otfs: sub 944, 0 bin 0%, 71 trn 8%, 873 lrg 92%
c phas: 3 computed, 64631 set, 23082 pos (36%), 41549 neg (64%)
c prbs: 5 basic, 298838 probed, 645 failed, 253 lifted
c prbs: 6 simple, 475865 probed, 96 failed, 193 eqs
c prbs: 5 treelook, 1753 probed, 11 failed, 0 lifted
c prom: 95661 locked 15% out of 625785 tried
c prps: 319819144 props, 36 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 14 count, 21371 quat, 5460 self1, 37 self2, 633 dup
c queu: 18 sorted, 8821206 next (73576 steps 0.01)
c queu: 28900969 enq (753841071 steps 26.08), 28331438 deq 98%
c redc: 21676 clauses 8%, 270873 tried 38%, 9 sat 0%
c redc: 27067 lits 1%, 2625687 tried 14%, 9 sat 0%
c redc: 529 times jump level reduced, 7.0 levels on average
c reds: 11 count, 64187.6 conflicts per reduce
c reds: 0 memlim 0%, 11 arith 100%
c reds: 302517 collected 74%, 104291 retired 26%
c rmbd: 1443 removed, 785 red 54%
c rsts: 20446 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: 18 count, 17 confs 94%, 0 vars 0%
c simp: 1 its 6%, 0 bin 0%, 0 trns 0%
c subl: 674981 count (286862 tried 0.4), 57930 sub out of 667293 (8.7%)
c swps: 12 count, 15 rounds, 15755 queries (1050.3/round)
c swps: 15687 sat calls, 327 unsat (0.4% success rate)
c swps: 325587 decisions 20.8, 6137 conflicts 0.4
c swps; 746.7 avg class size, 30.6 avg environment size
c swps: 4 failed, 185 impls, 388 equivs
c swp0: 5248 type 0 queries, 542 unsat (10.3%), 5182 sat (98.7%)
c swp1: 10507 type 1 queries, 2821 unsat (26.8%), 10185 sat (96.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: 18992767 calls to obtain time
c tops: 9169 fixed 3%, 52 its, 13578.15 confs/it
c trds: 14 transitive reductions, 3035 removed, 5 failed
c trds: 765969 nodes, 363446 edges, 5087548 steps
c trim: 622758 words, 2.4 MB
c trnr: 14 count, 2567 bin, 44967 trn, 191419536 steps
c unhd: 15 count, 19 rounds, 44691671 steps
c unhd: 1108 non-trivial sccs of average size 2.3
c unhd: 52 units, 52 bin, 0 trn, 0 lrg
c unhd: 252 failed, 242 stamp, 0 lits, 1 bin, 7 trn, 0 lrg
c unhd: 25938 tauts, 183 bin 1%, 12377 trn 48%, 10172 lrg 39%
c unhd: 25938 tauts, 3206 stamp 12%, 22714 red 88%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 242561 str, 52 bin 0%, 2056 trn 1%, 240453 lrg 99%, 219692 red 91%
c vars: 19874 remaining 7% and 246531 removed 93% out of 266405
c vars: 9169 fixed 3%, 231151 eliminated 87%, 6211 equivalent 2%
c vsts: 4684493776 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 14.7 search visits per propagation, 6511.5 per conflict
c wchs: 1017242636 pushed, 30011550 enlarged, 183 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         688664        302517        104291      30398452       3347264        312631
c 
c  0 0        181553  26      6200   2         0   0  23269885  77<  1859565  56    154824  50     3.8
c  1 5         69144  10     35472  12     12856  12   2860174   9    413938  12<    42199  13<    0.6
c  2 6        163720  24<    98181  32     29232  28   2755697   9    596447  18     62291  20     1.6
c  3 9        161313  23     98463  33<    30712  29<  1126358   4    340074  10     38451  12     2.3
c  4 14        75461  11     44724  15     18595  18    297286   1    102410   3     11141   4     1.2
c  5 21        25884   4     14036   5      8290   8     66704   0     26068   1      2810   1     0.6
c  6 30         8153   1      4004   1      3138   3     16686   0      6396   0       649   0     0.3
c  7 41         2365   0      1051   0      1011   1      3930   0      1666   0       190   0     0.2
c  8 54          679   0       282   0       304   0      1195   0       459   0        52   0     0.1
c  9 69          199   0        69   0        98   0       275   0       111   0        17   0     0.0
c 10 86          124   0        25   0        38   0       177   0        77   0         3   0     0.0
c 11 126          54   0        10   0        13   0        69   0        45   0         4   0     0.0
c 12 230          13   0         0   0         3   0        14   0         7   0         0   0     0.0
c 13 534           2   0         0   0         1   0         2   0         1   0         0   0     0.0
c 
c avg                  2.0           2.7           3.0           0.4           1.0           1.1
c std                  1.6           1.2           1.4           0.9           1.3           1.3
c 
c   18.896   9% elim
c   12.249   6% bump
c    9.113   4% sweep
c    6.833   3% probe
c    6.219   3% decide
c    4.475   2% unhide
c    4.251   2% cce
c    2.895   1% quatres
c    2.251   1% block
c    1.767   1% bca
c 
c    3.448 < 1% rest (below)
c 
c    1.690   1% ternres
c    0.980   0% gauss
c    0.428   0% transred
c    0.349   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.207   2% preprocessing     9%
c   53.098  25% inprocessing     91%
c ==================================
c   58.305  27% simplifying
c  154.957  73% search
c ==================================
c  213.266 100% all
c 
c        706064 conflicts,        3310.7 confs/sec
c          5641 ternaries,         125.2 confs/ternary
c           727 binaries,          971.2 confs/binary
c            52 iterations,      13578.2 confs/iteration
c 
c            11 reductions,          0.1 redus/sec,  64187.6 confs/reduction
c         20446 restarts,           95.9 rests/sec,     34.5 confs/restart
c       8821206 decisions,       41362.4 decis/sec,     12.5 decis/conflict
c     319819144 propagations,  1499625.1 props/sec,     36.3 props/decision
c 
c 213.3 seconds, 75.5 MB
c launch: done
