c launch: /data/cnf/sc2014/app/UR-20-10p0.cnf.bz2
c host: atom20
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/UR-20-10p0.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UR-20-10p0.cnf.bz2
c no embedded options
c found 'p cnf 258781 1372095' header
c read 258781 variables, 1372095 clauses, 3305764 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=2
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 245632 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] VMTF (--score=2)
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  245632  1358076         0       0      0     0    0     0   58   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 6804 at-most-one constraints of average size 5.6
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6804 out of 6804 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 62852 variables
c [simpleprobe-1] all 195929 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 70 variables
c [simpleprobe-1] 14722 variables remain 8% (181137 retained 92%)
c [simpleprobe-1] removed 70 variables, found 15244 hbrs, 1 units
c [unhide-1] limit 65167 based on 1042681 irredundant clauses
c [unhide-1-1] 3 units, 1349 failed, 9125 tauts, 0 hbrs, 12840 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 194873 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 62441 not tried 32% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 74913 = 38% variables out of 194873 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 869726 negative 99.2% of 876327 except 6601 0.8%
c [phase-count-1] 704626 positive 80.4% of 876327 except 171701 19.6%
c [phase-count-1] less non-negative clauses 6601 than limit 87600 (10.0%)
c [phase-count-1] non-pos/non-neg = 171701/6601 = 26.01 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 119960 negative 100%
c [sort-queue-1] sorted 119960 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 119960 (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 82244 variables 40.7% (119960 remain 49%)
c [simplification-1] removed 481749 irredundant clauses 35.5% (876327 remain 65%)
c [simplification-1] maximum reduction of 41% = max (41%, 35%)
c [simplification-1] large reduction 41% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    5.2  119959   876327        19      13      2 10579    0     5   58   1%      0    5    0    0 24611%
c i    5.2  119107   876327        20      13      2 10579    0     5   58   1%      0    5    0    0 24515%
c i    5.3  119096   876327       146     127      7 10584    0     8   58   5%      0    8    5    0 20121%
c i    5.3  118368   876327       151     131      7 10584    0     8   58   5%      0    8    5    0 19915%
c i    5.4  118356   876327       227     187     14 10594    0     9   58   5%      0    9    5    0 16333%
c i    5.4  118292   876327       263     207     20 10601    1    10   58   5%      0   10    5    0 14834%
c i    5.5  117591   876327       300     235     25 10604    1    10   58   5%      0   10    5    0 13768%
c i    5.7  117578   876327       576     457     54 10624    1    15   58   7%      1   15    6    0 9563%
c i    5.7  117436   876327       577     457     54 10624    1    15   58   7%      1   15    6    0 9526%
c i    5.7  117424   876327       605     481     55 10625    1    15   58   6%      1   15    6    0 8979%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 2720 variables
c [simpleprobe-2] 14264 schedulable variables 12%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 14971 variables remain 13% (102269 retained 87%)
c [simpleprobe-2] removed 0 variables, found 1581 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 83998 literals 36%
c [treelook-1] scheduling used 586381 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 542318 steps
c [treelook-1] 83988 literals remain 36%
c [treelook-1] 81118 variables remain to probed next time 69%
c [treelook-1] removed 5 variables, found 3263 hbrs
c [basicprobe-1] limit 6865416 based on 858177 irredundant clauses
c [basicprobe-1-0] 45264 probes remain 39% after last round
c [basicprobe-1-0] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 540 variables, found 23256 hbrs
c [unhide-2] limit 53636 based on 858177 irredundant clauses
c [unhide-2-2] 3 units, 1244 failed, 8398 tauts, 0 hbrs, 1542 literals
c [elim-2] 60691 variables 53% will be scheduled this time
c [elim-2] scheduled 60691 variables 53%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 25444 not tried 22% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 61 = 0% variables out of 60691 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 821280 negative 99.2% of 827883 except 6603 0.8%
c [phase-count-2] 662243 positive 80.0% of 827883 except 165640 20.0%
c [phase-count-2] less non-negative clauses 6603 than limit 82700 (10.0%)
c [phase-count-2] non-pos/non-neg = 165640/6603 = 25.09 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 19257 negative 100%
c [sort-queue-2] sorted 115408 enqueued variables after 605 conflicts
c [score-dist-2] active 0 (0%), one 10369 (9%), zero 105039 (91%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 1917 variables 1.6% (115408 remain 47%)
c [simplification-2] removed 48444 irredundant clauses 5.5% (827883 remain 61%)
c [simplification-2] maximum reduction of 6% = max (2%, 6%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1022 (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    9.3  115407   827883       671     515     64 27822    2    21   55  10%      1   21   21    0 14700%
c i    9.3  115313   827883       673     516     64 27822    2    21   55  10%      1   21   21    0 14587%
c i    9.4  115273   827883       708     544     68 27824    2    24   55   9%      1   24   19    0 12928%
c i    9.4  114070   827883       721     552     71 27825    2    24   55   9%      1   24   18    0 12349%
c i    9.4  113207   827883       724     554     71 27825    2    24   55   9%      1   24   18    0 12213%
c i    9.5  113195   827883       768     588     75 27830    2    25   55   9%      1   25   16    0 10533%
c i    9.5  113166   827883       772     590     75 27831    2    25   55   9%      1   25   15    0 10390%
c i    9.6  113006   827883       778     594     76 27831    2    26   55   9%      1   26   15    0 10202%
c i    9.6  112880   827883       794     606     77 27833    2    26   55   9%      1   26   14    0 9675%
c i    9.6  112650   827883       803     612     77 27835    2    26   55   9%      1   26   14    0 9385%
c i    9.6  112382   827883       804     612     77 27835    2    26   55   9%      1   26   14    0 9349%
c i    9.6  112369   827883       807     612     79 27835    2    26   55   8%      1   26   14    0 9243%
c i    9.7  112163   827883       821     619     81 27839    2    27   55   8%      1   27   13    0 8801%
c i    9.9  112159   827883       926     688     96 27858    2    32   55   7%      1   32   12    0 7087%
c i    9.9  112149   827883       943     702     96 27859    2    32   55   8%      1   32   13    0 7442%
c 
c [simplification-3] limit 1047 conflicts (hard 11000) hit after 1047 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3979 at-most-one constraints of average size 4.6
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3979 out of 3979 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 3391 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 90756 literals 41%
c [treelook-2] scheduling used 669332 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 327492 steps
c [treelook-2] 90746 literals remain 41%
c [treelook-2] 69702 variables remain to probed next time 62%
c [treelook-2] removed 3 variables, found 2481 hbrs
c [unhide-3] limit 50213 based on 803418 irredundant clauses
c [unhide-3-3] 8 units, 585 failed, 13762 tauts, 0 hbrs, 580 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 110990 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 33513 not tried 30% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 3266 = 3% variables out of 110990 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 768996 negative 99.2% of 775524 except 6528 0.8%
c [phase-count-3] 621473 positive 80.1% of 775524 except 154051 19.9%
c [phase-count-3] less non-negative clauses 6528 than limit 77500 (10.0%)
c [phase-count-3] non-pos/non-neg = 154051/6528 = 23.60 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 6300 negative 100%
c [sort-queue-3] sorted 107724 enqueued variables after 1047 conflicts
c [score-dist-3] active 0 (0%), one 22234 (21%), zero 85490 (79%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 4412 variables 3.9% (107724 remain 44%)
c [simplification-3] removed 52359 irredundant clauses 6.3% (775524 remain 57%)
c [simplification-3] maximum reduction of 6% = max (4%, 6%)
c [simplification-3] large reduction 6% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13047 (soft 3047 + delta 10000)
c [simplification-3] new conflict limit 3047 (hard 13047)
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   12.9  107723   775524      1096     789    103 27479    3    39   53   8%      1   39   17    0 7924%
c i   12.9  107720   775524      1099     791    103 27479    3    39   53   8%      1   39   17    0 7942%
c i   13.0  107709   775524      1126     813    106 27480    3    40   53   8%      1   40   16    0 7344%
c i   13.0  107653   775524      1137     820    106 27482    3    40   53   8%      1   40   16    0 7097%
c i   13.0  107281   775524      1142     822    106 27484    3    40   53   8%      1   40   15    0 6971%
c i   13.0  107270   775524      1149     826    106 27486    3    40   53   8%      1   40   15    0 6813%
c i   13.0  107260   775524      1151     826    107 27486    3    40   53   8%      1   40   15    0 6763%
c i   13.1  107218   775524      1189     848    109 27494    3    41   53   8%      1   40   14    0 6095%
c i   13.1  107205   775524      1194     849    109 27497    3    41   53   8%      1   40   13    0 5983%
c i   13.1  107203   775524      1217     868    111 27498    3    41   53   8%      1   41   13    0 5614%
c i   13.1  106787   775524      1224     873    111 27499    3    41   53   8%      1   40   12    0 5487%
c i   13.2  106785   775524      1274     904    118 27507    3    42   53   8%      1   42   11    0 4757%
c i   13.2  106773   775524      1334     948    126 27512    3    42   53   8%      1   42    9    0 4045%
c i   13.2  106760   775524      1335     948    126 27512    3    42   53   8%      1   42    9    0 4029%
c i   13.3  106747   775524      1358     965    128 27515    3    42   53   8%      1   42    9    0 3821%
c i   13.3  106469   775524      1367     967    131 27518    3    42   53   8%      1   42    9    0 3709%
c i   13.3  106370   775524      1368     967    131 27518    3    42   53   8%      1   42    9    0 3695%
c i   13.3  106361   775524      1393     988    132 27519    3    43   53   8%      1   42    9    0 3625%
c i   13.3  105946   775524      1394     988    132 27519    3    43   53   8%      1   42    9    0 3611%
c i   13.3  105922   775524      1421    1003    135 27526    3    43   53   8%      1   42    8    0 3351%
c i   13.4  105291   775524      1462    1035    138 27531    3    43   53   8%      1   43    8    0 3326%
c i   13.4  105277   775524      1511    1066    146 27538    3    44   53   8%      1   43    8    0 3059%
c i   13.6  104590   775524      1606    1133    159 27550    3    44   53   8%      1   43    6    0 2574%
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.6  104425   775524      1608    1133    159 27551    3    44   53   8%      1   43    6    0 2556%
c i   13.6  104415   775524      1628    1141    162 27558    3    44   53   8%      1   43    6    0 2455%
c i   13.6  104262   775524      1678    1169    172 27567    3    45   53   7%      1   44    6    0 2277%
c i   13.7  104247   775524      1706    1190    174 27571    3    45   53   7%      1   45    6    0 2221%
c i   13.7  104212   775524      1713    1194    175 27572    3    45   53   7%      1   45    6    0 2198%
c 
c [simplification-4] limit of 192 binary hit after 192 binaries
c [decomp-8] removed 3585 variables
c [basicprobe-2] limit 6041872 based on 755234 irredundant clauses
c [basicprobe-2-0] 36459 probes remain 36% after last round
c [basicprobe-2-0] 28 units = 28 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 3332 variables, found 19839 hbrs
c [unhide-4] limit 70634 with penalty 1 = 0 + 1
c [unhide-4-4] 11 units, 915 failed, 8912 tauts, 0 hbrs, 760 literals
c [elim-4] 24399 variables 25% will be scheduled this time
c [elim-4] scheduled 24399 variables 25%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 2 variables 0% in round 1 in 45942929 steps
c [elim-4-1] backward subsumption/strengthening limit 45942900
c [elim-4-1-1] backward checking 59 touched variables 0%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 1 and strengthened 0 clauses in 132301 steps
c [elim-4-1] rescheduled 3 variables 0% by backward subsumption
c [elim-4-2] eliminated 2 variables 0% in round 2 in 504 steps
c [elim-4-2] backward subsumption/strengthening limit 500
c [elim-4-2-1] backward checking 9 touched variables 0%
c [elim-4-2-1] incomplete backward checking 7 remain 78%
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 501 steps
c [elim-4-2] fully rescheduled 99480 variables 100%
c [elim-4-3] eliminated 1668 variables 2% in round 3 in 69297933 steps
c [elim-4-3] backward subsumption/strengthening limit 69297900
c [elim-4-3-1] backward checking 5262 touched variables 5%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 0 and strengthened 0 clauses in 1947423 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 1692 = 7% variables out of 24399 scheduled
c [phase-count-4] 703535 negative 99.1% of 709936 except 6401 0.9%
c [phase-count-4] 569678 positive 80.2% of 709936 except 140258 19.8%
c [phase-count-4] less non-negative clauses 6401 than limit 70900 (10.0%)
c [phase-count-4] non-pos/non-neg = 140258/6401 = 21.91 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 3721 negative 100%
c [sort-queue-4] sorted 97792 enqueued variables after 1733 conflicts
c [score-dist-4] active 0 (0%), one 29359 (30%), zero 68433 (70%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 6415 variables 6.2% (97792 remain 40%)
c [simplification-4] removed 65588 irredundant clauses 8.5% (709936 remain 52%)
c [simplification-4] maximum reduction of 8% = max (6%, 8%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3098 (hard 13047)
c [simplification-4] 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   17.7   97791   709936      1900    1300    183 35276    3    49   49   7%      1   49    6    0 2197%
c i   17.7   97494   709936      1902    1301    183 35276    3    49   49   7%      1   49    6    0 2184%
c i   17.9   97274   709936      1965    1344    185 35288    4    52   50   7%      1   51    6    0 2152%
c i   17.9   97268   709936      1970    1347    186 35288    4    51   50   7%      1   51    6    0 2124%
c i   17.9   97234   709936      1989    1362    187 35290    4    52   50   7%      1   51    7    0 2360%
c i   17.9   97061   709936      2002    1367    189 35295    4    52   50   7%      1   51    7    0 2273%
c i   18.0   97054   709936      2037    1385    195 35305    4    52   50   7%      1   51    6    0 2128%
c i   18.0   97019   709936      2042    1387    197 35305    4    52   50   7%      1   51    6    0 2100%
c i   18.0   97012   709936      2080    1412    197 35311    4    52   50   7%      1   51    7    0 2387%
c i   18.1   97005   709936      2099    1425    200 35313    4    52   50   7%      1   52    7    0 2330%
c i   18.2   96996   709936      2257    1556    208 35323    4    55   50   7%      1   54    8    0 2399%
c i   18.2   96995   709936      2279    1567    209 35328    4    55   50   7%      1   54    7    0 2265%
c i   18.2   96993   709936      2280    1567    209 35328    4    55   50   7%      1   54    7    0 2256%
c i   18.2   96992   709936      2300    1584    210 35329    4    56   50   7%      1   55    8    0 2534%
c i   18.2   96986   709936      2301    1584    210 35329    4    56   50   7%      1   55    8    0 2524%
c i   18.3   96826   709936      2340    1616    213 35332    4    56   50   7%      1   55    8    0 2350%
c i   18.3   96816   709936      2341    1616    213 35332    4    56   50   7%      1   55    8    0 2341%
c i   18.3   96553   709936      2397    1660    216 35339    4    56   50   7%      1   55    7    0 2137%
c i   18.4   96551   709936      2497    1727    229 35354    4    57   50   7%      1   56   10    0 2804%
c i   18.4   96542   709936      2508    1734    230 35356    4    57   50   7%      1   56   10    0 2762%
c i   18.5   96349   709936      2519    1743    230 35357    4    57   50   7%      1   56   10    0 2699%
c i   18.5   96142   709936      2564    1771    236 35366    4    58   50   7%      1   56    9    0 2474%
c i   18.5   96006   709936      2566    1771    236 35367    4    58   50   7%      1   56    9    0 2456%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   18.5   95989   709936      2579    1777    239 35370    4    58   50   7%      1   56    8    0 2363%
c i   18.6   95984   709936      2604    1788    240 35382    4    58   50   7%      1   56    8    0 2215%
c i   18.9   95869   709936      2782    1891    256 35437    4    58   50   7%      1   57    6    0 1706%
c i   18.9   95866   709936      2791    1895    257 35440    4    58   50   7%      1   57    6    0 1667%
c i   18.9   95856   709936      2792    1895    257 35440    4    58   50   7%      1   57    6    0 1660%
c i   19.0   95852   709936      2852    1933    262 35456    4    59   50   7%      1   58    6    0 1520%
c i   19.0   95844   709936      2854    1933    262 35457    4    59   50   7%      1   58    6    0 1509%
c i   19.0   95678   709936      2873    1940    266 35462    4    59   50   7%      1   57    5    0 1433%
c i   19.0   95673   709936      2898    1957    269 35464    4    59   50   7%      1   57    5    0 1380%
c i   19.0   95668   709936      2909    1962    271 35467    4    59   50   7%      1   57    5    0 1347%
c i   19.0   95667   709936      2944    1980    279 35473    4    59   50   7%      1   57    5    0 1276%
c i   19.0   95661   709936      2946    1980    280 35473    4    58   50   7%      1   57    5    0 1268%
c i   19.2   95628   709936      3049    2055    293 35486    4    60   50   7%      1   58    5    0 1311%
c 
c [simplification-5] limit 3163 conflicts (hard 13047) hit after 3163 conflicts
c [quatres-1] found 38626 quaternary clauses 40% in total
c [quatres-1-2] added 2 single-self-subsuming ternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 95620 free variables schedulable
c [ternres-1] 21 ternary resolvents (0 bin, 21 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 89 xors of average arity 2.6
c [gauss-1] connected 228 occurrences of 206 variables (average 1.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 104 variables
c [gauss-1] exported 1 unary, 0 binary and 0 ternary equations
c [unhide-5] limit 243767 with penalty 0 = 0 + 0
c [unhide-5-5] 7 units, 438 failed, 13663 tauts, 0 hbrs, 1720 literals
c [transred-1] limit 1218838 with penalty 0 = 0 + 0
c [transred-1] removed 106 transitive binary clauses
c [transred-1] found 4 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 94998 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 10284 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 7 clauses out of 215 (3%) of length 10
c [cce-1-1] eliminated 121 clauses out of 2063 (6%) of length 9
c [cce-1-1] eliminated 16 clauses out of 444 (4%) of length 8
c [cce-1-1] eliminated 13 clauses out of 934 (1%) of length 7
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 157 large clauses in 30000001 steps
c [cce-1-1] allowing another 15000000 steps for small clauses
c [cce-1-1] scheduling 537990 clauses = 311825 binary + 226165 ternary
c [cce-1-1] tried to eliminate 296 small clauses 0%
c [cce-1-1] eliminated 56 binary clauses 0%
c [cce-1-1] eliminated 36 ternary clauses 0%
c [cce-1-1] eliminated 92 small clauses 0%
c [cce-1-1] eliminated 92 small clauses in 30000003 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 249 covered clauses in round 1
c [cce-1] eliminated 249 covered clauses in TOTAL during 1 rounds
c [cce-1] 249 < 1/100 * 665606 = 6656 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 94998 variables 100%
c [elim-5] limit of 24376774 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 19694 not tried 21% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2484 = 3% variables out of 94998 scheduled
c [bca-1] limit of 10000000 steps and 1317796 added (scaled 2)
c [bca-1] 170416 out of 185030 literals actually usable 92%
c [bca-1] added 1119 blocked clauses in 515464 steps
c [sweep-1] limit 1317296 based on 658648 irredundant clauses
c [sweep-1-1] 6424 pos 6.9% + 86090 neg 93.1% = 92514 sched 100.0% ret 0
c [sweep-1-1] 1355722 steps 19 queries 28202.63 avg class size
c [sweep-1-1] 204 decisions 14 SAT calls 79.50 avg env size
c [sweep-1-1] 92436 variables remain 100% (78 retained 0%)
c [decomp-11] removed 9 variables
c [sweep-1-1] removed 9 vars (0 failed, 4 eqs, 9 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 9 vars in TOTAL (1 rounds, 18 queries)
c [phase-count-5] 652431 negative 99.1% of 658628 except 6197 0.9%
c [phase-count-5] 538536 positive 81.8% of 658628 except 120092 18.2%
c [phase-count-5] less non-negative clauses 6197 than limit 65800 (10.0%)
c [phase-count-5] non-pos/non-neg = 120092/6197 = 19.38 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 1907 negative 100%
c [sort-queue-5] sorted 92505 enqueued variables after 3163 conflicts
c [score-dist-5] active 0 (0%), one 34576 (37%), zero 57929 (63%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 3115 variables 3.3% (92505 remain 38%)
c [simplification-5] removed 51308 irredundant clauses 7.2% (658628 remain 48%)
c [simplification-5] maximum reduction of 7% = max (3%, 7%)
c [simplification-5] large reduction 7% >= 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 15163 (soft 5163 + delta 10000)
c [simplification-5] new conflict limit 5163 (hard 15163)
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   24.6   92504   658628      3287    2026    378 46474    4    66   48   7%      1   64    7    0 1686%
c i   24.6   92497   658628      3294    2030    378 46476    4    66   48   7%      1   64    7    0 1668%
c i   24.8   92493   658628      3415    2117    389 46492    5    71   48   6%      1   69    8    0 1816%
c i   24.9   92490   658628      3493    2182    394 46498    5    71   48   6%      1   69    8    0 1777%
c i   24.9   92487   658628      3503    2190    395 46498    5    71   48   7%      1   69    8    0 1782%
c i   25.0   92486   658628      3623    2282    406 46511    5    72   48   7%      1   70    8    0 1815%
c i   25.0   92327   658628      3646    2302    406 46512    5    73   48   7%      1   70   10    0 2127%
c i   25.1   92322   658627      3659    2311    409 46512    5    73   48   7%      1   70   10    0 2162%
c i   25.1   92319   658627      3660    2311    409 46512    5    73   48   7%      1   70   10    0 2154%
c i   25.2   92316   658627      3743    2357    424 46526    5    73   48   7%      1   71    9    0 1898%
c i   25.2   92315   658627      3744    2357    424 46526    5    73   48   7%      1   71    9    0 1891%
c i   25.3   92310   658627      3837    2428    432 46537    5    76   48   7%      1   73    9    0 1950%
c i   25.3   92184   658627      3871    2456    433 46540    5    76   48   7%      1   73    9    0 1862%
c i   25.5   92181   658627      3987    2546    441 46552    5    77   48   7%      1   74    9    1 1702%
c i   25.5   92180   658627      3988    2546    441 46552    5    77   48   7%      1   74    9    1 1695%
c i   25.5   92175   658627      3989    2546    441 46552    5    77   48   7%      1   74    8    1 1689%
c i   25.7   92174   658627      4160    2666    457 46581    5    80   48   7%      1   77    8    1 1496%
c i   25.7   91670   658627      4173    2676    458 46582    5    79   48   7%      1   76    8    1 1476%
c i   25.8   91668   658627      4205    2702    460 46585    5    80   48   7%      1   77    8    1 1517%
c i   25.9   91654   658627      4325    2792    470 46602    6    81   48   7%      1   77   11    1 2056%
c i   26.0   91642   658627      4425    2871    477 46612    6    82   48   7%      1   78   13    1 2206%
c i   26.1   91633   658627      4480    2913    479 46621    6    82   48   7%      1   79   11    1 1961%
c i   26.1   91625   658627      4481    2913    479 46621    6    82   48   7%      1   79   11    1 1954%
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   26.1   91619   658627      4489    2918    480 46622    6    82   48   7%      1   79   11    1 1913%
c i   26.3   91602   658627      4676    3065    495 46640    6    86   48   7%      1   82   10    1 1621%
c i   26.4   91598   658627      4729    3099    501 46650    6    86   48   7%      1   82    9    1 1481%
c i   26.4   91574   658627      4737    3103    503 46651    6    86   48   7%      1   82    9    1 1449%
c i   26.4   91565   658627      4740    3105    503 46651    6    86   48   7%      1   82    9    1 1442%
c i   26.6   91441   658627      4854    3183    515 46671    6    86   48   7%      1   82   10    1 1536%
c i   26.8   91434   658627      5047    3323    525 46709    7    87   49   8%      1   83   14    1 2073%
c i   26.8   91429   658627      5048    3323    525 46709    7    87   49   8%      1   83   14    1 2064%
c i   26.9   91416   658627      5190    3419    537 46739    7    89   49   7%      1   84   11    1 1661%
c i   26.9   91307   658627      5191    3419    537 46739    7    89   49   7%      1   84   11    1 1654%
c i   26.9   91301   658627      5192    3419    537 46739    7    89   49   7%      1   84   11    1 1648%
c 
c [simplification-6] limit 5250 conflicts (hard 15163) hit after 5253 conflicts
c [quatres-2] found 40048 quaternary clauses 41% in total
c [quatres-2-2] added 4 single-self-subsuming ternary resolvents
c [quatres-2-2] added 2 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 91301 free variables schedulable
c [ternres-2] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-2] 66166 variables remain 72% (25135 retained 28%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2213 at-most-one constraints of average size 4.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2213 out of 2213 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 167 xors of average arity 2.4
c [gauss-2] connected 404 occurrences of 198 variables (average 2.0)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 75 variables
c [simpleprobe-3] 12896 schedulable variables 14%
c [simpleprobe-3] limit 3949252 penalty 1 = 1 + 0
c [decomp-13] removed 4 variables
c [simpleprobe-3] 13191 variables remain 14% (78031 retained 86%)
c [simpleprobe-3] removed 4 variables, found 5261 hbrs, 2 units
c [unhide-6] limit 394925 with penalty 0 = 0 + 0
c [unhide-6-6] 19 units, 564 failed, 6314 tauts, 0 hbrs, 3214 literals
c [transred-2] limit 1974626 with penalty 0 = 0 + 0
c [transred-2] removed 193 transitive binary clauses
c [transred-2] found 3 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 90459 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 7 blocked clauses
c [block-2] 7 < 1/100 * 650706 = 6507 considered unsuccessful
c [elim-6] 19635 variables 22% will be scheduled this time
c [elim-6] scheduled 19635 variables 22%
c [elim-6] limit of 39492525 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 39009157 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 19635 scheduled
c [bca-2] limit of 10000000 steps and 1282403 added (scaled 2)
c [bca-2] 162553 out of 180920 literals actually usable 90%
c [bca-2] added 97 blocked clauses in 484221 steps
c [sweep-2] limit 1281344 based on 640672 irredundant clauses
c [sweep-2-1] 6968 pos 7.7% + 83420 neg 92.3% = 90388 sched 99.9% ret 71
c [sweep-2-1] 1441754 steps 18 queries 14832.94 avg class size
c [sweep-2-1] 258 decisions 14 SAT calls 69.50 avg env size
c [sweep-2-1] 90183 variables remain 100% (178 retained 0%)
c [decomp-14] removed 160 variables
c [sweep-2-1] removed 160 vars (0 failed, 3 eqs, 4 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 160 vars in TOTAL (1 rounds, 17 queries)
c [phase-count-6] 633784 negative 99.0% of 639967 except 6183 1.0%
c [phase-count-6] 523387 positive 81.8% of 639967 except 116580 18.2%
c [phase-count-6] less non-negative clauses 6183 than limit 63900 (10.0%)
c [phase-count-6] non-pos/non-neg = 116580/6183 = 18.85 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 1873 negative 100%
c [sort-queue-6] sorted 90299 enqueued variables after 5253 conflicts
c [score-dist-6] active 0 (0%), one 35825 (40%), zero 54474 (60%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 1002 variables 1.1% (90299 remain 37%)
c [simplification-6] removed 18660 irredundant clauses 2.8% (639967 remain 47%)
c [simplification-6] maximum reduction of 3% = max (1%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 5000
c [simplification-6] penalized conflict interval 5000 = 1 * 5000
c [simplification-6] hard conflict limit 20253 (soft 10253 + delta 10000)
c [simplification-6] new conflict limit 10253 (hard 20253)
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   30.9   90298   639967      5278    3411    522 47864    7    92   48   7%      1   87   12    1 1647%
c i   30.9   90291   639967      5286    3417    522 47865    7    92   48   7%      1   88   11    1 1617%
c i   30.9   90178   639967      5311    3433    527 47868    7    92   48   7%      1   88   11    1 1513%
c i   31.0   90166   639967      5346    3450    534 47876    7    92   48   7%      1   87   10    1 1405%
c i   31.1   90133   639967      5371    3465    538 47879    7    92   48   7%      1   87    9    1 1330%
c i   31.2   89764   639967      5446    3518    546 47888    7    92   48   7%      1   87   10    1 1424%
c i   31.2   89761   639967      5450    3519    547 47889    7    92   48   7%      1   87   10    1 1404%
c i   31.2   89481   639967      5472    3534    549 47893    7    92   48   7%      1   87   11    1 1451%
c i   31.3   89473   639967      5503    3557    552 47897    7    94   48   7%      1   89   10    1 1388%
c i   31.3   89463   639967      5515    3562    556 47899    7    94   48   7%      1   89   11    1 1450%
c i   31.4   89370   639967      5538    3573    560 47906    7    94   48   7%      1   89   10    1 1358%
c i   31.7   89362   639967      5636    3640    574 47921    7    97   48   7%      1   92   10    1 1311%
c i   31.7   89162   639967      5662    3655    575 47927    7    97   48   7%      1   92   10    1 1344%
c i   31.7   89124   639967      5701    3683    580 47932    7    97   48   7%      1   92   10    1 1329%
c i   31.8   89115   639967      5726    3705    580 47934    7    97   48   7%      1   92   10    1 1276%
c i   31.9   89112   639967      5788    3761    582 47936    7    98   48   7%      1   93   11    1 1376%
c i   31.9   89107   639967      5839    3806    584 47939    7   100   48   7%      1   95   11    1 1381%
c i   31.9   89100   639967      5842    3807    584 47940    7   100   48   7%      1   95   11    1 1450%
c i   32.2   89099   639967      5974    3914    595 47952    7   102   48   7%      1   97   11    1 1432%
c i   32.3   88956   639967      6033    3966    595 47957    7   103   48   7%      1   97   13    1 1557%
c i   32.4   88948   639967      6178    4093    603 47962    8   102   48   8%      1   97   16    1 1880%
c i   32.5   88945   639967      6219    4124    606 47967    8   104   48   8%      1   99   15    1 1749%
c i   32.6   88942   639967      6301    4174    613 47974    8   106   48   8%      1  100   17    1 1905%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   32.7   88939   639967      6369    4220    620 47986    8   106   48   8%      1  100   15    1 1660%
c i   32.7   88938   639967      6416    4261    621 47990    8   107   48   8%      1  101   15    1 1610%
c i   32.7   88937   639967      6417    4261    621 47990    8   106   48   8%      1  101   15    1 1604%
c i   32.8   88935   639967      6458    4293    624 47994    8   107   48   8%      1  101   15    1 1623%
c i   33.0   88930   639967      6608    4418    631 48009    9   110   48   8%      1  103   15    1 1624%
c i   33.0   88929   639967      6636    4433    635 48016    9   110   48   8%      1  104   15    1 1548%
c i   33.1   88923   639967      6697    4478    639 48027    9   112   48   8%      1  106   13    1 1380%
c i   33.3   88920   639967      6807    4565    647 48041    9   112   48   8%      1  105   12    1 1208%
c i   33.3   88919   639967      6848    4595    652 48044    9   112   48   8%      1  105   11    1 1167%
c i   33.4   88918   639967      6943    4671    664 48049    9   111   48   8%      1  104   10    1 1040%
c i   33.7   88917   639967      7182    4866    689 48066    9   113   48   8%      1  105   12    1 1135%
c i   33.8   88876   639967      7260    4925    697 48070    9   112   48   8%      1  105   15    1 1380%
c i   33.8   88871   639967      7296    4953    700 48074    9   113   48   8%      1  106   13    1 1260%
c i   33.8   88817   639967      7297    4953    700 48074    9   113   48   8%      1  106   13    1 1255%
c i   33.9   88816   639967      7421    5060    705 48084    9   114   48   8%      1  107   17    1 1564%
c i   33.9   88815   639967      7422    5060    705 48084    9   114   48   8%      1  107   17    1 1558%
c i   34.2   88812   639967      7752    5352    714 48102   10   117   48   9%      1  109   19    1 1559%
c i   34.3   88805   639967      7790    5383    720 48102   10   118   48   9%      1  109   18    1 1471%
c i   34.4   88804   639967      7949    5510    729 48120   10   117   48   9%      1  109   15    1 1209%
c i   34.4   88752   639967      7950    5510    729 48120   10   117   48   9%      1  109   15    1 1204%
c i   34.5   88742   639967      8005    5544    739 48128   10   117   48   9%      1  109   13    1 1050%
c i   34.5   88737   639967      8039    5568    741 48133   10   117   48   9%      1  109   14    1 1127%
c i   34.6   88681   639967      8126    5640    747 48139   10   117   48   9%      1  108   13    1 1004%
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   34.7   88544   639967      8226    5728    752 48145   10   119   48   9%      1  110   15    1 1162%
c i   35.0   88540   639967      8639    6072    777 48163   11   120   49   9%      2  111   18    1 1285%
c i   35.1   88534   639967      8648    6078    777 48165   11   121   49   9%      2  111   18    1 1266%
c i   35.1   88530   639967      8672    6097    778 48167   11   120   49   9%      2  111   17    1 1195%
c i   35.2   88528   639967      8744    6153    782 48174   11   121   49   9%      2  111   16    1 1122%
c i   35.4   88525   639967      8871    6254    792 48187   11   122   49   9%      2  112   14    1 1013%
c i   35.4   88523   639967      8898    6271    796 48190   12   121   49   9%      2  111   15    1 1072%
c i   35.5   88193   639967      8940    6296    800 48199   11   121   49   9%      2  111   14    1  982%
c i   35.6   88192   639967      8983    6330    801 48205   11   122   49   9%      1  112   13    1  889%
c i   35.9   88186   639967      9164    6489    811 48215   11   126   49   9%      1  116   13    1  851%
c i   35.9   88180   639967      9165    6489    811 48215   11   126   49   9%      1  116   13    1  848%
c i   36.0   88129   639967      9253    6551    814 48234   12   127   49   9%      1  117   14    1  913%
c i   36.2   88124   639967      9396    6663    824 48253   12   127   49   9%      1  116   12    2  792%
c i   36.4   88118   639967      9501    6747    831 48265   12   128   49   9%      1  117   15    2  990%
c i   36.4   88115   639967      9557    6786    836 48274   12   128   49   9%      1  117   14    2  896%
c i   36.6   88102   639967      9654    6868    841 48283   12   130   49   9%      1  119   20    2 1259%
c i   36.6   88096   639967      9682    6886    845 48287   12   130   49   9%      1  119   19    2 1198%
c i   37.1   87983   639967      9945    7090    867 48316   13   133   49   9%      1  122   18    2 1088%
c i   37.1   87979   639967      9953    7095    868 48317   13   133   49   9%      1  121   18    2 1065%
c i   37.2   87978   639967     10005    7141    870 48320   13   135   49   9%      1  123   17    2 1016%
c i   37.2   87969   639967     10034    7166    872 48320   13   134   49   9%      1  122   16    2  962%
c i   37.2   87966   639967     10046    7176    873 48320   13   134   49   9%      1  122   16    2  926%
c i   37.2   87959   639967     10054    7179    874 48322   12   134   49   9%      1  122   15    2  904%
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   37.3   87946   639967     10080    7191    881 48327   12   134   49   9%      1  122   14    2  836%
c i   37.5   87865   639967     10157    7253    886 48335   12   135   49   9%      1  122   14    2  810%
c i   37.5   87861   639967     10176    7265    887 48340   12   135   49   9%      1  122   13    2  773%
c i   37.5   87826   639967     10184    7270    888 48341   12   134   49   9%      1  122   13    2  760%
c i   37.5   87816   639967     10185    7270    888 48341   12   134   49   9%      1  122   13    2  757%
c i   37.6   87814   639967     10228    7300    892 48348   12   135   49   9%      1  122   14    2  825%
c i   37.6   87653   639967     10247    7314    894 48349   12   134   49   9%      1  122   14    2  821%
c i   37.6   87652   639967     10248    7314    894 48349   12   134   49   9%      1  122   14    2  818%
c 
c [simplification-7] limit 10333 conflicts (hard 20253) hit after 10333 conflicts
c [quatres-3] found 33160 quaternary clauses 40% in total
c [quatres-3-2] added 3 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 63519 schedulable variables 70%
c [ternres-3] 12 ternary resolvents (0 bin, 12 trn)
c [ternres-3] 38535 variables remain 44% (49113 retained 56%)
c [decomp-15] removed 3492 variables
c [treelook-3] limit 387789 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 52318 literals 30%
c [treelook-3] scheduling used 438106 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 387789 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 557034 steps
c [treelook-3] 52300 literals remain 30%
c [treelook-3] 38935 variables remain to probed next time 45%
c [treelook-3] removed 13 variables, found 4108 hbrs
c [unhide-7] limit 775578 with penalty 0 = 0 + 0
c [unhide-7-7] 29 units, 378 failed, 11059 tauts, 0 hbrs, 9009 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 162 transitive binary clauses
c [transred-3] found 12 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 7500001 steps for small clauses
c [cce-2-1] scheduling 496868 clauses = 285542 binary + 211326 ternary
c [cce-2-1] tried to eliminate 145 small clauses 0%
c [cce-2-1] eliminated 24 binary clauses 0%
c [cce-2-1] eliminated 7 ternary clauses 0%
c [cce-2-1] eliminated 31 small clauses 0%
c [cce-2-1] eliminated 6228 small clauses in 15000020 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 6228 covered clauses in round 1
c [cce-2] eliminated 6228 covered clauses in TOTAL during 1 rounds
c [bca-3] limit of 10000000 steps and 1216778 added (scaled 2)
c [bca-3] 148342 out of 172236 literals actually usable 86%
c [bca-3] added 56 blocked clauses in 425868 steps
c [sweep-3] limit 1215670 based on 607835 irredundant clauses
c [sweep-3-1] 6297 pos 7.3% + 79658 neg 92.7% = 85955 sched 99.8% ret 162
c [sweep-3-1] 1496126 steps 12 queries 13377.58 avg class size
c [sweep-3-1] 154 decisions 8 SAT calls 138.00 avg env size
c [sweep-3-1] 85922 variables remain 100% (187 retained 0%)
c [decomp-17] removed 147 variables
c [sweep-3-1] removed 147 vars (0 failed, 3 eqs, 5 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 147 vars in TOTAL (1 rounds, 11 queries)
c [phase-count-7] 601065 negative 99.0% of 607198 except 6133 1.0%
c [phase-count-7] 498705 positive 82.1% of 607198 except 108493 17.9%
c [phase-count-7] less non-negative clauses 6133 than limit 60700 (10.0%)
c [phase-count-7] non-pos/non-neg = 108493/6133 = 17.69 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 585 negative 100%
c [sort-queue-7] sorted 85970 enqueued variables after 10333 conflicts
c [score-dist-7] active 0 (0%), one 41833 (49%), zero 44137 (51%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 1678 variables 1.9% (85970 remain 35%)
c [simplification-7] removed 32769 irredundant clauses 5.1% (607198 remain 45%)
c [simplification-7] maximum reduction of 5% = max (2%, 5%)
c [simplification-7] large reduction 5% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 22333 (soft 12333 + delta 10000)
c [simplification-7] new conflict limit 12333 (hard 22333)
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   40.7   85969   607198     10335    7256    854 51695   12   135   47   9%      1  122   13    2  771%
c i   40.7   85936   607198     10343    7262    854 51696   12   136   48   9%      1  123   13    2  762%
c i   40.8   85832   607198     10360    7278    854 51696   12   136   48   9%      1  124   13    2  741%
c i   40.8   85831   607198     10361    7278    854 51696   12   136   48   9%      1  124   13    2  738%
c i   40.9   85823   607198     10451    7357    857 51700   12   136   48   9%      1  123   12    2  672%
c i   41.3   85820   607198     10747    7584    882 51734   12   138   49   9%      1  125   12    2  693%
c i   41.4   85817   607198     10835    7658    885 51742   13   140   49   9%      1  127   15    2  841%
c i   41.6   85815   607198     10961    7771    888 51748   13   140   49   9%      1  127   16    2  844%
c i   41.6   85812   607198     10975    7782    889 51749   13   140   49   9%      1  126   15    2  835%
c i   41.6   85804   607198     10980    7786    889 51749   13   140   49   9%      1  127   15    2  822%
c i   41.6   85798   607198     10992    7797    889 51749   13   141   49   9%      1  127   16    2  856%
c i   41.7   85796   607198     11070    7862    893 51754   13   143   49   9%      1  129   15    2  823%
c i   41.8   85795   607198     11092    7881    894 51755   13   143   49   9%      1  129   15    2  814%
c i   41.8   85790   607198     11116    7898    896 51758   13   142   49   9%      1  128   15    2  815%
c i   41.8   85789   607198     11117    7898    896 51758   13   142   49   9%      1  128   15    2  812%
c i   41.8   85788   607198     11121    7899    898 51758   13   142   49   9%      1  128   15    2  802%
c i   41.9   85787   607198     11178    7948    899 51764   13   142   49   9%      1  128   15    2  817%
c i   41.9   85786   607198     11197    7962    899 51768   13   142   49   9%      1  128   15    2  808%
c i   42.0   85785   607198     11280    8034    901 51776   13   144   49   9%      1  130   16    2  834%
c i   42.4   85782   607198     11566    8255    928 51799   13   149   49   9%      1  134   14    2  707%
c i   42.8   85776   607198     11755    8404    943 51820   13   155   49   9%      1  139   16    2  787%
c i   42.9   85768   607198     11794    8436    947 51822   13   155   49   9%      1  139   17    2  848%
c i   43.0   85762   607198     11836    8469    950 51825   13   155   49   9%      1  140   16    2  790%
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   43.2   85757   607198     11944    8555    955 51835   14   156   49   9%      1  140   20    2  961%
c i   43.4   85756   607198     12060    8651    961 51844   14   155   49   9%      1  139   23    2 1077%
c i   43.4   85751   607198     12076    8666    961 51844   14   155   49   9%      1  139   23    2 1075%
c i   43.4   85744   607198     12077    8666    961 51844   14   155   49   9%      1  139   23    2 1071%
c i   43.4   85727   607198     12100    8681    964 51844   14   155   49   9%      1  139   24    2 1139%
c i   43.7   85722   607198     12231    8777    973 51864   14   156   49   9%      1  140   20    2  945%
c i   43.7   85716   607198     12278    8809    981 51869   14   155   49   9%      1  139   18    2  847%
c 
c [simplification-8] limit 12368 conflicts (hard 22333) hit after 12368 conflicts
c [quatres-4] found 34457 quaternary clauses 40% in total
c [quatres-4-2] added 1 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1 quaternary resolvents
c [ternres-4] limit 4756452 with penalty 0 = 0 + 0
c [ternres-4] 37687 schedulable variables 44%
c [ternres-4] 22 ternary resolvents (0 bin, 22 trn)
c [ternres-4] 7876 variables remain 9% (77827 retained 91%)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 190 xors of average arity 2.5
c [gauss-3] connected 476 occurrences of 362 variables (average 1.3)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-18] removed 121 variables
c [basicprobe-3] limit 23782262 penalty 0 = 0 + 0
c [basicprobe-3-0] 27835 probes remain 33% after last round
c [basicprobe-3-0] 118 units = 118 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 878 variables, found 82397 hbrs
c [bate-1] eliminated 73 asymmetric tautologies during probing
c [unhide-8] limit 951290 with penalty 0 = 0 + 0
c [unhide-8-8] 18 units, 655 failed, 16305 tauts, 0 hbrs, 13961 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 205 transitive binary clauses
c [transred-4] found 9 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 83975 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 35 blocked clauses
c [block-3] 35 < 1/100 * 598257 = 5982 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 1311 (0%) of length 9
c [cce-3-1] eliminated 45 clauses out of 766 (6%) of length 7
c [cce-3-1] eliminated 2756 clauses out of 5172 (53%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 2802 large clauses in 30000003 steps
c [cce-3-1] allowing another 15000001 steps for small clauses
c [cce-3-1] scheduling 483637 clauses = 282121 binary + 201516 ternary
c [cce-3-1] tried to eliminate 354 small clauses 0%
c [cce-3-1] eliminated 76 binary clauses 0%
c [cce-3-1] eliminated 28 ternary clauses 0%
c [cce-3-1] eliminated 104 small clauses 0%
c [cce-3-1] eliminated 104 small clauses in 30000018 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 2906 covered clauses in round 1
c [cce-3] eliminated 2906 covered clauses in TOTAL during 1 rounds
c [cce-3] 2906 < 1/100 * 590724 = 5907 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 83974 variables 100%
c [elim-7] limit of 47564524 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 2801 not tried 3% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 3545 = 4% variables out of 83974 scheduled
c [bca-4] limit of 10000000 steps and 1159098 added (scaled 2)
c [bca-4] 139288 out of 160860 literals actually usable 87%
c [bca-4] added 249 blocked clauses in 400865 steps
c [sweep-4] limit 1426935 penalty 0 = 0 + 0
c [sweep-4-1] 5971 pos 7.4% + 74306 neg 92.6% = 80277 sched 99.8% ret 152
c [sweep-4-1] 2146582 steps 14 queries 23083.50 avg class size
c [sweep-4-1] 136 decisions 11 SAT calls 183.27 avg env size
c [sweep-4-1] 80235 variables remain 100% (192 retained 0%)
c [decomp-19] removed 33 variables
c [sweep-4-1] removed 33 vars (0 failed, 2 eqs, 8 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 33 vars in TOTAL (1 rounds, 13 queries)
c [phase-count-8] 576372 negative 99.6% of 578903 except 2531 0.4%
c [phase-count-8] 471463 positive 81.4% of 578903 except 107440 18.6%
c [phase-count-8] less non-negative clauses 2531 than limit 57800 (10.0%)
c [phase-count-8] non-pos/non-neg = 107440/2531 = 42.45 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 446 negative 100%
c [sort-queue-8] sorted 80396 enqueued variables after 12368 conflicts
c [score-dist-8] active 0 (0%), one 42086 (52%), zero 38310 (48%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 5307 variables 6.2% (80396 remain 33%)
c [simplification-8] removed 28295 irredundant clauses 4.7% (578903 remain 43%)
c [simplification-8] maximum reduction of 6% = max (6%, 5%)
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 24368 (soft 14368 + delta 10000)
c [simplification-8] new conflict limit 14368 (hard 24368)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   50.1   80395   578903     12387    6686    954 102682   14   158   47   9%      1  142   19    2  862%
c i   50.4   80383   578903     12651    6912    961 102701   15   159   47   9%      1  142   20    2  889%
c i   50.4   80375   578903     12667    6925    961 102702   15   159   47   9%      1  142   19    2  853%
c i   50.4   80369   578903     12702    6954    963 102704   15   159   47   9%      1  142   19    2  823%
c i   50.6   80365   578903     12843    7077    970 102711   15   163   47   9%      1  146   18    2  786%
c i   50.8   80360   578903     12955    7167    983 102717   15   163   47   9%      1  145   16    2  697%
c i   50.9   80359   578903     13102    7296    988 102722   15   164   47   9%      1  146   20    2  858%
c i   51.0   80354   578903     13160    7343    989 102727   15   164   47   9%      1  146   19    2  786%
c i   51.1   80343   578903     13172    7353    990 102727   15   164   47   9%      1  146   18    2  758%
c i   51.3   80340   578903     13380    7519   1006 102743   15   164   47   9%      1  145   18    2  743%
c i   51.4   80335   578903     13511    7628   1016 102749   15   163   47   9%      1  144   18    2  724%
c i   51.8   80330   578903     13882    7940   1035 102780   16   163   47  10%      2  143   20    3  794%
c i   52.1   80295   578903     14101    8126   1047 102799   16   163   47  10%      2  143   16    3  610%
c i   52.2   80230   578903     14131    8146   1052 102803   15   164   47   9%      2  143   15    3  564%
c i   52.2   80137   578903     14132    8146   1052 102803   15   164   47   9%      2  143   15    3  562%
c i   52.3   80131   578903     14238    8233   1059 102811   16   164   47   9%      1  143   16    3  611%
c 
c [simplification-9] limit 14378 conflicts (hard 24368) hit after 14378 conflicts
c [quatres-5] found 37294 quaternary clauses 45% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 3 single-self-subsuming ternary resolvents
c [quatres-5-2] added 4 quaternary resolvents
c [ternres-5] limit 5473470 with penalty 0 = 0 + 0
c [ternres-5] 7363 schedulable variables 9%
c [ternres-5] 82 ternary resolvents (0 bin, 82 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-20] removed 291 variables
c [simpleprobe-4] 12093 schedulable variables 15%
c [simpleprobe-4] limit 21893881 penalty 0 = 0 + 0
c [decomp-21] removed 131 variables
c [simpleprobe-4] 1582 variables remain 2% (78392 retained 98%)
c [simpleprobe-4] removed 131 variables, found 24106 hbrs, 47 units
c [unhide-9] limit 1094694 with penalty 0 = 0 + 0
c [unhide-9-9] 5 units, 152 failed, 11423 tauts, 0 hbrs, 8670 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 222 transitive binary clauses
c [transred-5] found 6 units
c [elim-8] 2764 variables 3% will be scheduled this time
c [elim-8] scheduled 2764 variables 3%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2189388140 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 7456220 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 2764 scheduled
c [bca-5] limit of 10000000 steps and 1127116 added (scaled 2)
c [bca-5] 135018 out of 159040 literals actually usable 85%
c [bca-5] added 116 blocked clauses in 384032 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 16420410 penalty 0 = 0 + 0
c [sweep-5-1] 6029 pos 7.6% + 73307 neg 92.4% = 79336 sched 99.8% ret 183
c [sweep-5-1] 16500866 steps 161 queries 3828.40 avg class size
c [sweep-5-1] 1209 decisions 136 SAT calls 105.10 avg env size
c [sweep-5-1] 73693 variables remain 93% (5796 retained 7%)
c [decomp-22] removed 77 variables
c [sweep-5-1] removed 77 vars (0 failed, 27 eqs, 54 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 77 vars in TOTAL (1 rounds, 160 queries)
c [phase-count-9] 559978 negative 99.5% of 562515 except 2537 0.5%
c [phase-count-9] 459428 positive 81.7% of 562515 except 103087 18.3%
c [phase-count-9] less non-negative clauses 2537 than limit 56200 (10.0%)
c [phase-count-9] non-pos/non-neg = 103087/2537 = 40.63 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 368 negative 100%
c [sort-queue-9] sorted 79442 enqueued variables after 14378 conflicts
c [score-dist-9] active 0 (0%), one 44356 (56%), zero 35086 (44%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 684 variables 0.9% (79442 remain 32%)
c [simplification-9] removed 16388 irredundant clauses 2.8% (562515 remain 41%)
c [simplification-9] maximum reduction of 3% = max (1%, 3%)
c [simplification-9] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-9] new conflict interval 10000
c [simplification-9] penalized conflict interval 10000 = 1 * 10000
c [simplification-9] hard conflict limit 34378 (soft 24378 + delta 10000)
c [simplification-9] new conflict limit 24378 (hard 34378)
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   56.4   79441   562515     14380    8351   1118 153415   15   167   47   9%      1  146   14    3  542%
c i   56.5   79438   562515     14510    8458   1125 153425   15   168   48   9%      1  147   14    3  513%
c i   56.5   79400   562515     14513    8460   1125 153425   15   168   48   9%      1  146   14    3  508%
c i   56.6   79393   562515     14536    8479   1126 153427   15   168   48   9%      1  146   13    3  484%
c i   56.8   79391   562515     14640    8566   1131 153433   15   169   48   9%      1  148   12    3  438%
c i   56.9   79366   562515     14739    8655   1134 153439   15   168   48   9%      1  146   12    3  446%
c i   57.0   79361   562515     14818    8714   1141 153448   15   170   48   9%      1  148   10    3  380%
c i   57.1   79291   562515     14859    8737   1148 153457   15   169   48   9%      1  147   10    3  384%
c i   57.2   79287   562515     14960    8819   1159 153463   15   170   48   9%      1  148   14    3  503%
c i   57.3   79277   562515     15022    8871   1162 153465   15   170   48   9%      1  148   14    3  508%
c i   57.4   79272   562515     15081    8912   1169 153470   15   170   48   9%      1  147   17    3  604%
c i   57.4   79271   562515     15082    8912   1169 153470   15   170   48   9%      1  147   17    3  601%
c i   57.5   79261   562515     15179    8999   1171 153476   15   170   48   9%      1  147   18    3  647%
c i   57.6   79206   562515     15257    9073   1171 153478   15   171   48   9%      1  148   20    3  706%
c i   57.8   79205   562515     15400    9204   1177 153483   16   173   48   9%      1  150   19    3  662%
c i   57.9   79203   562515     15432    9231   1178 153486   16   174   48   9%      1  150   18    3  638%
c i   58.1   79201   562515     15542    9317   1187 153495   16   174   48   9%      1  150   17    3  591%
c i   58.1   79194   562515     15552    9324   1189 153495   15   174   48   9%      1  150   16    3  574%
c i   58.1   79189   562515     15556    9326   1190 153495   15   174   48   9%      1  150   16    3  567%
c i   58.2   79180   562515     15591    9356   1193 153496   15   174   48   9%      1  150   15    3  531%
c i   58.2   79063   562515     15628    9383   1198 153500   15   173   48   9%      1  149   14    3  477%
c i   58.2   79058   562515     15644    9394   1199 153503   15   172   48   9%      1  149   13    3  460%
c i   58.3   79052   562515     15710    9439   1210 153512   15   171   48   9%      1  147   11    3  383%
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   58.5   79043   562515     15814    9520   1222 153521   15   171   48   9%      1  147    9    3  315%
c i   58.6   79035   562515     15848    9541   1228 153527   15   171   48   9%      1  147    8    3  293%
c i   58.8   79026   562515     15988    9668   1234 153530   15   171   48   9%      1  146   13    3  460%
c i   59.5   79025   562515     16671   10247   1262 153570   15   170   48   9%      3  144   16    3  531%
c i   60.3   79017   562515     17230   10738   1300 153590   16   179   48   9%      4  151   22    3  696%
c i   60.3   79010   562515     17251   10758   1300 153590   16   179   48   9%      4  151   23    3  705%
c i   60.3   78996   562515     17300   10803   1303 153590   16   178   48   9%      3  150   22    3  675%
c i   60.4   78982   562515     17326   10822   1305 153593   16   177   48   9%      3  150   21    3  641%
c i   60.4   78981   562515     17365   10855   1308 153594   16   178   48   9%      3  150   21    3  642%
c i   60.5   78973   562515     17373   10862   1308 153594   16   178   48   9%      3  150   20    3  628%
c i   60.6   78970   562515     17429   10906   1312 153600   16   179   49   9%      3  151   22    3  680%
c i   60.6   78967   562515     17432   10908   1312 153600   16   179   49   9%      3  151   22    3  678%
c i   60.6   78959   562515     17476   10944   1313 153606   16   178   49   9%      3  150   21    3  640%
c i   60.8   78829   562515     17608   11062   1318 153610   16   177   49   9%      3  149   21    3  638%
c i   60.9   78824   562515     17610   11063   1318 153610   16   177   49   9%      3  149   21    3  634%
c i   60.9   78796   562515     17614   11066   1318 153610   16   177   49   9%      3  149   21    3  625%
c i   60.9   78789   562515     17619   11069   1318 153611   16   177   49   9%      3  149   20    3  617%
c i   61.4   78786   562515     17994   11405   1327 153626   17   178   49  10%      3  149   24    3  692%
c i   61.6   78781   562515     18109   11514   1329 153627   17   178   49  10%      2  148   23    3  673%
c i   61.9   78780   562515     18339   11709   1337 153645   17   182   49   9%      2  152   18    3  503%
c i   62.0   78775   562515     18377   11738   1339 153651   17   183   49   9%      2  153   16    4  471%
c i   62.1   78767   562515     18442   11794   1343 153652   17   184   49   9%      2  154   20    4  556%
c i   62.2   78749   562515     18447   11798   1343 153652   17   184   49   9%      2  154   19    4  552%
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   62.2   78747   562515     18458   11803   1343 153652   17   184   49   9%      2  154   19    4  544%
c i   62.2   78745   562515     18467   11807   1345 153654   17   183   49   9%      2  153   19    4  529%
c i   62.4   78741   562515     18633   11958   1353 153658   17   182   49   9%      2  151   17    4  490%
c i   62.5   78737   562515     18718   12026   1359 153666   18   184   49  10%      2  153   23    4  631%
c i   62.7   78736   562515     18837   12132   1366 153671   18   185   49  10%      2  154   22    4  600%
c i   62.9   78732   562515     19024   12296   1375 153677   18   183   49  10%      2  151   21    4  567%
c i   63.0   78729   562515     19109   12370   1380 153681   18   181   49  10%      1  149   22    4  590%
c i   63.2   78727   562515     19242   12483   1387 153691   18   181   50  10%      1  149   25    4  673%
c i   63.4   78726   562515     19414   12631   1392 153700   18   180   50  10%      1  147   24    4  632%
c i   63.4   78722   562515     19444   12654   1397 153701   18   181   50  10%      1  148   23    4  598%
c i   63.5   78721   562515     19486   12686   1400 153705   18   180   50  10%      1  148   21    4  544%
c i   63.5   78720   562515     19487   12686   1400 153705   18   180   50  10%      1  148   21    4  542%
c i   63.7   78717   562515     19585   12765   1408 153715   18   182   50  10%      1  149   20    4  520%
c i   63.7   78629   562515     19589   12767   1408 153716   18   182   50  10%      1  149   20    4  514%
c i   63.7   78620   562515     19592   12767   1408 153718   18   182   50  10%      1  149   19    4  508%
c i   63.8   78614   562515     19639   12797   1413 153728   18   181   50  10%      1  149   17    4  446%
c i   64.4   78612   562515     20109   13207   1438 153748   19   183   50  10%      2  149   24    4  598%
c i   64.6   78595   562515     20236   13307   1445 153765   19   183   50  10%      2  148   22    4  559%
c i   64.6   78594   562515     20237   13307   1445 153765   19   183   50  10%      2  148   22    4  557%
c i   64.7   78590   562515     20289   13349   1448 153769   19   182   50  10%      2  148   21    4  512%
c i   64.7   78589   562515     20290   13349   1448 153769   19   182   50  10%      2  148   21    4  510%
c i   65.0   78580   562515     20432   13480   1453 153774   19   185   50  10%      2  150   20    4  501%
c i   65.1   78579   562515     20501   13538   1456 153779   19   186   50  10%      2  151   20    4  488%
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   65.2   78575   562515     20551   13580   1461 153781   19   186   50  10%      1  151   19    4  473%
c i   65.4   78573   562515     20711   13716   1468 153793   19   186   50  10%      1  151   19    4  458%
c i   65.6   78561   562515     20892   13871   1479 153801   19   186   51  10%      1  150   22    4  517%
c i   66.4   78560   562515     21327   14238   1506 153828   19   192   51  10%      2  155   23    4  534%
c i   66.4   78555   562515     21331   14240   1507 153828   19   191   51  10%      2  155   23    4  527%
c i   66.8   78551   562515     21666   14542   1522 153838   19   190   51  10%      2  152   19    4  430%
c i   67.0   78550   562515     21802   14661   1526 153843   20   191   51  11%      2  153   27    4  597%
c i   67.1   78507   562515     21821   14677   1527 153844   20   191   51  10%      2  153   25    4  571%
c i   67.1   78506   562515     21829   14684   1527 153844   20   191   51  10%      2  153   25    4  559%
c i   67.3   78411   562515     22023   14855   1535 153850   20   189   51  11%      2  151   24    5  525%
c i   67.5   78407   562515     22114   14939   1535 153855   21   189   51  11%      2  151   28    5  622%
c i   67.6   78404   562515     22188   15008   1535 153855   21   191   51  11%      1  153   32    5  693%
c i   67.6   78403   562515     22211   15028   1535 153855   21   192   52  11%      1  153   36    5  784%
c i   67.7   78402   562515     22264   15073   1539 153858   21   193   52  11%      1  154   34    5  730%
c i   68.2   78393   562515     22581   15355   1553 153873   22   195   52  11%      2  155   28    5  591%
c i   68.3   78387   562515     22638   15399   1555 153880   22   195   52  11%      2  156   26    5  557%
c i   68.3   78382   562515     22671   15429   1557 153880   22   195   52  11%      1  156   29    5  607%
c i   68.7   78381   562515     22925   15658   1570 153888   22   197   52  11%      1  157   29    5  592%
c i   68.9   78375   562515     23026   15743   1572 153897   22   197   52  11%      1  157   28    5  573%
c i   69.3   78329   562515     23290   15964   1587 153918   22   200   52  11%      1  158   27    5  535%
c i   69.4   78321   562515     23349   16007   1592 153926   22   199   52  11%      1  158   24    5  477%
c i   69.7   78319   562515     23520   16154   1598 153937   22   199   52  11%      1  157   24    5  468%
c i   69.7   78314   562515     23530   16162   1598 153938   22   199   52  11%      1  157   24    5  487%
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   78306   562515     23531   16162   1598 153938   22   198   52  11%      1  157   24    5  485%
c i   69.7   78300   562515     23532   16162   1598 153938   22   198   52  11%      1  157   24    5  483%
c i   69.7   78299   562515     23539   16167   1598 153939   22   198   52  11%      1  156   24    5  472%
c i   70.0   78269   562515     23752   16351   1613 153952   22   199   52  11%      1  156   20    5  389%
c i   70.5   78268   562515     24003   16578   1626 153958   22   201   53  11%      1  158   22    5  428%
c i   70.5   78218   562515     24013   16587   1626 153958   22   201   53  11%      1  158   24    5  474%
c i   70.6   78212   562515     24046   16613   1627 153961   22   201   53  11%      1  158   24    5  467%
c i   70.8   78208   562515     24190   16729   1637 153971   23   203   53  11%      1  159   30    5  571%
c 
c [simplification-10] limit of 346 iterations hit after 346 iterations
c [quatres-6] found 32694 quaternary clauses 43% in total
c [quatres-6-1] removed 2 duplicate quaternary clauses
c [quatres-6-2] added 3 single-self-subsuming ternary resolvents
c [quatres-6-2] added 1 quaternary resolvents
c [ternres-6] limit 9563292 with penalty 0 = 0 + 0
c [ternres-6] all 78113 free variables schedulable
c [ternres-6] 51 ternary resolvents (0 bin, 51 trn)
c [ternres-6] 24549 variables remain 31% (53564 retained 69%)
c [card-4] limit 597705 penalty 3 = 3 + 0
c [card-4] found 1588 at-most-one constraints of average size 3.8
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 597705 for elimination
c [card-4] 1588 out of 1588 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-23] removed 1409 variables
c [treelook-4] limit 956329 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 99912 literals 64%
c [treelook-4] scheduling used 956501 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 956329 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 975224 steps
c [treelook-4] 99894 literals remain 64%
c [treelook-4] 33596 variables remain to probed next time 43%
c [treelook-4] removed 4 variables, found 4273 hbrs
c [unhide-10] limit 1912658 with penalty 0 = 0 + 0
c [unhide-10-10] 13 units, 515 failed, 20306 tauts, 0 hbrs, 45382 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 208 transitive binary clauses
c [transred-6] found 3 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 239082300 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 1 clauses out of 137 (1%) of length 10
c [cce-4-1] eliminated 1 clauses out of 443 (0%) of length 8
c [cce-4-1] eliminated 42 clauses out of 768 (5%) of length 7
c [cce-4-1] eliminated 167 clauses out of 2311 (7%) of length 6
c [cce-4-1] eliminated 18414 clauses out of 35034 (53%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 18625 large clauses in 239082305 steps
c [cce-4-1] allowing another 119541152 steps for small clauses
c [cce-4-1] scheduling 447970 clauses = 259723 binary + 188247 ternary
c [cce-4-1] tried to eliminate 2368 small clauses 1%
c [cce-4-1] eliminated 396 binary clauses 0%
c [cce-4-1] eliminated 138 ternary clauses 0%
c [cce-4-1] eliminated 534 small clauses 0%
c [cce-4-1] eliminated 5913 small clauses in 239082316 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 24538 covered clauses in round 1
c [cce-4] eliminated 24538 covered clauses in TOTAL during 1 rounds
c [bca-6] limit of 10000000 steps and 1056824 added (scaled 2)
c [bca-6] 121691 out of 154936 literals actually usable 79%
c [bca-6] added 86 blocked clauses in 303252 steps
c [sweep-6] limit 2868987 penalty 0 = 0 + 0
c [sweep-6-1] 5428 pos 7.5% + 66671 neg 92.5% = 72099 sched 93.1% ret 5368
c [sweep-6-1] 2906924 steps 21 queries 10258.86 avg class size
c [sweep-6-1] 205 decisions 19 SAT calls 198.47 avg env size
c [sweep-6-1] 72023 variables remain 93% (5436 retained 7%)
c [decomp-25] removed 24 variables
c [sweep-6-1] removed 24 vars (0 failed, 2 eqs, 3 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 24 vars in TOTAL (1 rounds, 20 queries)
c [phase-count-10] 525768 negative 99.6% of 527627 except 1859 0.4%
c [phase-count-10] 428205 positive 81.2% of 527627 except 99422 18.8%
c [phase-count-10] less non-negative clauses 1859 than limit 52700 (10.0%)
c [phase-count-10] non-pos/non-neg = 99422/1859 = 53.48 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 21 negative 100%
c [sort-queue-10] sorted 77443 enqueued variables after 24190 conflicts
c [score-dist-10] active 0 (0%), one 50106 (65%), zero 27337 (35%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 670 variables 0.9% (77443 remain 32%)
c [simplification-10] removed 34888 irredundant clauses 6.2% (527627 remain 39%)
c [simplification-10] maximum reduction of 6% = max (1%, 6%)
c [simplification-10] forced so keeping old conflict interval 10000
c [simplification-10] conflict limit remains at 24471 (hard 34378)
c [simplification-10] new iteration 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   80.5   77442   527627     24245   16610   1749 137052   23   202   51  11%      1  158   26    5  491%
c i   80.6   77438   527627     24281   16641   1751 137053   22   202   51  11%      1  158   24    5  452%
c 
c [simplification-11] limit 24471 conflicts (hard 34378) hit after 24471 conflicts
c [quatres-7] found 34119 quaternary clauses 58% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [ternres-7] limit 9693185 with penalty 0 = 0 + 0
c [ternres-7] 24335 schedulable variables 31%
c [ternres-7] 38 ternary resolvents (0 bin, 38 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-4] limit 500000 penalty 2 = 2 + 0
c [gauss-4] extracted 18 xors of average arity 2.9
c [gauss-4] connected 53 occurrences of 53 variables (average 1.0)
c [gauss-4] limit 500000 penalty 2 = 2 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-26] removed 1 variables
c [basicprobe-4] limit 48465925 penalty 0 = 0 + 0
c [basicprobe-4-0] 23861 probes remain 31% after last round
c [basicprobe-4-0] 277 units = 277 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 894 variables, found 137174 hbrs
c [bate-2] eliminated 128 asymmetric tautologies during probing
c [unhide-11] limit 1938637 with penalty 0 = 0 + 0
c [unhide-11-11] 3 units, 233 failed, 9106 tauts, 0 hbrs, 27928 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 172 transitive binary clauses
c [transred-7] found 2 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 76391 variables 100%
c [block-4] limit of 24232962 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 833 blocked clauses
c [block-4] 833 < 1/100 * 516238 = 5162 considered unsuccessful
c [cce-5] limit of 48465925 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 928 (0%) of length 9
c [cce-5-1] eliminated 1 clauses out of 722 (0%) of length 7
c [cce-5-1] eliminated 8 clauses out of 2187 (0%) of length 6
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 10 large clauses in 48465926 steps
c [cce-5-1] allowing another 24232963 steps for small clauses
c [cce-5-1] scheduling 434936 clauses = 250632 binary + 184304 ternary
c [cce-5-1] tried to eliminate 519 small clauses 0%
c [cce-5-1] eliminated 98 binary clauses 0%
c [cce-5-1] eliminated 12 ternary clauses 0%
c [cce-5-1] eliminated 110 small clauses 0%
c [cce-5-1] eliminated 110 small clauses in 48465925 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 120 covered clauses in round 1
c [cce-5] eliminated 120 covered clauses in TOTAL during 1 rounds
c [cce-5] 120 < 1/100 * 514009 = 5140 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 76341 variables 100%
c [elim-9] limit of 96931850 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 13381 variables 18% in round 1 in 47368232 steps
c [elim-9-1] backward subsumption/strengthening limit 47368200
c [elim-9-1-1] backward checking 32678 touched variables 43%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 26 and strengthened 119 clauses in 5773362 steps
c [elim-9-1] rescheduled 356 variables 0% by backward subsumption
c [elim-9-2] eliminated 37 variables 0% in round 2 in 251433 steps
c [elim-9-2] backward subsumption/strengthening limit 251400
c [elim-9-2-1] backward checking 340 touched variables 0%
c [elim-9-2-1] incomplete backward checking 0 remain 0%
c [elim-9-2] subsumed 5 and strengthened 11 clauses in 251401 steps
c [elim-9-2] rescheduled 53 variables 0% by backward subsumption
c [elim-9-3] eliminated 5 variables 0% in round 3 in 47758 steps
c [elim-9-3] backward subsumption/strengthening limit 47700
c [elim-9-3-1] backward checking 54 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 0 and strengthened 10 clauses in 47701 steps
c [elim-9] incomplete 40 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 13460 = 18% variables out of 76341 scheduled
c [bca-7] limit of 10000000 steps and 965041 added (scaled 2)
c [bca-7] 111100 out of 125764 literals actually usable 88%
c [bca-7] added 156 blocked clauses in 279897 steps
c [sweep-7] limit 2907955 penalty 0 = 0 + 0
c [sweep-7-1] 5130 pos 8.8% + 53161 neg 91.2% = 58291 sched 92.7% ret 4590
c [sweep-7-1] 3013216 steps 31 queries 12181.03 avg class size
c [sweep-7-1] 405 decisions 29 SAT calls 65.31 avg env size
c [sweep-7-1] 57930 variables remain 92% (4941 retained 8%)
c [decomp-27] removed 119 variables
c [sweep-7-1] removed 119 vars (0 failed, 2 eqs, 8 impls)
c [sweep-7] removed 119 vars in TOTAL (1 rounds, 30 queries)
c [phase-count-11] 480154 negative 99.7% of 481565 except 1411 0.3%
c [phase-count-11] 385553 positive 80.1% of 481565 except 96012 19.9%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 3 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 62762 enqueued variables after 24471 conflicts
c [score-dist-11] active 0 (0%), one 40324 (64%), zero 22438 (36%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 14670 variables 18.9% (62762 remain 26%)
c [simplification-11] removed 46062 irredundant clauses 8.7% (481565 remain 35%)
c [simplification-11] maximum reduction of 19% = max (19%, 9%)
c [simplification-11] large reduction 19% >= 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 36471 (soft 26471 + delta 10000)
c [simplification-11] new conflict limit 26471 (hard 36471)
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   89.4   62761   481565     24645    4925   1638 236643   22   201   44  11%      2  157   17    5  322%
c i   89.5   62758   481565     24735    5003   1643 236647   22   201   44  11%      1  156   15    5  273%
c i   89.6   62754   481565     24861    5107   1648 236661   22   200   44  11%      1  155   15    5  273%
c i   89.7   62747   481565     24886    5129   1649 236662   21   200   44  11%      1  155   14    5  261%
c i   90.1   62745   481565     25510    5699   1671 236682   20   188   44  11%      3  142   13    5  248%
c i   90.1   62741   481565     25513    5700   1671 236683   20   188   44  11%      3  142   13    5  246%
c i   90.4   62736   481565     25819    5965   1686 236702   20   187   44  11%      3  140   14    5  258%
c i   90.5   62706   481565     25875    6006   1691 236707   20   187   44  11%      3  139   13    5  238%
c i   90.5   62702   481565     25876    6006   1691 236707   20   187   44  11%      3  139   13    5  237%
c i   90.9   62700   481565     26180    6265   1717 236722   19   186   44  10%      2  138   16    5  291%
c 
c [simplification-12] limit 26484 conflicts (hard 36471) hit after 26485 conflicts
c [quatres-8] found 39309 quaternary clauses 63% in total
c [quatres-8-1] removed 2 duplicate quaternary clauses
c [quatres-8-2] added 8 quaternary resolvents
c [ternres-8] limit 10375487 with penalty 0 = 0 + 0
c [ternres-8] all 62694 free variables schedulable
c [ternres-8] 145 ternary resolvents (1 bin, 144 trn)
c [ternres-8] 16247 variables remain 26% (46447 retained 74%)
c [decomp-28] removed 73 variables
c [simpleprobe-5] 1491 schedulable variables 2%
c [simpleprobe-5] limit 41501951 penalty 0 = 0 + 0
c [decomp-29] removed 790 variables
c [simpleprobe-5] 3387 variables remain 5% (58512 retained 95%)
c [simpleprobe-5] removed 790 variables, found 63933 hbrs, 259 units
c [unhide-12] limit 2075097 with penalty 0 = 0 + 0
c [unhide-12-12] 12 units, 434 failed, 37858 tauts, 0 hbrs, 5181 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 284 transitive binary clauses
c [transred-8] found 3 units
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 61599 variables 100%
c [elim-10] limit of 207509757 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 690 variables 1% in round 1 in 44508300 steps
c [elim-10-1] backward subsumption/strengthening limit 44508300
c [elim-10-1-1] backward checking 2804 touched variables 5%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 10 and strengthened 41 clauses in 931314 steps
c [elim-10-1] rescheduled 120 variables 0% by backward subsumption
c [elim-10-2] eliminated 12 variables 0% in round 2 in 275909 steps
c [elim-10-2] backward subsumption/strengthening limit 275900
c [elim-10-2-1] backward checking 121 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 8 and strengthened 12 clauses in 165087 steps
c [elim-10-2] rescheduled 53 variables 0% by backward subsumption
c [elim-10-3] eliminated 3 variables 0% in round 3 in 563303 steps
c [elim-10-3] backward subsumption/strengthening limit 563300
c [elim-10-3-1] backward checking 35 touched variables 0%
c [elim-10-3-1] fully completed backward checking in 1 rounds
c [elim-10-3] subsumed 0 and strengthened 6 clauses in 94005 steps
c [elim-10] incomplete 24 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 715 = 1% variables out of 61599 scheduled
c [bca-8] limit of 10000000 steps and 941539 added (scaled 2)
c [bca-8] 104413 out of 121770 literals actually usable 86%
c [bca-8] added 47 blocked clauses in 255963 steps
c [sweep-8] limit 3112646 penalty 0 = 0 + 0
c [sweep-8-1] 5233 pos 9.3% + 51121 neg 90.7% = 56354 sched 92.6% ret 4530
c [sweep-8-1] 3142752 steps 37 queries 8093.08 avg class size
c [sweep-8-1] 482 decisions 32 SAT calls 206.28 avg env size
c [sweep-8-1] 56000 variables remain 92% (4877 retained 8%)
c [decomp-30] removed 17 variables
c [sweep-8-1] removed 17 vars (0 failed, 4 eqs, 6 impls)
c [sweep-8] 17 < 1/1000 * 60884 = 60 considered unsuccessful
c [sweep-8] removed 17 vars in TOTAL (1 rounds, 36 queries)
c [phase-count-12] 468599 negative 99.7% of 469962 except 1363 0.3%
c [phase-count-12] 375129 positive 79.8% of 469962 except 94833 20.2%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 60867 enqueued variables after 26485 conflicts
c [score-dist-12] active 0 (0%), one 39853 (65%), zero 21014 (35%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 1827 variables 2.9% (60867 remain 25%)
c [simplification-12] removed 11603 irredundant clauses 2.4% (469962 remain 35%)
c [simplification-12] maximum reduction of 3% = max (3%, 2%)
c [simplification-12] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-12] new conflict interval 15000
c [simplification-12] penalized conflict interval 15000 = 1 * 15000
c [simplification-12] hard conflict limit 51485 (soft 41485 + delta 10000)
c [simplification-12] new conflict limit 41485 (hard 51485)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   96.0   60866   469962     26884    6486   1746 259919   18   181   44  10%      4  131   10    6  172%
c i   96.3   60864   469962     27334    6876   1779 259931   18   177   44  10%      4  127   14    6  255%
c i   96.4   60863   469962     27416    6953   1780 259934   18   177   44  10%      3  126   13    6  237%
c i   96.5   60862   469962     27470    6995   1786 259938   18   176   44  10%      3  126   12    6  220%
c i   96.8   60769   469962     27770    7259   1798 259953   17   177   44  10%      3  126   14    6  253%
c i   97.0   60712   469962     27933    7409   1803 259958   17   176   44  10%      3  125   16    6  279%
c i   97.0   60710   469962     27979    7447   1804 259964   17   176   44  10%      2  124   15    6  258%
c i   97.0   60704   469962     27980    7447   1804 259964   17   176   44  10%      2  124   15    6  257%
c i   97.1   60702   469962     28002    7467   1804 259965   17   176   44  10%      2  125   14    6  248%
c i   97.2   60694   469962     28071    7526   1808 259968   17   176   44  10%      2  124   13    6  222%
c i   97.3   60689   469962     28208    7644   1820 259972   17   174   44  10%      2  122   12    6  202%
c i   97.8   60688   469962     28554    7951   1835 259985   17   177   44  10%      2  124   16    6  278%
c i   98.4   60683   469962     29198    8523   1862 260008   17   172   45  10%      3  118   18    6  301%
c i   98.4   60682   469962     29205    8528   1862 260008   17   172   45  10%      3  118   19    6  317%
c i   98.5   60677   469962     29259    8573   1866 260011   17   172   45  10%      3  118   17    6  283%
c i  100.1   60669   469962     30645    9795   1926 260078   19   179   46  10%     10  123   26    6  410%
c i  100.2   60668   469962     30727    9870   1928 260082   19   179   46  11%      9  122   25    6  397%
c i  100.9   60637   469962     31364   10452   1947 260098   19   178   46  11%      7  120   18    6  286%
c i  101.3   60635   469962     31664   10718   1955 260106   21   183   46  11%      6  125   34    7  514%
c i  101.5   60632   469962     31728   10775   1956 260108   21   186   46  11%      5  128   38    7  572%
c i  101.6   60627   469962     31864   10899   1960 260112   21   187   46  11%      5  129   33    7  504%
c i  101.7   60625   469962     32001   11016   1967 260120   21   184   46  11%      4  125   27    7  400%
c i  101.9   60549   469962     32172   11165   1977 260127   21   184   46  11%      4  125   21    7  313%
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  102.0   60548   469962     32192   11181   1978 260129   21   184   46  11%      3  125   21    7  310%
c i  102.2   60547   469962     32338   11311   1983 260135   21   184   46  11%      3  124   18    7  261%
c i  102.5   60543   469962     32632   11585   1993 260141   20   182   46  11%      3  122   17    7  258%
c i  102.8   60538   469962     32807   11729   2003 260159   20   185   46  11%      2  124   17    7  245%
c i  102.9   60533   469962     32873   11791   2005 260159   20   186   46  11%      2  125   18    7  271%
c i  102.9   60532   469962     32889   11804   2006 260160   20   185   46  11%      2  125   18    7  262%
c i  102.9   60482   469962     32890   11804   2006 260160   20   185   46  11%      2  125   18    7  261%
c i  102.9   60481   469962     32891   11804   2006 260160   20   185   46  11%      2  125   18    7  260%
c i  103.1   60427   469962     33088   11976   2018 260165   21   186   46  11%      2  125   23    7  335%
c i  104.4   60424   469962     34289   13057   2060 260203   23   190   48  12%      8  127   34    7  464%
c i  104.6   60423   469962     34424   13184   2063 260205   24   193   48  12%      7  129   35    7  475%
c i  104.6   60420   469962     34442   13198   2063 260205   24   193   48  12%      7  129   35    7  479%
c i  105.1   60419   469962     34804   13518   2075 260222   24   195   48  13%      5  130   28    8  370%
c i  105.5   60416   469962     35113   13798   2088 260230   24   196   49  12%      4  131   22    8  290%
c i  105.5   60413   469962     35142   13821   2091 260230   24   195   49  12%      4  130   21    8  277%
c i  105.9   60412   469962     35489   14144   2104 260234   24   193   49  13%      3  127   26    8  334%
c i  106.1   60411   469962     35667   14301   2114 260242   24   190   49  13%      3  124   25    8  327%
c i  106.4   60410   469962     35956   14558   2126 260255   24   185   49  13%      2  119   23    8  300%
c i  106.7   60346   469962     36202   14774   2141 260264   24   186   49  13%      2  119   21    8  273%
c i  109.5   60344   469962     38343   16711   2213 260348   24   191   51  13%     18  120   23    8  278%
c i  109.6   60342   469962     38502   16856   2215 260353   25   189   51  13%     16  118   29    8  341%
c i  109.7   60340   469962     38568   16913   2217 260359   25   189   51  13%     15  118   26    8  311%
c i  109.7   60337   469962     38576   16919   2218 260359   25   189   51  13%     15  118   26    8  303%
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  110.3   60333   469962     38998   17311   2225 260371   25   192   51  13%     10  120   29    9  333%
c i  111.0   60331   469962     39447   17733   2235 260379   26   198   51  13%      7  125   34    9  382%
c i  111.4   60330   469962     39838   18094   2245 260390   26   197   51  13%      6  123   24    9  275%
c i  111.4   60327   469962     39853   18103   2245 260391   26   196   51  13%      5  122   24    9  269%
c i  111.5   60326   469962     39881   18124   2248 260392   26   196   51  13%      5  122   22    9  251%
c i  111.8   60188   469962     40171   18378   2254 260405   26   195   51  14%      4  121   29    9  328%
c i  111.8   60151   469962     40172   18378   2254 260405   26   195   51  14%      4  121   29    9  326%
c i  111.9   60147   469962     40246   18438   2259 260407   26   195   51  13%      4  120   27    9  297%
c i  111.9   60095   469962     40265   18454   2259 260409   26   195   51  13%      4  120   25    9  283%
c i  112.2   60094   469962     40418   18600   2260 260411   27   198   51  14%      3  123   37    9  408%
c i  112.3   60093   469962     40477   18655   2261 260412   27   199   51  14%      3  124   34    9  378%
c i  112.6   60092   469962     40674   18836   2267 260421   27   199   52  13%      2  124   27    9  300%
c i  112.7   60091   469962     40736   18887   2271 260427   27   198   52  13%      2  123   26    9  281%
c i  113.0   60090   469962     40935   19063   2276 260430   27   202   52  13%      2  127   32    9  350%
c i  113.3   60089   469962     41241   19347   2285 260438   27   201   52  14%      2  124   26    9  277%
c i  113.4   60065   469962     41338   19435   2288 260441   27   201   52  13%      1  125   25    9  273%
c 
c [simplification-13] limit 41527 conflicts (hard 51485) hit after 41527 conflicts
c [quatres-9] found 35106 quaternary clauses 59% in total
c [quatres-9-1] removed 2 duplicate quaternary clauses
c [quatres-9-2] added 5 single-self-subsuming ternary resolvents
c [quatres-9-2] added 24 quaternary resolvents
c [ternres-9] limit 16039610 with penalty 0 = 0 + 0
c [ternres-9] 15603 schedulable variables 26%
c [ternres-9] 311 ternary resolvents (2 bin, 309 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-31] removed 846 variables
c [treelook-5] limit 1603961 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 101726 literals 85%
c [treelook-5] scheduling used 1604411 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 1603961 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1610695 steps
c [treelook-5] 101695 literals remain 85%
c [treelook-5] 22258 variables remain to probed next time 37%
c [decomp-32] removed 1 variables
c [treelook-5] removed 6 variables, found 8135 hbrs
c [unhide-13] limit 3207922 with penalty 0 = 0 + 0
c [unhide-13-14] 11 units, 410 failed, 27139 tauts, 0 hbrs, 80427 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 211 transitive binary clauses
c [transred-9] found 1 units
c [cce-6] limit of 40099025 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 7 clauses out of 198 (4%) of length 7
c [cce-6-1] eliminated 39 clauses out of 2961 (1%) of length 6
c [cce-6-1] eliminated 1412 clauses out of 15784 (9%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 1458 large clauses in 40099030 steps
c [cce-6-1] allowing another 20049515 steps for small clauses
c [cce-6-1] scheduling 371407 clauses = 202891 binary + 168516 ternary
c [cce-6-1] tried to eliminate 433 small clauses 0%
c [cce-6-1] eliminated 65 binary clauses 0%
c [cce-6-1] eliminated 20 ternary clauses 0%
c [cce-6-1] eliminated 85 small clauses 0%
c [cce-6-1] eliminated 2715 small clauses in 40099028 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 4173 covered clauses in round 1
c [cce-6] eliminated 4173 covered clauses in TOTAL during 1 rounds
c [cce-6] 4173 < 1/100 * 454122 = 4541 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 59539 variables 100%
c [elim-11] limit of 320792207 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 1912 variables 3% in round 1 in 42018429 steps
c [elim-11-1] backward subsumption/strengthening limit 42018400
c [elim-11-1-1] backward checking 7086 touched variables 12%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 13 and strengthened 22 clauses in 1934957 steps
c [elim-11-1] rescheduled 136 variables 0% by backward subsumption
c [elim-11-2] eliminated 8 variables 0% in round 2 in 306915 steps
c [elim-11-2] backward subsumption/strengthening limit 306900
c [elim-11-2-1] backward checking 72 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 3 and strengthened 9 clauses in 145058 steps
c [elim-11-2] rescheduled 39 variables 0% by backward subsumption
c [elim-11-3] eliminated 3 variables 0% in round 3 in 187555 steps
c [elim-11-3] backward subsumption/strengthening limit 187500
c [elim-11-3-1] backward checking 32 touched variables 0%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 0 and strengthened 6 clauses in 125855 steps
c [elim-11] incomplete 24 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 1933 = 3% variables out of 59539 scheduled
c [bca-9] limit of 10000000 steps and 891143 added (scaled 2)
c [bca-9] 92507 out of 115214 literals actually usable 80%
c [bca-9] added 51 blocked clauses in 225558 steps
c [sort-queue-13] sorted 57606 enqueued variables after 41527 conflicts
c [score-dist-13] active 0 (0%), one 39116 (68%), zero 18490 (32%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 2458 variables 4.1% (57606 remain 23%)
c [simplification-13] removed 25122 irredundant clauses 5.3% (444840 remain 33%)
c [simplification-13] maximum reduction of 5% = max (4%, 5%)
c [simplification-13] large reduction 5% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 53527 (soft 43527 + delta 10000)
c [simplification-13] new conflict limit 43527 (hard 53527)
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  119.6   57605   444840     42157   12499   2424 232081   26   195   45  13%      4  116   19    9  198%
c i  120.0   57602   444840     42497   12806   2439 232090   25   194   45  13%      3  116   17    9  180%
c i  120.6   57597   444840     43142   13400   2458 232111   24   189   45  12%      3  110   15   10  153%
c 
c [simplification-14] limit 43527 conflicts (hard 53527) hit after 43529 conflicts
c [quatres-10] found 35642 quaternary clauses 61% in total
c [quatres-10-1] removed 3 duplicate quaternary clauses
c [quatres-10-2] added 1 single-self-subsuming ternary resolvents
c [quatres-10-2] added 2 quaternary resolvents
c [ternres-10] limit 16791375 with penalty 0 = 0 + 0
c [ternres-10] all 57511 free variables schedulable
c [ternres-10] 310 ternary resolvents (0 bin, 310 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-33] removed 112 variables
c [basicprobe-5] limit 83956877 penalty 0 = 0 + 0
c [basicprobe-5-0] 12438 probes remain 22% after last round
c [basicprobe-5-0] 460 units = 447 failed (97%) + 13 lifted (3%)
c [basicprobe-5-0] removed 809 variables, found 252493 hbrs
c [bate-3] eliminated 715 asymmetric tautologies during probing
c [unhide-14] limit 3358275 with penalty 0 = 0 + 0
c [unhide-14-16] 12 units, 281 failed, 56110 tauts, 0 hbrs, 19595 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 173 transitive binary clauses
c [transred-10] found 1 units
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 56269 variables 100%
c [elim-12] limit of 335827510 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 668 variables 1% in round 1 in 39418221 steps
c [elim-12-1] backward subsumption/strengthening limit 39418200
c [elim-12-1-1] backward checking 4026 touched variables 7%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 23 and strengthened 42 clauses in 1233548 steps
c [elim-12-1] rescheduled 158 variables 0% by backward subsumption
c [elim-12-2] eliminated 22 variables 0% in round 2 in 120940 steps
c [elim-12-2] backward subsumption/strengthening limit 120900
c [elim-12-2-1] backward checking 203 touched variables 0%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 19 and strengthened 23 clauses in 120901 steps
c [elim-12-2] rescheduled 97 variables 0% by backward subsumption
c [elim-12-3] eliminated 9 variables 0% in round 3 in 119612 steps
c [elim-12-3] backward subsumption/strengthening limit 119600
c [elim-12-3-1] backward checking 90 touched variables 0%
c [elim-12-3-1] incomplete backward checking 0 remain 0%
c [elim-12-3] subsumed 0 and strengthened 13 clauses in 119601 steps
c [elim-12] incomplete 52 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 707 = 1% variables out of 56269 scheduled
c [bca-10] limit of 10000000 steps and 851906 added (scaled 2)
c [bca-10] 87981 out of 111126 literals actually usable 79%
c [bca-10] added 98 blocked clauses in 213055 steps
c [sweep-9] limit 2518706 penalty 1 = 1 + 0
c [sweep-9-1] 4766 pos 9.2% + 46787 neg 90.8% = 51553 sched 92.8% ret 4009
c [sweep-9-1] 2526580 steps 39 queries 10408.69 avg class size
c [sweep-9-1] 443 decisions 36 SAT calls 188.11 avg env size
c [sweep-9-1] 51136 variables remain 92% (4411 retained 8%)
c [decomp-34] removed 91 variables
c [sweep-9-1] removed 91 vars (0 failed, 2 eqs, 6 impls)
c [sweep-9] removed 91 vars in TOTAL (1 rounds, 38 queries)
c [sort-queue-14] sorted 55471 enqueued variables after 43529 conflicts
c [score-dist-14] active 0 (0%), one 38328 (69%), zero 17143 (31%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 2040 variables 3.5% (55471 remain 23%)
c [simplification-14] removed 19789 irredundant clauses 4.4% (425051 remain 31%)
c [simplification-14] maximum reduction of 4% = max (4%, 4%)
c [simplification-14] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-14] new conflict interval 19000
c [simplification-14] penalized conflict interval 19000 = 1 * 19000
c [simplification-14] hard conflict limit 72529 (soft 62529 + delta 10000)
c [simplification-14] new conflict limit 62529 (hard 72529)
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.1   55470   425051     44161   13769   2927 416559   23   191   49  12%      6  110   22   10  224%
c i  130.1   55468   425051     44224   13825   2929 416560   23   191   49  12%      6  109   21   10  214%
c i  131.5   55465   425051     45494   15004   2967 416587   22   184   49  12%      9  101   18   10  178%
c i  131.8   55463   425051     45785   15275   2971 416595   22   185   49  12%      7  101   19   10  187%
c i  132.2   55462   425051     46058   15519   2977 416606   22   185   49  12%      5  101   25   10  245%
c i  133.0   55459   425051     46646   16057   3000 416618   23   191   49  12%      4  105   25   10  246%
c i  133.3   55458   425051     46930   16322   3008 416623   23   191   49  12%      3  105   26   10  256%
c i  135.0   55457   425051     48320   17601   3044 416657   24   191   50  12%      9  103   27   11  252%
c i  135.4   55452   425051     48629   17888   3053 416662   24   187   50  13%      7   99   23   11  214%
c i  135.5   55439   425051     48735   17989   3055 416663   24   188   50  13%      6   99   24   11  222%
c i  135.5   55437   425051     48736   17989   3055 416663   24   188   50  13%      6   99   24   11  221%
c i  135.9   55433   425051     49050   18276   3066 416673   24   189   50  13%      5  100   25   11  229%
c i  135.9   55431   425051     49051   18276   3066 416673   24   189   50  13%      5  100   24   11  228%
c i  136.2   55424   425051     49268   18483   3072 416674   24   187   50  13%      4   97   24   11  219%
c i  136.6   55423   425051     49607   18779   3088 416688   24   184   50  13%      3   94   28   11  255%
c i  136.7   55419   425051     49733   18899   3090 416690   24   181   50  13%      2   91   22   11  207%
c i  136.7   55418   425051     49745   18909   3091 416690   24   181   50  13%      2   91   22   11  203%
c i  136.9   55416   425051     49942   19076   3101 416700   24   179   50  13%      2   88   22   11  202%
c i  137.6   55413   425051     50570   19654   3110 416713   25   184   52  13%      2   93   31   11  279%
c i  141.5   55412   425051     54698   23435   3201 416798   27   190   54  14%     45   93   21   12  176%
c i  141.7   55411   425051     54866   23582   3205 416803   27   193   54  14%     38   95   25   12  203%
c i  142.3   55410   425051     55336   23992   3208 416815   32   200   55  16%     24  102   65   13  516%
c i  145.0   55392   425051     58052   26479   3253 416858   36   200   57  18%     25   97   37   14  269%
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  145.0   55387   425051     58053   26479   3253 416858   36   200   57  18%     25   97   37   14  268%
c i  145.9   55386   425051     58831   27192   3265 416872   37   205   57  18%     13  102   38   14  274%
c i  146.5   55385   425051     59436   27721   3282 416892   38   206   58  18%      7  102   46   14  320%
c i  146.5   55374   425051     59437   27721   3282 416892   38   206   58  18%      7  102   46   14  319%
c i  146.5   55370   425051     59438   27721   3282 416892   38   206   58  18%      7  102   46   14  318%
c i  148.2   55339   425051     60982   29142   3319 416925   39   220   61  18%      9  113   32   15  211%
c i  148.3   55325   425051     61044   29197   3324 416925   38   219   61  18%      9  112   30   15  203%
c i  148.9   55324   425051     61559   29664   3338 416936   38   217   61  17%      5  109   31   15  208%
c i  149.0   55203   425051     61662   29760   3338 416937   38   222   61  17%      4  114   43   15  281%
c i  150.0   55197   425051     62497   30527   3359 416949   40   226   61  18%      3  116   55   16  355%
c 
c [simplification-15] limit 62579 conflicts (hard 72529) hit after 62579 conflicts
c [quatres-11] found 32517 quaternary clauses 58% in total
c [quatres-11-1] removed 2 duplicate quaternary clauses
c [quatres-11-2] added 1 single-self-subsuming ternary resolvents
c [quatres-11-2] added 21 quaternary resolvents
c [ternres-11] limit 23093697 with penalty 0 = 0 + 0
c [ternres-11] all 55195 free variables schedulable
c [ternres-11] 413 ternary resolvents (3 bin, 410 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 721678 penalty 4 = 4 + 0
c [card-5] found 1285 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 721678 for elimination
c [card-5] 1285 out of 1285 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-5] limit 577342 penalty 3 = 3 + 0
c [gauss-5] extracted 14 xors of average arity 2.6
c [gauss-5] connected 37 occurrences of 37 variables (average 1.0)
c [gauss-5] limit 577342 penalty 3 = 3 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-35] removed 46 variables
c [simpleprobe-6] 3155 schedulable variables 6%
c [simpleprobe-6] limit 92374791 penalty 0 = 0 + 0
c [decomp-36] removed 497 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 497 variables, found 60798 hbrs, 204 units
c [unhide-15] limit 2309369 with penalty 1 = 0 + 1
c [unhide-15-17] 4 units, 31 failed, 8759 tauts, 0 hbrs, 98670 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 296 transitive binary clauses
c [transred-11] found 2 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 54596 variables 100%
c [block-5] limit of 28867122 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 202 blocked clauses
c [block-5] 202 < 1/100 * 413300 = 4133 considered unsuccessful
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 54595 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 482 variables 1% in round 1 in 37860204 steps
c [elim-13-1] backward subsumption/strengthening limit 37860200
c [elim-13-1-1] backward checking 2421 touched variables 4%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 12 and strengthened 18 clauses in 815803 steps
c [elim-13-1] rescheduled 83 variables 0% by backward subsumption
c [elim-13-2] eliminated 13 variables 0% in round 2 in 448133 steps
c [elim-13-2] backward subsumption/strengthening limit 448100
c [elim-13-2-1] backward checking 114 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 10 and strengthened 9 clauses in 136555 steps
c [elim-13-2] rescheduled 50 variables 0% by backward subsumption
c [elim-13-3] eliminated 7 variables 0% in round 3 in 60659 steps
c [elim-13-3] backward subsumption/strengthening limit 60600
c [elim-13-3-1] backward checking 110 touched variables 0%
c [elim-13-3-1] incomplete backward checking 39 remain 35%
c [elim-13-3] subsumed 6 and strengthened 0 clauses in 60637 steps
c [elim-13] incomplete 9 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 515 = 1% variables out of 54595 scheduled
c [elim-13] 515 < 1/100 * 54595 = 545 considered unsuccessful
c [bca-11] limit of 10000000 steps and 823325 added (scaled 2)
c [bca-11] 78977 out of 108162 literals actually usable 73%
c [bca-11] added 19 blocked clauses in 204780 steps
c [sweep-10] limit 6928109 penalty 0 = 0 + 0
c [sweep-10-1] 5069 pos 10.1% + 44873 neg 89.9% = 49942 sched 92.3% ret 4138
c [sweep-10-1] 7044235 steps 67 queries 4169.01 avg class size
c [sweep-10-1] 1419 decisions 60 SAT calls 232.50 avg env size
c [sweep-10-1] 47694 variables remain 88% (6367 retained 12%)
c [decomp-37] removed 38 variables
c [sweep-10-1] removed 38 vars (0 failed, 7 eqs, 10 impls)
c [sweep-10] 38 < 1/1000 * 54080 = 54 considered unsuccessful
c [sweep-10] removed 38 vars in TOTAL (1 rounds, 66 queries)
c [sort-queue-15] sorted 54042 enqueued variables after 62579 conflicts
c [score-dist-15] active 0 (0%), one 38405 (71%), zero 15637 (29%)
c [score-dist-15] max exp 1, different 2 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 1153 variables 2.1% (54042 remain 22%)
c [simplification-15] removed 14391 irredundant clauses 3.4% (410660 remain 30%)
c [simplification-15] maximum reduction of 3% = max (2%, 3%)
c [simplification-15] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-15] new conflict interval 24000
c [simplification-15] penalized conflict interval 24000 = 1 * 24000
c [simplification-15] hard conflict limit 98579 (soft 86579 + delta 12000)
c [simplification-15] new conflict limit 86579 (hard 98579)
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  157.5   54041   410660     63922   28604   3489 463495   40   232   64  17%      7  120   41   16  257%
c i  157.9   54040   410660     64261   28912   3496 463507   40   236   64  17%      5  123   40   16  247%
c i  157.9   54030   410660     64262   28912   3496 463507   40   236   64  17%      5  123   40   16  246%
c i  158.0   54028   410660     64372   29016   3497 463509   40   235   64  17%      4  122   38   16  234%
c i  158.0   54025   410660     64380   29022   3497 463510   40   234   64  17%      4  121   37   16  230%
c i  160.1   53843   410660     66133   30644   3526 463542   43   242   64  18%     11  126   48   17  277%
c i  160.2   53839   410660     66247   30751   3527 463544   43   239   64  18%      9  122   40   17  232%
c i  160.2   53838   410660     66248   30751   3527 463544   43   239   64  18%      9  122   40   17  231%
c i  160.5   53835   410660     66503   30988   3529 463545   43   234   64  18%      6  117   40   17  229%
c i  161.7   53834   410660     67489   31880   3561 463565   47   239   64  20%      5  120   60   18  335%
c i  161.8   53818   410660     67583   31966   3562 463565   47   240   64  20%      4  121   61   18  337%
c i  163.6   53815   410660     69179   33435   3589 463586   47   234   65  20%      9  112   44   19  238%
c i  164.0   53814   410660     69600   33822   3594 463592   48   234   65  21%      5  112   59   19  312%
c i  164.2   53244   410660     69776   33988   3598 463593   48   234   65  20%      4  111   48   19  250%
c i  164.6   53242   410660     70039   34232   3601 463594   49   235   65  21%      2  112   57   19  297%
c i  165.4   53241   410660     70703   34832   3613 463603   52   240   65  21%      1  116   70   20  354%
c i  166.2   53240   410660     71407   35479   3626 463615   52   243   66  21%      1  117   50   20  250%
c i  166.3   53239   410660     71448   35517   3628 463615   52   242   66  21%      1  116   47   20  233%
c i  166.9   53219   410660     71897   35930   3632 463627   52   243   66  21%     -0  117   48   20  238%
c i  167.3   52892   410660     72213   36220   3637 463631   53   247   67  21%     -1  120   65   20  320%
c i  167.7   52870   410660     72658   36611   3648 463649   53   247   68  22%     -1  119   63   21  306%
c i  168.9   52855   410660     73799   37624   3669 463680   53   244   68  22%      3  114   39   21  184%
c i  169.0   52854   410660     73852   37673   3672 463680   53   245   68  22%      3  115   44   21  208%
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  170.2   52851   410660     74903   38650   3684 463702   52   239   69  22%      4  107   45   22  210%
c i  170.4   52850   410660     75134   38867   3685 463704   51   239   69  21%      2  106   47   22  215%
c i  171.6   52849   410660     76169   39801   3706 463727   52   239   70  22%      3  105   43   22  194%
c i  172.3   52848   410660     76725   40313   3714 463734   55   242   72  23%      2  107   76   23  337%
c i  173.8   52846   410660     77968   41429   3728 463757   54   236   72  23%      5   99   48   23  208%
c i  173.8   52830   410660     77969   41429   3728 463757   54   235   72  23%      5   99   48   23  207%
c i  173.9   52829   410660     78018   41473   3728 463758   54   235   72  23%      4   98   47   23  200%
c i  175.3   52825   410660     79128   42495   3741 463774   54   236   74  23%      4   98   50   24  209%
c i  175.6   52824   410660     79361   42719   3741 463774   54   235   74  23%      3   96   47   24  197%
c i  175.9   52801   410660     79616   42953   3743 463776   55   236   76  23%      1   96   58   24  243%
c i  176.5   52800   410660     80060   43367   3746 463780   55   240   78  23%      0  100   56   24  232%
c i  176.6   52764   410660     80198   43488   3748 463784   55   239   78  23%     -0   99   48   24  196%
c i  177.5   52624   410660     80904   44096   3763 463800   58   240   78  24%      0   99   72   25  288%
c i  177.9   52623   410660     81229   44393   3765 463801   59   239   78  25%     -1   97   69   25  275%
c i  179.0   52622   410660     82210   45289   3776 463815   59   236   80  25%      2   93   55   26  216%
c i  182.5   52621   410660     84922   47776   3806 463847   58   235   82  25%     22   88   59   27  217%
c i  183.6   52582   410660     85674   48471   3816 463855   58   241   82  24%     11   93   58   27  213%
c 
c [simplification-16] limit 86610 conflicts (hard 98579) hit after 86612 conflicts
c [quatres-12] found 30119 quaternary clauses 55% in total
c [quatres-12-1] removed 2 duplicate quaternary clauses
c [quatres-12-1] added 1 double-self-subsuming ternary resolvents
c [quatres-12-2] added 2 single-self-subsuming ternary resolvents
c [quatres-12-2] added 7 quaternary resolvents
c [ternres-12] limit 31256108 with penalty 0 = 0 + 0
c [ternres-12] all 52582 free variables schedulable
c [ternres-12] 319 ternary resolvents (0 bin, 319 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-38] removed 1486 variables
c [treelook-6] limit 3125610 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 88102 literals 84%
c [treelook-6] scheduling used 1857743 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3125610 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 3221405 steps
c [treelook-6] 88049 literals remain 84%
c [treelook-6] 18240 variables remain to probed next time 35%
c [treelook-6] removed 7 variables, found 17327 hbrs
c [unhide-16] limit 3125610 with penalty 1 = 0 + 1
c [unhide-16-18] 8 units, 212 failed, 38554 tauts, 0 hbrs, 215311 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 196 transitive binary clauses
c [cce-7] limit of 39070135 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 53
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 52
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 51
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 50
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 49
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 48
c [cce-7-1] eliminated 3 clauses out of 3 (100%) of length 47
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 46
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 45
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 44
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 43
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 42
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 41
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 40
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 39
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 38
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 37
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 36
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 35
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 34
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 33
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 32
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 31
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 30
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 29
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 28
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 27
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 26
c [cce-7-1] eliminated 4 clauses out of 5 (80%) of length 25
c [cce-7-1] eliminated 3 clauses out of 3 (100%) of length 24
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 23
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 22
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 21
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 20
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 19
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 18
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 17
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 16
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 15
c [cce-7-1] eliminated 6 clauses out of 10 (60%) of length 14
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 13
c [cce-7-1] eliminated 7 clauses out of 8 (88%) of length 12
c [cce-7-1] eliminated 5 clauses out of 8 (62%) of length 11
c [cce-7-1] eliminated 12 clauses out of 18 (67%) of length 10
c [cce-7-1] eliminated 5 clauses out of 20 (25%) of length 9
c [cce-7-1] eliminated 9 clauses out of 56 (16%) of length 8
c [cce-7-1] eliminated 15 clauses out of 123 (12%) of length 7
c [cce-7-1] eliminated 125 clauses out of 2800 (4%) of length 6
c [cce-7-1] eliminated 1223 clauses out of 12895 (9%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 1538 large clauses in 39070138 steps
c [cce-7-1] allowing another 19535069 steps for small clauses
c [cce-7-1] scheduling 213846 clauses = 190932 binary + 22914 ternary
c [cce-7-1] tried to eliminate 947 small clauses 0%
c [cce-7-1] eliminated 247 binary clauses 0%
c [cce-7-1] eliminated 46 ternary clauses 0%
c [cce-7-1] eliminated 293 small clauses 0%
c [cce-7-1] eliminated 2635 small clauses in 39070138 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 4173 covered clauses in round 1
c [cce-7] eliminated 4173 covered clauses in TOTAL during 1 rounds
c [bca-12] limit of 10000000 steps and 775239 added (scaled 2)
c [bca-12] 70290 out of 104690 literals actually usable 67%
c [bca-12] added 40 blocked clauses in 205258 steps
c [sort-queue-16] sorted 52344 enqueued variables after 86612 conflicts
c [score-dist-16] active 0 (0%), one 38591 (74%), zero 13753 (26%)
c [score-dist-16] max exp 1, different 2 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 238 variables 0.5% (52344 remain 21%)
c [simplification-16] removed 23814 irredundant clauses 5.8% (386846 remain 28%)
c [simplification-16] maximum reduction of 6% = max (0%, 6%)
c [simplification-16] large reduction 6% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 98612 (soft 88612 + delta 10000)
c [simplification-16] new conflict limit 88612 (hard 98612)
c 
c [simplification-17] limit 88612 conflicts (hard 98612) hit after 88612 conflicts
c [quatres-13] found 30391 quaternary clauses 56% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-2] added 1 quaternary resolvents
c [ternres-13] limit 31938273 with penalty 0 = 0 + 0
c [ternres-13] all 52344 free variables schedulable
c [ternres-13] 165 ternary resolvents (0 bin, 165 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-40] removed 12 variables
c [basicprobe-6] limit 159691366 penalty 0 = 0 + 0
c [basicprobe-6-0] 6677 probes remain 13% after last round
c [basicprobe-6-0] 680 units = 653 failed (96%) + 27 lifted (4%)
c [basicprobe-6-0] removed 1359 variables, found 398741 hbrs
c [bate-4] eliminated 1054 asymmetric tautologies during probing
c [unhide-17] limit 1596913 with penalty 2 = 0 + 2
c [unhide-17-19] 3 units, 40 failed, 11877 tauts, 0 hbrs, 174369 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 228 transitive binary clauses
c [transred-13] found 2 units
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 50928 variables 100%
c [elim-14] limit of 319382732 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 1718 variables 3% in round 1 in 30290224 steps
c [elim-14-1] backward subsumption/strengthening limit 30290200
c [elim-14-1-1] backward checking 7518 touched variables 15%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 20 and strengthened 48 clauses in 2053539 steps
c [elim-14-1] rescheduled 174 variables 0% by backward subsumption
c [elim-14-2] eliminated 15 variables 0% in round 2 in 387674 steps
c [elim-14-2] backward subsumption/strengthening limit 387600
c [elim-14-2-1] backward checking 162 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 0 and strengthened 12 clauses in 146479 steps
c [elim-14-2] rescheduled 47 variables 0% by backward subsumption
c [elim-14-3] eliminated 4 variables 0% in round 3 in 39325 steps
c [elim-14-3] backward subsumption/strengthening limit 39300
c [elim-14-3-1] backward checking 48 touched variables 0%
c [elim-14-3-1] incomplete backward checking 2 remain 4%
c [elim-14-3] subsumed 0 and strengthened 8 clauses in 39305 steps
c [elim-14] incomplete 32 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 1737 = 3% variables out of 50928 scheduled
c [bca-13] limit of 10000000 steps and 715689 added (scaled 2)
c [bca-13] 70380 out of 98384 literals actually usable 72%
c [bca-13] added 39 blocked clauses in 181111 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 47907405 penalty 1 = 1 + 0
c [sweep-11-1] 4221 pos 9.6% + 39914 neg 90.4% = 44135 sched 89.7% ret 5056
c [sweep-11-1] 47916252 steps 775 queries 417.95 avg class size
c [sweep-11-1] 11353 decisions 730 SAT calls 144.87 avg env size
c [sweep-11-1] 28532 variables remain 58% (20615 retained 42%)
c [decomp-41] removed 225 variables
c [sweep-11-1] removed 225 vars (0 failed, 52 eqs, 90 impls)
c [sweep-11] removed 225 vars in TOTAL (1 rounds, 774 queries)
c [sort-queue-17] sorted 48966 enqueued variables after 88612 conflicts
c [score-dist-17] active 0 (0%), one 36891 (75%), zero 12075 (25%)
c [score-dist-17] max exp 1, different 2 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 3378 variables 6.5% (48966 remain 20%)
c [simplification-17] removed 30489 irredundant clauses 7.9% (356357 remain 26%)
c [simplification-17] maximum reduction of 8% = max (6%, 8%)
c [simplification-17] large reduction 8% >= 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 100612 (soft 90612 + delta 10000)
c [simplification-17] new conflict limit 90612 (hard 100612)
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  209.9   48965   356357     89785   27187   4360 792232   63   256   63  24%     42  102   49   30  166%
c 
c [simplification-18] limit 90612 conflicts (hard 100612) hit after 90612 conflicts
c [quatres-14] found 28135 quaternary clauses 57% in total
c [quatres-14-1] removed 2 duplicate quaternary clauses
c [quatres-14-2] added 1 single-self-subsuming ternary resolvents
c [quatres-14-2] added 4 quaternary resolvents
c [ternres-14] limit 32541874 with penalty 0 = 0 + 0
c [ternres-14] all 48938 free variables schedulable
c [ternres-14] 436 ternary resolvents (0 bin, 436 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-42] removed 28 variables
c [simpleprobe-7] all 48938 free variables schedulable
c [simpleprobe-7] limit 130167496 penalty 0 = 0 + 0
c [decomp-43] removed 375 variables
c [simpleprobe-7] 680 variables remain 1% (47883 retained 99%)
c [simpleprobe-7] removed 375 variables, found 101587 hbrs, 216 units
c [unhide-18] limit 6508374 with penalty 0 = 0 + 0
c [unhide-18-22] 5 units, 94 failed, 145694 tauts, 0 hbrs, 105773 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 162 transitive binary clauses
c [transred-14] found 1 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 813546850 steps penalty 1 = 1 + 0
c [cce-8-1] eliminated 4 clauses out of 5 (80%) of length 43
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 42
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 41
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 40
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 39
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 38
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 37
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 36
c [cce-8-1] eliminated 5 clauses out of 7 (71%) of length 35
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 34
c [cce-8-1] eliminated 5 clauses out of 7 (71%) of length 33
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 32
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 31
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 30
c [cce-8-1] eliminated 5 clauses out of 7 (71%) of length 29
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 28
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 27
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 26
c [cce-8-1] eliminated 5 clauses out of 7 (71%) of length 25
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 24
c [cce-8-1] eliminated 5 clauses out of 7 (71%) of length 23
c [cce-8-1] eliminated 4 clauses out of 8 (50%) of length 22
c [cce-8-1] eliminated 7 clauses out of 9 (78%) of length 21
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 20
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 19
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 18
c [cce-8-1] eliminated 5 clauses out of 10 (50%) of length 17
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 16
c [cce-8-1] eliminated 6 clauses out of 11 (55%) of length 15
c [cce-8-1] eliminated 6 clauses out of 13 (46%) of length 14
c [cce-8-1] eliminated 9 clauses out of 13 (69%) of length 13
c [cce-8-1] eliminated 6 clauses out of 10 (60%) of length 12
c [cce-8-1] eliminated 9 clauses out of 13 (69%) of length 11
c [cce-8-1] eliminated 6 clauses out of 17 (35%) of length 10
c [cce-8-1] eliminated 9 clauses out of 14 (64%) of length 9
c [cce-8-1] eliminated 6 clauses out of 11 (55%) of length 8
c [cce-8-1] eliminated 9 clauses out of 26 (35%) of length 7
c [cce-8-1] eliminated 35 clauses out of 2727 (1%) of length 6
c [cce-8-1] eliminated 2175 clauses out of 11037 (20%) of length 5
c [cce-8-1] eliminated 8606 clauses out of 25737 (33%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 11004 large clauses in 525087137 steps
c [cce-8-1] allowing another 262543568 steps for small clauses
c [cce-8-1] scheduling 195037 clauses = 172187 binary + 22850 ternary
c [cce-8-1] tried to eliminate 34037 small clauses 17%
c [cce-8-1] eliminated 6698 binary clauses 4%
c [cce-8-1] eliminated 1970 ternary clauses 9%
c [cce-8-1] eliminated 8668 small clauses 4%
c [cce-8-1] eliminated 9296 small clauses in 813546852 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 20300 covered clauses in round 1
c [cce-8] eliminated 20300 covered clauses in TOTAL during 1 rounds
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 48430 variables 100%
c [elim-15] limit of 650837481 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 1667 variables 3% in round 1 in 26374898 steps
c [elim-15-1] backward subsumption/strengthening limit 26374800
c [elim-15-1-1] backward checking 8660 touched variables 18%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 10 and strengthened 54 clauses in 1854707 steps
c [elim-15-1] rescheduled 160 variables 0% by backward subsumption
c [elim-15-2] eliminated 9 variables 0% in round 2 in 121880 steps
c [elim-15-2] backward subsumption/strengthening limit 121800
c [elim-15-2-1] backward checking 101 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 3 and strengthened 2 clauses in 114539 steps
c [elim-15-2] rescheduled 15 variables 0% by backward subsumption
c [elim-15-3] eliminated 1 variables 0% in round 3 in 92696 steps
c [elim-15-3] backward subsumption/strengthening limit 92600
c [elim-15-3-1] backward checking 10 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 0 and strengthened 2 clauses in 63383 steps
c [elim-15] incomplete 8 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 1677 = 3% variables out of 48430 scheduled
c [bca-14] limit of 10000000 steps and 651854 added (scaled 2)
c [bca-14] 67917 out of 93508 literals actually usable 73%
c [bca-14] added 100 blocked clauses in 167868 steps
c [sweep-12] limit 9762562 penalty 0 = 0 + 0
c [sweep-12-1] 3513 pos 12.8% + 23836 neg 87.2% = 27349 sched 58.5% ret 19404
c [sweep-12-1] 9764158 steps 187 queries 1372.13 avg class size
c [sweep-12-1] 3466 decisions 178 SAT calls 167.01 avg env size
c [sweep-12-1] 25652 variables remain 55% (21070 retained 45%)
c [decomp-44] removed 49 variables
c [sweep-12-1] removed 49 vars (0 failed, 10 eqs, 22 impls)
c [sweep-12] removed 49 vars in TOTAL (1 rounds, 186 queries)
c [sort-queue-18] sorted 46704 enqueued variables after 90612 conflicts
c [score-dist-18] active 0 (0%), one 35583 (76%), zero 11121 (24%)
c [score-dist-18] max exp 1, different 2 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 2234 variables 4.6% (46704 remain 19%)
c [simplification-18] removed 31399 irredundant clauses 8.8% (324958 remain 24%)
c [simplification-18] maximum reduction of 9% = max (5%, 9%)
c [simplification-18] large reduction 9% >= 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 102612 (soft 92612 + delta 10000)
c [simplification-18] new conflict limit 92612 (hard 102612)
c 
c [simplification-19] limit 92612 conflicts (hard 102612) hit after 92612 conflicts
c [quatres-15] found 19832 quaternary clauses 51% in total
c [quatres-15-1] removed 3 duplicate quaternary clauses
c [quatres-15-2] added 4 single-self-subsuming ternary resolvents
c [quatres-15-2] added 13 quaternary resolvents
c [ternres-15] limit 32931880 with penalty 0 = 0 + 0
c [ternres-15] all 46704 free variables schedulable
c [ternres-15] 519 ternary resolvents (0 bin, 519 trn)
c [ternres-15] fully completed ternary resolution
c [treelook-7] limit 3293188 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 75361 literals 81%
c [treelook-7] scheduling used 1954913 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 3293188 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 3306551 steps
c [treelook-7] 75254 literals remain 81%
c [treelook-7] 15497 variables remain to probed next time 33%
c [treelook-7] removed 14 variables, found 11287 hbrs
c [unhide-19] limit 6586376 with penalty 0 = 0 + 0
c [unhide-19-25] 2 units, 48 failed, 23333 tauts, 0 hbrs, 91274 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 146 transitive binary clauses
c [transred-15] found 1 units
c [cce-9] limit of 164659403 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 71
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 70
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 69
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 67
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 66
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 65
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 64
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 63
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 62
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 61
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 60
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 59
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 58
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 57
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 56
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 55
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 54
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 53
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 52
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 51
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 50
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 49
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 48
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 47
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 46
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 45
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 44
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 43
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 22
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 21
c [cce-9-1] eliminated 1 clauses out of 9 (11%) of length 14
c [cce-9-1] eliminated 3 clauses out of 14 (21%) of length 10
c [cce-9-1] eliminated 2 clauses out of 8 (25%) of length 9
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 8
c [cce-9-1] eliminated 2 clauses out of 27 (7%) of length 7
c [cce-9-1] eliminated 87 clauses out of 2799 (3%) of length 6
c [cce-9-1] eliminated 295 clauses out of 9325 (3%) of length 5
c [cce-9-1] eliminated 1 clauses out of 18218 (0%) of length 4
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 436 large clauses in 164659407 steps
c [cce-9-1] allowing another 82329703 steps for small clauses
c [cce-9-1] scheduling 271731 clauses = 160260 binary + 111471 ternary
c [cce-9-1] tried to eliminate 3226 small clauses 1%
c [cce-9-1] eliminated 387 binary clauses 0%
c [cce-9-1] eliminated 102 ternary clauses 0%
c [cce-9-1] eliminated 489 small clauses 0%
c [cce-9-1] eliminated 502 small clauses in 164659411 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 938 covered clauses in round 1
c [cce-9] eliminated 938 covered clauses in TOTAL during 1 rounds
c [cce-9] 938 < 1/100 * 322438 = 3224 considered unsuccessful
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 46660 variables 100%
c [elim-16] limit of 658637612 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 158 variables 0% in round 1 in 25282224 steps
c [elim-16-1] backward subsumption/strengthening limit 25282200
c [elim-16-1-1] backward checking 1377 touched variables 3%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 4 and strengthened 18 clauses in 444935 steps
c [elim-16-1] rescheduled 52 variables 0% by backward subsumption
c [elim-16-2] eliminated 5 variables 0% in round 2 in 54344 steps
c [elim-16-2] backward subsumption/strengthening limit 54300
c [elim-16-2-1] backward checking 81 touched variables 0%
c [elim-16-2-1] incomplete backward checking 1 remain 1%
c [elim-16-2] subsumed 3 and strengthened 3 clauses in 54331 steps
c [elim-16-2] rescheduled 16 variables 0% by backward subsumption
c [elim-16-3] eliminated 1 variables 0% in round 3 in 26898 steps
c [elim-16-3] backward subsumption/strengthening limit 26800
c [elim-16-3-1] backward checking 18 touched variables 0%
c [elim-16-3-1] incomplete backward checking 0 remain 0%
c [elim-16-3] subsumed 0 and strengthened 2 clauses in 26801 steps
c [elim-16] incomplete 8 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 164 = 0% variables out of 46660 scheduled
c [elim-16] 164 < 1/100 * 46660 = 466 considered unsuccessful
c [bca-15] limit of 10000000 steps and 643682 added (scaled 2)
c [bca-15] 66859 out of 92994 literals actually usable 72%
c [bca-15] added 167 blocked clauses in 167146 steps
c [sweep-13] limit 9879564 penalty 0 = 0 + 0
c [sweep-13-1] 3577 pos 14.0% + 21946 neg 86.0% = 25523 sched 54.9% ret 20973
c [sweep-13-1] 9921549 steps 216 queries 1314.56 avg class size
c [sweep-13-1] 3616 decisions 201 SAT calls 209.99 avg env size
c [sweep-13-1] 23934 variables remain 51% (22559 retained 49%)
c [decomp-47] removed 25 variables
c [sweep-13-1] removed 25 vars (0 failed, 15 eqs, 29 impls)
c [sweep-13] 25 < 1/1000 * 46496 = 46 considered unsuccessful
c [sweep-13] removed 25 vars in TOTAL (1 rounds, 215 queries)
c [sort-queue-19] sorted 46471 enqueued variables after 92612 conflicts
c [score-dist-19] active 0 (0%), one 35487 (76%), zero 10984 (24%)
c [score-dist-19] max exp 1, different 2 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 233 variables 0.5% (46471 remain 19%)
c [simplification-19] removed 3998 irredundant clauses 1.2% (320960 remain 24%)
c [simplification-19] maximum reduction of 1% = max (0%, 1%)
c [simplification-19] geometric conflict interval increment 12000 = 24000 / 2
c [simplification-19] new conflict interval 36000
c [simplification-19] penalized conflict interval 36000 = 1 * 36000
c [simplification-19] hard conflict limit 146612 (soft 128612 + delta 18000)
c [simplification-19] new conflict limit 128612 (hard 146612)
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  258.3   46470   320960    103580   32180   6710 693065   37   162   73  23%    175   -1   39   31  126%
c i  260.5   46469   320960    106242   34612   6756 693091   43   179   77  24%     15   17   58   32  184%
c i  263.5   46466   320960    109412   37539   6794 693133   45   184   82  24%      9   21   63   32  196%
c i  263.5   46461   320960    109413   37539   6794 693133   44   184   82  24%      9   21   63   32  195%
c i  268.8   46460   320960    114894   42669   6856 693183   42   177   84  24%     42   12   52   33  160%
c i  268.8   46459   320960    114895   42669   6856 693183   42   177   84  24%     42   12   52   33  159%
c i  269.6   46457   320960    115605   43319   6872 693186   43   187   87  23%     10   22   57   33  173%
c i  274.6   46456   320960    120236   47630   6937 693221   53   217   94  24%     29   49   41   35  119%
c i  275.0   46421   320960    120731   48073   6951 693228   53   217   94  24%      8   48   53   35  152%
c i  282.8   46420   320960    128409   55146   7037 693303   49   183  105  27%     73   11   61   36  169%
c 
c [simplification-20] limit 128632 conflicts (hard 146612) hit after 128634 conflicts
c [quatres-16] found 20151 quaternary clauses 48% in total
c [quatres-16-2] added 4 single-self-subsuming ternary resolvents
c [quatres-16-2] added 5 quaternary resolvents
c [ternres-16] limit 42368342 with penalty 0 = 0 + 0
c [ternres-16] all 46415 free variables schedulable
c [ternres-16] 234 ternary resolvents (0 bin, 234 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-6] limit 529604 penalty 4 = 4 + 0
c [gauss-6] extracted 6 xors of average arity 3.0
c [gauss-6] connected 18 occurrences of 18 variables (average 1.0)
c [gauss-6] limit 529604 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-7] limit 211841712 penalty 0 = 0 + 0
c [basicprobe-7-0] 425 probes remain 1% after last round
c [basicprobe-7-0] 806 units = 781 failed (97%) + 25 lifted (3%)
c [basicprobe-7-0] removed 1512 variables, found 415936 hbrs
c [bate-5] eliminated 826 asymmetric tautologies during probing
c [unhide-20] limit 2118417 with penalty 2 = 0 + 2
c [unhide-20-26] 0 units, 37 failed, 93896 tauts, 0 hbrs, 623340 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 172 transitive binary clauses
c [transred-16] found 1 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 44884 variables 100%
c [block-6] limit of 26480214 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 175 blocked clauses
c [block-6] 175 < 1/100 * 305605 = 3056 considered unsuccessful
c [bca-16] limit of 10000000 steps and 612184 added (scaled 2)
c [bca-16] 56318 out of 89770 literals actually usable 63%
c [bca-16] added 47 blocked clauses in 175777 steps
c [sort-queue-20] sorted 44884 enqueued variables after 128634 conflicts
c [score-dist-20] active 0 (0%), one 35383 (79%), zero 9501 (21%)
c [score-dist-20] max exp 1, different 2 (100%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 1531 variables 3.3% (44884 remain 18%)
c [simplification-20] removed 15728 irredundant clauses 4.9% (305232 remain 22%)
c [simplification-20] maximum reduction of 5% = max (3%, 5%)
c [simplification-20] large reduction 5% >= 5% limit
c [simplification-20] next conflict interval 2000 = 2000/1
c [simplification-20] penalized conflict interval 2000 = 1 * 2000
c [simplification-20] hard conflict limit 140634 (soft 130634 + delta 10000)
c [simplification-20] new conflict limit 130634 (hard 140634)
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  299.9   44883   305232    129300   55799   7576 966378   52   192  129  27%     17   20   62   37  169%
c 
c [simplification-21] limit 130634 conflicts (hard 140634) hit after 132059 conflicts
c [quatres-17] found 19397 quaternary clauses 47% in total
c [quatres-17-1] removed 1 duplicate quaternary clauses
c [quatres-17-2] added 7 single-self-subsuming ternary resolvents
c [ternres-17] limit 43357614 with penalty 0 = 0 + 0
c [ternres-17] all 44876 free variables schedulable
c [ternres-17] 217 ternary resolvents (0 bin, 217 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 1354925 penalty 4 = 4 + 0
c [card-6] found 1050 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 1354925 for elimination
c [card-6] 1050 out of 1050 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-49] removed 38 variables
c [simpleprobe-8] 629 schedulable variables 1%
c [simpleprobe-8] limit 173430456 penalty 0 = 0 + 0
c [decomp-50] removed 112 variables
c [simpleprobe-8] 1357 variables remain 3% (43377 retained 97%)
c [simpleprobe-8] removed 112 variables, found 84040 hbrs, 52 units
c [unhide-21] limit 2167880 with penalty 2 = 0 + 2
c [unhide-21-27] 0 units, 2 failed, 5467 tauts, 0 hbrs, 491384 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 184 transitive binary clauses
c [cce-10] limit of 108394035 steps penalty 1 = 1 + 0
c [cce-10-1] eliminated 1 clauses out of 7 (14%) of length 18
c [cce-10-1] eliminated 1 clauses out of 7 (14%) of length 14
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 8
c [cce-10-1] eliminated 1 clauses out of 2711 (0%) of length 6
c [cce-10-1] eliminated 12 clauses out of 8595 (0%) of length 5
c [cce-10-1] incomplete large round (ATE)
c [cce-10-1] eliminated 17 large clauses in 108394036 steps
c [cce-10-1] allowing another 54197018 steps for small clauses
c [cce-10-1] scheduling 253810 clauses = 157934 binary + 95876 ternary
c [cce-10-1] tried to eliminate 2620 small clauses 1%
c [cce-10-1] eliminated 313 binary clauses 0%
c [cce-10-1] eliminated 75 ternary clauses 0%
c [cce-10-1] eliminated 388 small clauses 0%
c [cce-10-1] eliminated 397 small clauses in 108394037 steps
c [cce-10-1] incomplete small round (ATE)
c [cce-10-1] eliminated 414 covered clauses in round 1
c [cce-10] eliminated 414 covered clauses in TOTAL during 1 rounds
c [cce-10] 414 < 1/100 * 300601 = 3006 considered unsuccessful
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 44733 variables 100%
c [elim-17] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 449 variables 1% in round 1 in 23056346 steps
c [elim-17-1] backward subsumption/strengthening limit 23056300
c [elim-17-1-1] backward checking 2863 touched variables 6%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 26 clauses in 759941 steps
c [elim-17-1] rescheduled 58 variables 0% by backward subsumption
c [elim-17-2] eliminated 5 variables 0% in round 2 in 36515 steps
c [elim-17-2] backward subsumption/strengthening limit 36500
c [elim-17-2-1] backward checking 62 touched variables 0%
c [elim-17-2-1] incomplete backward checking 0 remain 0%
c [elim-17-2] subsumed 0 and strengthened 2 clauses in 36501 steps
c [elim-17-2] rescheduled 8 variables 0% by backward subsumption
c [elim-17-3] eliminated 1 variables 0% in round 3 in 16658 steps
c [elim-17-3] backward subsumption/strengthening limit 16600
c [elim-17-3-1] backward checking 10 touched variables 0%
c [elim-17-3-1] incomplete backward checking 1 remain 10%
c [elim-17-3] subsumed 0 and strengthened 1 clauses in 16666 steps
c [elim-17] incomplete 4 not tried 0% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 455 = 1% variables out of 44733 scheduled
c [bca-17] limit of 10000000 steps and 600735 added (scaled 2)
c [bca-17] 55468 out of 88558 literals actually usable 63%
c [bca-17] added 12 blocked clauses in 173900 steps
c [sweep-14] limit 6503642 penalty 1 = 1 + 0
c [sweep-14-1] 3135 pos 13.5% + 20014 neg 86.5% = 23149 sched 52.3% ret 21129
c [sweep-14-1] 6565487 steps 150 queries 1595.47 avg class size
c [sweep-14-1] 3175 decisions 139 SAT calls 191.14 avg env size
c [sweep-14-1] 22186 variables remain 50% (22081 retained 50%)
c [decomp-51] removed 55 variables
c [sweep-14-1] removed 55 vars (0 failed, 10 eqs, 16 impls)
c [sweep-14] removed 55 vars in TOTAL (1 rounds, 149 queries)
c [sort-queue-21] sorted 44223 enqueued variables after 132059 conflicts
c [score-dist-21] active 0 (0%), one 34946 (79%), zero 9277 (21%)
c [score-dist-21] max exp 1, different 2 (100%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 653 variables 1.5% (44223 remain 18%)
c [simplification-21] removed 5881 irredundant clauses 1.9% (299351 remain 22%)
c [simplification-21] maximum reduction of 2% = max (1%, 2%)
c [simplification-21] geometric conflict interval increment 12000 = 36000 / 3
c [simplification-21] new conflict interval 48000
c [simplification-21] penalized conflict interval 48000 = 1 * 48000
c [simplification-21] hard conflict limit 204059 (soft 180059 + delta 24000)
c [simplification-21] new conflict limit 180059 (hard 204059)
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  315.0   44222   299351    132191   54726   7390 1004839   56   208  117  27%      2   35   75   38  200%
c i  317.3   44221   299351    134120   56480   7415 1004859   59   214  117  28%    -10   40   65   38  169%
c i  317.3   44217   299351    134126   56483   7415 1004861   59   214  117  28%    -10   40   64   38  166%
c i  319.5   44216   299351    135920   58089   7424 1004876   61   219  117  28%    -12   43   51   39  130%
c i  324.1   44207   299351    139778   61646   7454 1004896   63   218  117  29%     15   40   75   41  183%
c i  325.2   44206   299351    140735   62511   7461 1004905   66   222  117  30%     -7   44   73   41  177%
c -  325.6   44196   299351    140991   24754   7462 1004907   66   223   58  29%    -12   44   64   41  154%
c i  336.8   44195   299351    152565   35436   7588 1004983   57   208   77  27%    130   22   33   44   75%
c i  339.1   44183   299351    155340   37921   7599 1004999   55   188   77  29%     -0    1   62   45  138%
c i  339.8   44181   299351    155910   38417   7606 1005006   60   201   78  30%    -15   14   94   45  208%
c i  350.3   44142   299351    166703   48272   7684 1005081   54   175  100  31%    107   -9   56   46  123%
c i  350.3   44140   299351    166704   48272   7684 1005081   54   175  100  31%    107   -9   56   46  123%
c i  350.3   44139   299351    166705   48272   7684 1005081   54   175  100  31%    107   -9   56   46  122%
c i  360.4   44138   299351    176500   57130   7768 1005138   46   129  116  35%     87  -55   41   47   87%
c i  362.1   44123   299351    178443   58916   7784 1005151   42   112  116  38%    -13  -71   28   47   60%
c 
c [simplification-22] limit 180080 conflicts (hard 204059) hit after 184853 conflicts
c [quatres-18] found 19464 quaternary clauses 44% in total
c [quatres-18-2] added 2 single-self-subsuming ternary resolvents
c [quatres-18-2] added 4 quaternary resolvents
c [ternres-18] limit 57562706 with penalty 0 = 0 + 0
c [ternres-18] all 44113 free variables schedulable
c [ternres-18] 222 ternary resolvents (0 bin, 222 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-52] removed 112 variables
c [treelook-8] limit 5756270 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 70802 literals 80%
c [treelook-8] scheduling used 2286336 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 5756270 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 5764886 steps
c [treelook-8] 70675 literals remain 80%
c [treelook-8] 14258 variables remain to probed next time 32%
c [treelook-8] removed 18 variables, found 22284 hbrs
c [unhide-22] limit 2878135 with penalty 2 = 0 + 2
c [unhide-22-28] 0 units, 8 failed, 56800 tauts, 0 hbrs, 724467 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 192 transitive binary clauses
c [elim-18] no untried remaining variables left
c [elim-18] scheduled 44074 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 16000000000 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 46 variables 0% in round 1 in 22972959 steps
c [elim-18-1] backward subsumption/strengthening limit 22972900
c [elim-18-1-1] backward checking 384 touched variables 1%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 1 and strengthened 2 clauses in 147962 steps
c [elim-18-1] rescheduled 11 variables 0% by backward subsumption
c [elim-18-2] no variable eliminated in round 2 in 14945 steps
c [elim-18] fully completed in 2 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 46 = 0% variables out of 44074 scheduled
c [elim-18] 46 < 1/100 * 44074 = 440 considered unsuccessful
c [bca-18] limit of 10000000 steps and 597967 added (scaled 2)
c [bca-18] 54416 out of 88058 literals actually usable 62%
c [bca-18] added 53 blocked clauses in 180897 steps
c [sweep-15] limit 17268811 penalty 0 = 0 + 0
c [sweep-15-1] 2993 pos 13.6% + 19020 neg 86.4% = 22013 sched 50.0% ret 22015
c [sweep-15-1] 17299390 steps 329 queries 477.31 avg class size
c [sweep-15-1] 9363 decisions 315 SAT calls 244.51 avg env size
c [sweep-15-1] 19115 variables remain 43% (24911 retained 57%)
c [decomp-54] removed 19 variables
c [sweep-15-1] removed 19 vars (0 failed, 15 eqs, 29 impls)
c [sweep-15] 19 < 1/1000 * 44028 = 44 considered unsuccessful
c [sweep-15] removed 19 vars in TOTAL (1 rounds, 328 queries)
c [sort-queue-22] sorted 44009 enqueued variables after 184853 conflicts
c [score-dist-22] active 0 (0%), one 35124 (80%), zero 8885 (20%)
c [score-dist-22] max exp 1, different 2 (100%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 104 variables 0.2% (44009 remain 18%)
c [simplification-22] removed 1283 irredundant clauses 0.4% (298068 remain 22%)
c [simplification-22] maximum reduction of 0% = max (0%, 0%)
c [simplification-22] full geometric conflict interval increment 48000
c [simplification-22] new conflict interval 96000
c [simplification-22] penalized conflict interval 96000 = 1 * 96000
c [simplification-22] hard conflict limit 328853 (soft 280853 + delta 48000)
c [simplification-22] new conflict limit 280853 (hard 328853)
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 -  380.9   44009   298068    186735   30469   7820 972571   65   193   60  33%     62   13   81   49  166%
c i  383.9   44008   298068    189569   33062   7844 972593   70   214   69  32%    103   33   62   50  124%
c i  394.2   44006   298068    199152   41816   7905 972642   59   168   87  35%     76  -15   65   51  127%
c i  410.0   43986   298068    213652   55036   7999 972713   72   214  126  34%    142   34   68   53  128%
c i  415.2   43955   298068    217893   58850   8024 972738   79   218  130  36%    -15   35  180   55  326%
c -  429.3   43954   298068    229151   33543   8101 972779   58   157   61  37%     89  -25   48   56   85%
c i  452.9   43953   298068    249926   51943   8226 972873   72   190  104  38%    343    4   80   61  131%
c -  478.6   43948   298068    271344   35098   8325 972956   67   173   62  39%    166  -13   46   64   73%
c 
c [simplification-23] limit 280853 conflicts (hard 328853) hit after 283920 conflicts
c [quatres-19] found 19688 quaternary clauses 44% in total
c [quatres-19-1] removed 1 duplicate quaternary clauses
c [quatres-19-1] added 1 double-self-subsuming ternary resolvents
c [quatres-19-2] added 2 single-self-subsuming ternary resolvents
c [quatres-19-2] added 5 quaternary resolvents
c [ternres-19] limit 86053992 with penalty 0 = 0 + 0
c [ternres-19] all 43948 free variables schedulable
c [ternres-19] 174 ternary resolvents (0 bin, 174 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-55] removed 63 variables
c [basicprobe-8] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 1889 sched 4%, 382 failed, 69 lifted, 75446 hbrs
c [decomp-56] removed 1172 variables
c [basicprobe-8-1] 14417 sched 34%, 212 failed, 2 lifted, 202795 hbrs
c [decomp-57] removed 356 variables
c [basicprobe-8-2] 12558 probes remain 30% after last round
c [basicprobe-8-2] 669 units = 598 failed (89%) + 71 lifted (11%)
c [basicprobe-8-2] removed 1532 variables, found 285182 hbrs
c [bate-6] eliminated 341 asymmetric tautologies during probing
c [unhide-23] limit 4302699 with penalty 2 = 0 + 2
c [unhide-23-30] 0 units, 3 failed, 70812 tauts, 0 hbrs, 1218502 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 188 transitive binary clauses
c [bca-19] limit of 10000000 steps and 552058 added (scaled 2)
c [bca-19] 53866 out of 84824 literals actually usable 64%
c [bca-19] added 18 blocked clauses in 161217 steps
c [sort-queue-23] sorted 42411 enqueued variables after 283920 conflicts
c [score-dist-23] active 0 (0%), one 35155 (83%), zero 7256 (17%)
c [score-dist-23] max exp 1, different 2 (100%)
c [score-dist-23] median active exp 0, avg 0.0
c [simplification-23] removed 1537 variables 3.5% (42411 remain 17%)
c [simplification-23] removed 22927 irredundant clauses 7.7% (275141 remain 20%)
c [simplification-23] maximum reduction of 8% = max (3%, 8%)
c [simplification-23] large reduction 8% >= 5% limit
c [simplification-23] next conflict interval 2839 = min (283920/100, 96000)
c [simplification-23] penalized conflict interval 2839 = 1 * 2839
c [simplification-23] hard conflict limit 296759 (soft 286759 + delta 10000)
c [simplification-23] new conflict limit 286759 (hard 296759)
c 
c [simplification-24] limit 286759 conflicts (hard 296759) hit after 296761 conflicts
c [quatres-20] found 19466 quaternary clauses 43% in total
c [quatres-20-1] removed 3 duplicate quaternary clauses
c [ternres-20] limit 89402813 with penalty 0 = 0 + 0
c [ternres-20] all 42411 free variables schedulable
c [ternres-20] 55 ternary resolvents (0 bin, 55 trn)
c [ternres-20] fully completed ternary resolution
c [simpleprobe-9] 1278 schedulable variables 3%
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-59] removed 41 variables
c [simpleprobe-9] 1354 variables remain 3% (41016 retained 97%)
c [simpleprobe-9] removed 41 variables, found 57235 hbrs, 16 units
c [unhide-24] limit 4470140 with penalty 2 = 0 + 2
c [unhide-24-31] 0 units, 0 failed, 55121 tauts, 0 hbrs, 1156530 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 105 transitive binary clauses
c [cce-11] limit of 111753516 steps penalty 2 = 2 + 0
c [cce-11-1] eliminated 2 clauses out of 3 (67%) of length 39
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 38
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 37
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 36
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 35
c [cce-11-1] eliminated 1 clauses out of 6 (17%) of length 34
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 33
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 32
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 31
c [cce-11-1] eliminated 1 clauses out of 3 (33%) of length 30
c [cce-11-1] eliminated 1 clauses out of 3 (33%) of length 29
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 28
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 27
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 26
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 25
c [cce-11-1] eliminated 1 clauses out of 7 (14%) of length 24
c [cce-11-1] eliminated 3 clauses out of 7 (43%) of length 23
c [cce-11-1] eliminated 1 clauses out of 6 (17%) of length 22
c [cce-11-1] eliminated 3 clauses out of 6 (50%) of length 21
c [cce-11-1] eliminated 2 clauses out of 7 (29%) of length 20
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 19
c [cce-11-1] eliminated 1 clauses out of 9 (11%) of length 18
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 17
c [cce-11-1] eliminated 1 clauses out of 6 (17%) of length 16
c [cce-11-1] eliminated 1 clauses out of 8 (12%) of length 15
c [cce-11-1] eliminated 2 clauses out of 9 (22%) of length 14
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 13
c [cce-11-1] eliminated 2 clauses out of 10 (20%) of length 12
c [cce-11-1] eliminated 4 clauses out of 7 (57%) of length 11
c [cce-11-1] eliminated 4 clauses out of 20 (20%) of length 10
c [cce-11-1] eliminated 8 clauses out of 15 (53%) of length 9
c [cce-11-1] eliminated 5 clauses out of 19 (26%) of length 8
c [cce-11-1] eliminated 12 clauses out of 40 (30%) of length 7
c [cce-11-1] eliminated 9 clauses out of 2747 (0%) of length 6
c [cce-11-1] eliminated 33 clauses out of 8544 (0%) of length 5
c [cce-11-1] eliminated 12 clauses out of 16808 (0%) of length 4
c [cce-11-1] incomplete large round (ACCE)
c [cce-11-1] eliminated 124 large clauses in 111753516 steps
c [cce-11-1] allowing another 55876758 steps for small clauses
c [cce-11-1] scheduling 170294 clauses = 154218 binary + 16076 ternary
c [cce-11-1] tried to eliminate 4633 small clauses 3%
c [cce-11-1] eliminated 885 binary clauses 1%
c [cce-11-1] eliminated 136 ternary clauses 1%
c [cce-11-1] eliminated 1021 small clauses 1%
c [cce-11-1] eliminated 1021 small clauses in 111753522 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 1145 covered clauses in round 1
c [cce-11] eliminated 1145 covered clauses in TOTAL during 1 rounds
c [cce-11] 1145 < 1/100 * 274814 = 2748 considered unsuccessful
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 42370 variables 100%
c [elim-19] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 381 variables 1% in round 1 in 20323936 steps
c [elim-19-1] backward subsumption/strengthening limit 20323900
c [elim-19-1-1] backward checking 2557 touched variables 6%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 2 and strengthened 3 clauses in 579898 steps
c [elim-19-1] rescheduled 14 variables 0% by backward subsumption
c [elim-19-2] eliminated 1 variables 0% in round 2 in 21519 steps
c [elim-19-2] backward subsumption/strengthening limit 21500
c [elim-19-2-1] backward checking 10 touched variables 0%
c [elim-19-2-1] incomplete backward checking 6 remain 60%
c [elim-19-2] subsumed 0 and strengthened 2 clauses in 21521 steps
c [elim-19-2] rescheduled 8 variables 0% by backward subsumption
c [elim-19-3] eliminated 1 variables 0% in round 3 in 19372 steps
c [elim-19-3] backward subsumption/strengthening limit 19300
c [elim-19-3-1] backward checking 13 touched variables 0%
c [elim-19-3-1] incomplete backward checking 4 remain 31%
c [elim-19-3] subsumed 0 and strengthened 1 clauses in 19382 steps
c [elim-19] incomplete 4 not tried 0% in round 3
c [elim-19] transition to [ all 1 rem 1 ] state
c [elim-19] eliminated 383 = 1% variables out of 42370 scheduled
c [elim-19] 383 < 1/100 * 42370 = 423 considered unsuccessful
c [bca-20] limit of 10000000 steps and 548147 added (scaled 2)
c [bca-20] 52287 out of 83976 literals actually usable 62%
c [bca-20] added 14 blocked clauses in 166779 steps
c [sweep-16] limit 13410422 penalty 1 = 1 + 0
c [sweep-16-1] 2866 pos 15.3% + 15847 neg 84.7% = 18713 sched 44.6% ret 23274
c [sweep-16-1] 13439983 steps 339 queries 405.99 avg class size
c [sweep-16-1] 6651 decisions 320 SAT calls 154.65 avg env size
c [sweep-16-1] 16686 variables remain 40% (25301 retained 60%)
c [decomp-60] removed 22 variables
c [sweep-16-1] removed 22 vars (0 failed, 20 eqs, 34 impls)
c [sweep-16] 22 < 1/1000 * 41987 = 41 considered unsuccessful
c [sweep-16] removed 22 vars in TOTAL (1 rounds, 338 queries)
c [sort-queue-24] sorted 41965 enqueued variables after 296761 conflicts
c [score-dist-24] active 0 (0%), one 34879 (83%), zero 7086 (17%)
c [score-dist-24] max exp 1, different 2 (100%)
c [score-dist-24] median active exp 0, avg 0.0
c [simplification-24] removed 446 variables 1.1% (41965 remain 17%)
c [simplification-24] removed 1986 irredundant clauses 0.7% (273155 remain 20%)
c [simplification-24] maximum reduction of 1% = max (1%, 1%)
c [simplification-24] geometric conflict interval increment 48000 = 96000 / 2
c [simplification-24] new conflict interval 144000
c [simplification-24] penalized conflict interval 144000 = 1 * 144000
c [simplification-24] hard conflict limit 512761 (soft 440761 + delta 72000)
c [simplification-24] new conflict limit 440761 (hard 512761)
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 -  566.0   41965   273155    315501   36169   8438 1095426   88   215   63  41%    587   39  106   67  159%
c -  614.6   41965   273155    358135   38150   8611 1095543   78   181   64  43%    796   11   61   67   91%
c i  657.6   41964   273155    395931   71522   8759 1095625   61   149  166  41%    896  -12   69   65  106%
c i  660.0   41963   273155    397868   73159   8773 1095628   63   151  166  42%  -1001   -9   57   65   87%
c -  664.0   41806   273155    400658   40075   8783 1095643   71   172   65  41%  -1256   12   59   66   89%
c -  715.1   41806   273155    443155   41174   8973 1095736   64   141   65  46%   -181  -18   39   67   59%
c i  715.3   41805   273155    443312   41317   8973 1095736   63   138   74  46%   -178  -20   37   67   55%
c i  732.6   41804   273155    458576   54595   9021 1095778   76   165  101  46%   -500    6  101   69  147%
c i  747.8   41803   273155    471181   65571   9076 1095821   78   173  129  45%   -433   14   88   69  128%
c i  757.7   41802   273155    478616   71971   9090 1095835   85   190  147  45%   -455   28   74   71  105%
c i  763.8   41801   273155    483164   75866   9116 1095845   64   129  153  49%   -465  -33   41   70   59%
c i  768.6   41751   273155    487213   79319   9131 1095859   70   145  153  49%   -444  -16   69   70   99%
c -  769.4   41749   273155    487696   42492   9133 1095860   72   147  102  49%   -457  -13   91   70  130%
c i  770.4   41748   273155    488538   43194   9135 1095863   80   169  113  48%   -461    8  125   71  176%
c 
c [simplification-25] limit 440761 conflicts (hard 512761) hit after 512762 conflicts
c [ternres-21] limit 147729427 with penalty 0 = 0 + 0
c [ternres-21] all 41566 free variables schedulable
c [ternres-21] 260 ternary resolvents (0 bin, 260 trn)
c [ternres-21] fully completed ternary resolution
c [decomp-61] removed 404 variables
c [treelook-9] limit 14772942 penalty 0 = 0 + 0 boost 1
c [treelook-9] scheduled 65681 literals 79%
c [treelook-9] scheduling used 2178519 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 14772942 penalty 0 = 0 + 0 boost 1
c [treelook-9] used 14808344 steps
c [treelook-9] 65317 literals remain 79%
c [treelook-9] 12279 variables remain to probed next time 30%
c [decomp-62] removed 2 variables
c [treelook-9] removed 6 variables, found 50750 hbrs
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 128 transitive binary clauses
c [bca-21] limit of 10000000 steps and 536790 added (scaled 2)
c [bca-21] 50011 out of 83112 literals actually usable 60%
c [bca-21] added 3 blocked clauses in 170920 steps
c [sort-queue-25] sorted 41555 enqueued variables after 512762 conflicts
c [score-dist-25] active 0 (0%), one 35104 (84%), zero 6451 (16%)
c [score-dist-25] max exp 1, different 2 (100%)
c [score-dist-25] median active exp 0, avg 0.0
c [simplification-25] removed 11 variables 0.0% (41555 remain 17%)
c [simplification-25] removed 5656 irredundant clauses 2.1% (267499 remain 20%)
c [simplification-25] maximum reduction of 2% = max (0%, 2%)
c [simplification-25] geometric conflict interval increment 48000 = 144000 / 3
c [simplification-25] new conflict interval 192000
c [simplification-25] penalized conflict interval 192000 = 1 * 192000
c [simplification-25] hard conflict limit 800762 (soft 704762 + delta 96000)
c [simplification-25] new conflict limit 704762 (hard 800762)
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  809.9   41554   267499    520821   70592   9423 1133353   70   143  135  49%     93  -14   59   71   84%
c -  824.7   41554   267499    532832   44138   9459 1133386   60   138   66  43%   -178  -15   53   69   76%
c i  852.8   41553   267499    557507   65814   9541 1133432   65   150  127  43%    199   -6   80   70  115%
c i  868.0   41552   267499    569062   75702   9589 1133478   67   132  169  51%   -156  -21   79   69  114%
c i  875.7   41200   267499    574591   80691   9610 1133492   71   154  173  46%   -228    4   89   68  130%
c i  877.7   41199   267499    576274   82080   9620 1133493   69   143  173  48%   -265   -6   62   68   91%
c -  879.0   41182   267499    577311   45213   9623 1133493   71   145   67  49%   -272   -5  100   68  147%
c i  910.0   41181   267499    602873   67375   9688 1133544   83   188  129  44%    136   36  127   70  181%
c i  930.1   41149   267499    617624   79955   9726 1133575   74   157  161  47%    -22    1   81   71  115%
c -  936.8   41149   267499    622263   44914   9741 1133585   86   191   66  45%   -167   36  113   72  157%
c i  938.6   41148   267499    623894   46292   9747 1133590   87   192   77  45%   -139   36  120   73  165%
c i  978.3   41146   267499    657146   74729   9857 1133664   72   152  142  48%    263    1   87   70  123%
c -  994.2   41146   267499    669074   46819   9891 1133686   60   109   67  55%    -50  -42   60   70   85%
c i  995.2   41145   267499    669815   47515   9894 1133686   58   106   79  55%    -38  -45   49   70   71%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 3137 basic ate = 2449 trn 78% + 688 lrg 22% in 6 updates
c bcas: 21 count, 2587 added (2145 skipped), 5443828 steps
c bkwd: tried 455667 clauses, 910865 lits, 2.00 lits/clause
c bkwd: checked 13489062 occs, 29.60 occs/clause, 14.81 occs/lit
c bkwd: subsumed 32 binary, 98 ternary, 49 large
c bkwd: strengthened 3 binary, 0 ternary (0% self), 524 large (0% self)
c blkd: 6 bces, 11536 removed, 10219375 resolutions, 28478172 steps
c blkd: 15047 blocking literals 3%, 52 pure
c bump: 672960 bumped seen, 458073157 lits 680.7 on average
c card: 6 count, 0 units, 0 am1, 398378793 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 72211 subsumed
c card: 16919 at-most-one constraints found, average size 4.84
c card: 16919 at-most-one constraints used 100%, average size 4.84
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: 11 cces, 47986 eliminated, 47599 ate 99%, 387 abce 1%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 4677859 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 182 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 62 decompositions, 9181 equivalent 4%
c deco: 68798 decision-only clauses 10%, 73% reduction
c decs: 8576469 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 19 elims, 107593 eliminated 42%, 43 pure 0%
c elms: 53 rounds, 2.8 rounds/bve
c elms: 85328 small 79%, 22170 large 21%
c elms: 241187 tried small, 85331 succeeded 35%, 155856 failed 65%
c elms: 54147 subsumed, 74302 strengthened, 2370 blocked
c elms: 27235028 copies, 26639519 resolutions, 6615844 ipos
c elms: 7094353 subchks, 4086983 strchks
c gaus: 6 extractions, 484 extracted, 2.5 size, 3 max
c gaus: exported 1 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 13219482 steps, 6609741 extr 50%, 4394 elim 0%
c glue: 61.9 orig avg, 61.9 real avg, 5.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 2296514 = 413785 simple 18% + 1843652 trn 80% + 39077 lrg 2%, 5277 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 672960 clauses, 362.3 length
c lrnd: 243812322 lits = 329568850 orig - 85756528 removed 26%
c lrnd: 298912 uips 44%, 314060 flips 47%
c mins: 578944 mins 88%, 4345 bin 1%, 8838 size 1%
c mins: 488753352 poisoned searches, 119346820 hits, 24% hit rate
c mins: 557044568 used twice searches, 17177161 hits, 3% hit rate
c move: moved 31525, 20134 bin 64%, 11391 trn 36%
c otfs: 1839 driving 19%, 7722 restarting 81%
c otfs: str 9561, 9383 red 98%, 178 irr 2%
c otfs: str 9561, 0 bin 0%, 211 trn 2%, 9350 lrg 98%
c otfs: sub 28, 27 red 96%, 1 irr 4%
c otfs: sub 28, 0 bin 0%, 4 trn 14%, 24 lrg 86%
c phas: 12 computed, 154441 set, 3 pos (0%), 154438 neg (100%)
c prbs: 8 basic, 69641 probed, 2911 failed, 136 lifted
c prbs: 9 simple, 794049 probed, 797 failed, 708 eqs
c prbs: 9 treelook, 652 probed, 45 failed, 0 lifted
c prom: 180026 locked 7% out of 2401804 tried
c prps: 2163191948 props, 243 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c quat: 20 count, 103 quat, 46 self1, 2 self2, 1194 dup
c queu: 25 sorted, 8576469 next (3 steps 0.00)
c queu: 460023157 enq (460023106 steps 1.00), 458073157 deq 100%
c redc: 10069 clauses 27%, 36650 tried 5%, 141 sat 0%
c redc: 25280 lits 6%, 411356 tried 0%, 141 sat 0%
c redc: 1347 times jump level reduced, 21.2 levels on average
c reds: 13 count, 51817.2 conflicts per reduce
c reds: 0 memlim 0%, 13 arith 100%
c reds: 364063 collected 76%, 113108 retired 24%
c rmbd: 54859 removed, 5551 red 10%
c rsts: 18341 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: 25 count, 22 confs 88%, 0 vars 0%
c simp: 2 its 8%, 1 bin 4%, 0 trns 0%
c subl: 672960 count (935235 tried 1.4), 63922 sub out of 660071 (9.7%)
c swps: 16 count, 16 rounds, 2399 queries (149.9/round)
c swps: 2242 sat calls, 34 unsat (0.5% success rate)
c swps: 42539 decisions 19.0, 1176 conflicts 0.5
c swps; 2033.8 avg class size, 170.9 avg environment size
c swps: 0 failed, 333 impls, 178 equivs
c swp0: 794 type 0 queries, 210 unsat (26.4%), 767 sat (96.6%)
c swp1: 1605 type 1 queries, 777 unsat (48.4%), 1454 sat (90.6%)
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: 18499884 calls to obtain time
c tops: 100862 fixed 39%, 546 its, 1233.74 confs/it
c trds: 21 transitive reductions, 3933 removed, 51 failed
c trds: 20803 nodes, 60866 edges, 41255105 steps
c trim: 2554420 words, 9.7 MB
c trnr: 21 count, 6 bin, 4006 trn, 238173930 steps
c unhd: 24 count, 31 rounds, 101133667 steps
c unhd: 698 non-trivial sccs of average size 2.3
c unhd: 176 units, 176 bin, 0 trn, 0 lrg
c unhd: 8628 failed, 8543 stamp, 0 lits, 36 bin, 41 trn, 0 lrg
c unhd: 759793 tauts, 26455 bin 3%, 13564 trn 2%, 879 lrg 0%
c unhd: 759793 tauts, 718895 stamp 95%, 670609 red 88%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 5130429 str, 176 bin 0%, 3319 trn 0%, 5126934 lrg 100%, 5108385 red 100%
c vars: 41145 remaining 16% and 217636 removed 84% out of 258781
c vars: 100862 fixed 39%, 107593 eliminated 42%, 9181 equivalent 4%
c vsts: 19850192379 visits, 96% srch, 4% simp, 0% lkhd
c vsts: 9.2 search visits per propagation, 28327.5 per conflict
c wchs: 2582227430 pushed, 69532956 enlarged, 269 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         660175        364063        113108      64572775       7657578        354658
c 
c  0 0         49225   7     15776   4         0   0  37110985  57   3195693  42     77654  22     2.8
c  1 5         19779   3     10120   3      2846   3   4596122   7    586354   8     25077   7     1.2
c  2 6         53346   8     31974   9      7709   7   6349071  10<   813845  11<    41684  12     3.8
c  3 9         60567   9     37855  10      9210   8   4437821   7    640479   8     35543  10     6.0
c  4 14        56815   9     35621  10      8938   8   3750414   6    595609   8     33197   9<    6.9
c  5 21        60287   9     38612  11     10166   9   2896620   4    529980   7     30923   9     8.3
c  6 30        63697  10<    41758  11<    11243  10   2164639   3    418771   5     28227   8    10.0
c  7 41        61668   9     41440  11     11290  10<  1356180   2    302288   4     23734   7    12.6
c  8 54        55756   8     37337  10     10935  10    819767   1    213525   3     18250   5    12.5
c  9 69        46196   7     30607   8      9749   9    427249   1    129569   2     13871   4    11.5
c 10 86        46216   7     25915   7      9788   9    430429   1    129381   2     13430   4     8.3
c 11 126       48422   7     11081   3     10477   9    169895   0     70050   1      9029   3     3.6
c 12 230       35984   5      5595   2     10082   9     60808   0     30443   0      3833   1     4.5
c 13 534        2217   0       372   0       675   1      2775   0      1591   0       206   0     0.6
c 
c avg                  6.0           5.7           7.0           1.5           2.5           3.9
c std                  3.5           3.0           3.2           2.3           2.9           3.3
c 
c   64.565   6% probe
c   64.398   6% bump
c   46.444   5% cce
c   28.928   3% unhide
c   23.683   2% elim
c   14.246   1% sweep
c    5.597   1% decide
c    4.803   0% bca
c 
c   11.383 < 1% rest (below)
c 
c    3.098   0% block
c    2.891   0% transred
c    2.267   0% gauss
c    1.610   0% ternres
c    1.129   0% quatres
c    0.388   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.122   1% preprocessing     2%
c  204.549  20% inprocessing     98%
c ==================================
c  209.671  21% simplifying
c  789.608  79% search
c ==================================
c  999.283 100% all
c 
c        673623 conflicts,         674.1 confs/sec
c          6316 ternaries,         106.7 confs/ternary
c          5730 binaries,          117.6 confs/binary
c           546 iterations,       1233.7 confs/iteration
c 
c            13 reductions,          0.0 redus/sec,  51817.2 confs/reduction
c         18341 restarts,           18.4 rests/sec,     36.7 confs/restart
c       8576469 decisions,        8582.6 decis/sec,     12.7 decis/conflict
c    2163191948 propagations,  2164743.7 props/sec,    252.2 props/decision
c 
c 999.3 seconds, 190.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
