c launch: /data/cnf/sc2014/app/SAT_dat.k70-24_1_rule_3.cnf.bz2
c host: atom32
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_3.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/SAT_dat.k70-24_1_rule_3.cnf.bz2
c no embedded options
c found 'p cnf 1131646 4433512' header
c read 1131646 variables, 4433512 clauses, 11129223 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 1096143 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 1096143  4397875         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 1099468 based on 4397875 irredundant clauses
c [card-1] found 1023 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1099468 for elimination
c [card-1] 1023 out of 1023 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 855857 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 6951670 based on 3475835 irredundant clauses
c [decomp-2] removed 1837 variables
c [simpleprobe-1] 790936 variables remain 93% (63084 retained 7%)
c [simpleprobe-1] removed 1837 variables, found 17079 hbrs, 417 units
c [unhide-1] limit 216664 based on 3466637 irredundant clauses
c [unhide-1-1] 1302 units, 1097 failed, 7267 tauts, 0 hbrs, 43324 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 849609 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 768525 not tried 90% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 81717 = 10% variables out of 849609 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 3050149 negative 95.2% of 3204322 except 154173 4.8%
c [phase-count-1] 2999317 positive 93.6% of 3204322 except 205005 6.4%
c [phase-1] phase bias: 356619 positive 46%, 411273 negative 54%
c [sort-queue-1] sorted 767892 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 767892 (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 160486 variables 17.3% (767892 remain 70%)
c [simplification-1] removed 1193553 irredundant clauses 27.1% (3204322 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.2  767891  3204322        10       4     10 13623    0     1  203   1%      0    1    0    0 25079%
c i   13.2  767890  3204322        12       4     11 13623    0     1  203   1%      0    1    0    0 24946%
c i   13.2  767838  3204322        13       4     11 13623    0     1  203   1%      0    1    0    0 24849%
c i   13.2  767791  3204322        16       4     11 13625    0     1  203   1%      0    1    0    0 24641%
c i   13.3  767744  3204322        23       6     13 13627    0     1  203   1%      0    1    0    0 24373%
c i   13.6  767702  3204322        85      40     30 13637    0    10  203   1%      0   10    1    0 21803%
c i   13.6  767583  3204322        99      41     34 13645    0    12  203   0%      0   12    1    0 20965%
c i   13.6  767582  3204322       109      43     37 13649    0    14  203   0%      0   14    1    0 20439%
c i   13.7  767581  3204322       112      44     37 13650    0    15  203   0%      0   15    1    0 20351%
c i   13.7  767580  3204322       113      44     37 13650    0    15  203   0%      0   15    1    0 20272%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 2869 variables
c [simpleprobe-2] 708732 schedulable variables 93%
c [simpleprobe-2] limit 6394470 based on 3197235 irredundant clauses
c [decomp-4] removed 719 variables
c [simpleprobe-2] 710726 variables remain 93% (53578 retained 7%)
c [simpleprobe-2] removed 719 variables, found 30761 hbrs, 108 units
c [treelook-1] limit 798559 based on 3194237 irredundant clauses
c [treelook-1] scheduled 159289 literals 10%
c [treelook-1] scheduling used 798644 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 798559 based on 3194237 irredundant clauses
c [treelook-1] used 801230 steps
c [treelook-1] 159148 literals remain 10%
c [treelook-1] 157384 variables remain to probed next time 21%
c [decomp-5] removed 145 variables
c [treelook-1] removed 159 variables, found 1833 hbrs
c [basicprobe-1] limit 25549136 based on 3193642 irredundant clauses
c [basicprobe-1-0] 689996 probes remain 91% after last round
c [basicprobe-1-0] 4050 units = 1859 failed (46%) + 2191 lifted (54%)
c [basicprobe-1-0] removed 9477 variables, found 165815 hbrs
c [unhide-2] limit 199602 based on 3193642 irredundant clauses
c [unhide-2-2] 757 units, 1033 failed, 11364 tauts, 0 hbrs, 29758 literals
c [elim-2] 752373 variables 100% will be scheduled this time
c [elim-2] scheduled 752373 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 667989 not tried 89% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 84445 = 11% variables out of 752373 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 2798476 negative 95.1% of 2944113 except 145637 4.9%
c [phase-count-2] 2747384 positive 93.3% of 2944113 except 196729 6.7%
c [phase-2] phase bias: 787 positive 29%, 1950 negative 71%
c [sort-queue-2] sorted 667928 enqueued variables after 113 conflicts
c [score-dist-2] active 0 (0%), one 0 (0%), zero 667928 (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 99652 variables 13.0% (667928 remain 61%)
c [simplification-2] removed 260209 irredundant clauses 8.1% (2944113 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 1034 (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.6  667927  2944113       122      36     24 146034    0    16  196   0%      0   16    1    0 19974%
c i   32.7  667926  2944113       142      44     30 146039    0    16  196   0%      0   16    1    0 19325%
c i   32.7  667893  2944113       150      50     30 146039    0    17  196   0%      0   17    1    0 19143%
c i   33.2  667890  2944113       253      97     54 146068    0    33  196   0%      0   33    1    0 16201%
c i   33.3  667889  2944113       266     108     55 146068    0    37  196   0%      0   37    1    0 15983%
c i   33.3  667888  2944113       269     109     56 146068    0    37  196   0%      0   37    1    0 15847%
c i   33.5  667881  2944113       302     122     68 146075    0    43  196   0%      0   43    2    0 15211%
c i   33.7  667876  2944113       346     145     73 146089    0    54  196   0%      0   54    2    0 14268%
c i   33.8  667875  2944113       349     146     74 146089    0    54  196   0%      0   54    2    0 14191%
c i   33.8  667874  2944113       377     159     84 146093    0    63  196   0%      0   63    2    0 13473%
c i   33.9  667857  2944113       380     160     85 146093    0    64  196   0%      0   63    2    0 13346%
c i   34.0  667856  2944113       403     172     88 146100    0    67  196   0%      0   67    2    0 12761%
c i   34.0  667851  2944113       404     172     88 146100    0    67  196   0%      0   67    2    0 12712%
c i   34.0  667849  2944113       413     179     89 146100    0    68  196   0%      0   68    2    0 12580%
c i   34.3  667848  2944113       510     214    125 146125    0    89  196   0%      0   89    2    0 10837%
c 
c [simplification-3] limit of 128 binary hit after 128 binaries
c [card-2] limit 736028 based on 2944113 irredundant clauses
c [card-2] found 636 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 736028 for elimination
c [card-2] 636 out of 636 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 4990 variables
c [treelook-2] limit 733778 based on 2935112 irredundant clauses
c [treelook-2] scheduled 137985 literals 10%
c [treelook-2] scheduling used 734854 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 733778 based on 2935112 irredundant clauses
c [treelook-2] used 744548 steps
c [treelook-2] 137741 literals remain 10%
c [treelook-2] 85397 variables remain to probed next time 13%
c [decomp-7] removed 85 variables
c [treelook-2] removed 120 variables, found 2336 hbrs
c [unhide-3] limit 183413 based on 2934623 irredundant clauses
c [unhide-3-3] 324 units, 560 failed, 14000 tauts, 0 hbrs, 16818 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 661925 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 512868 not tried 77% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 149055 = 23% variables out of 661925 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 2461355 negative 94.9% of 2593307 except 131952 5.1%
c [phase-count-3] 2406852 positive 92.8% of 2593307 except 186455 7.2%
c [phase-3] phase bias: 506 positive 29%, 1219 negative 71%
c [sort-queue-3] sorted 512870 enqueued variables after 532 conflicts
c [score-dist-3] active 0 (0%), one 0 (0%), zero 512870 (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 154978 variables 23.2% (512870 remain 47%)
c [simplification-3] removed 350806 irredundant clauses 11.9% (2593307 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 1056 (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   47.4  512869  2593307       549     148     95 100322    0    98  185   0%      0   98    2    0 10122%
c i   47.4  512868  2593307       552     149     96 100322    0    98  185   0%      0   98    2    0 10073%
c i   47.5  512867  2593307       558     151     99 100322    0    98  185   0%      0   98    2    0 9963%
c i   48.0  512854  2593307       677     215    121 100345    0   114  185   0%      0  113    2    0 9061%
c i   48.2  512853  2593307       705     229    129 100350    0   122  185   0%      0  121    2    0 8765%
c i   48.2  512852  2593307       718     234    131 100355    0   125  185   0%      0  125    2    0 8558%
c i   48.3  512851  2593307       743     245    135 100364    0   131  185   0%      0  131    2    0 8273%
c i   48.5  512850  2593307       832     287    166 100379    0   141  185   0%      0  141    2    0 7161%
c i   48.5  512849  2593307       842     290    171 100380    0   145  185   0%      0  144    2    0 7085%
c i   48.6  512848  2593307       843     290    171 100380    0   145  185   0%      0  144    2    0 7058%
c i   48.6  512847  2593307       853     295    174 100381    0   147  185   0%      0  146    2    0 7005%
c i   48.6  512846  2593307       860     297    175 100384    0   147  185   0%      0  146    2    0 6904%
c i   48.9  512845  2593307       959     333    208 100408    0   176  185   0%      0  175    2    0 6603%
c i   49.1  512844  2593307      1042     377    224 100429    0   214  185   0%      0  213    2    0 6391%
c 
c [simplification-4] limit 1073 conflicts (hard 11000) hit after 1073 conflicts
c [decomp-8] removed 692 variables
c [basicprobe-2] limit 20732320 based on 2591540 irredundant clauses
c [basicprobe-2-0] 393546 probes remain 77% after last round
c [basicprobe-2-0] 1164 units = 1084 failed (93%) + 80 lifted (7%)
c [basicprobe-2-0] removed 2258 variables, found 107897 hbrs
c [unhide-4] limit 161971 based on 2591540 irredundant clauses
c [unhide-4-4] 326 units, 476 failed, 10337 tauts, 0 hbrs, 43047 literals
c [elim-4] 509140 variables 100% will be scheduled this time
c [elim-4] scheduled 509140 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 15363 not tried 3% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 240831 = 47% variables out of 509140 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 1827041 negative 95.6% of 1911145 except 84104 4.4%
c [phase-count-4] 1792187 positive 93.8% of 1911145 except 118958 6.2%
c [phase-4] phase bias: 346 positive 41%, 508 negative 59%
c [sort-queue-4] sorted 268311 enqueued variables after 1073 conflicts
c [score-dist-4] active 0 (0%), one 0 (0%), zero 268311 (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 244528 variables 47.7% (268311 remain 24%)
c [simplification-4] removed 682162 irredundant clauses 26.3% (1911145 remain 43%)
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 13073 (soft 3073 + delta 10000)
c [simplification-4] new conflict limit 3073 (hard 13073)
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.5  268310  1911145      1278     232    194 64204    1   238  170   0%      1  236    2    0 5384%
c i   69.5  268309  1911145      1284     235    194 64206    1   239  170   0%      1  236    2    0 5375%
c i   69.5  268308  1911145      1286     235    194 64207    1   239  170   0%      1  236    2    0 5341%
c i   69.5  268307  1911145      1287     235    194 64207    1   239  170   0%      1  236    2    0 5321%
c i   69.5  268306  1911145      1288     235    194 64207    1   238  170   0%      1  236    2    0 5300%
c i   69.5  268305  1911145      1294     238    196 64207    1   241  170   0%      1  238    2    0 5293%
c i   69.5  268304  1911145      1295     238    196 64207    1   241  170   0%      1  238    2    0 5273%
c i   69.5  268303  1911145      1297     238    196 64208    1   241  170   0%      1  238    2    0 5239%
c i   69.5  268302  1911145      1298     238    196 64208    1   240  170   0%      1  238    2    0 5219%
c i   69.5  268301  1911145      1299     238    196 64208    1   240  170   0%      1  238    2    0 5199%
c i   69.5  268300  1911145      1305     242    197 64208    1   241  170   0%      1  239    2    0 5163%
c i   69.5  268299  1911145      1306     242    197 64208    1   241  170   0%      1  239    2    0 5143%
c i   69.6  268298  1911145      1316     243    201 64212    1   241  170   0%      1  239    2    0 5031%
c i   69.6  268297  1911145      1322     245    201 64215    1   241  170   0%      1  239    2    0 4953%
c i   69.6  268296  1911145      1331     245    204 64219    1   241  170   0%      1  239    2    0 4879%
c i   69.6  268295  1911145      1343     249    207 64223    1   243  170   0%      1  240    2    0 4771%
c i   69.6  268294  1911145      1350     252    208 64225    1   244  170   0%      1  241    2    0 4750%
c i   69.7  268293  1911145      1363     257    213 64227    1   246  170   0%      1  244    2    0 4713%
c i   69.7  268292  1911145      1383     268    215 64232    1   247  170   0%      1  245    2    0 4570%
c i   69.7  268291  1911145      1388     270    216 64233    1   248  170   0%      1  245    2    0 4528%
c i   69.7  268290  1911145      1389     270    216 64233    1   248  170   0%      1  245    2    0 4510%
c i   69.7  268289  1911145      1390     270    216 64233    1   248  170   0%      1  245    2    0 4493%
c i   69.7  268288  1911145      1391     270    216 64233    1   248  170   0%      1  245    2    0 4475%
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.7  268287  1911145      1392     270    216 64233    1   248  170   0%      1  245    2    0 4458%
c i   69.7  268286  1911145      1397     273    217 64233    1   248  170   0%      1  246    2    0 4479%
c i   69.8  268285  1911145      1412     281    218 64237    1   251  170   0%      1  248    2    0 4443%
c i   69.8  268284  1911145      1413     281    218 64237    1   251  170   0%      1  248    2    0 4426%
c i   70.2  268283  1911145      1541     326    261 64275    1   291  170   0%      1  288    2    0 4076%
c i   70.3  268282  1911145      1579     349    273 64276    1   306  170   0%      1  303    2    0 4183%
c i   70.3  268281  1911145      1590     351    275 64282    1   305  170   0%      1  302    2    0 4102%
c i   70.4  268280  1911145      1612     356    282 64289    1   305  170   0%      1  301    2    0 4052%
c i   70.7  268279  1911145      1716     392    320 64314    1   307  170   0%      1  303    2    0 3776%
c i   70.7  268260  1911145      1717     392    320 64314    1   307  170   0%      1  303    2    0 3761%
c i   70.7  268259  1911145      1718     392    320 64314    1   307  170   0%      1  303    2    0 3746%
c i   70.7  268258  1911145      1730     398    322 64317    1   309  170   0%      1  305    2    0 3754%
c i   70.7  268257  1911145      1736     401    322 64319    1   309  170   0%      1  305    2    0 3712%
c i   70.8  268256  1911145      1760     410    327 64327    1   313  170   0%      1  309    2    0 3707%
c i   70.9  268255  1911145      1777     417    333 64330    1   316  170   0%      1  312    2    0 3709%
c i   70.9  268254  1911145      1780     418    333 64331    1   316  170   0%      1  312    2    0 3685%
c i   70.9  268253  1911145      1781     418    333 64331    1   316  170   0%      1  312    2    0 3670%
c i   70.9  268252  1911145      1789     423    333 64333    1   318  170   0%      1  314    2    0 3645%
c i   70.9  268251  1911145      1797     426    335 64334    1   319  170   0%      1  315    2    0 3621%
c i   70.9  268250  1911145      1798     426    335 64334    1   319  170   0%      1  315    2    0 3607%
c i   70.9  268249  1911145      1803     427    338 64334    1   319  170   0%      1  314    2    0 3581%
c i   70.9  268248  1911145      1805     428    338 64334    1   319  170   0%      1  314    2    0 3566%
c i   71.0  268247  1911145      1825     433    343 64343    1   322  170   0%      1  318    2    0 3511%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   71.0  268246  1911145      1837     438    347 64344    1   323  170   0%      1  319    2    0 3478%
c i   71.1  268245  1911145      1887     454    367 64356    1   330  170   0%      1  325    2    0 3350%
c i   71.1  268244  1911145      1888     454    367 64356    1   330  170   0%      1  325    2    0 3337%
c i   71.1  268243  1911145      1891     455    368 64356    1   330  170   0%      1  325    2    0 3323%
c i   71.1  268242  1911145      1896     458    368 64357    1   330  170   0%      1  325    2    0 3289%
c i   71.2  268241  1911145      1906     461    369 64362    1   331  170   0%      1  326    2    0 3301%
c i   71.4  268240  1911145      2005     506    400 64384    1   363  170   0%      1  358    2    0 3230%
c i   71.4  268239  1911145      2007     506    401 64384    1   363  170   0%      1  358    2    0 3217%
c i   72.1  268238  1911144      2237     601    482 64435    1   390  170   0%      1  383    2    0 3015%
c i   72.1  268237  1911144      2247     604    483 64440    1   390  170   0%      1  383    2    0 2987%
c i   72.2  268236  1911144      2285     618    497 64448    1   395  170   0%      1  388    2    0 2918%
c i   72.2  268235  1911144      2293     621    498 64451    1   396  170   0%      1  389    2    0 2920%
c i   72.4  268234  1911144      2379     654    526 64475    1   401  170   0%      1  393    2    0 2755%
c i   72.5  268233  1911144      2395     660    530 64479    1   402  170   0%      1  394    2    0 2716%
c i   72.5  268232  1911144      2396     660    530 64479    1   402  170   0%      1  394    2    0 2705%
c i   72.5  268231  1911144      2397     660    530 64479    1   402  170   0%      1  394    2    0 2695%
c i   72.5  268230  1911144      2414     666    535 64484    1   401  170   0%      1  393    2    0 2647%
c i   72.5  268229  1911144      2415     666    535 64484    1   401  170   0%      1  393    2    0 2637%
c i   72.6  268228  1911144      2451     679    546 64495    1   411  170   0%      1  403    2    0 2625%
c i   72.6  268227  1911144      2452     679    546 64495    1   411  170   0%      1  403    2    0 2615%
c i   72.6  268226  1911144      2468     687    552 64496    1   414  170   0%      1  406    2    0 2618%
c i   73.0  268225  1911144      2628     764    596 64533    1   458  170   0%      1  449    2    0 2546%
c i   73.4  268224  1911144      2778     841    635 64557    1   460  170   0%      1  450    2    0 2585%
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   73.4  268223  1911144      2780     842    635 64557    1   460  170   0%      1  450    2    0 2578%
c i   73.4  268222  1911144      2787     844    637 64559    1   460  170   0%      1  450    2    0 2542%
c i   73.5  268221  1911144      2819     863    644 64564    1   462  170   0%      1  451    2    0 2551%
c i   73.6  268220  1911144      2825     868    644 64564    1   462  170   0%      1  452    2    0 2593%
c i   73.6  268219  1911144      2829     869    645 64565    1   462  170   0%      1  452    2    0 2569%
c i   73.7  268218  1911144      2886     888    668 64579    1   463  170   0%      1  453    2    0 2407%
c i   73.8  268217  1911144      2936     905    687 64592    1   468  170   0%      1  457    2    0 2276%
c i   74.5  268216  1911142      3187    1005    758 64660    1   514  170   0%      1  501    2    0 2112%
c i   74.5  268215  1911142      3188    1005    758 64660    1   514  170   0%      1  501    2    0 2104%
c i   74.7  268214  1911142      3280    1046    778 64687    1   511  170   0%      1  498    2    0 2045%
c i   74.8  268213  1911142      3303    1054    782 64697    1   512  170   0%      1  498    2    0 2000%
c i   74.8  268212  1911142      3306    1054    783 64698    1   512  170   0%      1  498    2    0 1984%
c i   74.9  268211  1911142      3324    1062    788 64701    1   513  170   0%      1  499    2    0 1966%
c 
c [simplification-5] limit 3342 conflicts (hard 13073) hit after 3342 conflicts
c [quatres-1] found 236898 quaternary clauses 39% in total
c [quatres-1-1] added 104 double-self-subsuming ternary resolvents
c [quatres-1-2] added 2822 single-self-subsuming ternary resolvents
c [quatres-1-2] added 7367 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 268211 free variables schedulable
c [ternres-1] 80744 ternary resolvents (840 bin, 79904 trn)
c [ternres-1] 23121 variables remain 9% (245090 retained 91%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 8751 xors of average arity 3.0
c [gauss-1] connected 25907 occurrences of 9508 variables (average 2.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 1651 variables
c [simpleprobe-3] 248634 schedulable variables 93%
c [simpleprobe-3] limit 4517233 penalty 0 = 0 + 0
c [decomp-10] removed 236 variables
c [simpleprobe-3] 222424 variables remain 84% (43900 retained 16%)
c [simpleprobe-3] removed 236 variables, found 7110 hbrs, 87 units
c [unhide-5] limit 119037 based on 1904605 irredundant clauses
c [unhide-5-5] 206 units, 192 failed, 60916 tauts, 0 hbrs, 71829 literals
c [transred-1] limit 1855183 based on 1855183 irredundant clauses
c [transred-1] removed 561 transitive binary clauses
c [transred-1] found 22 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 265926 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 21762 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 29
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 7 clauses out of 10 (70%) of length 26
c [cce-1-1] eliminated 3 clauses out of 7 (43%) of length 25
c [cce-1-1] eliminated 6 clauses out of 10 (60%) of length 24
c [cce-1-1] eliminated 5 clauses out of 9 (56%) of length 23
c [cce-1-1] eliminated 3 clauses out of 11 (27%) of length 22
c [cce-1-1] eliminated 5 clauses out of 24 (21%) of length 21
c [cce-1-1] eliminated 10 clauses out of 24 (42%) of length 19
c [cce-1-1] eliminated 220 clauses out of 865 (25%) of length 18
c [cce-1-1] eliminated 104 clauses out of 1128 (9%) of length 17
c [cce-1-1] eliminated 258 clauses out of 757 (34%) of length 16
c [cce-1-1] eliminated 254 clauses out of 1421 (18%) of length 15
c [cce-1-1] eliminated 618 clauses out of 2371 (26%) of length 14
c [cce-1-1] eliminated 208 clauses out of 3773 (6%) of length 13
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1705 large clauses in 30000040 steps
c [cce-1-1] allowing another 15000020 steps for small clauses
c [cce-1-1] scheduling 1027960 clauses = 813205 binary + 214755 ternary
c [cce-1-1] tried to eliminate 6897 small clauses 1%
c [cce-1-1] eliminated 1220 binary clauses 0%
c [cce-1-1] eliminated 277 ternary clauses 0%
c [cce-1-1] eliminated 1497 small clauses 0%
c [cce-1-1] eliminated 1497 small clauses in 30000226 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3202 covered clauses in round 1
c [cce-1] eliminated 3202 covered clauses in TOTAL during 1 rounds
c [cce-1] 3202 < 1/100 * 1829273 = 18292 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 265396 variables 100%
c [elim-5] limit of 22586166 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 157919 not tried 60% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 12734 = 5% variables out of 265396 scheduled
c [bca-1] limit of 10000000 steps and 3601974 added (scaled 2)
c [bca-1] 484676 out of 505326 literals actually usable 96%
c [bca-1] added 6275 blocked clauses in 1531508 steps
c [sweep-1] limit 3601474 based on 1800737 irredundant clauses
c [sweep-1-1] 108786 pos 43.1% + 143876 neg 56.9% = 252662 sched 100.0% ret 0
c [sweep-1-1] 3605407 steps 101 queries 76945.72 avg class size
c [sweep-1-1] 1368 decisions 94 SAT calls 31.57 avg env size
c [sweep-1-1] 252096 variables remain 100% (566 retained 0%)
c [decomp-11] removed 413 variables
c [sweep-1-1] removed 413 vars (0 failed, 15 eqs, 21 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 413 vars in TOTAL (1 rounds, 100 queries)
c [sort-queue-5] sorted 252249 enqueued variables after 3342 conflicts
c [score-dist-5] active 0 (0%), one 0 (0%), zero 252249 (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 15962 variables 6.0% (252249 remain 23%)
c [simplification-5] removed 111386 irredundant clauses 5.8% (1799756 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 15342 (soft 5342 + delta 10000)
c [simplification-5] new conflict limit 5342 (hard 15342)
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   93.2  252248  1799756      3391    7101  60884 74799    1   511  171   0%      1  496    2    0 2054%
c i   93.2  252247  1799756      3393    7101  60885 74799    1   510  171   0%      1  496    2    0 2045%
c i   93.6  252246  1799756      3513    7160  60920 74822    1   513  171   0%      1  497    2    0 2080%
c i   93.6  252245  1799756      3527    7165  60925 74825    1   514  171   0%      1  499    2    0 2051%
c i   93.6  252198  1799756      3528    7165  60925 74825    1   514  171   0%      1  499    2    0 2043%
c i   93.7  252197  1799756      3580    7186  60936 74840    1   520  171   0%      1  504    2    0 1971%
c i   93.7  252196  1799756      3581    7186  60936 74840    1   519  171   0%      1  504    2    0 1963%
c i   93.8  252195  1799756      3588    7188  60937 74843    1   520  171   0%      1  504    2    0 1941%
c i   93.8  252194  1799756      3596    7190  60936 74847    1   520  171   0%      1  504    2    0 1919%
c i   93.8  252193  1799756      3599    7191  60937 74847    1   520  171   0%      1  504    2    0 1907%
c i   93.8  252192  1799756      3600    7191  60937 74847    1   520  171   0%      1  504    2    0 1900%
c i   93.8  252191  1799756      3609    7192  60942 74849    1   519  171   0%      1  503    2    0 1872%
c i   93.9  252190  1799756      3637    7200  60947 74861    1   520  171   0%      1  504    2    0 1823%
c i   94.0  252189  1799756      3692    7221  60965 74874    1   524  171   0%      1  508    2    0 1797%
c i   94.0  252188  1799756      3698    7224  60967 74874    1   525  171   0%      1  508    2    0 1793%
c i   94.0  252187  1799756      3700    7225  60967 74874    1   525  171   0%      1  508    2    0 1782%
c i   94.0  252186  1799756      3717    7232  60971 74879    1   529  171   0%      1  512    2    0 1783%
c i   94.5  252185  1799756      3891    7318  61017 74916    1   591  171   0%      1  572    2    0 1873%
c i   94.5  252184  1799756      3896    7318  61017 74918    1   590  171   0%      1  572    2    0 1864%
c i   94.9  252183  1799756      4083    7410  61062 74963    1   591  171   0%      1  571    2    0 1811%
c i   94.9  252182  1799756      4084    7410  61062 74963    1   591  171   0%      1  571    2    0 1804%
c i   94.9  252181  1799756      4085    7410  61062 74963    1   590  171   0%      1  570    2    0 1797%
c i   95.2  252180  1799756      4187    7468  61080 74987    1   602  171   0%      1  581    2    0 1752%
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   95.2  252143  1799756      4190    7468  61080 74989    1   602  171   0%      1  581    2    0 1738%
c i   95.3  252142  1799756      4250    7492  61101 75001    1   604  171   0%      1  583    2    0 1654%
c i   95.3  251930  1799756      4257    7494  61105 75001    1   604  171   0%      1  583    2    0 1636%
c i   95.6  251929  1799756      4341    7536  61126 75020    1   617  171   0%      1  595    2    0 1621%
c i   95.6  251928  1799756      4368    7549  61134 75025    1   627  171   0%      1  605    2    0 1626%
c i   95.8  251927  1799756      4412    7570  61149 75032    1   637  171   0%      1  614    2    0 1643%
c i   95.8  251926  1799756      4419    7573  61150 75034    1   636  171   0%      1  613    2    0 1635%
c i   95.8  251925  1799756      4421    7573  61150 75035    1   636  171   0%      1  613    2    0 1625%
c i   95.8  251924  1799756      4425    7575  61151 75035    1   635  171   0%      1  612    2    0 1617%
c i   95.8  251923  1799756      4429    7576  61152 75036    1   635  171   0%      1  612    2    0 1603%
c i   95.8  251922  1799756      4434    7577  61154 75037    1   634  171   0%      1  611    2    0 1595%
c i   96.3  251921  1799756      4647    7684  61197 75089    1   636  171   0%      1  611    2    0 1561%
c i   96.8  251920  1799755      4868    7788  61265 75131    1   663  171   0%      1  636    2    0 1483%
c i   97.1  251919  1799755      4963    7827  61296 75154    1   680  171   0%      1  652    2    0 1423%
c i   97.2  251918  1799755      5033    7859  61308 75176    1   673  171   0%      1  644    2    0 1342%
c i   97.2  251567  1799755      5035    7859  61308 75177    1   672  171   0%      1  644    2    0 1334%
c i   97.3  251554  1799755      5086    7880  61318 75193    1   670  171   0%      1  641    2    0 1339%
c i   97.4  251553  1799755      5103    7887  61321 75199    1   671  171   0%      1  642    2    0 1333%
c i   97.5  251474  1799755      5140    7905  61332 75206    1   672  171   0%      1  642    2    0 1360%
c i   97.5  251473  1799755      5151    7908  61336 75209    1   672  171   0%      1  642    2    0 1347%
c i   97.6  251472  1799755      5204    7931  61349 75222    1   671  171   0%      1  641    2    0 1306%
c i   97.7  251471  1799755      5214    7935  61352 75224    1   672  171   0%      1  641    2    0 1300%
c i   97.7  251470  1799755      5236    7946  61356 75230    1   671  171   0%      1  641    2    0 1275%
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   97.8  251469  1799755      5249    7951  61363 75230    1   673  171   0%      1  643    2    0 1269%
c i   98.1  251468  1799755      5409    8027  61409 75263    1   704  171   0%      1  672    2    0 1274%
c 
c [simplification-6] limit 5433 conflicts (hard 15342) hit after 5433 conflicts
c [quatres-2] found 240449 quaternary clauses 40% in total
c [quatres-2-1] removed 36 duplicate quaternary clauses
c [quatres-2-1] added 30 double-self-subsuming ternary resolvents
c [quatres-2-2] added 1919 single-self-subsuming ternary resolvents
c [quatres-2-2] added 5757 quaternary resolvents
c [ternres-2] limit 7198016 based on 1799504 irredundant clauses
c [ternres-2] 21338 schedulable variables 8%
c [ternres-2] 42428 ternary resolvents (1595 bin, 40833 trn)
c [ternres-2] 12650 variables remain 5% (238394 retained 95%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 241 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] 241 out of 241 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 2154 variables
c [treelook-3] limit 446617 based on 1786471 irredundant clauses
c [treelook-3] scheduled 53028 literals 11%
c [treelook-3] scheduling used 447052 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 446617 based on 1786471 irredundant clauses
c [treelook-3] used 466577 steps
c [treelook-3] 52981 literals remain 11%
c [treelook-3] 31102 variables remain to probed next time 12%
c [decomp-13] removed 5 variables
c [treelook-3] removed 13 variables, found 961 hbrs
c [unhide-6] limit 111645 based on 1786334 irredundant clauses
c [unhide-6-6] 280 units, 554 failed, 6892 tauts, 0 hbrs, 43375 literals
c [transred-2] limit 1783182 based on 1783182 irredundant clauses
c [transred-2] removed 608 transitive binary clauses
c [transred-2] found 13 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 249195 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 15332 blocked clauses
c [block-2] 15332 < 1/100 * 1782730 = 17827 considered unsuccessful
c [elim-6] 14937 variables 6% will be scheduled this time
c [elim-6] scheduled 14937 variables 6%
c [elim-6] limit of 33579051 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 7060 not tried 3% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 92 = 1% variables out of 14937 scheduled
c [elim-6] 92 < 1/100 * 14937 = 149 considered unsuccessful
c [bca-2] limit of 10000000 steps and 3480313 added (scaled 2)
c [bca-2] 465857 out of 497816 literals actually usable 94%
c [bca-2] added 1825 blocked clauses in 1447994 steps
c [sweep-2] limit 3476676 based on 1738338 irredundant clauses
c [sweep-2-1] 105901 pos 42.6% + 142457 neg 57.4% = 248358 sched 99.8% ret 549
c [sweep-2-1] 3497828 steps 99 queries 78517.07 avg class size
c [sweep-2-1] 1448 decisions 98 SAT calls 36.04 avg env size
c [sweep-2-1] 247612 variables remain 99% (1293 retained 1%)
c [decomp-14] removed 764 variables
c [sweep-2-1] removed 764 vars (0 failed, 5 eqs, 8 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 764 vars in TOTAL (1 rounds, 98 queries)
c [sort-queue-6] sorted 248143 enqueued variables after 5433 conflicts
c [score-dist-6] active 0 (0%), one 0 (0%), zero 248143 (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 2901 variables 1.2% (248143 remain 23%)
c [simplification-6] removed 63440 irredundant clauses 3.5% (1736315 remain 39%)
c [simplification-6] maximum reduction of 4% = max (1%, 4%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 4000
c [simplification-6] penalized conflict interval 4000 = 1 * 4000
c [simplification-6] hard conflict limit 19433 (soft 9433 + delta 10000)
c [simplification-6] new conflict limit 9433 (hard 19433)
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  111.8  248142  1736315      5451   13000  89286 79524    1   707  170   0%      1  675    2    0 1272%
c i  111.8  248120  1736315      5452   13000  89286 79524    1   707  170   0%      1  675    2    0 1267%
c i  111.8  248099  1736315      5456   13000  89287 79526    1   707  170   0%      1  674    2    0 1257%
c i  111.8  248098  1736315      5463   13001  89290 79528    1   705  170   0%      1  673    2    0 1244%
c i  111.8  248097  1736315      5472   13007  89292 79528    1   704  170   0%      1  671    2    0 1254%
c i  111.8  248096  1736315      5488   13014  89298 79530    1   702  170   0%      1  669    2    0 1253%
c i  111.8  248095  1736315      5490   13014  89299 79530    1   702  170   0%      1  669    2    0 1248%
c i  112.3  248090  1736315      5732   13142  89325 79609    2   695  170   0%      1  660    2    0 1256%
c i  112.5  248089  1736315      5814   13168  89351 79636    2   697  170   0%      1  661    2    0 1180%
c i  112.6  248088  1736315      5835   13180  89358 79637    2   698  170   0%      1  662    2    0 1201%
c i  113.0  248087  1736315      6001   13254  89402 79680    2   727  170   0%      1  689    2    0 1168%
c i  113.0  248086  1736315      6007   13256  89402 79683    2   726  170   0%      1  688    2    0 1160%
c i  113.4  248085  1736315      6184   13339  89459 79716    2   715  170   0%      1  675    2    0 1179%
c i  113.5  248079  1736314      6214   13350  89471 79722    2   713  170   0%      1  673    2    0 1155%
c i  113.6  248078  1736314      6250   13370  89480 79728    2   714  170   0%      1  673    2    0 1156%
c i  113.6  248077  1736314      6252   13370  89480 79729    2   713  170   0%      1  673    2    0 1149%
c i  113.6  248076  1736314      6253   13370  89480 79729    2   713  170   0%      1  673    2    0 1144%
c i  113.6  248075  1736314      6263   13374  89482 79732    2   713  170   0%      1  672    2    0 1127%
c i  113.9  248073  1736314      6393   13417  89525 79770    2   712  170   0%      1  670    2    0 1042%
c i  114.0  248072  1736314      6422   13423  89541 79775    2   716  170   0%      1  674    2    0 1031%
c i  114.7  248071  1736314      6723   13560  89632 79841    2   728  170   0%      1  683    2    0 1073%
c i  114.8  248069  1736314      6759   13578  89642 79848    2   730  170   0%      1  684    2    0 1074%
c i  114.8  248068  1736314      6785   13590  89646 79856    2   730  170   0%      1  684    2    0 1051%
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  115.0  248067  1736314      6893   13627  89684 79885    2   724  170   0%      1  677    2    0  957%
c i  115.3  248066  1736314      6981   13661  89711 79907    2   733  170   0%      1  685    2    0  961%
c i  115.3  248065  1736314      6987   13664  89712 79908    2   734  170   0%      1  685    2    0  963%
c i  115.5  248064  1736314      7081   13701  89741 79934    2   745  170   0%      1  696    2    0  935%
c i  116.0  248063  1736313      7307   13812  89794 79993    2   726  170   0%      1  675    2    0  974%
c i  116.3  248062  1736313      7455   13876  89839 80028    2   728  170   0%      1  675    2    0  942%
c i  116.4  248061  1736313      7482   13888  89849 80032    2   728  170   0%      1  675    2    0  946%
c i  116.5  248060  1736313      7534   13905  89878 80037    2   735  170   0%      1  681    2    0  936%
c i  116.8  248059  1736313      7648   13957  89906 80066    2   756  170   0%      1  701    2    0  977%
c i  116.8  248058  1736313      7649   13957  89906 80066    2   756  170   0%      1  701    2    0  973%
c i  116.8  248041  1736313      7661   13963  89908 80068    2   754  170   0%      1  699    2    0  976%
c i  117.0  248040  1736313      7766   14001  89946 80093    2   745  170   0%      1  689    2    0  931%
c i  117.4  248033  1736313      7928   14084  89973 80134    2   743  170   0%      1  685    2    0  929%
c i  117.6  248032  1736313      8046   14127  90018 80162    2   741  170   0%      1  682    2    0  855%
c i  118.1  248031  1736313      8240   14230  90061 80206    2   779  170   0%      1  718    2    0  939%
c i  118.1  248004  1736313      8241   14230  90061 80206    2   779  170   0%      1  718    2    0  935%
c i  118.1  248003  1736313      8272   14237  90075 80213    2   774  170   0%      1  713    2    0  917%
c i  118.5  248002  1736313      8406   14297  90101 80256    2   759  170   0%      1  696    2    0  878%
c i  118.5  248001  1736313      8408   14298  90101 80256    2   759  170   0%      1  696    2    0  876%
c i  118.8  247999  1736313      8505   14338  90138 80274    2   756  170   0%      1  692    2    0  854%
c i  119.0  247998  1736313      8571   14363  90166 80286    2   759  170   0%      1  695    2    0  826%
c i  119.1  247997  1736313      8604   14374  90181 80291    2   758  170   0%      1  693    2    0  801%
c i  119.2  247996  1736313      8660   14400  90201 80298    2   764  170   0%      1  698    2    0  819%
c 
c [simplification-7] limit of 2517 ternary hit after 2517 ternaries
c [quatres-3] found 240542 quaternary clauses 42% in total
c [quatres-3-1] removed 8 duplicate quaternary clauses
c [quatres-3-1] added 16 double-self-subsuming ternary resolvents
c [quatres-3-2] added 594 single-self-subsuming ternary resolvents
c [quatres-3-2] added 3945 quaternary resolvents
c [ternres-3] limit 6945044 based on 1736261 irredundant clauses
c [ternres-3] 12307 schedulable variables 5%
c [ternres-3] 39807 ternary resolvents (1524 bin, 38283 trn)
c [ternres-3] 7083 variables remain 3% (240913 retained 97%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 3721 xors of average arity 3.0
c [gauss-2] connected 11087 occurrences of 4311 variables (average 2.6)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 547 variables
c [basicprobe-3] limit 13866088 based on 1733261 irredundant clauses
c [basicprobe-3-0] 169262 probes remain 69% after last round
c [basicprobe-3-0] 726 units = 688 failed (95%) + 38 lifted (5%)
c [basicprobe-3-0] removed 1104 variables, found 48221 hbrs
c [bate-1] eliminated 1048 asymmetric tautologies during probing
c [unhide-7] limit 108263 based on 1732213 irredundant clauses
c [unhide-7-7] 201 units, 241 failed, 27055 tauts, 0 hbrs, 20763 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 815 transitive binary clauses
c [transred-3] found 11 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 23
c [cce-2-1] eliminated 1 clauses out of 5 (20%) of length 22
c [cce-2-1] eliminated 3 clauses out of 9 (33%) of length 20
c [cce-2-1] eliminated 4 clauses out of 20 (20%) of length 19
c [cce-2-1] eliminated 7 clauses out of 600 (1%) of length 18
c [cce-2-1] eliminated 18 clauses out of 856 (2%) of length 17
c [cce-2-1] eliminated 18 clauses out of 659 (3%) of length 16
c [cce-2-1] eliminated 23 clauses out of 1256 (2%) of length 15
c [cce-2-1] eliminated 117 clauses out of 1464 (8%) of length 14
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 192 large clauses in 15000004 steps
c [cce-2-1] allowing another 7500002 steps for small clauses
c [cce-2-1] scheduling 947686 clauses = 732766 binary + 214920 ternary
c [cce-2-1] tried to eliminate 2159 small clauses 0%
c [cce-2-1] eliminated 316 binary clauses 0%
c [cce-2-1] eliminated 89 ternary clauses 0%
c [cce-2-1] eliminated 405 small clauses 0%
c [cce-2-1] eliminated 4775 small clauses in 15000007 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 4967 covered clauses in round 1
c [cce-2] eliminated 4967 covered clauses in TOTAL during 1 rounds
c [cce-2] 4967 < 1/100 * 1696308 = 16963 considered unsuccessful
c [bca-3] limit of 10000000 steps and 3387232 added (scaled 2)
c [bca-3] 451763 out of 491716 literals actually usable 92%
c [bca-3] added 256 blocked clauses in 1380706 steps
c [sweep-3] limit 3382682 based on 1691341 irredundant clauses
c [sweep-3-1] 102407 pos 41.9% + 142167 neg 58.1% = 244574 sched 99.5% ret 1283
c [sweep-3-1] 3521877 steps 65 queries 69191.51 avg class size
c [sweep-3-1] 679 decisions 53 SAT calls 39.15 avg env size
c [sweep-3-1] 244295 variables remain 99% (1560 retained 1%)
c [decomp-16] removed 1483 variables
c [sweep-3-1] removed 1483 vars (0 failed, 11 eqs, 20 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 1483 vars in TOTAL (1 rounds, 64 queries)
c [sort-queue-7] sorted 244374 enqueued variables after 8704 conflicts
c [score-dist-7] active 0 (0%), one 0 (0%), zero 244374 (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 3622 variables 1.5% (244374 remain 22%)
c [simplification-7] removed 48044 irredundant clauses 2.8% (1688269 remain 38%)
c [simplification-7] maximum reduction of 3% = max (1%, 3%)
c [simplification-7] forced so keeping old conflict interval 4000
c [simplification-7] conflict limit remains at 9495 (hard 19433)
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  130.6  244373  1688269      8735   17732 110687 114172    2   774  170   0%      1  708    2    0  882%
c i  130.6  244372  1688269      8736   17732 110687 114172    2   774  170   0%      1  708    2    0  878%
c i  130.6  244371  1688269      8737   17732 110687 114172    2   774  170   0%      1  708    2    0  875%
c i  130.6  244370  1688269      8758   17746 110691 114174    2   771  170   0%      1  705    2    0  882%
c i  130.8  244369  1688269      8791   17767 110697 114178    2   770  170   0%      1  703    2    0  879%
c i  131.4  244368  1688269      8970   17840 110756 114218    2   759  170   0%      1  690    2    0  864%
c i  131.4  244367  1688269      8973   17840 110756 114219    2   758  170   0%      1  690    2    0  859%
c i  131.8  244366  1688269      9095   17891 110794 114248    2   758  170   0%      1  689    2    0  802%
c i  132.3  244365  1688269      9268   17968 110839 114293    2   774  170   0%      1  702    2    0  840%
c i  132.3  244364  1688269      9270   17969 110839 114293    2   773  170   0%      1  701    2    0  842%
c i  132.3  244363  1688269      9274   17971 110840 114293    2   773  170   0%      1  701    2    0  844%
c i  132.3  244362  1688269      9280   17973 110841 114295    2   772  170   0%      1  700    2    0  834%
c i  133.0  244361  1688269      9448   18046 110892 114337    2   755  170   0%      1  682    2    0  806%
c i  133.1  244360  1688269      9488   18064 110905 114345    2   754  170   0%      1  680    2    0  790%
c i  133.2  244359  1688269      9493   18064 110907 114347    2   753  170   0%      1  679    2    0  784%
c i  133.3  244358  1688269      9519   18073 110915 114355    2   752  170   0%      1  678    2    0  767%
c 
c [simplification-8] limit 9528 conflicts (hard 19433) hit after 9528 conflicts
c [quatres-4] found 239720 quaternary clauses 43% in total
c [quatres-4-1] removed 50 duplicate quaternary clauses
c [quatres-4-1] added 12 double-self-subsuming ternary resolvents
c [quatres-4-2] added 525 single-self-subsuming ternary resolvents
c [quatres-4-2] added 2161 quaternary resolvents
c [ternres-4] limit 6752844 based on 1688211 irredundant clauses
c [ternres-4] 6914 schedulable variables 3%
c [ternres-4] 39978 ternary resolvents (1294 bin, 38684 trn)
c [ternres-4] 3655 variables remain 1% (240703 retained 99%)
c [decomp-17] removed 372 variables
c [simpleprobe-4] 203574 schedulable variables 83%
c [simpleprobe-4] limit 11828358 penalty 0 = 0 + 0
c [decomp-18] removed 898 variables
c [simpleprobe-4] 207625 variables remain 85% (35479 retained 15%)
c [simpleprobe-4] removed 898 variables, found 32910 hbrs, 195 units
c [unhide-8] limit 147854 with penalty 2 = 0 + 2
c [unhide-8-8] 117 units, 483 failed, 15805 tauts, 0 hbrs, 20272 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 775 transitive binary clauses
c [transred-4] found 14 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 242508 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 3570 blocked clauses
c [block-3] 3570 < 1/100 * 1678803 = 16788 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 242359 variables 100%
c [elim-7] limit of 29570897 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 116366 not tried 48% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 11020 = 5% variables out of 242359 scheduled
c [bca-4] limit of 10000000 steps and 3303194 added (scaled 2)
c [bca-4] 423469 out of 462680 literals actually usable 92%
c [bca-4] added 966 blocked clauses in 1320741 steps
c [sweep-4] limit 3298516 based on 1649258 irredundant clauses
c [sweep-4-1] 95300 pos 41.5% + 134570 neg 58.5% = 229870 sched 99.4% ret 1469
c [sweep-4-1] 3341806 steps 77 queries 63795.92 avg class size
c [sweep-4-1] 1084 decisions 70 SAT calls 36.53 avg env size
c [sweep-4-1] 229307 variables remain 99% (2006 retained 1%)
c [decomp-19] removed 526 variables
c [sweep-4-1] removed 526 vars (0 failed, 13 eqs, 17 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 526 vars in TOTAL (1 rounds, 76 queries)
c [sort-queue-8] sorted 230813 enqueued variables after 9528 conflicts
c [score-dist-8] active 0 (0%), one 0 (0%), zero 230813 (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 13545 variables 5.5% (230813 remain 21%)
c [simplification-8] removed 40897 irredundant clauses 2.4% (1647372 remain 37%)
c [simplification-8] maximum reduction of 6% = max (6%, 2%)
c [simplification-8] large reduction 6% >= 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 21528 (soft 11528 + delta 10000)
c [simplification-8] new conflict limit 11528 (hard 21528)
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  148.3  230812  1647372      9682   18313 116324 119892    2   735  170   0%      1  659    2    0  781%
c i  149.0  230811  1647372      9890   18409 116384 119935    2   737  170   0%      1  659    2    0  770%
c i  149.2  230810  1647372      9949   18435 116403 119945    2   747  170   0%      1  668    2    0  778%
c i  149.9  230809  1647372     10178   18544 116472 119989    2   752  170   0%      1  671    2    0  789%
c i  150.0  230806  1647372     10190   18551 116475 119990    2   752  170   0%      1  671    2    0  789%
c i  150.6  230805  1647371     10378   18642 116513 120046    2   760  170   0%      1  677    2    0  804%
c i  152.0  230804  1647371     10717   18826 116592 120108    2   772  170   0%      2  686    3    0  875%
c i  152.5  230802  1647371     10833   18888 116625 120127    2   779  170   0%      2  691    3    0  846%
c i  152.6  230801  1647371     10861   18903 116633 120130    2   785  170   0%      1  697    3    0  850%
c i  154.7  230799  1647371     11422   19215 116766 120240    2   837  170   0%      3  743    3    0  884%
c 
c [simplification-9] limit 11528 conflicts (hard 21528) hit after 11529 conflicts
c [quatres-5] found 244445 quaternary clauses 43% in total
c [quatres-5-1] removed 42 duplicate quaternary clauses
c [quatres-5-1] added 15 double-self-subsuming ternary resolvents
c [quatres-5-2] added 1409 single-self-subsuming ternary resolvents
c [quatres-5-2] added 3802 quaternary resolvents
c [ternres-5] limit 6588968 based on 1647242 irredundant clauses
c [ternres-5] 3492 schedulable variables 2%
c [ternres-5] 37758 ternary resolvents (937 bin, 36821 trn)
c [ternres-5] 2007 variables remain 1% (228792 retained 99%)
c [decomp-20] removed 309 variables
c [treelook-4] limit 411632 based on 1646530 irredundant clauses
c [treelook-4] scheduled 46686 literals 10%
c [treelook-4] scheduling used 411635 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 411632 based on 1646530 irredundant clauses
c [treelook-4] used 579361 steps
c [treelook-4] 46649 literals remain 10%
c [treelook-4] 21785 variables remain to probed next time 9%
c [decomp-21] removed 1 variables
c [treelook-4] removed 2 variables, found 1579 hbrs
c [unhide-9] limit 200240 with penalty 2 = 0 + 2
c [unhide-9-9] 84 units, 171 failed, 18109 tauts, 0 hbrs, 16247 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 897 transitive binary clauses
c [transred-5] found 27 units
c [elim-8] 6938 variables 3% will be scheduled this time
c [elim-8] scheduled 6938 variables 3%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1601920820 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 2 variables 0% in round 1 in 443970362 steps
c [elim-8-1] backward subsumption/strengthening limit 443970300
c [elim-8-1-1] backward checking 34649 touched variables 15%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 2374 and strengthened 6399 clauses in 124768648 steps
c [elim-8-1] rescheduled 15746 variables 7% by backward subsumption
c [elim-8-2] eliminated 479 variables 0% in round 2 in 225013859 steps
c [elim-8-2] backward subsumption/strengthening limit 225013800
c [elim-8-2-1] backward checking 11039 touched variables 5%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 504 and strengthened 702 clauses in 37352333 steps
c [elim-8-2] rescheduled 3016 variables 1% by backward subsumption
c [elim-8-3] eliminated 104 variables 0% in round 3 in 43635536 steps
c [elim-8-3] backward subsumption/strengthening limit 43635500
c [elim-8-3-1] backward checking 1453 touched variables 1%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 69 and strengthened 198 clauses in 6502137 steps
c [elim-8] incomplete 515 not tried 0% in round 3
c [elim-8] transition to [ all 0 rem 1 ] state
c [elim-8] eliminated 676 = 10% variables out of 6938 scheduled
c [elim-8] 676 < 1/100 * 6938 = 69 considered unsuccessful
c [bca-5] limit of 10000000 steps and 3205465 added (scaled 2)
c [bca-5] 413378 out of 458972 literals actually usable 90%
c [bca-5] added 624 blocked clauses in 1288114 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 12014400 penalty 0 = 0 + 0
c [sweep-5-1] 92930 pos 40.8% + 134575 neg 59.2% = 227505 sched 99.1% ret 1980
c [sweep-5-1] 12047267 steps 278 queries 51383.92 avg class size
c [sweep-5-1] 3934 decisions 273 SAT calls 33.27 avg env size
c [sweep-5-1] 225389 variables remain 98% (4021 retained 2%)
c [decomp-22] removed 852 variables
c [sweep-5-1] removed 852 vars (0 failed, 63 eqs, 60 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 852 vars in TOTAL (1 rounds, 277 queries)
c [sort-queue-9] sorted 228633 enqueued variables after 11529 conflicts
c [score-dist-9] active 0 (0%), one 0 (0%), zero 228633 (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 2166 variables 0.9% (228633 remain 21%)
c [simplification-9] removed 50292 irredundant clauses 3.1% (1597079 remain 36%)
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 9000
c [simplification-9] penalized conflict interval 9000 = 1 * 9000
c [simplification-9] hard conflict limit 30529 (soft 20529 + delta 10000)
c [simplification-9] new conflict limit 20529 (hard 30529)
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  180.1  228632  1597079     12251   22928 130842 120221    2   844  168   0%      5  741    3    0  778%
c i  180.3  228631  1597079     12314   22960 130860 120233    2   847  168   0%      5  743    3    0  781%
c i  180.8  228630  1597079     12455   23036 130888 120267    2   867  168   0%      4  761    3    0  716%
c i  180.8  228629  1597079     12468   23037 130892 120274    2   864  168   0%      4  758    3    0  699%
c i  182.8  228628  1597079     13040   23356 131040 120368    2   899  168   0%      4  786    3    0  666%
c i  182.8  228627  1597079     13041   23356 131040 120368    2   899  168   0%      4  786    3    0  664%
c i  183.9  228626  1597079     13338   23531 131108 120413    2   889  168   0%      4  774    3    0  669%
c i  184.5  228624  1597079     13488   23601 131153 120445    2   916  168   0%      3  798    3    0  629%
c i  184.9  228623  1597079     13607   23665 131178 120471    2   902  168   0%      3  783    3    0  625%
c i  185.4  228622  1597079     13735   23740 131205 120492    2   906  168   0%      3  786    3    0  630%
c i  186.7  228621  1597079     14146   23985 131304 120551    2   917  168   0%      3  791    3    0  617%
c i  187.7  228620  1597079     14450   24129 131389 120620    2   926  168   0%      3  797    2    0  547%
c i  189.1  228619  1597078     14796   24301 131495 120679    2   932  168   0%      3  799    2    0  546%
c i  189.6  228618  1597078     14971   24396 131546 120706    2   930  168   0%      2  795    2    0  551%
c i  190.1  228617  1597078     15095   24470 131574 120722    2   925  168   0%      2  788    3    0  592%
c i  190.1  228616  1597078     15110   24477 131576 120727    2   925  168   0%      2  787    3    0  579%
c i  190.4  228615  1597078     15193   24521 131593 120744    2   932  168   0%      2  794    3    0  564%
c i  190.6  228614  1597078     15253   24545 131615 120757    2   940  168   0%      2  801    3    0  543%
c i  190.6  228613  1597078     15258   24545 131618 120758    2   940  168   0%      2  801    2    0  538%
c i  190.6  228612  1597078     15267   24545 131620 120764    2   938  168   0%      2  799    2    0  528%
c i  190.6  228611  1597078     15272   24545 131621 120767    2   936  168   0%      2  798    2    0  521%
c i  190.6  228610  1597078     15281   24545 131623 120773    2   935  168   0%      2  796    2    0  512%
c i  192.3  228609  1597078     15718   24799 131724 120845    2   941  168   0%      2  797    3    0  548%
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  193.2  228608  1597078     15938   24932 131777 120875    2   943  168   0%      2  796    3    0  623%
c i  193.4  228607  1597078     15974   24958 131782 120878    2   941  168   0%      2  793    3    0  635%
c i  193.6  228606  1597078     16012   24982 131788 120884    2   937  168   0%      2  789    3    0  617%
c i  194.5  228605  1597078     16243   25110 131845 120925    2   946  168   0%      2  796    3    0  541%
c i  195.5  228604  1597078     16503   25247 131913 120972    2   929  168   0%      2  776    3    1  547%
c i  195.8  228603  1597078     16569   25278 131927 120992    2   928  168   0%      2  774    3    1  515%
c i  196.3  228602  1597078     16698   25356 131959 121010    2   942  168   0%      2  786    3    1  514%
c i  196.8  228601  1597078     16810   25425 131972 121036    3   938  168   0%      1  781    3    1  569%
c i  197.7  228600  1597078     17004   25540 132009 121072    3   928  168   0%      1  769    3    1  543%
c i  198.1  228599  1597078     17092   25590 132029 121087    3   936  168   0%      1  775    3    1  561%
c i  198.5  228598  1597078     17186   25638 132053 121106    3   946  168   0%      1  784    3    1  540%
c 
c [simplification-10] limit of 3516 binary hit after 3516 binaries
c [quatres-6] found 241137 quaternary clauses 45% in total
c [quatres-6-1] removed 121 duplicate quaternary clauses
c [quatres-6-1] added 21 double-self-subsuming ternary resolvents
c [quatres-6-2] added 320 single-self-subsuming ternary resolvents
c [quatres-6-2] added 1899 quaternary resolvents
c [ternres-6] limit 7322148 with penalty 0 = 0 + 0
c [ternres-6] 1981 schedulable variables 1%
c [ternres-6] 37216 ternary resolvents (1047 bin, 36169 trn)
c [ternres-6] 614 variables remain 0% (227984 retained 100%)
c [card-4] limit 457634 penalty 3 = 3 + 0
c [card-4] found 247 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 457634 for elimination
c [card-4] 247 out of 247 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 798521 based on 1597043 irredundant clauses
c [gauss-3] extracted 2424 xors of average arity 3.0
c [gauss-3] connected 7230 occurrences of 2852 variables (average 2.5)
c [gauss-3] limit 798174 based on 1596348 irredundant clauses
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 363 variables
c [basicprobe-4] limit 36610741 penalty 0 = 0 + 0
c [basicprobe-4-0] 137524 probes remain 61% after last round
c [basicprobe-4-0] 900 units = 858 failed (95%) + 42 lifted (5%)
c [basicprobe-4-0] removed 1151 variables, found 48244 hbrs
c [bate-2] eliminated 583 asymmetric tautologies during probing
c [unhide-10] limit 366107 with penalty 2 = 0 + 2
c [unhide-10-10] 192 units, 472 failed, 18672 tauts, 0 hbrs, 17959 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 762 transitive binary clauses
c [transred-6] found 12 units
c [cce-3] limit of 9152685 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 19
c [cce-3-1] eliminated 6 clauses out of 544 (1%) of length 18
c [cce-3-1] eliminated 12 clauses out of 422 (3%) of length 17
c [cce-3-1] eliminated 11 clauses out of 379 (3%) of length 16
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 33 large clauses in 9152685 steps
c [cce-3-1] allowing another 4576342 steps for small clauses
c [cce-3-1] scheduling 875814 clauses = 669417 binary + 206397 ternary
c [cce-3-1] tried to eliminate 1258 small clauses 0%
c [cce-3-1] eliminated 356 binary clauses 0%
c [cce-3-1] eliminated 96 ternary clauses 0%
c [cce-3-1] eliminated 452 small clauses 0%
c [cce-3-1] eliminated 5354 small clauses in 9152685 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 5387 covered clauses in round 1
c [cce-3] eliminated 5387 covered clauses in TOTAL during 1 rounds
c [cce-3] 5387 < 1/100 * 1578409 = 15784 considered unsuccessful
c [bca-6] limit of 10000000 steps and 3151517 added (scaled 2)
c [bca-6] 399529 out of 453032 literals actually usable 88%
c [bca-6] added 318 blocked clauses in 1224815 steps
c [sweep-6] limit 3146044 based on 1573022 irredundant clauses
c [sweep-6-1] 89046 pos 40.0% + 133581 neg 60.0% = 222627 sched 98.3% ret 3888
c [sweep-6-1] 3156084 steps 84 queries 69202.31 avg class size
c [sweep-6-1] 963 decisions 74 SAT calls 33.41 avg env size
c [sweep-6-1] 222327 variables remain 98% (4186 retained 2%)
c [decomp-24] removed 1786 variables
c [sweep-6-1] removed 1786 vars (0 failed, 29 eqs, 37 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 1786 vars in TOTAL (1 rounds, 83 queries)
c [sort-queue-10] sorted 224729 enqueued variables after 17481 conflicts
c [score-dist-10] active 0 (0%), one 0 (0%), zero 224729 (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 3869 variables 1.7% (224729 remain 21%)
c [simplification-10] removed 27449 irredundant clauses 1.7% (1569629 remain 36%)
c [simplification-10] maximum reduction of 2% = max (2%, 2%)
c [simplification-10] forced so keeping old conflict interval 9000
c [simplification-10] conflict limit remains at 20545 (hard 30529)
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  213.0  224728  1569629     17833   26913 134244 140437    3   939  168   0%      3  770    3    1  524%
c i  213.6  224727  1569629     17987   27020 134264 140459    3   930  168   0%      3  759    3    1  527%
c i  213.9  224726  1569629     18064   27078 134276 140464    3   924  168   0%      3  752    3    1  530%
c i  214.0  224725  1569629     18080   27087 134282 140464    3   922  168   0%      3  750    3    1  528%
c i  214.1  224724  1569629     18109   27109 134284 140468    3   920  168   0%      2  748    3    1  547%
c i  215.1  224723  1569629     18318   27225 134332 140507    3   934  168   0%      2  759    3    1  535%
c i  217.4  224722  1569628     18879   27555 134454 140597    3   947  168   0%      3  766    3    1  531%
c i  218.9  224648  1569628     19234   27763 134548 140640    3   961  168   0%      3  776    3    1  492%
c i  219.2  224647  1569628     19293   27792 134565 140650    3   964  168   0%      3  778    3    1  487%
c i  221.4  224646  1569628     19797   28098 134688 140716    3   952  168   0%      3  760    3    1  447%
c i  223.7  224645  1569628     20320   28428 134797 140788    3   947  168   0%      3  750    3    1  481%
c i  223.9  224644  1569628     20364   28452 134810 140793    3   944  168   0%      3  746    3    1  467%
c 
c [simplification-11] limit 20545 conflicts (hard 30529) hit after 20545 conflicts
c [quatres-7] found 239225 quaternary clauses 45% in total
c [quatres-7-1] removed 75 duplicate quaternary clauses
c [quatres-7-1] added 12 double-self-subsuming ternary resolvents
c [quatres-7-2] added 429 single-self-subsuming ternary resolvents
c [quatres-7-2] added 1259 quaternary resolvents
c [ternres-7] limit 9348664 with penalty 0 = 0 + 0
c [ternres-7] 596 schedulable variables 0%
c [ternres-7] 41254 ternary resolvents (878 bin, 40376 trn)
c [ternres-7] 28 variables remain 0% (224616 retained 100%)
c [decomp-25] removed 421 variables
c [simpleprobe-5] 191423 schedulable variables 85%
c [simpleprobe-5] limit 37394659 penalty 0 = 0 + 0
c [decomp-26] removed 2745 variables
c [simpleprobe-5] 117019 variables remain 53% (104544 retained 47%)
c [simpleprobe-5] removed 2745 variables, found 69304 hbrs, 615 units
c [unhide-11] limit 467433 with penalty 2 = 0 + 2
c [unhide-11-11] 61 units, 136 failed, 13196 tauts, 0 hbrs, 8362 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1016 transitive binary clauses
c [transred-7] found 10 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 221158 variables 100%
c [block-4] limit of 23371662 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 8732 blocked clauses
c [block-4] 8732 < 1/100 * 1538330 = 15383 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 220813 variables 100%
c [elim-9] limit of 93486649 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 13764 not tried 6% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 8493 = 4% variables out of 220813 scheduled
c [bca-7] limit of 10000000 steps and 3001310 added (scaled 2)
c [bca-7] 371830 out of 424642 literals actually usable 88%
c [bca-7] added 669 blocked clauses in 1154581 steps
c [sweep-7] limit 2995678 based on 1497839 irredundant clauses
c [sweep-7-1] 82245 pos 39.4% + 126275 neg 60.6% = 208520 sched 98.2% ret 3800
c [sweep-7-1] 3021978 steps 68 queries 54784.93 avg class size
c [sweep-7-1] 1122 decisions 67 SAT calls 36.51 avg env size
c [sweep-7-1] 208031 variables remain 98% (4284 retained 2%)
c [decomp-27] removed 385 variables
c [sweep-7-1] removed 385 vars (0 failed, 13 eqs, 12 impls)
c [sweep-7] removed 385 vars in TOTAL (1 rounds, 67 queries)
c [sort-queue-11] sorted 211935 enqueued variables after 20545 conflicts
c [score-dist-11] active 0 (0%), one 0 (0%), zero 211935 (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 12709 variables 5.7% (211935 remain 19%)
c [simplification-11] removed 72760 irredundant clauses 4.6% (1496868 remain 34%)
c [simplification-11] maximum reduction of 6% = max (6%, 5%)
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 32545 (soft 22545 + delta 10000)
c [simplification-11] new conflict limit 22545 (hard 32545)
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  241.5  211934  1496868     20660   27255 138253 181982    3   952  166   0%      3  751    3    1  476%
c i  246.2  211933  1496867     21820   28016 138478 182139    3   971  166   0%      8  756    3    1  449%
c i  246.6  211932  1496867     21903   28060 138505 182150    3   964  166   0%      7  748    3    1  423%
c i  247.8  211931  1496867     22181   28241 138564 182181    3   996  166   0%      6  777    3    1  461%
c i  248.3  211930  1496867     22285   28323 138579 182186    3   990  166   0%      5  770    3    1  449%
c i  248.3  211929  1496867     22292   28326 138580 182187    3   989  166   0%      5  769    3    1  447%
c i  248.3  211928  1496867     22302   28332 138582 182188    3   991  166   0%      5  771    3    1  446%
c i  248.4  211927  1496867     22308   28335 138584 182188    3   991  166   0%      5  771    3    1  443%
c i  248.4  211926  1496867     22310   28335 138584 182189    3   990  166   0%      5  770    3    1  440%
c i  248.4  211925  1496867     22323   28340 138588 182192    3   990  166   0%      5  770    3    1  432%
c i  248.5  211924  1496867     22333   28346 138590 182192    3   991  166   0%      5  770    3    1  430%
c i  248.7  211923  1496867     22404   28395 138605 182198    3  1000  166   0%      5  778    3    1  419%
c i  248.9  211922  1496867     22434   28414 138611 182202    3  1002  166   0%      5  780    3    1  412%
c i  249.3  211921  1496867     22550   28489 138638 182211    3  1016  166   0%      4  793    3    1  410%
c i  249.3  211920  1496867     22554   28490 138640 182211    3  1015  166   0%      4  792    3    1  406%
c 
c [simplification-12] limit 22556 conflicts (hard 32545) hit after 22556 conflicts
c [quatres-8] found 235994 quaternary clauses 45% in total
c [quatres-8-1] removed 266 duplicate quaternary clauses
c [quatres-8-1] added 13 double-self-subsuming ternary resolvents
c [quatres-8-2] added 939 single-self-subsuming ternary resolvents
c [quatres-8-2] added 2425 quaternary resolvents
c [ternres-8] limit 10597419 with penalty 0 = 0 + 0
c [ternres-8] 28 schedulable variables 0%
c [ternres-8] 16986 ternary resolvents (303 bin, 16683 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-28] removed 146 variables
c [treelook-5] limit 1059741 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 87496 literals 21%
c [treelook-5] scheduling used 1059743 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 1059741 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1305606 steps
c [treelook-5] 87387 literals remain 21%
c [treelook-5] 19480 variables remain to probed next time 9%
c [decomp-29] removed 3 variables
c [treelook-5] removed 10 variables, found 2580 hbrs
c [unhide-12] limit 529870 with penalty 2 = 0 + 2
c [unhide-12-12] 121 units, 269 failed, 16604 tauts, 0 hbrs, 16409 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 850 transitive binary clauses
c [transred-8] found 16 units
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 211389 variables 100%
c [elim-10] limit of 211948388 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 1992 not tried 1% in round 1
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 2599 = 1% variables out of 211389 scheduled
c [bca-8] limit of 10000000 steps and 2949290 added (scaled 2)
c [bca-8] 361766 out of 417582 literals actually usable 87%
c [bca-8] added 625 blocked clauses in 1120710 steps
c [sweep-8] limit 3179225 penalty 0 = 0 + 0
c [sweep-8-1] 80178 pos 39.2% + 124426 neg 60.8% = 204604 sched 98.0% ret 4186
c [sweep-8-1] 3201085 steps 80 queries 57601.14 avg class size
c [sweep-8-1] 1113 decisions 72 SAT calls 37.36 avg env size
c [sweep-8-1] 204130 variables remain 98% (4660 retained 2%)
c [decomp-30] removed 644 variables
c [sweep-8-1] removed 644 vars (0 failed, 10 eqs, 17 impls)
c [sweep-8] removed 644 vars in TOTAL (1 rounds, 79 queries)
c [sort-queue-12] sorted 208146 enqueued variables after 22556 conflicts
c [score-dist-12] active 0 (0%), one 0 (0%), zero 208146 (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 3774 variables 1.8% (208146 remain 19%)
c [simplification-12] removed 26758 irredundant clauses 1.8% (1470109 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 15666
c [simplification-12] penalized conflict interval 15666 = 1 * 15666
c [simplification-12] hard conflict limit 48222 (soft 38222 + delta 10000)
c [simplification-12] new conflict limit 38222 (hard 48222)
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  264.9  208145  1470109     22979   29690 137544 163996    3  1013  165   0%      4  785    3    1  399%
c i  265.8  208144  1470109     23188   29833 137586 164017    3   998  165   0%      3  767    3    1  401%
c i  266.1  208143  1470109     23290   29897 137605 164033    3  1002  165   0%      3  770    3    1  394%
c i  267.0  208142  1470109     23498   30037 137644 164059    3  1007  165   0%      2  773    3    1  389%
c i  267.7  208141  1470109     23658   30138 137684 164074    3  1014  165   0%      2  778    3    1  393%
c i  268.0  207982  1470109     23731   30175 137698 164091    3  1025  165   0%      2  788    3    1  381%
c i  269.2  207981  1470109     24015   30368 137753 164120    3  1020  165   0%      2  780    3    1  406%
c i  270.1  207980  1470109     24231   30500 137799 164151    3  1038  165   0%      2  795    3    1  425%
c i  270.2  207979  1470109     24262   30525 137801 164154    3  1036  165   0%      2  793    3    1  423%
c i  270.4  207978  1470109     24318   30560 137815 164158    3  1037  165   0%      2  793    3    1  411%
c i  270.7  207977  1470109     24379   30600 137825 164166    3  1039  165   0%      1  794    3    1  425%
c i  270.8  207976  1470109     24407   30616 137831 164170    3  1040  165   0%      1  796    3    1  413%
c i  271.1  207975  1470109     24484   30655 137852 164185    3  1046  165   0%      1  800    3    1  386%
c i  271.2  207974  1470109     24490   30659 137853 164185    3  1048  165   0%      1  802    3    1  383%
c i  271.3  207973  1470109     24520   30678 137858 164190    3  1051  165   0%      1  805    3    1  389%
c i  271.3  207972  1470109     24521   30678 137858 164190    3  1051  165   0%      1  805    3    1  388%
c i  271.3  207971  1470109     24523   30679 137858 164190    3  1050  165   0%      1  804    3    1  386%
c i  272.3  207970  1470109     24783   30845 137916 164221    3  1033  165   0%      1  783    3    1  381%
c i  272.5  207969  1470109     24812   30861 137921 164227    3  1039  165   0%      1  789    3    1  376%
c i  273.9  207968  1470109     25156   31095 137990 164261    3  1036  165   0%      1  782    3    1  371%
c i  274.1  207967  1470109     25181   31112 137994 164264    3  1035  165   0%      1  781    3    1  365%
c i  275.7  207966  1470109     25577   31354 138080 164315    3  1035  165   0%      2  776    3    1  360%
c i  275.9  207965  1470109     25647   31397 138094 164327    3  1035  165   0%      2  775    3    1  349%
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  275.9  207922  1470109     25648   31397 138094 164327    3  1035  165   0%      2  775    3    1  347%
c i  276.1  207838  1470109     25679   31419 138100 164329    3  1038  165   0%      2  778    3    1  361%
c i  276.2  207837  1470109     25724   31441 138110 164341    3  1048  165   0%      1  787    3    1  349%
c i  276.2  207836  1470109     25725   31441 138110 164341    3  1048  165   0%      1  787    3    1  348%
c i  276.4  207835  1470109     25776   31463 138127 164352    3  1047  165   0%      1  786    3    1  329%
c i  278.6  207834  1470109     26307   31809 138226 164424    3  1023  165   0%      2  756    3    1  359%
c i  278.6  207833  1470109     26309   31810 138226 164424    3  1023  165   0%      2  756    3    1  358%
c i  278.7  207832  1470109     26333   31825 138233 164425    3  1023  165   0%      2  756    3    1  359%
c i  278.7  207831  1470109     26336   31827 138233 164425    3  1023  165   0%      2  755    3    1  358%
c i  278.8  207830  1470109     26347   31831 138236 164428    3  1023  165   0%      2  755    3    1  353%
c i  281.3  207829  1470109     26902   32190 138341 164507    3  1050  165   0%      3  776    3    1  355%
c i  285.4  207818  1470109     27912   32867 138525 164635    3  1035  165   0%      6  749    3    1  359%
c i  285.5  207817  1470109     27929   32877 138528 164638    3  1034  165   0%      6  748    3    1  356%
c i  285.5  207811  1470109     27943   32886 138532 164638    3  1033  165   0%      6  747    3    1  349%
c i  285.8  207809  1470109     28026   32943 138546 164648    3  1035  165   0%      6  748    3    1  342%
c i  287.7  207808  1470109     28483   33254 138630 164700    3  1044  165   0%      5  752    3    1  337%
c i  288.0  207805  1470109     28565   33298 138649 164717    3  1056  165   0%      4  763    3    1  341%
c i  289.1  207804  1470109     28799   33474 138681 164738    3  1037  165   0%      4  741    3    1  345%
c i  294.7  207803  1470109     30088   34356 138920 164878    3  1033  165   0%      9  723    3    1  342%
c i  295.1  207802  1470109     30196   34430 138936 164892    3  1047  165   0%      8  736    3    1  336%
c i  297.1  207801  1470109     30659   34756 139003 164946    3  1048  165   0%      6  732    3    1  334%
c i  297.1  207800  1470109     30665   34756 139003 164951    3  1047  165   0%      6  730    3    1  328%
c i  299.1  207799  1470109     31119   35098 139062 164994    3  1037  165   0%      5  716    3    1  334%
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  300.6  207798  1470109     31475   35365 139117 165023    3  1028  165   0%      4  703    4    1  349%
c i  302.5  207797  1470109     31861   35626 139188 165073    3  1037  165   0%      3  708    3    1  306%
c i  303.5  207795  1470109     32119   35807 139231 165102    3  1049  165   0%      3  717    4    1  337%
c i  303.5  207794  1470109     32120   35807 139231 165102    3  1049  165   0%      3  717    4    1  336%
c i  303.5  207793  1470109     32125   35809 139233 165102    3  1048  165   0%      3  716    4    1  333%
c i  305.6  207792  1470109     32554   36107 139315 165146    3  1050  165   0%      3  714    4    1  334%
c i  306.2  207790  1470109     32646   36174 139332 165153    3  1045  165   0%      2  707    4    1  335%
c i  307.9  207789  1470109     33012   36420 139398 165198    3  1050  165   0%      2  708    3    1  295%
c i  308.3  207788  1470109     33102   36488 139405 165211    3  1053  165   0%      2  711    3    1  301%
c i  308.3  207787  1470109     33114   36495 139408 165212    3  1052  165   0%      2  710    3    1  297%
c i  308.3  207786  1470109     33121   36500 139409 165212    3  1052  165   0%      2  709    3    1  295%
c i  308.4  207785  1470109     33142   36512 139415 165214    3  1051  165   0%      2  708    3    1  295%
c i  308.5  207784  1470109     33169   36532 139419 165216    3  1057  165   0%      2  713    3    1  299%
c i  310.0  207783  1470109     33493   36761 139479 165248    3  1052  165   0%      2  705    4    1  318%
c i  310.9  207782  1470109     33706   36893 139525 165276    3  1063  165   0%      1  714    3    1  301%
c i  312.6  207781  1470109     34105   37186 139586 165318    3  1052  165   0%      2  699    3    1  301%
c i  312.6  207780  1470109     34107   37186 139586 165319    3  1052  165   0%      2  698    3    1  299%
c i  313.8  207779  1470109     34409   37390 139633 165364    3  1036  165   0%      2  679    3    1  278%
c i  316.8  207778  1470109     35149   37910 139753 165449    3  1039  165   0%      3  675    3    1  298%
c i  319.6  207777  1470109     35790   38366 139862 165514    3  1034  165   0%      4  663    3    1  294%
c i  319.7  207776  1470109     35810   38375 139869 165517    3  1036  165   0%      4  666    3    1  291%
c i  320.0  207775  1470109     35873   38423 139876 165522    3  1043  165   0%      3  672    3    1  286%
c i  320.0  207774  1470109     35888   38429 139880 165526    3  1044  165   0%      3  672    3    1  280%
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  320.7  207773  1470109     36054   38547 139911 165537    3  1038  165   0%      3  665    4    1  297%
c i  320.9  207772  1470109     36095   38576 139914 165543    3  1035  165   0%      3  662    4    1  296%
c i  321.3  207771  1470109     36189   38639 139928 165558    3  1035  165   0%      2  660    3    1  287%
c i  321.5  207770  1470109     36232   38663 139938 165566    3  1038  165   0%      2  663    3    1  280%
c i  321.5  207769  1470109     36235   38664 139938 165567    3  1037  165   0%      2  662    3    1  277%
c i  322.0  207768  1470109     36357   38748 139957 165585    3  1055  165   0%      2  679    3    1  278%
c i  322.0  207767  1470109     36361   38748 139958 165586    3  1054  165   0%      2  678    3    1  275%
c i  322.0  207766  1470109     36362   38748 139958 165586    3  1054  165   0%      2  678    3    1  274%
c i  322.6  207765  1470109     36500   38844 139988 165595    3  1036  165   0%      2  659    3    1  269%
c i  322.8  207764  1470109     36533   38864 139991 165602    3  1034  165   0%      2  656    3    1  266%
c i  323.3  207763  1470109     36650   38937 140015 165620    3  1039  165   0%      1  660    3    1  272%
c i  323.6  207762  1470109     36727   38989 140029 165630    3  1049  165   0%      1  669    3    1  266%
c i  324.3  207761  1470109     36889   39109 140050 165645    3  1034  165   0%      1  652    3    1  280%
c i  325.4  207760  1470109     37102   39253 140088 165670    3  1045  165   0%      1  661    3    1  276%
c i  326.6  207759  1470109     37382   39449 140133 165704    3  1036  165   0%      1  650    3    1  271%
c i  327.4  207758  1470109     37569   39590 140164 165716    3  1054  165   0%      1  665    4    1  289%
c 
c [simplification-13] limit 38300 conflicts (hard 48222) hit after 38301 conflicts
c [quatres-9] found 236037 quaternary clauses 46% in total
c [quatres-9-1] removed 61 duplicate quaternary clauses
c [quatres-9-1] added 12 double-self-subsuming ternary resolvents
c [quatres-9-2] added 265 single-self-subsuming ternary resolvents
c [quatres-9-2] added 1323 quaternary resolvents
c [ternres-9] limit 21103441 with penalty 0 = 0 + 0
c [ternres-9] all 207758 free variables schedulable
c [ternres-9] 22649 ternary resolvents (410 bin, 22239 trn)
c [ternres-9] 45858 variables remain 22% (161900 retained 78%)
c [decomp-31] removed 802 variables
c [basicprobe-5] limit 105517208 penalty 0 = 0 + 0
c [basicprobe-5-0] 100845 probes remain 49% after last round
c [basicprobe-5-0] 1467 units = 1310 failed (89%) + 157 lifted (11%)
c [basicprobe-5-0] removed 2786 variables, found 75968 hbrs
c [bate-3] eliminated 971 asymmetric tautologies during probing
c [unhide-13] limit 1055172 with penalty 2 = 0 + 2
c [unhide-13-13] 166 units, 239 failed, 15945 tauts, 0 hbrs, 8752 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 868 transitive binary clauses
c [transred-9] found 5 units
c [elim-11] 1967 variables 1% will be scheduled this time
c [elim-11] scheduled 1967 variables 1%
c [elim-11] limit of 422068834 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] no variable eliminated in round 1 in 274362014 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 11 = 1% variables out of 1967 scheduled
c [elim-11] 11 < 1/100 * 1967 = 19 considered unsuccessful
c [bca-9] limit of 10000000 steps and 2838099 added (scaled 2)
c [bca-9] 336063 out of 408296 literals actually usable 82%
c [bca-9] added 255 blocked clauses in 1033161 steps
c [sweep-9] limit 6331032 penalty 0 = 0 + 0
c [sweep-9-1] 77237 pos 38.7% + 122474 neg 61.3% = 199711 sched 97.8% ret 4436
c [sweep-9-1] 6332546 steps 120 queries 36682.45 avg class size
c [sweep-9-1] 1432 decisions 105 SAT calls 50.39 avg env size
c [sweep-9-1] 198913 variables remain 97% (5232 retained 3%)
c [decomp-32] removed 2585 variables
c [sweep-9-1] removed 2585 vars (0 failed, 25 eqs, 32 impls)
c [sweep-9] removed 2585 vars in TOTAL (1 rounds, 119 queries)
c [sort-queue-13] sorted 201562 enqueued variables after 38301 conflicts
c [score-dist-13] active 0 (0%), one 0 (0%), zero 201562 (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 6196 variables 3.0% (201562 remain 18%)
c [simplification-13] removed 58726 irredundant clauses 4.0% (1411383 remain 32%)
c [simplification-13] maximum reduction of 4% = max (3%, 4%)
c [simplification-13] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-13] new conflict interval 19666
c [simplification-13] penalized conflict interval 19666 = 1 * 19666
c [simplification-13] hard conflict limit 67967 (soft 57967 + delta 10000)
c [simplification-13] new conflict limit 57967 (hard 67967)
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  347.0  201561  1411383     38447   40125 140359 208415    3  1029  164   0%      4  632    4    1  296%
c i  348.0  201560  1411383     38695   40283 140404 208457    3  1036  164   0%      3  636    3    1  257%
c i  349.3  201559  1411383     38996   40508 140445 208484    3  1031  164   0%      3  629    4    1  289%
c i  350.6  201558  1411383     39351   40767 140502 208512    3  1040  164   0%      2  634    4    1  286%
c i  351.9  201557  1411383     39656   40987 140551 208544    3  1055  164   0%      2  647    4    1  280%
c i  357.0  201555  1411383     40749   41754 140741 208655    4  1026  164   0%      6  607    4    1  280%
c i  364.2  201552  1411383     42419   43002 140996 208796    4  1062  164   0%     13  628    4    1  260%
c i  364.3  201550  1411383     42433   43012 140996 208798    4  1062  164   0%     13  627    4    1  261%
c i  367.9  201549  1411383     43224   43610 141106 208869    4  1068  164   0%      9  625    4    1  245%
c i  373.3  201548  1411382     44417   44465 141315 208975    4  1057  164   0%      9  603    3    1  229%
c i  375.3  201547  1411382     44875   44808 141383 209010    4  1048  164   0%      6  590    3    1  229%
c i  376.3  201546  1411382     45119   44981 141422 209034    4  1046  164   0%      5  586    3    1  229%
c i  377.4  201545  1411382     45337   45129 141463 209055    4  1058  164   0%      4  597    4    2  238%
c i  381.3  201544  1411382     46196   45768 141588 209135    4  1070  164   0%      5  601    4    2  258%
c i  381.3  201543  1411382     46200   45771 141588 209135    4  1071  164   0%      5  602    4    2  256%
c i  383.3  201542  1411382     46643   46114 141649 209166    4  1056  164   0%      4  583    4    2  234%
c i  383.3  201541  1411382     46646   46115 141649 209167    4  1057  164   0%      4  583    4    2  232%
c i  383.4  201540  1411382     46671   46127 141653 209175    4  1055  164   0%      4  581    3    2  222%
c i  386.8  201539  1411382     47372   46665 141746 209235    4  1043  164   0%      4  564    4    2  229%
c i  387.0  201538  1411382     47402   46685 141750 209239    4  1044  164   0%      4  564    4    2  228%
c i  387.9  201537  1411382     47617   46838 141792 209257    4  1073  164   0%      3  592    4    2  232%
c i  388.3  201536  1411382     47697   46903 141798 209263    4  1060  164   0%      3  578    4    2  234%
c i  390.6  201535  1411381     48187   47290 141862 209294    4  1047  164   0%      2  561    4    2  251%
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  394.6  201531  1411380     49041   47927 141995 209366    4  1034  164   0%      4  540    4    2  245%
c i  394.8  201530  1411380     49093   47968 142002 209369    4  1029  164   0%      4  535    4    2  257%
c i  396.0  201529  1411380     49327   48135 142050 209386    4  1050  164   0%      3  554    4    2  248%
c i  399.9  201528  1411380     50192   48800 142177 209447    4  1066  164   0%      4  563    4    2  220%
c i  401.5  200463  1411380     50546   49051 142239 209481    4  1052  164   0%      3  546    3    2  202%
c i  401.9  200462  1411380     50633   49111 142257 209488    4  1065  164   0%      3  558    3    2  190%
c i  403.9  200461  1411380     51064   49418 142333 209526    4  1063  164   0%      2  552    3    2  204%
c i  405.8  200460  1411380     51497   49720 142409 209577    4  1055  164   0%      2  541    3    2  196%
c i  407.2  200459  1411380     51846   49979 142454 209613    4  1033  164   0%      2  516    4    2  216%
c i  407.3  200458  1411380     51854   49981 142457 209615    4  1033  164   0%      2  516    4    2  213%
c i  407.6  200457  1411380     51955   50044 142478 209629    4  1042  164   0%      1  524    4    2  206%
c i  408.0  200456  1411380     52071   50125 142493 209644    4  1043  164   0%      1  524    3    2  199%
c i  408.2  200455  1411380     52121   50157 142503 209649    4  1036  164   0%      1  517    3    2  197%
c i  408.5  200441  1411380     52217   50224 142520 209659    4  1029  164   0%      1  509    3    2  197%
c i  409.2  200440  1411380     52410   50344 142568 209682    4  1033  164   0%      0  512    3    2  183%
c i  410.7  200439  1411380     52778   50586 142640 209725    4  1017  164   0%      1  493    3    2  178%
c i  410.7  200438  1411380     52780   50586 142640 209725    4  1017  164   0%      1  493    3    2  177%
c i  410.8  200437  1411380     52789   50589 142643 209727    4  1016  164   0%      0  492    3    2  177%
c i  412.2  200436  1411380     53170   50874 142702 209757    4  1002  164   0%      1  475    3    2  189%
c i  412.3  200435  1411380     53210   50900 142707 209764    4  1000  164   0%      1  473    3    2  187%
c i  414.4  200434  1411380     53698   51264 142784 209802    4  1004  164   0%      1  473    4    2  214%
c i  414.5  200433  1411380     53704   51267 142786 209802    4  1004  164   0%      1  473    4    2  214%
c i  414.8  200432  1411380     53771   51308 142804 209809    4  1009  164   0%      1  478    4    2  205%
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  414.8  200431  1411380     53801   51325 142811 209813    4  1012  164   0%      1  481    4    2  202%
c i  416.5  200430  1411380     54197   51629 142865 209844    4  1007  164   0%      1  472    4    2  224%
c i  416.8  200429  1411380     54267   51674 142880 209853    4  1018  164   0%      1  483    4    2  211%
c i  417.4  200428  1411380     54449   51815 142903 209864    4  1006  164   0%      0  469    4    2  224%
c i  419.9  200427  1411380     55029   52230 142997 209919    4   993  164   0%      1  453    4    2  211%
c i  420.0  200426  1411380     55051   52240 143004 209922    4   993  164   0%      1  453    4    2  205%
c i  421.2  200425  1411379     55386   52479 143056 209957    4  1002  164   0%      1  459    4    2  207%
c i  421.2  200424  1411379     55387   52479 143056 209957    4  1002  164   0%      1  459    4    2  207%
c i  422.1  200422  1411377     55615   52636 143095 209984    4  1005  164   0%      1  460    4    2  193%
c i  422.1  200295  1411377     55616   52636 143095 209984    4  1005  164   0%      1  460    4    2  193%
c i  422.3  198635  1411377     55667   52668 143108 209988    4  1007  164   0%      1  462    3    2  182%
c i  422.5  198634  1411377     55729   52716 143117 209992    4  1003  164   0%      0  458    4    2  192%
c i  424.8  198633  1411377     56214   53076 143188 210039    4   995  164   0%      1  447    4    2  219%
c i  425.0  198475  1411377     56267   53121 143191 210042    4   988  164   0%      1  440    4    2  219%
c i  425.1  198474  1411377     56290   53142 143191 210043    4   987  164   0%      1  438    4    2  219%
c i  425.2  198470  1411377     56303   53152 143191 210045    4   986  164   0%      1  437    4    2  218%
c i  430.2  198469  1411377     57646   54114 143431 210164    4   998  164   0%      8  440    4    2  192%
c i  430.7  198468  1411377     57768   54199 143454 210176    4   995  164   0%      7  436    3    2  181%
c i  430.7  198467  1411377     57774   54199 143455 210180    4   993  164   0%      7  434    3    2  178%
c 
c [simplification-14] limit 58001 conflicts (hard 67967) hit after 58001 conflicts
c [quatres-10] found 227823 quaternary clauses 46% in total
c [quatres-10-1] removed 150 duplicate quaternary clauses
c [quatres-10-1] added 9 double-self-subsuming ternary resolvents
c [quatres-10-2] added 580 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1112 quaternary resolvents
c [ternres-10] limit 34741347 with penalty 0 = 0 + 0
c [ternres-10] 43132 schedulable variables 21%
c [ternres-10] 43892 ternary resolvents (868 bin, 43024 trn)
c [ternres-10] 655 variables remain 0% (197812 retained 100%)
c [gauss-4] limit 868533 penalty 3 = 3 + 0
c [gauss-4] extracted 2081 xors of average arity 2.9
c [gauss-4] connected 6138 occurrences of 2639 variables (average 2.3)
c [gauss-4] limit 868533 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-33] removed 1040 variables
c [simpleprobe-6] 103207 schedulable variables 52%
c [simpleprobe-6] limit 138965389 penalty 0 = 0 + 0
c [decomp-34] removed 7187 variables
c [simpleprobe-6] 52569 variables remain 28% (137671 retained 72%)
c [simpleprobe-6] removed 7187 variables, found 195001 hbrs, 1467 units
c [unhide-14] limit 1737067 with penalty 2 = 0 + 2
c [unhide-14-14] 96 units, 201 failed, 52354 tauts, 0 hbrs, 32137 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 1156 transitive binary clauses
c [transred-10] found 5 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 217133420 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 25
c [cce-4-1] eliminated 4 clauses out of 535 (1%) of length 18
c [cce-4-1] eliminated 33 clauses out of 413 (8%) of length 17
c [cce-4-1] eliminated 17 clauses out of 351 (5%) of length 16
c [cce-4-1] eliminated 15 clauses out of 1017 (1%) of length 15
c [cce-4-1] eliminated 63 clauses out of 1039 (6%) of length 14
c [cce-4-1] eliminated 558 clauses out of 2432 (23%) of length 13
c [cce-4-1] eliminated 795 clauses out of 3942 (20%) of length 12
c [cce-4-1] eliminated 724 clauses out of 5181 (14%) of length 11
c [cce-4-1] eliminated 4506 clauses out of 12235 (37%) of length 10
c [cce-4-1] eliminated 5856 clauses out of 15714 (37%) of length 9
c [cce-4-1] eliminated 1835 clauses out of 22715 (8%) of length 8
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 14407 large clauses in 217133424 steps
c [cce-4-1] allowing another 108566712 steps for small clauses
c [cce-4-1] scheduling 717535 clauses = 550161 binary + 167374 ternary
c [cce-4-1] tried to eliminate 36568 small clauses 5%
c [cce-4-1] eliminated 5889 binary clauses 1%
c [cce-4-1] eliminated 1669 ternary clauses 1%
c [cce-4-1] eliminated 7558 small clauses 1%
c [cce-4-1] eliminated 10244 small clauses in 217133424 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 24651 covered clauses in round 1
c [cce-4] eliminated 24651 covered clauses in TOTAL during 1 rounds
c [bca-10] limit of 10000000 steps and 2628310 added (scaled 2)
c [bca-10] 297117 out of 379906 literals actually usable 78%
c [bca-10] added 1442 blocked clauses in 918021 steps
c [sweep-10] limit 10422404 penalty 0 = 0 + 0
c [sweep-10-1] 70115 pos 37.9% + 114834 neg 62.1% = 184949 sched 97.4% ret 5003
c [sweep-10-1] 10460150 steps 216 queries 29908.63 avg class size
c [sweep-10-1] 3289 decisions 197 SAT calls 45.75 avg env size
c [sweep-10-1] 182562 variables remain 96% (7325 retained 4%)
c [decomp-35] removed 699 variables
c [sweep-10-1] removed 699 vars (0 failed, 43 eqs, 60 impls)
c [sweep-10] removed 699 vars in TOTAL (1 rounds, 215 queries)
c [sort-queue-14] sorted 189253 enqueued variables after 58001 conflicts
c [score-dist-14] active 0 (0%), one 0 (0%), zero 189253 (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 9214 variables 4.6% (189253 remain 17%)
c [simplification-14] removed 102639 irredundant clauses 7.3% (1308738 remain 30%)
c [simplification-14] maximum reduction of 7% = max (5%, 7%)
c [simplification-14] large reduction 7% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 70001 (soft 60001 + delta 10000)
c [simplification-14] new conflict limit 60001 (hard 70001)
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  451.8  189252  1308737     58268   53234 155066 308937    4   989  163   0%      5  427    4    2  206%
c i  453.2  189251  1308737     58570   53470 155098 308959    4   992  163   0%      4  428    4    2  235%
c i  453.8  189249  1308737     58707   53570 155118 308973    4   990  163   0%      3  425    5    2  244%
c i  454.5  189248  1308737     58866   53678 155154 308985    4  1013  163   0%      2  447    4    2  222%
c i  456.8  189239  1308737     59421   54094 155237 309031    4  1000  163   0%      2  430    4    2  213%
c 
c [simplification-15] limit 60001 conflicts (hard 70001) hit after 60002 conflicts
c [quatres-11] found 221837 quaternary clauses 47% in total
c [quatres-11-1] removed 1090 duplicate quaternary clauses
c [quatres-11-1] added 49 double-self-subsuming ternary resolvents
c [quatres-11-2] added 908 single-self-subsuming ternary resolvents
c [quatres-11-2] added 1300 quaternary resolvents
c [ternres-11] limit 36258606 with penalty 0 = 0 + 0
c [ternres-11] 613 schedulable variables 0%
c [ternres-11] 44068 ternary resolvents (839 bin, 43229 trn)
c [ternres-11] 73 variables remain 0% (189113 retained 100%)
c [card-5] limit 1133081 penalty 4 = 4 + 0
c [card-5] found 667 at-most-one constraints of average size 3.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1133081 for elimination
c [card-5] 667 out of 667 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-36] removed 357 variables
c [treelook-6] limit 3625860 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 145586 literals 39%
c [treelook-6] scheduling used 3208775 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3625860 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 3713508 steps
c [treelook-6] 145555 literals remain 39%
c [treelook-6] 17050 variables remain to probed next time 9%
c [decomp-37] removed 2 variables
c [treelook-6] removed 6 variables, found 4283 hbrs
c [unhide-15] limit 1812930 with penalty 2 = 0 + 2
c [unhide-15-15] 62 units, 92 failed, 12670 tauts, 0 hbrs, 9415 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1060 transitive binary clauses
c [transred-11] found 14 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 188705 variables 100%
c [block-5] limit of 45323257 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 18401 blocked clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 187955 variables 100%
c [elim-12] limit of 362586060 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 60 not tried 0% in round 1
c [gc-111] reconnected 309057 binary clauses (produced 0 empty 4 units)
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 12219 = 7% variables out of 187955 scheduled
c [bca-11] limit of 10000000 steps and 2473245 added (scaled 2)
c [bca-11] 275944 out of 351474 literals actually usable 79%
c [bca-11] added 1704 blocked clauses in 868641 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 108775810 penalty 0 = 0 + 0
c [sweep-11-1] 62716 pos 37.1% + 106333 neg 62.9% = 169049 sched 96.2% ret 6687
c [sweep-11-1] 108779178 steps 2017 queries 6825.36 avg class size
c [sweep-11-1] 26679 decisions 1888 SAT calls 35.28 avg env size
c [sweep-11-1] 135338 variables remain 77% (40100 retained 23%)
c [decomp-38] removed 1889 variables
c [sweep-11-1] removed 1889 vars (0 failed, 403 eqs, 478 impls)
c [sweep-11] removed 1889 vars in TOTAL (1 rounds, 2016 queries)
c [sort-queue-15] sorted 173847 enqueued variables after 60002 conflicts
c [score-dist-15] active 0 (0%), one 0 (0%), zero 173847 (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 15339 variables 8.1% (173847 remain 16%)
c [simplification-15] removed 85172 irredundant clauses 6.5% (1223565 remain 28%)
c [simplification-15] maximum reduction of 8% = max (8%, 7%)
c [simplification-15] large reduction 8% >= 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 72002 (soft 62002 + delta 10000)
c [simplification-15] new conflict limit 62002 (hard 72002)
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  489.4  173846  1223565     60161   48337 157216 281321    4  1000  158   0%      3  425    4    2  215%
c i  492.0  173845  1223565     60781   48766 157331 281382    4  1017  158   0%      3  438    4    2  183%
c 
c [simplification-16] limit 62002 conflicts (hard 72002) hit after 62004 conflicts
c [quatres-12] found 213378 quaternary clauses 47% in total
c [quatres-12-1] removed 84 duplicate quaternary clauses
c [quatres-12-1] added 13 double-self-subsuming ternary resolvents
c [quatres-12-2] added 651 single-self-subsuming ternary resolvents
c [quatres-12-2] added 2794 quaternary resolvents
c [ternres-12] limit 37552009 with penalty 0 = 0 + 0
c [ternres-12] 69 schedulable variables 0%
c [ternres-12] 35579 ternary resolvents (515 bin, 35064 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-39] removed 151 variables
c [basicprobe-6] limit 187760049 penalty 0 = 0 + 0
c [basicprobe-6-0] 50991 probes remain 30% after last round
c [basicprobe-6-0] 1638 units = 1523 failed (93%) + 115 lifted (7%)
c [basicprobe-6-0] removed 2113 variables, found 61294 hbrs
c [bate-4] eliminated 1300 asymmetric tautologies during probing
c [unhide-16] limit 1877600 with penalty 2 = 0 + 2
c [unhide-16-16] 160 units, 429 failed, 45391 tauts, 0 hbrs, 26746 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 936 transitive binary clauses
c [transred-12] found 7 units
c [cce-5] limit of 46940012 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 23
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 22
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 21
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 20
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 19
c [cce-5-1] eliminated 2 clauses out of 518 (0%) of length 18
c [cce-5-1] eliminated 8 clauses out of 361 (2%) of length 17
c [cce-5-1] eliminated 9 clauses out of 312 (3%) of length 16
c [cce-5-1] eliminated 16 clauses out of 1081 (1%) of length 15
c [cce-5-1] eliminated 10 clauses out of 1035 (1%) of length 14
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 56 large clauses in 46940077 steps
c [cce-5-1] allowing another 23470038 steps for small clauses
c [cce-5-1] scheduling 639964 clauses = 483917 binary + 156047 ternary
c [cce-5-1] tried to eliminate 7767 small clauses 1%
c [cce-5-1] eliminated 1739 binary clauses 0%
c [cce-5-1] eliminated 493 ternary clauses 0%
c [cce-5-1] eliminated 2232 small clauses 0%
c [cce-5-1] eliminated 5708 small clauses in 46940015 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 5764 covered clauses in round 1
c [cce-5] eliminated 5764 covered clauses in TOTAL during 1 rounds
c [cce-5] 5764 < 1/100 * 1192780 = 11927 considered unsuccessful
c [elim-13] 57 variables 0% will be scheduled this time
c [elim-13] scheduled 57 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 17585800 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 33 = 58% variables out of 57 scheduled
c [elim-13] 33 < 1/100 * 57 = 0 considered unsuccessful
c [bca-12] limit of 10000000 steps and 2380989 added (scaled 2)
c [bca-12] 264980 out of 342222 literals actually usable 77%
c [bca-12] added 475 blocked clauses in 825530 steps
c [sweep-12] limit 11265602 penalty 0 = 0 + 0
c [sweep-12-1] 49794 pos 37.6% + 82625 neg 62.4% = 132419 sched 77.4% ret 38691
c [sweep-12-1] 11276089 steps 256 queries 22536.11 avg class size
c [sweep-12-1] 3318 decisions 232 SAT calls 38.15 avg env size
c [sweep-12-1] 130981 variables remain 77% (40093 retained 23%)
c [decomp-40] removed 2256 variables
c [sweep-12-1] removed 2256 vars (0 failed, 60 eqs, 67 impls)
c [sweep-12] removed 2256 vars in TOTAL (1 rounds, 255 queries)
c [sort-queue-16] sorted 168854 enqueued variables after 62004 conflicts
c [score-dist-16] active 0 (0%), one 0 (0%), zero 168854 (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 4990 variables 2.9% (168854 remain 15%)
c [simplification-16] removed 42702 irredundant clauses 3.5% (1180863 remain 27%)
c [simplification-16] maximum reduction of 3% = max (3%, 3%)
c [simplification-16] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-16] new conflict interval 24666
c [simplification-16] penalized conflict interval 24666 = 1 * 24666
c [simplification-16] hard conflict limit 99003 (soft 86670 + delta 12333)
c [simplification-16] new conflict limit 86670 (hard 99003)
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  518.1  168853  1180863     63027   51080 148039 273859    4  1015  155   0%     19  422    4    2  192%
c i  521.0  168852  1180863     63898   51728 148174 273922    4  1025  155   0%     11  425    4    2  178%
c i  521.1  168851  1180863     63931   51750 148179 273926    4  1034  155   0%     10  435    4    2  175%
c i  521.1  168850  1180863     63933   51750 148180 273926    4  1034  155   0%     10  434    4    2  174%
c i  522.5  168849  1180863     64318   52037 148244 273952    4  1038  155   0%      7  437    4    2  179%
c i  522.5  168848  1180863     64326   52042 148246 273952    4  1042  155   0%      7  440    4    2  180%
c i  525.1  168847  1180863     65060   52600 148362 274002    4  1033  155   0%      5  427    4    2  174%
c i  526.2  168714  1180862     65434   52873 148419 274033    4  1025  155   0%      4  416    4    2  178%
c i  526.6  168688  1180862     65551   52971 148428 274040    4  1015  155   0%      3  406    4    2  191%
c i  532.6  168687  1180862     67266   54280 148689 274154    4  1017  155   0%     12  396    4    2  188%
c i  535.2  168686  1180860     68173   54948 148826 274228    4  1028  155   0%      8  402    4    2  164%
c i  535.4  168630  1180860     68212   54972 148838 274230    4  1037  155   0%      7  411    4    2  161%
c i  536.6  168629  1180860     68593   55267 148888 274257    4  1039  155   0%      5  411    4    2  179%
c i  536.6  168628  1180860     68595   55267 148888 274258    4  1039  155   0%      5  410    4    2  177%
c i  536.7  168627  1180860     68615   55283 148889 274259    4  1046  155   0%      5  418    4    2  179%
c i  541.2  168626  1180860     70028   56345 149100 274368    4  1017  155   0%      9  380    4    2  174%
c i  541.2  168535  1180860     70032   56346 149100 274369    4  1017  155   0%      9  380    4    2  173%
c i  541.3  168534  1180860     70043   56354 149101 274370    4  1015  155   0%      8  379    4    2  172%
c i  541.3  168466  1180860     70044   56354 149101 274370    4  1015  155   0%      8  378    4    2  172%
c i  546.9  168460  1180860     71671   57605 149326 274494    4  1015  155   0%     11  369    4    2  180%
c i  550.3  168459  1180860     72586   58327 149440 274555    4  1035  155   0%      7  384    4    2  160%
c i  552.5  168458  1180860     73316   58872 149569 274599    4  1016  155   0%      5  361    4    2  157%
c i  553.1  168457  1180860     73504   59020 149595 274610    4  1012  155   0%      4  356    4    2  173%
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  553.5  168456  1180860     73613   59105 149607 274619    4  1006  155   0%      3  349    4    2  172%
c i  564.8  168418  1180860     76929   61733 150034 274809    4   997  155   0%     32  323    4    2  155%
c i  568.3  168417  1180860     77838   62431 150162 274876    4  1001  155   0%     15  323    4    2  176%
c i  568.6  168416  1180860     77896   62481 150167 274877    4  1008  155   0%     14  330    4    2  169%
c i  568.6  168415  1180860     77920   62493 150175 274880    4  1014  155   0%     14  335    4    2  163%
c i  574.6  168414  1180859     79466   63717 150354 274980    4  1006  155   0%     11  319    5    2  182%
c i  578.3  168413  1180859     80413   64440 150484 275054    4  1012  155   0%      6  321    4    3  167%
c i  580.2  168412  1180859     80892   64826 150541 275081    4  1005  155   0%      3  311    4    3  176%
c i  580.9  168411  1180859     81098   64975 150572 275101    4  1017  155   0%      2  323    4    3  166%
c i  580.9  168410  1180859     81105   64980 150572 275102    4  1022  155   0%      2  327    4    3  165%
c i  586.0  168384  1180857     82581   66162 150742 275196    4   994  155   0%      7  292    4    3  159%
c i  589.7  168383  1180857     83524   66929 150853 275240    4  1002  155   0%      5  296    4    3  160%
c i  589.7  168381  1180857     83530   66933 150854 275240    4  1002  155   0%      5  296    4    3  159%
c i  591.1  168219  1180857     83940   67251 150909 275264    4  1010  155   0%      3  302    4    3  164%
c i  595.9  168218  1180857     85297   68329 151070 275352    4  1004  155   0%      6  291    5    3  180%
c i  598.7  168176  1180857     85920   68843 151144 275376    4   992  156   0%      3  275    5    3  170%
c 
c [simplification-17] limit 86695 conflicts (hard 99003) hit after 86695 conflicts
c [quatres-13] found 209249 quaternary clauses 48% in total
c [quatres-13-1] removed 28 duplicate quaternary clauses
c [quatres-13-1] added 15 double-self-subsuming ternary resolvents
c [quatres-13-2] added 750 single-self-subsuming ternary resolvents
c [quatres-13-2] added 1270 quaternary resolvents
c [ternres-13] limit 51153871 with penalty 0 = 0 + 0
c [ternres-13] all 168176 free variables schedulable
c [ternres-13] 33192 ternary resolvents (940 bin, 32252 trn)
c [ternres-13] 949 variables remain 1% (167227 retained 99%)
c [decomp-41] removed 1385 variables
c [simpleprobe-7] 44123 schedulable variables 26%
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-42] removed 4679 variables
c [simpleprobe-7] 26125 variables remain 16% (136665 retained 84%)
c [simpleprobe-7] removed 4679 variables, found 162842 hbrs, 1019 units
c [unhide-17] limit 2557693 with penalty 2 = 0 + 2
c [unhide-17-17] 23 units, 46 failed, 18263 tauts, 0 hbrs, 13820 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 1313 transitive binary clauses
c [transred-13] found 5 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 162440 variables 100%
c [block-6] limit of 127884678 steps penalty 2 = 2 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 6480 blocked clauses
c [block-6] 6480 < 1/100 * 1125180 = 11251 considered unsuccessful
c [bca-13] limit of 10000000 steps and 2241747 added (scaled 2)
c [bca-13] 235132 out of 324066 literals actually usable 73%
c [bca-13] added 404 blocked clauses in 753738 steps
c [sweep-13] limit 15346161 penalty 0 = 0 + 0
c [sweep-13-1] 45462 pos 36.8% + 78134 neg 63.2% = 123596 sched 76.3% ret 38436
c [sweep-13-1] 15451811 steps 288 queries 13838.51 avg class size
c [sweep-13-1] 4733 decisions 258 SAT calls 42.79 avg env size
c [sweep-13-1] 121431 variables remain 75% (40582 retained 25%)
c [decomp-43] removed 286 variables
c [sweep-13-1] removed 286 vars (0 failed, 61 eqs, 88 impls)
c [sweep-13] removed 286 vars in TOTAL (1 rounds, 287 queries)
c [sort-queue-17] sorted 161746 enqueued variables after 86695 conflicts
c [score-dist-17] active 0 (0%), one 0 (0%), zero 161746 (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 6430 variables 3.8% (161746 remain 15%)
c [simplification-17] removed 64954 irredundant clauses 5.5% (1115903 remain 25%)
c [simplification-17] maximum reduction of 6% = max (4%, 6%)
c [simplification-17] large reduction 6% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 98695 (soft 88695 + delta 10000)
c [simplification-17] new conflict limit 88695 (hard 98695)
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  619.4  161745  1115902     87987   70104 159747 393109    4   961  158   0%     14  236    5    3  168%
c 
c [simplification-18] limit 88695 conflicts (hard 98695) hit after 88695 conflicts
c [quatres-14] found 202821 quaternary clauses 48% in total
c [quatres-14-1] removed 449 duplicate quaternary clauses
c [quatres-14-1] added 26 double-self-subsuming ternary resolvents
c [quatres-14-2] added 705 single-self-subsuming ternary resolvents
c [quatres-14-2] added 760 quaternary resolvents
c [ternres-14] limit 52367831 with penalty 0 = 0 + 0
c [ternres-14] 852 schedulable variables 1%
c [ternres-14] 23823 ternary resolvents (642 bin, 23181 trn)
c [ternres-14] 35 variables remain 0% (161702 retained 100%)
c [decomp-44] removed 134 variables
c [treelook-7] limit 5236783 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 131860 literals 41%
c [treelook-7] scheduling used 2966495 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 5236783 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 5293319 steps
c [treelook-7] 128286 literals remain 40%
c [treelook-7] 14028 variables remain to probed next time 9%
c [decomp-45] removed 184 variables
c [treelook-7] removed 3224 variables, found 11402 hbrs
c [unhide-18] limit 2618391 with penalty 2 = 0 + 2
c [unhide-18-18] 44 units, 334 failed, 65592 tauts, 0 hbrs, 31240 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 1214 transitive binary clauses
c [transred-14] found 2 units
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 158114 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 8688 variables 5% in round 1 in 325476983 steps
c [elim-14-1] backward subsumption/strengthening limit 74523017
c [elim-14-1-1] backward checking 48545 touched variables 31%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 743 and strengthened 679 clauses in 44710869 steps
c [elim-14-1] rescheduled 3892 variables 2% by backward subsumption
c [elim-14] incomplete 26 not tried 0% in round 2
c [gc-133] reconnected 312178 binary clauses (produced 0 empty 1 units)
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 9012 = 6% variables out of 158114 scheduled
c [bca-14] limit of 10000000 steps and 2107877 added (scaled 2)
c [bca-14] 218135 out of 298206 literals actually usable 73%
c [bca-14] added 790 blocked clauses in 703737 steps
c [sweep-14] limit 15710349 penalty 0 = 0 + 0
c [sweep-14-1] 40747 pos 36.2% + 71746 neg 63.8% = 112493 sched 75.4% ret 36609
c [sweep-14-1] 15721097 steps 384 queries 15764.44 avg class size
c [sweep-14-1] 4647 decisions 354 SAT calls 35.71 avg env size
c [sweep-14-1] 109835 variables remain 74% (39252 retained 26%)
c [decomp-46] removed 416 variables
c [sweep-14-1] removed 416 vars (0 failed, 91 eqs, 100 impls)
c [sweep-14] removed 416 vars in TOTAL (1 rounds, 383 queries)
c [sort-queue-18] sorted 148686 enqueued variables after 88695 conflicts
c [score-dist-18] active 0 (0%), one 0 (0%), zero 148686 (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 13051 variables 8.1% (148686 remain 14%)
c [simplification-18] removed 67100 irredundant clauses 6.0% (1048801 remain 24%)
c [simplification-18] maximum reduction of 8% = max (8%, 6%)
c [simplification-18] large reduction 8% >= 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 100695 (soft 90695 + delta 10000)
c [simplification-18] new conflict limit 90695 (hard 100695)
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.5  148685  1048801     89647   62228 151259 285229    4   957  150   0%     11  226    4    3  161%
c i  642.7  148600  1048801     90053   62547 151314 285254    4   957  150   0%      7  224    5    3  167%
c i  643.1  148599  1048801     90178   62633 151331 285271    4   957  150   0%      5  225    4    3  147%
c i  643.9  148593  1048801     90446   62837 151372 285288    4   959  150   0%      3  226    4    3  152%
c 
c [simplification-19] limit 90695 conflicts (hard 100695) hit after 90695 conflicts
c [quatres-15] found 193959 quaternary clauses 48% in total
c [quatres-15-1] removed 61 duplicate quaternary clauses
c [quatres-15-1] added 5 double-self-subsuming ternary resolvents
c [quatres-15-2] added 462 single-self-subsuming ternary resolvents
c [quatres-15-2] added 2143 quaternary resolvents
c [ternres-15] limit 53349605 with penalty 0 = 0 + 0
c [ternres-15] 31 schedulable variables 0%
c [ternres-15] 11340 ternary resolvents (247 bin, 11093 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 666870 penalty 4 = 4 + 0
c [gauss-5] extracted 1327 xors of average arity 3.0
c [gauss-5] connected 3959 occurrences of 1700 variables (average 2.3)
c [gauss-5] limit 666870 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-47] removed 110 variables
c [basicprobe-7] limit 266748027 penalty 0 = 0 + 0
c [basicprobe-7-0] 42118 sched 29%, 2019 failed, 152 lifted, 68923 hbrs
c [decomp-48] removed 4511 variables
c [basicprobe-7-1] 86441 probes remain 60% after last round
c [basicprobe-7-1] 2209 units = 2056 failed (93%) + 153 lifted (7%)
c [basicprobe-7-1] removed 4574 variables, found 72487 hbrs
c [bate-5] eliminated 1557 asymmetric tautologies during probing
c [unhide-19] limit 2667480 with penalty 2 = 0 + 2
c [unhide-19-19] 39 units, 134 failed, 8890 tauts, 0 hbrs, 6456 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 1295 transitive binary clauses
c [transred-15] found 8 units
c [cce-6] limit of 33343503 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 23
c [cce-6-1] eliminated 1 clauses out of 4 (25%) of length 21
c [cce-6-1] eliminated 2 clauses out of 463 (0%) of length 18
c [cce-6-1] eliminated 4 clauses out of 284 (1%) of length 17
c [cce-6-1] eliminated 9 clauses out of 287 (3%) of length 16
c [cce-6-1] eliminated 4 clauses out of 919 (0%) of length 15
c [cce-6-1] eliminated 51 clauses out of 927 (6%) of length 14
c [cce-6-1] eliminated 1 clauses out of 1417 (0%) of length 13
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 73 large clauses in 33343516 steps
c [cce-6-1] allowing another 16671758 steps for small clauses
c [cce-6-1] scheduling 521728 clauses = 386784 binary + 134944 ternary
c [cce-6-1] tried to eliminate 7405 small clauses 1%
c [cce-6-1] eliminated 770 binary clauses 0%
c [cce-6-1] eliminated 355 ternary clauses 0%
c [cce-6-1] eliminated 1125 small clauses 0%
c [cce-6-1] eliminated 2131 small clauses in 33343509 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 2204 covered clauses in round 1
c [cce-6] eliminated 2204 covered clauses in TOTAL during 1 rounds
c [cce-6] 2204 < 1/100 * 995307 = 9953 considered unsuccessful
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 143776 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 4387 variables 3% in round 1 in 293004654 steps
c [elim-15-1] backward subsumption/strengthening limit 293004600
c [elim-15-1-1] backward checking 26014 touched variables 18%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 261 and strengthened 441 clauses in 29449456 steps
c [elim-15-1] rescheduled 2710 variables 2% by backward subsumption
c [elim-15-2] eliminated 81 variables 0% in round 2 in 17746545 steps
c [elim-15-2] backward subsumption/strengthening limit 17746500
c [elim-15-2-1] backward checking 664 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 21 and strengthened 46 clauses in 1732064 steps
c [elim-15-2] rescheduled 191 variables 0% by backward subsumption
c [elim-15-3] eliminated 8 variables 0% in round 3 in 1850211 steps
c [elim-15-3] backward subsumption/strengthening limit 1850200
c [elim-15-3-1] backward checking 105 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 9 and strengthened 5 clauses in 706735 steps
c [elim-15] incomplete 34 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 4553 = 3% variables out of 143776 scheduled
c [bca-15] limit of 10000000 steps and 1954246 added (scaled 2)
c [bca-15] 201357 out of 278448 literals actually usable 72%
c [bca-15] added 705 blocked clauses in 654991 steps
c [sweep-15] limit 16004881 penalty 0 = 0 + 0
c [sweep-15-1] 37103 pos 36.0% + 65907 neg 64.0% = 103010 sched 74.0% ret 36213
c [sweep-15-1] 16079062 steps 479 queries 11240.48 avg class size
c [sweep-15-1] 6532 decisions 473 SAT calls 35.82 avg env size
c [sweep-15-1] 98465 variables remain 71% (40751 retained 29%)
c [decomp-49] removed 254 variables
c [sweep-15-1] removed 254 vars (0 failed, 72 eqs, 65 impls)
c [sweep-15] removed 254 vars in TOTAL (1 rounds, 478 queries)
c [sort-queue-19] sorted 138969 enqueued variables after 90695 conflicts
c [score-dist-19] active 0 (0%), one 0 (0%), zero 138969 (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 9624 variables 6.5% (138969 remain 13%)
c [simplification-19] removed 76782 irredundant clauses 7.3% (972019 remain 22%)
c [simplification-19] maximum reduction of 7% = max (6%, 7%)
c [simplification-19] large reduction 7% >= 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 102695 (soft 92695 + delta 10000)
c [simplification-19] new conflict limit 92695 (hard 102695)
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  673.8  138968   972019     90939   60326 143829 296388    4   928  146   0%      1  193    4    3  158%
c i  675.8  138967   972019     91606   60835 143929 296428    4   931  146   0%      1  194    4    3  144%
c i  676.9  138966   972019     91940   61115 143962 296443    4   937  146   0%     -0  199    5    3  172%
c i  678.9  138965   972018     92659   61671 144054 296495    4   946  146   0%     -0  206    4    3  143%
c i  680.0  138960   972018     93019   61948 144103 296523    4   948  146   0%     -1  207    4    3  146%
c i  680.9  138950   972018     93310   62185 144130 296542    4   951  146   0%     -2  209    5    3  168%
c i  683.0  138949   972018     94010   62756 144213 296577    4   956  146   0%     -1  211    4    3  153%
c i  683.7  138931   972018     94238   62937 144238 296589    4   975  146   0%     -1  230    5    3  172%
c i  685.0  138901   972018     94668   63274 144290 296619    4   963  146   0%     -2  216    5    3  162%
c i  685.7  138900   972018     94960   63506 144325 296639    4   975  146   0%     -2  228    4    3  147%
c i  685.8  138899   972018     94995   63534 144330 296639    4   972  146   0%     -2  224    4    3  145%
c i  686.2  138897   972018     95108   63624 144346 296642    4   966  146   0%     -2  217    4    3  146%
c i  686.2  138896   972018     95118   63630 144347 296644    4   964  146   0%     -2  216    4    3  144%
c i  686.2  138895   972018     95119   63630 144347 296644    4   964  146   0%     -2  216    4    3  144%
c i  686.6  138894   972018     95274   63744 144372 296656    4   979  146   0%     -3  231    4    3  137%
c i  688.6  138887   972018     95884   64228 144457 296685    4   963  146   0%     -2  212    4    3  150%
c i  690.9  138886   972018     96565   64775 144534 296732    4   958  146   0%     -1  205    5    3  160%
c 
c [simplification-20] limit 92706 conflicts (hard 102695) hit after 97310 conflicts
c [quatres-16] found 185302 quaternary clauses 48% in total
c [quatres-16-1] removed 48 duplicate quaternary clauses
c [quatres-16-1] added 14 double-self-subsuming ternary resolvents
c [quatres-16-2] added 210 single-self-subsuming ternary resolvents
c [quatres-16-2] added 1682 quaternary resolvents
c [ternres-16] limit 56574919 with penalty 0 = 0 + 0
c [ternres-16] all 138885 free variables schedulable
c [ternres-16] 21351 ternary resolvents (622 bin, 20729 trn)
c [ternres-16] 443 variables remain 0% (138442 retained 100%)
c [decomp-50] removed 211 variables
c [simpleprobe-8] 20072 schedulable variables 14%
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-51] removed 2931 variables
c [simpleprobe-8] 16158 variables remain 12% (119669 retained 88%)
c [simpleprobe-8] removed 2931 variables, found 106467 hbrs, 603 units
c [unhide-20] limit 2828745 with penalty 2 = 0 + 2
c [unhide-20-20] 10 units, 77 failed, 72814 tauts, 0 hbrs, 26256 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 1329 transitive binary clauses
c [transred-16] found 4 units
c [block-7] scheduling all variables this time
c [block-7] scheduled 135636 variables 100%
c [block-7] limit of 70718648 steps penalty 3 = 3 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 2836 blocked clauses
c [block-7] 2836 < 1/100 * 948544 = 9485 considered unsuccessful
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 135552 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 2305 variables 2% in round 1 in 278369051 steps
c [elim-16-1] backward subsumption/strengthening limit 278369000
c [elim-16-1-1] backward checking 22549 touched variables 17%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 321 and strengthened 308 clauses in 26575114 steps
c [elim-16-1] rescheduled 1811 variables 1% by backward subsumption
c [elim-16-2] eliminated 63 variables 0% in round 2 in 13129814 steps
c [elim-16-2] backward subsumption/strengthening limit 13129800
c [elim-16-2-1] backward checking 610 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 27 and strengthened 27 clauses in 1346499 steps
c [elim-16-2] rescheduled 148 variables 0% by backward subsumption
c [elim-16-3] eliminated 12 variables 0% in round 3 in 1765732 steps
c [elim-16-3] backward subsumption/strengthening limit 1765700
c [elim-16-3-1] backward checking 113 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 9 and strengthened 12 clauses in 637240 steps
c [elim-16] incomplete 40 not tried 0% in round 3
c [gc-151] reconnected 301619 binary clauses (produced 0 empty 2 units)
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 2425 = 2% variables out of 135552 scheduled
c [bca-16] limit of 10000000 steps and 1870450 added (scaled 2)
c [bca-16] 188843 out of 266256 literals actually usable 71%
c [bca-16] added 518 blocked clauses in 619353 steps
c [sweep-16] limit 16972475 penalty 0 = 0 + 0
c [sweep-16-1] 33470 pos 35.5% + 60722 neg 64.5% = 94192 sched 70.8% ret 38935
c [sweep-16-1] 17098412 steps 477 queries 11505.38 avg class size
c [sweep-16-1] 6039 decisions 460 SAT calls 36.09 avg env size
c [sweep-16-1] 90475 variables remain 68% (42586 retained 32%)
c [decomp-52] removed 268 variables
c [sweep-16-1] removed 268 vars (0 failed, 86 eqs, 74 impls)
c [sweep-16] removed 268 vars in TOTAL (1 rounds, 476 queries)
c [sort-queue-20] sorted 132859 enqueued variables after 97310 conflicts
c [score-dist-20] active 0 (0%), one 0 (0%), zero 132859 (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 6026 variables 4.3% (132859 remain 12%)
c [simplification-20] removed 42207 irredundant clauses 4.3% (929811 remain 21%)
c [simplification-20] maximum reduction of 4% = max (4%, 4%)
c [simplification-20] geometric conflict interval increment 4933 = 24666 / 5
c [simplification-20] new conflict interval 29599
c [simplification-20] penalized conflict interval 29599 = 1 * 29599
c [simplification-20] hard conflict limit 141708 (soft 126909 + delta 14799)
c [simplification-20] new conflict limit 126909 (hard 141708)
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  711.2  132858   929811     97398   63309 150106 291033    5   960  145   0%      1  204    5    3  170%
c i  711.6  132857   929811     97528   63412 150119 291042    5   949  145   0%     -0  193    5    3  159%
c i  714.7  132845   929811     98687   64304 150270 291135    4   959  145   0%      3  200    4    3  146%
c i  715.1  132783   929811     98859   64457 150277 291143    4   940  145   0%      2  180    4    3  146%
c i  716.6  132753   929811     99289   64799 150334 291162    4   940  145   0%      1  178    4    3  142%
c i  722.5  132658   929811    101253   66380 150572 291272    4   933  145   0%     12  167    4    3  144%
c i  723.4  132654   929811    101521   66595 150603 291286    4   934  145   0%      8  167    4    3  144%
c i  724.6  132652   929811    101901   66903 150644 291307    4   937  145   0%      5  169    5    3  165%
c i  726.2  132650   929811    102418   67318 150705 291338    4   967  145   0%      2  197    5    3  157%
c i  726.3  132605   929811    102430   67328 150706 291338    4   964  145   0%      2  195    5    3  155%
c i  731.2  132600   929811    103985   68601 150875 291422    5   956  145   0%      8  182    5    3  155%
c i  736.5  132599   929811    105662   69982 151044 291514    5   967  145   0%     10  189    4    3  143%
c i  748.6  132597   929811    109593   73236 151438 291721    5   958  145   0%     39  169    5    3  152%
c i  759.8  132594   929811    113312   76305 151848 291887    5   940  145   1%     35  142    5    3  147%
c i  760.4  132593   929811    113503   76457 151877 291894    5   941  145   1%     28  142    5    3  143%
c i  763.6  132592   929811    114488   77271 151975 291949    5   950  145   1%     11  149    4    3  132%
c i  765.5  132528   929811    115047   77727 152039 291977    5   927  145   1%      4  125    4    3  128%
c i  767.0  132518   929811    115536   78107 152095 292014    5   952  145   1%      1  149    5    3  147%
c i  774.5  132516   929811    117909   80076 152354 292118    5   939  145   1%     15  131    5    3  155%
c i  777.3  132515   929811    118820   80847 152444 292154    5   932  145   1%      5  122    5    3  141%
c i  785.0  132514   929811    121332   82946 152699 292257    5   913  145   1%     17   99    5    4  155%
c i  791.6  132513   929811    123475   84754 152914 292342    5   875  145   1%     13   58    5    4  143%
c i  793.3  132509   929811    124084   85258 152981 292370    5   871  145   1%      5   54    5    4  137%
c 
c [simplification-21] limit 126909 conflicts (hard 141708) hit after 126910 conflicts
c [quatres-17] found 183057 quaternary clauses 48% in total
c [quatres-17-1] removed 124 duplicate quaternary clauses
c [quatres-17-1] added 19 double-self-subsuming ternary resolvents
c [quatres-17-2] added 450 single-self-subsuming ternary resolvents
c [quatres-17-2] added 1462 quaternary resolvents
c [ternres-17] limit 71698676 with penalty 0 = 0 + 0
c [ternres-17] 404 schedulable variables 0%
c [ternres-17] 18927 ternary resolvents (756 bin, 18171 trn)
c [ternres-17] 1 variables remain 0% (132508 retained 100%)
c [card-6] limit 2240583 penalty 4 = 4 + 0
c [card-6] found 1392 at-most-one constraints of average size 3.2
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 2240583 for elimination
c [card-6] 1392 out of 1392 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-53] removed 688 variables
c [treelook-8] limit 7169867 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 107548 literals 41%
c [treelook-8] scheduling used 2469123 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 7169867 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 7536658 steps
c [treelook-8] 107350 literals remain 41%
c [treelook-8] 11382 variables remain to probed next time 9%
c [decomp-54] removed 13 variables
c [treelook-8] removed 26 variables, found 7331 hbrs
c [unhide-21] limit 3584933 with penalty 2 = 0 + 2
c [unhide-21-21] 12 units, 49 failed, 5908 tauts, 0 hbrs, 13901 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 1220 transitive binary clauses
c [transred-17] found 4 units
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 132092 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 1104 variables 1% in round 1 in 269326184 steps
c [elim-17-1] backward subsumption/strengthening limit 269326100
c [elim-17-1-1] backward checking 9423 touched variables 7%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 58 and strengthened 73 clauses in 13324250 steps
c [elim-17-1] rescheduled 479 variables 0% by backward subsumption
c [elim-17-2] eliminated 15 variables 0% in round 2 in 6111816 steps
c [elim-17-2] backward subsumption/strengthening limit 6111800
c [elim-17-2-1] backward checking 161 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 15 and strengthened 17 clauses in 784532 steps
c [elim-17-2] rescheduled 51 variables 0% by backward subsumption
c [elim-17-3] eliminated 1 variables 0% in round 3 in 666639 steps
c [elim-17-3] backward subsumption/strengthening limit 666600
c [elim-17-3-1] backward checking 16 touched variables 0%
c [elim-17-3-1] fully completed backward checking in 1 rounds
c [elim-17-3] subsumed 0 and strengthened 0 clauses in 401793 steps
c [elim-17] fully completed in 3 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 1139 = 1% variables out of 132092 scheduled
c [elim-17] 1139 < 1/100 * 132092 = 1320 considered unsuccessful
c [bca-17] limit of 10000000 steps and 1835775 added (scaled 2)
c [bca-17] 171695 out of 261908 literals actually usable 66%
c [bca-17] added 169 blocked clauses in 588058 steps
c [sweep-17] limit 21509602 penalty 0 = 0 + 0
c [sweep-17-1] 31499 pos 35.3% + 57652 neg 64.7% = 89151 sched 68.1% ret 41802
c [sweep-17-1] 21948545 steps 449 queries 8189.45 avg class size
c [sweep-17-1] 7208 decisions 441 SAT calls 39.50 avg env size
c [sweep-17-1] 85062 variables remain 65% (45873 retained 35%)
c [decomp-55] removed 207 variables
c [sweep-17-1] removed 207 vars (0 failed, 64 eqs, 57 impls)
c [sweep-17] removed 207 vars in TOTAL (1 rounds, 448 queries)
c [sort-queue-21] sorted 130746 enqueued variables after 126910 conflicts
c [score-dist-21] active 0 (0%), one 0 (0%), zero 130746 (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 1763 variables 1.3% (130746 remain 12%)
c [simplification-21] removed 17218 irredundant clauses 1.9% (912593 remain 21%)
c [simplification-21] maximum reduction of 2% = max (1%, 2%)
c [simplification-21] geometric conflict interval increment 9866 = 29599 / 3
c [simplification-21] new conflict interval 39465
c [simplification-21] penalized conflict interval 39465 = 1 * 39465
c [simplification-21] hard conflict limit 186107 (soft 166375 + delta 19732)
c [simplification-21] new conflict limit 166375 (hard 186107)
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  820.6  130745   912593    128100   87042 164658 293280    5   912  148   1%     37   91    5    4  138%
c i  825.5  130740   912593    129711   88415 164809 293337    5   905  148   1%     11   81    5    4  125%
c i  828.8  130729   912593    130797   89377 164887 293364    5   900  148   1%      3   75    6    4  156%
c i  845.3  130728   912593    135972   93849 165336 293533    6   879  148   1%     53   49    6    4  150%
c i  848.7  130714   912593    137063   94790 165424 293573    6   900  148   1%     16   69    7    4  165%
c i  851.7  130713   912593    137918   95537 165492 293600    6   882  148   1%      4   51    5    4  129%
c i  853.2  130701   912593    138430   95980 165537 293616    6   878  148   1%     -1   46    6    4  141%
c i  861.4  130610   912593    140823   98036 165755 293702    6   884  148   1%     11   50    6    4  157%
c i  866.7  130604   912593    142372   99382 165875 293755    6   898  148   1%      4   63    6    4  136%
c i  868.1  130595   912593    142818   99782 165911 293763    6   894  148   1%     -1   59    6    4  143%
c i  877.7  130502   912593    145703  102299 166150 293840    6   886  149   1%     17   48    6    4  131%
c i  883.2  130501   912593    147281  103662 166292 293885    6   893  149   1%      5   53    5    4  130%
c i  884.7  130497   912593    147755  104082 166324 293900    6   896  149   1%     -0   56    6    4  139%
c i  890.6  130490   912593    149552  105619 166492 293952    6   895  149   1%      4   54    6    4  138%
c i  896.6  130465   912593    151286  107120 166635 294006    6   876  149   1%      4   34    6    4  145%
c i  897.1  130464   912593    151463  107277 166650 294010    6   870  149   1%      1   28    6    4  131%
c i  897.4  130463   912593    151544  107345 166658 294014    6   888  149   1%      0   45    5    4  125%
c i  898.5  130457   912593    151903  107666 166680 294023    6   859  149   1%     -3   16    6    4  131%
c i  912.7  130456   912593    156249  111502 167014 294135    6   866  150   1%     38   21    6    4  129%
c i  914.3  130449   912593    156773  111950 167066 294152    6   885  150   1%     19   41    6    4  131%
c i  925.5  130438   912593    160038  114805 167325 294233    6   896  150   1%     22   49    7    5  146%
c i  931.3  130437   912593    161724  116303 167454 294263    6   926  150   1%      5   77    6    5  136%
c i  931.9  130436   912593    161904  116460 167468 294269    6   933  150   1%      2   84    6    5  140%
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  934.8  130434   912593    162777  117216 167542 294295    6   925  150   1%     -3   76    6    5  130%
c i  936.5  130420   912593    163282  117660 167581 294310    6   930  150   1%     -6   80    7    5  141%
c i  938.4  130419   912593    163816  118131 167613 294329    6   919  150   1%     -8   68    7    5  143%
c i  942.0  130418   912593    164835  119020 167695 294360    6   934  150   1%     -6   82    6    5  128%
c 
c [simplification-22] limit 166375 conflicts (hard 186107) hit after 166487 conflicts
c [quatres-18] found 185362 quaternary clauses 47% in total
c [quatres-18-1] removed 22 duplicate quaternary clauses
c [quatres-18-1] added 18 double-self-subsuming ternary resolvents
c [quatres-18-2] added 280 single-self-subsuming ternary resolvents
c [quatres-18-2] added 866 quaternary resolvents
c [ternres-18] limit 94878297 with penalty 0 = 0 + 0
c [ternres-18] 1 schedulable variables 0%
c [ternres-18] 22020 ternary resolvents (348 bin, 21672 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-56] removed 611 variables
c [basicprobe-8] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 43782 probes remain 34% after last round
c [basicprobe-8-0] 1365 units = 1168 failed (86%) + 197 lifted (14%)
c [basicprobe-8-0] removed 2156 variables, found 87757 hbrs
c [bate-6] eliminated 557 asymmetric tautologies during probing
c [unhide-22] limit 4743914 with penalty 2 = 0 + 2
c [unhide-22-22] 23 units, 132 failed, 47423 tauts, 0 hbrs, 101704 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 497 transitive binary clauses
c [bca-18] limit of 10000000 steps and 1771724 added (scaled 2)
c [bca-18] 153306 out of 255616 literals actually usable 60%
c [bca-18] added 349 blocked clauses in 556767 steps
c [sweep-18] boosting sweeping limit by 10
c [sweep-18] limit 284634890 penalty 0 = 0 + 0
c [sweep-18-1] 29553 pos 35.4% + 53885 neg 64.6% = 83438 sched 65.3% ret 44369
c [sweep-18-1] 284947653 steps 4217 queries 957.43 avg class size
c [sweep-18-1] 53708 decisions 3945 SAT calls 35.02 avg env size
c [sweep-18-1] 39531 variables remain 31% (87272 retained 69%)
c [decomp-57] removed 3711 variables
c [sweep-18-1] removed 3711 vars (0 failed, 1168 eqs, 948 impls)
c [sweep-18] removed 3711 vars in TOTAL (1 rounds, 4216 queries)
c [sort-queue-22] sorted 124096 enqueued variables after 166487 conflicts
c [score-dist-22] active 0 (0%), one 0 (0%), zero 124096 (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 6321 variables 4.8% (124096 remain 11%)
c [simplification-22] removed 47432 irredundant clauses 5.2% (865161 remain 20%)
c [simplification-22] maximum reduction of 5% = max (5%, 5%)
c [simplification-22] large reduction 5% >= 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 178487 (soft 168487 + delta 10000)
c [simplification-22] new conflict limit 168487 (hard 178487)
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  996.6  124095   865161    167202  120718 151985 311134    6   877  150   1%      9   23    6    5  129%
c i  996.9  124094   865161    167302  120810 151990 311136    6   873  150   1%      7   19    6    5  136%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 6016 basic ate = 4537 trn 75% + 1479 lrg 25% in 6 updates
c bcas: 18 count, 18369 added (14446 skipped), 17991166 steps
c bkwd: tried 2396695 clauses, 4785384 lits, 2.00 lits/clause
c bkwd: checked 206781523 occs, 86.28 occs/clause, 43.21 occs/lit
c bkwd: subsumed 57 binary, 2093 ternary, 2261 large
c bkwd: strengthened 40 binary, 43 ternary (100% self), 8824 large (0% self)
c blkd: 7 bces, 77113 removed, 48269166 resolutions, 126846586 steps
c blkd: 33498 blocking literals 1%, 2462 pure
c bump: 0 bumped seen, 0 lits 0.0 on average
c card: 6 count, 0 units, 0 am1, 84181807 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 12599 subsumed
c card: 4206 at-most-one constraints found, average size 3.11
c card: 4206 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, 29735 eliminated, 29020 ate 98%, 715 abce 2%
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: 15562735 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 166 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 57 decompositions, 122868 equivalent 11%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 58681913 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 17 elims, 622043 eliminated 55%, 9655 pure 2%
c elms: 30 rounds, 1.8 rounds/bve
c elms: 537485 small 86%, 72441 large 12%
c elms: 730027 tried small, 537485 succeeded 74%, 192542 failed 26%
c elms: 272674 subsumed, 343524 strengthened, 6495 blocked
c elms: 51265120 copies, 63203782 resolutions, 14866900 ipos
c elms: 45113087 subchks, 81772535 strchks
c gaus: 5 extractions, 18304 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10680064 steps, 5340032 extr 50%, 5201550 elim 49%
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: 1396370 = 621474 simple 45% + 763930 trn 55% + 10966 lrg 1%, 30891 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 178902 clauses, 9.5 length
c lrnd: 1700262 lits = 2251416 orig - 551154 removed 24%
c lrnd: 109900 uips 61%, 12625 flips 7%
c mins: 141730 mins 79%, 10435 bin 6%, 26737 size 15%
c mins: 3711956 poisoned searches, 457697 hits, 12% hit rate
c mins: 5243306 used twice searches, 363943 hits, 7% hit rate
c move: moved 106827, 45643 bin 43%, 61184 trn 57%
c otfs: 2480 driving 48%, 2688 restarting 52%
c otfs: str 5168, 3497 red 68%, 1671 irr 32%
c otfs: str 5168, 0 bin 0%, 1959 trn 38%, 3209 lrg 62%
c otfs: sub 167, 138 red 83%, 29 irr 17%
c otfs: sub 167, 0 bin 0%, 128 trn 77%, 39 lrg 23%
c phas: 4 computed, 773208 set, 358258 pos (46%), 414950 neg (54%)
c prbs: 8 basic, 402275 probed, 10546 failed, 2973 lifted
c prbs: 8 simple, 1974282 probed, 4511 failed, 19917 eqs
c prbs: 8 treelook, 870 probed, 78 failed, 0 lifted
c prom: 0 locked 0% out of 39080 tried
c prps: 1594885061 props, 25 props/dec
c prps: 92% srch, 8% simp, 0% lkhd
c quat: 18 count, 43327 quat, 14218 self1, 403 self2, 4675 dup
c queu: 22 sorted, 58681913 next (0 steps 0.00)
c queu: 6768287 enq (6768264 steps 1.00), 0 deq 0%
c redc: 19245 clauses 17%, 110603 tried 66%, 641 sat 1%
c redc: 29800 lits 4%, 762380 tried 34%, 642 sat 0%
c redc: 1498 times jump level reduced, 303.8 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: 254988 removed, 166046 red 65%
c rsts: 16165 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: 22 count, 18 confs 82%, 0 vars 0%
c simp: 1 its 5%, 2 bin 9%, 1 trns 5%
c subl: 178902 count (38056 tried 0.2), 2039 sub out of 135697 (1.5%)
c swps: 18 count, 18 rounds, 9737 queries (540.9/round)
c swps: 9154 sat calls, 1724 unsat (1.5% success rate)
c swps: 129296 decisions 14.1, 14041 conflicts 1.5
c swps; 11544.6 avg class size, 36.1 avg environment size
c swps: 0 failed, 2161 impls, 2232 equivs
c swp0: 3238 type 0 queries, 917 unsat (28.3%), 2929 sat (90.5%)
c swp1: 6499 type 1 queries, 4684 unsat (72.1%), 4576 sat (70.4%)
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: 117364815 calls to obtain time
c tops: 262641 fixed 23%, 572 its, 292.55 confs/it
c trds: 18 transitive reductions, 17172 removed, 179 failed
c trds: 274029 nodes, 452740 edges, 35645998 steps
c trim: 398239 words, 1.5 MB
c trnr: 18 count, 14605 bin, 598407 trn, 584431716 steps
c unhd: 22 count, 22 rounds, 226020685 steps
c unhd: 25897 non-trivial sccs of average size 2.5
c unhd: 4606 units, 4562 bin, 42 trn, 2 lrg
c unhd: 7417 failed, 6569 stamp, 0 lits, 54 bin, 645 trn, 2 lrg
c unhd: 565467 tauts, 8964 bin 2%, 138118 trn 24%, 33709 lrg 6%
c unhd: 565467 tauts, 384676 stamp 68%, 418438 red 74%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 618590 str, 4562 bin 1%, 84240 trn 14%, 529788 lrg 86%, 196358 red 32%
c vars: 124094 remaining 11% and 1007552 removed 89% out of 1131646
c vars: 262641 fixed 23%, 622043 eliminated 55%, 122868 equivalent 11%
c vsts: 10669228958 visits, 89% srch, 11% simp, 0% lkhd
c vsts: 6.5 search visits per propagation, 57012.2 per conflict
c wchs: 1955548373 pushed, 217031261 enlarged, 245 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         179024             0             0      25765072        478608         30516
c 
c  0 0        125323  70         0   0<        0   0< 23995199  93<   420176  88<    26814  88<    2.3
c  1 5         14140   8<        0   0         0   0    821699   3     24518   5      1647   5     0.5
c  2 6         21789  12         0   0         0   0    719049   3     24024   5      1443   5     1.1
c  3 9         11563   6         0   0         0   0    187603   1      7421   2       448   1     0.9
c  4 14         4384   2         0   0         0   0     30696   0      1812   0       129   0     0.5
c  5 21         1369   1         0   0         0   0      9675   0       530   0        27   0     0.2
c  6 30          351   0         0   0         0   0      1027   0        97   0         5   0     0.1
c  7 41           85   0         0   0         0   0        99   0        24   0         2   0     0.0
c  8 54           20   0         0   0         0   0        25   0         6   0         1   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   91.531   9% elim
c   84.040   8% probe
c   65.848   7% sweep
c   36.239   4% decide
c   28.928   3% unhide
c   17.118   2% block
c   17.000   2% cce
c   16.167   2% bca
c   14.976   2% quatres
c 
c   23.106 < 1% rest (below)
c 
c   13.656   1% ternres
c    6.514   1% gauss
c    2.361   0% transred
c    0.575   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.041   1% preprocessing     3%
c  390.373  39% inprocessing     97%
c ==================================
c  403.414  40% simplifying
c  593.607  60% search
c ==================================
c  997.041 100% all
c 
c        167341 conflicts,         167.8 confs/sec
c         23813 ternaries,           7.0 confs/ternary
c         12517 binaries,           13.4 confs/binary
c           572 iterations,        292.6 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c         16165 restarts,           16.2 rests/sec,     10.4 confs/restart
c      58681913 decisions,       58856.0 decis/sec,    350.7 decis/conflict
c    1594885061 propagations,  1599617.6 props/sec,     27.2 props/decision
c 
c 997.0 seconds, 389.6 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
