c launch: /data/cnf/sc2014/app/atco_enc3_opt1_03_53.cnf.bz2
c host: atom23
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/atco_enc3_opt1_03_53.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc3_opt1_03_53.cnf.bz2
c no embedded options
c found 'p cnf 1296235 5156702' header
c read 1296235 variables, 5156702 clauses, 12869708 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 1254502 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 1254502  4931292         0       0      0     0    0     0  256   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1232823 based on 4931292 irredundant clauses
c [card-1] found 980 at-most-one constraints of average size 3.8
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1232823 for elimination
c [card-1] 980 out of 980 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 324478 variables
c [simpleprobe-1] all 971757 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 7806618 based on 3903309 irredundant clauses
c [decomp-2] removed 89 variables
c [simpleprobe-1] 787600 variables remain 81% (184068 retained 19%)
c [simpleprobe-1] removed 89 variables, found 275 hbrs, 7 units
c [unhide-1] limit 243938 based on 3903010 irredundant clauses
c [unhide-1-1] 5 units, 210 failed, 3875 tauts, 0 hbrs, 593 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 970387 variables 100%
c [elim-1] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 943340 not tried 97% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 25941 = 3% variables out of 970387 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 3822000 negative 99.9% of 3826922 except 4922 0.1%
c [phase-count-1] 3801621 positive 99.3% of 3826922 except 25301 0.7%
c [phase-count-1] less non-negative clauses 4922 than limit 382600 (10.0%)
c [phase-count-1] non-pos/non-neg = 25301/4922 = 5.14 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 944446 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 944446 zero 100.00%
c [score-distribution-1] 1 different 0.00% out of total 944446 variables
c [simplification-1] removed 69241 variables 6.8% (944446 remain 75%)
c [simplification-1] removed 1104370 irredundant clauses 22.4% (3826922 remain 78%)
c [simplification-1] maximum reduction of 22% = max (7%, 22%)
c [simplification-1] large reduction 22% >= 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   10.2  944445  3826922       110      41     52   169    0     3  269   2%      0    3    1    0 21133%
c i   10.2  944386  3826922       111      41     52   169    0     3  269   2%      0    3    1    0 21051%
c i   10.2  944377  3826922       115      41     52   172    0     3  269   2%      0    3    1    0 20780%
c i   10.2  944313  3826922       116      41     52   172    0     3  269   2%      0    3    1    0 20699%
c i   10.4  944304  3826922       124      42     52   178    0     3  269   2%      0    3    1    0 20297%
c i   10.5  944178  3826922       131      43     52   183    0     3  269   2%      0    3    1    0 19872%
c i   10.6  943996  3826922       136      43     52   187    0     3  269   2%      0    3    1    0 19572%
c i   10.6  943893  3826922       140      43     54   188    0     3  269   2%      0    3    1    0 19335%
c i   10.7  943864  3826922       144      43     54   191    0     3  269   2%      0    3    1    0 19103%
c i   10.7  943821  3826922       145      43     54   191    0     3  269   2%      0    3    1    0 19029%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 781 variables
c [simpleprobe-2] 764783 schedulable variables 81%
c [simpleprobe-2] limit 7646010 based on 3823005 irredundant clauses
c [decomp-4] removed 116 variables
c [simpleprobe-2] 745597 variables remain 79% (197952 retained 21%)
c [simpleprobe-2] removed 116 variables, found 280 hbrs, 2 units
c [treelook-1] limit 955634 based on 3822537 irredundant clauses
c [treelook-1] scheduled 168291 literals 9%
c [treelook-1] scheduling used 1177258 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 955634 based on 3822537 irredundant clauses
c [treelook-1] used 1108986 steps
c [treelook-1] 168069 literals remain 9%
c [treelook-1] 154552 variables remain to probed next time 16%
c [decomp-5] removed 53 variables
c [treelook-1] removed 266 variables, found 446 hbrs
c [basicprobe-1] limit 30570112 based on 3821264 irredundant clauses
c [basicprobe-1-0] 8806 probes remain 1% after last round
c [basicprobe-1-0] 37 units = 36 failed (97%) + 1 lifted (3%)
c [basicprobe-1-0] removed 1260 variables, found 21597 hbrs
c [unhide-2] limit 238829 based on 3821264 irredundant clauses
c [unhide-2-2] 2 units, 1176 failed, 8286 tauts, 0 hbrs, 2395 literals
c [elim-2] 935835 variables 100% will be scheduled this time
c [elim-2] scheduled 935835 variables 100%
c [elim-2] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 915137 not tried 98% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 20596 = 2% variables out of 935835 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 3779451 negative 99.9% of 3784387 except 4936 0.1%
c [phase-count-2] 3757827 positive 99.3% of 3784387 except 26560 0.7%
c [phase-count-2] less non-negative clauses 4936 than limit 378400 (10.0%)
c [phase-count-2] non-pos/non-neg = 26560/4936 = 5.38 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 458013 negative 100%
c [score-distribution-2] 2060 pos 0.22%, 0 min 0.00%, 914285 zero 99.78%
c [score-distribution-2] 332 different 0.04% out of total 916345 variables
c [simplification-2] removed 27468 variables 2.9% (916345 remain 73%)
c [simplification-2] removed 42535 irredundant clauses 1.1% (3784387 remain 77%)
c [simplification-2] maximum reduction of 3% = max (3%, 1%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1040 (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   22.9  916344  3784387       162      37     50  8739    0     3  267   2%      0    3    1    0 18543%
c 
c [simplification-3] limit of 136 binary hit after 136 binaries
c [card-2] limit 946096 based on 3784387 irredundant clauses
c [card-2] found 573 at-most-one constraints of average size 3.4
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 946096 for elimination
c [card-2] 573 out of 573 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 2825 variables
c [treelook-2] limit 943204 based on 3772819 irredundant clauses
c [treelook-2] scheduled 154658 literals 8%
c [treelook-2] scheduling used 1053231 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 943204 based on 3772819 irredundant clauses
c [treelook-2] used 1311808 steps
c [treelook-2] 154455 literals remain 8%
c [treelook-2] 21968 variables remain to probed next time 2%
c [decomp-7] removed 3 variables
c [treelook-2] removed 199 variables, found 537 hbrs
c [unhide-3] limit 235731 based on 3771702 irredundant clauses
c [unhide-3-3] 4 units, 194 failed, 16427 tauts, 0 hbrs, 3109 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 912635 variables 100%
c [elim-3] limit of 8102483 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 878831 not tried 96% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 32577 = 4% variables out of 912635 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 3734632 negative 99.9% of 3739651 except 5019 0.1%
c [phase-count-3] 3714378 positive 99.3% of 3739651 except 25273 0.7%
c [phase-count-3] less non-negative clauses 5019 than limit 373900 (10.0%)
c [phase-count-3] non-pos/non-neg = 25273/5019 = 5.04 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 249501 negative 100%
c [score-distribution-3] 4602 pos 0.52%, 0 min 0.00%, 875456 zero 99.48%
c [score-distribution-3] 925 different 0.11% out of total 880058 variables
c [simplification-3] removed 33714 variables 3.7% (880058 remain 70%)
c [simplification-3] removed 44736 irredundant clauses 1.2% (3739651 remain 76%)
c [simplification-3] maximum reduction of 4% = max (4%, 1%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 1040 (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   36.0  880057  3739651       715     345    122  8220    1    23  272   3%      2   23    4    0 10300%
c 
c [simplification-4] limit 1040 conflicts (hard 11000) hit after 1040 conflicts
c [decomp-8] removed 100 variables
c [basicprobe-2] limit 29915104 based on 3739388 irredundant clauses
c [basicprobe-2-0] 4906 probes remain 1% after last round
c [basicprobe-2-0] 715 units = 182 failed (25%) + 533 lifted (75%)
c [basicprobe-2-0] removed 1110 variables, found 15881 hbrs
c [unhide-4] limit 233711 based on 3739388 irredundant clauses
c [unhide-4-4] 3 units, 831 failed, 8263 tauts, 0 hbrs, 5399 literals
c [elim-4] 873737 variables 100% will be scheduled this time
c [elim-4] scheduled 873737 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 274374890 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 3707 not tried 0% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 316203 = 36% variables out of 873737 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 3604394 negative 99.8% of 3611252 except 6858 0.2%
c [phase-count-4] 3586654 positive 99.3% of 3611252 except 24598 0.7%
c [phase-count-4] less non-negative clauses 6858 than limit 361100 (10.0%)
c [phase-count-4] non-pos/non-neg = 24598/6858 = 3.59 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 107016 negative 100%
c [score-distribution-4] 4560 pos 0.82%, 0 min 0.00%, 554412 zero 99.18%
c [score-distribution-4] 1120 different 0.20% out of total 558972 variables
c [simplification-4] removed 321085 variables 36.5% (558972 remain 45%)
c [simplification-4] removed 128399 irredundant clauses 3.4% (3611252 remain 73%)
c [simplification-4] maximum reduction of 36% = max (36%, 3%)
c [simplification-4] large reduction 36% >= 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 13040 (soft 3040 + delta 10000)
c [simplification-4] new conflict limit 3040 (hard 13040)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   89.3  558971  3611252      2083    1163    247  7640    2    55  283   3%     10   54    5    0 3329%
c i   89.8  557778  3611252      2230    1261    288  7644    2    55  283   4%      9   54    5    0 2996%
c 
c [simplification-5] limit 3040 conflicts (hard 13040) hit after 3040 conflicts
c [quatres-1] found 647753 quaternary clauses 99% in total
c [quatres-1-2] added 95 single-self-subsuming ternary resolvents
c [quatres-1-2] added 108 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 14445000 based on 3611250 irredundant clauses
c [ternres-1] all 557751 free variables schedulable
c [ternres-1] 2349 ternary resolvents (0 bin, 2349 trn)
c [ternres-1] 542412 variables remain 97% (15339 retained 3%)
c [gauss-1] limit 1805625 based on 3611250 irredundant clauses
c [gauss-1] extracted 209 xors of average arity 2.7
c [gauss-1] connected 561 occurrences of 528 variables (average 1.1)
c [gauss-1] limit 1801488 based on 3602976 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-9] removed 687 variables
c [simpleprobe-3] 440219 schedulable variables 79%
c [simpleprobe-3] limit 7202806 based on 3601403 irredundant clauses
c [decomp-10] removed 4 variables
c [simpleprobe-3] 440363 variables remain 79% (116697 retained 21%)
c [simpleprobe-3] removed 4 variables, found 274 hbrs, 0 units
c [unhide-5] limit 225086 based on 3601386 irredundant clauses
c [unhide-5-5] 42 units, 818 failed, 25991 tauts, 0 hbrs, 46743 literals
c [transred-1] limit 3571547 based on 3571547 irredundant clauses
c [transred-1] removed 7 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 553810 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 166097960 steps penalty 2 = 0 + 2
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 4975 blocked clauses
c [block-1] 4975 < 1/100 * 3571540 = 35715 considered unsuccessful
c [cce-1] limit of 8304898 steps penalty 2 = 0 + 2
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 20
c [cce-1-1] eliminated 2 clauses out of 136 (1%) of length 14
c [cce-1-1] eliminated 55 clauses out of 257 (21%) of length 13
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 58 large clauses in 8304900 steps
c [cce-1-1] allowing another 4152450 steps for small clauses
c [cce-1-1] scheduling 2550080 clauses = 1155233 binary + 1394847 ternary
c [cce-1-1] tried to eliminate 35 small clauses 0%
c [cce-1-1] eliminated 7 binary clauses 0%
c [cce-1-1] eliminated 1 ternary clauses 0%
c [cce-1-1] eliminated 8 small clauses 0%
c [cce-1-1] eliminated 8 small clauses in 8304902 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 66 covered clauses in round 1
c [cce-1] eliminated 66 covered clauses in TOTAL during 1 rounds
c [cce-1] 66 < 1/100 * 3547337 = 35473 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 553810 variables 100%
c [elim-5] limit of 33219592 steps penalty 2 = 0 + 2
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 430809 not tried 78% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 16325 = 3% variables out of 553810 scheduled
c [bca-1] limit of 10000000 steps and 7059410 added (scaled 2)
c [bca-1] 1071278 out of 1074972 literals actually usable 100%
c [bca-1] added 10503 blocked clauses in 2194193 steps
c [sweep-1] limit 7058910 based on 3529455 irredundant clauses
c [sweep-1-1] 249224 pos 46.4% + 288261 neg 53.6% = 537485 sched 100.0% ret 0
c [sweep-1-1] 7210571 steps 25 queries 133123.72 avg class size
c [sweep-1-1] 113 decisions 23 SAT calls 15.48 avg env size
c [sweep-1-1] 537384 variables remain 100% (101 retained 0%)
c [decomp-11] removed 173 variables
c [sweep-1-1] removed 173 vars (0 failed, 1 eqs, 4 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 173 vars in TOTAL (1 rounds, 24 queries)
c [phase-count-5] 3523082 negative 99.8% of 3528794 except 5712 0.2%
c [phase-count-5] 3508900 positive 99.4% of 3528794 except 19894 0.6%
c [phase-count-5] less non-negative clauses 5712 than limit 352800 (10.0%)
c [phase-count-5] non-pos/non-neg = 19894/5712 = 3.48 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 51692 negative 100%
c [score-distribution-5] 11133 pos 2.07%, 0 min 0.00%, 526179 zero 97.93%
c [score-distribution-5] 2806 different 0.52% out of total 537312 variables
c [simplification-5] removed 20439 variables 3.7% (537312 remain 43%)
c [simplification-5] removed 82458 irredundant clauses 2.3% (3528794 remain 72%)
c [simplification-5] maximum reduction of 4% = max (4%, 2%)
c [simplification-5] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-5] new conflict interval 4000
c [simplification-5] penalized conflict interval 4000 = 1 * 4000
c [simplification-5] hard conflict limit 17040 (soft 7040 + delta 10000)
c [simplification-5] new conflict limit 7040 (hard 17040)
c 
c [simplification-6] limit 7040 conflicts (hard 17040) hit after 7040 conflicts
c [quatres-2] found 548557 quaternary clauses 98% in total
c [quatres-2-2] added 95 single-self-subsuming ternary resolvents
c [quatres-2-2] added 50 quaternary resolvents
c [ternres-2] limit 14115092 based on 3528773 irredundant clauses
c [ternres-2] 522542 schedulable variables 97%
c [ternres-2] 7536 ternary resolvents (3 bin, 7533 trn)
c [ternres-2] 509767 variables remain 95% (27545 retained 5%)
c [card-3] limit 882193 based on 3528773 irredundant clauses
c [card-3] found 403 at-most-one constraints of average size 3.5
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 882193 for elimination
c [card-3] 403 out of 403 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 1764386 based on 3528773 irredundant clauses
c [gauss-2] extracted 130 xors of average arity 3.0
c [gauss-2] connected 390 occurrences of 387 variables (average 1.0)
c [gauss-2] limit 1764386 based on 3528773 irredundant clauses
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 73 variables
c [treelook-3] limit 882129 based on 3528516 irredundant clauses
c [treelook-3] scheduled 77194 literals 7%
c [treelook-3] scheduling used 882131 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 882129 based on 3528516 irredundant clauses
c [treelook-3] used 962383 steps
c [treelook-3] 77064 literals remain 7%
c [treelook-3] 4142 variables remain to probed next time 1%
c [treelook-3] removed 124 variables, found 194 hbrs
c [unhide-6] limit 220468 based on 3527501 irredundant clauses
c [unhide-6-6] 27 units, 1775 failed, 826 tauts, 0 hbrs, 46096 literals
c [transred-2] limit 3521217 based on 3521217 irredundant clauses
c [transred-2] removed 12 transitive binary clauses
c [elim-6] 3333 variables 1% will be scheduled this time
c [elim-6] scheduled 3333 variables 1%
c [elim-6] limit of 68926463 steps penalty 2 = 0 + 2
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 2850 not tried 1% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 1 = 0% variables out of 3333 scheduled
c [elim-6] 1 < 1/100 * 3333 = 33 considered unsuccessful
c [bca-2] limit of 10000000 steps and 6982667 added (scaled 2)
c [bca-2] 1057089 out of 1064554 literals actually usable 99%
c [bca-2] added 110 blocked clauses in 2162622 steps
c [sweep-2] limit 6976916 based on 3488458 irredundant clauses
c [sweep-2-1] 281656 pos 52.9% + 250520 neg 47.1% = 532176 sched 100.0% ret 100
c [sweep-2-1] 7150484 steps 23 queries 142657.22 avg class size
c [sweep-2-1] 158 decisions 22 SAT calls 47.18 avg env size
c [sweep-2-1] 532093 variables remain 100% (183 retained 0%)
c [decomp-14] removed 369 variables
c [sweep-2-1] removed 369 vars (0 failed, 1 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 369 vars in TOTAL (1 rounds, 22 queries)
c [phase-count-6] 3482348 negative 99.8% of 3487714 except 5366 0.2%
c [phase-count-6] 3468211 positive 99.4% of 3487714 except 19503 0.6%
c [phase-count-6] less non-negative clauses 5366 than limit 348700 (10.0%)
c [phase-count-6] non-pos/non-neg = 19503/5366 = 3.63 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 15826 negative 100%
c [score-distribution-6] 14468 pos 2.72%, 5327 min 1.00%, 512112 zero 96.28%
c [score-distribution-6] 3603 different 0.68% out of total 531907 variables
c [simplification-6] removed 5405 variables 1.0% (531907 remain 42%)
c [simplification-6] removed 41080 irredundant clauses 1.2% (3487714 remain 71%)
c [simplification-6] maximum reduction of 1% = max (1%, 1%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 14000
c [simplification-6] penalized conflict interval 14000 = 1 * 14000
c [simplification-6] hard conflict limit 31040 (soft 21040 + delta 10000)
c [simplification-6] new conflict limit 21040 (hard 31040)
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.5  531906  3487714      7353    4830  11998 17844    5    90  277   5%     62   84    6    1 1100%
c i  183.1  531604  3487714     10566    7522  12310 17936    6   107  279   6%     34   96    7    1  820%
c i  191.2  531593  3487714     11708    8499  12405 17970    6   112  279   5%     15  100    6    1  646%
c i  194.8  530531  3487714     12213    8937  12436 17984    6   114  279   6%      9  100    7    1  722%
c i  204.8  528898  3487714     13543   10074  12549 18017    7   114  279   6%      8   99    7    1  627%
c i  207.4  528892  3487714     13922   10391  12584 18028    7   114  279   6%      5   97    7    1  608%
c i  246.1  528021  3487714     19103   14947  12903 18143    7   122  280   6%     59   98    6    2  374%
c 
c [simplification-7] limit of 2212 ternary hit after 2212 ternaries
c [quatres-3] found 489752 quaternary clauses 98% in total
c [quatres-3-2] added 41 single-self-subsuming ternary resolvents
c [quatres-3-2] added 27 quaternary resolvents
c [ternres-3] limit 13950852 based on 3487713 irredundant clauses
c [ternres-3] 499857 schedulable variables 94%
c [ternres-3] 8711 ternary resolvents (1 bin, 8710 trn)
c [ternres-3] 482805 variables remain 92% (44048 retained 8%)
c [decomp-15] removed 5135 variables
c [basicprobe-3] limit 51877354 penalty 2 = 0 + 2
c [basicprobe-3-0] 1982 probes remain 0% after last round
c [basicprobe-3-0] 150 units = 150 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 929 variables, found 18940 hbrs
c [bate-1] eliminated 533 asymmetric tautologies during probing
c [unhide-7] limit 518773 with penalty 4 = 0 + 4
c [unhide-7-7] 82 units, 609 failed, 28676 tauts, 0 hbrs, 22386 literals
c [transred-3] limit 3421393 based on 3421393 irredundant clauses
c [transred-3] removed 9 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 520734 variables 100%
c [block-2] limit of 51877354 steps penalty 3 = 1 + 2
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 214 blocked clauses
c [block-2] 214 < 1/100 * 3421385 = 34213 considered unsuccessful
c [cce-2] limit of 25938677 steps penalty 3 = 1 + 2
c [cce-2-1] eliminated 26 clauses out of 530 (5%) of length 12
c [cce-2-1] eliminated 11 clauses out of 178 (6%) of length 10
c [cce-2-1] eliminated 251 clauses out of 1236 (20%) of length 9
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 288 large clauses in 25938678 steps
c [cce-2-1] allowing another 12969339 steps for small clauses
c [cce-2-1] scheduling 1549972 clauses = 1103252 binary + 446720 ternary
c [cce-2-1] tried to eliminate 120 small clauses 0%
c [cce-2-1] eliminated 16 binary clauses 0%
c [cce-2-1] eliminated 2 ternary clauses 0%
c [cce-2-1] eliminated 18 small clauses 0%
c [cce-2-1] eliminated 18 small clauses in 25938677 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 306 covered clauses in round 1
c [cce-2] eliminated 306 covered clauses in TOTAL during 1 rounds
c [cce-2] 306 < 1/100 * 3391028 = 33910 considered unsuccessful
c [bca-3] limit of 10000000 steps and 6787250 added (scaled 2)
c [bca-3] 1027718 out of 1041462 literals actually usable 99%
c [bca-3] added 42 blocked clauses in 2105902 steps
c [sweep-3] limit 6781444 based on 3390722 irredundant clauses
c [sweep-3-1] 273484 pos 52.5% + 247066 neg 47.5% = 520550 sched 100.0% ret 180
c [sweep-3-1] 6868563 steps 32 queries 144453.72 avg class size
c [sweep-3-1] 235 decisions 28 SAT calls 98.29 avg env size
c [sweep-3-1] 520433 variables remain 100% (297 retained 0%)
c [decomp-16] removed 1144 variables
c [sweep-3-1] removed 1144 vars (0 failed, 3 eqs, 8 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 1144 vars in TOTAL (1 rounds, 31 queries)
c [phase-count-7] 3384895 negative 99.9% of 3389906 except 5011 0.1%
c [phase-count-7] 3371181 positive 99.4% of 3389906 except 18725 0.6%
c [phase-count-7] less non-negative clauses 5011 than limit 338900 (10.0%)
c [phase-count-7] non-pos/non-neg = 18725/5011 = 3.74 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 2379 negative 100%
c [score-distribution-7] 15715 pos 3.02%, 15556 min 2.99%, 488315 zero 93.98%
c [score-distribution-7] 3513 different 0.68% out of total 519586 variables
c [simplification-7] removed 7267 variables 1.4% (519586 remain 41%)
c [simplification-7] removed 97808 irredundant clauses 2.8% (3389906 remain 69%)
c [simplification-7] maximum reduction of 3% = max (1%, 3%)
c [simplification-7] forced so keeping old conflict interval 14000
c [simplification-7] conflict limit remains at 21040 (hard 31040)
c [simplification-7] new ternary interval 10000
c 
c [simplification-8] limit 21040 conflicts (hard 31040) hit after 21040 conflicts
c [quatres-4] found 363829 quaternary clauses 97% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 15 single-self-subsuming ternary resolvents
c [quatres-4-2] added 10 quaternary resolvents
c [ternres-4] limit 13559576 based on 3389894 irredundant clauses
c [ternres-4] 476158 schedulable variables 92%
c [ternres-4] 25256 ternary resolvents (3 bin, 25253 trn)
c [ternres-4] 459398 variables remain 88% (60188 retained 12%)
c [gauss-3] limit 1694947 based on 3389894 irredundant clauses
c [gauss-3] extracted 116 xors of average arity 2.9
c [gauss-3] connected 340 occurrences of 330 variables (average 1.0)
c [gauss-3] limit 1694947 based on 3389894 irredundant clauses
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 64 variables
c [simpleprobe-4] 410631 schedulable variables 79%
c [simpleprobe-4] limit 44770419 penalty 2 = 0 + 2
c [decomp-18] removed 521 variables
c [simpleprobe-4] 359789 variables remain 69% (159212 retained 31%)
c [simpleprobe-4] removed 521 variables, found 1001 hbrs, 35 units
c [unhide-8] limit 559630 with penalty 4 = 0 + 4
c [unhide-8-8] 18 units, 1184 failed, 3400 tauts, 0 hbrs, 96193 literals
c [transred-4] limit 3374411 based on 3374411 irredundant clauses
c [transred-4] removed 2 transitive binary clauses
c [transred-4] found 2 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 512828 variables 100%
c [elim-7] limit of 100000000 steps penalty 3 = 1 + 2
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 309221 not tried 60% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 49948 = 10% variables out of 512828 scheduled
c [bca-4] limit of 10000000 steps and 6554731 added (scaled 2)
c [bca-4] 913632 out of 925762 literals actually usable 99%
c [bca-4] added 111 blocked clauses in 1883487 steps
c [sweep-4] limit 6548904 based on 3274452 irredundant clauses
c [sweep-4-1] 236836 pos 51.2% + 225792 neg 48.8% = 462628 sched 99.9% ret 252
c [sweep-4-1] 6670462 steps 28 queries 106760.68 avg class size
c [sweep-4-1] 385 decisions 20 SAT calls 223.55 avg env size
c [sweep-4-1] 462457 variables remain 100% (308 retained 0%)
c [decomp-19] removed 254 variables
c [sweep-4-1] removed 254 vars (0 failed, 7 eqs, 8 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 254 vars in TOTAL (1 rounds, 27 queries)
c [phase-count-8] 3267621 negative 99.8% of 3273141 except 5520 0.2%
c [phase-count-8] 3254994 positive 99.4% of 3273141 except 18147 0.6%
c [phase-count-8] less non-negative clauses 5520 than limit 327300 (10.0%)
c [phase-count-8] non-pos/non-neg = 18147/5520 = 3.29 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 2007 negative 100%
c [score-distribution-8] 16678 pos 3.61%, 12705 min 2.75%, 433243 zero 93.65%
c [score-distribution-8] 3894 different 0.84% out of total 462626 variables
c [simplification-8] removed 56960 variables 11.0% (462626 remain 37%)
c [simplification-8] removed 116765 irredundant clauses 3.4% (3273141 remain 66%)
c [simplification-8] maximum reduction of 11% = max (11%, 3%)
c [simplification-8] large reduction 11% >= 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 33040 (soft 23040 + delta 10000)
c [simplification-8] new conflict limit 23040 (hard 33040)
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  313.4  462625  3273141     22714   15933  37382 20459    7   116  270   6%     35   88    7    2  379%
c 
c [simplification-9] limit 23040 conflicts (hard 33040) hit after 23041 conflicts
c [quatres-5] found 305991 quaternary clauses 96% in total
c [quatres-5-1] removed 5 duplicate quaternary clauses
c [quatres-5-2] added 1075 single-self-subsuming ternary resolvents
c [quatres-5-2] added 297 quaternary resolvents
c [ternres-5] limit 13092464 based on 3273116 irredundant clauses
c [ternres-5] 408483 schedulable variables 88%
c [ternres-5] 20228 ternary resolvents (30 bin, 20198 trn)
c [ternres-5] 396130 variables remain 86% (65883 retained 14%)
c [decomp-20] removed 646 variables
c [treelook-4] limit 1227758 penalty 2 = 0 + 2 boost 1
c [treelook-4] scheduled 69718 literals 8%
c [treelook-4] scheduling used 1227761 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 1227758 penalty 2 = 0 + 2 boost 1
c [treelook-4] used 1411783 steps
c [treelook-4] 69544 literals remain 8%
c [treelook-4] 2334 variables remain to probed next time 1%
c [treelook-4] removed 163 variables, found 214 hbrs
c [unhide-9] limit 1227758 with penalty 3 = 0 + 3
c [unhide-9-9] 21 units, 608 failed, 58551 tauts, 0 hbrs, 15665 literals
c [transred-5] limit 3219897 based on 3219897 irredundant clauses
c [transred-5] removed 6 transitive binary clauses
c [elim-8] 2093 variables 0% will be scheduled this time
c [elim-8] scheduled 2093 variables 0%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4000000000 steps penalty 2 = 0 + 2
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 3520552535 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 39 = 2% variables out of 2093 scheduled
c [elim-8] 39 < 1/100 * 2093 = 20 considered unsuccessful
c [bca-5] limit of 10000000 steps and 6188297 added (scaled 2)
c [bca-5] 904517 out of 918076 literals actually usable 99%
c [bca-5] added 11 blocked clauses in 1866149 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 36832767 penalty 2 = 0 + 2
c [sweep-5-1] 241138 pos 52.6% + 217601 neg 47.4% = 458739 sched 99.9% ret 298
c [sweep-5-1] 37046408 steps 182 queries 42624.13 avg class size
c [sweep-5-1] 756 decisions 138 SAT calls 39.45 avg env size
c [sweep-5-1] 457055 variables remain 100% (1122 retained 0%)
c [decomp-22] removed 2283 variables
c [sweep-5-1] removed 2283 vars (0 failed, 45 eqs, 53 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 2283 vars in TOTAL (1 rounds, 181 queries)
c [phase-count-9] 3077354 negative 99.8% of 3082287 except 4933 0.2%
c [phase-count-9] 3065765 positive 99.5% of 3082287 except 16522 0.5%
c [phase-count-9] less non-negative clauses 4933 than limit 308200 (10.0%)
c [phase-count-9] non-pos/non-neg = 16522/4933 = 3.35 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 1433 negative 100%
c [score-distribution-9] 13616 pos 2.98%, 18895 min 4.14%, 424243 zero 92.88%
c [score-distribution-9] 3560 different 0.78% out of total 456754 variables
c [simplification-9] removed 5259 variables 1.1% (456754 remain 36%)
c [simplification-9] removed 190854 irredundant clauses 5.8% (3082287 remain 63%)
c [simplification-9] maximum reduction of 6% = max (1%, 6%)
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 35041 (soft 25041 + delta 10000)
c [simplification-9] new conflict limit 25041 (hard 35041)
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  368.6  456753  3082287     24475   17672  56739 20864    7   119  260   6%     14   88    8    2  374%
c 
c [simplification-10] limit 25041 conflicts (hard 35041) hit after 25041 conflicts
c [quatres-6] found 258808 quaternary clauses 96% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 174 single-self-subsuming ternary resolvents
c [quatres-6-2] added 41 quaternary resolvents
c [ternres-6] limit 13569598 with penalty 2 = 0 + 2
c [ternres-6] 391669 schedulable variables 86%
c [ternres-6] 29865 ternary resolvents (3 bin, 29862 trn)
c [ternres-6] 376009 variables remain 82% (80739 retained 18%)
c [card-4] limit 848099 penalty 5 = 3 + 2
c [card-4] found 328 at-most-one constraints of average size 3.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 848099 for elimination
c [card-4] 328 out of 328 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-23] removed 18 variables
c [basicprobe-4] limit 67847993 penalty 2 = 0 + 2
c [basicprobe-4-0] 2356 sched 1%, 366 failed, 0 lifted, 16982 hbrs
c [decomp-24] removed 2582 variables
c [basicprobe-4-1] 7160 probes remain 2% after last round
c [basicprobe-4-1] 444 units = 444 failed (100%) + 0 lifted (0%)
c [basicprobe-4-1] removed 2908 variables, found 23354 hbrs
c [bate-2] eliminated 616 asymmetric tautologies during probing
c [unhide-10] limit 1356959 with penalty 3 = 0 + 3
c [unhide-10-10] 34 units, 1666 failed, 6491 tauts, 0 hbrs, 55102 literals
c [transred-6] limit 3056793 based on 3056793 irredundant clauses
c [transred-6] removed 15 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 445833 variables 100%
c [block-3] limit of 33923996 steps penalty 4 = 2 + 2
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 123 blocked clauses
c [block-3] 123 < 1/100 * 3056779 = 30567 considered unsuccessful
c [cce-3] limit of 16961998 steps penalty 4 = 2 + 2
c [cce-3-1] eliminated 2 clauses out of 23 (9%) of length 18
c [cce-3-1] eliminated 57 clauses out of 128 (45%) of length 14
c [cce-3-1] eliminated 51 clauses out of 505 (10%) of length 13
c [cce-3-1] eliminated 313 clauses out of 661 (47%) of length 12
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 423 large clauses in 16962030 steps
c [cce-3-1] allowing another 8481015 steps for small clauses
c [cce-3-1] scheduling 2302154 clauses = 1010816 binary + 1291338 ternary
c [cce-3-1] tried to eliminate 94 small clauses 0%
c [cce-3-1] eliminated 13 binary clauses 0%
c [cce-3-1] eliminated 13 small clauses 0%
c [cce-3-1] eliminated 13 small clauses in 16961999 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 436 covered clauses in round 1
c [cce-3] eliminated 436 covered clauses in TOTAL during 1 rounds
c [cce-3] 436 < 1/100 * 3004796 = 30047 considered unsuccessful
c [bca-6] limit of 10000000 steps and 6014608 added (scaled 2)
c [bca-6] 877594 out of 891668 literals actually usable 98%
c [bca-6] added 959 blocked clauses in 1809412 steps
c [sweep-6] limit 6008720 based on 3004360 irredundant clauses
c [sweep-6-1] 233094 pos 52.4% + 211708 neg 47.6% = 444802 sched 99.8% ret 1031
c [sweep-6-1] 6037981 steps 23 queries 100666.13 avg class size
c [sweep-6-1] 167 decisions 19 SAT calls 149.79 avg env size
c [sweep-6-1] 444755 variables remain 100% (1078 retained 0%)
c [decomp-25] removed 537 variables
c [sweep-6-1] removed 537 vars (0 failed, 3 eqs, 4 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 537 vars in TOTAL (1 rounds, 22 queries)
c [phase-count-10] 2997989 negative 99.8% of 3003054 except 5065 0.2%
c [phase-count-10] 2986013 positive 99.4% of 3003054 except 17041 0.6%
c [phase-count-10] less non-negative clauses 5065 than limit 300300 (10.0%)
c [phase-count-10] non-pos/non-neg = 17041/5065 = 3.36 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 831 negative 100%
c [score-distribution-10] 13581 pos 3.05%, 20208 min 4.54%, 411507 zero 92.41%
c [score-distribution-10] 3205 different 0.72% out of total 445296 variables
c [simplification-10] removed 11452 variables 2.5% (445296 remain 35%)
c [simplification-10] removed 79233 irredundant clauses 2.6% (3003054 remain 61%)
c [simplification-10] maximum reduction of 3% = max (3%, 3%)
c [simplification-10] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-10] new conflict interval 19000
c [simplification-10] penalized conflict interval 19000 = 1 * 19000
c [simplification-10] hard conflict limit 54041 (soft 44041 + delta 10000)
c [simplification-10] new conflict limit 44041 (hard 54041)
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  421.1  445295  3003054     29438   22165  84795 26363    7   117  260   6%     52   80    7    3  289%
c i  457.9  445293  3003054     34578   26916  85003 26409    8   124  260   6%     53   81    7    3  228%
c i  466.8  445001  3003054     35802   28022  85085 26423    8   123  260   6%     15   78    8    3  270%
c i  497.4  444851  3003054     39926   31842  85236 26455    8   121  260   7%     36   72    8    3  231%
c 
c [simplification-11] limit 44041 conflicts (hard 54041) hit after 44042 conflicts
c [quatres-7] found 158689 quaternary clauses 92% in total
c [quatres-7-2] added 1092 single-self-subsuming ternary resolvents
c [quatres-7-2] added 36 quaternary resolvents
c [ternres-7] limit 25373958 with penalty 2 = 0 + 2
c [ternres-7] 365884 schedulable variables 82%
c [ternres-7] 79489 ternary resolvents (25 bin, 79464 trn)
c [ternres-7] 340185 variables remain 77% (104243 retained 23%)
c [gauss-4] limit 1501524 based on 3003049 irredundant clauses
c [gauss-4] extracted 116 xors of average arity 2.9
c [gauss-4] connected 336 occurrences of 332 variables (average 1.0)
c [gauss-4] limit 2537395 penalty 3 = 2 + 1
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-26] removed 95 variables
c [simpleprobe-5] 307559 schedulable variables 69%
c [simpleprobe-5] limit 100000000 penalty 1 = 0 + 1
c [decomp-27] removed 192 variables
c [simpleprobe-5] 309042 variables remain 70% (135099 retained 30%)
c [simpleprobe-5] removed 192 variables, found 2200 hbrs, 7 units
c [unhide-11] limit 2500000 with penalty 3 = 0 + 3
c [unhide-11-11] 21 units, 328 failed, 26863 tauts, 0 hbrs, 8303 literals
c [transred-7] limit 2965978 based on 2965978 irredundant clauses
c [transred-7] removed 4 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 440456 variables 100%
c [elim-9] limit of 200000000 steps penalty 2 = 1 + 1
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 146402 not tried 33% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 91282 = 21% variables out of 440456 scheduled
c [bca-7] limit of 10000000 steps and 5621994 added (scaled 2)
c [bca-7] 681524 out of 698350 literals actually usable 98%
c [bca-7] added 13 blocked clauses in 1430147 steps
c [sweep-7] limit 15224375 penalty 1 = 0 + 1
c [sweep-7-1] 180258 pos 51.7% + 168136 neg 48.3% = 348394 sched 99.8% ret 780
c [sweep-7-1] 15964977 steps 65 queries 51249.31 avg class size
c [sweep-7-1] 1012 decisions 48 SAT calls 197.85 avg env size
c [sweep-7-1] 347874 variables remain 100% (1076 retained 0%)
c [decomp-28] removed 278 variables
c [sweep-7-1] removed 278 vars (0 failed, 16 eqs, 9 impls)
c [sweep-7] 278 < 1/1000 * 349174 = 349 considered unsuccessful
c [sweep-7] removed 278 vars in TOTAL (1 rounds, 64 queries)
c [phase-count-11] 2800687 negative 99.8% of 2805561 except 4874 0.2%
c [phase-count-11] 2788789 positive 99.4% of 2805561 except 16772 0.6%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 76 positive 100%, 0 negative 0%
c [score-distribution-11] 12321 pos 3.53%, 25551 min 7.32%, 311024 zero 89.15%
c [score-distribution-11] 3182 different 0.91% out of total 348896 variables
c [simplification-11] removed 95532 variables 21.5% (348896 remain 28%)
c [simplification-11] removed 197493 irredundant clauses 6.6% (2805561 remain 57%)
c [simplification-11] maximum reduction of 21% = max (21%, 7%)
c [simplification-11] large reduction 21% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 56042 (soft 46042 + delta 10000)
c [simplification-11] new conflict limit 46042 (hard 56042)
c 
c [simplification-12] limit 46042 conflicts (hard 56042) hit after 46043 conflicts
c [quatres-8] found 228932 quaternary clauses 94% in total
c [quatres-8-1] removed 10 duplicate quaternary clauses
c [quatres-8-2] added 3265 single-self-subsuming ternary resolvents
c [quatres-8-2] added 2345 quaternary resolvents
c [ternres-8] limit 53030971 with penalty 1 = 0 + 1
c [ternres-8] 267190 schedulable variables 77%
c [ternres-8] 262051 ternary resolvents (43 bin, 262008 trn)
c [ternres-8] 160313 variables remain 46% (188583 retained 54%)
c [decomp-29] removed 4 variables
c [treelook-5] limit 5303097 penalty 1 = 0 + 1 boost 1
c [treelook-5] scheduled 66946 literals 10%
c [treelook-5] scheduling used 3055074 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 5303097 penalty 1 = 0 + 1 boost 1
c [treelook-5] used 5349108 steps
c [treelook-5] 65850 literals remain 9%
c [treelook-5] 1690 variables remain to probed next time 0%
c [decomp-30] removed 15 variables
c [treelook-5] removed 1034 variables, found 4391 hbrs
c [unhide-12] limit 2500000 with penalty 3 = 0 + 3
c [unhide-12-12] 7 units, 1363 failed, 3426 tauts, 0 hbrs, 31694 literals
c [transred-8] limit 2780795 based on 2780795 irredundant clauses
c [transred-8] removed 68 transitive binary clauses
c [elim-10] 144966 variables 42% will be scheduled this time
c [elim-10] scheduled 144966 variables 42%
c [elim-10] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 829 not tried 0% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 9081 = 6% variables out of 144966 scheduled
c [bca-8] limit of 10000000 steps and 5303148 added (scaled 2)
c [bca-8] 652899 out of 673882 literals actually usable 97%
c [bca-8] added 19 blocked clauses in 1375096 steps
c [phase-count-12] 2643492 negative 99.8% of 2648387 except 4895 0.2%
c [phase-count-12] 2631950 positive 99.4% of 2648387 except 16437 0.6%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 9 positive 39%, 14 negative 61%
c [score-distribution-12] 13465 pos 4.00%, 24355 min 7.23%, 299120 zero 88.78%
c [score-distribution-12] 3247 different 0.96% out of total 336940 variables
c [simplification-12] removed 11956 variables 3.4% (336940 remain 27%)
c [simplification-12] removed 157174 irredundant clauses 5.6% (2648387 remain 54%)
c [simplification-12] maximum reduction of 6% = max (3%, 6%)
c [simplification-12] large reduction 6% >= 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 58043 (soft 48043 + delta 10000)
c [simplification-12] new conflict limit 48043 (hard 58043)
c 
c [simplification-13] limit 48043 conflicts (hard 58043) hit after 48045 conflicts
c [quatres-9] found 201608 quaternary clauses 93% in total
c [quatres-9-1] removed 3 duplicate quaternary clauses
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 622 single-self-subsuming ternary resolvents
c [quatres-9-2] added 1019 quaternary resolvents
c [ternres-9] limit 55422586 with penalty 1 = 0 + 1
c [ternres-9] 154771 schedulable variables 46%
c [ternres-9] 422847 ternary resolvents (65 bin, 422782 trn)
c [ternres-9] 52408 variables remain 16% (284532 retained 84%)
c [decomp-31] removed 482 variables
c [basicprobe-5] limit 200000000 penalty 1 = 0 + 1
c [basicprobe-5-0] 7345 sched 2%, 534 failed, 70 lifted, 25139 hbrs
c [decomp-32] removed 1703 variables
c [basicprobe-5-1] 2507 probes remain 1% after last round
c [basicprobe-5-1] 1076 units = 968 failed (90%) + 108 lifted (10%)
c [basicprobe-5-1] removed 3251 variables, found 34439 hbrs
c [bate-3] eliminated 649 asymmetric tautologies during probing
c [unhide-13] limit 2500000 with penalty 3 = 0 + 3
c [unhide-13-13] 77 units, 287 failed, 74421 tauts, 0 hbrs, 13048 literals
c [transred-9] limit 2551827 based on 2551827 irredundant clauses
c [transred-9] removed 51 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 330717 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 746 not tried 0% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 33735 = 10% variables out of 330717 scheduled
c [bca-9] limit of 10000000 steps and 4851922 added (scaled 2)
c [bca-9] 571502 out of 593966 literals actually usable 96%
c [bca-9] added 0 blocked clauses in 1214095 steps
c [sweep-8] limit 8313387 penalty 2 = 1 + 1
c [sweep-8-1] 155078 pos 52.4% + 140989 neg 47.6% = 296067 sched 99.7% ret 915
c [sweep-8-1] 8371514 steps 41 queries 47460.34 avg class size
c [sweep-8-1] 513 decisions 33 SAT calls 139.39 avg env size
c [sweep-8-1] 295896 variables remain 100% (1086 retained 0%)
c [decomp-33] removed 214 variables
c [sweep-8-1] removed 214 vars (0 failed, 7 eqs, 9 impls)
c [sweep-8] 214 < 1/1000 * 296982 = 296 considered unsuccessful
c [sweep-8] removed 214 vars in TOTAL (1 rounds, 40 queries)
c [phase-count-13] 2417407 negative 99.8% of 2422173 except 4766 0.2%
c [phase-count-13] 2406601 positive 99.4% of 2422173 except 15572 0.6%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 24 positive 73%, 9 negative 27%
c [score-distribution-13] 13408 pos 4.52%, 22646 min 7.63%, 260714 zero 87.85%
c [score-distribution-13] 3738 different 1.26% out of total 296768 variables
c [simplification-13] removed 40172 variables 11.9% (296768 remain 24%)
c [simplification-13] removed 226214 irredundant clauses 8.5% (2422173 remain 49%)
c [simplification-13] maximum reduction of 12% = max (12%, 9%)
c [simplification-13] large reduction 12% >= 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 60045 (soft 50045 + delta 10000)
c [simplification-13] new conflict limit 50045 (hard 60045)
c 
c [simplification-14] limit 50045 conflicts (hard 60045) hit after 50045 conflicts
c [quatres-10] found 196220 quaternary clauses 93% in total
c [quatres-10-1] removed 13 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 2924 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1915 quaternary resolvents
c [ternres-10] limit 58286767 with penalty 1 = 0 + 1
c [ternres-10] 48986 schedulable variables 17%
c [ternres-10] 361377 ternary resolvents (175 bin, 361202 trn)
c [ternres-10] 12150 variables remain 4% (284618 retained 96%)
c [decomp-34] removed 12 variables
c [simpleprobe-6] 206593 schedulable variables 70%
c [simpleprobe-6] limit 100000000 penalty 1 = 0 + 1
c [decomp-35] removed 45 variables
c [simpleprobe-6] 208030 variables remain 70% (88681 retained 30%)
c [simpleprobe-6] removed 45 variables, found 1943 hbrs, 1 units
c [unhide-14] limit 2500000 with penalty 3 = 0 + 3
c [unhide-14-14] 7 units, 798 failed, 12502 tauts, 0 hbrs, 17705 literals
c [transred-10] limit 2419115 based on 2419115 irredundant clauses
c [transred-10] removed 74 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 294121 variables 100%
c [block-4] limit of 50000000 steps penalty 4 = 3 + 1
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 56 blocked clauses
c [block-4] 56 < 1/100 * 2419044 = 24190 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 364292295 steps penalty 4 = 3 + 1
c [cce-4-1] eliminated 57 clauses out of 398 (14%) of length 12
c [cce-4-1] eliminated 4 clauses out of 112 (4%) of length 11
c [cce-4-1] eliminated 30 clauses out of 1428 (2%) of length 9
c [cce-4-1] eliminated 263 clauses out of 1407 (19%) of length 8
c [cce-4-1] eliminated 31 clauses out of 1062 (3%) of length 7
c [cce-4-1] eliminated 27 clauses out of 72 (38%) of length 6
c [cce-4-1] eliminated 866 clauses out of 1664 (52%) of length 5
c [cce-4-1] eliminated 1570 clauses out of 176322 (1%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 2848 large clauses in 364292300 steps
c [cce-4-1] allowing another 182146150 steps for small clauses
c [cce-4-1] scheduling 1380805 clauses = 813720 binary + 567085 ternary
c [cce-4-1] tried to eliminate 4059 small clauses 0%
c [cce-4-1] eliminated 876 binary clauses 0%
c [cce-4-1] eliminated 718 ternary clauses 0%
c [cce-4-1] eliminated 1594 small clauses 0%
c [cce-4-1] eliminated 1594 small clauses in 364292302 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 4442 covered clauses in round 1
c [cce-4] eliminated 4442 covered clauses in TOTAL during 1 rounds
c [cce-4] 4442 < 1/100 * 2397481 = 23974 considered unsuccessful
c [elim-12] 666 variables 0% will be scheduled this time
c [elim-12] scheduled 666 variables 0%
c [elim-12] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 328 not tried 0% in round 1
c [elim-12] transition to [ all 0 rem 1 ] state
c [elim-12] eliminated 18 = 3% variables out of 666 scheduled
c [elim-12] 18 < 1/100 * 666 = 6 considered unsuccessful
c [phase-count-14] 2384766 negative 99.8% of 2389230 except 4464 0.2%
c [phase-count-14] 2373704 positive 99.4% of 2389230 except 15526 0.6%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 7 positive 41%, 10 negative 59%
c [score-distribution-14] 13009 pos 4.42%, 23506 min 7.99%, 257588 zero 87.58%
c [score-distribution-14] 3006 different 1.02% out of total 294103 variables
c [simplification-14] removed 2665 variables 0.9% (294103 remain 23%)
c [simplification-14] removed 32943 irredundant clauses 1.4% (2389230 remain 48%)
c [simplification-14] maximum reduction of 1% = max (1%, 1%)
c [simplification-14] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-14] new conflict interval 29000
c [simplification-14] penalized conflict interval 29000 = 1 * 29000
c [simplification-14] hard conflict limit 93545 (soft 79045 + delta 14500)
c [simplification-14] new conflict limit 79045 (hard 93545)
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  749.1  294102  2389230     61956   52569 1024272 35045    8   116  297   7%    270   48    8    5  170%
c 
c [simplification-15] limit 79045 conflicts (hard 93545) hit after 79046 conflicts
c [quatres-11] found 176214 quaternary clauses 90% in total
c [quatres-11-2] added 838 single-self-subsuming ternary resolvents
c [quatres-11-2] added 119 quaternary resolvents
c [ternres-11] limit 100000000 with penalty 1 = 0 + 1
c [ternres-11] 12099 schedulable variables 4%
c [ternres-11] 55216 ternary resolvents (278 bin, 54938 trn)
c [ternres-11] 11375 variables remain 4% (282727 retained 96%)
c [card-5] limit 3178677 penalty 5 = 4 + 1
c [card-5] found 1039 at-most-one constraints of average size 3.5
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 3178677 for elimination
c [card-5] 1039 out of 1039 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-5] limit 2542942 penalty 4 = 3 + 1
c [gauss-5] extracted 131 xors of average arity 2.8
c [gauss-5] connected 365 occurrences of 347 variables (average 1.1)
c [gauss-5] limit 2542942 penalty 4 = 3 + 1
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-36] removed 470 variables
c [treelook-6] limit 10171768 penalty 1 = 0 + 1 boost 1
c [treelook-6] scheduled 49092 literals 8%
c [treelook-6] scheduling used 2795699 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 10171768 penalty 1 = 0 + 1 boost 1
c [treelook-6] used 10328490 steps
c [treelook-6] 47612 literals remain 8%
c [treelook-6] 1608 variables remain to probed next time 1%
c [decomp-37] removed 163 variables
c [treelook-6] removed 1289 variables, found 2784 hbrs
c [unhide-15] limit 2500000 with penalty 3 = 0 + 3
c [unhide-15-15] 10 units, 200 failed, 41587 tauts, 0 hbrs, 19386 literals
c [transred-11] limit 2341635 based on 2341635 irredundant clauses
c [transred-11] removed 42 transitive binary clauses
c [bca-10] limit of 10000000 steps and 4672388 added (scaled 2)
c [bca-10] 550158 out of 582268 literals actually usable 94%
c [bca-10] added 70 blocked clauses in 1198216 steps
c [phase-count-15] 2328931 negative 99.8% of 2333002 except 4071 0.2%
c [phase-count-15] 2318167 positive 99.4% of 2333002 except 14835 0.6%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 1 positive 33%, 2 negative 67%
c [score-distribution-15] 13252 pos 4.55%, 27131 min 9.32%, 250750 zero 86.13%
c [score-distribution-15] 3335 different 1.15% out of total 291133 variables
c [simplification-15] removed 2969 variables 1.0% (291133 remain 23%)
c [simplification-15] removed 56228 irredundant clauses 2.4% (2333002 remain 47%)
c [simplification-15] maximum reduction of 2% = max (1%, 2%)
c [simplification-15] geometric conflict interval increment 9666 = 29000 / 3
c [simplification-15] new conflict interval 38666
c [simplification-15] penalized conflict interval 38666 = 1 * 38666
c [simplification-15] hard conflict limit 137045 (soft 117712 + delta 19333)
c [simplification-15] new conflict limit 117712 (hard 137045)
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 -  888.1  291133  2333002     79997   26250 1060130 37542    9   114  292   8%    186   35    9    6  159%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 1798 basic ate = 1201 trn 67% + 597 lrg 33% in 3 updates
c bcas: 10 count, 11838 added (828 skipped), 17239319 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 4 bces, 5368 removed, 38190712 resolutions, 110263391 steps
c blkd: 5122 blocking literals 0%, 4 pure
c bump: 95592 bumped seen, 4278636 lits 44.8 on average
c card: 5 count, 0 units, 0 am1, 15862398 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 28027 subsumed
c card: 3323 at-most-one constraints found, average size 3.57
c card: 3323 at-most-one constraints used 100%, average size 3.57
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: 4 cces, 5250 eliminated, 5176 ate 99%, 74 abce 1%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 18026410 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 96 gcs, 0 rescored clauses, 50 rescored vars
c dcps: 37 decompositions, 50276 equivalent 4%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1963339 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 14142960 push, 12847539 pop (12847539 dec 100%)
c dsch: 235508084 swaps, 0 down, 226550046 up
c elms: 12 elims, 595524 eliminated 46%, 94 pure 0%
c elms: 12 rounds, 1.0 rounds/bve
c elms: 592917 small 100%, 2509 large 0%
c elms: 1622677 tried small, 592917 succeeded 37%, 1029760 failed 63%
c elms: 324707 subsumed, 65966 strengthened, 41 blocked
c elms: 46168157 copies, 37104569 resolutions, 83064500 ipos
c elms: 47194035 subchks, 27772543 strchks
c gaus: 5 extractions, 702 extracted, 2.8 size, 3 max
c gaus: exported 0 units, 0 binary and 2 ternary equations
c gaus: 0 gc, 18629992 steps, 9314996 extr 50%, 3062 elim 0%
c glue: 7.9 orig avg, 7.9 real avg, 1.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 134125 = 5973 simple 4% + 127326 trn 95% + 826 lrg 1%, 20058 sub 15%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 95592 clauses, 16.4 length
c lrnd: 1565534 lits = 1992045 orig - 426511 removed 21%
c lrnd: 50046 uips 52%, 31933 flips 33%
c mins: 88090 mins 92%, 870 bin 1%, 6632 size 7%
c mins: 2555979 poisoned searches, 402667 hits, 16% hit rate
c mins: 4025121 used twice searches, 388974 hits, 10% hit rate
c move: moved 54291, 1591 bin 3%, 52700 trn 97%
c otfs: 435 driving 46%, 519 restarting 54%
c otfs: str 954, 762 red 80%, 192 irr 20%
c otfs: str 954, 0 bin 0%, 129 trn 14%, 825 lrg 86%
c otfs: sub 4, 4 red 100%, 0 irr 0%
c otfs: sub 4, 0 bin 0%, 2 trn 50%, 2 lrg 50%
c phas: 15 computed, 1833296 set, 117 pos (0%), 1833179 neg (100%)
c prbs: 5 basic, 50601 probed, 1780 failed, 642 lifted
c prbs: 6 simple, 955856 probed, 52 failed, 335 eqs
c prbs: 6 treelook, 468 probed, 79 failed, 0 lifted
c prom: 452 locked 1% out of 57527 tried
c prps: 2036496762 props, 1021 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 11 count, 5967 quat, 10236 self1, 2 self2, 248 dup
c redc: 3390 clauses 8%, 40245 tried 42%, 90 sat 0%
c redc: 4929 lits 1%, 393627 tried 20%, 90 sat 0%
c redc: 308 times jump level reduced, 8.4 levels on average
c reds: 1 count, 95857.0 conflicts per reduce
c reds: 0 memlim 0%, 1 arith 100%
c reds: 25003 collected 57%, 18569 retired 43%
c rmbd: 107955 removed, 18894 red 18%
c rsts: 9022 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: 15 count, 12 confs 80%, 0 vars 0%
c simp: 1 its 7%, 1 bin 7%, 1 trns 7%
c subl: 95592 count (35224 tried 0.4), 2015 sub out of 89920 (2.2%)
c swps: 8 count, 8 rounds, 411 queries (51.4/round)
c swps: 331 sat calls, 7 unsat (0.5% success rate)
c swps: 3339 decisions 10.1, 170 conflicts 0.5
c swps; 71948.9 avg class size, 93.7 avg environment size
c swps: 0 failed, 96 impls, 83 equivs
c swp0: 135 type 0 queries, 17 unsat (12.6%), 133 sat (98.5%)
c swp1: 276 type 1 queries, 227 unsat (82.2%), 195 sat (70.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: 4118262 calls to obtain time
c tops: 359302 fixed 28%, 28 its, 3423.46 confs/it
c trds: 11 transitive reductions, 290 removed, 2 failed
c trds: 5586 nodes, 6461 edges, 33287566 steps
c trim: 22134 words, 0.1 MB
c trnr: 11 count, 626 bin, 1274299 trn, 374846870 steps
c unhd: 15 count, 15 rounds, 220055532 steps
c unhd: 635 non-trivial sccs of average size 2.6
c unhd: 360 units, 309 bin, 32 trn, 19 lrg
c unhd: 12047 failed, 11662 stamp, 0 lits, 91 bin, 282 trn, 19 lrg
c unhd: 319585 tauts, 1182 bin 0%, 110630 trn 35%, 2239 lrg 1%
c unhd: 319585 tauts, 205534 stamp 64%, 99564 red 31%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 383817 str, 309 bin 0%, 35705 trn 9%, 347803 lrg 91%, 50999 red 13%
c vars: 291133 remaining 22% and 1005102 removed 78% out of 1296235
c vars: 359302 fixed 28%, 595524 eliminated 46%, 50276 equivalent 4%
c vsts: 25840791989 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 12.7 search visits per propagation, 265622.1 per conflict
c wchs: 1228601197 pushed, 211086490 enlarged, 148 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all          95887         25003         18569       2818432        324356         36077
c 
c  0 0         27700  29       411   2         0   0   2155807  76<   191974  59     17159  48     0.8
c  1 5         10430  11      2987  12      1668   9    277151  10     43234  13<     5861  16<    0.4
c  2 6         25703  27<    10552  42<     5842  31    279800  10     59981  18      9457  26     1.2
c  3 9         19846  21      7341  29      6264  34<    85899   3     22253   7      3035   8     1.3
c  4 14         8576   9      2766  11      3293  18     15249   1      5274   2       472   1     0.8
c  5 21         2799   3       756   3      1149   6      3577   0      1314   0        73   0     0.4
c  6 30          692   1       159   1       295   2       785   0       276   0        15   0     0.1
c  7 41          120   0        26   0        45   0       135   0        43   0         5   0     0.0
c  8 54           18   0         5   0        10   0        23   0         7   0         0   0     0.0
c  9 69            2   0         0   0         2   0         2   0         0   0         0   0     0.0
c 10 86            0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 11 126           1   0         0   0         1   0         4   0         0   0         0   0     0.0
c 
c avg                  1.8           2.5           2.9           0.4           0.8           1.0
c std                  1.5           1.0           1.1           0.9           1.1           1.1
c 
c  122.558  12% elim
c   41.774   4% probe
c   35.319   4% quatres
c   23.456   2% unhide
c   18.090   2% sweep
c   17.486   2% cce
c   11.121   1% block
c   11.097   1% bca
c    6.189   1% gauss
c 
c   14.451 < 1% rest (below)
c 
c    4.696   0% ternres
c    4.236   0% transred
c    3.437   0% decide
c    0.989   0% card
c    0.741   0% rescore
c    0.353   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    9.702   1% preprocessing     3%
c  325.707  33% inprocessing     97%
c ==================================
c  335.408  34% simplifying
c  661.528  66% search
c ==================================
c  996.960 100% all
c 
c         95857 conflicts,          96.1 confs/sec
c          4406 ternaries,          21.8 confs/ternary
c          1124 binaries,           85.3 confs/binary
c            28 iterations,       3423.5 confs/iteration
c 
c             1 reductions,          0.0 redus/sec,  95857.0 confs/reduction
c          9022 restarts,            9.0 rests/sec,     10.6 confs/restart
c       1963339 decisions,        1969.3 decis/sec,     20.5 decis/conflict
c    2036496762 propagations,  2042706.8 props/sec,   1037.3 props/decision
c 
c 997.0 seconds, 423.6 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
