c launch: /data/cnf/sc2014/app/SAT_dat.k70-24_1_rule_1.cnf.bz2
c host: atom19
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/SAT_dat.k70-24_1_rule_1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/SAT_dat.k70-24_1_rule_1.cnf.bz2
c no embedded options
c found 'p cnf 1131652 4433524' header
c read 1131652 variables, 4433524 clauses, 11129247 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=0
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 1096149 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] STATIC (--score=0)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0 1096149  4397887         0       0      0     0    0     0  254   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1099471 based on 4397887 irredundant clauses
c [card-1] found 972 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1099471 for elimination
c [card-1] 972 out of 972 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 275789 variables
c [simpleprobe-1] all 855863 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 6951694 based on 3475847 irredundant clauses
c [decomp-2] removed 2404 variables
c [simpleprobe-1] 722398 variables remain 85% (131061 retained 15%)
c [simpleprobe-1] removed 2404 variables, found 8129 hbrs, 778 units
c [unhide-1] limit 216302 based on 3460846 irredundant clauses
c [unhide-1-1] 1003 units, 1105 failed, 7637 tauts, 0 hbrs, 42551 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 849097 variables 100%
c [elim-1] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 768445 not tried 91% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 81297 = 10% variables out of 849097 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 3049395 negative 95.2% of 3203267 except 153872 4.8%
c [phase-count-1] 2998266 positive 93.6% of 3203267 except 205001 6.4%
c [phase-1] phase bias: 356508 positive 46%, 411292 negative 54%
c [sort-queue-1] sorted 767800 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 767800 (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 160584 variables 17.3% (767800 remain 70%)
c [simplification-1] removed 1194620 irredundant clauses 27.2% (3203267 remain 73%)
c [simplification-1] maximum reduction of 27% = max (17%, 27%)
c [simplification-1] large reduction 27% >= 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   13.4  767799  3203267         8       5     17  6599    0     1  203   1%      0    1    0    0 25168%
c i   13.6  767798  3203267        40      20     25  6607    0     3  203   1%      0    3    0    0 23803%
c i   13.8  767796  3203267       111      44     35  6643    0     9  203   1%      0    9    1    0 20807%
c i   13.9  767795  3203267       121      48     37  6646    0    12  203   0%      0   12    1    0 20612%
c i   13.9  767754  3203267       122      48     37  6646    0    12  203   0%      0   12    1    0 20532%
c i   13.9  767714  3203267       126      49     38  6647    0    13  203   0%      0   13    1    0 20340%
c i   13.9  767713  3203267       127      49     38  6647    0    13  203   0%      0   13    1    0 20261%
c i   13.9  767712  3203267       128      49     38  6647    0    13  203   0%      0   13    1    0 20182%
c i   13.9  767711  3203267       129      49     38  6647    0    13  203   0%      0   13    1    0 20103%
c i   13.9  767710  3203267       130      49     38  6647    0    13  203   0%      0   13    1    0 20025%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 2234 variables
c [simpleprobe-2] 648121 schedulable variables 85%
c [simpleprobe-2] limit 6396422 based on 3198211 irredundant clauses
c [decomp-4] removed 3798 variables
c [simpleprobe-2] 538121 variables remain 71% (223647 retained 29%)
c [simpleprobe-2] removed 3798 variables, found 25664 hbrs, 412 units
c [treelook-1] limit 795436 based on 3181744 irredundant clauses
c [treelook-1] scheduled 159058 literals 10%
c [treelook-1] scheduling used 795884 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 795436 based on 3181744 irredundant clauses
c [treelook-1] used 800828 steps
c [treelook-1] 158918 literals remain 10%
c [treelook-1] 157060 variables remain to probed next time 21%
c [decomp-5] removed 139 variables
c [treelook-1] removed 146 variables, found 2837 hbrs
c [basicprobe-1] limit 25449424 based on 3181178 irredundant clauses
c [basicprobe-1-0] 687219 probes remain 91% after last round
c [basicprobe-1-0] 3676 units = 1834 failed (50%) + 1842 lifted (50%)
c [basicprobe-1-0] removed 8920 variables, found 166164 hbrs
c [unhide-2] limit 198823 based on 3181178 irredundant clauses
c [unhide-2-2] 597 units, 906 failed, 10152 tauts, 0 hbrs, 27226 literals
c [elim-2] 750814 variables 100% will be scheduled this time
c [elim-2] scheduled 750814 variables 100%
c [elim-2] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 666341 not tried 89% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 84571 = 11% variables out of 750814 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 2795729 negative 95.1% of 2940351 except 144622 4.9%
c [phase-count-2] 2744358 positive 93.3% of 2940351 except 195993 6.7%
c [phase-2] phase bias: 799 positive 28%, 2046 negative 72%
c [sort-queue-2] sorted 666243 enqueued variables after 130 conflicts
c [score-dist-2] active 0 (0%), one 0 (0%), zero 666243 (100%)
c [score-dist-2] max exp 0, different 1 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 101467 variables 13.2% (666243 remain 61%)
c [simplification-2] removed 262916 irredundant clauses 8.2% (2940351 remain 67%)
c [simplification-2] maximum reduction of 13% = max (13%, 8%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1054 (hard 11000)
c [simplification-2] 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   32.7  666242  2940351       140      42     20 138260    0    14  195   0%      0   14    1    0 19614%
c i   32.8  666241  2940351       142      42     21 138260    0    14  195   0%      0   14    1    0 19507%
c i   32.8  666205  2940351       145      44     21 138260    0    14  195   0%      0   14    1    0 19327%
c i   33.3  666168  2940351       256     110     39 138285    0    30  195   0%      0   30    1    0 16711%
c i   33.4  666167  2940351       260     111     41 138285    0    31  195   0%      0   31    1    0 16550%
c i   33.4  666166  2940351       261     111     41 138285    0    31  195   0%      0   31    1    0 16485%
c i   33.4  666165  2940351       267     114     42 138286    0    31  195   0%      0   31    1    0 16300%
c i   33.4  666164  2940351       270     114     43 138287    0    32  195   0%      0   32    1    0 16160%
c i   33.5  666163  2940351       281     120     46 138288    0    34  195   0%      0   34    1    0 15902%
c i   33.5  666162  2940351       282     120     46 138288    0    34  195   0%      0   34    1    0 15840%
c i   33.5  666133  2940351       285     121     46 138289    0    34  195   0%      0   34    1    0 15705%
c i   33.8  665658  2940351       320     132     61 138296    0    43  195   0%      0   43    2    0 14810%
c i   34.5  665657  2940351       516     226    113 138339    0   103  195   0%      0  103    2    0 11244%
c i   34.5  665651  2940351       546     237    119 138351    0   114  195   0%      0  113    2    0 10807%
c i   34.5  665650  2940351       556     238    126 138352    0   114  195   0%      0  113    2    0 10599%
c 
c [simplification-3] limit of 148 binary hit after 148 binaries
c [card-2] limit 735087 based on 2940351 irredundant clauses
c [card-2] found 678 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 735087 for elimination
c [card-2] 678 out of 678 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 4644 variables
c [treelook-2] limit 732410 based on 2929642 irredundant clauses
c [treelook-2] scheduled 137319 literals 10%
c [treelook-2] scheduling used 732836 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 732410 based on 2929642 irredundant clauses
c [treelook-2] used 737761 steps
c [treelook-2] 137208 literals remain 10%
c [treelook-2] 84238 variables remain to probed next time 13%
c [decomp-7] removed 99 variables
c [treelook-2] removed 104 variables, found 2422 hbrs
c [unhide-3] limit 183065 based on 2929041 irredundant clauses
c [unhide-3-3] 296 units, 492 failed, 13151 tauts, 0 hbrs, 16937 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 660675 variables 100%
c [elim-3] limit of 10000000 steps penalty 1 = 0 + 1
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 511999 not tried 77% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 148676 = 23% variables out of 660675 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 2460552 negative 95.0% of 2591186 except 130634 5.0%
c [phase-count-3] 2405569 positive 92.8% of 2591186 except 185617 7.2%
c [phase-3] phase bias: 331 positive 23%, 1080 negative 77%
c [sort-queue-3] sorted 511999 enqueued variables after 591 conflicts
c [score-dist-3] active 0 (0%), one 0 (0%), zero 511999 (100%)
c [score-dist-3] max exp 0, different 1 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 153647 variables 23.1% (511999 remain 47%)
c [simplification-3] removed 349165 irredundant clauses 11.9% (2591186 remain 59%)
c [simplification-3] maximum reduction of 23% = max (23%, 12%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 1093 (hard 11000)
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   48.2  511998  2591186       604     162     97 94582    0   114  185   0%      0  114    2    0 10132%
c i   48.2  511997  2591186       608     162     99 94583    0   114  185   0%      0  114    2    0 10037%
c i   48.2  511996  2591186       610     163     99 94583    0   114  185   0%      0  114    2    0 9971%
c i   48.7  511995  2591185       718     215    120 94609    0   126  185   0%      0  126    2    0 8972%
c i   48.8  511994  2591185       719     215    120 94609    0   126  185   0%      0  126    2    0 8937%
c i   48.8  511993  2591185       723     216    120 94611    0   127  185   0%      0  127    2    0 8844%
c i   48.8  511992  2591185       724     216    120 94611    0   127  185   0%      0  127    2    0 8809%
c i   49.2  511991  2591185       815     255    143 94631    0   149  185   0%      0  148    2    0 8276%
c i   49.4  511990  2591185       889     299    159 94643    0   161  185   0%      0  160    2    0 7291%
c i   49.4  511989  2591185       895     303    160 94643    0   161  185   0%      0  160    2    0 7192%
c i   49.4  511988  2591185       896     303    160 94643    0   161  185   0%      0  160    2    0 7164%
c i   49.4  511987  2591185       900     305    160 94644    0   161  185   0%      0  160    2    0 7093%
c i   49.4  511986  2591185       909     306    166 94645    0   162  185   0%      0  160    2    0 7018%
c i   49.4  511985  2591185       912     308    166 94645    0   161  185   0%      0  160    2    0 6976%
c i   49.5  511984  2591185       935     319    170 94652    0   163  185   0%      0  162    2    0 6807%
c i   50.0  511983  2591185      1091     386    211 94695    0   212  185   0%      1  211    2    0 6247%
c i   50.2  511977  2591185      1136     410    225 94700    1   220  185   0%      1  219    2    0 6156%
c 
c [simplification-4] limit 1139 conflicts (hard 11000) hit after 1140 conflicts
c [decomp-8] removed 649 variables
c [basicprobe-2] limit 20716760 based on 2589595 irredundant clauses
c [basicprobe-2-0] 394054 probes remain 77% after last round
c [basicprobe-2-0] 1098 units = 1020 failed (93%) + 78 lifted (7%)
c [basicprobe-2-0] removed 1950 variables, found 107862 hbrs
c [unhide-4] limit 161849 based on 2589595 irredundant clauses
c [unhide-4-4] 272 units, 436 failed, 10176 tauts, 0 hbrs, 44842 literals
c [elim-4] 508791 variables 100% will be scheduled this time
c [elim-4] scheduled 508791 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 200000000 steps penalty 1 = 0 + 1
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 15652 not tried 3% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 240355 = 47% variables out of 508791 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 1830473 negative 95.7% of 1913627 except 83154 4.3%
c [phase-count-4] 1795254 positive 93.8% of 1913627 except 118373 6.2%
c [phase-4] phase bias: 358 positive 42%, 489 negative 58%
c [sort-queue-4] sorted 268437 enqueued variables after 1140 conflicts
c [score-dist-4] active 0 (0%), one 0 (0%), zero 268437 (100%)
c [score-dist-4] max exp 0, different 1 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 243537 variables 47.6% (268437 remain 24%)
c [simplification-4] removed 677558 irredundant clauses 26.1% (1913627 remain 44%)
c [simplification-4] maximum reduction of 48% = max (48%, 26%)
c [simplification-4] large reduction 48% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 13140 (soft 3140 + delta 10000)
c [simplification-4] new conflict limit 3140 (hard 13140)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   69.9  268436  1913626      1165     166    132 61280    1   221  170   0%      1  220    2    0 6163%
c i   69.9  268435  1913626      1166     166    132 61280    1   221  170   0%      1  220    2    0 6139%
c i   69.9  268434  1913626      1177     173    132 61283    1   221  170   0%      1  219    2    0 6083%
c i   70.0  268433  1913626      1183     176    132 61285    1   221  170   0%      1  220    2    0 6028%
c i   70.0  268432  1913626      1188     177    135 61285    1   222  170   0%      1  220    2    0 5982%
c i   70.0  268431  1913626      1197     181    137 61287    1   222  170   0%      1  220    2    0 5884%
c i   70.4  268430  1913626      1332     251    169 61314    1   233  170   0%      1  230    2    0 5180%
c i   70.5  268429  1913626      1371     267    181 61323    1   237  170   0%      1  235    2    0 4981%
c i   70.6  268428  1913626      1411     278    194 61337    1   241  170   0%      1  238    2    0 4689%
c i   70.7  268427  1913626      1461     296    208 61352    1   249  170   0%      1  247    2    0 4433%
c i   70.7  268426  1913626      1462     296    208 61352    1   249  170   0%      1  247    2    0 4415%
c i   70.8  268425  1913626      1484     306    213 61357    1   260  170   0%      1  257    2    0 4369%
c i   70.9  268424  1913626      1505     316    217 61362    1   268  170   0%      1  266    2    0 4390%
c i   71.1  268423  1913626      1613     342    246 61413    1   293  170   0%      1  290    2    0 4000%
c i   71.3  268422  1913626      1665     361    267 61421    1   309  170   0%      1  305    2    0 3902%
c i   71.3  268421  1913626      1692     367    273 61431    1   308  170   0%      1  304    2    0 3774%
c i   71.7  268420  1913626      1815     422    310 61455    1   314  170   0%      1  309    2    0 3558%
c i   71.8  268419  1913626      1859     446    322 61461    1   319  170   0%      1  315    2    0 3520%
c i   71.8  268418  1913626      1860     446    322 61461    1   319  170   0%      1  315    2    0 3506%
c i   71.8  268417  1913626      1861     446    322 61461    1   319  170   0%      1  315    2    0 3493%
c i   71.9  268416  1913626      1866     447    324 61462    1   319  170   0%      1  315    2    0 3495%
c i   71.9  268415  1913626      1873     449    326 61464    1   320  170   0%      1  315    2    0 3477%
c i   72.0  268414  1913626      1936     473    344 61483    1   328  170   0%      1  324    2    0 3293%
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   72.1  268413  1913626      1959     484    349 61489    1   332  170   0%      1  327    2    0 3247%
c i   72.1  268412  1913626      1960     484    349 61489    1   332  170   0%      1  327    2    0 3234%
c i   72.4  268411  1913626      2052     523    379 61507    1   354  170   0%      1  349    2    0 3222%
c i   72.7  268410  1913626      2147     563    409 61530    1   380  170   0%      1  374    2    0 3141%
c i   72.7  268367  1913626      2163     569    412 61534    1   379  170   0%      1  373    2    0 3101%
c i   72.7  268366  1913626      2178     572    420 61536    1   378  170   0%      1  372    2    0 3064%
c i   73.2  268365  1913626      2338     630    467 61581    1   383  170   0%      1  376    2    0 2798%
c i   73.2  268364  1913626      2358     640    474 61583    1   386  170   0%      1  379    2    0 2852%
c i   73.3  268363  1913626      2366     644    477 61583    1   388  170   0%      1  381    2    0 2831%
c i   73.3  268362  1913626      2368     645    477 61583    1   389  170   0%      1  382    2    0 2829%
c i   73.3  268361  1913626      2386     650    484 61588    1   389  170   0%      1  382    2    0 2768%
c i   73.3  268360  1913626      2387     650    484 61588    1   389  170   0%      1  382    2    0 2757%
c i   73.3  268359  1913626      2394     652    486 61589    1   389  170   0%      1  381    2    0 2722%
c i   73.5  268358  1913626      2478     673    513 61623    1   398  170   0%      1  390    2    0 2494%
c i   73.5  268357  1913626      2479     673    513 61623    1   398  170   0%      1  390    2    0 2485%
c i   73.5  268356  1913626      2481     674    513 61623    1   398  170   0%      1  390    2    0 2475%
c i   73.5  268355  1913626      2482     674    513 61623    1   398  170   0%      1  390    2    0 2465%
c i   73.5  268354  1913626      2489     678    514 61624    1   398  170   0%      1  390    2    0 2446%
c i   73.6  268353  1913626      2529     702    523 61630    1   407  170   0%      1  399    2    0 2522%
c i   73.8  268352  1913626      2595     733    540 61645    1   428  170   0%      1  419    2    0 2543%
c i   74.1  268351  1913626      2691     774    564 61671    1   454  170   0%      1  445    2    0 2514%
c i   74.1  268350  1913626      2695     775    564 61673    1   454  170   0%      1  445    2    0 2492%
c i   74.4  268349  1913625      2784     814    584 61700    1   452  170   0%      1  443    2    0 2382%
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   74.5  268341  1913625      2840     836    603 61713    1   456  170   0%      1  446    2    0 2308%
c i   74.6  268340  1913625      2880     857    614 61719    1   459  170   0%      1  449    2    0 2286%
c i   74.7  268339  1913625      2893     862    619 61721    1   461  170   0%      1  450    2    0 2343%
c i   74.7  268338  1913625      2894     862    619 61721    1   460  170   0%      1  450    2    0 2334%
c i   74.7  268337  1913625      2908     869    623 61722    1   463  170   0%      1  452    2    0 2350%
c i   74.7  268336  1913625      2910     870    623 61722    1   462  170   0%      1  452    2    0 2344%
c i   74.7  268335  1913625      2911     870    623 61722    1   462  170   0%      1  452    2    0 2335%
c i   75.0  268334  1913625      3021     917    655 61751    1   470  170   0%      1  459    2    0 2220%
c i   75.0  268333  1913625      3046     930    659 61758    1   472  170   0%      1  460    2    0 2198%
c i   75.1  268332  1913625      3082     941    670 61769    1   477  170   0%      1  466    2    0 2168%
c 
c [simplification-5] limit 3267 conflicts (hard 13140) hit after 3267 conflicts
c [quatres-1] found 236758 quaternary clauses 39% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-1] added 103 double-self-subsuming ternary resolvents
c [quatres-1-2] added 3022 single-self-subsuming ternary resolvents
c [quatres-1-2] added 7382 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 268332 free variables schedulable
c [ternres-1] 79053 ternary resolvents (791 bin, 78262 trn)
c [ternres-1] 25125 variables remain 9% (243207 retained 91%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 8796 xors of average arity 3.0
c [gauss-1] connected 26086 occurrences of 9498 variables (average 2.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-9] removed 1524 variables
c [simpleprobe-3] 190566 schedulable variables 71%
c [simpleprobe-3] limit 4522235 penalty 0 = 0 + 0
c [decomp-10] removed 197 variables
c [simpleprobe-3] 193297 variables remain 73% (73314 retained 27%)
c [simpleprobe-3] removed 197 variables, found 11684 hbrs, 40 units
c [unhide-5] limit 119219 based on 1907512 irredundant clauses
c [unhide-5-5] 189 units, 229 failed, 62169 tauts, 0 hbrs, 74897 literals
c [transred-1] limit 1857297 based on 1857297 irredundant clauses
c [transred-1] removed 855 transitive binary clauses
c [transred-1] found 17 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 266192 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 22394 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 28
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 27
c [cce-1-1] eliminated 3 clauses out of 5 (60%) of length 26
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 25
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 24
c [cce-1-1] eliminated 3 clauses out of 7 (43%) of length 23
c [cce-1-1] eliminated 1 clauses out of 5 (20%) of length 22
c [cce-1-1] eliminated 3 clauses out of 9 (33%) of length 21
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 20
c [cce-1-1] eliminated 18 clauses out of 29 (62%) of length 19
c [cce-1-1] eliminated 227 clauses out of 878 (26%) of length 18
c [cce-1-1] eliminated 97 clauses out of 1093 (9%) of length 17
c [cce-1-1] eliminated 242 clauses out of 764 (32%) of length 16
c [cce-1-1] eliminated 241 clauses out of 1436 (17%) of length 15
c [cce-1-1] eliminated 587 clauses out of 2351 (25%) of length 14
c [cce-1-1] eliminated 208 clauses out of 3805 (5%) of length 13
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1641 large clauses in 30000029 steps
c [cce-1-1] allowing another 15000014 steps for small clauses
c [cce-1-1] scheduling 1029067 clauses = 812952 binary + 216115 ternary
c [cce-1-1] tried to eliminate 6167 small clauses 1%
c [cce-1-1] eliminated 982 binary clauses 0%
c [cce-1-1] eliminated 243 ternary clauses 0%
c [cce-1-1] eliminated 1225 small clauses 0%
c [cce-1-1] eliminated 1225 small clauses in 30000063 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2866 covered clauses in round 1
c [cce-1] eliminated 2866 covered clauses in TOTAL during 1 rounds
c [cce-1] 2866 < 1/100 * 1830395 = 18303 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 265594 variables 100%
c [elim-5] limit of 22611178 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 157938 not tried 59% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 12590 = 5% variables out of 265594 scheduled
c [bca-1] limit of 10000000 steps and 3604308 added (scaled 2)
c [bca-1] 485879 out of 506010 literals actually usable 96%
c [bca-1] added 6293 blocked clauses in 1541484 steps
c [sweep-1] limit 3603808 based on 1801904 irredundant clauses
c [sweep-1-1] 108424 pos 42.9% + 144580 neg 57.1% = 253004 sched 100.0% ret 0
c [sweep-1-1] 3605409 steps 96 queries 81753.05 avg class size
c [sweep-1-1] 1179 decisions 89 SAT calls 34.36 avg env size
c [sweep-1-1] 252669 variables remain 100% (312 retained 0%)
c [decomp-11] removed 454 variables
c [sweep-1-1] removed 454 vars (0 failed, 28 eqs, 30 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 454 vars in TOTAL (1 rounds, 95 queries)
c [sort-queue-5] sorted 252550 enqueued variables after 3267 conflicts
c [score-dist-5] active 0 (0%), one 0 (0%), zero 252550 (100%)
c [score-dist-5] max exp 0, different 1 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 15782 variables 5.9% (252550 remain 23%)
c [simplification-5] removed 113126 irredundant clauses 5.9% (1800499 remain 41%)
c [simplification-5] maximum reduction of 6% = max (6%, 6%)
c [simplification-5] large reduction 6% >= 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 15267 (soft 5267 + delta 10000)
c [simplification-5] new conflict limit 5267 (hard 15267)
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   94.3  252549  1800499      3284    6919  61489 75201    1   506  171   0%      1  493    2    0 2120%
c i   94.3  252548  1800498      3318    6929  61499 75212    1   504  171   0%      1  491    2    0 2128%
c i   94.5  252539  1800498      3368    6956  61508 75225    1   502  171   0%      1  488    2    0 2092%
c i   94.5  252538  1800498      3405    6963  61523 75239    1   500  171   0%      1  486    2    0 2030%
c i   94.7  252537  1800498      3457    6985  61535 75255    1   502  171   0%      1  488    2    0 1963%
c i   94.7  252536  1800498      3463    6985  61531 75263    1   503  171   0%      1  488    2    0 1946%
c i   94.7  252535  1800498      3464    6985  61531 75263    1   503  171   0%      1  488    2    0 1938%
c i   94.8  252534  1800498      3479    6988  61538 75267    1   502  171   0%      1  487    2    0 1904%
c i   94.8  252533  1800498      3502    6997  61541 75275    1   504  171   0%      1  490    2    0 1868%
c i   94.9  252532  1800498      3514    7001  61545 75278    1   506  171   0%      1  491    2    0 1874%
c i   94.9  252531  1800498      3521    7002  61548 75280    1   506  171   0%      1  491    2    0 1855%
c i   94.9  252530  1800498      3530    7005  61551 75282    1   507  171   0%      1  492    2    0 1829%
c i   95.1  252529  1800498      3604    7029  61583 75298    1   510  171   0%      1  495    2    0 1766%
c i   95.1  252528  1800498      3614    7032  61585 75301    1   511  171   0%      1  495    2    0 1749%
c i   95.6  252527  1800498      3788    7111  61639 75336    1   547  171   0%      1  530    2    0 1788%
c i   95.6  252526  1800498      3789    7111  61639 75336    1   547  171   0%      1  530    2    0 1781%
c i   95.6  252525  1800498      3793    7112  61640 75336    1   547  171   0%      1  530    2    0 1777%
c i   95.9  252524  1800498      3920    7170  61676 75362    1   548  171   0%      1  530    2    0 1774%
c i   96.1  252523  1800498      4001    7207  61695 75384    1   552  171   0%      1  533    2    0 1719%
c i   96.2  252522  1800498      4003    7207  61696 75384    1   552  171   0%      1  533    2    0 1712%
c i   96.2  252521  1800498      4033    7218  61702 75396    1   552  171   0%      1  534    2    0 1654%
c i   96.5  252520  1800498      4177    7277  61754 75426    1   568  171   0%      1  548    2    0 1617%
c i   96.7  252519  1800498      4228    7294  61776 75435    1   578  171   0%      1  558    2    0 1604%
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   96.9  252518  1800498      4307    7319  61803 75461    1   586  171   0%      1  564    2    0 1564%
c i   97.4  252517  1800498      4546    7393  61859 75551    1   577  171   0%      1  554    2    0 1429%
c i   97.5  252516  1800498      4570    7401  61865 75560    1   580  171   0%      1  556    2    0 1395%
c i   97.5  252515  1800498      4571    7401  61865 75560    1   579  171   0%      1  556    2    0 1390%
c i   97.5  252514  1800498      4572    7401  61865 75560    1   579  171   0%      1  556    2    0 1385%
c i   97.7  252513  1800498      4653    7433  61892 75577    1   579  171   0%      1  555    2    0 1322%
c i   97.7  252512  1800498      4658    7436  61893 75577    1   579  171   0%      1  555    2    0 1316%
c i   97.7  252511  1800498      4696    7453  61904 75586    1   579  171   0%      1  555    2    0 1299%
c i   97.7  252510  1800498      4698    7454  61904 75586    1   579  171   0%      1  555    2    0 1291%
c i   97.8  252509  1800498      4710    7455  61912 75588    1   581  171   0%      1  556    2    0 1283%
c i   98.2  252508  1800498      4847    7515  61954 75620    1   602  171   0%      1  576    2    0 1319%
c i   98.8  252507  1800498      5055    7617  62001 75670    1   599  171   0%      1  572    2    0 1358%
c i   98.9  252506  1800498      5093    7627  62015 75683    1   600  171   0%      1  572    2    0 1311%
c i   99.0  252505  1800498      5176    7660  62044 75701    1   603  171   0%      1  575    2    0 1269%
c i   99.0  252504  1800498      5177    7660  62044 75701    1   603  171   0%      1  575    2    0 1264%
c i   99.3  252503  1800498      5271    7702  62072 75721    1   630  171   0%      1  601    2    0 1277%
c i   99.3  252502  1800498      5304    7711  62079 75735    1   633  171   0%      1  603    2    0 1241%
c 
c [simplification-6] limit 5335 conflicts (hard 15267) hit after 5335 conflicts
c [quatres-2] found 241489 quaternary clauses 40% in total
c [quatres-2-1] removed 29 duplicate quaternary clauses
c [quatres-2-1] added 26 double-self-subsuming ternary resolvents
c [quatres-2-2] added 1944 single-self-subsuming ternary resolvents
c [quatres-2-2] added 5797 quaternary resolvents
c [ternres-2] limit 7201352 based on 1800338 irredundant clauses
c [ternres-2] 23182 schedulable variables 9%
c [ternres-2] 36335 ternary resolvents (1578 bin, 34757 trn)
c [ternres-2] 14465 variables remain 6% (238037 retained 94%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 242 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] 242 out of 242 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 8048 xors of average arity 3.0
c [gauss-2] connected 24021 occurrences of 8146 variables (average 2.9)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 520 variables
c [treelook-3] limit 449743 based on 1798973 irredundant clauses
c [treelook-3] scheduled 54096 literals 11%
c [treelook-3] scheduling used 450243 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 449743 based on 1798973 irredundant clauses
c [treelook-3] used 453420 steps
c [treelook-3] 54059 literals remain 11%
c [treelook-3] 31167 variables remain to probed next time 12%
c [decomp-13] removed 26 variables
c [treelook-3] removed 26 variables, found 879 hbrs
c [unhide-6] limit 112430 based on 1798893 irredundant clauses
c [unhide-6-6] 210 units, 583 failed, 6893 tauts, 0 hbrs, 43005 literals
c [transred-2] limit 1796244 based on 1796244 irredundant clauses
c [transred-2] removed 835 transitive binary clauses
c [transred-2] found 19 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 251191 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 15375 blocked clauses
c [block-2] 15375 < 1/100 * 1795616 = 17956 considered unsuccessful
c [elim-6] 15318 variables 6% will be scheduled this time
c [elim-6] scheduled 15318 variables 6%
c [elim-6] limit of 33847607 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 7126 not tried 3% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 86 = 1% variables out of 15318 scheduled
c [elim-6] 86 < 1/100 * 15318 = 153 considered unsuccessful
c [bca-2] limit of 10000000 steps and 3509434 added (scaled 2)
c [bca-2] 470580 out of 501900 literals actually usable 94%
c [bca-2] added 1850 blocked clauses in 1473694 steps
c [sweep-2] limit 3505788 based on 1752894 irredundant clauses
c [sweep-2-1] 106665 pos 42.6% + 144008 neg 57.4% = 250673 sched 99.9% ret 276
c [sweep-2-1] 3531351 steps 95 queries 79800.22 avg class size
c [sweep-2-1] 1134 decisions 85 SAT calls 32.67 avg env size
c [sweep-2-1] 250196 variables remain 100% (747 retained 0%)
c [decomp-14] removed 669 variables
c [sweep-2-1] removed 669 vars (0 failed, 15 eqs, 26 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 669 vars in TOTAL (1 rounds, 94 queries)
c [sort-queue-6] sorted 250280 enqueued variables after 5335 conflicts
c [score-dist-6] active 0 (0%), one 0 (0%), zero 250280 (100%)
c [score-dist-6] max exp 0, different 1 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 2222 variables 0.9% (250280 remain 23%)
c [simplification-6] removed 49346 irredundant clauses 2.7% (1751152 remain 40%)
c [simplification-6] maximum reduction of 3% = max (1%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 5000
c [simplification-6] penalized conflict interval 5000 = 1 * 5000
c [simplification-6] hard conflict limit 20335 (soft 10335 + delta 10000)
c [simplification-6] new conflict limit 10335 (hard 20335)
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  114.5  250279  1751152      5521   12824  85242 81244    1   626  171   0%      1  595    2    0 1185%
c i  114.5  250278  1751152      5546   12834  85252 81248    1   625  171   0%      1  594    2    0 1177%
c i  114.5  250277  1751152      5547   12834  85252 81248    1   625  171   0%      1  594    2    0 1172%
c i  114.6  250276  1751152      5555   12839  85253 81249    1   626  171   0%      1  594    2    0 1171%
c i  114.6  250275  1751152      5585   12851  85262 81257    1   626  171   0%      1  594    2    0 1173%
c i  114.7  250274  1751152      5597   12856  85265 81259    1   626  171   0%      1  594    2    0 1174%
c i  114.7  250273  1751152      5600   12857  85265 81260    1   626  171   0%      1  593    2    0 1166%
c i  114.7  250272  1751152      5601   12857  85265 81260    1   625  171   0%      1  593    2    0 1161%
c i  114.7  250271  1751152      5606   12860  85266 81260    1   625  171   0%      1  593    2    0 1155%
c i  114.9  250270  1751152      5676   12884  85287 81284    1   627  171   0%      1  594    2    0 1108%
c i  114.9  250269  1751152      5687   12886  85292 81287    1   626  171   0%      1  593    2    0 1094%
c i  115.2  250268  1751152      5780   12940  85314 81302    1   650  171   0%      1  617    2    0 1166%
c i  115.2  250267  1751152      5787   12943  85317 81302    1   650  171   0%      1  616    2    0 1168%
c i  115.2  250266  1751152      5816   12953  85324 81309    1   657  171   0%      1  623    2    0 1173%
c i  115.4  250265  1751152      5893   12996  85345 81320    1   668  171   0%      1  633    2    0 1174%
c i  115.9  250264  1751152      6089   13082  85411 81360    2   659  171   0%      1  623    2    0 1211%
c i  115.9  250263  1751152      6095   13085  85412 81361    2   659  171   0%      1  623    2    0 1204%
c i  115.9  250262  1751152      6098   13086  85412 81361    2   659  171   0%      1  622    2    0 1227%
c i  116.0  250256  1751152      6121   13094  85421 81366    2   660  171   0%      1  623    2    0 1211%
c i  116.0  250255  1751152      6125   13094  85423 81367    2   660  171   0%      1  623    2    0 1202%
c i  116.3  250254  1751152      6213   13135  85454 81379    2   663  171   0%      1  625    2    0 1150%
c i  116.8  250253  1751152      6416   13234  85520 81412    2   692  171   0%      1  652    2    0 1164%
c i  117.5  250252  1751152      6643   13320  85611 81456    2   682  171   0%      1  640    2    0 1124%
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  117.8  250157  1751152      6712   13345  85634 81474    2   683  171   0%      1  641    2    0 1087%
c i  117.8  250156  1751152      6723   13351  85635 81477    2   686  171   0%      1  643    2    0 1091%
c i  117.8  250155  1751152      6742   13361  85641 81479    2   686  171   0%      1  643    2    0 1079%
c i  117.8  250154  1751152      6748   13361  85645 81480    2   686  171   0%      1  643    2    0 1070%
c i  117.9  250153  1751152      6752   13362  85645 81482    2   686  171   0%      1  643    2    0 1065%
c i  118.2  250152  1751152      6885   13419  85688 81512    2   706  171   0%      1  662    2    0 1086%
c i  118.5  250151  1751152      6979   13473  85705 81534    2   725  171   0%      1  680    2    0 1107%
c i  119.0  250150  1751151      7140   13551  85750 81566    2   715  171   0%      1  668    2    0 1135%
c i  119.1  250149  1751151      7143   13553  85750 81566    2   715  171   0%      1  668    2    0 1129%
c i  119.1  250148  1751151      7148   13554  85752 81567    2   715  171   0%      1  668    2    0 1127%
c i  119.4  250147  1751151      7234   13599  85776 81581    2   714  171   0%      1  666    2    0 1142%
c i  119.5  250146  1751151      7250   13604  85780 81587    2   715  171   0%      1  667    2    0 1117%
c i  119.9  250145  1751151      7379   13658  85826 81612    2   723  171   0%      1  674    2    0 1056%
c i  120.3  250144  1751151      7545   13745  85866 81646    2   759  171   0%      1  708    2    0 1120%
c i  120.6  250143  1751151      7669   13795  85888 81696    2   746  171   0%      1  694    2    0 1002%
c i  120.7  250142  1751151      7697   13807  85901 81698    2   745  171   0%      1  693    2    0 1002%
c i  120.7  250141  1751151      7704   13811  85901 81700    2   746  171   0%      1  693    2    0  998%
c i  120.9  250137  1751151      7747   13833  85912 81709    2   747  171   0%      1  694    2    0  994%
c i  120.9  250136  1751151      7750   13834  85913 81709    2   747  171   0%      1  694    2    0  990%
c i  121.1  250135  1751151      7844   13874  85937 81736    2   749  171   0%      1  695    2    0  944%
c i  121.2  250134  1751151      7853   13878  85938 81739    2   749  171   0%      1  695    2    0  931%
c i  121.6  250133  1751151      7962   13923  85975 81763    2   777  171   0%      1  722    2    0 1049%
c i  121.7  250131  1751151      8025   13953  85989 81780    2   795  171   0%      1  739    2    0 1061%
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  121.8  250114  1751151      8040   13958  85994 81783    2   793  171   0%      1  737    2    0 1064%
c i  122.6  250113  1751151      8304   14080  86047 81862    2   780  171   0%      1  721    2    0  913%
c i  122.7  250112  1751151      8326   14091  86052 81866    2   779  171   0%      1  720    2    0  897%
c i  123.2  250111  1751150      8468   14156  86082 81907    2   793  171   0%      1  732    2    0  944%
c 
c [simplification-7] limit of 2543 ternary hit after 2543 ternaries
c [quatres-3] found 242468 quaternary clauses 42% in total
c [quatres-3-1] removed 10 duplicate quaternary clauses
c [quatres-3-1] added 26 double-self-subsuming ternary resolvents
c [quatres-3-2] added 590 single-self-subsuming ternary resolvents
c [quatres-3-2] added 3926 quaternary resolvents
c [ternres-3] limit 7004404 based on 1751101 irredundant clauses
c [ternres-3] 14076 schedulable variables 6%
c [ternres-3] 42886 ternary resolvents (1520 bin, 41366 trn)
c [ternres-3] 7928 variables remain 3% (242183 retained 97%)
c [decomp-15] removed 764 variables
c [basicprobe-3] limit 15262470 penalty 0 = 0 + 0
c [basicprobe-3-0] 173828 probes remain 70% after last round
c [basicprobe-3-0] 506 units = 492 failed (97%) + 14 lifted (3%)
c [basicprobe-3-0] removed 998 variables, found 37144 hbrs
c [bate-1] eliminated 747 asymmetric tautologies during probing
c [unhide-7] limit 109201 based on 1747225 irredundant clauses
c [unhide-7-7] 149 units, 234 failed, 25843 tauts, 0 hbrs, 20218 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 846 transitive binary clauses
c [transred-3] found 6 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 4 clauses out of 4 (100%) of length 23
c [cce-2-1] eliminated 2 clauses out of 3 (67%) of length 22
c [cce-2-1] eliminated 2 clauses out of 9 (22%) of length 20
c [cce-2-1] eliminated 4 clauses out of 610 (1%) of length 18
c [cce-2-1] eliminated 7 clauses out of 844 (1%) of length 17
c [cce-2-1] eliminated 14 clauses out of 659 (2%) of length 16
c [cce-2-1] eliminated 24 clauses out of 1260 (2%) of length 15
c [cce-2-1] eliminated 64 clauses out of 1452 (4%) of length 14
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 121 large clauses in 15000006 steps
c [cce-2-1] allowing another 7500003 steps for small clauses
c [cce-2-1] scheduling 956658 clauses = 740349 binary + 216309 ternary
c [cce-2-1] tried to eliminate 3745 small clauses 0%
c [cce-2-1] eliminated 527 binary clauses 0%
c [cce-2-1] eliminated 208 ternary clauses 0%
c [cce-2-1] eliminated 735 small clauses 0%
c [cce-2-1] eliminated 4686 small clauses in 15000156 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 4807 covered clauses in round 1
c [cce-2] eliminated 4807 covered clauses in TOTAL during 1 rounds
c [cce-2] 4807 < 1/100 * 1714379 = 17143 considered unsuccessful
c [bca-3] limit of 10000000 steps and 3423715 added (scaled 2)
c [bca-3] 455534 out of 496192 literals actually usable 92%
c [bca-3] added 220 blocked clauses in 1403166 steps
c [sweep-3] limit 3419144 based on 1709572 irredundant clauses
c [sweep-3-1] 101803 pos 41.2% + 145570 neg 58.8% = 247373 sched 99.7% ret 722
c [sweep-3-1] 3446630 steps 90 queries 73857.17 avg class size
c [sweep-3-1] 1048 decisions 81 SAT calls 34.96 avg env size
c [sweep-3-1] 246967 variables remain 100% (1126 retained 0%)
c [decomp-16] removed 1211 variables
c [sweep-3-1] removed 1211 vars (0 failed, 24 eqs, 33 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 1211 vars in TOTAL (1 rounds, 89 queries)
c [sort-queue-7] sorted 246884 enqueued variables after 8910 conflicts
c [score-dist-7] active 0 (0%), one 0 (0%), zero 246884 (100%)
c [score-dist-7] max exp 0, different 1 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 3227 variables 1.3% (246884 remain 23%)
c [simplification-7] removed 44207 irredundant clauses 2.5% (1706943 remain 39%)
c [simplification-7] maximum reduction of 3% = max (1%, 3%)
c [simplification-7] forced so keeping old conflict interval 5000
c [simplification-7] conflict limit remains at 10381 (hard 20335)
c [simplification-7] new ternary interval 10000
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  136.8  246883  1706943      9191   17866 112082 108686    2   794  171   0%      4  725    3    0  975%
c i  137.0  246882  1706943      9268   17897 112103 108705    2   799  171   0%      3  729    3    0  980%
c i  137.4  246881  1706943      9363   17948 112132 108718    2   812  171   0%      3  741    3    0  939%
c i  137.4  246880  1706943      9375   17951 112136 108722    2   813  171   0%      3  742    3    0  919%
c i  137.7  246879  1706943      9444   17989 112152 108735    2   830  171   0%      3  759    3    0  936%
c i  137.8  246878  1706943      9465   18001 112156 108738    2   829  171   0%      3  757    3    0  923%
c i  138.0  246857  1706943      9501   18014 112168 108747    2   824  171   0%      3  751    2    0  890%
c i  139.3  246856  1706943      9827   18197 112254 108800    2   840  171   0%      3  764    3    0  872%
c i  140.3  246855  1706943     10060   18339 112299 108836    2   839  171   0%      3  760    3    0  885%
c i  140.5  246854  1706943     10085   18353 112306 108839    2   837  171   0%      2  758    3    0  885%
c i  140.5  246853  1706943     10088   18354 112307 108839    2   837  171   0%      2  758    3    0  880%
c i  140.7  246852  1706943     10131   18373 112323 108845    2   834  171   0%      2  755    3    0  854%
c i  140.8  246851  1706943     10159   18386 112333 108848    2   834  171   0%      2  754    3    0  850%
c 
c [simplification-8] limit 10384 conflicts (hard 20335) hit after 10384 conflicts
c [quatres-4] found 241458 quaternary clauses 43% in total
c [quatres-4-1] removed 115 duplicate quaternary clauses
c [quatres-4-1] added 10 double-self-subsuming ternary resolvents
c [quatres-4-2] added 583 single-self-subsuming ternary resolvents
c [quatres-4-2] added 2100 quaternary resolvents
c [ternres-4] limit 6827524 based on 1706881 irredundant clauses
c [ternres-4] 7721 schedulable variables 3%
c [ternres-4] 40152 ternary resolvents (1215 bin, 38937 trn)
c [ternres-4] 5081 variables remain 2% (241770 retained 98%)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 3477 xors of average arity 3.0
c [gauss-3] connected 10375 occurrences of 4009 variables (average 2.6)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 326 variables
c [simpleprobe-4] 178636 schedulable variables 72%
c [simpleprobe-4] limit 15631634 penalty 0 = 0 + 0
c [decomp-18] removed 1056 variables
c [simpleprobe-4] 185721 variables remain 76% (59748 retained 24%)
c [simpleprobe-4] removed 1056 variables, found 36793 hbrs, 225 units
c [unhide-8] limit 106231 based on 1699701 irredundant clauses
c [unhide-8-8] 209 units, 435 failed, 15171 tauts, 0 hbrs, 22178 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 955 transitive binary clauses
c [transred-4] found 16 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 244808 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 3883 blocked clauses
c [block-3] 3883 < 1/100 * 1696665 = 16966 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 244642 variables 100%
c [elim-7] limit of 39079086 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 94326 not tried 39% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 10741 = 4% variables out of 244642 scheduled
c [bca-4] limit of 10000000 steps and 3332911 added (scaled 2)
c [bca-4] 427308 out of 467804 literals actually usable 91%
c [bca-4] added 921 blocked clauses in 1336471 steps
c [sweep-4] limit 3328230 based on 1664115 irredundant clauses
c [sweep-4-1] 94777 pos 40.7% + 138109 neg 59.3% = 232886 sched 99.6% ret 1015
c [sweep-4-1] 3365698 steps 72 queries 47411.76 avg class size
c [sweep-4-1] 849 decisions 63 SAT calls 34.38 avg env size
c [sweep-4-1] 232431 variables remain 99% (1468 retained 1%)
c [decomp-19] removed 558 variables
c [sweep-4-1] removed 558 vars (0 failed, 9 eqs, 13 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 558 vars in TOTAL (1 rounds, 71 queries)
c [sort-queue-8] sorted 233343 enqueued variables after 10384 conflicts
c [score-dist-8] active 0 (0%), one 0 (0%), zero 233343 (100%)
c [score-dist-8] max exp 0, different 1 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 13508 variables 5.5% (233343 remain 21%)
c [simplification-8] removed 44998 irredundant clauses 2.6% (1661945 remain 38%)
c [simplification-8] maximum reduction of 5% = max (5%, 3%)
c [simplification-8] large reduction 5% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 22384 (soft 12384 + delta 10000)
c [simplification-8] new conflict limit 12384 (hard 22384)
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  158.3  233342  1661945     10526   18468 116732 118396    2   835  171   0%      2  751    2    0  781%
c i  158.6  233341  1661945     10582   18500 116749 118401    2   833  171   0%      2  749    2    0  751%
c i  159.4  233340  1661945     10799   18615 116808 118438    2   863  171   0%      2  776    2    0  757%
c i  159.4  233339  1661945     10801   18615 116808 118439    2   863  171   0%      2  775    2    0  752%
c i  160.2  233337  1661942     11019   18729 116859 118487    2   850  171   0%      2  760    3    0  800%
c i  161.2  233336  1661942     11242   18844 116925 118524    2   868  171   0%      2  776    3    0  770%
c i  162.2  233335  1661942     11488   18979 116987 118567    2   862  171   0%      2  766    3    0  740%
c i  164.1  233334  1661941     11986   19262 117107 118652    2   873  171   0%      3  773    3    0  728%
c i  164.3  233333  1661941     12020   19282 117108 118662    2   874  171   0%      3  773    3    0  717%
c i  164.5  233332  1661941     12069   19309 117120 118671    2   877  171   0%      2  775    3    0  703%
c 
c [simplification-9] limit 12389 conflicts (hard 22384) hit after 12389 conflicts
c [quatres-5] found 245246 quaternary clauses 43% in total
c [quatres-5-1] removed 87 duplicate quaternary clauses
c [quatres-5-1] added 13 double-self-subsuming ternary resolvents
c [quatres-5-2] added 1377 single-self-subsuming ternary resolvents
c [quatres-5-2] added 3636 quaternary resolvents
c [ternres-5] limit 6647168 based on 1661792 irredundant clauses
c [ternres-5] 4801 schedulable variables 2%
c [ternres-5] 38221 ternary resolvents (1072 bin, 37149 trn)
c [ternres-5] 2907 variables remain 1% (230425 retained 99%)
c [decomp-20] removed 350 variables
c [treelook-4] limit 503656 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 56684 literals 12%
c [treelook-4] scheduling used 503668 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 503656 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 546091 steps
c [treelook-4] 56554 literals remain 12%
c [treelook-4] 24332 variables remain to probed next time 10%
c [decomp-21] removed 12 variables
c [treelook-4] removed 16 variables, found 762 hbrs
c [unhide-9] limit 251828 with penalty 2 = 0 + 2
c [unhide-9-9] 83 units, 178 failed, 18962 tauts, 0 hbrs, 15886 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 858 transitive binary clauses
c [transred-5] found 15 units
c [elim-8] 7002 variables 3% will be scheduled this time
c [elim-8] scheduled 7002 variables 3%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2014626080 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1 variables 0% in round 1 in 447876307 steps
c [elim-8-1] backward subsumption/strengthening limit 447876300
c [elim-8-1-1] backward checking 35957 touched variables 15%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1983 and strengthened 4708 clauses in 115645240 steps
c [elim-8-1] rescheduled 13369 variables 6% by backward subsumption
c [elim-8-2] eliminated 417 variables 0% in round 2 in 213148258 steps
c [elim-8-2] backward subsumption/strengthening limit 213148200
c [elim-8-2-1] backward checking 9607 touched variables 4%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 566 and strengthened 751 clauses in 34216183 steps
c [elim-8-2] rescheduled 3133 variables 1% by backward subsumption
c [elim-8-3] eliminated 124 variables 0% in round 3 in 42991874 steps
c [elim-8-3] backward subsumption/strengthening limit 42991800
c [elim-8-3-1] backward checking 1616 touched variables 1%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 50 and strengthened 132 clauses in 6730004 steps
c [elim-8] incomplete 501 not tried 0% in round 3
c [elim-8] transition to [ all 0 rem 1 ] state
c [elim-8] eliminated 621 = 9% variables out of 7002 scheduled
c [elim-8] 621 < 1/100 * 7002 = 70 considered unsuccessful
c [bca-5] limit of 10000000 steps and 3235602 added (scaled 2)
c [bca-5] 417636 out of 464138 literals actually usable 90%
c [bca-5] added 749 blocked clauses in 1305546 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 15109690 penalty 0 = 0 + 0
c [sweep-5-1] 92919 pos 40.3% + 137702 neg 59.7% = 230621 sched 99.4% ret 1447
c [sweep-5-1] 15123669 steps 314 queries 40341.48 avg class size
c [sweep-5-1] 4178 decisions 304 SAT calls 36.18 avg env size
c [sweep-5-1] 227956 variables remain 98% (4096 retained 2%)
c [decomp-22] removed 742 variables
c [sweep-5-1] removed 742 vars (0 failed, 25 eqs, 44 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 742 vars in TOTAL (1 rounds, 313 queries)
c [sort-queue-9] sorted 231326 enqueued variables after 12389 conflicts
c [score-dist-9] active 0 (0%), one 0 (0%), zero 231326 (100%)
c [score-dist-9] max exp 0, different 1 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 2006 variables 0.9% (231326 remain 21%)
c [simplification-9] removed 49481 irredundant clauses 3.0% (1612457 remain 37%)
c [simplification-9] maximum reduction of 3% = max (1%, 3%)
c [simplification-9] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-9] new conflict interval 10000
c [simplification-9] penalized conflict interval 10000 = 1 * 10000
c [simplification-9] hard conflict limit 32389 (soft 22389 + delta 10000)
c [simplification-9] new conflict limit 22389 (hard 32389)
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  190.4  231325  1612457     12846   22703 132291 120280    2   891  169   0%      5  780    2    0  608%
c i  190.4  231304  1612457     12856   22705 132294 120284    2   889  169   0%      5  778    2    0  598%
c i  191.7  231303  1612457     13145   22867 132357 120341    2   883  169   0%      4  769    3    0  626%
c i  192.0  231302  1612457     13226   22917 132372 120354    2   894  169   0%      4  778    3    0  641%
c i  192.0  231301  1612457     13227   22917 132372 120354    2   893  169   0%      4  778    3    0  638%
c i  192.2  231300  1612457     13291   22946 132387 120371    2   896  169   0%      3  780    3    0  636%
c i  192.2  231299  1612457     13294   22947 132387 120372    2   896  169   0%      3  780    3    0  632%
c i  192.2  231298  1612457     13302   22950 132388 120375    2   894  169   0%      3  778    3    0  631%
c i  192.5  231297  1612457     13364   22990 132404 120380    2   888  169   0%      3  771    3    0  631%
c i  192.7  231296  1612457     13412   23027 132412 120381    2   886  169   0%      3  769    3    0  665%
c i  193.2  231295  1612457     13533   23103 132439 120394    2   886  169   0%      3  767    3    0  631%
c i  194.1  231294  1612457     13735   23215 132484 120435    2   900  169   0%      3  779    3    0  613%
c i  194.2  231222  1612457     13757   23221 132492 120441    2   896  169   0%      2  775    3    0  604%
c i  194.2  231221  1612457     13765   23223 132496 120441    2   895  169   0%      2  773    3    0  601%
c i  194.6  231220  1612457     13879   23292 132514 120467    2   883  169   0%      2  760    3    0  606%
c i  195.5  231219  1612457     14075   23402 132563 120500    2   886  169   0%      2  761    2    0  551%
c i  196.6  231218  1612457     14332   23555 132620 120543    2   892  169   0%      2  764    3    0  586%
c i  196.6  231217  1612457     14339   23558 132623 120543    2   893  169   0%      2  764    3    0  591%
c i  197.7  231216  1612457     14545   23675 132669 120584    2   912  169   0%      2  781    3    0  641%
c i  197.7  231215  1612457     14565   23687 132674 120585    2   916  169   0%      2  785    3    0  634%
c i  198.3  231165  1612457     14702   23775 132700 120605    2   911  169   0%      2  779    3    0  625%
c i  198.7  231163  1612457     14781   23820 132717 120618    2   905  169   0%      2  771    3    0  599%
c i  198.8  231161  1612457     14811   23837 132723 120624    2   905  169   0%      2  771    3    0  592%
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  199.0  231160  1612457     14857   23858 132738 120633    2   903  169   0%      1  769    3    0  567%
c i  199.0  231159  1612457     14865   23861 132740 120635    2   903  169   0%      1  769    3    0  562%
c i  199.7  231158  1612457     15022   23947 132779 120662    2   923  169   0%      1  786    3    0  580%
c i  199.7  231157  1612457     15027   23947 132781 120664    2   922  169   0%      1  785    3    0  572%
c i  199.7  231156  1612457     15031   23948 132782 120665    2   921  169   0%      1  784    3    0  568%
c i  199.9  231155  1612457     15095   23993 132796 120669    2   915  169   0%      1  778    3    0  589%
c i  202.7  231154  1612457     15776   24357 132979 120790    2   941  169   0%      3  795    3    0  549%
c i  203.1  231153  1612457     15860   24404 133000 120803    3   961  169   0%      3  815    3    0  584%
c i  203.7  231152  1612457     16040   24516 133036 120827    3   945  169   0%      3  797    3    1  581%
c i  203.9  231151  1612457     16067   24530 133043 120832    3   945  169   0%      3  796    3    1  574%
c i  204.9  231150  1612457     16317   24667 133107 120874    3   975  169   0%      2  823    3    1  533%
c i  205.0  231149  1612457     16345   24686 133112 120876    3   972  169   0%      2  820    3    1  542%
c i  205.2  231148  1612457     16404   24721 133127 120884    3   966  169   0%      2  813    3    1  531%
c i  206.6  231147  1612457     16727   24908 133193 120948    3   998  169   0%      2  841    3    1  529%
c i  208.0  231146  1612457     17063   25131 133264 120984    3   983  169   0%      2  822    3    1  550%
c i  208.1  231145  1612457     17075   25137 133267 120986    3   983  169   0%      2  822    3    1  545%
c i  208.6  231144  1612457     17236   25212 133313 121020    3   995  169   0%      2  832    3    1  509%
c i  208.8  231140  1612457     17273   25234 133322 121025    3   990  169   0%      2  826    3    1  517%
c i  208.9  231134  1612457     17297   25249 133327 121027    3   987  169   0%      2  823    3    1  523%
c i  212.9  231130  1612457     18168   25789 133511 121158    3   991  169   0%      5  817    3    1  523%
c i  213.2  231129  1612457     18228   25830 133526 121161    3   990  169   0%      5  814    3    1  521%
c i  214.3  231128  1612457     18448   25950 133585 121201    3  1005  169   0%      4  827    3    1  483%
c i  214.3  231127  1612457     18451   25950 133585 121203    3  1005  169   0%      4  826    3    1  479%
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  214.3  231126  1612457     18453   25950 133585 121204    3  1004  169   0%      4  826    3    1  476%
c i  214.4  231125  1612457     18461   25956 133585 121205    3  1002  169   0%      4  824    3    1  476%
c i  215.2  231124  1612457     18611   26048 133616 121230    3   985  169   0%      4  805    3    1  482%
c i  215.3  231123  1612457     18633   26062 133621 121231    3   983  169   0%      3  802    3    1  493%
c i  215.6  231122  1612457     18696   26099 133642 121235    3   986  169   0%      3  804    3    1  490%
c 
c [simplification-10] limit of 3733 binary hit after 3733 binaries
c [quatres-6] found 241569 quaternary clauses 45% in total
c [quatres-6-1] removed 195 duplicate quaternary clauses
c [quatres-6-1] added 11 double-self-subsuming ternary resolvents
c [quatres-6-2] added 333 single-self-subsuming ternary resolvents
c [quatres-6-2] added 2006 quaternary resolvents
c [ternres-6] limit 8996661 with penalty 0 = 0 + 0
c [ternres-6] 2866 schedulable variables 1%
c [ternres-6] 50100 ternary resolvents (1386 bin, 48714 trn)
c [ternres-6] 576 variables remain 0% (230546 retained 100%)
c [card-4] limit 562291 penalty 3 = 3 + 0
c [card-4] found 342 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 562291 for elimination
c [card-4] 342 out of 342 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-23] removed 768 variables
c [basicprobe-4] limit 44983307 penalty 0 = 0 + 0
c [basicprobe-4-0] 138675 probes remain 61% after last round
c [basicprobe-4-0] 1356 units = 1170 failed (86%) + 186 lifted (14%)
c [basicprobe-4-0] removed 2216 variables, found 58172 hbrs
c [bate-2] eliminated 850 asymmetric tautologies during probing
c [unhide-10] limit 449833 with penalty 2 = 0 + 2
c [unhide-10-10] 240 units, 542 failed, 21308 tauts, 0 hbrs, 18036 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 980 transitive binary clauses
c [transred-6] found 15 units
c [cce-3] limit of 11245826 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 22
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 21
c [cce-3-1] eliminated 7 clauses out of 7 (100%) of length 20
c [cce-3-1] eliminated 3 clauses out of 8 (38%) of length 19
c [cce-3-1] eliminated 11 clauses out of 556 (2%) of length 18
c [cce-3-1] eliminated 5 clauses out of 435 (1%) of length 17
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 29 large clauses in 11245828 steps
c [cce-3-1] allowing another 5622914 steps for small clauses
c [cce-3-1] scheduling 877285 clauses = 671504 binary + 205781 ternary
c [cce-3-1] tried to eliminate 1817 small clauses 0%
c [cce-3-1] eliminated 402 binary clauses 0%
c [cce-3-1] eliminated 146 ternary clauses 0%
c [cce-3-1] eliminated 548 small clauses 0%
c [cce-3-1] eliminated 5776 small clauses in 11245947 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 5805 covered clauses in round 1
c [cce-3] eliminated 5805 covered clauses in TOTAL during 1 rounds
c [cce-3] 5805 < 1/100 * 1580163 = 15801 considered unsuccessful
c [bca-6] limit of 10000000 steps and 3154232 added (scaled 2)
c [bca-6] 400991 out of 455532 literals actually usable 88%
c [bca-6] added 285 blocked clauses in 1227358 steps
c [sweep-6] limit 3148716 based on 1574358 irredundant clauses
c [sweep-6-1] 89455 pos 40.0% + 134292 neg 60.0% = 223747 sched 98.2% ret 4018
c [sweep-6-1] 3267595 steps 55 queries 61479.25 avg class size
c [sweep-6-1] 964 decisions 52 SAT calls 54.48 avg env size
c [sweep-6-1] 223452 variables remain 98% (4309 retained 2%)
c [decomp-24] removed 2348 variables
c [sweep-6-1] removed 2348 vars (0 failed, 11 eqs, 12 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 2348 vars in TOTAL (1 rounds, 54 queries)
c [sort-queue-10] sorted 225417 enqueued variables after 18731 conflicts
c [score-dist-10] active 0 (0%), one 0 (0%), zero 225417 (100%)
c [score-dist-10] max exp 0, different 1 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 5705 variables 2.5% (225417 remain 21%)
c [simplification-10] removed 42997 irredundant clauses 2.7% (1569460 remain 36%)
c [simplification-10] maximum reduction of 3% = max (2%, 3%)
c [simplification-10] forced so keeping old conflict interval 10000
c [simplification-10] conflict limit remains at 22420 (hard 32389)
c [simplification-10] new binary interval 10000
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  227.2  225416  1569460     18741   26790 134606 143856    3   984  168   0%      3  802    3    1  504%
c i  227.2  225397  1569460     18750   26789 134608 143860    3   982  168   0%      3  801    3    1  496%
c i  231.2  225382  1569460     19637   27358 134791 143979    3   995  168   0%      6  802    3    1  481%
c i  232.1  225267  1569460     19834   27489 134826 144005    3   973  168   0%      5  778    3    1  481%
c i  232.2  225266  1569460     19854   27496 134836 144007    3   971  168   0%      5  776    3    1  470%
c i  232.4  225265  1569460     19881   27513 134842 144010    3   971  168   0%      5  775    3    1  465%
c i  233.3  225264  1569460     20081   27636 134884 144042    3   992  168   0%      4  795    3    1  469%
c i  233.7  225263  1569460     20171   27682 134906 144061    3   982  168   0%      4  783    3    1  463%
c i  234.9  225262  1569460     20449   27848 134968 144107    3   990  168   0%      3  788    3    1  439%
c i  235.7  225261  1569460     20629   27972 134999 144126    3   985  168   0%      3  781    3    1  436%
c i  236.6  225237  1569460     20818   28108 135029 144146    3   983  168   0%      2  777    3    1  442%
c i  236.8  225235  1569460     20847   28126 135035 144150    3   985  168   0%      2  779    3    1  435%
c i  236.9  225234  1569460     20857   28133 135037 144150    3   986  168   0%      2  779    3    1  438%
c i  237.2  225233  1569460     20953   28190 135052 144171    3   998  168   0%      2  790    3    1  435%
c i  237.2  225232  1569460     20954   28190 135052 144171    3   998  168   0%      2  790    3    1  434%
c i  237.2  225231  1569460     20955   28190 135052 144171    3   998  168   0%      2  790    3    1  432%
c i  237.2  225230  1569460     20957   28190 135053 144171    3   997  168   0%      2  789    3    1  430%
c i  237.2  225229  1569460     20958   28190 135053 144171    3   997  168   0%      2  789    3    1  428%
c i  237.3  225228  1569460     20962   28192 135053 144172    3   996  168   0%      2  788    3    1  426%
c i  237.3  225227  1569460     20963   28192 135053 144172    3   996  168   0%      2  788    3    1  424%
c i  237.3  225226  1569460     20970   28195 135054 144174    3   995  168   0%      2  786    3    1  421%
c i  238.0  225225  1569460     21108   28288 135074 144197    3   981  168   0%      2  771    3    1  425%
c i  238.2  225224  1569460     21169   28325 135084 144208    3   980  168   0%      2  770    3    1  432%
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  240.0  225223  1569460     21567   28586 135157 144261    3   971  168   0%      2  756    3    1  441%
c i  240.8  225222  1569460     21684   28657 135185 144277    3   971  168   0%      2  754    3    1  443%
c i  241.0  225221  1569460     21713   28675 135192 144280    3   973  168   0%      2  757    3    1  434%
c i  241.2  225220  1569460     21772   28716 135205 144284    3   985  168   0%      2  767    3    1  434%
c i  241.2  225219  1569460     21777   28716 135207 144286    3   983  168   0%      2  766    3    1  429%
c i  241.4  225218  1569460     21842   28740 135219 144313    3   983  168   0%      2  765    3    1  413%
c i  241.4  225217  1569460     21846   28743 135219 144313    3   985  168   0%      2  767    3    1  418%
c i  241.7  225105  1569460     21925   28800 135233 144318    3   975  168   0%      1  756    3    1  407%
c i  241.9  225104  1569460     21961   28819 135243 144321    3   971  168   0%      1  751    3    1  405%
c i  242.1  225103  1569460     22007   28853 135251 144324    3   969  168   0%      1  749    3    1  411%
c i  242.1  225102  1569460     22008   28853 135251 144324    3   969  168   0%      1  749    3    1  410%
c i  242.1  225101  1569460     22011   28854 135251 144325    3   968  168   0%      1  748    3    1  406%
c i  242.3  225100  1569460     22049   28879 135255 144333    3   967  168   0%      1  747    3    1  399%
c i  242.4  225099  1569460     22068   28887 135261 144336    3   967  168   0%      1  747    3    1  393%
c i  242.5  225098  1569460     22087   28898 135264 144340    3   965  168   0%      1  744    3    1  387%
c i  242.6  225097  1569460     22101   28904 135268 144343    3   966  168   0%      1  745    3    1  381%
c i  242.7  225096  1569460     22132   28926 135269 144350    3   966  168   0%      1  745    3    1  371%
c 
c [simplification-11] limit 22487 conflicts (hard 32389) hit after 22487 conflicts
c [quatres-7] found 237566 quaternary clauses 45% in total
c [quatres-7-1] removed 75 duplicate quaternary clauses
c [quatres-7-1] added 17 double-self-subsuming ternary resolvents
c [quatres-7-2] added 479 single-self-subsuming ternary resolvents
c [quatres-7-2] added 1452 quaternary resolvents
c [ternres-7] limit 11599238 with penalty 0 = 0 + 0
c [ternres-7] 533 schedulable variables 0%
c [ternres-7] 42854 ternary resolvents (888 bin, 41966 trn)
c [ternres-7] 9 variables remain 0% (225087 retained 100%)
c [gauss-4] limit 784687 based on 1569375 irredundant clauses
c [gauss-4] extracted 2369 xors of average arity 3.0
c [gauss-4] connected 7055 occurrences of 2726 variables (average 2.6)
c [gauss-4] limit 782831 based on 1565662 irredundant clauses
c [gauss-4] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-25] removed 550 variables
c [simpleprobe-5] 169282 schedulable variables 75%
c [simpleprobe-5] limit 46396953 penalty 0 = 0 + 0
c [decomp-26] removed 3274 variables
c [simpleprobe-5] 123056 variables remain 56% (98216 retained 44%)
c [simpleprobe-5] removed 3274 variables, found 91689 hbrs, 708 units
c [unhide-11] limit 579961 with penalty 2 = 0 + 2
c [unhide-11-11] 95 units, 166 failed, 14412 tauts, 0 hbrs, 8700 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1046 transitive binary clauses
c [transred-7] found 21 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 220890 variables 100%
c [block-4] limit of 28998095 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 9741 blocked clauses
c [block-4] 9741 < 1/100 * 1531453 = 15314 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 220552 variables 100%
c [elim-9] limit of 115992383 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 7649 not tried 3% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 9377 = 4% variables out of 220552 scheduled
c [bca-7] limit of 10000000 steps and 2972587 added (scaled 2)
c [bca-7] 367939 out of 422352 literals actually usable 87%
c [bca-7] added 756 blocked clauses in 1142521 steps
c [sweep-7] limit 3479771 penalty 0 = 0 + 0
c [sweep-7-1] 81684 pos 39.4% + 125453 neg 60.6% = 207137 sched 98.1% ret 4038
c [sweep-7-1] 3500555 steps 78 queries 53050.33 avg class size
c [sweep-7-1] 1032 decisions 73 SAT calls 45.89 avg env size
c [sweep-7-1] 206758 variables remain 98% (4395 retained 2%)
c [decomp-27] removed 482 variables
c [sweep-7-1] removed 482 vars (0 failed, 21 eqs, 26 impls)
c [sweep-7] removed 482 vars in TOTAL (1 rounds, 77 queries)
c [sort-queue-11] sorted 210693 enqueued variables after 22487 conflicts
c [score-dist-11] active 0 (0%), one 0 (0%), zero 210693 (100%)
c [score-dist-11] max exp 0, different 1 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 14403 variables 6.4% (210693 remain 19%)
c [simplification-11] removed 87529 irredundant clauses 5.6% (1481931 remain 34%)
c [simplification-11] maximum reduction of 6% = max (6%, 6%)
c [simplification-11] large reduction 6% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 34487 (soft 24487 + delta 10000)
c [simplification-11] new conflict limit 24487 (hard 34487)
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  265.8  210692  1481931     23378   28247 138330 201395    3   993  166   0%      8  758    3    1  407%
c i  267.0  210691  1481931     23710   28465 138387 201446    3  1001  166   0%      6  762    3    1  394%
c i  267.3  210690  1481931     23791   28513 138406 201455    3  1006  166   0%      6  766    3    1  378%
c i  269.7  210689  1481931     24391   28903 138520 201534    3   997  166   0%      5  750    3    1  389%
c i  269.7  210688  1481931     24392   28903 138520 201534    3   996  166   0%      5  749    3    1  388%
c i  269.9  210687  1481931     24435   28923 138526 201549    3   997  166   0%      5  749    3    1  370%
c 
c [simplification-12] limit 24497 conflicts (hard 34487) hit after 24498 conflicts
c [quatres-8] found 233761 quaternary clauses 45% in total
c [quatres-8-1] removed 313 duplicate quaternary clauses
c [quatres-8-1] added 10 double-self-subsuming ternary resolvents
c [quatres-8-2] added 630 single-self-subsuming ternary resolvents
c [quatres-8-2] added 2655 quaternary resolvents
c [ternres-8] limit 12782368 with penalty 0 = 0 + 0
c [ternres-8] 8 schedulable variables 0%
c [ternres-8] 18658 ternary resolvents (200 bin, 18458 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-28] removed 96 variables
c [treelook-5] limit 1278236 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 97627 literals 23%
c [treelook-5] scheduling used 1278240 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 1278236 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1295527 steps
c [treelook-5] 97555 literals remain 23%
c [treelook-5] 21541 variables remain to probed next time 10%
c [decomp-29] removed 8 variables
c [treelook-5] removed 28 variables, found 1072 hbrs
c [unhide-12] limit 639118 with penalty 2 = 0 + 2
c [unhide-12-12] 167 units, 306 failed, 20120 tauts, 0 hbrs, 16470 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 771 transitive binary clauses
c [transred-8] found 9 units
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 210100 variables 100%
c [elim-10] limit of 255647371 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 1283 not tried 1% in round 1
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 2886 = 1% variables out of 210100 scheduled
c [bca-8] limit of 10000000 steps and 2922153 added (scaled 2)
c [bca-8] 357110 out of 414430 literals actually usable 86%
c [bca-8] added 488 blocked clauses in 1107577 steps
c [sweep-8] limit 3834710 penalty 0 = 0 + 0
c [sweep-8-1] 80265 pos 39.6% + 122665 neg 60.4% = 202930 sched 97.9% ret 4284
c [sweep-8-1] 3924688 steps 102 queries 50159.03 avg class size
c [sweep-8-1] 1268 decisions 91 SAT calls 35.24 avg env size
c [sweep-8-1] 202344 variables remain 98% (4868 retained 2%)
c [decomp-30] removed 619 variables
c [sweep-8-1] removed 619 vars (0 failed, 21 eqs, 26 impls)
c [sweep-8] removed 619 vars in TOTAL (1 rounds, 101 queries)
c [sort-queue-12] sorted 206595 enqueued variables after 24498 conflicts
c [score-dist-12] active 0 (0%), one 0 (0%), zero 206595 (100%)
c [score-dist-12] max exp 0, different 1 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 4092 variables 1.9% (206595 remain 19%)
c [simplification-12] removed 25280 irredundant clauses 1.7% (1456651 remain 33%)
c [simplification-12] maximum reduction of 2% = max (2%, 2%)
c [simplification-12] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-12] new conflict interval 16666
c [simplification-12] penalized conflict interval 16666 = 1 * 16666
c [simplification-12] hard conflict limit 51164 (soft 41164 + delta 10000)
c [simplification-12] new conflict limit 41164 (hard 51164)
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  285.5  206594  1456651     24619   30073 138590 180305    3   980  164   0%      4  731    3    1  381%
c i  285.6  206593  1456651     24656   30097 138599 180308    3   978  164   0%      4  728    3    1  378%
c i  285.8  206592  1456651     24702   30131 138608 180310    3   978  164   0%      4  728    3    1  389%
c i  285.8  206591  1456651     24709   30133 138609 180313    3   977  164   0%      4  727    3    1  383%
c i  285.9  206590  1456651     24733   30146 138617 180315    3   976  164   0%      4  725    3    1  372%
c i  285.9  206589  1456651     24735   30147 138617 180315    3   975  164   0%      4  724    3    1  370%
c i  286.2  206588  1456651     24795   30181 138629 180326    3   979  164   0%      3  727    3    1  372%
c i  286.6  206587  1456651     24914   30255 138654 180345    3  1001  164   0%      3  748    3    1  362%
c i  286.6  206586  1456651     24916   30255 138654 180346    3  1000  164   0%      3  747    3    1  360%
c i  286.7  206585  1456651     24926   30263 138654 180347    3   998  164   0%      3  745    3    1  394%
c i  286.7  206584  1456651     24927   30263 138654 180347    3   998  164   0%      3  745    3    1  392%
c i  286.7  206583  1456651     24930   30265 138654 180347    3   998  164   0%      3  745    3    1  389%
c i  289.1  206582  1456651     25500   30666 138745 180412    3   992  165   0%      3  732    4    1  425%
c i  290.0  206581  1456651     25724   30805 138793 180444    3  1013  165   0%      3  751    3    1  405%
c i  290.2  206580  1456651     25785   30835 138809 180458    3  1018  165   0%      3  755    3    1  408%
c i  290.2  206579  1456651     25787   30835 138809 180459    3  1017  165   0%      3  755    3    1  405%
c i  290.2  206578  1456651     25788   30835 138809 180459    3  1017  165   0%      3  754    3    1  404%
c i  290.2  206577  1456651     25791   30835 138809 180461    3  1016  165   0%      3  754    3    1  400%
c i  290.2  206576  1456651     25797   30837 138812 180461    3  1015  165   0%      3  752    3    1  398%
c i  290.2  206575  1456651     25798   30837 138812 180461    3  1015  165   0%      3  752    3    1  397%
c i  290.2  206574  1456651     25799   30837 138812 180461    3  1015  165   0%      3  752    3    1  395%
c i  290.2  206573  1456651     25803   30837 138814 180462    3  1014  165   0%      3  751    3    1  390%
c i  290.3  206572  1456651     25809   30841 138815 180462    3  1013  165   0%      3  750    3    1  387%
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  291.6  206571  1456651     26120   31056 138857 180511    3  1007  165   0%      2  741    3    1  373%
c i  291.8  206563  1456651     26174   31092 138865 180520    3  1016  165   0%      2  749    3    1  377%
c i  293.8  206562  1456651     26761   31439 138990 180615    3   998  165   0%      3  725    3    1  338%
c i  294.0  206561  1456651     26824   31475 139005 180626    3   995  165   0%      3  721    3    1  334%
c i  294.1  206560  1456651     26841   31481 139011 180629    3   995  165   0%      3  721    3    1  330%
c i  294.9  206559  1456651     27044   31618 139056 180647    3  1018  165   0%      2  742    3    1  346%
c i  296.0  206558  1456651     27318   31800 139105 180680    3   999  165   0%      2  720    3    1  341%
c i  296.0  206557  1456651     27327   31803 139107 180682    3   998  165   0%      2  719    3    1  339%
c i  296.3  206549  1456651     27383   31832 139124 180690    3  1000  165   0%      2  719    3    1  344%
c i  296.3  206513  1456651     27390   31835 139125 180691    3  1000  165   0%      2  720    3    1  342%
c i  296.6  206290  1456651     27483   31886 139150 180706    3  1012  165   0%      2  731    3    1  324%
c i  296.6  206289  1456651     27503   31887 139153 180721    3  1008  165   0%      2  726    3    1  310%
c i  298.3  206288  1456651     27903   32153 139226 180776    3  1015  165   0%      2  729    3    1  345%
c i  298.3  206287  1456651     27909   32154 139228 180778    3  1014  165   0%      2  728    3    1  341%
c i  299.4  206286  1456651     28181   32344 139274 180806    3  1001  165   0%      2  712    3    1  346%
c i  300.8  206285  1456651     28527   32576 139346 180845    3   998  165   0%      2  705    3    1  320%
c i  301.8  206270  1456651     28796   32745 139396 180889    3  1018  165   0%      2  722    3    1  316%
c i  301.8  206269  1456651     28800   32745 139395 180893    3  1017  165   0%      2  721    3    1  312%
c i  303.1  206268  1456651     29071   32930 139445 180926    3   999  165   0%      2  701    3    1  344%
c i  305.8  206267  1456651     29654   33348 139532 180988    3  1006  165   0%      3  702    3    1  335%
c i  307.0  206266  1456651     29955   33559 139584 181022    3   988  165   0%      2  681    3    1  338%
c i  307.0  206265  1456651     29957   33560 139584 181022    3   988  165   0%      2  680    3    1  336%
c i  307.3  206264  1456651     30045   33615 139600 181036    3   992  165   0%      2  683    3    1  322%
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  307.4  206262  1456651     30059   33624 139602 181038    3   993  165   0%      2  685    3    1  322%
c i  307.5  206261  1456651     30091   33634 139616 181043    3   996  165   0%      2  687    3    1  313%
c i  307.5  206260  1456651     30094   33636 139616 181043    3   996  165   0%      2  687    3    1  313%
c i  308.6  206259  1456651     30327   33798 139667 181059    3   985  165   0%      2  674    3    1  311%
c i  308.9  206258  1456651     30404   33844 139683 181070    3   988  165   0%      2  676    3    1  304%
c i  308.9  206257  1456651     30405   33844 139683 181070    3   988  165   0%      2  675    3    1  303%
c i  308.9  206226  1456651     30406   33844 139683 181070    3   987  165   0%      2  675    3    1  301%
c i  309.0  206209  1456651     30422   33853 139686 181073    3   987  165   0%      2  675    3    1  301%
c i  309.4  206078  1456651     30527   33922 139706 181086    3   993  165   0%      1  680    3    1  307%
c i  309.4  206077  1456651     30529   33922 139706 181087    3   993  165   0%      1  679    3    1  305%
c i  309.4  206076  1456651     30530   33922 139706 181087    3   993  165   0%      1  679    3    1  304%
c i  312.2  206075  1456651     31181   34381 139802 181173    3   986  165   0%      3  666    3    1  325%
c i  312.7  206074  1456651     31281   34442 139819 181192    3   995  165   0%      3  674    3    1  320%
c i  312.9  206073  1456651     31316   34462 139827 181198    3   999  165   0%      2  678    3    1  323%
c i  316.7  206072  1456650     32201   35053 139997 181304    3  1022  165   0%      5  692    3    1  298%
c i  319.6  206071  1456650     32867   35512 140114 181383    3  1023  165   0%      5  686    3    1  296%
c i  322.4  206070  1456650     33484   35905 140258 181450    3  1026  165   0%      4  682    3    1  315%
c i  322.4  206069  1456650     33485   35905 140258 181450    3  1026  165   0%      4  682    3    1  313%
c i  323.8  206068  1456650     33781   36111 140311 181480    3  1029  165   0%      4  683    3    1  306%
c i  323.9  206067  1456650     33807   36125 140317 181484    3  1033  165   0%      4  686    3    1  295%
c i  329.0  206066  1456650     34932   36922 140512 181592    3  1032  165   0%      7  673    3    1  301%
c i  331.1  206065  1456650     35482   37319 140614 181637    3  1049  165   0%      6  685    4    1  298%
c i  331.6  206064  1456650     35589   37399 140632 181644    3  1064  165   0%      5  699    4    1  311%
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  331.9  206063  1456650     35677   37465 140644 181651    3  1053  165   0%      5  686    4    1  308%
c i  332.4  206062  1456650     35767   37532 140657 181659    3  1049  165   0%      4  682    4    1  303%
c i  332.7  206061  1456650     35821   37575 140663 181663    3  1050  165   0%      4  682    4    1  300%
c i  333.8  206060  1456650     36132   37779 140721 181701    3  1063  165   0%      3  692    3    1  285%
c i  334.0  206059  1456650     36193   37826 140728 181705    3  1059  165   0%      3  687    3    1  285%
c i  334.8  206058  1456650     36375   37963 140755 181720    3  1062  165   0%      2  689    3    1  286%
c i  334.9  206057  1456650     36399   37974 140761 181724    3  1065  165   0%      2  691    3    1  281%
c i  335.0  206056  1456650     36441   38003 140767 181729    3  1071  165   0%      2  697    3    1  285%
c i  336.0  206055  1456650     36681   38192 140798 181745    3  1044  165   0%      2  668    4    1  297%
c i  339.9  206054  1456650     37591   38875 140939 181815    3  1045  165   0%      5  659    4    1  293%
c i  340.1  206053  1456650     37625   38899 140946 181817    3  1043  165   0%      5  657    4    1  291%
c i  340.1  206052  1456650     37626   38899 140946 181817    3  1043  165   0%      5  656    4    1  290%
c i  340.2  205699  1456650     37667   38929 140952 181821    3  1042  165   0%      4  655    4    1  284%
c i  340.9  205698  1456650     37810   39025 140979 181835    3  1061  165   0%      4  673    3    1  272%
c i  341.5  205697  1456650     37955   39139 141003 181840    3  1057  165   0%      3  667    4    1  301%
c i  343.2  205696  1456650     38393   39416 141094 181903    3  1067  165   0%      3  673    3    1  256%
c i  343.3  205695  1456650     38411   39429 141096 181905    3  1065  165   0%      3  671    3    1  255%
c i  346.1  205694  1456650     39141   39909 141242 181996    3  1067  165   0%      4  666    3    1  249%
c i  347.3  205688  1456650     39431   40124 141283 182024    3  1046  165   0%      3  642    4    1  274%
c i  347.3  205636  1456650     39437   40125 141287 182024    3  1046  165   0%      3  641    4    1  271%
c i  348.4  205635  1456650     39701   40297 141337 182054    3  1061  165   0%      3  654    4    1  281%
c i  348.4  205395  1456650     39713   40307 141337 182055    3  1059  165   0%      2  652    4    1  286%
c i  351.0  205394  1456650     40291   40742 141414 182110    4  1050  165   0%      3  637    4    1  283%
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  351.1  205393  1456650     40312   40758 141416 182112    4  1050  165   0%      3  637    4    1  279%
c i  351.3  205392  1456650     40359   40786 141427 182117    4  1050  165   0%      3  637    4    1  285%
c i  351.8  205391  1456650     40483   40867 141453 182133    4  1059  165   0%      2  644    4    1  260%
c i  351.8  205390  1456650     40484   40867 141453 182133    4  1059  165   0%      2  644    4    1  259%
c i  352.3  205389  1456650     40608   40954 141477 182142    4  1046  165   0%      2  630    4    1  268%
c i  353.6  205388  1456650     40887   41165 141523 182162    4  1045  165   0%      2  626    4    1  266%
c i  354.3  205387  1456650     41037   41261 141551 182183    4  1052  165   0%      1  632    4    1  279%
c i  355.3  205386  1456650     41269   41423 141590 182207    4  1042  165   0%      1  620    4    1  267%
c 
c [simplification-13] limit of 408 iterations hit after 408 iterations
c [quatres-9] found 233008 quaternary clauses 46% in total
c [quatres-9-1] removed 33 duplicate quaternary clauses
c [quatres-9-1] added 16 double-self-subsuming ternary resolvents
c [quatres-9-2] added 254 single-self-subsuming ternary resolvents
c [quatres-9-2] added 1262 quaternary resolvents
c [ternres-9] limit 23689869 with penalty 0 = 0 + 0
c [ternres-9] all 205385 free variables schedulable
c [ternres-9] 24525 ternary resolvents (457 bin, 24068 trn)
c [ternres-9] 21150 variables remain 10% (184235 retained 90%)
c [gauss-5] limit 2368986 penalty 1 = 1 + 0
c [gauss-5] extracted 6468 xors of average arity 3.0
c [gauss-5] connected 19252 occurrences of 7399 variables (average 2.6)
c [gauss-5] limit 2368986 penalty 1 = 1 + 0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-31] removed 591 variables
c [basicprobe-5] limit 118449347 penalty 0 = 0 + 0
c [basicprobe-5-0] 95856 probes remain 48% after last round
c [basicprobe-5-0] 1570 units = 1453 failed (93%) + 117 lifted (7%)
c [basicprobe-5-0] removed 5976 variables, found 82808 hbrs
c [bate-3] eliminated 998 asymmetric tautologies during probing
c [unhide-13] limit 1184493 with penalty 2 = 0 + 2
c [unhide-13-13] 142 units, 251 failed, 14624 tauts, 0 hbrs, 12399 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1140 transitive binary clauses
c [transred-9] found 18 units
c [elim-11] 1277 variables 1% will be scheduled this time
c [elim-11] scheduled 1277 variables 1%
c [elim-11] limit of 473797389 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] no variable eliminated in round 1 in 218488671 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 21 = 2% variables out of 1277 scheduled
c [elim-11] 21 < 1/100 * 1277 = 12 considered unsuccessful
c [bca-9] limit of 10000000 steps and 2745477 added (scaled 2)
c [bca-9] 323672 out of 396472 literals actually usable 82%
c [bca-9] added 375 blocked clauses in 997727 steps
c [sweep-9] limit 7106960 penalty 0 = 0 + 0
c [sweep-9-1] 75204 pos 38.8% + 118391 neg 61.2% = 193595 sched 97.7% ret 4640
c [sweep-9-1] 7110129 steps 141 queries 25050.16 avg class size
c [sweep-9-1] 2136 decisions 136 SAT calls 36.65 avg env size
c [sweep-9-1] 192424 variables remain 97% (5804 retained 3%)
c [decomp-32] removed 3075 variables
c [sweep-9-1] removed 3075 vars (0 failed, 22 eqs, 24 impls)
c [sweep-9] removed 3075 vars in TOTAL (1 rounds, 140 queries)
c [sort-queue-13] sorted 195160 enqueued variables after 41269 conflicts
c [score-dist-13] active 0 (0%), one 0 (0%), zero 195160 (100%)
c [score-dist-13] max exp 0, different 1 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 10225 variables 5.0% (195160 remain 18%)
c [simplification-13] removed 92690 irredundant clauses 6.4% (1363960 remain 31%)
c [simplification-13] maximum reduction of 6% = max (5%, 6%)
c [simplification-13] forced so keeping old conflict interval 16666
c [simplification-13] conflict limit remains at 41310 (hard 51164)
c [simplification-13] new iteration interval 1000
c 
c [simplification-14] limit 41310 conflicts (hard 51164) hit after 41310 conflicts
c [quatres-10] found 222580 quaternary clauses 46% in total
c [quatres-10-1] removed 93 duplicate quaternary clauses
c [quatres-10-1] added 45 double-self-subsuming ternary resolvents
c [quatres-10-2] added 810 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1145 quaternary resolvents
c [ternres-10] limit 23719670 with penalty 0 = 0 + 0
c [ternres-10] 19325 schedulable variables 10%
c [ternres-10] 32731 ternary resolvents (826 bin, 31905 trn)
c [ternres-10] 1133 variables remain 1% (194027 retained 99%)
c [decomp-33] removed 175 variables
c [simpleprobe-6] 107184 schedulable variables 55%
c [simpleprobe-6] limit 94878682 penalty 0 = 0 + 0
c [decomp-34] removed 5063 variables
c [simpleprobe-6] 62737 variables remain 33% (127185 retained 67%)
c [simpleprobe-6] removed 5063 variables, found 137086 hbrs, 1087 units
c [unhide-14] limit 1185983 with penalty 2 = 0 + 2
c [unhide-14-14] 113 units, 250 failed, 44669 tauts, 0 hbrs, 23975 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 1207 transitive binary clauses
c [transred-10] found 7 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 148247941 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 3 clauses out of 6 (50%) of length 19
c [cce-4-1] eliminated 11 clauses out of 544 (2%) of length 18
c [cce-4-1] eliminated 23 clauses out of 417 (6%) of length 17
c [cce-4-1] eliminated 8 clauses out of 375 (2%) of length 16
c [cce-4-1] eliminated 7 clauses out of 996 (1%) of length 15
c [cce-4-1] eliminated 87 clauses out of 1009 (9%) of length 14
c [cce-4-1] eliminated 586 clauses out of 2498 (23%) of length 13
c [cce-4-1] eliminated 845 clauses out of 3916 (22%) of length 12
c [cce-4-1] eliminated 734 clauses out of 5281 (14%) of length 11
c [cce-4-1] eliminated 4109 clauses out of 12009 (34%) of length 10
c [cce-4-1] eliminated 235 clauses out of 15825 (1%) of length 9
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 6648 large clauses in 148247955 steps
c [cce-4-1] allowing another 74123977 steps for small clauses
c [cce-4-1] scheduling 714922 clauses = 548933 binary + 165989 ternary
c [cce-4-1] tried to eliminate 24214 small clauses 3%
c [cce-4-1] eliminated 3506 binary clauses 1%
c [cce-4-1] eliminated 1254 ternary clauses 1%
c [cce-4-1] eliminated 4760 small clauses 1%
c [cce-4-1] eliminated 8311 small clauses in 148247942 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 14959 covered clauses in round 1
c [cce-4] eliminated 14959 covered clauses in TOTAL during 1 rounds
c [bca-10] limit of 10000000 steps and 2633568 added (scaled 2)
c [bca-10] 309018 out of 379044 literals actually usable 82%
c [bca-10] added 838 blocked clauses in 946617 steps
c [sweep-10] limit 7115901 penalty 0 = 0 + 0
c [sweep-10-1] 70769 pos 38.5% + 113074 neg 61.5% = 183843 sched 97.0% ret 5678
c [sweep-10-1] 7141955 steps 189 queries 40028.11 avg class size
c [sweep-10-1] 2417 decisions 175 SAT calls 34.81 avg env size
c [sweep-10-1] 181963 variables remain 96% (7417 retained 4%)
c [decomp-35] removed 723 variables
c [sweep-10-1] removed 723 vars (0 failed, 36 eqs, 42 impls)
c [sweep-10] removed 723 vars in TOTAL (1 rounds, 188 queries)
c [sort-queue-14] sorted 188798 enqueued variables after 41310 conflicts
c [score-dist-14] active 0 (0%), one 0 (0%), zero 188798 (100%)
c [score-dist-14] max exp 0, different 1 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 6362 variables 3.3% (188798 remain 17%)
c [simplification-14] removed 53216 irredundant clauses 3.9% (1310744 remain 30%)
c [simplification-14] maximum reduction of 4% = max (3%, 4%)
c [simplification-14] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-14] new conflict interval 20666
c [simplification-14] penalized conflict interval 20666 = 1 * 20666
c [simplification-14] hard conflict limit 72309 (soft 61976 + delta 10333)
c [simplification-14] new conflict limit 61976 (hard 72309)
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  389.4  188797  1310744     42023   40617 147989 281052    4  1013  160   0%      3  584    4    1  261%
c i  390.4  188796  1310744     42292   40818 148027 281075    4  1018  160   0%      3  587    4    1  295%
c i  392.9  188754  1310744     42936   41248 148158 281145    4  1015  160   0%      3  578    3    1  217%
c i  393.2  188753  1310744     42992   41288 148162 281153    4  1012  160   0%      3  574    3    1  228%
c i  399.1  188752  1310744     44515   42413 148403 281286    4  1017  160   0%     11  566    4    1  247%
c i  399.5  188751  1310744     44650   42499 148427 281306    4  1034  160   0%      9  583    3    1  234%
c i  403.0  188750  1310744     45536   43142 148571 281390    4  1015  160   0%      7  555    3    2  222%
c i  403.6  188749  1310744     45672   43244 148591 281400    4  1008  160   0%      6  547    3    2  224%
c i  404.2  188748  1310744     45827   43366 148613 281409    4  1002  160   0%      5  541    4    2  237%
c i  407.6  188654  1310743     46690   43999 148759 281479    4   996  160   0%      6  527    4    2  225%
c i  408.8  188653  1310743     46984   44222 148809 281495    4   993  160   0%      4  522    4    2  237%
c i  408.8  188652  1310743     46985   44222 148809 281495    4   993  160   0%      4  522    4    2  236%
c i  409.1  188651  1310743     47050   44266 148826 281497    4   992  160   0%      4  520    4    2  231%
c i  409.2  188650  1310743     47076   44284 148831 281499    4   992  160   0%      4  520    4    2  235%
c i  409.2  188649  1310743     47078   44284 148831 281500    4   991  160   0%      4  520    4    2  233%
c i  409.2  188648  1310743     47079   44284 148831 281500    4   991  160   0%      4  519    4    2  232%
c i  409.3  188591  1310743     47082   44285 148832 281500    4   991  160   0%      4  519    4    2  231%
c i  409.3  188590  1310743     47088   44287 148833 281502    4   990  160   0%      4  518    4    2  228%
c i  409.3  188589  1310743     47089   44287 148833 281502    4   990  160   0%      4  518    4    2  227%
c i  409.3  187933  1310743     47090   44287 148833 281502    4   990  160   0%      4  518    4    2  226%
c i  409.3  187877  1310743     47091   44287 148833 281502    4   989  160   0%      4  517    4    2  225%
c i  409.3  187869  1310743     47096   44287 148834 281504    4   988  160   0%      4  516    3    2  223%
c i  409.3  187095  1310743     47097   44287 148834 281504    4   988  160   0%      4  516    3    2  222%
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  410.2  187078  1310743     47352   44482 148870 281522    4  1003  160   0%      3  529    4    2  239%
c i  414.2  186717  1310742     48390   45262 149024 281608    4  1004  160   0%      6  522    4    2  239%
c i  415.6  186712  1310741     48793   45547 149091 281650    4  1010  160   0%      4  524    4    2  225%
c i  423.1  186711  1310741     50718   46924 149410 281846    4  1013  160   0%     15  513    4    2  214%
c i  424.4  186706  1310741     51088   47177 149478 281886    4  1007  160   0%     11  504    3    2  201%
c i  436.0  186705  1310741     54039   49396 149933 282115    4  1013  160   0%     29  488    4    2  210%
c i  436.1  186704  1310741     54054   49403 149938 282117    4  1018  160   0%     28  493    4    2  206%
c i  441.2  186703  1310741     55400   50421 150145 282208    4  1032  160   0%     14  497    4    2  206%
c i  442.9  186702  1310741     55847   50754 150217 282241    4  1027  160   0%      9  488    4    2  195%
c i  446.2  186701  1310741     56676   51411 150308 282303    4  1022  160   0%      6  477    4    2  208%
c i  446.3  186700  1310741     56708   51427 150318 282308    4  1026  160   0%      6  482    4    2  199%
c i  446.4  186699  1310741     56747   51448 150326 282317    4  1028  160   0%      6  483    4    2  192%
c i  448.4  186698  1310741     57214   51800 150404 282342    4  1002  160   0%      4  453    4    2  200%
c i  452.7  186697  1310741     58303   52661 150533 282415    4   992  160   0%      5  436    4    2  207%
c i  460.8  186696  1310738     60325   54187 150806 282598    4   979  161   0%     15  411    4    2  204%
c i  461.9  186695  1310738     60602   54403 150849 282612    4   962  161   0%     11  392    4    2  210%
c i  465.7  186694  1310738     61683   55190 151036 282695    4   982  161   0%      8  406    4    2  192%
c i  466.8  186693  1310738     61963   55399 151085 282712    4   963  161   0%      5  384    4    2  199%
c 
c [simplification-15] limit 62047 conflicts (hard 72309) hit after 62047 conflicts
c [quatres-11] found 216426 quaternary clauses 47% in total
c [quatres-11-1] removed 731 duplicate quaternary clauses
c [quatres-11-1] added 15 double-self-subsuming ternary resolvents
c [quatres-11-2] added 647 single-self-subsuming ternary resolvents
c [quatres-11-2] added 1020 quaternary resolvents
c [ternres-11] limit 36587049 with penalty 0 = 0 + 0
c [ternres-11] 1048 schedulable variables 1%
c [ternres-11] 52467 ternary resolvents (1021 bin, 51446 trn)
c [ternres-11] 90 variables remain 0% (186603 retained 100%)
c [card-5] limit 1143345 penalty 4 = 4 + 0
c [card-5] found 664 at-most-one constraints of average size 3.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1143345 for elimination
c [card-5] 664 out of 664 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-36] removed 3095 variables
c [treelook-6] limit 3658704 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 143405 literals 39%
c [treelook-6] scheduling used 3142077 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3658704 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 3663628 steps
c [treelook-6] 143176 literals remain 39%
c [treelook-6] 18902 variables remain to probed next time 10%
c [decomp-37] removed 28 variables
c [treelook-6] removed 45 variables, found 14177 hbrs
c [unhide-15] limit 1829352 with penalty 2 = 0 + 2
c [unhide-15-15] 84 units, 128 failed, 13125 tauts, 0 hbrs, 12050 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1467 transitive binary clauses
c [transred-11] found 8 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 184300 variables 100%
c [block-5] limit of 45733811 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 17165 blocked clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 183650 variables 100%
c [elim-12] limit of 365870491 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 75 not tried 0% in round 1
c [gc-113] reconnected 282020 binary clauses (produced 0 empty 1 units)
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 12684 = 7% variables out of 183650 scheduled
c [bca-11] limit of 10000000 steps and 2415375 added (scaled 2)
c [bca-11] 266161 out of 341934 literals actually usable 78%
c [bca-11] added 1680 blocked clauses in 839470 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 109761140 penalty 0 = 0 + 0
c [sweep-11-1] 61480 pos 37.4% + 102838 neg 62.6% = 164318 sched 96.1% ret 6648
c [sweep-11-1] 109783116 steps 2271 queries 5655.69 avg class size
c [sweep-11-1] 28427 decisions 2088 SAT calls 35.11 avg env size
c [sweep-11-1] 126146 variables remain 74% (44647 retained 26%)
c [decomp-38] removed 1639 variables
c [sweep-11-1] removed 1639 vars (0 failed, 451 eqs, 594 impls)
c [sweep-11] removed 1639 vars in TOTAL (1 rounds, 2270 queries)
c [sort-queue-15] sorted 169327 enqueued variables after 62047 conflicts
c [score-dist-15] active 0 (0%), one 0 (0%), zero 169327 (100%)
c [score-dist-15] max exp 0, different 1 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 17366 variables 9.3% (169327 remain 15%)
c [simplification-15] removed 112220 irredundant clauses 8.6% (1198518 remain 27%)
c [simplification-15] maximum reduction of 9% = max (9%, 9%)
c [simplification-15] large reduction 9% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 74047 (soft 64047 + delta 10000)
c [simplification-15] new conflict limit 64047 (hard 74047)
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  498.1  169326  1198518     62420   48847 149599 256269    4   963  156   0%      3  382    4    2  183%
c i  498.1  169325  1198518     62431   48851 149604 256270    4   960  156   0%      3  380    4    2  180%
c i  498.1  169324  1198518     62437   48854 149605 256271    4   962  156   0%      3  381    4    2  178%
c i  498.1  169323  1198518     62443   48857 149606 256272    4   962  156   0%      3  381    4    2  178%
c i  498.1  169322  1198518     62445   48858 149606 256272    4   963  156   0%      3  382    4    2  178%
c i  500.6  169286  1198518     63218   49456 149727 256316    4   966  156   0%      3  381    4    2  179%
c i  500.9  169285  1198518     63322   49525 149744 256329    4   968  156   0%      2  382    4    2  185%
c i  502.1  169284  1198518     63621   49755 149781 256356    4   956  156   0%      1  369    4    2  190%
c i  502.5  169283  1198518     63723   49827 149800 256366    4   966  156   0%      1  378    4    2  193%
c 
c [simplification-16] limit 64054 conflicts (hard 74047) hit after 64054 conflicts
c [quatres-12] found 207172 quaternary clauses 47% in total
c [quatres-12-1] removed 61 duplicate quaternary clauses
c [quatres-12-1] added 12 double-self-subsuming ternary resolvents
c [quatres-12-2] added 763 single-self-subsuming ternary resolvents
c [quatres-12-2] added 2984 quaternary resolvents
c [ternres-12] limit 37679067 with penalty 0 = 0 + 0
c [ternres-12] 86 schedulable variables 0%
c [ternres-12] 32545 ternary resolvents (366 bin, 32179 trn)
c [ternres-12] 1 variables remain 0% (169282 retained 100%)
c [gauss-6] limit 1883953 penalty 2 = 2 + 0
c [gauss-6] extracted 4049 xors of average arity 3.0
c [gauss-6] connected 12094 occurrences of 4829 variables (average 2.5)
c [gauss-6] limit 1883953 penalty 2 = 2 + 0
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-39] removed 137 variables
c [basicprobe-6] limit 188395339 penalty 0 = 0 + 0
c [basicprobe-6-0] 29190 probes remain 18% after last round
c [basicprobe-6-0] 2703 units = 2587 failed (96%) + 116 lifted (4%)
c [basicprobe-6-0] removed 3286 variables, found 79468 hbrs
c [bate-4] eliminated 2129 asymmetric tautologies during probing
c [unhide-16] limit 1883953 with penalty 2 = 0 + 2
c [unhide-16-16] 111 units, 351 failed, 40793 tauts, 0 hbrs, 26032 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 1215 transitive binary clauses
c [transred-12] found 6 units
c [cce-5] limit of 47098834 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 23
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 22
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 21
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 20
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 19
c [cce-5-1] eliminated 11 clauses out of 529 (2%) of length 18
c [cce-5-1] eliminated 4 clauses out of 366 (1%) of length 17
c [cce-5-1] eliminated 11 clauses out of 314 (4%) of length 16
c [cce-5-1] eliminated 16 clauses out of 1053 (2%) of length 15
c [cce-5-1] eliminated 7 clauses out of 962 (1%) of length 14
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 55 large clauses in 47098850 steps
c [cce-5-1] allowing another 23549425 steps for small clauses
c [cce-5-1] scheduling 613196 clauses = 464760 binary + 148436 ternary
c [cce-5-1] tried to eliminate 6939 small clauses 1%
c [cce-5-1] eliminated 1507 binary clauses 0%
c [cce-5-1] eliminated 419 ternary clauses 0%
c [cce-5-1] eliminated 1926 small clauses 0%
c [cce-5-1] eliminated 4820 small clauses in 47098928 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 4875 covered clauses in round 1
c [cce-5] eliminated 4875 covered clauses in TOTAL during 1 rounds
c [cce-5] 4875 < 1/100 * 1150401 = 11504 considered unsuccessful
c [elim-13] 75 variables 0% will be scheduled this time
c [elim-13] scheduled 75 variables 0%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] no variable eliminated in round 1 in 20046805 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 14 = 19% variables out of 75 scheduled
c [elim-13] 14 < 1/100 * 75 = 0 considered unsuccessful
c [bca-12] limit of 10000000 steps and 2298339 added (scaled 2)
c [bca-12] 252179 out of 330932 literals actually usable 76%
c [bca-12] added 433 blocked clauses in 785789 steps
c [sweep-12] limit 11303720 penalty 0 = 0 + 0
c [sweep-12-1] 46458 pos 37.9% + 76123 neg 62.1% = 122581 sched 74.1% ret 42884
c [sweep-12-1] 11314203 steps 333 queries 22648.02 avg class size
c [sweep-12-1] 4009 decisions 303 SAT calls 34.05 avg env size
c [sweep-12-1] 120488 variables remain 73% (44969 retained 27%)
c [decomp-40] removed 2466 variables
c [sweep-12-1] removed 2466 vars (0 failed, 64 eqs, 87 impls)
c [sweep-12] removed 2466 vars in TOTAL (1 rounds, 332 queries)
c [sort-queue-16] sorted 162999 enqueued variables after 64054 conflicts
c [score-dist-16] active 0 (0%), one 0 (0%), zero 162999 (100%)
c [score-dist-16] max exp 0, different 1 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 6284 variables 3.7% (162999 remain 15%)
c [simplification-16] removed 57867 irredundant clauses 4.8% (1140651 remain 26%)
c [simplification-16] maximum reduction of 5% = max (4%, 5%)
c [simplification-16] large reduction 5% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 76054 (soft 66054 + delta 10000)
c [simplification-16] new conflict limit 66054 (hard 76054)
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  525.7  162998  1140651     64724   51828 140362 257040    4   967  152   0%      3  373    4    2  168%
c i  528.4  162991  1140651     65479   52412 140466 257095    4   985  152   0%      3  387    4    2  181%
c 
c [simplification-17] limit 66054 conflicts (hard 76054) hit after 66054 conflicts
c [quatres-13] found 201576 quaternary clauses 47% in total
c [quatres-13-1] removed 55 duplicate quaternary clauses
c [quatres-13-1] added 30 double-self-subsuming ternary resolvents
c [quatres-13-2] added 570 single-self-subsuming ternary resolvents
c [quatres-13-2] added 1037 quaternary resolvents
c [ternres-13] limit 38747848 with penalty 0 = 0 + 0
c [ternres-13] 1 schedulable variables 0%
c [ternres-13] 1649 ternary resolvents (19 bin, 1630 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-41] removed 43 variables
c [simpleprobe-7] 51557 schedulable variables 32%
c [simpleprobe-7] limit 154991393 penalty 0 = 0 + 0
c [decomp-42] removed 4121 variables
c [simpleprobe-7] 28752 variables remain 18% (130083 retained 82%)
c [simpleprobe-7] removed 4121 variables, found 152420 hbrs, 733 units
c [unhide-17] limit 1937392 with penalty 2 = 0 + 2
c [unhide-17-17] 18 units, 30 failed, 12605 tauts, 0 hbrs, 7802 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 1384 transitive binary clauses
c [transred-13] found 2 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 158792 variables 100%
c [block-6] limit of 96869620 steps penalty 2 = 2 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 5759 blocked clauses
c [block-6] 5759 < 1/100 * 1102515 = 11025 considered unsuccessful
c [bca-13] limit of 10000000 steps and 2200938 added (scaled 2)
c [bca-13] 239019 out of 317044 literals actually usable 75%
c [bca-13] added 198 blocked clauses in 747474 steps
c [sweep-13] limit 11624354 penalty 0 = 0 + 0
c [sweep-13-1] 42801 pos 37.4% + 71793 neg 62.6% = 114594 sched 72.3% ret 43927
c [sweep-13-1] 11630697 steps 359 queries 18855.55 avg class size
c [sweep-13-1] 4279 decisions 344 SAT calls 33.49 avg env size
c [sweep-13-1] 112097 variables remain 71% (46407 retained 29%)
c [decomp-43] removed 187 variables
c [sweep-13-1] removed 187 vars (0 failed, 57 eqs, 73 impls)
c [sweep-13] removed 187 vars in TOTAL (1 rounds, 358 queries)
c [sort-queue-17] sorted 158334 enqueued variables after 66054 conflicts
c [score-dist-17] active 0 (0%), one 0 (0%), zero 158334 (100%)
c [score-dist-17] max exp 0, different 1 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 4657 variables 2.9% (158334 remain 14%)
c [simplification-17] removed 44746 irredundant clauses 3.9% (1095905 remain 25%)
c [simplification-17] maximum reduction of 4% = max (3%, 4%)
c [simplification-17] geometric conflict interval increment 4133 = 20666 / 5
c [simplification-17] new conflict interval 24799
c [simplification-17] penalized conflict interval 24799 = 1 * 24799
c [simplification-17] hard conflict limit 103252 (soft 90853 + delta 12399)
c [simplification-17] new conflict limit 90853 (hard 103252)
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  542.5  158333  1095905     66334   53243 131467 374606    4   967  152   0%      3  364    4    2  189%
c i  542.5  158332  1095905     66343   53250 131468 374606    4   967  152   0%      3  364    4    2  189%
c i  543.9  158331  1095905     66752   53555 131531 374638    4   972  152   0%      2  367    4    2  167%
c i  544.4  158330  1095905     66886   53656 131556 374643    4   986  152   0%      1  380    4    2  173%
c i  546.4  158326  1095905     67527   54140 131650 374683    4   981  152   0%      1  371    4    2  172%
c i  550.2  158325  1095905     68672   55034 131810 374752    4  1003  152   0%      5  386    4    2  168%
c i  553.3  158324  1095905     69598   55754 131948 374797    4  1002  152   0%      4  381    4    2  186%
c i  556.2  158323  1095905     70607   56507 132117 374867    4   993  152   0%      5  365    4    2  164%
c i  557.3  158322  1095905     70982   56793 132171 374891    4  1000  152   0%      3  370    4    2  171%
c i  558.5  158320  1095905     71343   57061 132220 374927    4   987  152   0%      2  356    4    2  170%
c i  562.0  158319  1095905     72536   57976 132379 375023    4   981  152   0%      5  343    4    2  160%
c i  562.0  158318  1095905     72543   57978 132382 375024    4   981  152   0%      5  342    4    2  158%
c i  562.0  158261  1095905     72544   57978 132382 375024    4   980  152   0%      5  342    4    2  157%
c i  562.0  158211  1095905     72552   57985 132382 375024    4   981  152   0%      5  343    4    2  161%
c i  562.0  158193  1095905     72555   57985 132383 375025    4   980  152   0%      5  342    4    2  159%
c i  562.0  158192  1095905     72556   57985 132383 375025    4   980  152   0%      5  342    4    2  159%
c i  562.1  158191  1095905     72572   57998 132384 375026    4   981  152   0%      5  342    4    2  158%
c i  562.4  158190  1095905     72681   58081 132395 375038    4  1000  152   0%      4  361    4    2  160%
c i  562.4  158189  1095905     72683   58081 132395 375039    4   999  152   0%      4  360    4    2  159%
c i  562.5  158186  1095905     72732   58117 132404 375040    4   992  152   0%      4  353    4    2  161%
c i  565.7  158071  1095905     73699   58875 132543 375093    4   979  152   0%      4  335    4    2  173%
c i  567.7  158070  1095905     74222   59293 132606 375128    4  1007  152   0%      2  361    4    2  190%
c i  567.8  158051  1095905     74259   59320 132613 375129    4  1001  152   0%      2  354    4    2  191%
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  569.3  158050  1095905     74780   59729 132682 375161    4   990  152   0%      1  341    4    2  165%
c i  569.8  158048  1095903     74921   59826 132706 375177    4   989  152   0%      1  338    4    2  161%
c i  569.9  158047  1095903     74961   59851 132715 375182    4   989  152   0%      1  339    4    2  154%
c i  570.7  158046  1095903     75176   60025 132739 375196    4   981  152   0%     -0  329    4    2  165%
c i  572.4  158045  1095903     75634   60387 132798 375221    4   982  152   0%     -0  328    4    2  180%
c i  575.4  158044  1095901     76538   61075 132927 375292    4   989  152   0%      2  330    4    2  173%
c i  579.1  158043  1095901     77585   61890 133069 375351    4   998  152   0%      4  334    4    2  169%
c i  579.6  158042  1095901     77724   61988 133092 375363    4  1019  152   0%      3  355    4    2  177%
c i  581.6  158041  1095899     78362   62498 133170 375400    4  1009  152   0%      2  342    4    2  165%
c i  583.5  157949  1095899     78933   62952 133244 375430    4  1029  152   0%      1  359    5    2  186%
c i  583.6  157948  1095899     78936   62952 133245 375431    4  1029  152   0%      1  358    5    2  185%
c i  583.6  157947  1095899     78937   62952 133245 375431    4  1029  152   0%      1  358    5    2  184%
c i  583.6  157920  1095899     78938   62952 133244 375432    4  1028  152   0%      1  357    5    2  183%
c i  583.6  157899  1095899     78939   62952 133244 375432    4  1028  152   0%      1  357    5    2  182%
c i  586.2  157876  1095899     79635   63516 133325 375469    4  1033  152   0%      1  358    5    2  188%
c i  587.3  157875  1095899     79973   63786 133370 375487    4  1025  152   0%      1  349    4    3  170%
c i  587.3  157874  1095899     79974   63786 133370 375487    4  1025  152   0%      1  348    4    3  169%
c i  587.5  157873  1095899     80022   63827 133375 375488    4  1025  152   0%      0  349    4    3  168%
c i  588.0  157872  1095899     80193   63959 133398 375500    4  1025  152   0%     -0  347    4    3  172%
c i  589.8  157871  1095899     80719   64389 133457 375524    4  1014  153   0%     -0  334    5    3  185%
c i  595.5  157865  1095899     82337   65683 133666 375606    4  1023  153   0%      9  334    5    3  180%
c i  595.7  157864  1095899     82397   65725 133679 375610    4  1020  153   0%      8  331    5    3  176%
c i  596.0  157863  1095899     82469   65781 133689 375615    4  1022  153   0%      7  333    4    3  169%
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  600.2  157862  1095899     83768   66831 133848 375690    4  1029  153   0%      7  334    4    3  158%
c i  600.2  157861  1095899     83770   66831 133849 375690    4  1029  153   0%      7  334    4    3  157%
c i  600.2  157860  1095899     83771   66831 133849 375690    4  1029  153   0%      7  333    4    3  156%
c i  601.7  157859  1095898     84176   67158 133897 375709    4  1022  153   0%      5  324    4    3  160%
c i  609.0  157854  1095898     86223   68841 134131 375811    5   993  153   0%     14  286    5    3  170%
c i  609.0  157853  1095898     86224   68841 134131 375811    5   993  153   0%     14  286    5    3  169%
c i  611.8  157852  1095898     87047   69483 134249 375857    4   996  153   0%      8  286    4    3  150%
c i  611.8  157851  1095898     87048   69483 134249 375857    4   996  153   0%      8  285    4    3  149%
c i  611.8  157850  1095898     87049   69483 134249 375857    4   996  153   0%      8  285    4    3  148%
c i  612.9  157849  1095898     87409   69765 134304 375876    4   980  153   0%      5  268    4    3  161%
c i  617.0  157848  1095897     88659   70749 134463 375952    4   970  153   0%      6  253    4    3  153%
c i  617.4  157847  1095897     88755   70818 134478 375962    4   975  153   0%      5  258    4    3  145%
c i  618.7  157846  1095897     89189   71170 134528 375990    4   976  153   0%      3  257    4    3  144%
c i  619.8  157815  1095896     89559   71458 134570 376021    4   991  153   0%      1  270    4    3  145%
c i  624.4  157756  1095892     90966   72574 134766 376088    4   978  153   0%      6  252    4    3  157%
c 
c [simplification-18] limit 90972 conflicts (hard 103252) hit after 90972 conflicts
c [quatres-14] found 197528 quaternary clauses 47% in total
c [quatres-14-1] removed 549 duplicate quaternary clauses
c [quatres-14-1] added 11 double-self-subsuming ternary resolvents
c [quatres-14-2] added 286 single-self-subsuming ternary resolvents
c [quatres-14-2] added 762 quaternary resolvents
c [ternres-14] limit 51635915 with penalty 0 = 0 + 0
c [ternres-14] all 157756 free variables schedulable
c [ternres-14] 33423 ternary resolvents (1047 bin, 32376 trn)
c [ternres-14] 718 variables remain 0% (157038 retained 100%)
c [decomp-44] removed 1274 variables
c [treelook-7] limit 5163591 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 134240 literals 43%
c [treelook-7] scheduling used 2905881 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 5163591 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 5170209 steps
c [treelook-7] 134104 literals remain 43%
c [treelook-7] 15520 variables remain to probed next time 10%
c [decomp-45] removed 18 variables
c [treelook-7] removed 24 variables, found 7467 hbrs
c [unhide-18] limit 2581795 with penalty 2 = 0 + 2
c [unhide-18-18] 44 units, 284 failed, 65181 tauts, 0 hbrs, 34083 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 1439 transitive binary clauses
c [transred-14] found 5 units
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 156782 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 8660 variables 6% in round 1 in 328963334 steps
c [elim-14-1] backward subsumption/strengthening limit 71036666
c [elim-14-1-1] backward checking 48183 touched variables 31%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 623 and strengthened 731 clauses in 43722812 steps
c [elim-14-1] rescheduled 3552 variables 2% by backward subsumption
c [elim-14] incomplete 17 not tried 0% in round 2
c [gc-136] reconnected 314815 binary clauses (produced 0 empty 5 units)
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 8878 = 6% variables out of 156782 scheduled
c [bca-14] limit of 10000000 steps and 2088619 added (scaled 2)
c [bca-14] 211891 out of 295810 literals actually usable 72%
c [bca-14] added 922 blocked clauses in 687120 steps
c [sweep-14] limit 15490774 penalty 0 = 0 + 0
c [sweep-14-1] 38528 pos 36.7% + 66414 neg 63.3% = 104942 sched 71.0% ret 42962
c [sweep-14-1] 15515137 steps 422 queries 11676.19 avg class size
c [sweep-14-1] 5773 decisions 407 SAT calls 38.40 avg env size
c [sweep-14-1] 101297 variables remain 68% (46601 retained 32%)
c [decomp-46] removed 428 variables
c [sweep-14-1] removed 428 vars (0 failed, 68 eqs, 78 impls)
c [sweep-14] removed 428 vars in TOTAL (1 rounds, 421 queries)
c [sort-queue-18] sorted 147476 enqueued variables after 90972 conflicts
c [score-dist-18] active 0 (0%), one 0 (0%), zero 147476 (100%)
c [score-dist-18] max exp 0, different 1 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 10280 variables 6.5% (147476 remain 13%)
c [simplification-18] removed 56763 irredundant clauses 5.2% (1039129 remain 24%)
c [simplification-18] maximum reduction of 7% = max (7%, 5%)
c [simplification-18] large reduction 7% >= 5% limit
c [simplification-18] next conflict interval 2000 = 2000/1
c [simplification-18] penalized conflict interval 2000 = 1 * 2000
c [simplification-18] hard conflict limit 102972 (soft 92972 + delta 10000)
c [simplification-18] new conflict limit 92972 (hard 102972)
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  641.0  147475  1039129     91013   63658 140392 287545    4   971  150   0%      6  245    4    3  157%
c i  645.8  147474  1039129     92603   64892 140600 287657    4   965  150   0%      9  233    4    3  152%
c 
c [simplification-19] limit 92972 conflicts (hard 102972) hit after 92972 conflicts
c [quatres-15] found 192099 quaternary clauses 47% in total
c [quatres-15-1] removed 47 duplicate quaternary clauses
c [quatres-15-1] added 7 double-self-subsuming ternary resolvents
c [quatres-15-2] added 669 single-self-subsuming ternary resolvents
c [quatres-15-2] added 2418 quaternary resolvents
c [ternres-15] limit 52564010 with penalty 0 = 0 + 0
c [ternres-15] 676 schedulable variables 0%
c [ternres-15] 24541 ternary resolvents (1061 bin, 23480 trn)
c [ternres-15] 17 variables remain 0% (147457 retained 100%)
c [decomp-47] removed 152 variables
c [basicprobe-7] limit 262820052 penalty 0 = 0 + 0
c [basicprobe-7-0] 25835 sched 18%, 1189 failed, 99 lifted, 51749 hbrs
c [decomp-48] removed 3263 variables
c [basicprobe-7-1] 71205 probes remain 50% after last round
c [basicprobe-7-1] 1649 units = 1535 failed (93%) + 114 lifted (7%)
c [basicprobe-7-1] removed 3887 variables, found 70550 hbrs
c [bate-5] eliminated 1493 asymmetric tautologies during probing
c [unhide-19] limit 2628200 with penalty 2 = 0 + 2
c [unhide-19-19] 45 units, 108 failed, 8639 tauts, 0 hbrs, 8238 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 1455 transitive binary clauses
c [transred-15] found 5 units
c [cce-6] limit of 32852506 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 21
c [cce-6-1] eliminated 9 clauses out of 321 (3%) of length 16
c [cce-6-1] eliminated 7 clauses out of 949 (1%) of length 15
c [cce-6-1] eliminated 4 clauses out of 893 (0%) of length 14
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 21 large clauses in 32852538 steps
c [cce-6-1] allowing another 16426269 steps for small clauses
c [cce-6-1] scheduling 523208 clauses = 388001 binary + 135207 ternary
c [cce-6-1] tried to eliminate 7725 small clauses 1%
c [cce-6-1] eliminated 897 binary clauses 0%
c [cce-6-1] eliminated 409 ternary clauses 0%
c [cce-6-1] eliminated 1306 small clauses 0%
c [cce-6-1] eliminated 2336 small clauses in 32852646 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 2357 covered clauses in round 1
c [cce-6] eliminated 2357 covered clauses in TOTAL during 1 rounds
c [cce-6] 2357 < 1/100 * 998297 = 9982 considered unsuccessful
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 143320 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 3964 variables 3% in round 1 in 299118269 steps
c [elim-15-1] backward subsumption/strengthening limit 299118200
c [elim-15-1-1] backward checking 24414 touched variables 17%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 212 and strengthened 308 clauses in 28786295 steps
c [elim-15-1] rescheduled 1393 variables 1% by backward subsumption
c [elim-15-2] eliminated 40 variables 0% in round 2 in 13969446 steps
c [elim-15-2] backward subsumption/strengthening limit 13969400
c [elim-15-2-1] backward checking 414 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 15 and strengthened 39 clauses in 1027295 steps
c [elim-15-2] rescheduled 118 variables 0% by backward subsumption
c [elim-15-3] eliminated 4 variables 0% in round 3 in 629943 steps
c [elim-15-3] backward subsumption/strengthening limit 629900
c [elim-15-3-1] backward checking 41 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 1 and strengthened 5 clauses in 525997 steps
c [elim-15] incomplete 18 not tried 0% in round 3
c [gc-145] reconnected 321757 binary clauses (produced 0 empty 1 units)
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 4045 = 3% variables out of 143320 scheduled
c [bca-15] limit of 10000000 steps and 1964662 added (scaled 2)
c [bca-15] 197712 out of 278552 literals actually usable 71%
c [bca-15] added 686 blocked clauses in 647446 steps
c [sweep-15] limit 15769203 penalty 0 = 0 + 0
c [sweep-15-1] 34771 pos 36.5% + 60520 neg 63.5% = 95291 sched 68.4% ret 43984
c [sweep-15-1] 15783829 steps 478 queries 13083.87 avg class size
c [sweep-15-1] 6215 decisions 432 SAT calls 36.38 avg env size
c [sweep-15-1] 91639 variables remain 66% (47631 retained 34%)
c [decomp-49] removed 428 variables
c [sweep-15-1] removed 428 vars (0 failed, 79 eqs, 97 impls)
c [sweep-15] removed 428 vars in TOTAL (1 rounds, 477 queries)
c [sort-queue-19] sorted 138847 enqueued variables after 92972 conflicts
c [score-dist-19] active 0 (0%), one 0 (0%), zero 138847 (100%)
c [score-dist-19] max exp 0, different 1 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 8627 variables 5.8% (138847 remain 13%)
c [simplification-19] removed 61918 irredundant clauses 6.0% (977211 remain 22%)
c [simplification-19] maximum reduction of 6% = max (6%, 6%)
c [simplification-19] large reduction 6% >= 5% limit
c [simplification-19] next conflict interval 2000 = 2000/1
c [simplification-19] penalized conflict interval 2000 = 1 * 2000
c [simplification-19] hard conflict limit 104972 (soft 94972 + delta 10000)
c [simplification-19] new conflict limit 94972 (hard 104972)
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  675.0  138846   977211     93197   63306 145588 308857    4   937  147   0%      5  203    5    3  166%
c 
c [simplification-20] limit 94972 conflicts (hard 104972) hit after 94972 conflicts
c [quatres-16] found 185537 quaternary clauses 48% in total
c [quatres-16-1] removed 52 duplicate quaternary clauses
c [quatres-16-1] added 27 double-self-subsuming ternary resolvents
c [quatres-16-2] added 320 single-self-subsuming ternary resolvents
c [quatres-16-2] added 1485 quaternary resolvents
c [ternres-16] limit 53482020 with penalty 0 = 0 + 0
c [ternres-16] 15 schedulable variables 0%
c [ternres-16] 12218 ternary resolvents (103 bin, 12115 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-7] limit 1337050 penalty 3 = 3 + 0
c [gauss-7] extracted 2377 xors of average arity 3.0
c [gauss-7] connected 7114 occurrences of 2977 variables (average 2.4)
c [gauss-7] limit 1337050 penalty 3 = 3 + 0
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-50] removed 34 variables
c [simpleprobe-8] 23499 schedulable variables 17%
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-51] removed 3069 variables
c [simpleprobe-8] 16700 variables remain 12% (119043 retained 88%)
c [simpleprobe-8] removed 3069 variables, found 116282 hbrs, 490 units
c [unhide-20] limit 2674101 with penalty 2 = 0 + 2
c [unhide-20-20] 6 units, 92 failed, 74071 tauts, 0 hbrs, 24202 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 638 transitive binary clauses
c [transred-16] found 3 units
c [block-7] scheduling all variables this time
c [block-7] scheduled 135602 variables 100%
c [block-7] limit of 66852525 steps penalty 3 = 3 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 2223 blocked clauses
c [block-7] 2223 < 1/100 * 954587 = 9545 considered unsuccessful
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 135532 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 2171 variables 2% in round 1 in 284904109 steps
c [elim-16-1] backward subsumption/strengthening limit 284904100
c [elim-16-1-1] backward checking 22020 touched variables 16%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 399 and strengthened 332 clauses in 26832434 steps
c [elim-16-1] rescheduled 1664 variables 1% by backward subsumption
c [elim-16-2] eliminated 56 variables 0% in round 2 in 12498403 steps
c [elim-16-2] backward subsumption/strengthening limit 12498400
c [elim-16-2-1] backward checking 546 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 38 and strengthened 37 clauses in 1364601 steps
c [elim-16-2] rescheduled 156 variables 0% by backward subsumption
c [elim-16-3] eliminated 9 variables 0% in round 3 in 1856730 steps
c [elim-16-3] backward subsumption/strengthening limit 1856700
c [elim-16-3-1] backward checking 127 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 2 and strengthened 4 clauses in 633905 steps
c [elim-16] incomplete 29 not tried 0% in round 3
c [gc-154] reconnected 320280 binary clauses (produced 0 empty 2 units)
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 2282 = 2% variables out of 135532 scheduled
c [bca-16] limit of 10000000 steps and 1885265 added (scaled 2)
c [bca-16] 188488 out of 266502 literals actually usable 71%
c [bca-16] added 430 blocked clauses in 617650 steps
c [sweep-16] limit 16044606 penalty 0 = 0 + 0
c [sweep-16-1] 31945 pos 36.5% + 55566 neg 63.5% = 87511 sched 65.7% ret 45739
c [sweep-16-1] 16277949 steps 479 queries 10883.76 avg class size
c [sweep-16-1] 6374 decisions 476 SAT calls 36.00 avg env size
c [sweep-16-1] 83742 variables remain 63% (49460 retained 37%)
c [decomp-52] removed 266 variables
c [sweep-16-1] removed 266 vars (0 failed, 77 eqs, 76 impls)
c [sweep-16] removed 266 vars in TOTAL (1 rounds, 478 queries)
c [sort-queue-20] sorted 132984 enqueued variables after 94972 conflicts
c [score-dist-20] active 0 (0%), one 0 (0%), zero 132984 (100%)
c [score-dist-20] max exp 0, different 1 (100%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 5862 variables 4.2% (132984 remain 12%)
c [simplification-20] removed 40219 irredundant clauses 4.1% (936992 remain 21%)
c [simplification-20] maximum reduction of 4% = max (4%, 4%)
c [simplification-20] geometric conflict interval increment 4959 = 24799 / 5
c [simplification-20] new conflict interval 29758
c [simplification-20] penalized conflict interval 29758 = 1 * 29758
c [simplification-20] hard conflict limit 139609 (soft 124730 + delta 14879)
c [simplification-20] new conflict limit 124730 (hard 139609)
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  700.0  132983   936992     95299   62272 144583 310281    4   942  145   0%     15  201    4    3  142%
c i  701.3  132949   936992     95788   62654 144645 310316    4   916  145   0%      8  174    4    3  148%
c i  705.5  132939   936992     97307   63865 144823 310417    4   938  145   0%      9  192    4    3  147%
c i  707.6  132938   936992     98079   64493 144913 310451    4   954  145   0%      5  205    5    3  168%
c i  709.2  132926   936992     98697   64987 144979 310491    5   954  145   0%      2  203    5    3  162%
c i  713.9  132922   936992    100340   66306 145156 310602    5   946  145   0%      9  191    5    3  165%
c i  714.2  132921   936992    100433   66388 145161 310604    5   937  145   0%      7  182    5    3  157%
c i  719.5  132920   936992    102219   67844 145379 310685    5   963  145   0%     11  202    5    3  160%
c i  722.3  132822   936992    103112   68585 145466 310731    5   950  145   0%      6  187    5    3  156%
c i  727.3  132821   936992    104764   69949 145634 310814    5   952  145   0%      9  184    5    3  154%
c i  727.3  132819   936992    104786   69965 145637 310814    5   952  145   0%      9  184    5    3  150%
c i  728.4  132802   936991    105156   70265 145674 310836    5   956  145   0%      5  187    5    3  151%
c i  730.7  132801   936991    105961   70918 145770 310873    5   953  145   0%      3  181    5    3  154%
c i  731.9  132800   936991    106370   71248 145822 310893    5   954  145   0%      1  182    5    3  147%
c i  736.8  132799   936991    107925   72532 145986 310967    5   936  145   1%      7  159    5    3  141%
c i  742.8  132796   936991    109914   74169 146204 311061    5   928  145   1%     13  147    5    3  148%
c i  743.5  132795   936991    110136   74356 146223 311072    5   923  145   1%      9  142    5    3  146%
c i  749.7  132736   936991    112126   76046 146411 311149    5   943  145   1%     13  157    5    3  144%
c i  754.7  132711   936991    113753   77418 146576 311215    5   933  145   1%     10  143    6    3  174%
c i  755.4  132710   936991    113976   77613 146599 311218    5   922  145   1%      7  133    5    3  153%
c i  760.1  132695   936991    115366   78762 146752 311287    5   912  145   1%      6  119    5    3  145%
c i  761.7  132694   936991    115876   79174 146809 311313    5   932  145   1%      3  138    5    3  135%
c i  764.8  132685   936991    116878   80034 146900 311345    5   923  145   1%      2  127    5    3  159%
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  768.5  132684   936991    117986   80957 147021 311391    5   928  145   1%      3  130    5    3  152%
c i  769.5  132671   936991    118278   81200 147054 311400    5   924  145   1%      1  125    5    3  148%
c i  773.8  132668   936991    119539   82278 147172 311446    5   938  145   1%      3  137    5    4  155%
c i  774.5  132665   936991    119783   82471 147201 311459    5   922  145   1%      2  120    5    4  144%
c i  780.5  132608   936991    121670   84059 147386 311535    5   911  145   1%     10  106    6    4  156%
c i  785.9  132578   936991    123355   85478 147560 311598    5   898  146   1%      9   91    6    4  153%
c 
c [simplification-21] limit 124730 conflicts (hard 139609) hit after 124730 conflicts
c [quatres-17] found 181811 quaternary clauses 47% in total
c [quatres-17-1] removed 156 duplicate quaternary clauses
c [quatres-17-1] added 17 double-self-subsuming ternary resolvents
c [quatres-17-2] added 267 single-self-subsuming ternary resolvents
c [quatres-17-2] added 1293 quaternary resolvents
c [ternres-17] limit 68182876 with penalty 0 = 0 + 0
c [ternres-17] all 132573 free variables schedulable
c [ternres-17] 24910 ternary resolvents (867 bin, 24043 trn)
c [ternres-17] 250 variables remain 0% (132323 retained 100%)
c [card-6] limit 2130714 penalty 4 = 4 + 0
c [card-6] found 1184 at-most-one constraints of average size 3.2
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 2130714 for elimination
c [card-6] 1184 out of 1184 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-53] removed 820 variables
c [treelook-8] limit 6818287 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 115179 literals 44%
c [treelook-8] scheduling used 2565381 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 6818287 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 6860239 steps
c [treelook-8] 115053 literals remain 44%
c [treelook-8] 12969 variables remain to probed next time 10%
c [decomp-54] removed 15 variables
c [treelook-8] removed 52 variables, found 8124 hbrs
c [unhide-21] limit 3409143 with penalty 2 = 0 + 2
c [unhide-21-21] 13 units, 26 failed, 6857 tauts, 0 hbrs, 15038 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 1016 transitive binary clauses
c [transred-17] found 2 units
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 132048 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 1493 variables 1% in round 1 in 274941474 steps
c [elim-17-1] backward subsumption/strengthening limit 274941400
c [elim-17-1-1] backward checking 11175 touched variables 8%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 129 and strengthened 194 clauses in 15162702 steps
c [elim-17-1] rescheduled 804 variables 1% by backward subsumption
c [elim-17-2] eliminated 48 variables 0% in round 2 in 7324600 steps
c [elim-17-2] backward subsumption/strengthening limit 7324600
c [elim-17-2-1] backward checking 399 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 24 and strengthened 21 clauses in 967858 steps
c [elim-17-2] rescheduled 125 variables 0% by backward subsumption
c [elim-17-3] eliminated 12 variables 0% in round 3 in 1045740 steps
c [elim-17-3] backward subsumption/strengthening limit 1045700
c [elim-17-3-1] backward checking 90 touched variables 0%
c [elim-17-3-1] fully completed backward checking in 1 rounds
c [elim-17-3] subsumed 2 and strengthened 6 clauses in 453083 steps
c [elim-17] incomplete 15 not tried 0% in round 3
c [gc-161] reconnected 312132 binary clauses (produced 0 empty 4 units)
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 1576 = 1% variables out of 132048 scheduled
c [bca-17] limit of 10000000 steps and 1841032 added (scaled 2)
c [bca-17] 171061 out of 260946 literals actually usable 66%
c [bca-17] added 251 blocked clauses in 582557 steps
c [sweep-17] limit 20454862 penalty 0 = 0 + 0
c [sweep-17-1] 29785 pos 36.3% + 52273 neg 63.7% = 82058 sched 62.9% ret 48414
c [sweep-17-1] 20482938 steps 543 queries 10154.39 avg class size
c [sweep-17-1] 8087 decisions 551 SAT calls 36.57 avg env size
c [sweep-17-1] 78097 variables remain 60% (52336 retained 40%)
c [decomp-55] removed 289 variables
c [sweep-17-1] removed 289 vars (0 failed, 106 eqs, 81 impls)
c [sweep-17] removed 289 vars in TOTAL (1 rounds, 542 queries)
c [sort-queue-21] sorted 130183 enqueued variables after 124730 conflicts
c [score-dist-21] active 0 (0%), one 0 (0%), zero 130183 (100%)
c [score-dist-21] max exp 0, different 1 (100%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 2390 variables 1.8% (130183 remain 12%)
c [simplification-21] removed 22072 irredundant clauses 2.4% (914919 remain 21%)
c [simplification-21] maximum reduction of 2% = max (2%, 2%)
c [simplification-21] geometric conflict interval increment 9919 = 29758 / 3
c [simplification-21] new conflict interval 39677
c [simplification-21] penalized conflict interval 39677 = 1 * 39677
c [simplification-21] hard conflict limit 184245 (soft 164407 + delta 19838)
c [simplification-21] new conflict limit 164407 (hard 184245)
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  805.9  130182   914919    125138   83175 159878 309339    5   908  148   1%     10   98    5    4  134%
c i  806.9  130179   914919    125459   83445 159903 309357    5   898  148   1%      6   87    5    4  131%
c i  807.7  130177   914919    125726   83669 159931 309365    5   894  148   1%      3   83    5    4  137%
c i  820.5  130175   914919    129959   87213 160396 309525    5   893  148   1%     42   76    5    4  123%
c i  821.2  130174   914919    130186   87395 160427 309537    5   900  148   1%     32   83    5    4  128%
c i  832.1  130172   914919    133534   90280 160704 309661    5   900  148   1%     29   80    5    4  140%
c i  832.5  130171   914919    133632   90354 160717 309665    5   910  148   1%     25   90    5    4  137%
c i  832.5  130170   914919    133637   90357 160718 309665    5   909  148   1%     25   89    5    4  137%
c i  833.0  130169   914919    133794   90493 160731 309671    5   898  148   1%     20   77    5    4  141%
c i  835.8  130168   914919    134611   91164 160818 309712    5   894  148   1%      7   72    5    4  134%
c i  845.4  130167   914919    137512   93650 161065 309839    5   900  148   1%     21   76    5    4  126%
c i  845.7  130166   914919    137617   93741 161072 309841    6   884  148   1%     18   59    6    4  139%
c i  846.4  130162   914919    137825   93924 161088 309845    6   880  148   1%     13   56    6    4  140%
c i  850.8  130024   914919    139224   95138 161213 309888    6   898  148   1%      5   72    6    4  151%
c i  854.8  130018   914919    140453   96197 161314 309931    6   889  148   1%      2   62    5    4  134%
c i  861.9  130017   914919    142560   98002 161503 309998    6   920  148   1%     10   90    6    4  145%
c i  864.4  130014   914919    143258   98593 161574 310017    6   926  148   1%      3   95    6    4  146%
c i  866.4  130013   914919    143885   99125 161621 310046    6   921  148   1%     -1   89    6    4  136%
c i  868.0  130003   914919    144388   99560 161671 310054    6   907  148   1%     -3   75    5    4  132%
c i  869.8  130002   914919    144973  100057 161717 310086    6   927  148   1%     -4   94    6    4  138%
c i  871.6  129998   914919    145448  100479 161754 310097    6   918  148   1%     -5   84    6    4  149%
c i  874.2  129994   914919    146209  101143 161813 310120    6   920  148   1%     -4   86    6    4  140%
c i  874.2  129984   914919    146211  101142 161815 310120    6   920  148   1%     -4   85    6    4  139%
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  874.3  129980   914919    146242  101170 161815 310121    6   917  148   1%     -5   82    6    4  136%
c i  882.7  129979   914919    148755  103350 162026 310195    6   904  148   1%     15   67    6    4  143%
c i  889.4  129977   914919    150838  105156 162207 310254    6   906  149   1%     11   66    6    4  133%
c i  913.0  129976   914919    157502  110937 162778 310466    6   898  149   1%     74   52    7    4  156%
c i  913.5  129970   914919    157613  111031 162787 310469    6   892  149   1%     65   46    7    4  147%
c i  916.3  129931   914919    158429  111736 162859 310496    6   903  149   1%     25   56    6    5  136%
c i  916.5  129930   914919    158478  111776 162865 310498    6   904  149   1%     23   57    6    5  139%
c i  918.4  129928   914919    159040  112267 162909 310517    6   907  149   1%      9   59    7    5  148%
c i  927.2  129920   914919    161741  114612 163119 310605    6   871  149   1%     14   22    7    5  144%
c i  929.5  129918   914919    162401  115179 163187 310622    6   870  149   1%      3   21    6    5  137%
c i  930.5  129917   914919    162683  115421 163212 310634    6   878  149   1%     -1   29    6    5  139%
c 
c [simplification-22] limit 164414 conflicts (hard 184245) hit after 164418 conflicts
c [quatres-18] found 184330 quaternary clauses 47% in total
c [quatres-18-1] removed 35 duplicate quaternary clauses
c [quatres-18-1] added 13 double-self-subsuming ternary resolvents
c [quatres-18-2] added 446 single-self-subsuming ternary resolvents
c [quatres-18-2] added 1157 quaternary resolvents
c [ternres-18] limit 91300213 with penalty 0 = 0 + 0
c [ternres-18] 240 schedulable variables 0%
c [ternres-18] 22036 ternary resolvents (233 bin, 21803 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-56] removed 618 variables
c [basicprobe-8] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 30911 probes remain 24% after last round
c [basicprobe-8-0] 1637 units = 1377 failed (84%) + 260 lifted (16%)
c [basicprobe-8-0] removed 2643 variables, found 92848 hbrs
c [bate-6] eliminated 688 asymmetric tautologies during probing
c [unhide-22] limit 4565010 with penalty 2 = 0 + 2
c [unhide-22-22] 42 units, 106 failed, 51794 tauts, 0 hbrs, 98047 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 285 transitive binary clauses
c [transred-18] found 2 units
c [elim-18] no untried remaining variables left
c [elim-18] scheduled 126743 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 16000000000 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 3017 variables 2% in round 1 in 251183183 steps
c [elim-18-1] backward subsumption/strengthening limit 251183100
c [elim-18-1-1] backward checking 21686 touched variables 17%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 261 and strengthened 197 clauses in 23330934 steps
c [elim-18-1] rescheduled 1268 variables 1% by backward subsumption
c [elim-18-2] eliminated 56 variables 0% in round 2 in 9993510 steps
c [elim-18-2] backward subsumption/strengthening limit 9993500
c [elim-18-2-1] backward checking 407 touched variables 0%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 30 and strengthened 33 clauses in 1269176 steps
c [elim-18-2] rescheduled 147 variables 0% by backward subsumption
c [elim-18-3] eliminated 4 variables 0% in round 3 in 2297397 steps
c [elim-18-3] backward subsumption/strengthening limit 2297300
c [elim-18-3-1] backward checking 51 touched variables 0%
c [elim-18-3-1] fully completed backward checking in 1 rounds
c [elim-18-3] subsumed 3 and strengthened 3 clauses in 574455 steps
c [elim-18] incomplete 15 not tried 0% in round 3
c [gc-168] reconnected 319087 binary clauses (produced 0 empty 4 units)
c [elim-18] transition to [ all 1 rem 1 ] state
c [elim-18] eliminated 3130 = 2% variables out of 126743 scheduled
c [bca-18] limit of 10000000 steps and 1725501 added (scaled 2)
c [bca-18] 149509 out of 247228 literals actually usable 60%
c [bca-18] added 692 blocked clauses in 540566 steps
c [sweep-18] boosting sweeping limit by 10
c [sweep-18] limit 273900640 penalty 0 = 0 + 0
c [sweep-18-1] 27198 pos 36.6% + 47089 neg 63.4% = 74287 sched 60.1% ret 49326
c [sweep-18-1] 273975878 steps 5150 queries 814.28 avg class size
c [sweep-18-1] 59964 decisions 4823 SAT calls 33.18 avg env size
c [sweep-18-1] 29940 variables remain 24% (92977 retained 76%)
c [decomp-57] removed 3340 variables
c [sweep-18-1] removed 3340 vars (0 failed, 1418 eqs, 1100 impls)
c [sweep-18] removed 3340 vars in TOTAL (1 rounds, 5149 queries)
c [sort-queue-22] sorted 120273 enqueued variables after 164418 conflicts
c [score-dist-22] active 0 (0%), one 0 (0%), zero 120273 (100%)
c [score-dist-22] max exp 0, different 1 (100%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 9641 variables 7.4% (120273 remain 11%)
c [simplification-22] removed 69387 irredundant clauses 7.6% (845532 remain 19%)
c [simplification-22] maximum reduction of 8% = max (7%, 8%)
c [simplification-22] large reduction 8% >= 5% limit
c [simplification-22] next conflict interval 2000 = 2000/1
c [simplification-22] penalized conflict interval 2000 = 1 * 2000
c [simplification-22] hard conflict limit 176418 (soft 166418 + delta 10000)
c [simplification-22] new conflict limit 166418 (hard 176418)
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  982.0  120272   845532    164636  110516 150368 310933    6   860  147   1%      4   10    6    5  136%
c i  985.9  120271   845532    165873  111599 150461 310969    6   888  147   1%     -1   38    5    5  107%
c 
c [simplification-23] limit 166418 conflicts (hard 176418) hit after 167424 conflicts
c [quatres-19] found 175040 quaternary clauses 47% in total
c [quatres-19-1] removed 206 duplicate quaternary clauses
c [quatres-19-1] added 38 double-self-subsuming ternary resolvents
c [quatres-19-2] added 699 single-self-subsuming ternary resolvents
c [quatres-19-2] added 1978 quaternary resolvents
c [ternres-19] limit 92951338 with penalty 0 = 0 + 0
c [ternres-19] all 120271 free variables schedulable
c [ternres-19] 25950 ternary resolvents (895 bin, 25055 trn)
c [ternres-19] 67 variables remain 0% (120204 retained 100%)
c [decomp-58] removed 97 variables
c [simpleprobe-9] 13665 schedulable variables 11%
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-59] removed 2856 variables
c [simpleprobe-9] 15651 variables remain 13% (101669 retained 87%)
c [simpleprobe-9] removed 2856 variables, found 106277 hbrs, 558 units
c [unhide-23] limit 9295133 with penalty 1 = 0 + 1
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 6905 basic ate = 5122 trn 74% + 1783 lrg 26% in 6 updates
c bcas: 18 count, 18067 added (14620 skipped), 17930233 steps
c bkwd: tried 2573447 clauses, 5139439 lits, 2.00 lits/clause
c bkwd: checked 213700501 occs, 83.04 occs/clause, 41.58 occs/lit
c bkwd: subsumed 79 binary, 2073 ternary, 2186 large
c bkwd: strengthened 34 binary, 40 ternary (100% self), 7427 large (0% self)
c blkd: 7 bces, 76540 removed, 48309434 resolutions, 126935225 steps
c blkd: 33572 blocking literals 1%, 2249 pure
c bump: 0 bumped seen, 0 lits 0.0 on average
c card: 6 count, 0 units, 0 am1, 101470498 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 10130 subsumed
c card: 4082 at-most-one constraints found, average size 3.11
c card: 4082 at-most-one constraints used 100%, average size 3.11
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: 6 cces, 19015 eliminated, 18351 ate 97%, 664 abce 3%
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: 15562771 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 175 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 59 decompositions, 124810 equivalent 11%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 58331010 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 18 elims, 624420 eliminated 55%, 9688 pure 2%
c elms: 34 rounds, 1.9 rounds/bve
c elms: 538868 small 86%, 73615 large 12%
c elms: 742861 tried small, 538868 succeeded 73%, 203993 failed 27%
c elms: 286551 subsumed, 354751 strengthened, 8306 blocked
c elms: 55806948 copies, 68772550 resolutions, 15400808 ipos
c elms: 48740620 subchks, 87961201 strchks
c gaus: 7 extractions, 35584 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 2 ternary equations
c gaus: 0 gc, 22759090 steps, 11379545 extr 50%, 11431152 elim 50%
c glue: 4.2 orig avg, 4.2 real avg, 0.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1483198 = 686024 simple 46% + 787052 trn 53% + 10122 lrg 1%, 31189 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 180031 clauses, 9.5 length
c lrnd: 1713448 lits = 2263808 orig - 550360 removed 24%
c lrnd: 109938 uips 61%, 13165 flips 7%
c mins: 142291 mins 79%, 10544 bin 6%, 27196 size 15%
c mins: 3741530 poisoned searches, 467202 hits, 12% hit rate
c mins: 5273829 used twice searches, 363281 hits, 7% hit rate
c move: moved 104636, 43442 bin 42%, 61194 trn 58%
c otfs: 2660 driving 49%, 2752 restarting 51%
c otfs: str 5412, 3652 red 67%, 1760 irr 33%
c otfs: str 5412, 0 bin 0%, 2059 trn 38%, 3353 lrg 62%
c otfs: sub 170, 132 red 78%, 38 irr 22%
c otfs: sub 170, 0 bin 0%, 125 trn 74%, 45 lrg 26%
c phas: 4 computed, 772903 set, 357996 pos (46%), 414907 neg (54%)
c prbs: 8 basic, 437083 probed, 11468 failed, 2727 lifted
c prbs: 9 simple, 1576580 probed, 5031 failed, 20814 eqs
c prbs: 8 treelook, 889 probed, 57 failed, 0 lifted
c prom: 0 locked 0% out of 39105 tried
c prps: 1564654953 props, 25 props/dec
c prps: 92% srch, 8% simp, 0% lkhd
c quat: 19 count, 45495 quat, 14689 self1, 447 self2, 5246 dup
c queu: 22 sorted, 58331010 next (0 steps 0.00)
c queu: 6747600 enq (6747577 steps 1.00), 0 deq 0%
c redc: 19466 clauses 18%, 111181 tried 66%, 590 sat 1%
c redc: 30464 lits 4%, 762342 tried 34%, 591 sat 0%
c redc: 1583 times jump level reduced, 298.4 levels on average
c reds: 0 count, 0.0 conflicts per reduce
c reds: 0 memlim 0%, 0 arith 0%
c reds: 0 collected 0%, 0 retired 0%
c rmbd: 274800 removed, 183160 red 67%
c rsts: 16000 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: 23 count, 18 confs 78%, 0 vars 0%
c simp: 2 its 9%, 2 bin 9%, 1 trns 4%
c subl: 180031 count (38752 tried 0.2), 2082 sub out of 136091 (1.5%)
c swps: 18 count, 18 rounds, 11249 queries (624.9/round)
c swps: 10573 sat calls, 1955 unsat (1.4% success rate)
c swps: 139333 decisions 13.2, 15267 conflicts 1.4
c swps; 10236.2 avg class size, 34.6 avg environment size
c swps: 0 failed, 2462 impls, 2532 equivs
c swp0: 3741 type 0 queries, 1181 unsat (31.6%), 3328 sat (89.0%)
c swp1: 7508 type 1 queries, 5245 unsat (69.9%), 5389 sat (71.8%)
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: 116663040 calls to obtain time
c tops: 265219 fixed 23%, 589 its, 284.25 confs/it
c trds: 18 transitive reductions, 18392 removed, 176 failed
c trds: 290661 nodes, 472204 edges, 35672654 steps
c trim: 396718 words, 1.5 MB
c trnr: 19 count, 15545 bin, 619709 trn, 616597234 steps
c unhd: 23 count, 24 rounds, 239670442 steps
c unhd: 25485 non-trivial sccs of average size 2.5
c unhd: 4138 units, 4096 bin, 40 trn, 2 lrg
c unhd: 7321 failed, 6363 stamp, 0 lits, 53 bin, 765 trn, 2 lrg
c unhd: 633790 tauts, 11127 bin 2%, 141676 trn 22%, 34858 lrg 5%
c unhd: 633790 tauts, 446129 stamp 70%, 484024 red 76%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 663982 str, 4096 bin 1%, 87648 trn 13%, 572238 lrg 86%, 230847 red 35%
c vars: 117203 remaining 10% and 1014449 removed 90% out of 1131652
c vars: 265219 fixed 23%, 624420 eliminated 55%, 124810 equivalent 11%
c vsts: 10417860609 visits, 89% srch, 11% simp, 0% lkhd
c vsts: 6.5 search visits per propagation, 55518.5 per conflict
c wchs: 1974695624 pushed, 219549105 enlarged, 256 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         181586             0             0      25570191        481122         30467
c 
c  0 0        127989  70         0   0<        0   0< 23757936  93<   422692  88<    26713  88<    2.3
c  1 5         14332   8<        0   0         0   0    830449   3     25343   5      1680   6     0.5
c  2 6         21359  12         0   0         0   0    693288   3     22556   5      1438   5     1.0
c  3 9         11765   6         0   0         0   0    209219   1      7567   2       470   2     0.8
c  4 14         4323   2         0   0         0   0     51745   0      2159   0       120   0     0.5
c  5 21         1378   1         0   0         0   0     12480   0       590   0        38   0     0.2
c  6 30          356   0         0   0         0   0      9618   0       176   0         6   0     0.1
c  7 41           63   0         0   0         0   0      5432   0        32   0         2   0     0.0
c  8 54           19   0         0   0         0   0        22   0         7   0         0   0     0.0
c  9 69            1   0         0   0         0   0         1   0         0   0         0   0     0.0
c 10 86            0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 11 126           1   0         0   0         0   0         1   0         0   0         0   0     0.0
c 
c avg                  0.7           0.0           0.0           0.1           0.2           0.2
c std                  1.2           0.0           0.0           0.5           0.7           0.7
c 
c   97.870  10% elim
c   88.311   9% probe
c   67.693   7% sweep
c   35.843   4% decide
c   30.829   3% unhide
c   17.198   2% block
c   16.009   2% bca
c   15.670   2% quatres
c   15.222   2% cce
c    9.441   1% gauss
c 
c   10.227 < 1% rest (below)
c 
c    7.215   1% ternres
c    2.448   0% transred
c    0.565   0% card
c    0.000   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   13.265   1% preprocessing     3%
c  399.354  40% inprocessing     97%
c ==================================
c  412.619  41% simplifying
c  584.369  59% search
c ==================================
c  997.008 100% all
c 
c        167424 conflicts,         167.9 confs/sec
c         23896 ternaries,           7.0 confs/ternary
c         12572 binaries,           13.3 confs/binary
c           589 iterations,        284.3 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c         16000 restarts,           16.0 rests/sec,     10.5 confs/restart
c      58331010 decisions,       58506.1 decis/sec,    348.4 decis/conflict
c    1564654953 propagations,  1569350.8 props/sec,     26.8 props/decision
c 
c 997.0 seconds, 389.5 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
