c launch: /data/cnf/sc2014/app/UR-20-10p1.cnf.bz2
c host: atom31
c Lingeling SAT Solver
c 
c Version b7ztzud 55d9a3e9649fc56eacf3e72d8e2e2d5c615d5f18
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Fri May  1 11:44:04 CEST 2015
c compiled Fri May  1 11:44:04 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-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/UR-20-10p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UR-20-10p1.cnf.bz2
c no embedded options
c found 'p cnf 259234 1387934' header
c read 259234 variables, 1387934 clauses, 3351923 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 --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 246085 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 [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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  246085  1373915         0       0      0     0    0     0   57   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 6535 at-most-one constraints of average size 5.7
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6535 out of 6535 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 62780 variables
c [simpleprobe-1] all 196454 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 144 variables
c [simpleprobe-1] 15292 variables remain 8% (181018 retained 92%)
c [simpleprobe-1] removed 144 variables, found 17443 hbrs, 1 units
c [unhide-1] limit 66116 based on 1057870 irredundant clauses
c [unhide-1-1] 1 units, 672 failed, 9916 tauts, 0 hbrs, 9346 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 195745 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 62823 not tried 32% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 74694 = 38% variables out of 195745 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 889020 negative 99.3% of 895640 except 6620 0.7%
c [phase-count-1] 723947 positive 80.8% of 895640 except 171693 19.2%
c [phase-count-1] less non-negative clauses 6620 than limit 89500 (10.0%)
c [phase-count-1] non-pos/non-neg = 171693/6620 = 25.94 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 121051 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 121051 zero 100.00%
c [score-distribution-1] 1 different 0.00% out of total 121051 variables
c [simplification-1] removed 81605 variables 40.3% (121051 remain 49%)
c [simplification-1] removed 478275 irredundant clauses 34.8% (895640 remain 65%)
c [simplification-1] maximum reduction of 40% = max (40%, 35%)
c [simplification-1] large reduction 40% >= 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.1  121050   895640        27      24      2 12549    0     2   58  10%      0    2    3    0 24188%
c i    5.2  120988   895640        31      26      2 12550    0     2   58  10%      0    2    3    0 23848%
c i    5.2  119800   895640        37      29      3 12551    0     2   58  11%      0    2    3    0 23364%
c i    5.2  119627   895640        54      40      5 12554    0     2   58  10%      0    2    3    0 22048%
c i    5.2  119418   895640        59      40      7 12556    0     2   58  10%      0    2    3    0 21646%
c i    5.2  119257   895640        61      40      7 12557    0     2   58  10%      0    2    3    0 21482%
c i    5.2  119256   895640        63      40      7 12558    0     2   58  10%      0    2    3    0 21319%
c i    5.2  119176   895640        64      40      7 12558    0     2   58  10%      0    2    3    0 21236%
c i    5.2  118940   895640        73      47      7 12559    0     2   58  10%      0    2    3    0 20638%
c i    5.2  118697   895640        81      51      8 12561    0     2   58  10%      0    2    3    0 20072%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 2791 variables
c [simpleprobe-2] 14511 schedulable variables 12%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 14936 variables remain 13% (103324 retained 87%)
c [simpleprobe-2] removed 0 variables, found 1654 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 33136 literals 14%
c [treelook-1] scheduling used 352226 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 313495 steps
c [treelook-1] 33086 literals remain 14%
c [treelook-1] 33021 variables remain to probed next time 28%
c [decomp-5] removed 1 variables
c [treelook-1] removed 47 variables, found 1842 hbrs
c [basicprobe-1] limit 6992432 based on 874054 irredundant clauses
c [basicprobe-1-0] 43397 probes remain 38% after last round
c [basicprobe-1-0] 27 units = 27 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 3592 variables, found 26304 hbrs
c [unhide-2] limit 54628 based on 874054 irredundant clauses
c [unhide-2-2] 2 units, 1723 failed, 6232 tauts, 0 hbrs, 1316 literals
c [elim-2] 59860 variables 53% will be scheduled this time
c [elim-2] scheduled 59860 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 25017 not tried 22% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 50 = 0% variables out of 59860 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 816125 negative 99.2% of 822745 except 6620 0.8%
c [phase-count-2] 662673 positive 80.5% of 822745 except 160072 19.5%
c [phase-count-2] less non-negative clauses 6620 than limit 82200 (10.0%)
c [phase-count-2] non-pos/non-neg = 160072/6620 = 24.18 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 18959 negative 100%
c [score-distribution-2] 4466 pos 3.95%, 0 min 0.00%, 108697 zero 96.05%
c [score-distribution-2] 223 different 0.20% out of total 113163 variables
c [simplification-2] removed 5215 variables 4.4% (113163 remain 46%)
c [simplification-2] removed 72895 irredundant clauses 8.1% (822745 remain 60%)
c [simplification-2] maximum reduction of 8% = max (4%, 8%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1027 (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    8.5  113162   822745       117      73     12 31433    0     3   54   9%      0    3    3    0 18444%
c i    8.6  113147   822745       135      82     15 31438    0     3   54   9%      0    3    3    0 17631%
c i    8.6  112691   822745       139      84     15 31439    0     3   54   9%      0    3    3    0 17441%
c i    8.7  112671   822745       231     142     26 31456    0     6   54   7%      0    6    4    0 14727%
c i    8.8  112607   822745       325     202     33 31480    0     7   54   7%      0    7    4    0 12404%
c i    8.9  112596   822745       391     243     41 31493    1     8   54   7%      0    8    5    0 12371%
c i    8.9  112587   822745       398     246     42 31495    1     8   54   8%      0    8    5    0 12755%
c i    8.9  112449   822745       400     246     42 31496    1     8   54   8%      0    8    5    0 12660%
c i    8.9  112380   822745       413     254     42 31500    1     9   54   8%      0    9    5    0 12229%
c i    8.9  112217   822745       463     290     47 31506    1    10   54   7%      0   10    5    0 11175%
c i    9.1  112159   822745       610     388     71 31528    1    13   54   6%      0   13    5    0 8688%
c 
c [simplification-3] limit of 112 binary hit after 112 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3757 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] 3757 out of 3757 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 1657 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 45082 literals 20%
c [treelook-2] scheduling used 347075 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 436716 steps
c [treelook-2] 45080 literals remain 20%
c [treelook-2] 25615 variables remain to probed next time 23%
c [treelook-2] removed 1 variables, found 2150 hbrs
c [unhide-3] limit 50933 based on 814935 irredundant clauses
c [unhide-3-3] 6 units, 753 failed, 15268 tauts, 0 hbrs, 375 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 110760 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 33468 not tried 30% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2765 = 2% variables out of 110760 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 785276 negative 99.2% of 791627 except 6351 0.8%
c [phase-count-3] 638642 positive 80.7% of 791627 except 152985 19.3%
c [phase-count-3] less non-negative clauses 6351 than limit 79100 (10.0%)
c [phase-count-3] non-pos/non-neg = 152985/6351 = 24.09 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 11386 negative 100%
c [score-distribution-3] 12496 pos 11.57%, 0 min 0.00%, 95499 zero 88.43%
c [score-distribution-3] 1419 different 1.31% out of total 107995 variables
c [simplification-3] removed 4130 variables 3.7% (107995 remain 44%)
c [simplification-3] removed 31118 irredundant clauses 3.8% (791627 remain 58%)
c [simplification-3] maximum reduction of 4% = max (4%, 4%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 1035 (hard 11000)
c [simplification-3] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   12.0  107994   791627       674     360     81 27215    1    14   53   6%      0   14    5    0 7823%
c i   12.0  107921   791627       694     376     83 27216    1    15   53   6%      0   15    5    0 7606%
c i   12.1  107887   791627       848     462    102 27261    1    16   53   6%      0   16    4    0 5910%
c i   12.2  107874   791627       864     472    102 27265    1    16   53   6%      0   16    4    0 5801%
c 
c [simplification-4] limit 1035 conflicts (hard 11000) hit after 1037 conflicts
c [decomp-8] removed 136 variables
c [basicprobe-2] limit 6325712 based on 790714 irredundant clauses
c [basicprobe-2-0] 38085 probes remain 37% after last round
c [basicprobe-2-0] 33 units = 33 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 4163 variables, found 22592 hbrs
c [unhide-4] limit 50000 with penalty 1 = 0 + 1
c [unhide-4-4] 6 units, 928 failed, 8606 tauts, 0 hbrs, 713 literals
c [elim-4] 24194 variables 24% will be scheduled this time
c [elim-4] scheduled 24194 variables 24%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 48960666 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 24194 scheduled
c [phase-count-4] 744321 negative 99.2% of 750673 except 6352 0.8%
c [phase-count-4] 605629 positive 80.7% of 750673 except 145044 19.3%
c [phase-count-4] less non-negative clauses 6352 than limit 75000 (10.0%)
c [phase-count-4] non-pos/non-neg = 145044/6352 = 22.83 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 10465 negative 100%
c [score-distribution-4] 16152 pos 15.74%, 0 min 0.00%, 86494 zero 84.26%
c [score-distribution-4] 1873 different 1.82% out of total 102646 variables
c [simplification-4] removed 5219 variables 4.8% (102646 remain 42%)
c [simplification-4] removed 40954 irredundant clauses 5.2% (750673 remain 55%)
c [simplification-4] maximum reduction of 5% = max (5%, 5%)
c [simplification-4] large reduction 5% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 13037 (soft 3037 + delta 10000)
c [simplification-4] new conflict limit 3037 (hard 13037)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   14.7  102645   750673      1048     596    115 37912    1    21   50   6%      1   20    5    0 6041%
c i   14.7  102640   750673      1093     628    118 37921    1    21   50   6%      1   21    6    0 6248%
c i   14.9  102635   750673      1213     703    130 37951    1    25   50   6%      1   24    6    0 5484%
c i   15.1  102623   750673      1351     810    147 37960    2    28   50   6%      1   28    7    0 5477%
c i   15.2  101986   750673      1540     954    157 37984    2    32   50   7%      1   31   11    0 6719%
c i   15.3  101984   750673      1610    1005    166 37992    2    32   51   7%      1   32    9    0 5700%
c i   15.3  101949   750673      1613    1006    167 37992    2    32   51   7%      1   32    9    0 5642%
c i   15.3  101927   750673      1615    1007    167 37992    2    32   51   7%      1   32    9    0 5606%
c i   15.3  101921   750673      1658    1031    173 38000    2    33   51   7%      1   33    9    0 5364%
c i   15.4  101907   750673      1691    1059    176 38000    2    34   51   7%      1   33    9    0 5097%
c i   15.6  101897   750673      1827    1162    192 38014    2    36   51   7%      1   36    8    0 4207%
c i   15.6  101889   750673      1828    1162    192 38014    2    36   51   7%      1   35    8    0 4191%
c i   15.6  101884   750673      1857    1179    196 38019    3    37   51   7%      1   36    8    0 4071%
c i   15.7  101197   750673      1935    1245    200 38025    3    40   51   7%      1   40   10    0 4688%
c i   15.8  101191   750673      1983    1282    204 38031    3    42   51   7%      1   41   10    0 4525%
c i   15.8  100650   750673      2012    1304    205 38033    3    43   51   7%      1   42   13    0 5665%
c i   15.9  100254   750673      2052    1326    213 38042    3    44   51   7%      1   43   12    0 5135%
c i   15.9   99823   750673      2068    1337    215 38042    3    44   51   7%      1   43   12    0 5100%
c i   15.9   99815   750673      2105    1367    217 38044    3    44   51   7%      1   44   11    0 4634%
c i   16.0   99808   750673      2130    1389    218 38045    3    45   51   7%      1   44   11    0 4393%
c i   16.4   99801   750673      2439    1634    249 38073    4    54   51   7%      1   53   13    0 4228%
c i   16.4   99790   750673      2467    1655    252 38075    4    56   51   7%      1   55   12    0 3945%
c i   16.4   99680   750673      2479    1661    254 38078    4    55   51   7%      1   54   11    0 3785%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   16.4   99667   750673      2499    1677    256 38078    4    56   51   7%      1   55   12    0 3834%
c i   16.5   99656   750673      2522    1687    261 38083    4    56   51   7%      1   55   11    0 3723%
c i   16.5   99408   750673      2527    1690    261 38084    4    56   51   7%      1   55   11    0 3696%
c i   16.5   99403   750673      2530    1691    261 38085    4    56   51   7%      1   55   11    0 3657%
c i   16.5   99029   750673      2531    1691    261 38085    4    56   51   7%      1   55   11    0 3643%
c i   16.6   99016   750673      2628    1767    272 38092    4    57   51   7%      1   56    9    0 2910%
c i   16.7   98880   750673      2668    1790    278 38102    4    58   51   7%      1   57    8    0 2618%
c i   16.8   98375   750673      2750    1838    295 38118    4    61   51   7%      1   59    9    0 2638%
c i   16.8   98261   750673      2751    1838    295 38118    4    60   51   7%      1   59    9    0 2627%
c i   16.8   98215   750673      2762    1843    297 38121    4    60   51   7%      1   59    9    0 2640%
c i   16.9   98214   750673      2777    1847    303 38125    4    61   51   7%      1   60    8    0 2531%
c i   16.9   98090   750673      2827    1883    308 38133    4    62   51   7%      1   61    9    0 2586%
c i   17.1   98084   750673      2986    2007    328 38143    4    62   51   7%      1   61    9    0 2496%
c 
c [simplification-5] limit 3080 conflicts (hard 13037) hit after 3082 conflicts
c [quatres-1] found 35645 quaternary clauses 38% in total
c [quatres-1-2] added 1 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 98077 free variables schedulable
c [ternres-1] 16 ternary resolvents (0 bin, 16 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 113 xors of average arity 2.4
c [gauss-1] connected 272 occurrences of 175 variables (average 1.6)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 190 variables
c [unhide-5] limit 224089 with penalty 0 = 0 + 0
c [unhide-5-5] 7 units, 521 failed, 18948 tauts, 0 hbrs, 1997 literals
c [transred-1] limit 1120445 with penalty 0 = 0 + 0
c [transred-1] removed 89 transitive binary clauses
c [transred-1] found 5 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 97170 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 9978 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 10 clauses out of 334 (3%) of length 10
c [cce-1-1] eliminated 196 clauses out of 2084 (9%) of length 9
c [cce-1-1] eliminated 58 clauses out of 416 (14%) of length 8
c [cce-1-1] eliminated 22 clauses out of 640 (3%) of length 7
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 286 large clauses in 30000004 steps
c [cce-1-1] allowing another 15000002 steps for small clauses
c [cce-1-1] scheduling 338471 clauses = 320967 binary + 17504 ternary
c [cce-1-1] tried to eliminate 339 small clauses 0%
c [cce-1-1] eliminated 112 binary clauses 0%
c [cce-1-1] eliminated 11 ternary clauses 0%
c [cce-1-1] eliminated 123 small clauses 0%
c [cce-1-1] eliminated 123 small clauses in 30000006 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 409 covered clauses in round 1
c [cce-1] eliminated 409 covered clauses in TOTAL during 1 rounds
c [cce-1] 409 < 1/100 * 690504 = 6905 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1380690 added (scaled 2)
c [bca-1] 179451 out of 194342 literals actually usable 92%
c [bca-1] added 270 blocked clauses in 548137 steps
c [sweep-1] limit 1380190 based on 690095 irredundant clauses
c [sweep-1-1] 6375 pos 6.6% + 90795 neg 93.4% = 97170 sched 100.0% ret 0
c [sweep-1-1] 1416156 steps 31 queries 19661.84 avg class size
c [sweep-1-1] 221 decisions 25 SAT calls 88.84 avg env size
c [sweep-1-1] 97005 variables remain 100% (153 retained 0%)
c [decomp-10] removed 38 variables
c [sweep-1-1] removed 38 vars (0 failed, 7 eqs, 8 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 38 vars in TOTAL (1 rounds, 30 queries)
c [phase-count-5] 683522 negative 99.1% of 689852 except 6330 0.9%
c [phase-count-5] 567961 positive 82.3% of 689852 except 121891 17.7%
c [phase-count-5] less non-negative clauses 6330 than limit 68900 (10.0%)
c [phase-count-5] non-pos/non-neg = 121891/6330 = 19.26 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 7688 negative 100%
c [score-distribution-5] 29650 pos 30.53%, 19 min 0.02%, 67463 zero 69.45%
c [score-distribution-5] 4345 different 4.47% out of total 97132 variables
c [simplification-5] removed 945 variables 1.0% (97132 remain 39%)
c [simplification-5] removed 60821 irredundant clauses 8.1% (689852 remain 50%)
c [simplification-5] maximum reduction of 8% = max (1%, 8%)
c [simplification-5] large reduction 8% >= 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 15082 (soft 5082 + delta 10000)
c [simplification-5] new conflict limit 5082 (hard 15082)
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   21.0   97131   689852      3128    2077    356 47835    4    65   49   7%      1   63    9    0 2446%
c i   21.1   96734   689852      3184    2115    366 47841    5    66   49   7%      1   64    8    0 2194%
c i   21.1   96728   689852      3235    2156    368 47848    5    67   49   7%      1   66    9    0 2292%
c i   21.2   96722   689852      3280    2189    372 47853    5    68   49   7%      1   67   11    0 2666%
c i   21.2   96716   689852      3302    2205    372 47854    5    68   49   7%      1   67   11    0 2745%
c i   21.3   96452   689852      3404    2280    382 47868    5    71   49   7%      1   69    9    0 2205%
c i   21.3   96446   689852      3405    2280    382 47868    5    71   49   7%      1   69    9    0 2196%
c i   21.3   96444   689852      3406    2280    382 47868    5    71   49   7%      1   69    9    0 2188%
c i   21.4   96439   689852      3467    2327    389 47874    5    72   49   7%      1   70    9    0 2065%
c i   21.5   96438   689852      3552    2397    394 47882    5    73   49   7%      1   71    9    0 2100%
c i   21.5   96437   689852      3562    2406    394 47882    5    73   49   7%      1   71    9    0 2107%
c i   21.7   96436   689852      3727    2529    416 47896    5    76   49   7%      1   74   10    0 2104%
c i   22.0   96378   689852      3958    2689    442 47938    6    80   49   7%      1   78   10    0 2085%
c i   22.0   96251   689852      3986    2710    445 47941    6    81   49   7%      1   79   10    1 2012%
c i   22.0   96243   689852      4010    2725    450 47943    6    81   49   7%      1   79   10    1 1895%
c i   22.1   96234   689852      4080    2773    458 47955    6    82   49   7%      1   80    9    1 1805%
c i   22.1   96233   689852      4087    2779    458 47955    6    83   49   7%      1   80   10    1 1984%
c i   22.5   96230   689852      4520    3145    489 47979    7    90   49   8%      2   87   14    1 2307%
c i   22.7   96229   689852      4589    3200    494 47984    7    92   49   7%      2   88   13    1 1986%
c i   22.7   96093   689852      4640    3236    503 47989    7    92   50   7%      2   89   12    1 1911%
c i   23.2   96086   689852      5028    3536    539 48033    7    98   50   7%      2   95   11    1 1536%
c 
c [simplification-6] limit 5104 conflicts (hard 15082) hit after 5104 conflicts
c [quatres-2] found 38409 quaternary clauses 40% in total
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 96083 free variables schedulable
c [ternres-2] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-2] 71826 variables remain 75% (24257 retained 25%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 1820 at-most-one constraints of average size 4.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 1820 out of 1820 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 1105 variables
c [simpleprobe-3] 13104 schedulable variables 14%
c [simpleprobe-3] limit 3567785 penalty 1 = 1 + 0
c [decomp-12] removed 27 variables
c [simpleprobe-3] 14200 variables remain 15% (81800 retained 85%)
c [simpleprobe-3] removed 27 variables, found 4646 hbrs, 8 units
c [unhide-6] limit 356778 with penalty 0 = 0 + 0
c [unhide-6-6] 9 units, 563 failed, 5927 tauts, 0 hbrs, 3917 literals
c [transred-2] limit 1783892 with penalty 0 = 0 + 0
c [transred-2] removed 167 transitive binary clauses
c [transred-2] found 4 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 95203 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 1729 blocked clauses
c [block-2] 1729 < 1/100 * 681691 = 6816 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 95203 variables 100%
c [elim-5] limit of 17838927 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 26899 not tried 28% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 3319 = 3% variables out of 95203 scheduled
c [bca-2] limit of 10000000 steps and 1330271 added (scaled 2)
c [bca-2] 168314 out of 183770 literals actually usable 92%
c [bca-2] added 170 blocked clauses in 511104 steps
c [sweep-2] limit 1329636 based on 664818 irredundant clauses
c [sweep-2-1] 6180 pos 6.7% + 85576 neg 93.3% = 91756 sched 99.9% ret 128
c [sweep-2-1] 1356587 steps 19 queries 28694.58 avg class size
c [sweep-2-1] 127 decisions 16 SAT calls 58.75 avg env size
c [sweep-2-1] 91700 variables remain 100% (176 retained 0%)
c [decomp-13] removed 20 variables
c [sweep-2-1] removed 20 vars (0 failed, 2 eqs, 6 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 20 vars in TOTAL (1 rounds, 18 queries)
c [phase-count-6] 658639 negative 99.1% of 664683 except 6044 0.9%
c [phase-count-6] 545880 positive 82.1% of 664683 except 118803 17.9%
c [phase-count-6] less non-negative clauses 6044 than limit 66400 (10.0%)
c [phase-count-6] non-pos/non-neg = 118803/6044 = 19.66 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 7275 negative 100%
c [score-distribution-6] 25056 pos 27.28%, 3883 min 4.23%, 62925 zero 68.50%
c [score-distribution-6] 4231 different 4.61% out of total 91864 variables
c [simplification-6] removed 4219 variables 4.4% (91864 remain 37%)
c [simplification-6] removed 25169 irredundant clauses 3.6% (664683 remain 48%)
c [simplification-6] maximum reduction of 4% = max (4%, 4%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 4000
c [simplification-6] penalized conflict interval 4000 = 1 * 4000
c [simplification-6] hard conflict limit 19104 (soft 9104 + delta 10000)
c [simplification-6] new conflict limit 9104 (hard 19104)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   27.1   91863   664683      5138    2950    491 48605    7    99   48   7%      2   95   11    1 1607%
c i   27.1   91862   664683      5157    2966    492 48605    7    98   48   7%      2   94   12    1 1608%
c i   27.5   91861   664683      5551    3270    529 48646    8   102   48   7%      2   97   11    1 1389%
c i   27.5   91860   664683      5555    3271    529 48648    8   102   48   7%      2   97   11    1 1373%
c i   27.6   91854   664683      5609    3313    534 48653    8   102   48   7%      2   98   11    1 1402%
c i   27.8   91846   664683      5801    3457    552 48675    8   105   49   7%      2  100   12    1 1454%
c i   28.0   91845   664683      5939    3559    563 48697    8   112   49   7%      2  107   15    1 1695%
c i   28.0   91833   664683      5962    3573    565 48703    8   112   49   7%      2  107   14    1 1578%
c i   28.0   91831   664683      5963    3573    565 48703    8   112   49   7%      2  107   13    1 1572%
c i   28.1   91802   664683      6104    3673    575 48727    8   111   49   7%      2  105   11    1 1229%
c i   28.3   91798   664683      6201    3742    585 48740    8   110   49   7%      2  105   11    1 1236%
c i   28.4   91788   664683      6254    3788    589 48742    8   111   49   7%      2  105   10    1 1175%
c i   28.6   91784   664683      6393    3894    604 48758    8   111   49   7%      2  105   10    1 1109%
c i   28.7   91618   664683      6547    4020    614 48769    9   115   49   8%      1  109   15    1 1573%
c i   28.8   91613   664683      6604    4060    625 48774    9   115   49   8%      1  108   13    1 1377%
c i   29.0   91610   664683      6778    4191    644 48795    9   118   49   7%      1  111   13    1 1305%
c i   29.1   91607   664683      6846    4250    646 48800    9   120   49   7%      1  113   13    1 1304%
c i   29.1   91511   664683      6847    4250    646 48800    9   120   49   7%      1  113   13    1 1299%
c i   29.6   91476   664683      7285    4597    680 48849    9   124   49   7%      2  117   12    1 1155%
c i   29.7   91472   664683      7337    4640    685 48851    9   126   49   7%      2  118   13    1 1206%
c i   29.7   91469   664683      7440    4721    686 48862    9   125   49   8%      2  118   14    1 1226%
c i   29.7   91464   664683      7441    4721    686 48862    9   125   49   8%      2  118   14    1 1222%
c i   29.7   91456   664683      7443    4722    686 48862    9   125   49   8%      2  118   13    1 1213%
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   29.8   91453   664683      7494    4765    689 48866   10   126   49   8%      2  118   15    1 1296%
c i   29.8   91447   664683      7503    4771    689 48868   10   126   49   8%      2  118   14    1 1262%
c i   30.4   91446   664683      8213    5385    714 48918   11   129   50   9%      4  119   18    1 1386%
c i   30.4   91445   664683      8220    5391    714 48918   11   129   50   9%      4  120   20    1 1539%
c i   30.5   91439   664683      8261    5421    717 48922   11   129   50   9%      4  119   23    1 1688%
c i   30.5   91432   664683      8303    5450    723 48927   11   130   50   9%      4  121   20    1 1510%
c i   30.6   91426   664683      8322    5455    723 48940   11   130   50   9%      3  121   20    1 1461%
c i   30.9   91300   664683      8582    5674    742 48958   11   132   50   9%      3  122   14    1 1016%
c i   30.9   91295   664683      8614    5692    750 48962   12   132   50   9%      3  122   16    1 1151%
c i   30.9   91292   664683      8647    5717    753 48964   11   132   50   9%      3  122   15    1 1066%
c i   31.1   91287   664683      8792    5848    761 48968   12   133   50   9%      3  122   15    1 1043%
c i   31.1   91286   664683      8794    5848    761 48969   12   133   50   9%      3  122   15    1 1035%
c i   31.3   91284   664683      9028    6039    781 48991   12   132   50   9%      2  121   14    1  918%
c 
c [simplification-7] limit 9148 conflicts (hard 19104) hit after 9149 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 68234 schedulable variables 74%
c [ternres-3] 103 ternary resolvents (1 bin, 102 trn)
c [ternres-3] 44710 variables remain 49% (46572 retained 51%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 36 xors of average arity 2.7
c [gauss-2] connected 96 occurrences of 89 variables (average 1.1)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [decomp-14] removed 53 variables
c [gauss-2] exported 1 unary, 0 binary and 0 ternary equations
c [treelook-3] limit 304490 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 40273 literals 22%
c [treelook-3] scheduling used 305576 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 304490 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 446269 steps
c [treelook-3] 40269 literals remain 22%
c [treelook-3] 18998 variables remain to probed next time 21%
c [treelook-3] removed 0 variables, found 1778 hbrs
c [unhide-7] limit 608980 with penalty 0 = 0 + 0
c [unhide-7-7] 7 units, 308 failed, 8315 tauts, 0 hbrs, 10489 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 195 transitive binary clauses
c [transred-3] found 6 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 286 (1%) of length 10
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 2 large clauses in 15000009 steps
c [cce-2-1] allowing another 7500004 steps for small clauses
c [cce-2-1] scheduling 532818 clauses = 298031 binary + 234787 ternary
c [cce-2-1] tried to eliminate 125 small clauses 0%
c [cce-2-1] eliminated 25 binary clauses 0%
c [cce-2-1] eliminated 13 ternary clauses 0%
c [cce-2-1] eliminated 38 small clauses 0%
c [cce-2-1] eliminated 5145 small clauses in 15000000 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 5147 covered clauses in round 1
c [cce-2] eliminated 5147 covered clauses in TOTAL during 1 rounds
c [cce-2] 5147 < 1/100 * 652144 = 6521 considered unsuccessful
c [elim-6] 26724 variables 30% will be scheduled this time
c [elim-6] scheduled 26724 variables 30%
c [elim-6] limit of 60898084 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 11 variables 0% in round 1 in 46719721 steps
c [elim-6-1] backward subsumption/strengthening limit 14178363
c [elim-6-1-1] backward checking 238 touched variables 0%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 6 and strengthened 8 clauses in 190501 steps
c [elim-6-1] rescheduled 52 variables 0% by backward subsumption
c [elim-6-2] eliminated 11 variables 0% in round 2 in 70640 steps
c [elim-6-2] backward subsumption/strengthening limit 70600
c [elim-6-2-1] backward checking 77 touched variables 0%
c [elim-6-2-1] incomplete backward checking 0 remain 0%
c [elim-6-2] subsumed 3 and strengthened 1 clauses in 70601 steps
c [elim-6-2] rescheduled 8 variables 0% by backward subsumption
c [elim-6-3] no variable eliminated in round 3 in 16953 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 42 = 0% variables out of 26724 scheduled
c [elim-6] 42 < 1/100 * 26724 = 267 considered unsuccessful
c [bca-3] limit of 10000000 steps and 1290496 added (scaled 2)
c [bca-3] 161586 out of 181026 literals actually usable 89%
c [bca-3] added 83 blocked clauses in 492922 steps
c [sweep-3] limit 1289776 based on 644888 irredundant clauses
c [sweep-3-1] 6218 pos 6.9% + 84123 neg 93.1% = 90341 sched 99.8% ret 171
c [sweep-3-1] 1306987 steps 11 queries 22310.27 avg class size
c [sweep-3-1] 76 decisions 9 SAT calls 88.89 avg env size
c [sweep-3-1] 90309 variables remain 100% (196 retained 0%)
c [decomp-17] removed 304 variables
c [sweep-3-1] removed 304 vars (0 failed, 1 eqs, 3 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 304 vars in TOTAL (1 rounds, 10 queries)
c [phase-count-7] 638149 negative 99.1% of 644183 except 6034 0.9%
c [phase-count-7] 529788 positive 82.2% of 644183 except 114395 17.8%
c [phase-count-7] less non-negative clauses 6034 than limit 64400 (10.0%)
c [phase-count-7] non-pos/non-neg = 114395/6034 = 18.96 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 6377 negative 100%
c [score-distribution-7] 23610 pos 26.17%, 5122 min 5.68%, 61476 zero 68.15%
c [score-distribution-7] 3837 different 4.25% out of total 90208 variables
c [simplification-7] removed 1074 variables 1.2% (90208 remain 37%)
c [simplification-7] removed 20500 irredundant clauses 3.1% (644183 remain 47%)
c [simplification-7] maximum reduction of 3% = max (1%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 9000
c [simplification-7] penalized conflict interval 9000 = 1 * 9000
c [simplification-7] hard conflict limit 28149 (soft 18149 + delta 10000)
c [simplification-7] new conflict limit 18149 (hard 28149)
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   35.9   90207   644183      9223    6155    810 51334   12   138   49   9%      2  127   18    2 1165%
c i   36.1   90202   644183      9432    6329    821 51351   12   139   49   9%      2  127   15    2  930%
c i   36.2   90196   644183      9439    6332    822 51353   12   138   49   9%      2  127   14    2  908%
c i   36.3   90146   644183      9587    6457    831 51362   13   139   50  10%      2  127   32    2 1891%
c i   36.4   90145   644183      9692    6549    836 51369   13   139   50  10%      2  127   25    2 1501%
c i   36.4   90142   644183      9693    6549    836 51369   13   139   50  10%      2  127   25    2 1495%
c i   36.5   90141   644183      9766    6612    840 51372   13   141   50  10%      2  129   22    2 1307%
c i   36.6   90135   644183      9906    6720    857 51385   14   143   50  10%      2  131   22    2 1251%
c i   36.8   90134   644182     10012    6801    862 51403   14   144   50  10%      2  131   23    2 1282%
c i   36.9   90131   644182     10171    6924    878 51415   14   146   50  10%      1  133   23    2 1252%
c i   36.9   90129   644182     10172    6924    878 51415   14   146   50  10%      1  133   23    2 1247%
c i   37.1   90128   644182     10353    7076    885 51431   15   150   50  10%      1  137   29    2 1488%
c i   37.3   90060   644182     10553    7245    890 51454   15   151   50  10%      1  137   23    2 1165%
c i   37.3   90053   644182     10554    7245    890 51454   15   151   50  10%      1  137   23    2 1160%
c i   37.4   90052   644182     10608    7281    896 51464   15   150   50  10%      1  136   20    2  993%
c i   37.5   90051   644182     10727    7384    905 51468   15   149   50  10%      1  135   19    2  966%
c i   37.5   90044   644182     10770    7419    907 51473   15   149   50  10%      1  135   20    2  985%
c i   37.6   90037   644182     10870    7502    911 51481   16   149   50  11%      1  135   23    2 1094%
c i   37.6   90032   644182     10871    7502    911 51481   16   149   50  11%      1  135   23    2 1090%
c i   38.0   90026   644182     11197    7783    927 51503   16   151   50  11%      1  136   19    2  865%
c i   38.0   90018   644182     11215    7797    928 51504   16   151   50  11%      1  136   18    2  837%
c i   38.2   90016   644182     11327    7884    932 51520   16   153   50  11%      1  138   22    2 1021%
c i   38.3   90009   644182     11430    7965    945 51526   16   153   50  10%      1  138   17    2  778%
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   38.5   89990   644182     11663    8138    957 51533   18   154   50  11%      1  138   34    2 1446%
c i   38.7   89983   644182     11776    8227    971 51540   18   158   50  11%      1  142   29    2 1218%
c i   38.8   89846   644182     11854    8292    977 51546   18   159   50  11%      1  142   28    2 1151%
c i   38.8   89845   644182     11889    8317    981 51547   18   158   50  11%      1  142   30    2 1235%
c i   38.9   89844   644182     11987    8398    991 51552   18   160   50  11%      1  143   25    2 1034%
c i   38.9   89843   644182     11988    8398    991 51552   18   160   50  11%      1  143   25    2 1030%
c i   38.9   89839   644182     11991    8400    991 51552   18   160   50  11%      1  143   25    2 1020%
c i   39.1   89832   644182     12116    8505    998 51561   18   160   50  11%      1  143   20    2  796%
c i   39.1   89820   644182     12188    8566   1005 51563   18   159   50  11%      1  142   20    2  794%
c i   39.3   89805   644182     12269    8623   1014 51577   18   160   50  11%      1  142   17    3  687%
c i   39.4   89802   644182     12422    8765   1017 51581   18   160   50  11%      1  143   18    3  690%
c i   39.4   89790   644182     12426    8767   1017 51582   18   160   50  11%      1  143   17    3  687%
c i   39.5   89747   644182     12580    8901   1019 51592   18   160   50  11%      1  142   21    3  799%
c i   39.7   89746   644182     12698    9001   1026 51599   18   163   50  11%      1  145   23    3  877%
c i   39.8   89745   644182     12740    9030   1037 51600   18   165   50  11%      1  146   22    3  827%
c i   39.8   89741   644182     12742    9031   1037 51600   18   165   50  11%      1  146   22    3  824%
c i   39.9   89733   644182     12793    9077   1040 51600   19   166   50  11%      1  148   27    3 1002%
c i   39.9   89729   644182     12825    9104   1041 51601   19   167   50  11%      1  149   29    3 1080%
c i   40.0   89728   644182     12867    9138   1042 51606   19   168   50  11%      1  150   27    3  991%
c i   40.1   89726   644182     12970    9225   1047 51610   19   169   50  11%      1  151   30    3 1076%
c i   40.2   89725   644182     13020    9265   1049 51616   19   172   50  11%      1  153   29    3 1035%
c i   40.3   89723   644182     13139    9364   1056 51625   19   172   50  11%      1  153   23    3  810%
c i   40.4   89720   644182     13201    9413   1056 51632   19   171   50  11%      1  152   23    3  811%
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.5   89719   644182     13290    9488   1061 51637   19   168   50  11%      1  149   18    3  640%
c i   40.6   89711   644182     13369    9554   1066 51641   19   169   50  11%      1  149   19    3  673%
c i   40.7   89708   644182     13508    9672   1073 51652   19   169   50  11%      1  149   21    3  718%
c i   41.0   89705   644182     13706    9819   1088 51679   19   168   50  11%      1  148   18    3  607%
c i   41.2   89696   644182     13858    9941   1099 51693   18   167   50  11%      1  146   14    3  487%
c i   41.2   89689   644182     13871    9952   1100 51693   18   167   50  11%      1  146   14    3  469%
c i   41.3   89680   644182     13938   10011   1103 51697   19   167   50  11%      1  146   18    3  597%
c i   41.4   89679   644182     14039   10101   1110 51699   18   165   50  11%      1  144   16    3  540%
c i   41.5   89675   644182     14105   10149   1120 51704   18   166   51  11%      1  145   14    3  483%
c i   41.7   89637   644182     14211   10228   1132 51715   18   165   51  11%      1  144   12    3  399%
c i   41.7   89634   644182     14267   10274   1133 51723   18   164   51  11%      1  142   11    3  383%
c i   42.5   89540   644182     14982   10891   1164 51774   18   168   52  11%      3  145   23    3  733%
c i   42.5   89534   644182     14994   10902   1164 51774   18   168   52  11%      3  145   23    3  715%
c i   42.6   89530   644182     15037   10942   1165 51775   18   168   52  11%      3  144   21    3  658%
c i   42.6   89529   644182     15038   10942   1165 51775   18   168   52  11%      3  144   21    3  655%
c i   42.7   89528   644182     15097   10993   1167 51778   18   168   52  11%      3  145   21    3  647%
c i   42.7   89519   644182     15098   10993   1167 51778   18   168   52  11%      3  145   21    3  645%
c i   42.9   89513   644182     15322   11187   1174 51793   19   168   52  11%      3  144   22    3  665%
c i   43.2   89506   644182     15520   11344   1194 51810   19   175   52  11%      2  151   21    3  622%
c i   43.3   89474   644182     15572   11389   1196 51811   19   175   53  11%      2  151   20    3  608%
c i   43.3   89471   644182     15573   11389   1196 51811   19   175   53  11%      2  151   20    3  606%
c i   43.5   89465   644182     15729   11527   1201 51818   19   175   53  11%      2  150   28    3  814%
c i   43.5   89464   644182     15766   11559   1203 51820   19   175   53  11%      2  150   27    3  777%
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.8   89460   644182     15977   11725   1217 51835   20   175   53  11%      2  149   27    4  780%
c i   44.0   89450   644182     16143   11863   1230 51846   20   175   53  11%      2  149   23    4  644%
c i   44.3   89447   644182     16372   12059   1242 51857   20   177   53  11%      2  150   22    4  619%
c i   44.4   89439   644182     16463   12138   1248 51860   20   177   53  11%      2  151   23    4  632%
c i   44.6   89437   644182     16611   12260   1257 51871   21   182   53  11%      1  155   32    4  869%
c i   44.9   89436   644182     16748   12378   1265 51876   21   186   53  12%      1  159   34    4  891%
c i   44.9   89435   644182     16825   12442   1265 51885   22   185   53  12%      1  158   38    4  978%
c i   44.9   89432   644182     16853   12466   1266 51886   22   185   53  12%      1  158   36    4  935%
c i   45.0   89430   644182     16872   12482   1266 51887   22   186   53  12%      1  158   35    4  896%
c i   45.0   89427   644182     16907   12513   1265 51889   22   185   53  12%      1  158   38    4  969%
c i   45.0   89426   644182     16921   12521   1269 51890   22   186   53  12%      1  158   36    4  926%
c i   45.4   89425   644182     17281   12838   1288 51905   22   185   53  12%      2  156   28    4  692%
c i   45.4   89424   644182     17301   12857   1288 51905   22   185   53  12%      2  156   29    4  716%
c i   45.6   89423   644182     17441   12976   1294 51916   23   187   54  12%      1  158   31    4  754%
c i   45.6   89419   644182     17461   12995   1294 51916   23   187   54  12%      1  158   30    4  730%
c i   45.6   89418   644182     17462   12995   1294 51916   23   187   54  12%      1  158   30    4  727%
c i   45.7   89412   644182     17485   13014   1296 51917   23   189   54  12%      1  160   29    4  711%
c i   45.8   89409   644182     17594   13101   1301 51925   23   189   54  12%      1  160   25    4  599%
c i   45.9   89408   644182     17667   13161   1304 51931   22   188   54  12%      1  159   22    4  529%
c i   46.0   89404   644182     17785   13259   1312 51936   23   188   54  12%      1  158   24    4  571%
c i   46.4   89398   644182     18026   13453   1333 51958   22   189   54  12%      1  159   21    4  508%
c i   46.5   89346   644182     18083   13501   1335 51959   23   190   54  12%      1  159   24    4  563%
c i   46.6   89345   644182     18184   13593   1336 51965   22   189   54  12%      1  158   22    4  517%
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   46.7   89337   644182     18239   13626   1344 51977   23   191   54  12%      1  160   23    4  541%
c 
c [simplification-8] limit 18250 conflicts (hard 28149) hit after 18250 conflicts
c [quatres-3] found 35452 quaternary clauses 38% in total
c [quatres-3-2] added 4 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1 quaternary resolvents
c [ternres-4] limit 6015059 with penalty 0 = 0 + 0
c [ternres-4] 43733 schedulable variables 48%
c [ternres-4] 35 ternary resolvents (0 bin, 35 trn)
c [ternres-4] 8103 variables remain 9% (81227 retained 91%)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 137 xors of average arity 2.5
c [gauss-3] connected 349 occurrences of 161 variables (average 2.2)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-18] removed 137 variables
c [basicprobe-3] limit 30075297 penalty 0 = 0 + 0
c [basicprobe-3-0] 29059 probes remain 33% after last round
c [basicprobe-3-0] 144 units = 137 failed (95%) + 7 lifted (5%)
c [basicprobe-3-0] removed 2184 variables, found 79892 hbrs
c [bate-1] eliminated 96 asymmetric tautologies during probing
c [unhide-8] limit 601505 with penalty 1 = 0 + 1
c [unhide-8-8] 54 units, 835 failed, 16927 tauts, 0 hbrs, 44469 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 182 transitive binary clauses
c [transred-4] found 4 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 85949 variables 100%
c [block-3] limit of 30075297 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 60 blocked clauses
c [block-3] 60 < 1/100 * 622061 = 6220 considered unsuccessful
c [bca-4] limit of 10000000 steps and 1225121 added (scaled 2)
c [bca-4] 145377 out of 171898 literals actually usable 85%
c [bca-4] added 114 blocked clauses in 429805 steps
c [sweep-4] limit 1804517 penalty 0 = 0 + 0
c [sweep-4-1] 5367 pos 6.3% + 80400 neg 93.7% = 85767 sched 99.8% ret 181
c [sweep-4-1] 1829040 steps 25 queries 15642.68 avg class size
c [sweep-4-1] 236 decisions 23 SAT calls 56.96 avg env size
c [sweep-4-1] 85619 variables remain 100% (327 retained 0%)
c [decomp-19] removed 194 variables
c [sweep-4-1] removed 194 vars (0 failed, 2 eqs, 5 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 194 vars in TOTAL (1 rounds, 24 queries)
c [phase-count-8] 605561 negative 99.0% of 611549 except 5988 1.0%
c [phase-count-8] 503068 positive 82.3% of 611549 except 108481 17.7%
c [phase-count-8] less non-negative clauses 5988 than limit 61100 (10.0%)
c [phase-count-8] non-pos/non-neg = 108481/5988 = 18.12 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 1683 negative 100%
c [score-distribution-8] 29835 pos 34.79%, 6753 min 7.87%, 49166 zero 57.33%
c [score-distribution-8] 4291 different 5.00% out of total 85754 variables
c [simplification-8] removed 3576 variables 4.0% (85754 remain 35%)
c [simplification-8] removed 32633 irredundant clauses 5.1% (611549 remain 45%)
c [simplification-8] maximum reduction of 5% = max (4%, 5%)
c [simplification-8] large reduction 5% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 30250 (soft 20250 + delta 10000)
c [simplification-8] new conflict limit 20250 (hard 30250)
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   51.1   85753   611549     18383   13577   1320 110336   22   193   55  12%      1  161   22    4  512%
c i   51.2   85748   611549     18455   13636   1323 110341   23   193   55  12%      1  161   27    4  627%
c i   51.4   85747   611549     18564   13728   1329 110348   24   195   55  12%      1  164   35    4  787%
c i   51.6   85738   611549     18675   13825   1330 110356   23   197   55  12%      1  166   29    4  658%
c i   51.6   85730   611549     18708   13853   1332 110357   23   199   55  12%      1  167   28    4  621%
c i   51.7   85717   611549     18749   13890   1332 110360   23   198   55  12%      1  166   27    4  605%
c i   51.8   85712   611549     18943   14058   1336 110365   23   191   55  12%      1  159   25    5  554%
c i   52.0   85703   611549     19102   14197   1342 110376   23   190   56  12%      1  157   23    5  510%
c i   52.0   85675   611549     19111   14205   1342 110376   23   190   56  12%      1  157   23    5  500%
c i   52.2   85600   611548     19249   14325   1345 110384   24   191   56  12%      1  158   29    5  634%
c i   52.2   85597   611548     19262   14334   1345 110387   24   192   56  12%      1  158   28    5  608%
c i   52.2   85587   611548     19272   14340   1346 110389   24   192   56  12%      1  159   27    5  587%
c i   52.5   85578   611548     19442   14484   1350 110407   24   196   56  12%      1  162   25    5  534%
c i   52.5   85574   611548     19443   14484   1350 110407   24   196   56  12%      1  162   25    5  532%
c i   52.5   85527   611548     19444   14484   1350 110407   24   196   56  12%      1  162   25    5  530%
c i   52.5   85518   611548     19470   14506   1350 110410   24   196   56  12%      1  162   23    5  496%
c i   53.6   85514   611548     20208   15137   1395 110452   26   208   56  12%      3  172   40    5  785%
c i   53.6   85508   611548     20230   15157   1396 110452   26   208   56  12%      3  172   38    5  759%
c 
c [simplification-9] limit 20272 conflicts (hard 30250) hit after 20272 conflicts
c [quatres-4] found 36555 quaternary clauses 41% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-2] added 1 quaternary resolvents
c [ternres-5] limit 6796299 with penalty 0 = 0 + 0
c [ternres-5] 7737 schedulable variables 9%
c [ternres-5] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-20] removed 290 variables
c [simpleprobe-4] 13129 schedulable variables 15%
c [simpleprobe-4] limit 27185199 penalty 0 = 0 + 0
c [decomp-21] removed 339 variables
c [simpleprobe-4] 2378 variables remain 3% (82747 retained 97%)
c [simpleprobe-4] removed 339 variables, found 31611 hbrs, 108 units
c [unhide-9] limit 679629 with penalty 1 = 0 + 1
c [unhide-9-9] 9 units, 294 failed, 14864 tauts, 0 hbrs, 32577 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 239 transitive binary clauses
c [transred-5] found 9 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 84278 variables 100%
c [elim-7] limit of 67962999 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 3099 variables 4% in round 1 in 57880055 steps
c [elim-7-1] backward subsumption/strengthening limit 10082944
c [elim-7-1-1] backward checking 10520 touched variables 12%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 10 and strengthened 223 clauses in 3715928 steps
c [elim-7-1] rescheduled 622 variables 1% by backward subsumption
c [elim-7-2] eliminated 67 variables 0% in round 2 in 816135 steps
c [elim-7-2] backward subsumption/strengthening limit 816100
c [elim-7-2-1] backward checking 459 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 16 and strengthened 3 clauses in 315150 steps
c [elim-7-2] rescheduled 66 variables 0% by backward subsumption
c [elim-7-3] eliminated 4 variables 0% in round 3 in 72321 steps
c [elim-7-3] backward subsumption/strengthening limit 72300
c [elim-7-3-1] backward checking 35 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 3 and strengthened 2 clauses in 72301 steps
c [elim-7] incomplete 18 not tried 0% in round 3
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 3238 = 4% variables out of 84278 scheduled
c [bca-5] limit of 10000000 steps and 1167250 added (scaled 2)
c [bca-5] 138295 out of 162082 literals actually usable 85%
c [bca-5] added 81 blocked clauses in 403151 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 20388890 penalty 0 = 0 + 0
c [sweep-5-1] 5562 pos 6.9% + 75188 neg 93.1% = 80750 sched 99.6% ret 290
c [sweep-5-1] 20476082 steps 170 queries 3090.95 avg class size
c [sweep-5-1] 1331 decisions 147 SAT calls 87.76 avg env size
c [sweep-5-1] 73509 variables remain 91% (7320 retained 9%)
c [decomp-22] removed 253 variables
c [sweep-5-1] removed 253 vars (0 failed, 27 eqs, 53 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 253 vars in TOTAL (1 rounds, 169 queries)
c [phase-count-9] 576193 negative 99.1% of 581608 except 5415 0.9%
c [phase-count-9] 477581 positive 82.1% of 581608 except 104027 17.9%
c [phase-count-9] less non-negative clauses 5415 than limit 58100 (10.0%)
c [phase-count-9] non-pos/non-neg = 104027/5415 = 19.21 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 745 negative 100%
c [score-distribution-9] 30584 pos 37.86%, 8338 min 10.32%, 41865 zero 51.82%
c [score-distribution-9] 4570 different 5.66% out of total 80787 variables
c [simplification-9] removed 4721 variables 5.5% (80787 remain 33%)
c [simplification-9] removed 29940 irredundant clauses 4.9% (581608 remain 42%)
c [simplification-9] maximum reduction of 6% = max (6%, 5%)
c [simplification-9] large reduction 6% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 32272 (soft 22272 + delta 10000)
c [simplification-9] new conflict limit 22272 (hard 32272)
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   59.4   80786   581608     20372   10510   1269 150326   25   211   50  12%      3  175   30    5  581%
c i   59.4   80781   581608     20375   10510   1271 150326   25   211   50  12%      3  175   29    5  574%
c i   59.4   80777   581608     20399   10533   1271 150326   25   211   50  12%      3  175   29    5  572%
c i   60.1   80776   581608     20856   10930   1291 150351   26   217   50  12%      3  179   29    5  544%
c i   60.4   80773   581608     21192   11222   1305 150368   26   217   51  12%      3  178   25    5  471%
c i   60.4   80772   581608     21194   11223   1305 150368   26   217   51  12%      3  178   25    5  468%
c i   60.5   80771   581608     21288   11304   1310 150373   25   217   51  12%      3  178   23    5  422%
c i   60.5   80764   581608     21298   11309   1312 150374   25   216   51  12%      3  178   22    5  412%
c i   61.2   80753   581608     21985   11883   1352 150416   25   215   51  12%      4  174   24    6  431%
c 
c [simplification-10] limit 22281 conflicts (hard 32272) hit after 22281 conflicts
c [quatres-5] found 38203 quaternary clauses 44% in total
c [quatres-5-1] removed 3 duplicate quaternary clauses
c [quatres-5-2] added 5 quaternary resolvents
c [ternres-6] limit 7457201 with penalty 0 = 0 + 0
c [ternres-6] all 80752 free variables schedulable
c [ternres-6] 63 ternary resolvents (0 bin, 63 trn)
c [ternres-6] 41066 variables remain 51% (39686 retained 49%)
c [card-4] limit 466075 penalty 3 = 3 + 0
c [card-4] found 1413 at-most-one constraints of average size 4.2
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 466075 for elimination
c [card-4] 1413 out of 1413 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] extracted 20 xors of average arity 3.0
c [gauss-4] connected 59 occurrences of 59 variables (average 1.0)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 9 variables
c [unhide-10] limit 1491440 with penalty 0 = 0 + 0
c [unhide-10-10] 8 units, 426 failed, 17700 tauts, 0 hbrs, 19011 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 180 transitive binary clauses
c [transred-6] found 5 units
c [cce-3] limit of 9321502 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 1114 (0%) of length 9
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 1 large clauses in 9321517 steps
c [cce-3-1] allowing another 4660758 steps for small clauses
c [cce-3-1] scheduling 283852 clauses = 266077 binary + 17775 ternary
c [cce-3-1] tried to eliminate 149 small clauses 0%
c [cce-3-1] eliminated 38 binary clauses 0%
c [cce-3-1] eliminated 7 ternary clauses 0%
c [cce-3-1] eliminated 45 small clauses 0%
c [cce-3-1] eliminated 4835 small clauses in 9321512 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 4836 covered clauses in round 1
c [cce-3] eliminated 4836 covered clauses in TOTAL during 1 rounds
c [cce-3] 4836 < 1/100 * 580191 = 5801 considered unsuccessful
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 80216 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2982880700 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 997 variables 1% in round 1 in 56327943 steps
c [elim-8-1] backward subsumption/strengthening limit 56327900
c [elim-8-1-1] backward checking 3453 touched variables 4%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 11 and strengthened 146 clauses in 1604100 steps
c [elim-8-1] rescheduled 402 variables 1% by backward subsumption
c [elim-8-2] eliminated 49 variables 0% in round 2 in 448863 steps
c [elim-8-2] backward subsumption/strengthening limit 448800
c [elim-8-2-1] backward checking 346 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 24 and strengthened 1 clauses in 231971 steps
c [elim-8-2] rescheduled 40 variables 0% by backward subsumption
c [elim-8-3] eliminated 7 variables 0% in round 3 in 41149 steps
c [elim-8-3] backward subsumption/strengthening limit 41100
c [elim-8-3-1] backward checking 16 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 0 and strengthened 0 clauses in 41101 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1086 = 1% variables out of 80216 scheduled
c [bca-6] limit of 10000000 steps and 1145659 added (scaled 2)
c [bca-6] 133583 out of 158262 literals actually usable 84%
c [bca-6] added 117 blocked clauses in 388050 steps
c [sweep-6] limit 2237160 penalty 0 = 0 + 0
c [sweep-6-1] 6021 pos 8.3% + 66150 neg 91.7% = 72171 sched 91.2% ret 6959
c [sweep-6-1] 2455087 steps 20 queries 13948.70 avg class size
c [sweep-6-1] 134 decisions 16 SAT calls 122.75 avg env size
c [sweep-6-1] 72046 variables remain 91% (7041 retained 9%)
c [decomp-24] removed 66 variables
c [sweep-6-1] removed 66 vars (0 failed, 3 eqs, 7 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 66 vars in TOTAL (1 rounds, 19 queries)
c [phase-count-10] 566906 negative 99.1% of 572170 except 5264 0.9%
c [phase-count-10] 468934 positive 82.0% of 572170 except 103236 18.0%
c [phase-count-10] less non-negative clauses 5264 than limit 57200 (10.0%)
c [phase-count-10] non-pos/non-neg = 103236/5264 = 19.61 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 534 negative 100%
c [score-distribution-10] 29432 pos 37.23%, 9730 min 12.31%, 39902 zero 50.47%
c [score-distribution-10] 5016 different 6.34% out of total 79064 variables
c [simplification-10] removed 1688 variables 2.1% (79064 remain 32%)
c [simplification-10] removed 9438 irredundant clauses 1.6% (572170 remain 42%)
c [simplification-10] maximum reduction of 2% = max (2%, 2%)
c [simplification-10] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-10] new conflict interval 15666
c [simplification-10] penalized conflict interval 15666 = 1 * 15666
c [simplification-10] hard conflict limit 47947 (soft 37947 + delta 10000)
c [simplification-10] new conflict limit 37947 (hard 47947)
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.9   79063   572170     22412   11764   1395 133438   25   213   50  12%      4  171   23    6  399%
c i   66.0   79058   572170     22525   11870   1396 133439   25   210   50  12%      3  168   23    6  408%
c i   66.2   79056   572170     22693   12023   1400 133447   25   209   50  12%      3  166   28    6  482%
c i   66.2   79048   572170     22732   12058   1400 133449   25   207   50  12%      3  165   29    6  504%
c i   66.5   79047   572170     22966   12237   1424 133469   24   207   50  12%      2  164   20    6  343%
c i   66.8   78954   572170     23173   12417   1436 133477   24   207   50  12%      2  163   20    6  344%
c i   67.0   78947   572170     23332   12558   1446 133483   24   208   50  12%      2  164   20    6  345%
c i   67.2   78946   572170     23478   12686   1455 133489   24   208   50  11%      2  164   18    6  308%
c i   67.5   78720   572170     23715   12895   1470 133498   24   208   50  11%      2  164   20    6  332%
c i   67.6   78719   572170     23728   12905   1471 133498   24   209   50  12%      2  164   27    6  447%
c i   67.8   78718   572170     23942   13093   1479 133510   24   211   50  11%      2  166   24    6  394%
c i   67.9   78708   572170     23974   13112   1483 133516   24   210   50  11%      2  165   23    6  379%
c i   68.3   78707   572170     24226   13322   1493 133540   23   210   50  11%      2  164   14    6  235%
c i   68.4   78702   572170     24323   13406   1496 133546   23   211   50  11%      1  165   19    6  311%
c i   68.6   78692   572170     24574   13625   1507 133554   23   207   50  11%      1  160   21    6  347%
c i   69.1   78687   572170     24965   13958   1539 133572   22   207   50  11%      2  160   17    6  268%
c i   69.5   78679   572170     25204   14155   1562 133588   22   208   51  11%      2  160   16    6  248%
c i   69.5   78677   572170     25205   14155   1562 133588   22   208   51  11%      2  160   15    6  247%
c i   69.5   78647   572170     25215   14159   1563 133589   22   208   51  11%      2  159   15    6  247%
c i   69.5   78638   572170     25222   14164   1564 133589   22   208   51  11%      2  159   15    6  242%
c i   69.6   78634   572170     25285   14211   1568 133595   22   207   51  11%      2  158   14    6  218%
c i   69.8   78632   572170     25557   14454   1578 133601   22   203   51  11%      2  154   23    6  367%
c i   69.9   78627   572170     25618   14508   1580 133602   22   203   51  11%      1  154   23    6  365%
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   70.4   78621   572170     25966   14826   1587 133616   23   208   51  11%      2  157   29    6  448%
c i   70.4   78620   572170     25973   14832   1587 133616   23   207   51  11%      2  157   29    6  449%
c i   70.5   78619   572170     26066   14910   1590 133626   23   206   51  11%      2  156   27    6  414%
c i   70.5   78416   572170     26084   14921   1592 133628   23   206   51  11%      1  155   26    6  397%
c i   70.7   78407   572170     26212   15032   1599 133635   23   206   51  11%      1  155   24    7  362%
c i   70.7   78404   572170     26235   15053   1600 133635   23   205   51  11%      1  154   22    7  343%
c i   71.0   78402   572170     26419   15205   1612 133647   23   207   51  11%      1  156   27    7  403%
c i   71.0   78327   572170     26429   15210   1613 133650   23   207   51  11%      1  155   26    7  389%
c i   71.5   78323   572170     26894   15616   1629 133667   22   203   51  11%      2  151   20    7  305%
c i   72.6   78318   572170     27710   16331   1676 133701   24   200   51  12%      4  145   29    7  419%
c i   72.8   78314   572170     27836   16441   1681 133707   23   200   51  12%      4  146   25    7  365%
c i   73.0   78313   572170     28020   16600   1692 133718   24   202   51  12%      3  147   25    7  361%
c i   73.6   78308   572170     28396   16916   1720 133739   24   204   51  12%      3  148   25    7  348%
c i   73.6   78302   572170     28434   16949   1721 133741   24   202   51  12%      3  146   23    7  317%
c i   73.6   78298   572170     28437   16948   1722 133741   24   202   51  12%      3  146   22    7  314%
c i   73.6   78297   572170     28461   16967   1724 133742   23   201   51  12%      3  145   21    7  293%
c i   73.8   78291   572170     28654   17129   1730 133748   24   200   52  12%      3  143   28    7  385%
c i   74.6   78186   572170     29191   17618   1744 133763   25   204   53  12%      3  146   34    7  455%
c i   74.7   78183   572170     29222   17645   1747 133763   25   206   53  12%      3  148   32    7  426%
c i   75.2   78182   572170     29557   17955   1754 133769   26   207   53  12%      3  149   33    8  437%
c i   75.3   78179   572170     29673   18053   1758 133773   27   211   53  13%      2  152   46    8  600%
c i   75.8   78178   572170     30029   18372   1772 133787   28   217   55  13%      2  157   42    8  537%
c i   75.8   78177   572170     30030   18372   1772 133787   28   217   55  13%      2  157   42    8  535%
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   75.8   78176   572170     30031   18372   1772 133787   28   217   55  13%      2  157   42    8  533%
c i   76.7   78173   572170     30652   18911   1794 133819   28   217   55  13%      3  156   32    8  397%
c i   77.8   78172   572170     31561   19710   1825 133855   28   217   55  13%      6  154   26    8  314%
c i   78.2   78165   572170     31766   19890   1840 133860   29   221   55  13%      5  157   44    8  520%
c i   79.2   78163   572170     32422   20487   1857 133884   29   225   56  13%      5  160   28    9  328%
c i   79.4   78161   572170     32610   20657   1864 133890   29   227   56  13%      4  162   29    9  333%
c i   80.8   78160   572170     33457   21424   1888 133920   30   235   56  13%      5  167   31    9  345%
c i   80.9   78157   572170     33513   21473   1893 133921   30   235   56  13%      5  167   29    9  327%
c i   81.1   78154   572170     33656   21599   1899 133928   30   240   56  12%      4  172   35    9  390%
c i   81.1   78153   572170     33658   21600   1899 133928   30   240   56  12%      4  172   35    9  387%
c i   81.1   78152   572170     33681   21620   1899 133930   30   239   56  12%      4  171   33    9  364%
c i   81.2   78151   572170     33688   21622   1900 133932   30   239   56  12%      4  171   32    9  357%
c i   81.3   78143   572170     33809   21729   1901 133932   30   241   56  13%      4  172   38    9  412%
c i   81.6   78139   572170     33986   21890   1906 133936   30   240   56  13%      3  171   32    9  348%
c i   81.6   78135   572170     34075   21965   1911 133941   30   238   56  13%      3  169   31    9  337%
c i   82.0   78134   572170     34312   22184   1917 133947   30   239   56  12%      3  169   30    9  319%
c i   82.2   78131   572170     34460   22303   1928 133962   29   237   56  12%      2  167   24    9  258%
c i   82.7   78093   572170     34743   22551   1938 133979   29   233   56  12%      2  162   23    9  243%
c i   82.9   78039   572170     34926   22708   1948 133987   29   231   56  13%      2  160   26    9  276%
c i   83.0   78037   572170     34953   22731   1950 133988   29   230   56  13%      2  159   26    9  272%
c i   83.3   78033   572170     35219   22957   1966 134004   29   230   56  13%      2  158   30    9  320%
c i   84.1   78032   572170     35710   23388   1979 134029   29   232   57  13%      2  158   28   10  293%
c i   84.1   78030   572170     35735   23411   1979 134029   29   231   57  13%      2  158   27   10  282%
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   84.1   78029   572170     35772   23445   1980 134029   29   230   58  13%      2  157   26   10  273%
c i   84.4   78028   572170     35923   23578   1983 134036   29   232   58  12%      2  158   28   10  291%
c i   84.4   78023   572170     35924   23578   1983 134036   29   232   58  12%      2  158   28   10  289%
c i   84.4   78000   572170     35925   23578   1983 134036   29   232   58  12%      2  158   28   10  288%
c i   84.7   77994   572170     36139   23768   1985 134050   29   231   58  13%      1  156   33   10  337%
c i   85.3   77982   572170     36532   24124   1995 134064   29   231   59  13%      2  155   29   10  292%
c i   85.4   77977   572170     36599   24189   1996 134064   30   231   59  13%      2  156   39   10  391%
c i   85.4   77976   572170     36610   24198   1996 134065   30   231   59  13%      2  156   39   10  392%
c i   85.5   77975   572170     36715   24285   2003 134070   29   230   59  13%      1  155   32   10  320%
c i   86.4   77974   572170     37364   24854   2018 134090   32   233   59  14%      3  156   47   10  455%
c i   86.8   77967   572170     37655   25104   2026 134101   32   230   59  14%      2  152   36   10  351%
c i   86.8   77965   572170     37656   25104   2026 134101   32   230   59  14%      2  152   36   10  349%
c i   86.9   77962   572170     37762   25202   2029 134104   33   230   59  14%      2  151   51   11  483%
c i   87.0   77959   572170     37814   25249   2029 134107   33   227   59  14%      2  149   44   11  421%
c i   87.0   77956   572170     37819   25253   2029 134107   33   227   59  14%      2  149   44   11  414%
c i   87.1   77953   572170     37886   25308   2034 134111   33   228   59  14%      2  149   42   11  398%
c i   87.1   77952   572170     37895   25315   2034 134111   33   228   59  15%      2  149   42   11  394%
c 
c [simplification-11] limit 38023 conflicts (hard 47947) hit after 38023 conflicts
c [quatres-6] found 32549 quaternary clauses 40% in total
c [quatres-6-2] added 3 single-self-subsuming ternary resolvents
c [quatres-6-2] added 5 quaternary resolvents
c [ternres-7] limit 13952375 with penalty 0 = 0 + 0
c [ternres-7] 39640 schedulable variables 50%
c [ternres-7] 172 ternary resolvents (0 bin, 172 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-25] removed 1398 variables
c [treelook-4] limit 697618 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 75272 literals 48%
c [treelook-4] scheduling used 698204 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 697618 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 806461 steps
c [treelook-4] 75261 literals remain 48%
c [treelook-4] 15429 variables remain to probed next time 20%
c [treelook-4] removed 2 variables, found 2078 hbrs
c [unhide-11] limit 1395237 with penalty 1 = 0 + 1
c [unhide-11-11] 7 units, 495 failed, 6855 tauts, 0 hbrs, 55538 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 190 transitive binary clauses
c [transred-7] found 2 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 77503 variables 100%
c [block-4] limit of 34880938 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 55 blocked clauses
c [block-4] 55 < 1/100 * 558802 = 5588 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 77503 variables 100%
c [elim-9] limit of 279047510 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1239 variables 2% in round 1 in 54554900 steps
c [elim-9-1] backward subsumption/strengthening limit 54554900
c [elim-9-1-1] backward checking 4296 touched variables 6%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 9 and strengthened 81 clauses in 1669029 steps
c [elim-9-1] rescheduled 205 variables 0% by backward subsumption
c [elim-9-2] eliminated 25 variables 0% in round 2 in 488693 steps
c [elim-9-2] backward subsumption/strengthening limit 488600
c [elim-9-2-1] backward checking 200 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 151403 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 1271 = 2% variables out of 77503 scheduled
c [bca-7] limit of 10000000 steps and 1108741 added (scaled 2)
c [bca-7] 118676 out of 152466 literals actually usable 78%
c [bca-7] added 79 blocked clauses in 334643 steps
c [sweep-7] limit 4185712 penalty 0 = 0 + 0
c [sweep-7-1] 4974 pos 7.2% + 64466 neg 92.8% = 69440 sched 91.1% ret 6792
c [sweep-7-1] 4203505 steps 58 queries 9959.64 avg class size
c [sweep-7-1] 753 decisions 48 SAT calls 125.12 avg env size
c [sweep-7-1] 68869 variables remain 90% (7332 retained 10%)
c [decomp-27] removed 45 variables
c [sweep-7-1] removed 45 vars (0 failed, 11 eqs, 22 impls)
c [sweep-7] 45 < 1/1000 * 76232 = 76 considered unsuccessful
c [sweep-7] removed 45 vars in TOTAL (1 rounds, 57 queries)
c [phase-count-11] 548481 negative 99.1% of 553517 except 5036 0.9%
c [phase-count-11] 454408 positive 82.1% of 553517 except 99109 17.9%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 37 positive 100%, 0 negative 0%
c [score-distribution-11] 36963 pos 48.52%, 10583 min 13.89%, 28641 zero 37.59%
c [score-distribution-11] 5339 different 7.01% out of total 76187 variables
c [simplification-11] removed 1761 variables 2.3% (76187 remain 31%)
c [simplification-11] removed 18653 irredundant clauses 3.3% (553517 remain 40%)
c [simplification-11] maximum reduction of 3% = max (2%, 3%)
c [simplification-11] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-11] new conflict interval 20666
c [simplification-11] penalized conflict interval 20666 = 1 * 20666
c [simplification-11] hard conflict limit 69022 (soft 58689 + delta 10333)
c [simplification-11] new conflict limit 58689 (hard 69022)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   94.2   76186   553517     39341   21920   2094 133953   33   238   58  14%     10  157   39   11  351%
c i   95.3   76185   553517     40221   22693   2126 133992   33   236   58  14%      8  152   31   11  277%
c i   95.4   76130   553517     40267   22728   2130 133998   33   235   58  14%      8  151   28   11  243%
c i   95.5   76126   553517     40333   22789   2130 134001   33   235   58  14%      7  151   29   11  256%
c i   95.5   76125   553517     40335   22789   2130 134002   33   235   58  14%      7  151   29   11  254%
c i   96.7   76123   553517     41159   23541   2151 134015   33   245   58  13%      6  159   31   12  268%
c i   97.1   76118   553517     41433   23797   2155 134024   32   246   58  13%      5  159   29   12  251%
c i   97.1   76115   553517     41434   23797   2155 134024   32   246   58  13%      5  159   29   12  250%
c i   97.4   76110   553517     41593   23946   2157 134028   33   250   58  13%      4  163   40   12  338%
c i   97.4   76100   553517     41594   23946   2157 134028   33   250   58  13%      4  163   40   12  337%
c i   98.5   76062   553517     42308   24586   2183 134053   35   257   58  14%      4  169   42   12  347%
c i   98.5   76061   553517     42325   24602   2183 134053   36   257   58  14%      4  168   48   12  396%
c i   98.6   76060   553517     42418   24688   2183 134054   36   258   58  14%      4  169   47   12  385%
c i   99.4   76059   553517     42957   25182   2195 134070   38   259   58  15%      4  169   45   13  360%
c i   99.4   76053   553517     43031   25245   2199 134074   37   257   58  15%      3  166   40   13  318%
c i   99.5   76050   553517     43060   25271   2199 134076   37   256   58  15%      3  165   38   13  300%
c i   99.5   76047   553517     43138   25339   2201 134080   37   256   58  15%      3  165   34   13  274%
c i   99.5   76046   553517     43176   25371   2202 134080   37   254   58  15%      3  163   35   13  278%
c i  100.1   76043   553517     43541   25697   2217 134090   37   253   58  15%      2  161   33   13  261%
c i  100.1   76039   553517     43575   25727   2218 134091   37   253   58  14%      2  161   31   13  248%
c i  100.4   76038   553517     43760   25898   2224 134096   36   251   58  14%      2  159   29   13  227%
c i  100.9   76037   553517     44081   26175   2240 134117   37   253   58  15%      2  160   41   13  318%
c i  101.2   76036   553517     44247   26323   2247 134126   36   253   58  14%      1  159   33   13  257%
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  101.2   76035   553517     44258   26331   2247 134127   36   252   58  14%      1  158   34   13  264%
c i  101.5   76029   553517     44486   26539   2251 134130   37   255   58  15%      1  161   43   13  327%
c i  102.0   76027   553517     44812   26841   2256 134139   37   256   58  15%      1  160   37   13  281%
c i  102.4   76022   553517     45097   27085   2270 134156   37   252   58  15%      1  156   33   13  247%
c i  102.4   76021   553517     45105   27090   2270 134156   37   252   58  15%      1  156   36   13  269%
c i  102.8   76020   553517     45288   27254   2278 134162   37   254   59  15%      1  158   41   13  304%
c i  102.9   76016   553517     45339   27299   2280 134165   37   254   59  15%      1  158   37   13  280%
c i  102.9   76009   553517     45342   27300   2280 134166   37   254   59  15%      1  158   38   13  280%
c i  103.1   76005   553517     45490   27438   2283 134168   37   253   59  14%      1  156   31   13  235%
c i  103.9   76002   553517     46121   28022   2297 134180   37   257   59  14%      2  159   39   14  286%
c i  104.2   76001   553517     46323   28197   2307 134187   37   258   59  14%      2  160   38   14  280%
c i  105.0   75995   553517     46823   28643   2327 134206   37   258   59  14%      2  158   38   14  273%
c i  105.6   75984   553517     47186   28962   2337 134221   37   256   61  14%      2  155   34   14  244%
c i  105.8   75983   553517     47271   29038   2341 134224   37   257   61  14%      2  156   32   14  228%
c i  106.7   75982   553517     47817   29541   2350 134241   36   261   62  14%      2  159   35   14  247%
c i  106.8   75979   553517     47871   29591   2351 134242   36   261   62  14%      2  158   39   14  276%
c i  107.0   75977   553517     47939   29653   2352 134244   37   262   62  14%      2  160   52   14  361%
c i  107.2   75971   553517     48077   29778   2353 134246   38   267   63  14%      2  164   61   14  424%
c i  107.7   75930   553517     48393   30048   2368 134257   39   267   63  14%      1  164   47   15  321%
c i  108.0   75926   553517     48586   30223   2375 134262   38   267   63  14%      1  163   38   15  260%
c i  108.1   75920   553517     48639   30273   2377 134262   38   267   63  14%      1  163   36   15  247%
c i  108.6   75883   553517     49030   30628   2387 134273   39   264   63  15%      1  159   42   15  282%
c i  108.9   75882   553517     49268   30839   2392 134281   39   265   63  15%      1  159   42   15  285%
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  108.9   75881   553517     49307   30871   2393 134283   39   264   63  15%      1  158   40   15  272%
c i  109.0   75877   553517     49377   30937   2394 134284   39   262   63  15%      1  156   40   15  270%
c i  109.3   75874   553517     49523   31061   2399 134292   39   262   64  15%      1  155   42   15  281%
c i  109.8   75865   553517     49809   31310   2406 134306   42   272   64  15%      1  165   71   15  467%
c i  111.2   75619   553517     50887   32278   2437 134347   43   278   64  15%      6  168   53   16  333%
c i  111.2   75615   553517     50888   32278   2437 134347   43   278   64  15%      6  168   52   16  332%
c i  111.2   75611   553517     50911   32299   2437 134348   43   277   64  15%      5  167   52   16  330%
c i  111.3   75610   553517     51105   32468   2442 134355   43   273   64  16%      4  162   48   16  302%
c i  111.5   75609   553517     51242   32590   2448 134358   42   274   64  15%      4  163   35   16  219%
c i  112.2   75605   553517     51853   33136   2459 134365   45   278   65  16%      4  166   58   16  355%
c i  112.2   75600   553517     51895   33170   2459 134366   45   277   65  16%      3  165   53   16  328%
c i  112.5   75599   553517     52114   33366   2461 134377   45   281   65  16%      3  168   52   16  315%
c i  112.9   75065   553517     52477   33686   2476 134392   46   287   65  16%      2  173   44   17  267%
c i  113.1   75032   553517     52554   33751   2479 134392   47   290   65  16%      2  176   58   17  345%
c i  113.3   75031   553517     52757   33919   2490 134403   46   291   65  16%      2  176   51   17  305%
c i  113.3   75003   553517     52759   33919   2491 134403   46   290   65  16%      2  176   51   17  303%
c i  113.6   75002   553517     53055   34185   2499 134411   46   289   67  16%      1  173   45   17  266%
c i  113.6   74968   553517     53056   34185   2499 134411   46   289   67  16%      1  173   45   17  265%
c i  113.6   74942   553517     53057   34185   2499 134411   46   289   67  16%      1  173   45   17  264%
c i  113.7   74941   553517     53126   34247   2502 134414   45   288   67  16%      1  172   37   17  220%
c i  113.7   74933   553517     53128   34246   2502 134414   45   287   67  16%      1  172   37   17  219%
c i  113.8   74930   553517     53200   34315   2502 134415   45   288   67  16%      1  172   40   17  236%
c i  114.0   74929   553517     53365   34461   2505 134417   47   293   67  16%      1  177   57   17  335%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  114.5   74928   553517     53710   34769   2517 134432   48   304   67  16%      1  187   57   17  332%
c i  114.6   74908   553517     53786   34839   2518 134434   47   304   67  16%      1  186   50   17  287%
c i  114.6   74905   553517     53800   34851   2518 134434   47   303   67  16%      1  186   49   17  281%
c i  115.0   74900   553517     54044   35074   2522 134440   48   307   69  16%      1  189   54   17  308%
c i  115.3   74896   553517     54343   35354   2526 134444   48   315   69  15%      1  196   47   18  269%
c i  115.4   74893   553517     54346   35356   2526 134444   48   315   69  15%      1  196   47   18  268%
c i  115.9   74836   553517     54739   35715   2532 134461   49   319   69  15%      1  199   54   18  304%
c i  115.9   74829   553517     54740   35715   2532 134461   49   319   69  15%      1  199   54   18  303%
c i  116.3   74823   553517     55089   36026   2539 134470   48   318   69  15%      1  197   41   18  230%
c i  116.9   74822   553517     55559   36451   2547 134486   46   308   69  15%      1  186   30   18  167%
c i  117.1   74818   553517     55769   36637   2553 134493   46   306   69  15%      1  183   40   18  222%
c i  117.1   74812   553517     55770   36637   2553 134493   46   306   69  15%      1  183   40   18  221%
c i  117.7   74803   553517     56235   37052   2561 134503   50   312   71  16%      1  187   76   19  412%
c i  117.8   74802   553517     56248   37064   2561 134503   50   313   71  16%      1  189   75   19  404%
c i  118.3   74796   553517     56692   37465   2577 134513   52   313   71  16%      2  187   62   19  328%
c i  118.3   74716   553517     56709   37474   2579 134517   51   312   71  16%      2  186   59   19  314%
c i  118.8   74562   553517     57115   37822   2592 134532   52   320   71  16%      2  193   61   19  319%
c i  118.9   74561   553517     57150   37854   2593 134533   52   320   71  16%      1  193   58   19  300%
c i  118.9   74560   553517     57162   37863   2594 134534   52   319   71  16%      1  192   56   19  294%
c i  119.3   74212   553517     57546   38203   2601 134549   52   316   73  16%      1  187   47   19  242%
c i  119.4   74208   553517     57601   38246   2605 134551   52   315   73  16%      1  187   46   19  239%
c i  120.2   74207   553517     58230   38799   2626 134563   50   310   73  16%      2  180   46   20  235%
c i  120.3   74202   553517     58339   38895   2628 134568   51   313   73  16%      2  182   54   20  274%
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  120.4   74195   553517     58413   38965   2628 134569   50   311   73  16%      2  181   47   20  241%
c i  120.7   74194   553517     58604   39128   2636 134577   51   311   74  16%      1  180   52   20  263%
c i  120.9   74193   553517     58739   39250   2637 134578   54   319   74  17%      1  187   87   20  435%
c 
c [simplification-12] limit 58781 conflicts (hard 69022) hit after 58781 conflicts
c [quatres-7] found 32347 quaternary clauses 41% in total
c [quatres-7-1] removed 3 duplicate quaternary clauses
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [quatres-7-2] added 3 quaternary resolvents
c [ternres-8] limit 22439623 with penalty 0 = 0 + 0
c [ternres-8] all 74193 free variables schedulable
c [ternres-8] 123 ternary resolvents (0 bin, 123 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-28] removed 2262 variables
c [basicprobe-4] limit 112198118 penalty 0 = 0 + 0
c [basicprobe-4-0] 20805 probes remain 29% after last round
c [basicprobe-4-0] 605 units = 605 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 1246 variables, found 277959 hbrs
c [bate-2] eliminated 265 asymmetric tautologies during probing
c [unhide-12] limit 2243962 with penalty 1 = 0 + 1
c [unhide-12-12] 18 units, 657 failed, 53796 tauts, 0 hbrs, 212278 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 191 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 72118 variables 100%
c [elim-10] limit of 448792474 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 1671 variables 2% in round 1 in 48273563 steps
c [elim-10-1] backward subsumption/strengthening limit 48273500
c [elim-10-1-1] backward checking 6330 touched variables 9%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 19 and strengthened 279 clauses in 2066596 steps
c [elim-10-1] rescheduled 688 variables 1% by backward subsumption
c [elim-10-2] eliminated 85 variables 0% in round 2 in 1089203 steps
c [elim-10-2] backward subsumption/strengthening limit 1089200
c [elim-10-2-1] backward checking 680 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 7 and strengthened 17 clauses in 372972 steps
c [elim-10-2] rescheduled 53 variables 0% by backward subsumption
c [elim-10-3] eliminated 7 variables 0% in round 3 in 78600 steps
c [elim-10-3] backward subsumption/strengthening limit 78600
c [elim-10-3-1] backward checking 61 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 1 and strengthened 8 clauses in 78601 steps
c [elim-10] incomplete 33 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 1773 = 2% variables out of 72118 scheduled
c [bca-8] limit of 10000000 steps and 1021207 added (scaled 2)
c [bca-8] 105239 out of 140692 literals actually usable 75%
c [bca-8] added 63 blocked clauses in 303977 steps
c [phase-count-12] 505520 negative 99.1% of 510125 except 4605 0.9%
c [phase-count-12] 406473 positive 79.7% of 510125 except 103652 20.3%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [score-distribution-12] 34333 pos 48.81%, 12985 min 18.46%, 23027 zero 32.73%
c [score-distribution-12] 5624 different 7.99% out of total 70345 variables
c [simplification-12] removed 3848 variables 5.2% (70345 remain 29%)
c [simplification-12] removed 43392 irredundant clauses 7.8% (510125 remain 37%)
c [simplification-12] maximum reduction of 8% = max (5%, 8%)
c [simplification-12] large reduction 8% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 70781 (soft 60781 + delta 10000)
c [simplification-12] new conflict limit 60781 (hard 70781)
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  131.0   70344   510125     58989   28353   2644 328821   52   316   65  16%      1  184   48   20  238%
c i  131.1   70343   510125     59102   28456   2647 328824   51   314   66  16%      1  181   40   20  198%
c i  131.2   70340   510125     59139   28487   2650 328824   51   312   66  16%      1  179   37   20  183%
c i  131.3   70339   510125     59298   28617   2657 328838   50   309   66  16%      0  176   35   20  174%
c i  131.3   70338   510125     59299   28617   2657 328838   50   309   66  16%      0  176   35   20  174%
c i  132.0   70327   510125     59859   29131   2668 328851   49   308   66  16%      1  174   39   20  194%
c i  132.0   70318   510125     59897   29163   2669 328851   49   307   66  16%      1  172   38   20  188%
c i  132.2   70317   510125     60061   29305   2670 328863   49   304   66  16%      1  169   38   20  187%
c i  132.2   70316   510125     60099   29336   2671 328863   49   303   66  16%      1  168   41   20  201%
c i  132.4   70305   510125     60219   29436   2673 328863   49   301   66  16%      1  166   45   20  221%
c i  132.5   70304   510125     60345   29540   2680 328871   48   296   66  16%      1  161   41   20  202%
c i  132.8   70303   510125     60631   29799   2687 328879   49   293   66  17%      1  157   49   21  238%
c i  133.0   70271   510125     60774   29923   2695 328887   48   288   66  17%      0  151   36   21  177%
c 
c [simplification-13] limit 60791 conflicts (hard 70781) hit after 60792 conflicts
c [quatres-8] found 33313 quaternary clauses 44% in total
c [quatres-8-1] removed 3 duplicate quaternary clauses
c [quatres-8-2] added 3 single-self-subsuming ternary resolvents
c [quatres-8-2] added 1 quaternary resolvents
c [ternres-9] limit 23056762 with penalty 0 = 0 + 0
c [ternres-9] all 70270 free variables schedulable
c [ternres-9] 263 ternary resolvents (0 bin, 263 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-5] limit 1152838 penalty 2 = 2 + 0
c [gauss-5] extracted 25 xors of average arity 2.9
c [gauss-5] connected 72 occurrences of 64 variables (average 1.1)
c [gauss-5] limit 1152838 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-29] removed 29 variables
c [simpleprobe-5] 2056 schedulable variables 3%
c [simpleprobe-5] limit 92227049 penalty 0 = 0 + 0
c [decomp-30] removed 1093 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 1093 variables, found 83440 hbrs, 438 units
c [unhide-13] limit 2305676 with penalty 1 = 0 + 1
c [unhide-13-13] 7 units, 63 failed, 17792 tauts, 0 hbrs, 55778 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 243 transitive binary clauses
c [transred-9] found 1 units
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 69029 variables 100%
c [elim-11] limit of 461135248 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 741 variables 1% in round 1 in 45059697 steps
c [elim-11-1] backward subsumption/strengthening limit 45059600
c [elim-11-1-1] backward checking 3319 touched variables 5%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 39 and strengthened 55 clauses in 1083988 steps
c [elim-11-1] rescheduled 211 variables 0% by backward subsumption
c [elim-11-2] eliminated 27 variables 0% in round 2 in 203178 steps
c [elim-11-2] backward subsumption/strengthening limit 203100
c [elim-11-2-1] backward checking 198 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 5 and strengthened 19 clauses in 168839 steps
c [elim-11-2] rescheduled 52 variables 0% by backward subsumption
c [elim-11-3] eliminated 5 variables 0% in round 3 in 62697 steps
c [elim-11-3] backward subsumption/strengthening limit 62600
c [elim-11-3-1] backward checking 59 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 1 and strengthened 4 clauses in 62601 steps
c [elim-11] incomplete 17 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 781 = 1% variables out of 69029 scheduled
c [bca-9] limit of 10000000 steps and 970232 added (scaled 2)
c [bca-9] 102246 out of 136498 literals actually usable 75%
c [bca-9] added 49 blocked clauses in 289957 steps
c [sweep-8] limit 3458514 penalty 1 = 1 + 0
c [sweep-8-1] 5036 pos 8.1% + 57457 neg 91.9% = 62493 sched 91.6% ret 5755
c [sweep-8-1] 3886067 steps 59 queries 7688.95 avg class size
c [sweep-8-1] 863 decisions 52 SAT calls 181.48 avg env size
c [sweep-8-1] 61600 variables remain 90% (6636 retained 10%)
c [decomp-31] removed 40 variables
c [sweep-8-1] removed 40 vars (0 failed, 7 eqs, 15 impls)
c [sweep-8] 40 < 1/1000 * 68248 = 68 considered unsuccessful
c [sweep-8] removed 40 vars in TOTAL (1 rounds, 58 queries)
c [phase-count-13] 479870 negative 99.1% of 484345 except 4475 0.9%
c [phase-count-13] 390964 positive 80.7% of 484345 except 93381 19.3%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 1 negative 100%
c [score-distribution-13] 33393 pos 48.96%, 12802 min 18.77%, 22013 zero 32.27%
c [score-distribution-13] 5617 different 8.24% out of total 68208 variables
c [simplification-13] removed 2062 variables 2.9% (68208 remain 28%)
c [simplification-13] removed 25780 irredundant clauses 5.1% (484345 remain 35%)
c [simplification-13] maximum reduction of 5% = max (3%, 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 72792 (soft 62792 + delta 10000)
c [simplification-13] new conflict limit 62792 (hard 72792)
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  139.9   68207   484345     61491   25081   2751 395808   46   290   61  16%      2  151   40   21  192%
c i  140.6   68206   484345     62152   25673   2776 395822   45   275   61  16%      3  135   34   21  160%
c i  141.1   68205   484345     62681   26148   2789 395836   46   276   62  17%      3  135   44   21  209%
c 
c [simplification-14] limit 62792 conflicts (hard 72792) hit after 62793 conflicts
c [quatres-9] found 31828 quaternary clauses 43% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [quatres-9-2] added 4 single-self-subsuming ternary resolvents
c [quatres-9-2] added 12 quaternary resolvents
c [ternres-10] limit 23693589 with penalty 0 = 0 + 0
c [ternres-10] all 68205 free variables schedulable
c [ternres-10] 538 ternary resolvents (0 bin, 538 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-32] removed 3 variables
c [treelook-5] limit 2369358 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 101679 literals 75%
c [treelook-5] scheduling used 1775823 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2369358 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2402711 steps
c [treelook-5] 101631 literals remain 75%
c [treelook-5] 12535 variables remain to probed next time 18%
c [decomp-33] removed 2 variables
c [treelook-5] removed 11 variables, found 9836 hbrs
c [unhide-14] limit 2369358 with penalty 1 = 0 + 1
c [unhide-14-14] 34 units, 368 failed, 42358 tauts, 0 hbrs, 47923 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 197 transitive binary clauses
c [transred-10] found 2 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 148084932 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 116 (1%) of length 10
c [cce-4-1] eliminated 1 clauses out of 465 (0%) of length 8
c [cce-4-1] eliminated 16 clauses out of 676 (2%) of length 7
c [cce-4-1] eliminated 2418 clauses out of 4500 (54%) of length 6
c [cce-4-1] eliminated 12179 clauses out of 29581 (41%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 14615 large clauses in 148084942 steps
c [cce-4-1] allowing another 74042471 steps for small clauses
c [cce-4-1] scheduling 249331 clauses = 230708 binary + 18623 ternary
c [cce-4-1] tried to eliminate 2904 small clauses 1%
c [cce-4-1] eliminated 729 binary clauses 0%
c [cce-4-1] eliminated 135 ternary clauses 1%
c [cce-4-1] eliminated 864 small clauses 0%
c [cce-4-1] eliminated 3019 small clauses in 148084937 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 17634 covered clauses in round 1
c [cce-4] eliminated 17634 covered clauses in TOTAL during 1 rounds
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 67939 variables 100%
c [elim-12] limit of 473871786 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 7894 variables 12% in round 1 in 42164977 steps
c [elim-12-1] backward subsumption/strengthening limit 42164900
c [elim-12-1-1] backward checking 19412 touched variables 29%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 19 and strengthened 35 clauses in 3822724 steps
c [elim-12-1] rescheduled 115 variables 0% by backward subsumption
c [elim-12-2] eliminated 12 variables 0% in round 2 in 177705 steps
c [elim-12-2] backward subsumption/strengthening limit 177700
c [elim-12-2-1] backward checking 110 touched variables 0%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 7 and strengthened 6 clauses in 177701 steps
c [elim-12-2] rescheduled 35 variables 0% by backward subsumption
c [elim-12-3] eliminated 3 variables 0% in round 3 in 38586 steps
c [elim-12-3] backward subsumption/strengthening limit 38500
c [elim-12-3-1] backward checking 30 touched variables 0%
c [elim-12-3-1] incomplete backward checking 0 remain 0%
c [elim-12-3] subsumed 2 and strengthened 4 clauses in 38501 steps
c [elim-12] incomplete 18 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 7914 = 12% variables out of 67939 scheduled
c [bca-10] limit of 10000000 steps and 894281 added (scaled 2)
c [bca-10] 98174 out of 120052 literals actually usable 82%
c [bca-10] added 201 blocked clauses in 254341 steps
c [phase-count-14] 445223 negative 99.7% of 446634 except 1411 0.3%
c [phase-count-14] 354128 positive 79.3% of 446634 except 92506 20.7%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [score-distribution-14] 28224 pos 47.02%, 11677 min 19.45%, 20124 zero 33.53%
c [score-distribution-14] 5490 different 9.15% out of total 60025 variables
c [simplification-14] removed 8180 variables 12.0% (60025 remain 24%)
c [simplification-14] removed 37711 irredundant clauses 7.8% (446634 remain 33%)
c [simplification-14] maximum reduction of 12% = max (12%, 8%)
c [simplification-14] large reduction 12% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 74793 (soft 64793 + delta 10000)
c [simplification-14] new conflict limit 64793 (hard 74793)
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  149.7   60024   446634     62993   11482   3119 342489   45   276   47  16%      2  134   27   21  125%
c i  149.7   59973   446634     63093   11572   3123 342493   44   275   47  16%      2  133   20   21   96%
c i  150.2   59972   446634     63546   11984   3135 342505   42   275   47  15%      2  132   27   21  127%
c i  150.3   59969   446634     63669   12097   3139 342505   42   273   47  15%      2  129   31   21  147%
c i  150.4   59965   446634     63789   12206   3142 342510   41   272   47  15%      1  129   26   21  124%
c i  150.6   59964   446634     64242   12587   3148 342528   39   269   47  15%      1  124   24   21  114%
c 
c [simplification-15] limit 64793 conflicts (hard 74793) hit after 64794 conflicts
c [quatres-10] found 35664 quaternary clauses 58% in total
c [quatres-10-1] removed 5 duplicate quaternary clauses
c [quatres-10-2] added 2 single-self-subsuming ternary resolvents
c [quatres-10-2] added 3 quaternary resolvents
c [ternres-11] limit 24178766 with penalty 0 = 0 + 0
c [ternres-11] all 59962 free variables schedulable
c [ternres-11] 122 ternary resolvents (1 bin, 121 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 755586 penalty 4 = 4 + 0
c [card-5] found 1546 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 755586 for elimination
c [card-5] 1546 out of 1546 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-34] removed 69 variables
c [basicprobe-5] limit 120893832 penalty 0 = 0 + 0
c [basicprobe-5-0] 11695 probes remain 20% after last round
c [basicprobe-5-0] 690 units = 678 failed (98%) + 12 lifted (2%)
c [basicprobe-5-0] removed 1158 variables, found 315495 hbrs
c [bate-3] eliminated 710 asymmetric tautologies during probing
c [unhide-15] limit 4835753 with penalty 0 = 0 + 0
c [unhide-15-16] 17 units, 335 failed, 83344 tauts, 0 hbrs, 31463 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 161 transitive binary clauses
c [transred-11] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 58528 variables 100%
c [block-5] limit of 30223458 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 229 blocked clauses
c [block-5] 229 < 1/100 * 429483 = 4294 considered unsuccessful
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 58527 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 745 variables 1% in round 1 in 37773091 steps
c [elim-13-1] backward subsumption/strengthening limit 37773000
c [elim-13-1-1] backward checking 3824 touched variables 7%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 7 and strengthened 64 clauses in 1221558 steps
c [elim-13-1] rescheduled 207 variables 0% by backward subsumption
c [elim-13-2] eliminated 16 variables 0% in round 2 in 163240 steps
c [elim-13-2] backward subsumption/strengthening limit 163200
c [elim-13-2-1] backward checking 172 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 0 and strengthened 6 clauses in 143906 steps
c [elim-13-2] rescheduled 22 variables 0% by backward subsumption
c [elim-13-3] eliminated 2 variables 0% in round 3 in 26264 steps
c [elim-13-3] backward subsumption/strengthening limit 26200
c [elim-13-3-1] backward checking 20 touched variables 0%
c [elim-13-3-1] incomplete backward checking 0 remain 0%
c [elim-13-3] subsumed 0 and strengthened 4 clauses in 26201 steps
c [elim-13] incomplete 14 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 767 = 1% variables out of 58527 scheduled
c [bca-11] limit of 10000000 steps and 851119 added (scaled 2)
c [bca-11] 91823 out of 115522 literals actually usable 79%
c [bca-11] added 65 blocked clauses in 231786 steps
c [phase-count-15] 423642 negative 99.7% of 425003 except 1361 0.3%
c [phase-count-15] 336174 positive 79.1% of 425003 except 88829 20.9%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [score-distribution-15] 30467 pos 52.75%, 9047 min 15.66%, 18246 zero 31.59%
c [score-distribution-15] 5575 different 9.65% out of total 57760 variables
c [simplification-15] removed 2202 variables 3.7% (57760 remain 23%)
c [simplification-15] removed 21631 irredundant clauses 4.8% (425003 remain 31%)
c [simplification-15] maximum reduction of 5% = max (4%, 5%)
c [simplification-15] large reduction 5% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 76794 (soft 66794 + delta 10000)
c [simplification-15] new conflict limit 66794 (hard 76794)
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  161.1   57759   425003     65406   13015   3328 558245   39   261   52  15%      6  115   31   22  143%
c i  161.5   57689   425003     66040   13592   3345 558251   37   252   52  15%      5  105   28   22  127%
c i  161.6   57688   425003     66129   13664   3347 558251   37   250   52  15%      4  102   38   22  177%
c i  161.7   57687   425003     66218   13747   3350 558251   37   250   52  15%      4  102   39   22  179%
c i  161.8   57686   425003     66346   13861   3360 558253   37   251   52  15%      3  103   30   22  138%
c i  162.0   57682   425003     66600   14059   3379 558264   35   251   52  14%      3  102   20   22   92%
c 
c [simplification-16] limit 66794 conflicts (hard 76794) hit after 66794 conflicts
c [quatres-11] found 33597 quaternary clauses 60% in total
c [quatres-11-1] removed 3 duplicate quaternary clauses
c [quatres-11-2] added 2 single-self-subsuming ternary resolvents
c [quatres-11-2] added 14 quaternary resolvents
c [ternres-12] limit 24661611 with penalty 0 = 0 + 0
c [ternres-12] all 57591 free variables schedulable
c [ternres-12] 416 ternary resolvents (0 bin, 416 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-35] removed 178 variables
c [simpleprobe-6] all 57582 free variables schedulable
c [simpleprobe-6] limit 98646447 penalty 0 = 0 + 0
c [decomp-36] removed 470 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 470 variables, found 75328 hbrs, 279 units
c [unhide-16] limit 4932322 with penalty 0 = 0 + 0
c [unhide-16-18] 17 units, 104 failed, 42719 tauts, 0 hbrs, 31623 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 185 transitive binary clauses
c [cce-5] limit of 30827014 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 15 (7%) of length 10
c [cce-5-1] eliminated 1 clauses out of 133 (1%) of length 8
c [cce-5-1] eliminated 7 clauses out of 235 (3%) of length 7
c [cce-5-1] eliminated 26 clauses out of 2636 (1%) of length 6
c [cce-5-1] eliminated 436 clauses out of 14996 (3%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 471 large clauses in 30827021 steps
c [cce-5-1] allowing another 15413510 steps for small clauses
c [cce-5-1] scheduling 346501 clauses = 194435 binary + 152066 ternary
c [cce-5-1] tried to eliminate 450 small clauses 0%
c [cce-5-1] eliminated 61 binary clauses 0%
c [cce-5-1] eliminated 32 ternary clauses 0%
c [cce-5-1] eliminated 93 small clauses 0%
c [cce-5-1] eliminated 204 small clauses in 30827024 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 675 covered clauses in round 1
c [cce-5] eliminated 675 covered clauses in TOTAL during 1 rounds
c [cce-5] 675 < 1/100 * 416861 = 4168 considered unsuccessful
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 57008 variables 100%
c [elim-14] limit of 493232238 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 1039 variables 2% in round 1 in 36659882 steps
c [elim-14-1] backward subsumption/strengthening limit 36659800
c [elim-14-1-1] backward checking 4129 touched variables 7%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 17 and strengthened 142 clauses in 1173931 steps
c [elim-14-1] rescheduled 388 variables 1% by backward subsumption
c [elim-14-2] eliminated 49 variables 0% in round 2 in 432747 steps
c [elim-14-2] backward subsumption/strengthening limit 432700
c [elim-14-2-1] backward checking 384 touched variables 1%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 0 and strengthened 2 clauses in 226513 steps
c [elim-14-2] rescheduled 8 variables 0% by backward subsumption
c [elim-14-3] eliminated 1 variables 0% in round 3 in 11973 steps
c [elim-14-3] backward subsumption/strengthening limit 11900
c [elim-14-3-1] backward checking 10 touched variables 0%
c [elim-14-3-1] incomplete backward checking 6 remain 60%
c [elim-14-3] subsumed 0 and strengthened 2 clauses in 11928 steps
c [elim-14] incomplete 8 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 1093 = 2% variables out of 57008 scheduled
c [bca-12] limit of 10000000 steps and 827492 added (scaled 2)
c [bca-12] 88260 out of 111832 literals actually usable 79%
c [bca-12] added 77 blocked clauses in 219652 steps
c [sweep-9] limit 1849620 penalty 2 = 2 + 0
c [sweep-9-1] 5079 pos 10.0% + 45894 neg 90.0% = 50973 sched 91.2% ret 4942
c [sweep-9-1] 1891089 steps 40 queries 10017.50 avg class size
c [sweep-9-1] 665 decisions 35 SAT calls 172.66 avg env size
c [sweep-9-1] 50652 variables remain 91% (5261 retained 9%)
c [decomp-37] removed 11 variables
c [sweep-9-1] removed 11 vars (0 failed, 5 eqs, 8 impls)
c [sweep-9] 11 < 1/1000 * 55915 = 55 considered unsuccessful
c [sweep-9] removed 11 vars in TOTAL (1 rounds, 39 queries)
c [phase-count-16] 411852 negative 99.7% of 413140 except 1288 0.3%
c [phase-count-16] 326299 positive 79.0% of 413140 except 86841 21.0%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [score-distribution-16] 23506 pos 42.05%, 15352 min 27.46%, 17046 zero 30.49%
c [score-distribution-16] 4078 different 7.29% out of total 55904 variables
c [simplification-16] removed 1687 variables 2.9% (55904 remain 23%)
c [simplification-16] removed 11863 irredundant clauses 2.8% (413140 remain 30%)
c [simplification-16] maximum reduction of 3% = max (3%, 3%)
c [simplification-16] geometric conflict interval increment 5166 = 20666 / 4
c [simplification-16] new conflict interval 25832
c [simplification-16] penalized conflict interval 25832 = 1 * 25832
c [simplification-16] hard conflict limit 105542 (soft 92626 + delta 12916)
c [simplification-16] new conflict limit 92626 (hard 105542)
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  168.9   55903   413140     66826   12520   3597 572168   34   244   51  14%      2   96   14   22   67%
c i  170.6   55832   413140     69089   14544   3666 572225   32   251   53  13%     19   99   21   22   96%
c i  170.6   55828   413140     69090   14544   3666 572225   32   250   53  13%     19   99   21   22   96%
c i  171.3   55801   413140     70045   15389   3704 572258   31   246   54  12%     11   92   27   22  122%
c i  171.8   55795   413140     70677   15988   3714 572263   30   244   54  12%      7   90   31   22  141%
c i  171.9   55794   413140     70693   16003   3714 572263   30   244   54  12%      7   90   30   22  137%
c i  172.3   55793   413140     71188   16451   3728 572285   30   250   54  12%      5   95   29   22  132%
c i  172.5   55792   413140     71393   16632   3738 572289   29   249   54  12%      4   94   23   22  103%
c i  172.5   55788   413140     71395   16633   3738 572289   29   249   54  12%      4   93   22   22  102%
c i  172.5   55785   413140     71400   16634   3739 572291   29   248   54  12%      4   93   22   22  100%
c i  173.2   55691   413140     72269   17425   3762 572301   33   256   56  13%      4   99   50   22  225%
c i  175.0   55685   413140     74251   19219   3826 572354   32   254   58  13%     15   95   36   23  159%
c i  175.8   55684   413140     75081   19963   3861 572382   31   255   58  12%      9   95   24   23  107%
c i  176.5   55647   413140     75798   20631   3874 572396   31   250   59  12%      6   89   33   23  146%
c i  177.0   55646   413140     76244   21028   3885 572410   32   258   60  12%      4   96   38   23  167%
c i  177.3   55645   413140     76596   21348   3890 572415   32   261   60  12%      3   98   34   23  150%
c i  177.4   55644   413140     76671   21419   3893 572415   32   261   60  12%      2   98   32   23  139%
c i  177.5   55608   413140     76761   21503   3894 572417   32   260   60  12%      2   97   31   23  134%
c i  177.8   55601   413140     77164   21868   3899 572427   31   257   60  12%      1   93   27   23  119%
c i  177.9   55600   413140     77228   21923   3903 572427   32   259   60  12%      1   96   35   23  150%
c i  178.4   55479   413140     77727   22384   3914 572440   34   263   60  13%      1   98   44   23  190%
c i  178.5   55478   413140     77800   22451   3916 572441   34   263   60  13%      1   99   42   23  180%
c i  178.5   55477   413140     77839   22484   3917 572443   34   264   60  13%      1   99   40   23  171%
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  178.9   55476   413140     78201   22820   3929 572446   34   265   60  13%      0  100   36   23  155%
c i  179.3   55475   413140     78693   23256   3943 572454   35   258   60  14%      1   92   45   23  191%
c i  180.5   55474   413140     79940   24382   3974 572483   36   261   61  14%      6   94   37   24  157%
c i  180.9   55452   413140     80349   24770   3979 572490   37   261   61  14%      4   93   39   24  162%
c i  181.1   55451   413140     80555   24962   3981 572492   39   269   61  15%      3  101   61   24  255%
c i  181.9   55450   413140     81368   25699   3997 572514   39   266   62  15%      3   96   40   24  167%
c i  181.9   55414   413140     81370   25700   3997 572514   39   266   62  15%      3   96   40   24  166%
c i  182.4   55413   413140     81812   26104   4015 572525   38   262   62  14%      2   92   34   24  139%
c i  182.5   55412   413140     81997   26274   4019 572527   38   258   62  15%      2   88   36   24  148%
c i  182.5   55411   413140     81998   26274   4019 572527   38   258   62  15%      2   87   36   24  147%
c i  182.9   55410   413140     82403   26647   4033 572536   37   255   64  15%      1   84   34   24  140%
c i  183.7   55409   413140     83141   27309   4054 572547   40   252   66  16%      2   80   51   25  207%
c i  184.2   55408   413140     83725   27843   4071 572563   39   252   66  16%      2   79   39   25  157%
c i  184.3   55407   413140     83854   27962   4073 572563   39   253   66  15%      1   80   35   25  143%
c i  184.4   55386   413140     83971   28071   4076 572565   41   256   66  16%      1   83   57   25  229%
c i  184.5   55378   413140     84010   28107   4076 572566   41   256   66  16%      1   83   53   25  212%
c i  184.5   55377   413140     84026   28120   4077 572567   41   257   66  16%      1   84   54   25  216%
c i  184.6   55376   413140     84101   28184   4082 572569   40   259   66  16%      0   85   45   25  183%
c i  184.6   55253   413140     84128   28207   4083 572571   40   258   66  16%      0   85   43   25  172%
c i  184.8   55248   413140     84252   28318   4083 572572   41   259   66  16%      0   86   50   25  200%
c i  184.8   55247   413140     84300   28364   4083 572572   41   260   66  16%     -0   86   50   25  200%
c i  185.5   55246   413140     84976   28969   4108 572591   42   264   66  16%      1   90   43   25  172%
c i  186.0   55241   413140     85420   29375   4112 572596   43   267   69  16%      1   92   50   25  198%
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  188.0   55239   413140     87295   31070   4147 572638   48   285   70  17%     13  107   66   26  250%
c i  189.0   55238   413140     88278   31965   4163 572669   48   282   70  17%      8  102   51   27  193%
c i  190.2   55237   413140     89421   33025   4182 572678   48   277   70  17%      7   96   49   27  183%
c i  190.4   55235   413140     89670   33254   4190 572681   48   276   70  17%      5   95   49   27  182%
c i  190.6   55234   413140     89871   33433   4196 572688   49   277   71  18%      4   95   58   27  213%
c i  191.3   55187   413140     90562   34057   4207 572699   53   278   72  19%      3   96   88   28  318%
c i  191.6   55186   413140     90870   34340   4210 572704   55   280   72  20%      2   97   79   28  284%
c i  191.6   55185   413140     90871   34340   4210 572704   55   280   72  20%      2   97   79   28  283%
c i  192.2   55183   413140     91392   34800   4219 572721   55   284   72  19%      1  100   56   28  200%
c i  192.9   55182   413140     92033   35379   4230 572727   52   272   72  19%      1   87   42   28  151%
c i  193.0   55115   413140     92152   35490   4235 572727   52   273   72  19%      1   88   42   28  148%
c i  193.1   55114   413140     92238   35567   4236 572728   52   270   72  19%      1   85   42   28  149%
c i  193.4   55113   413140     92513   35822   4236 572731   52   270   74  19%      0   85   54   28  192%
c i  193.5   55112   413140     92598   35900   4237 572734   52   274   74  19%     -0   89   54   28  191%
c 
c [simplification-17] limit 92668 conflicts (hard 105542) hit after 93090 conflicts
c [quatres-12] found 30991 quaternary clauses 57% in total
c [quatres-12-1] removed 3 duplicate quaternary clauses
c [quatres-12-2] added 2 single-self-subsuming ternary resolvents
c [quatres-12-2] added 5 quaternary resolvents
c [ternres-13] limit 32435657 with penalty 0 = 0 + 0
c [ternres-13] all 55112 free variables schedulable
c [ternres-13] 332 ternary resolvents (2 bin, 330 trn)
c [ternres-13] fully completed ternary resolution
c [gauss-6] limit 810891 penalty 3 = 3 + 0
c [gauss-6] extracted 21 xors of average arity 2.7
c [gauss-6] connected 56 occurrences of 53 variables (average 1.1)
c [gauss-6] limit 810891 penalty 3 = 3 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-38] removed 48 variables
c [treelook-6] limit 3243565 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 81856 literals 74%
c [treelook-6] scheduling used 1718271 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3243565 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 3323351 steps
c [treelook-6] 81699 literals remain 74%
c [treelook-6] 9728 variables remain to probed next time 18%
c [treelook-6] removed 56 variables, found 6819 hbrs
c [unhide-17] limit 3243565 with penalty 1 = 0 + 1
c [unhide-17-20] 2 units, 131 failed, 21482 tauts, 0 hbrs, 251556 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 146 transitive binary clauses
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 54783 variables 100%
c [elim-15] limit of 648713156 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 747 variables 1% in round 1 in 36321710 steps
c [elim-15-1] backward subsumption/strengthening limit 36321700
c [elim-15-1-1] backward checking 3245 touched variables 6%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 3 and strengthened 13 clauses in 1064710 steps
c [elim-15-1] rescheduled 55 variables 0% by backward subsumption
c [elim-15-2] eliminated 5 variables 0% in round 2 in 33965 steps
c [elim-15-2] backward subsumption/strengthening limit 33900
c [elim-15-2-1] backward checking 58 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 11 and strengthened 8 clauses in 33901 steps
c [elim-15-2] rescheduled 24 variables 0% by backward subsumption
c [elim-15-3] eliminated 3 variables 0% in round 3 in 22261 steps
c [elim-15-3] backward subsumption/strengthening limit 22200
c [elim-15-3-1] backward checking 28 touched variables 0%
c [elim-15-3-1] incomplete backward checking 2 remain 7%
c [elim-15-3] subsumed 0 and strengthened 2 clauses in 22211 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 755 = 1% variables out of 54783 scheduled
c [bca-13] limit of 10000000 steps and 802104 added (scaled 2)
c [bca-13] 74596 out of 108058 literals actually usable 69%
c [bca-13] added 48 blocked clauses in 201458 steps
c [score-distribution-17] 28167 pos 52.13%, 11323 min 20.96%, 14538 zero 26.91%
c [score-distribution-17] 5096 different 9.43% out of total 54028 variables
c [simplification-17] removed 1084 variables 2.0% (54028 remain 22%)
c [simplification-17] removed 12680 irredundant clauses 3.1% (400460 remain 29%)
c [simplification-17] maximum reduction of 3% = max (2%, 3%)
c [simplification-17] geometric conflict interval increment 6458 = 25832 / 4
c [simplification-17] new conflict interval 32290
c [simplification-17] penalized conflict interval 32290 = 1 * 32290
c [simplification-17] hard conflict limit 141525 (soft 125380 + delta 16145)
c [simplification-17] new conflict limit 125380 (hard 141525)
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  200.6   54027   400460     93892   33881   4353 537524   52   275   74  19%      6   88   65   29  225%
c i  203.0   54026   400460     96206   35980   4403 537563   52   269   74  19%     19   79   53   30  180%
c i  203.4   54025   400460     96503   36248   4407 537569   53   273   74  19%     13   82   66   30  221%
c i  203.7   54024   400460     96776   36491   4415 537581   52   275   74  19%     10   84   46   30  154%
c i  204.5   54023   400460     97591   37215   4438 537602   52   269   74  19%      6   77   54   30  178%
c i  204.8   54022   400460     97866   37466   4438 537604   52   269   74  19%      4   77   58   30  193%
c i  204.8   54021   400460     97867   37466   4438 537604   52   269   74  19%      4   77   58   30  192%
c i  205.0   54018   400460     98030   37607   4441 537611   52   269   74  19%      3   77   55   30  181%
c i  205.0   53956   400460     98073   37647   4443 537611   52   268   74  19%      3   75   48   30  159%
c i  205.2   53954   400460     98213   37775   4446 537611   52   267   74  19%      2   74   48   30  159%
c i  208.2   53953   400460    101112   40420   4490 537645   60   272   75  22%     26   76   78   32  245%
c i  209.5   53947   400460    102428   41555   4516 537667   56   260   75  22%     12   63   49   32  152%
c i  211.1   53946   400460    103884   42902   4536 537687   56   264   75  21%      9   65   44   33  136%
c i  211.1   53945   400460    103946   42958   4538 537689   55   262   75  21%      9   64   44   33  135%
c i  212.3   53857   400460    104925   43837   4567 537708   57   266   75  21%      5   67   64   33  194%
c i  215.0   53856   400460    107467   46123   4618 537747   57   266   77  21%     20   64   51   34  151%
c i  217.1   53763   400460    109362   47879   4652 537770   60   275   83  22%     14   71   49   35  140%
c i  217.3   53675   400460    109516   48016   4660 537773   59   277   83  21%     11   72   45   35  129%
c i  218.4   53628   400460    110637   49021   4688 537793   54   254   86  21%      6   49   40   35  114%
c i  219.7   53618   400460    111764   50040   4709 537809   54   256   86  21%      5   49   52   35  147%
c i  219.9   53617   400460    111901   50166   4709 537810   54   256   86  21%      4   49   61   35  173%
c i  222.4   53612   400460    113828   51916   4742 537840   59   278   89  21%     12   70   69   36  190%
c i  223.0   53608   400460    114313   52351   4759 537848   59   281   89  21%      6   72   57   36  156%
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  225.5   53607   400460    116703   54459   4797 537878   61   258   94  23%     17   48   56   37  150%
c i  225.7   53606   400460    116843   54582   4797 537882   60   260   94  23%     14   49   53   37  141%
c i  227.3   53605   400460    118202   55797   4813 537906   60   250   97  24%      8   38   48   38  127%
c i  228.5   53602   400460    119271   56781   4830 537914   62   260   97  24%      5   48   71   38  185%
c i  229.6   53601   400460    120064   57499   4841 537922   65   266   97  25%      2   53   94   39  242%
c i  229.7   53600   400460    120205   57632   4844 537923   65   266   97  24%      1   53   72   39  186%
c i  229.8   53599   400460    120237   57661   4844 537924   65   268   97  24%      1   55   85   39  219%
c i  231.2   53597   400460    121419   58732   4871 537935   63   264   99  24%      3   50   47   39  121%
c i  232.1   53596   400460    122288   59530   4879 537937   62   260   99  24%      2   45   73   39  184%
c i  233.1   53595   400460    123010   60183   4893 537943   66   264   99  25%      0   48   88   40  220%
c -  234.6   53595   400460    124115   21584   4904 537963   70   273   51  26%      2   57   83   41  203%
c i  235.1   53594   400460    124511   21953   4912 537964   70   274   56  26%      6   57   83   41  203%
c i  235.1   53593   400460    124531   21971   4913 537964   70   274   56  26%      5   57   78   41  191%
c 
c [simplification-18] limit 125390 conflicts (hard 141525) hit after 125393 conflicts
c [quatres-13] found 29600 quaternary clauses 55% in total
c [quatres-13-1] removed 1 duplicate quaternary clauses
c [quatres-13-2] added 3 single-self-subsuming ternary resolvents
c [quatres-13-2] added 4 quaternary resolvents
c [ternres-14] limit 42428119 with penalty 0 = 0 + 0
c [ternres-14] all 53591 free variables schedulable
c [ternres-14] 230 ternary resolvents (0 bin, 230 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-40] removed 667 variables
c [basicprobe-6] limit 212140596 penalty 0 = 0 + 0
c [basicprobe-6-0] 5033 probes remain 10% after last round
c [basicprobe-6-0] 986 units = 958 failed (97%) + 28 lifted (3%)
c [basicprobe-6-0] removed 1456 variables, found 470790 hbrs
c [bate-4] eliminated 1004 asymmetric tautologies during probing
c [unhide-18] limit 8485623 with penalty 0 = 0 + 0
c [unhide-18-23] 5 units, 214 failed, 129882 tauts, 0 hbrs, 69140 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 84 transitive binary clauses
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 51737 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 809 variables 2% in round 1 in 34570947 steps
c [elim-16-1] backward subsumption/strengthening limit 34570900
c [elim-16-1-1] backward checking 4130 touched variables 8%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 4 and strengthened 43 clauses in 1212295 steps
c [elim-16-1] rescheduled 157 variables 0% by backward subsumption
c [elim-16-2] eliminated 13 variables 0% in round 2 in 94982 steps
c [elim-16-2] backward subsumption/strengthening limit 94900
c [elim-16-2-1] backward checking 151 touched variables 0%
c [elim-16-2-1] incomplete backward checking 0 remain 0%
c [elim-16-2] subsumed 0 and strengthened 13 clauses in 94901 steps
c [elim-16-2] rescheduled 51 variables 0% by backward subsumption
c [elim-16-3] eliminated 4 variables 0% in round 3 in 32180 steps
c [elim-16-3] backward subsumption/strengthening limit 32100
c [elim-16-3-1] backward checking 49 touched variables 0%
c [elim-16-3-1] incomplete backward checking 0 remain 0%
c [elim-16-3] subsumed 0 and strengthened 8 clauses in 32101 steps
c [elim-16] incomplete 31 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 826 = 2% variables out of 51737 scheduled
c [bca-14] limit of 10000000 steps and 748532 added (scaled 2)
c [bca-14] 73968 out of 101824 literals actually usable 73%
c [bca-14] added 46 blocked clauses in 184367 steps
c [score-distribution-18] 27095 pos 53.22%, 11474 min 22.54%, 12342 zero 24.24%
c [score-distribution-18] 5173 different 10.16% out of total 50911 variables
c [simplification-18] removed 2680 variables 5.0% (50911 remain 21%)
c [simplification-18] removed 26798 irredundant clauses 6.7% (373662 remain 27%)
c [simplification-18] maximum reduction of 7% = max (5%, 7%)
c [simplification-18] large reduction 7% >= 5% limit
c [simplification-18] next conflict interval 2000 = 2000/1
c [simplification-18] penalized conflict interval 2000 = 1 * 2000
c [simplification-18] hard conflict limit 137393 (soft 127393 + delta 10000)
c [simplification-18] new conflict limit 127393 (hard 137393)
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  251.1   50910   373662    125811   21277   5135 805082   65   269   59  24%      5   52   49   41  120%
c i  252.4   50908   373662    126958   22336   5152 805097   64   270   59  24%      4   52   57   41  138%
c 
c [simplification-19] limit 127393 conflicts (hard 137393) hit after 127399 conflicts
c [quatres-14] found 27956 quaternary clauses 55% in total
c [quatres-14-1] removed 6 duplicate quaternary clauses
c [quatres-14-2] added 5 quaternary resolvents
c [ternres-15] limit 43036577 with penalty 0 = 0 + 0
c [ternres-15] all 50892 free variables schedulable
c [ternres-15] 225 ternary resolvents (0 bin, 225 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-41] removed 147 variables
c [simpleprobe-7] all 50764 free variables schedulable
c [simpleprobe-7] limit 172146309 penalty 0 = 0 + 0
c [decomp-42] removed 228 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 228 variables, found 99446 hbrs, 143 units
c [unhide-19] limit 8607315 with penalty 0 = 0 + 0
c [unhide-19-27] 6 units, 75 failed, 68680 tauts, 0 hbrs, 58553 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 150 transitive binary clauses
c [cce-6] limit of 26897860 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 95
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 94
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 93
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 92
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 91
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 90
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 89
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 88
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 87
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 86
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 85
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 84
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 83
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 82
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 81
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 80
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 79
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 78
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 77
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 76
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 75
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 74
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 73
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 72
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 71
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 70
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 69
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 68
c [cce-6-1] eliminated 6 clauses out of 6 (100%) of length 67
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 66
c [cce-6-1] eliminated 6 clauses out of 6 (100%) of length 65
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 64
c [cce-6-1] eliminated 6 clauses out of 6 (100%) of length 63
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 62
c [cce-6-1] eliminated 6 clauses out of 6 (100%) of length 61
c [cce-6-1] eliminated 3 clauses out of 7 (43%) of length 60
c [cce-6-1] eliminated 7 clauses out of 7 (100%) of length 59
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 58
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 57
c [cce-6-1] eliminated 5 clauses out of 7 (71%) of length 56
c [cce-6-1] eliminated 6 clauses out of 7 (86%) of length 55
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 54
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 53
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 52
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 51
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 50
c [cce-6-1] eliminated 6 clauses out of 8 (75%) of length 49
c [cce-6-1] eliminated 6 clauses out of 7 (86%) of length 48
c [cce-6-1] eliminated 6 clauses out of 9 (67%) of length 47
c [cce-6-1] eliminated 6 clauses out of 7 (86%) of length 46
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 45
c [cce-6-1] eliminated 7 clauses out of 9 (78%) of length 44
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 43
c [cce-6-1] eliminated 8 clauses out of 9 (89%) of length 42
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 41
c [cce-6-1] eliminated 8 clauses out of 10 (80%) of length 40
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 39
c [cce-6-1] eliminated 7 clauses out of 9 (78%) of length 38
c [cce-6-1] eliminated 7 clauses out of 10 (70%) of length 37
c [cce-6-1] eliminated 9 clauses out of 11 (82%) of length 36
c [cce-6-1] eliminated 6 clauses out of 10 (60%) of length 35
c [cce-6-1] eliminated 9 clauses out of 10 (90%) of length 34
c [cce-6-1] eliminated 6 clauses out of 10 (60%) of length 33
c [cce-6-1] eliminated 9 clauses out of 10 (90%) of length 32
c [cce-6-1] eliminated 6 clauses out of 10 (60%) of length 31
c [cce-6-1] eliminated 9 clauses out of 10 (90%) of length 30
c [cce-6-1] eliminated 6 clauses out of 10 (60%) of length 29
c [cce-6-1] eliminated 9 clauses out of 10 (90%) of length 28
c [cce-6-1] eliminated 6 clauses out of 10 (60%) of length 27
c [cce-6-1] eliminated 9 clauses out of 10 (90%) of length 26
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 25
c [cce-6-1] eliminated 9 clauses out of 9 (100%) of length 24
c [cce-6-1] eliminated 7 clauses out of 11 (64%) of length 23
c [cce-6-1] eliminated 8 clauses out of 9 (89%) of length 22
c [cce-6-1] eliminated 7 clauses out of 11 (64%) of length 21
c [cce-6-1] eliminated 10 clauses out of 12 (83%) of length 20
c [cce-6-1] eliminated 8 clauses out of 12 (67%) of length 19
c [cce-6-1] eliminated 11 clauses out of 12 (92%) of length 18
c [cce-6-1] eliminated 6 clauses out of 10 (60%) of length 17
c [cce-6-1] eliminated 10 clauses out of 11 (91%) of length 16
c [cce-6-1] eliminated 9 clauses out of 13 (69%) of length 15
c [cce-6-1] eliminated 10 clauses out of 13 (77%) of length 14
c [cce-6-1] eliminated 9 clauses out of 12 (75%) of length 13
c [cce-6-1] eliminated 12 clauses out of 15 (80%) of length 12
c [cce-6-1] eliminated 9 clauses out of 13 (69%) of length 11
c [cce-6-1] eliminated 11 clauses out of 23 (48%) of length 10
c [cce-6-1] eliminated 11 clauses out of 92 (12%) of length 9
c [cce-6-1] eliminated 13 clauses out of 74 (18%) of length 8
c [cce-6-1] eliminated 11 clauses out of 172 (6%) of length 7
c [cce-6-1] eliminated 24 clauses out of 2691 (1%) of length 6
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 508 large clauses in 26897863 steps
c [cce-6-1] allowing another 13448931 steps for small clauses
c [cce-6-1] scheduling 307672 clauses = 177289 binary + 130383 ternary
c [cce-6-1] tried to eliminate 422 small clauses 0%
c [cce-6-1] eliminated 44 binary clauses 0%
c [cce-6-1] eliminated 19 ternary clauses 0%
c [cce-6-1] eliminated 63 small clauses 0%
c [cce-6-1] eliminated 181 small clauses in 26897863 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 689 covered clauses in round 1
c [cce-6] eliminated 689 covered clauses in TOTAL during 1 rounds
c [cce-6] 689 < 1/100 * 368118 = 3681 considered unsuccessful
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 50492 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 179 variables 0% in round 1 in 31831225 steps
c [elim-17-1] backward subsumption/strengthening limit 31831200
c [elim-17-1-1] backward checking 1194 touched variables 2%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 29 and strengthened 14 clauses in 466382 steps
c [elim-17-1] rescheduled 96 variables 0% by backward subsumption
c [elim-17-2] eliminated 11 variables 0% in round 2 in 303253 steps
c [elim-17-2] backward subsumption/strengthening limit 303200
c [elim-17-2-1] backward checking 102 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 12 and strengthened 8 clauses in 261185 steps
c [elim-17-2] rescheduled 42 variables 0% by backward subsumption
c [elim-17-3] eliminated 9 variables 0% in round 3 in 332321 steps
c [elim-17-3] backward subsumption/strengthening limit 332300
c [elim-17-3-1] backward checking 84 touched variables 0%
c [elim-17-3-1] fully completed backward checking in 1 rounds
c [elim-17-3] subsumed 0 and strengthened 6 clauses in 124147 steps
c [elim-17] incomplete 23 not tried 0% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 199 = 0% variables out of 50492 scheduled
c [elim-17] 199 < 1/100 * 50492 = 504 considered unsuccessful
c [bca-15] limit of 10000000 steps and 733799 added (scaled 2)
c [bca-15] 72452 out of 100588 literals actually usable 72%
c [bca-15] added 32 blocked clauses in 182177 steps
c [score-distribution-19] 26670 pos 53.03%, 11616 min 23.10%, 12007 zero 23.87%
c [score-distribution-19] 5267 different 10.47% out of total 50293 variables
c [simplification-19] removed 599 variables 1.2% (50293 remain 20%)
c [simplification-19] removed 7378 irredundant clauses 2.0% (366284 remain 27%)
c [simplification-19] maximum reduction of 2% = max (1%, 2%)
c [simplification-19] geometric conflict interval increment 10763 = 32290 / 3
c [simplification-19] new conflict interval 43053
c [simplification-19] penalized conflict interval 43053 = 1 * 43053
c [simplification-19] hard conflict limit 191978 (soft 170452 + delta 21526)
c [simplification-19] new conflict limit 170452 (hard 191978)
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  262.6   50292   366284    129233   23714   5096 821103   57   252   62  23%     15   31   49   42  117%
c i  263.4   50291   366284    129955   24369   5106 821110   58   254   63  23%      7   34   68   42  163%
c i  266.5   50240   366284    133194   27349   5139 821139   50   205   67  24%     28  -15   48   42  115%
c i  267.1   50236   366284    133903   27989   5145 821147   53   204   68  26%     13  -17   69   42  164%
c i  267.7   50235   366284    134641   28694   5149 821152   51   196   71  26%      5  -25   39   42   92%
c i  270.6   50234   366284    137344   31161   5170 821170   64   241   74  26%     20   21   68   43  156%
c i  270.6   50233   366284    137345   31161   5170 821170   64   241   74  26%     20   21   68   43  156%
c i  271.7   50232   366284    138436   32146   5184 821183   65   240   74  27%      7   19   66   44  150%
c i  277.6   50231   366284    143443   36742   5233 821223   70   263   81  26%     52   41  100   46  218%
c i  280.6   50230   366284    146066   39103   5258 821249   69   259   85  27%     20   36   77   47  165%
c i  284.8   50229   366284    150048   42704   5299 821274   65   237   96  27%     35   12   68   48  143%
c i  293.1   50228   366284    158048   49870   5390 821368   63   235  103  27%     92    8   63   50  128%
c i  293.6   50225   366284    158395   50161   5393 821371   62   224  103  28%     61   -3   55   50  111%
c i  293.7   50224   366284    158568   50317   5395 821372   61   228  103  27%     49    1   45   50   91%
c i  294.6   50223   366284    159319   51010   5406 821378   62   233  103  27%     17    6   65   50  130%
c i  295.8   50222   366284    160462   52022   5416 821387   64   224  103  29%      0   -4   71   50  142%
c i  296.1   50019   366284    160769   52265   5416 821391   67   223  103  30%     -4   -4   88   50  174%
c i  299.6   49932   366284    163412   54652   5450 821416   78   267  103  29%     10   39   88   52  168%
c i  300.7   49921   366284    164287   55474   5453 821418   73   264  103  28%     -2   36   43   52   83%
c i  303.4   49920   366284    166417   57355   5472 821432   78   271  107  29%      3   42   74   53  140%
c i  305.3   49919   366284    168081   58820   5486 821450   77   272  111  28%     -1   41   92   54  171%
c 
c [simplification-20] limit 170462 conflicts (hard 191978) hit after 170463 conflicts
c [quatres-15] found 27901 quaternary clauses 53% in total
c [quatres-15-1] removed 1 duplicate quaternary clauses
c [quatres-15-2] added 2 single-self-subsuming ternary resolvents
c [quatres-15-2] added 5 quaternary resolvents
c [ternres-16] limit 55750852 with penalty 0 = 0 + 0
c [ternres-16] all 49919 free variables schedulable
c [ternres-16] 204 ternary resolvents (0 bin, 204 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-43] removed 385 variables
c [treelook-7] limit 5575085 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 73713 literals 74%
c [treelook-7] scheduling used 1826503 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 5575085 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 5638897 steps
c [treelook-7] 73589 literals remain 74%
c [treelook-7] 8291 variables remain to probed next time 17%
c [treelook-7] removed 14 variables, found 22641 hbrs
c [unhide-20] limit 2787542 with penalty 2 = 0 + 2
c [unhide-20-28] 0 units, 28 failed, 15347 tauts, 0 hbrs, 743876 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 179 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 49873 variables 100%
c [block-6] limit of 34844282 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 12 blocked clauses
c [block-6] 12 < 1/100 * 360256 = 3602 considered unsuccessful
c [bca-16] limit of 10000000 steps and 721351 added (scaled 2)
c [bca-16] 63202 out of 99748 literals actually usable 63%
c [bca-16] added 18 blocked clauses in 199676 steps
c [sweep-10] limit 2090656 penalty 3 = 3 + 0
c [sweep-10-1] 4718 pos 10.3% + 40994 neg 89.7% = 45712 sched 91.7% ret 4161
c [sweep-10-1] 2235127 steps 20 queries 5154.20 avg class size
c [sweep-10-1] 843 decisions 18 SAT calls 439.33 avg env size
c [sweep-10-1] 45502 variables remain 91% (4367 retained 9%)
c [decomp-45] removed 11 variables
c [sweep-10-1] removed 11 vars (0 failed, 1 eqs, 2 impls)
c [sweep-10] 11 < 1/1000 * 49873 = 49 considered unsuccessful
c [sweep-10] removed 11 vars in TOTAL (1 rounds, 19 queries)
c [score-distribution-20] 25878 pos 51.90%, 12761 min 25.59%, 11223 zero 22.51%
c [score-distribution-20] 5720 different 11.47% out of total 49862 variables
c [simplification-20] removed 57 variables 0.1% (49862 remain 20%)
c [simplification-20] removed 6281 irredundant clauses 1.7% (360003 remain 26%)
c [simplification-20] maximum reduction of 2% = max (0%, 2%)
c [simplification-20] geometric conflict interval increment 14351 = 43053 / 3
c [simplification-20] new conflict interval 57404
c [simplification-20] penalized conflict interval 57404 = 1 * 57404
c [simplification-20] hard conflict limit 256569 (soft 227867 + delta 28702)
c [simplification-20] new conflict limit 227867 (hard 256569)
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.5   49861   360003    171213   61337   5664 817604   74   267  132  28%     17   34   85   54  156%
c i  317.4   49809   360003    172554   62547   5676 817612   77   274  132  28%      1   41   70   55  128%
c -  317.9   49809   360003    172813   25524   5676 817612   80   280   57  28%     -3   47  103   55  187%
c i  324.7   49808   360003    178991   31063   5736 817638   74   250   69  30%     65   12   35   57   61%
c i  332.7   49807   360003    186574   37710   5796 817690   76   260   82  29%     78   23   85   59  144%
c i  334.4   49627   360003    188431   39310   5819 817718   70   236   82  30%      7   -3   54   59   92%
c i  335.4   49626   360003    189653   40396   5847 817726   68   225   84  30%     -7  -13   71   59  120%
c i  335.4   49625   360003    189695   40427   5851 817731   67   224   84  30%     -8  -14   64   59  108%
c i  337.7   49614   360003    192913   43326   5906 817750   53   178   89  30%     11  -58   43   58   73%
c i  339.1   49610   360003    194096   44360   5913 817759   57   179   94  32%     -6  -56   86   58  147%
c i  346.7   49609   360003    200532   50135   5951 817795   74   249  107  30%     58   16   86   60  143%
c i  349.8   49607   360003    203227   52515   5972 817803   75   245  116  30%      7   11   74   61  122%
c i  351.6   49587   360003    204661   53783   5983 817809   79   255  116  31%     -8   21   89   61  146%
c i  358.4   49586   360003    210231   58695   6018 817845   80   253  123  32%     44   18   89   63  142%
c i  359.3   49585   360003    211006   59372   6021 817852   82   256  123  32%      9   20   88   63  139%
c i  361.1   49584   360003    212558   60748   6028 817865   82   258  123  32%     -8   22   92   63  145%
c i  363.7   49583   360003    214480   62449   6038 817874   87   268  123  32%     -8   31   99   64  154%
c i  365.0   49582   360003    215431   63276   6043 817882   86   269  123  32%    -14   32   76   65  117%
c i  366.4   49581   360003    216594   64262   6051 817887   85   256  130  33%    -15   18   92   65  142%
c i  367.7   49548   360003    217495   65061   6061 817895   89   271  138  33%    -17   33  104   65  159%
c -  369.2   49548   360003    218555   30045   6068 817904   82   257   59  32%    -16   18   51   65   78%
c i  373.0   49547   360003    222067   33171   6080 817913   73   210   72  35%     29  -28   70   65  107%
c i  374.7   49546   360003    223879   34858   6089 817919   61   183   78  33%     -2  -54   57   65   88%
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  377.2   49545   360003    226093   36814   6101 817927   71   223   78  32%     -3  -13   65   65  100%
c i  380.1   49544   360003    229137   39502   6112 817943   66   199   86  33%      8  -36   45   65   69%
c i  380.9   49534   360003    230298   40492   6119 817955   56   163   91  34%     -8  -71   20   65   31%
c i  381.7   49533   360003    231033   41138   6122 817956   59   169   91  35%    -14  -64   59   65   91%
c i  383.5   49524   360003    232661   42571   6139 817966   60   171   93  35%    -10  -61   28   65   43%
c i  384.1   49523   360003    233139   42986   6141 817971   64   183   93  35%    -14  -48   69   65  107%
c i  392.8   49522   360003    240447   49363   6178 818012   75   212   99  36%     71  -16   79   66  120%
c i  395.2   49521   360003    242560   51201   6186 818018   79   227  108  35%      3   -1   93   67  139%
c i  396.9   49520   360003    244068   52532   6198 818024   77   239  115  32%     -9   11   79   67  118%
c i  398.3   49519   360003    245348   53646   6204 818030   72   214  115  33%    -14  -14   58   66   88%
c i  400.8   49518   360003    247392   55434   6222 818040   81   238  120  34%     -7   10   64   67   95%
c i  401.1   49517   360003    247634   55629   6222 818040   79   231  120  34%    -11    4   59   67   87%
c i  401.7   49513   360003    248106   56035   6223 818042   80   233  120  34%    -15    5   80   68  118%
c i  402.4   49512   360003    248670   56530   6224 818047   81   238  120  34%    -18   10   98   68  144%
c 
c [simplification-21] limit 227867 conflicts (hard 256569) hit after 251689 conflicts
c [quatres-16] found 27435 quaternary clauses 53% in total
c [quatres-16-1] removed 1 duplicate quaternary clauses
c [quatres-16-2] added 6 single-self-subsuming ternary resolvents
c [ternres-17] limit 80022135 with penalty 0 = 0 + 0
c [ternres-17] all 49512 free variables schedulable
c [ternres-17] 53 ternary resolvents (0 bin, 53 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 2500691 penalty 4 = 4 + 0
c [card-6] found 2030 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 2500691 for elimination
c [card-6] 2030 out of 2030 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-46] removed 431 variables
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 5872 sched 12%, 923 failed, 27 lifted, 388670 hbrs
c [decomp-47] removed 1655 variables
c [basicprobe-7-1] 6673 probes remain 14% after last round
c [basicprobe-7-1] 1327 units = 1287 failed (97%) + 40 lifted (3%)
c [basicprobe-7-1] removed 2251 variables, found 564366 hbrs
c [bate-5] eliminated 885 asymmetric tautologies during probing
c [unhide-21] limit 4001106 with penalty 2 = 0 + 2
c [unhide-21-30] 2 units, 51 failed, 117427 tauts, 0 hbrs, 1399840 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 134 transitive binary clauses
c [elim-18] no untried remaining variables left
c [elim-18] scheduled 47153 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 8000000000 steps penalty 1 = 1 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 701 variables 1% in round 1 in 26801496 steps
c [elim-18-1] backward subsumption/strengthening limit 26801400
c [elim-18-1-1] backward checking 3699 touched variables 8%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 15 and strengthened 39 clauses in 1020161 steps
c [elim-18-1] rescheduled 164 variables 0% by backward subsumption
c [elim-18-2] eliminated 18 variables 0% in round 2 in 81031 steps
c [elim-18-2] backward subsumption/strengthening limit 81000
c [elim-18-2-1] backward checking 188 touched variables 0%
c [elim-18-2-1] incomplete backward checking 20 remain 11%
c [elim-18-2] subsumed 2 and strengthened 29 clauses in 81035 steps
c [elim-18-2] rescheduled 96 variables 0% by backward subsumption
c [elim-18-3] eliminated 7 variables 0% in round 3 in 78677 steps
c [elim-18-3] backward subsumption/strengthening limit 78600
c [elim-18-3-1] backward checking 103 touched variables 0%
c [elim-18-3-1] incomplete backward checking 0 remain 0%
c [elim-18-3] subsumed 3 and strengthened 12 clauses in 78601 steps
c [elim-18] incomplete 55 not tried 0% in round 3
c [elim-18] transition to [ all 1 rem 1 ] state
c [elim-18] eliminated 726 = 2% variables out of 47153 scheduled
c [bca-17] limit of 10000000 steps and 652162 added (scaled 2)
c [bca-17] 60073 out of 92856 literals actually usable 65%
c [bca-17] added 15 blocked clauses in 176807 steps
c [score-distribution-21] 22643 pos 48.77%, 14511 min 31.26%, 9273 zero 19.97%
c [score-distribution-21] 5429 different 11.69% out of total 46427 variables
c [simplification-21] removed 3085 variables 6.2% (46427 remain 19%)
c [simplification-21] removed 34550 irredundant clauses 9.6% (325453 remain 24%)
c [simplification-21] maximum reduction of 10% = max (6%, 10%)
c [simplification-21] large reduction 10% >= 5% limit
c [simplification-21] next conflict interval 2516 = min (251689/100, 57404)
c [simplification-21] penalized conflict interval 2516 = 1 * 2516
c [simplification-21] hard conflict limit 264205 (soft 254205 + delta 10000)
c [simplification-21] new conflict limit 254205 (hard 264205)
c 
c [simplification-22] limit 254205 conflicts (hard 264205) hit after 254209 conflicts
c [quatres-17] found 27203 quaternary clauses 54% in total
c [quatres-17-1] removed 3 duplicate quaternary clauses
c [quatres-17-2] added 2 quaternary resolvents
c [ternres-18] limit 80719173 with penalty 0 = 0 + 0
c [ternres-18] all 46427 free variables schedulable
c [ternres-18] 533 ternary resolvents (0 bin, 533 trn)
c [ternres-18] fully completed ternary resolution
c [gauss-7] limit 1008989 penalty 4 = 4 + 0
c [gauss-7] extracted 15 xors of average arity 2.9
c [gauss-7] connected 44 occurrences of 41 variables (average 1.1)
c [gauss-7] limit 1008989 penalty 4 = 4 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-48] removed 11 variables
c [simpleprobe-8] all 46416 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-49] removed 70 variables
c [simpleprobe-8] 1688 variables remain 4% (44658 retained 96%)
c [simpleprobe-8] removed 70 variables, found 102706 hbrs, 39 units
c [unhide-22] limit 4035958 with penalty 2 = 0 + 2
c [unhide-22-31] 2 units, 9 failed, 70276 tauts, 0 hbrs, 181741 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 153 transitive binary clauses
c [elim-19] no untried remaining variables left
c [elim-19] scheduled 46319 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 75 variables 0% in round 1 in 26590411 steps
c [elim-19-1] backward subsumption/strengthening limit 26590400
c [elim-19-1-1] backward checking 507 touched variables 1%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 3 and strengthened 7 clauses in 208745 steps
c [elim-19-1] rescheduled 36 variables 0% by backward subsumption
c [elim-19-2] eliminated 2 variables 0% in round 2 in 82002 steps
c [elim-19-2] backward subsumption/strengthening limit 82000
c [elim-19-2-1] backward checking 23 touched variables 0%
c [elim-19-2-1] fully completed backward checking in 1 rounds
c [elim-19-2] subsumed 1 and strengthened 2 clauses in 67744 steps
c [elim-19-2] rescheduled 11 variables 0% by backward subsumption
c [elim-19-3] eliminated 1 variables 0% in round 3 in 13073 steps
c [elim-19-3] backward subsumption/strengthening limit 13000
c [elim-19-3-1] backward checking 10 touched variables 0%
c [elim-19-3-1] incomplete backward checking 0 remain 0%
c [elim-19-3] subsumed 0 and strengthened 2 clauses in 13001 steps
c [elim-19] incomplete 8 not tried 0% in round 3
c [elim-19] transition to [ all 1 rem 1 ] state
c [elim-19] eliminated 78 = 0% variables out of 46319 scheduled
c [elim-19] 78 < 1/100 * 46319 = 463 considered unsuccessful
c [bca-18] limit of 10000000 steps and 650048 added (scaled 2)
c [bca-18] 60341 out of 92484 literals actually usable 65%
c [bca-18] added 10 blocked clauses in 172811 steps
c [score-distribution-22] 23374 pos 50.55%, 13663 min 29.55%, 9204 zero 19.90%
c [score-distribution-22] 6005 different 12.99% out of total 46241 variables
c [simplification-22] removed 186 variables 0.4% (46241 remain 19%)
c [simplification-22] removed 1061 irredundant clauses 0.3% (324392 remain 24%)
c [simplification-22] maximum reduction of 0% = max (0%, 0%)
c [simplification-22] full geometric conflict interval increment 57404
c [simplification-22] new conflict interval 114808
c [simplification-22] penalized conflict interval 114808 = 1 * 114808
c [simplification-22] hard conflict limit 426421 (soft 369017 + delta 57404)
c [simplification-22] new conflict limit 369017 (hard 426421)
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  444.4   46240   324392    255119   43732   6359 1172302   72   214   90  33%     57  -14   56   68   82%
c i  444.8   46227   324392    255543   44108   6362 1172302   72   220   90  33%     29   -9   66   68   97%
c i  462.9   46224   324392    273648   60103   6436 1172363   70   197  109  36%    213  -24   87   68  128%
c -  470.8   46087   324392    281062   31836   6474 1172387   69   219   63  32%     43    1   80   68  118%
c i  481.3   46086   324392    292157   41423   6525 1172427   72   198   90  36%    196  -18  114   68  168%
c i  484.7   46085   324392    295595   44343   6537 1172436   70   195   96  36%    -31  -20   38   68   55%
c i  507.4   46084   324392    317802   63816   6648 1172507   58   133  139  44%    226  -69   88   66  133%
c i  508.4   46079   324392    318933   64824   6652 1172513   53   123  139  43%     10  -77   45   66   69%
c -  514.1   46079   324392    323910   35258   6681 1172532   57   140   65  41%    -39  -56   55   65   83%
c i  530.5   46078   324392    339722   48989   6751 1172572   69   158  101  44%    188  -35   90   67  135%
c i  551.9   46077   324392    357640   64565   6825 1172620   70   171  133  41%    137  -21   69   68  101%
c -  562.3   46077   324392    365534   35781   6852 1172636   77   191   65  40%    -15   -3   51   70   72%
c i  564.6   46076   324392    367882   37767   6856 1172642   73   170   76  43%     22  -23   77   70  109%
c i  566.0   46075   324392    369173   38843   6865 1172646   77   184   78  42%    -72   -9   95   71  134%
c i  566.5   46074   324392    369574   39188   6868 1172647   78   188   78  42%    -86   -5   89   71  125%
c i  568.8   46073   324392    371531   40902   6877 1172651   75   186   79  40%    -96   -7   45   71   63%
c 
c [simplification-23] limit 369017 conflicts (hard 426421) hit after 384316 conflicts
c [quatres-18] found 27141 quaternary clauses 52% in total
c [quatres-18-2] added 8 single-self-subsuming ternary resolvents
c [quatres-18-2] added 1 quaternary resolvents
c [ternres-19] limit 117119753 with penalty 0 = 0 + 0
c [ternres-19] all 46073 free variables schedulable
c [ternres-19] 65 ternary resolvents (0 bin, 65 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-50] removed 170 variables
c [treelook-8] limit 11711975 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 65627 literals 71%
c [treelook-8] scheduling used 1829083 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 11711975 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 11721518 steps
c [treelook-8] 65008 literals remain 71%
c [treelook-8] 6749 variables remain to probed next time 15%
c [treelook-8] removed 233 variables, found 28825 hbrs
c [unhide-23] limit 5000000 with penalty 2 = 0 + 2
c [unhide-23-33] 0 units, 9 failed, 45856 tauts, 0 hbrs, 951396 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 104 transitive binary clauses
c [cce-7] limit of 36599923 steps penalty 4 = 4 + 0
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 61
c [cce-7-1] eliminated 1 clauses out of 5 (20%) of length 60
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 41
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 40
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 39
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 38
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 37
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 36
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 35
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 34
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 33
c [cce-7-1] eliminated 1 clauses out of 5 (20%) of length 32
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 31
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 30
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 29
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 28
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 27
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 26
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 25
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 24
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 23
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 22
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 21
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 20
c [cce-7-1] eliminated 4 clauses out of 9 (44%) of length 19
c [cce-7-1] eliminated 2 clauses out of 7 (29%) of length 18
c [cce-7-1] eliminated 5 clauses out of 9 (56%) of length 17
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 16
c [cce-7-1] eliminated 4 clauses out of 10 (40%) of length 15
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 14
c [cce-7-1] eliminated 5 clauses out of 9 (56%) of length 13
c [cce-7-1] eliminated 4 clauses out of 8 (50%) of length 12
c [cce-7-1] eliminated 5 clauses out of 10 (50%) of length 11
c [cce-7-1] eliminated 4 clauses out of 19 (21%) of length 10
c [cce-7-1] eliminated 7 clauses out of 42 (17%) of length 9
c [cce-7-1] eliminated 7 clauses out of 30 (23%) of length 8
c [cce-7-1] eliminated 11 clauses out of 82 (13%) of length 7
c [cce-7-1] eliminated 41 clauses out of 2734 (1%) of length 6
c [cce-7-1] eliminated 1569 clauses out of 9715 (16%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 1718 large clauses in 36599923 steps
c [cce-7-1] allowing another 18299961 steps for small clauses
c [cce-7-1] scheduling 183837 clauses = 167452 binary + 16385 ternary
c [cce-7-1] tried to eliminate 1296 small clauses 1%
c [cce-7-1] eliminated 287 binary clauses 0%
c [cce-7-1] eliminated 60 ternary clauses 0%
c [cce-7-1] eliminated 347 small clauses 0%
c [cce-7-1] eliminated 691 small clauses in 36599933 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 2409 covered clauses in round 1
c [cce-7] eliminated 2409 covered clauses in TOTAL during 1 rounds
c [cce-7] 2409 < 1/100 * 315566 = 3155 considered unsuccessful
c [bca-19] limit of 10000000 steps and 627583 added (scaled 2)
c [bca-19] 59056 out of 91544 literals actually usable 65%
c [bca-19] added 17 blocked clauses in 178045 steps
c [score-distribution-23] 23038 pos 50.33%, 14019 min 30.63%, 8714 zero 19.04%
c [score-distribution-23] 5627 different 12.29% out of total 45771 variables
c [simplification-23] removed 302 variables 0.7% (45771 remain 19%)
c [simplification-23] removed 11235 irredundant clauses 3.5% (313157 remain 23%)
c [simplification-23] maximum reduction of 3% = max (1%, 3%)
c [simplification-23] geometric conflict interval increment 28702 = 114808 / 4
c [simplification-23] new conflict interval 143510
c [simplification-23] penalized conflict interval 143510 = 1 * 143510
c [simplification-23] hard conflict limit 599581 (soft 527826 + delta 71755)
c [simplification-23] new conflict limit 527826 (hard 599581)
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  603.4   45770   313157    394324   60047   6914 1144550   75   184  116  41%    206   -4   87   72  122%
c i  611.8   45769   313157    401145   65843   6938 1144572   70   160  122  43%    -39  -27   86   71  121%
c -  620.8   45754   313157    408179   36451   6969 1144591   74   168   64  44%    -28  -20   55   72   76%
c i  621.4   45753   313157    408751   36933   6975 1144591   72   160   73  45%    -19  -27   59   72   82%
c i  635.1   45752   313157    421748   47931   7016 1144624   70   161  105  44%     69  -18   82   71  115%
c i  638.2   45750   313157    425185   50793   7023 1144642   62   144  110  43%    -70  -33   55   70   79%
c i  645.9   45749   313157    432026   56522   7053 1144673   73   180  118  41%    -17    3   72   71  102%
c i  653.1   45748   313157    438092   61481   7068 1144688   83   185  126  45%    -24    9  136   72  190%
c i  658.6   45747   313157    442806   65551   7107 1144701   72   170  129  42%    -40   -6   38   71   54%
c i  665.7   45746   313157    448474   70521   7128 1144718   75   190  157  39%    -21   14   71   72   99%
c -  670.5   45744   313157    452166   37986   7147 1144733   87   216   65  40%    -47   38  109   73  149%
c i  699.4   45743   313157    477702   59326   7223 1144803   76   165  113  46%    297  -16   63   74   84%
c i  703.9   45741   313157    481481   62514   7235 1144809   77   173  119  44%    -89   -8   77   75  103%
c -  724.2   45741   313157    497231   39690   7287 1144827   60   123   65  49%     93  -57   26   74   34%
c i  734.8   45740   313157    506846   47828   7322 1144840   70   144   87  48%    220  -30   71   73   97%
c i  737.5   45715   313157    509180   49794   7333 1144844   55   117   87  48%    -99  -56   22   72   31%
c i  763.2   45714   313157    530085   68198   7391 1144894   57   130  138  44%    151  -29   63   68   92%
c -  777.3   45714   313157    540687   41491   7417 1144911   81   163   65  50%     -1    7  133   69  192%
c 
c [simplification-24] limit 527826 conflicts (hard 599581) hit after 540764 conflicts
c [quatres-19] found 27572 quaternary clauses 52% in total
c [quatres-19-1] removed 1 duplicate quaternary clauses
c [quatres-19-2] added 2 single-self-subsuming ternary resolvents
c [quatres-19-2] added 1 quaternary resolvents
c [ternres-20] limit 162599329 with penalty 0 = 0 + 0
c [ternres-20] all 45714 free variables schedulable
c [ternres-20] 36 ternary resolvents (0 bin, 36 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-52] removed 63 variables
c [basicprobe-8] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 7142 sched 16%, 434 failed, 21 lifted, 170881 hbrs
c [decomp-53] removed 775 variables
c [basicprobe-8-1] 5216 probes remain 12% after last round
c [basicprobe-8-1] 592 units = 569 failed (96%) + 23 lifted (4%)
c [basicprobe-8-1] removed 1128 variables, found 244864 hbrs
c [bate-6] eliminated 484 asymmetric tautologies during probing
c [unhide-24] limit 10000000 with penalty 1 = 0 + 1
c [unhide-24-36] 1 units, 12 failed, 100826 tauts, 0 hbrs, 81461 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 93 transitive binary clauses
c [elim-20] no untried remaining variables left
c [elim-20] scheduled 44572 variables 100%
c [elim-20] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 1024 variables 2% in round 1 in 23844428 steps
c [elim-20-1] backward subsumption/strengthening limit 23844400
c [elim-20-1-1] backward checking 4689 touched variables 11%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 9 and strengthened 22 clauses in 1096692 steps
c [elim-20-1] rescheduled 76 variables 0% by backward subsumption
c [elim-20-2] eliminated 7 variables 0% in round 2 in 74213 steps
c [elim-20-2] backward subsumption/strengthening limit 74200
c [elim-20-2-1] backward checking 72 touched variables 0%
c [elim-20-2-1] incomplete backward checking 0 remain 0%
c [elim-20-2] subsumed 6 and strengthened 8 clauses in 74201 steps
c [elim-20-2] rescheduled 39 variables 0% by backward subsumption
c [elim-20-3] eliminated 2 variables 0% in round 3 in 65424 steps
c [elim-20-3] backward subsumption/strengthening limit 65400
c [elim-20-3-1] backward checking 24 touched variables 0%
c [elim-20-3-1] incomplete backward checking 0 remain 0%
c [elim-20-3] subsumed 0 and strengthened 4 clauses in 65401 steps
c [elim-20] incomplete 16 not tried 0% in round 3
c [elim-20] transition to [ all 1 rem 1 ] state
c [elim-20] eliminated 1033 = 2% variables out of 44572 scheduled
c [bca-20] limit of 10000000 steps and 591217 added (scaled 2)
c [bca-20] 58374 out of 87080 literals actually usable 67%
c [bca-20] added 17 blocked clauses in 155017 steps
c [score-distribution-24] 23458 pos 53.88%, 12646 min 29.05%, 7435 zero 17.08%
c [score-distribution-24] 6383 different 14.66% out of total 43539 variables
c [simplification-24] removed 2175 variables 4.8% (43539 remain 18%)
c [simplification-24] removed 18187 irredundant clauses 5.8% (294970 remain 21%)
c [simplification-24] maximum reduction of 6% = max (5%, 6%)
c [simplification-24] large reduction 6% >= 5% limit
c [simplification-24] next conflict interval 5407 = min (540764/100, 143510)
c [simplification-24] penalized conflict interval 5407 = 1 * 5407
c [simplification-24] hard conflict limit 556171 (soft 546171 + delta 10000)
c [simplification-24] new conflict limit 546171 (hard 556171)
c 
c [simplification-25] limit 546171 conflicts (hard 556171) hit after 556171 conflicts
c [quatres-20] found 27241 quaternary clauses 53% in total
c [quatres-20-1] removed 1 duplicate quaternary clauses
c [quatres-20-2] added 2 single-self-subsuming ternary resolvents
c [quatres-20-2] added 4 quaternary resolvents
c [ternres-21] limit 166288476 with penalty 0 = 0 + 0
c [ternres-21] all 43539 free variables schedulable
c [ternres-21] 619 ternary resolvents (0 bin, 619 trn)
c [ternres-21] fully completed ternary resolution
c [decomp-54] removed 1 variables
c [simpleprobe-9] 1519 schedulable variables 3%
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-55] removed 17 variables
c [simpleprobe-9] 1674 variables remain 4% (41847 retained 96%)
c [simpleprobe-9] removed 17 variables, found 50330 hbrs, 10 units
c [unhide-25] limit 5000000 with penalty 2 = 0 + 2
c [unhide-25-38] 0 units, 2 failed, 40944 tauts, 0 hbrs, 1221829 literals
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 86 transitive binary clauses
c [elim-21] no untried remaining variables left
c [elim-21] scheduled 43520 variables 100%
c [elim-21] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-21] rescheduling of touched variables disabled
c [elim-21-1] eliminated 67 variables 0% in round 1 in 24081660 steps
c [elim-21-1] backward subsumption/strengthening limit 24081600
c [elim-21-1-1] backward checking 552 touched variables 1%
c [elim-21-1-1] fully completed backward checking in 1 rounds
c [elim-21-1] subsumed 4 and strengthened 7 clauses in 217313 steps
c [elim-21-1] rescheduled 34 variables 0% by backward subsumption
c [elim-21-2] eliminated 2 variables 0% in round 2 in 25642 steps
c [elim-21-2] backward subsumption/strengthening limit 25600
c [elim-21-2-1] backward checking 26 touched variables 0%
c [elim-21-2-1] incomplete backward checking 5 remain 19%
c [elim-21-2] subsumed 0 and strengthened 4 clauses in 25617 steps
c [elim-21-2] rescheduled 16 variables 0% by backward subsumption
c [elim-21-3] eliminated 2 variables 0% in round 3 in 23127 steps
c [elim-21-3] backward subsumption/strengthening limit 23100
c [elim-21-3-1] backward checking 25 touched variables 0%
c [elim-21-3-1] incomplete backward checking 11 remain 44%
c [elim-21-3] subsumed 0 and strengthened 4 clauses in 23138 steps
c [elim-21] incomplete 16 not tried 0% in round 3
c [elim-21] transition to [ all 1 rem 1 ] state
c [elim-21] eliminated 71 = 0% variables out of 43520 scheduled
c [elim-21] 71 < 1/100 * 43520 = 435 considered unsuccessful
c [bca-21] limit of 10000000 steps and 587792 added (scaled 2)
c [bca-21] 56603 out of 86900 literals actually usable 65%
c [bca-21] added 9 blocked clauses in 161856 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 31179088 penalty 4 = 4 + 0
c [sweep-11-1] 4586 pos 11.3% + 35885 neg 88.7% = 40471 sched 93.1% ret 2978
c [sweep-11-1] 31232363 steps 607 queries 318.99 avg class size
c [sweep-11-1] 10659 decisions 588 SAT calls 192.80 avg env size
c [sweep-11-1] 25233 variables remain 58% (18213 retained 42%)
c [decomp-56] removed 41 variables
c [sweep-11-1] removed 41 vars (0 failed, 21 eqs, 48 impls)
c [sweep-11] 41 < 1/1000 * 43449 = 43 considered unsuccessful
c [sweep-11] removed 41 vars in TOTAL (1 rounds, 606 queries)
c [score-distribution-25] 24136 pos 55.60%, 11958 min 27.55%, 7314 zero 16.85%
c [score-distribution-25] 4422 different 10.19% out of total 43408 variables
c [simplification-25] removed 131 variables 0.3% (43408 remain 18%)
c [simplification-25] removed 1796 irredundant clauses 0.6% (293174 remain 21%)
c [simplification-25] maximum reduction of 1% = max (0%, 1%)
c [simplification-25] geometric conflict interval increment 71755 = 143510 / 2
c [simplification-25] new conflict interval 215265
c [simplification-25] penalized conflict interval 215265 = 1 * 215265
c [simplification-25] hard conflict limit 879068 (soft 771436 + delta 107632)
c [simplification-25] new conflict limit 771436 (hard 879068)
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  848.4   43407   293174    583304   63958   7679 1183581   58   137  123  43%    489  -11   48   63   75%
c i  862.2   43406   293174    595916   75208   7722 1183599   48   111  161  44%   -114  -31   40   60   67%
c -  866.5   43405   293174    599441   41366   7732 1183606   54   129   65  42%   -238  -12   72   60  119%
c i  912.8   43404   293174    640685   78366   7824 1183670   46    97  169  47%    348  -34   39   56   70%
c -  917.1   43404   293174    643745   44499   7832 1183684   59   129   66  46%   -264   -1  112   57  198%
c -  969.6   43404   293174    686714   45663   7948 1183754   43    83   66  52%    337  -46   18   56   32%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 3444 basic ate = 2240 trn 65% + 1204 lrg 35% in 6 updates
c bcas: 21 count, 1581 added (189 skipped), 6019739 steps
c bkwd: tried 502693 clauses, 1004735 lits, 2.00 lits/clause
c bkwd: checked 16200578 occs, 32.23 occs/clause, 16.12 occs/lit
c bkwd: subsumed 17 binary, 193 ternary, 98 large
c bkwd: strengthened 14 binary, 1 ternary (100% self), 1352 large (0% self)
c blkd: 6 bces, 12063 removed, 10871823 resolutions, 30415780 steps
c blkd: 12702 blocking literals 2%, 2 pure
c bump: 709380 bumped seen, 469157686 lits 661.4 on average
c card: 6 count, 0 units, 0 am1, 469119736 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 74841 subsumed
c card: 17101 at-most-one constraints found, average size 4.83
c card: 17101 at-most-one constraints used 100%, average size 4.83
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: 7 cces, 19174 eliminated, 19113 ate 100%, 61 abce 0%
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: 4739857 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 186 gcs, 0 rescored clauses, 373 rescored vars
c dcps: 56 decompositions, 9862 equivalent 4%
c deco: 71908 decision-only clauses 10%, 74% reduction
c decs: 9357715 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 40200747 push, 39947049 pop (39947049 dec 100%)
c dsch: 1069255766 swaps, 0 down, 436826175 up
c elms: 21 elims, 102322 eliminated 39%, 41 pure 0%
c elms: 67 rounds, 3.2 rounds/bve
c elms: 83464 small 82%, 18815 large 18%
c elms: 260639 tried small, 83465 succeeded 32%, 177174 failed 68%
c elms: 50733 subsumed, 67510 strengthened, 850 blocked
c elms: 30889599 copies, 30082988 resolutions, 7401657 ipos
c elms: 8673249 subchks, 4961318 strchks
c gaus: 7 extractions, 367 extracted, 2.6 size, 3 max
c gaus: exported 1 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 17947928 steps, 8973964 extr 50%, 5171 elim 0%
c glue: 61.2 orig avg, 61.2 real avg, 5.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 2610885 = 466604 simple 18% + 2121946 trn 81% + 22335 lrg 1%, 6125 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 709380 clauses, 329.9 length
c lrnd: 234043521 lits = 330276009 orig - 96232488 removed 29%
c lrnd: 328297 uips 46%, 313685 flips 44%
c mins: 611279 mins 88%, 4739 bin 1%, 9676 size 1%
c mins: 507875707 poisoned searches, 110712284 hits, 22% hit rate
c mins: 585092548 used twice searches, 18407862 hits, 3% hit rate
c move: moved 22148, 12973 bin 59%, 9175 trn 41%
c otfs: 1944 driving 22%, 6883 restarting 78%
c otfs: str 8827, 8735 red 99%, 92 irr 1%
c otfs: str 8827, 0 bin 0%, 164 trn 2%, 8663 lrg 98%
c otfs: sub 29, 27 red 93%, 2 irr 7%
c otfs: sub 29, 0 bin 0%, 3 trn 10%, 26 lrg 90%
c phas: 16 computed, 186201 set, 37 pos (0%), 186164 neg (100%)
c prbs: 8 basic, 80913 probed, 4294 failed, 110 lifted
c prbs: 9 simple, 1015054 probed, 1026 failed, 917 eqs
c prbs: 8 treelook, 392 probed, 43 failed, 0 lifted
c prom: 183781 locked 7% out of 2603827 tried
c prps: 2491212139 props, 255 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c quat: 20 count, 73 quat, 45 self1, 0 self2, 875 dup
c redc: 10470 clauses 27%, 38455 tried 5%, 235 sat 1%
c redc: 25772 lits 6%, 434928 tried 0%, 235 sat 0%
c redc: 1347 times jump level reduced, 27.0 levels on average
c reds: 13 count, 54687.0 conflicts per reduce
c reds: 0 memlim 0%, 13 arith 100%
c reds: 364088 collected 77%, 106493 retired 23%
c rmbd: 56217 removed, 6733 red 12%
c rsts: 18015 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 25 count, 23 confs 92%, 0 vars 0%
c simp: 1 its 4%, 1 bin 4%, 0 trns 0%
c subl: 709380 count (957797 tried 1.4), 71986 sub out of 695244 (10.4%)
c swps: 11 count, 11 rounds, 1049 queries (95.4/round)
c swps: 977 sat calls, 33 unsat (0.4% success rate)
c swps: 15908 decisions 16.3, 393 conflicts 0.4
c swps; 4122.4 avg class size, 166.7 avg environment size
c swps: 0 failed, 177 impls, 87 equivs
c swp0: 348 type 0 queries, 96 unsat (27.6%), 340 sat (97.7%)
c swp1: 701 type 1 queries, 367 unsat (52.4%), 622 sat (88.7%)
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: 20136035 calls to obtain time
c tops: 103646 fixed 40%, 630 its, 1128.46 confs/it
c trds: 21 transitive reductions, 3348 removed, 39 failed
c trds: 18251 nodes, 51635 edges, 40931692 steps
c trim: 2864348 words, 10.9 MB
c trnr: 21 count, 4 bin, 4150 trn, 272515779 steps
c unhd: 25 count, 38 rounds, 139305400 steps
c unhd: 2400 non-trivial sccs of average size 2.3
c unhd: 227 units, 227 bin, 0 trn, 0 lrg
c unhd: 9576 failed, 9516 stamp, 0 lits, 22 bin, 21 trn, 0 lrg
c unhd: 980287 tauts, 37582 bin 4%, 14807 trn 2%, 1174 lrg 0%
c unhd: 980287 tauts, 926724 stamp 95%, 880350 red 90%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 5518205 str, 227 bin 0%, 3654 trn 0%, 5514324 lrg 100%, 5499504 red 100%
c vars: 43404 remaining 17% and 215830 removed 83% out of 259234
c vars: 103646 fixed 40%, 102322 eliminated 39%, 9862 equivalent 4%
c vsts: 21886111575 visits, 96% srch, 4% simp, 0% lkhd
c vsts: 8.8 search visits per propagation, 29426.3 per conflict
c wchs: 2448924953 pushed, 77485670 enlarged, 267 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         695317        364088        106493      71214568       8057856        348243
c 
c  0 0         49565   7     15380   4         0   0  39222749  55   3214416  40     65551  19     2.1
c  1 5         20065   3      9414   3      2425   2   5730716   8    653122   8     24583   7     1.2
c  2 6         55073   8     29959   8      6948   7   7624046  11<   943703  12     42881  12     3.8
c  3 9         65643   9     36748  10      8751   8   5432954   8    719214   9<    35964  10     7.7
c  4 14        62231   9     36379  10      8772   8   3891775   5    599398   7     33717  10<    7.8
c  5 21        65593   9     39806  11      9672   9   3389958   5    575777   7     32571   9     8.9
c  6 30        65140   9<    40838  11<    10079   9   2031988   3    399561   5     27414   8    10.3
c  7 41        62352   9     40075  11     10234  10<  1541660   2    320035   4     24052   7    12.9
c  8 54        57552   8     37254  10      9954   9    979592   1    228789   3     17929   5    12.4
c  9 69        50053   7     32359   9      9169   9    629076   1    163740   2     15044   4    12.2
c 10 86        51852   7     28346   8      9687   9    472813   1    132564   2     14668   4     9.2
c 11 126       52910   8     12302   3     10349  10    204624   0     78033   1     10125   3     4.4
c 12 230       35047   5      4915   1      9772   9     59814   0     28079   0      3544   1     5.1
c 13 534        2241   0       313   0       681   1      2803   0      1425   0       200   0     0.7
c 
c avg                  6.0           5.8           7.1           1.6           2.5           4.1
c std                  3.5           3.0           3.2           2.3           2.9           3.3
c 
c   77.007   8% probe
c   47.124   5% bump
c   37.307   4% unhide
c   27.229   3% elim
c   14.975   1% decide
c   10.349   1% cce
c    8.345   1% sweep
c    4.832   0% bca
c 
c   12.606 < 1% rest (below)
c 
c    3.223   0% block
c    2.712   0% transred
c    2.530   0% gauss
c    1.862   0% ternres
c    1.255   0% quatres
c    0.611   0% rescore
c    0.414   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    5.063   1% preprocessing     3%
c  187.595  19% inprocessing     97%
c ==================================
c  192.658  19% simplifying
c  806.587  81% search
c ==================================
c  999.249 100% all
c 
c        710931 conflicts,         711.5 confs/sec
c          6979 ternaries,         101.9 confs/ternary
c          6382 binaries,          111.4 confs/binary
c           630 iterations,       1128.5 confs/iteration
c 
c            13 reductions,          0.0 redus/sec,  54687.0 confs/reduction
c         18015 restarts,           18.0 rests/sec,     39.5 confs/restart
c       9357715 decisions,        9364.7 decis/sec,     13.2 decis/conflict
c    2491212139 propagations,  2493084.6 props/sec,    266.2 props/decision
c 
c 999.2 seconds, 181.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
