c launch: /data/cnf/sc2014/app/SAT_dat.k100-24_1_rule_1.cnf.bz2
c host: atom02
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/SAT_dat.k100-24_1_rule_1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/SAT_dat.k100-24_1_rule_1.cnf.bz2
c no embedded options
c found 'p cnf 1621762 6356704' header
c read 1621762 variables, 6356704 clauses, 15957567 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=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 1571529 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] INC (--score=1)
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 1571529  6306337         0       0      0     0    0     0  298   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1576584 based on 6306337 irredundant clauses
c [card-1] found 1402 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1576584 for elimination
c [card-1] 1402 out of 1402 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 318929 variables
c [simpleprobe-1] all 1302833 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 10605514 based on 5302757 irredundant clauses
c [decomp-2] removed 3013 variables
c [simpleprobe-1] 1264778 variables remain 97% (35042 retained 3%)
c [simpleprobe-1] removed 3013 variables, found 30496 hbrs, 309 units
c [unhide-1] limit 330626 based on 5290025 irredundant clauses
c [unhide-1-1] 1965 units, 1560 failed, 10951 tauts, 0 hbrs, 65919 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 1293655 variables 100%
c [elim-1] limit of 5134746 steps based on 5134746 irredundant clauses
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 1211121 not tried 94% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 82864 = 6% variables out of 1293655 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 4739155 negative 95.2% of 4977964 except 238809 4.8%
c [phase-count-1] 4662911 positive 93.7% of 4977964 except 315053 6.3%
c [phase-1] phase bias: 562775 positive 46%, 648016 negative 54%
c [sort-queue-1] sorted 1210791 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 1210791 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 190963 variables 13.6% (1210791 remain 77%)
c [simplification-1] removed 1328373 irredundant clauses 21.1% (4977964 remain 79%)
c [simplification-1] maximum reduction of 21% = max (14%, 21%)
c [simplification-1] large reduction 21% >= 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   19.8 1210790  4977964         4       1     34 25615    0     0  296   0%      0    0    0    0 25368%
c i   19.9 1210659  4977964         8       3     34 25616    0     1  296   0%      0    1    0    0 25136%
c i   19.9 1210606  4977964        12       3     36 25617    0     1  296   0%      0    1    0    0 24898%
c i   20.0 1210605  4977964       108      68     50 25630    0     2  296   4%      0    2    1    0 21288%
c i   20.2 1210604  4977964       173     118     53 25635    0     2  296   7%      0    2    2    0 19399%
c i   20.2 1210603  4977964       184     125     53 25635    0     2  296   8%      0    2    2    0 19146%
c i   20.2 1210393  4977964       223     157     55 25636    0     2  296   9%      0    2    2    0 17707%
c i   20.5 1210392  4977964       278     198     64 25640    0     4  296   6%      0    4    2    0 15844%
c i   21.5 1210391  4977964       545     411     83 25665    1     7  296   8%      1    7    5    0 12661%
c 
c [simplification-2] limit 1006 conflicts (hard 11000) hit after 1006 conflicts
c [decomp-3] removed 4624 variables
c [simpleprobe-2] 1173605 schedulable variables 97%
c [simpleprobe-2] limit 9932564 based on 4966282 irredundant clauses
c [decomp-4] removed 844 variables
c [simpleprobe-2] 1173852 variables remain 97% (31471 retained 3%)
c [simpleprobe-2] removed 844 variables, found 35404 hbrs, 137 units
c [treelook-1] limit 1240679 based on 4962717 irredundant clauses
c [treelook-1] scheduled 249603 literals 10%
c [treelook-1] scheduling used 1240771 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1240679 based on 4962717 irredundant clauses
c [treelook-1] used 1276536 steps
c [treelook-1] 249254 literals remain 10%
c [treelook-1] 245950 variables remain to probed next time 20%
c [decomp-5] removed 203 variables
c [treelook-1] removed 249 variables, found 10503 hbrs
c [basicprobe-1] limit 39695984 based on 4961998 irredundant clauses
c [basicprobe-1-0] 1090583 probes remain 91% after last round
c [basicprobe-1-0] 6402 units = 2673 failed (42%) + 3729 lifted (58%)
c [basicprobe-1-0] removed 11758 variables, found 253105 hbrs
c [unhide-2] limit 310124 based on 4961998 irredundant clauses
c [unhide-2-2] 1206 units, 1316 failed, 16595 tauts, 0 hbrs, 38965 literals
c [elim-2] 1190452 variables 100% will be scheduled this time
c [elim-2] scheduled 1190452 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 1108747 not tried 93% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 81709 = 7% variables out of 1190452 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 4471563 negative 95.1% of 4700497 except 228934 4.9%
c [phase-count-2] 4394328 positive 93.5% of 4700497 except 306169 6.5%
c [phase-2] phase bias: 1171 positive 32%, 2482 negative 68%
c [sort-queue-2] sorted 1094756 enqueued variables after 1006 conflicts
c [score-dist-2] active 13987 (1%), one 0 (0%), zero 1094756 (99%)
c [score-dist-2] max exp 508, different 8 (2%)
c [score-dist-2] median active exp 503, avg 503.2
c [simplification-2] removed 101648 variables 8.4% (1108743 remain 71%)
c [simplification-2] removed 277467 irredundant clauses 5.6% (4700497 remain 75%)
c [simplification-2] maximum reduction of 8% = max (8%, 6%)
c [simplification-2] large reduction 8% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13006 (soft 3006 + delta 10000)
c [simplification-2] new conflict limit 3006 (hard 13006)
c 
c [simplification-3] limit of 183 binary hit after 183 binaries
c [card-2] limit 1175124 based on 4700497 irredundant clauses
c [card-2] found 1114 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1175124 for elimination
c [card-2] 1114 out of 1114 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 6871 variables
c [treelook-2] limit 1172441 based on 4689766 irredundant clauses
c [treelook-2] scheduled 221394 literals 10%
c [treelook-2] scheduling used 1173025 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1172441 based on 4689766 irredundant clauses
c [treelook-2] used 1191935 steps
c [treelook-2] 221102 literals remain 10%
c [treelook-2] 137652 variables remain to probed next time 12%
c [decomp-7] removed 169 variables
c [treelook-2] removed 180 variables, found 3781 hbrs
c [unhide-3] limit 293074 based on 4689186 irredundant clauses
c [unhide-3-3] 551 units, 881 failed, 18458 tauts, 0 hbrs, 20755 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 1100115 variables 100%
c [elim-3] limit of 12974601 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 901426 not tried 82% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 198689 = 18% variables out of 1100115 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 4023403 negative 95.0% of 4237328 except 213925 5.0%
c [phase-count-3] 3942161 positive 93.0% of 4237328 except 295167 7.0%
c [phase-3] phase bias: 973 positive 28%, 2490 negative 72%
c [sort-queue-3] sorted 874850 enqueued variables after 2274 conflicts
c [score-dist-3] active 26576 (3%), one 0 (0%), zero 874850 (97%)
c [score-dist-3] max exp 508, different 8 (2%)
c [score-dist-3] median active exp 503, avg 503.2
c [simplification-3] removed 207317 variables 18.7% (901426 remain 57%)
c [simplification-3] removed 463169 irredundant clauses 9.9% (4237328 remain 67%)
c [simplification-3] maximum reduction of 19% = max (19%, 10%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 3006 (hard 13006)
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   86.5  901425  4237328      2876    1529    264 177982    4    77  276   5%     22   75   13    0 4255%
c i   87.2  901269  4237328      2972    1605    272 177987    4    78  276   5%     20   76   11    0 3455%
c 
c [simplification-4] limit 3006 conflicts (hard 13006) hit after 3007 conflicts
c [decomp-8] removed 1343 variables
c [basicprobe-2] limit 33870352 based on 4233794 irredundant clauses
c [basicprobe-2-0] 693596 probes remain 77% after last round
c [basicprobe-2-0] 1817 units = 1605 failed (88%) + 212 lifted (12%)
c [basicprobe-2-0] removed 4104 variables, found 168169 hbrs
c [unhide-4] limit 264612 based on 4233794 irredundant clauses
c [unhide-4-4] 295 units, 619 failed, 16250 tauts, 0 hbrs, 55867 literals
c [elim-4] 895170 variables 100% will be scheduled this time
c [elim-4] scheduled 895170 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 332137220 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 19753 not tried 2% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 479957 = 54% variables out of 895170 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 2812956 negative 95.6% of 2942937 except 129981 4.4%
c [phase-count-4] 2759550 positive 93.8% of 2942937 except 183387 6.2%
c [phase-4] phase bias: 3483 positive 41%, 4952 negative 59%
c [sort-queue-4] sorted 396384 enqueued variables after 3007 conflicts
c [score-dist-4] active 18829 (5%), one 0 (0%), zero 396384 (95%)
c [score-dist-4] max exp 509, different 9 (2%)
c [score-dist-4] median active exp 503, avg 503.6
c [simplification-4] removed 486056 variables 53.9% (415213 remain 26%)
c [simplification-4] removed 1294391 irredundant clauses 30.5% (2942937 remain 47%)
c [simplification-4] maximum reduction of 54% = max (54%, 31%)
c [simplification-4] large reduction 54% >= 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 15007 (soft 5007 + delta 10000)
c [simplification-4] new conflict limit 5007 (hard 15007)
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.7  415212  2942937      3139     615    163 89942    4    81  246   5%     17   79   13    0 3663%
c i  124.0  415211  2942937      4703    1937    208 89978   11    78  246  15%     15   74   33    1 3480%
c 
c [simplification-5] limit 5007 conflicts (hard 15007) hit after 5007 conflicts
c [quatres-1] found 363920 quaternary clauses 39% in total
c [quatres-1-1] removed 5 duplicate quaternary clauses
c [quatres-1-1] added 124 double-self-subsuming ternary resolvents
c [quatres-1-2] added 4081 single-self-subsuming ternary resolvents
c [quatres-1-2] added 12132 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 11770384 based on 2942596 irredundant clauses
c [ternres-1] all 415204 free variables schedulable
c [ternres-1] 56510 ternary resolvents (276 bin, 56234 trn)
c [ternres-1] 293402 variables remain 71% (121802 retained 29%)
c [gauss-1] limit 1471298 based on 2942596 irredundant clauses
c [gauss-1] extracted 6779 xors of average arity 3.0
c [gauss-1] connected 20138 occurrences of 7696 variables (average 2.6)
c [gauss-1] limit 1471148 based on 2942296 irredundant clauses
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 2075 variables
c [simpleprobe-3] 402537 schedulable variables 97%
c [simpleprobe-3] limit 8969747 penalty 1 = 0 + 1
c [decomp-10] removed 228 variables
c [simpleprobe-3] 402721 variables remain 98% (10180 retained 2%)
c [simpleprobe-3] removed 228 variables, found 21346 hbrs, 32 units
c [unhide-5] limit 183570 based on 2937133 irredundant clauses
c [unhide-5-5] 223 units, 310 failed, 87956 tauts, 0 hbrs, 115947 literals
c [transred-1] limit 2866978 based on 2866978 irredundant clauses
c [transred-1] removed 1167 transitive binary clauses
c [transred-1] found 15 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 412393 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 250000000 steps penalty 1 = 0 + 1
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 31392 blocked clauses
c [cce-1] limit of 15000000 steps penalty 1 = 0 + 1
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 46
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 36
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 32
c [cce-1-1] eliminated 10 clauses out of 10 (100%) of length 31
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 30
c [cce-1-1] eliminated 2 clauses out of 7 (29%) of length 29
c [cce-1-1] eliminated 3 clauses out of 7 (43%) of length 28
c [cce-1-1] eliminated 3 clauses out of 8 (38%) of length 27
c [cce-1-1] eliminated 6 clauses out of 12 (50%) of length 26
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 25
c [cce-1-1] eliminated 7 clauses out of 14 (50%) of length 24
c [cce-1-1] eliminated 6 clauses out of 10 (60%) of length 23
c [cce-1-1] eliminated 3 clauses out of 10 (30%) of length 22
c [cce-1-1] eliminated 2 clauses out of 16 (12%) of length 21
c [cce-1-1] eliminated 14 clauses out of 32 (44%) of length 19
c [cce-1-1] eliminated 352 clauses out of 1340 (26%) of length 18
c [cce-1-1] eliminated 102 clauses out of 1596 (6%) of length 17
c [cce-1-1] eliminated 213 clauses out of 1079 (20%) of length 16
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 729 large clauses in 15000140 steps
c [cce-1-1] allowing another 7500070 steps for small clauses
c [cce-1-1] scheduling 1616313 clauses = 1264971 binary + 351342 ternary
c [cce-1-1] tried to eliminate 2366 small clauses 0%
c [cce-1-1] eliminated 508 binary clauses 0%
c [cce-1-1] eliminated 102 ternary clauses 0%
c [cce-1-1] eliminated 610 small clauses 0%
c [cce-1-1] eliminated 610 small clauses in 15000004 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1339 covered clauses in round 1
c [cce-1] eliminated 1339 covered clauses in TOTAL during 1 rounds
c [cce-1] 1339 < 1/100 * 2829891 = 28298 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 411730 variables 100%
c [elim-5] limit of 44848736 steps penalty 1 = 0 + 1
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 214648 not tried 52% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 20079 = 5% variables out of 411730 scheduled
c [bca-1] limit of 10000000 steps and 5576232 added (scaled 2)
c [bca-1] 751777 out of 783304 literals actually usable 96%
c [bca-1] added 10198 blocked clauses in 2395784 steps
c [sweep-1] limit 5575732 based on 2787866 irredundant clauses
c [sweep-1-1] 134328 pos 34.3% + 257323 neg 65.7% = 391651 sched 100.0% ret 0
c [sweep-1-1] 5603955 steps 87 queries 121429.84 avg class size
c [sweep-1-1] 1158 decisions 82 SAT calls 34.74 avg env size
c [sweep-1-1] 390825 variables remain 100% (822 retained 0%)
c [decomp-11] removed 463 variables
c [sweep-1-1] removed 463 vars (0 failed, 15 eqs, 19 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 463 vars in TOTAL (1 rounds, 86 queries)
c [phase-count-5] 2663473 negative 95.6% of 2786704 except 123231 4.4%
c [phase-count-5] 2634948 positive 94.6% of 2786704 except 151756 5.4%
c [phase-5] phase bias: 1372 positive 55%, 1144 negative 45%
c [sort-queue-5] sorted 368311 enqueued variables after 5007 conflicts
c [score-dist-5] active 22877 (6%), one 0 (0%), zero 368311 (94%)
c [score-dist-5] max exp 511, different 11 (2%)
c [score-dist-5] median active exp 504, avg 504.3
c [simplification-5] removed 24016 variables 5.8% (391188 remain 25%)
c [simplification-5] removed 156233 irredundant clauses 5.3% (2786704 remain 44%)
c [simplification-5] maximum reduction of 6% = max (6%, 5%)
c [simplification-5] large reduction 6% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 17007 (soft 7007 + delta 10000)
c [simplification-5] new conflict limit 7007 (hard 17007)
c 
c [simplification-6] limit 7007 conflicts (hard 17007) hit after 7007 conflicts
c [quatres-2] found 374086 quaternary clauses 40% in total
c [quatres-2-1] removed 20 duplicate quaternary clauses
c [quatres-2-1] added 37 double-self-subsuming ternary resolvents
c [quatres-2-2] added 2160 single-self-subsuming ternary resolvents
c [quatres-2-2] added 9265 quaternary resolvents
c [ternres-2] limit 11146020 based on 2786505 irredundant clauses
c [ternres-2] 276260 schedulable variables 71%
c [ternres-2] 48171 ternary resolvents (1061 bin, 47110 trn)
c [ternres-2] 174145 variables remain 45% (217043 retained 55%)
c [card-3] limit 696626 based on 2786505 irredundant clauses
c [card-3] found 314 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 696626 for elimination
c [card-3] 314 out of 314 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 374 variables
c [treelook-3] limit 696513 based on 2786053 irredundant clauses
c [treelook-3] scheduled 82308 literals 11%
c [treelook-3] scheduling used 696617 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 696513 based on 2786053 irredundant clauses
c [treelook-3] used 716115 steps
c [treelook-3] 82248 literals remain 11%
c [treelook-3] 49766 variables remain to probed next time 13%
c [decomp-13] removed 3 variables
c [treelook-3] removed 7 variables, found 850 hbrs
c [unhide-6] limit 174125 based on 2786010 irredundant clauses
c [unhide-6-6] 298 units, 657 failed, 6490 tauts, 0 hbrs, 62069 literals
c [transred-2] limit 2782970 based on 2782970 irredundant clauses
c [transred-2] removed 1012 transitive binary clauses
c [transred-2] found 14 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 389974 variables 100%
c [block-2] limit of 32511067 steps penalty 1 = 0 + 1
c [block-2] incomplete 1078 not tried 0%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 9643 blocked clauses
c [block-2] 9643 < 1/100 * 2782226 = 27822 considered unsuccessful
c [elim-6] 19451 variables 5% will be scheduled this time
c [elim-6] scheduled 19451 variables 5%
c [elim-6] limit of 65022135 steps penalty 1 = 0 + 1
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 9082 not tried 2% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 93 = 0% variables out of 19451 scheduled
c [elim-6] 93 < 1/100 * 19451 = 194 considered unsuccessful
c [bca-2] limit of 10000000 steps and 5472847 added (scaled 2)
c [bca-2] 730575 out of 779554 literals actually usable 94%
c [bca-2] added 998 blocked clauses in 2305292 steps
c [sweep-2] limit 5467248 based on 2733624 irredundant clauses
c [sweep-2-1] 137029 pos 35.2% + 251947 neg 64.8% = 388976 sched 99.8% ret 800
c [sweep-2-1] 5518849 steps 104 queries 119585.26 avg class size
c [sweep-2-1] 1436 decisions 95 SAT calls 38.31 avg env size
c [sweep-2-1] 388313 variables remain 100% (1463 retained 0%)
c [decomp-14] removed 713 variables
c [sweep-2-1] removed 713 vars (0 failed, 13 eqs, 23 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 713 vars in TOTAL (1 rounds, 103 queries)
c [phase-count-6] 2609430 negative 95.5% of 2731970 except 122540 4.5%
c [phase-count-6] 2580755 positive 94.5% of 2731970 except 151215 5.5%
c [phase-6] phase bias: 679 positive 61%, 441 negative 39%
c [sort-queue-6] sorted 356927 enqueued variables after 7007 conflicts
c [score-dist-6] active 32136 (8%), one 0 (0%), zero 356927 (92%)
c [score-dist-6] max exp 511, different 11 (2%)
c [score-dist-6] median active exp 504, avg 504.9
c [simplification-6] removed 2125 variables 0.5% (389063 remain 25%)
c [simplification-6] removed 54733 irredundant clauses 2.0% (2731970 remain 43%)
c [simplification-6] maximum reduction of 2% = max (1%, 2%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 6666
c [simplification-6] penalized conflict interval 6666 = 1 * 6666
c [simplification-6] hard conflict limit 23673 (soft 13673 + delta 10000)
c [simplification-6] new conflict limit 13673 (hard 23673)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  193.3  389062  2731970      8171   22699  85679 111236   16   164  248  10%     38  154   11    2  552%
c i  238.2  389061  2731960     12850   26455  85876 111330   37   261  251  14%     54  235   19    5  397%
c i  240.2  389060  2731960     13457   26942  85932 111367   33   271  252  12%     30  242   11    5  220%
c 
c [simplification-7] limit 13673 conflicts (hard 23673) hit after 13674 conflicts
c [quatres-3] found 373596 quaternary clauses 42% in total
c [quatres-3-1] removed 14 duplicate quaternary clauses
c [quatres-3-1] added 22 double-self-subsuming ternary resolvents
c [quatres-3-2] added 903 single-self-subsuming ternary resolvents
c [quatres-3-2] added 5789 quaternary resolvents
c [ternres-3] limit 10927620 based on 2731905 irredundant clauses
c [ternres-3] 173036 schedulable variables 44%
c [ternres-3] 50177 ternary resolvents (1721 bin, 48456 trn)
c [ternres-3] 98443 variables remain 25% (290617 retained 75%)
c [gauss-2] limit 1365952 based on 2731905 irredundant clauses
c [gauss-2] extracted 5517 xors of average arity 3.0
c [gauss-2] connected 16482 occurrences of 6577 variables (average 2.5)
c [gauss-2] limit 1365940 based on 2731880 irredundant clauses
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 510 variables
c [basicprobe-3] limit 42728521 penalty 1 = 0 + 1
c [basicprobe-3-0] 231046 probes remain 60% after last round
c [basicprobe-3-0] 3438 units = 3224 failed (94%) + 214 lifted (6%)
c [basicprobe-3-0] removed 4994 variables, found 189927 hbrs
c [bate-1] eliminated 3866 asymmetric tautologies during probing
c [unhide-7] limit 427285 with penalty 3 = 0 + 3
c [unhide-7-7] 204 units, 273 failed, 38308 tauts, 0 hbrs, 35925 literals
c [transred-3] limit 2637597 based on 2637597 irredundant clauses
c [transred-3] removed 1585 transitive binary clauses
c [transred-3] found 11 units
c [cce-2] limit of 21364260 steps penalty 2 = 1 + 1
c [cce-2-1] eliminated 2 clauses out of 6 (33%) of length 23
c [cce-2-1] eliminated 1 clauses out of 8 (12%) of length 20
c [cce-2-1] eliminated 2 clauses out of 19 (11%) of length 19
c [cce-2-1] eliminated 287 clauses out of 1227 (23%) of length 18
c [cce-2-1] eliminated 295 clauses out of 1561 (19%) of length 17
c [cce-2-1] eliminated 25 clauses out of 1020 (2%) of length 16
c [cce-2-1] eliminated 229 clauses out of 2164 (11%) of length 15
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 841 large clauses in 21364328 steps
c [cce-2-1] allowing another 10682164 steps for small clauses
c [cce-2-1] scheduling 1456495 clauses = 1141886 binary + 314609 ternary
c [cce-2-1] tried to eliminate 4549 small clauses 0%
c [cce-2-1] eliminated 620 binary clauses 0%
c [cce-2-1] eliminated 207 ternary clauses 0%
c [cce-2-1] eliminated 827 small clauses 0%
c [cce-2-1] eliminated 6395 small clauses in 21364266 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 7236 covered clauses in round 1
c [cce-2] eliminated 7236 covered clauses in TOTAL during 1 rounds
c [cce-2] 7236 < 1/100 * 2636998 = 26369 considered unsuccessful
c [bca-3] limit of 10000000 steps and 5265622 added (scaled 2)
c [bca-3] 702480 out of 765890 literals actually usable 92%
c [bca-3] added 509 blocked clauses in 2145160 steps
c [sweep-3] limit 5259524 based on 2629762 irredundant clauses
c [sweep-3-1] 151219 pos 39.6% + 230301 neg 60.4% = 381520 sched 99.6% ret 1424
c [sweep-3-1] 5287211 steps 98 queries 124818.21 avg class size
c [sweep-3-1] 1051 decisions 83 SAT calls 34.61 avg env size
c [sweep-3-1] 381256 variables remain 100% (1683 retained 0%)
c [decomp-16] removed 4994 variables
c [sweep-3-1] removed 4994 vars (0 failed, 36 eqs, 40 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 4994 vars in TOTAL (1 rounds, 97 queries)
c [phase-count-7] 2498239 negative 95.3% of 2621943 except 123704 4.7%
c [phase-count-7] 2476539 positive 94.5% of 2621943 except 145404 5.5%
c [phase-7] phase bias: 162 positive 53%, 146 negative 47%
c [sort-queue-7] sorted 320402 enqueued variables after 13674 conflicts
c [score-dist-7] active 57548 (15%), one 0 (0%), zero 320402 (85%)
c [score-dist-7] max exp 512, different 12 (2%)
c [score-dist-7] median active exp 505, avg 505.7
c [simplification-7] removed 11110 variables 2.9% (377950 remain 24%)
c [simplification-7] removed 110017 irredundant clauses 4.0% (2621943 remain 42%)
c [simplification-7] maximum reduction of 4% = max (3%, 4%)
c [simplification-7] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-7] new conflict interval 10666
c [simplification-7] penalized conflict interval 10666 = 1 * 10666
c [simplification-7] hard conflict limit 34340 (soft 24340 + delta 10000)
c [simplification-7] new conflict limit 24340 (hard 34340)
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  263.1  377949  2621942     14884   32838 116337 225509   28   252  249  11%     14  218   15    5  298%
c i  263.5  377948  2621942     15095   33027 116347 225513   28   245  249  11%     11  211   21    5  407%
c i  266.1  377947  2621942     16145   33964 116388 225542   25   218  249  12%      7  181   15    5  280%
c i  266.2  377946  2621942     16149   33966 116388 225542   25   218  249  12%      7  181   15    5  278%
c i  267.4  377945  2621942     16418   34189 116399 225557   25   212  249  12%      5  174   16    5  305%
c i  270.2  377944  2621941     17445   35128 116439 225568   23   185  249  13%      5  145   13    5  246%
c i  274.3  377943  2621941     18232   35792 116471 225613   21   187  250  11%      3  145   11    6  195%
c i  282.3  377942  2621933     21179   38364 116586 225691   16   138  250  11%     26   91    9    6  154%
c i  282.5  377864  2621933     21236   38409 116590 225694   16   137  250  11%     24   90    9    6  158%
c i  282.5  377842  2621933     21237   38409 116590 225694   16   137  250  11%     24   90    9    6  158%
c 
c [simplification-8] limit of 26 iterations hit after 26 iterations
c [quatres-4] found 367611 quaternary clauses 42% in total
c [quatres-4-1] removed 39 duplicate quaternary clauses
c [quatres-4-1] added 55 double-self-subsuming ternary resolvents
c [quatres-4-2] added 986 single-self-subsuming ternary resolvents
c [quatres-4-2] added 3511 quaternary resolvents
c [ternres-4] limit 10712068 with penalty 1 = 0 + 1
c [ternres-4] 95423 schedulable variables 25%
c [ternres-4] 38324 ternary resolvents (1766 bin, 36558 trn)
c [ternres-4] 64059 variables remain 17% (313675 retained 83%)
c [decomp-17] removed 727 variables
c [simpleprobe-4] 367910 schedulable variables 98%
c [simpleprobe-4] limit 42848273 penalty 1 = 0 + 1
c [decomp-18] removed 2737 variables
c [simpleprobe-4] 253226 variables remain 68% (121260 retained 32%)
c [simpleprobe-4] removed 2737 variables, found 89950 hbrs, 532 units
c [unhide-8] limit 535603 with penalty 3 = 0 + 3
c [unhide-8-8] 213 units, 431 failed, 29874 tauts, 0 hbrs, 44495 literals
c [transred-4] limit 2597248 based on 2597248 irredundant clauses
c [transred-4] removed 1103 transitive binary clauses
c [transred-4] found 11 units
c [block-3] 1072 variables 0% will be scheduled this time
c [block-3] scheduled 1072 variables 0%
c [block-3] limit of 53560341 steps penalty 2 = 1 + 1
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 373874 variables 100%
c [elim-7] limit of 107120682 steps penalty 2 = 1 + 1
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 62741 not tried 17% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 17753 = 5% variables out of 373874 scheduled
c [bca-4] limit of 10000000 steps and 5073582 added (scaled 2)
c [bca-4] 648086 out of 712244 literals actually usable 91%
c [bca-4] added 820 blocked clauses in 2014379 steps
c [sweep-4] limit 5067230 based on 2533615 irredundant clauses
c [sweep-4-1] 140902 pos 39.7% + 213739 neg 60.3% = 354641 sched 99.6% ret 1480
c [sweep-4-1] 5071588 steps 93 queries 107803.48 avg class size
c [sweep-4-1] 1661 decisions 86 SAT calls 41.47 avg env size
c [sweep-4-1] 354071 variables remain 99% (2048 retained 1%)
c [decomp-19] removed 640 variables
c [sweep-4-1] removed 640 vars (0 failed, 13 eqs, 17 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 640 vars in TOTAL (1 rounds, 92 queries)
c [phase-count-8] 2411003 negative 95.2% of 2531554 except 120551 4.8%
c [phase-count-8] 2391457 positive 94.5% of 2531554 except 140097 5.5%
c [phase-8] phase bias: 156 positive 46%, 183 negative 54%
c [sort-queue-8] sorted 295008 enqueued variables after 21237 conflicts
c [score-dist-8] active 60473 (17%), one 0 (0%), zero 295008 (83%)
c [score-dist-8] max exp 513, different 13 (3%)
c [score-dist-8] median active exp 505, avg 505.7
c [simplification-8] removed 22253 variables 5.9% (355481 remain 23%)
c [simplification-8] removed 90379 irredundant clauses 3.4% (2531554 remain 40%)
c [simplification-8] maximum reduction of 6% = max (6%, 3%)
c [simplification-8] forced so keeping old conflict interval 10666
c [simplification-8] conflict limit remains at 24352 (hard 34340)
c [simplification-8] 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  313.7  355480  2531553     23457   37581 124431 251306   13   106  247  12%     18   57    9    6  148%
c 
c [simplification-9] limit 24352 conflicts (hard 34340) hit after 24353 conflicts
c [quatres-5] found 369500 quaternary clauses 43% in total
c [quatres-5-1] removed 196 duplicate quaternary clauses
c [quatres-5-1] added 27 double-self-subsuming ternary resolvents
c [quatres-5-2] added 1795 single-self-subsuming ternary resolvents
c [quatres-5-2] added 4624 quaternary resolvents
c [ternres-5] limit 11497300 with penalty 1 = 0 + 1
c [ternres-5] 60174 schedulable variables 17%
c [ternres-5] 54943 ternary resolvents (2231 bin, 52712 trn)
c [ternres-5] 22603 variables remain 6% (332877 retained 94%)
c [decomp-20] removed 599 variables
c [treelook-4] limit 1149730 penalty 1 = 0 + 1 boost 1
c [treelook-4] scheduled 109204 literals 15%
c [treelook-4] scheduling used 1150267 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 1149730 penalty 1 = 0 + 1 boost 1
c [treelook-4] used 1174766 steps
c [treelook-4] 109076 literals remain 15%
c [treelook-4] 41981 variables remain to probed next time 12%
c [decomp-21] removed 9 variables
c [treelook-4] removed 21 variables, found 1449 hbrs
c [unhide-9] limit 574865 with penalty 3 = 0 + 3
c [unhide-9-9] 57 units, 162 failed, 27267 tauts, 0 hbrs, 24103 literals
c [transred-5] limit 2508435 based on 2508435 irredundant clauses
c [transred-5] removed 1185 transitive binary clauses
c [transred-5] found 12 units
c [elim-8] 8933 variables 3% will be scheduled this time
c [elim-8] scheduled 8933 variables 3%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4598920070 steps penalty 1 = 0 + 1
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 697294040 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 65 = 1% variables out of 8933 scheduled
c [elim-8] 65 < 1/100 * 8933 = 89 considered unsuccessful
c [bca-5] limit of 10000000 steps and 4979806 added (scaled 2)
c [bca-5] 639318 out of 709064 literals actually usable 90%
c [bca-5] added 753 blocked clauses in 1987489 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 34491900 penalty 1 = 0 + 1
c [sweep-5-1] 139064 pos 39.5% + 213440 neg 60.5% = 352504 sched 99.4% ret 2027
c [sweep-5-1] 34567617 steps 643 queries 69137.68 avg class size
c [sweep-5-1] 8892 decisions 613 SAT calls 37.01 avg env size
c [sweep-5-1] 347703 variables remain 98% (6795 retained 2%)
c [decomp-22] removed 767 variables
c [sweep-5-1] removed 767 vars (0 failed, 127 eqs, 151 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 767 vars in TOTAL (1 rounds, 642 queries)
c [phase-count-9] 2364238 negative 95.2% of 2484470 except 120232 4.8%
c [phase-count-9] 2345190 positive 94.4% of 2484470 except 139280 5.6%
c [phase-9] phase bias: 49 positive 49%, 50 negative 51%
c [sort-queue-9] sorted 291454 enqueued variables after 24353 conflicts
c [score-dist-9] active 62310 (18%), one 0 (0%), zero 291454 (82%)
c [score-dist-9] max exp 514, different 14 (3%)
c [score-dist-9] median active exp 505, avg 505.7
c [simplification-9] removed 1716 variables 0.5% (353764 remain 23%)
c [simplification-9] removed 47083 irredundant clauses 1.9% (2484470 remain 39%)
c [simplification-9] maximum reduction of 2% = max (0%, 2%)
c [simplification-9] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-9] new conflict interval 17332
c [simplification-9] penalized conflict interval 17332 = 1 * 17332
c [simplification-9] hard conflict limit 51685 (soft 41685 + delta 10000)
c [simplification-9] new conflict limit 41685 (hard 51685)
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  345.5  353763  2484470     25696   43496 158810 253684   10    71  247  15%     17   20    6    6  103%
c i  350.6  353689  2484470     26553   44272 158836 253702   11    98  248  11%      8   47   12    6  195%
c i  368.5  353688  2484470     28811   46346 158906 253738   16   147  248  11%     16   93   27    7  414%
c 
c [simplification-10] limit 41685 conflicts (hard 51685) hit after 41686 conflicts
c [quatres-6] found 371655 quaternary clauses 44% in total
c [quatres-6-1] removed 43 duplicate quaternary clauses
c [quatres-6-1] added 28 double-self-subsuming ternary resolvents
c [quatres-6-2] added 731 single-self-subsuming ternary resolvents
c [quatres-6-2] added 2434 quaternary resolvents
c [ternres-6] limit 35431619 with penalty 1 = 0 + 1
c [ternres-6] 22402 schedulable variables 6%
c [ternres-6] 103631 ternary resolvents (3092 bin, 100539 trn)
c [ternres-6] 299 variables remain 0% (353386 retained 100%)
c [card-4] limit 2214476 penalty 4 = 3 + 1
c [card-4] found 1150 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2214476 for elimination
c [card-4] 1150 out of 1150 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1771580 penalty 3 = 2 + 1
c [gauss-3] extracted 5708 xors of average arity 3.0
c [gauss-3] connected 16979 occurrences of 6702 variables (average 2.5)
c [gauss-3] limit 1771580 penalty 3 = 2 + 1
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 822 variables
c [basicprobe-4] limit 177158095 penalty 1 = 0 + 1
c [basicprobe-4-0] 19585 probes remain 6% after last round
c [basicprobe-4-0] 11243 units = 10636 failed (95%) + 607 lifted (5%)
c [basicprobe-4-0] removed 16579 variables, found 424585 hbrs
c [bate-2] eliminated 8604 asymmetric tautologies during probing
c [unhide-10] limit 1771580 with penalty 3 = 0 + 3
c [unhide-10-10] 122 units, 129 failed, 86607 tauts, 0 hbrs, 66525 literals
c [transred-6] limit 2291480 based on 2291480 irredundant clauses
c [transred-6] removed 2337 transitive binary clauses
c [transred-6] found 2 units
c [cce-3] limit of 44289523 steps penalty 3 = 2 + 1
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 25
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 20
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 19
c [cce-3-1] eliminated 28 clauses out of 856 (3%) of length 18
c [cce-3-1] eliminated 49 clauses out of 722 (7%) of length 17
c [cce-3-1] eliminated 47 clauses out of 566 (8%) of length 16
c [cce-3-1] eliminated 39 clauses out of 1308 (3%) of length 15
c [cce-3-1] eliminated 462 clauses out of 1969 (23%) of length 14
c [cce-3-1] eliminated 1907 clauses out of 4559 (42%) of length 13
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 2539 large clauses in 44289596 steps
c [cce-3-1] allowing another 22144798 steps for small clauses
c [cce-3-1] scheduling 1245667 clauses = 965850 binary + 279817 ternary
c [cce-3-1] tried to eliminate 8126 small clauses 1%
c [cce-3-1] eliminated 1889 binary clauses 0%
c [cce-3-1] eliminated 452 ternary clauses 0%
c [cce-3-1] eliminated 2341 small clauses 0%
c [cce-3-1] eliminated 4301 small clauses in 44289531 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 6840 covered clauses in round 1
c [cce-3] eliminated 6840 covered clauses in TOTAL during 1 rounds
c [cce-3] 6840 < 1/100 * 2290714 = 22907 considered unsuccessful
c [bca-6] limit of 10000000 steps and 4574887 added (scaled 2)
c [bca-6] 600549 out of 672074 literals actually usable 89%
c [bca-6] added 911 blocked clauses in 1802422 steps
c [sweep-6] limit 10629485 penalty 1 = 0 + 1
c [sweep-6-1] 128754 pos 39.0% + 201060 neg 61.0% = 329814 sched 98.1% ret 6222
c [sweep-6-1] 10633424 steps 224 queries 91570.50 avg class size
c [sweep-6-1] 3045 decisions 210 SAT calls 33.29 avg env size
c [sweep-6-1] 328228 variables remain 98% (7798 retained 2%)
c [decomp-24] removed 10631 variables
c [sweep-6-1] removed 10631 vars (0 failed, 44 eqs, 34 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 10631 vars in TOTAL (1 rounds, 223 queries)
c [phase-count-10] 2143267 negative 94.7% of 2262191 except 118924 5.3%
c [phase-count-10] 2123632 positive 93.9% of 2262191 except 138559 6.1%
c [phase-10] phase bias: 199 positive 66%, 104 negative 34%
c [sort-queue-10] sorted 259846 enqueued variables after 41686 conflicts
c [score-dist-10] active 65559 (20%), one 0 (0%), zero 259846 (80%)
c [score-dist-10] max exp 515, different 15 (3%)
c [score-dist-10] median active exp 506, avg 506.8
c [simplification-10] removed 28280 variables 8.0% (325405 remain 21%)
c [simplification-10] removed 222279 irredundant clauses 8.9% (2262191 remain 36%)
c [simplification-10] maximum reduction of 9% = max (8%, 9%)
c [simplification-10] large reduction 9% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 53686 (soft 43686 + delta 10000)
c [simplification-10] new conflict limit 43686 (hard 53686)
c 
c [simplification-11] limit 43686 conflicts (hard 53686) hit after 43688 conflicts
c [quatres-7] found 351791 quaternary clauses 45% in total
c [quatres-7-1] removed 317 duplicate quaternary clauses
c [quatres-7-1] added 87 double-self-subsuming ternary resolvents
c [quatres-7-2] added 1581 single-self-subsuming ternary resolvents
c [quatres-7-2] added 3129 quaternary resolvents
c [ternres-7] limit 36365361 with penalty 1 = 0 + 1
c [ternres-7] 269 schedulable variables 0%
c [ternres-7] 95172 ternary resolvents (2569 bin, 92603 trn)
c [ternres-7] 12 variables remain 0% (325393 retained 100%)
c [decomp-25] removed 725 variables
c [simpleprobe-5] 217671 schedulable variables 67%
c [simpleprobe-5] limit 100000000 penalty 1 = 0 + 1
c [decomp-26] removed 4209 variables
c [simpleprobe-5] 137792 variables remain 43% (182679 retained 57%)
c [simpleprobe-5] removed 4209 variables, found 156532 hbrs, 285 units
c [unhide-11] limit 1818268 with penalty 3 = 0 + 3
c [unhide-11-11] 47 units, 102 failed, 26184 tauts, 0 hbrs, 24078 literals
c [transred-7] limit 2211294 based on 2211294 irredundant clauses
c [transred-7] removed 2145 transitive binary clauses
c [transred-7] found 4 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 320310 variables 100%
c [block-4] limit of 90913404 steps penalty 3 = 2 + 1
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 24773 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 319593 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 8256 not tried 3% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 21875 = 7% variables out of 319593 scheduled
c [bca-7] limit of 10000000 steps and 4212270 added (scaled 2)
c [bca-7] 527483 out of 595438 literals actually usable 89%
c [bca-7] added 2746 blocked clauses in 1660392 steps
c [sweep-7] limit 10909608 penalty 1 = 0 + 1
c [sweep-7-1] 111288 pos 38.3% + 179453 neg 61.7% = 290741 sched 97.7% ret 6977
c [sweep-7-1] 10922216 steps 246 queries 71387.78 avg class size
c [sweep-7-1] 3830 decisions 236 SAT calls 42.32 avg env size
c [sweep-7-1] 288572 variables remain 97% (9119 retained 3%)
c [decomp-27] removed 594 variables
c [sweep-7-1] removed 594 vars (0 failed, 26 eqs, 35 impls)
c [sweep-7] removed 594 vars in TOTAL (1 rounds, 245 queries)
c [phase-count-11] 1993899 negative 94.9% of 2100444 except 106545 5.1%
c [phase-count-11] 1971305 positive 93.9% of 2100444 except 129139 6.1%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 108 positive 45%, 130 negative 55%
c [sort-queue-11] sorted 234720 enqueued variables after 43688 conflicts
c [score-dist-11] active 62404 (21%), one 0 (0%), zero 234720 (79%)
c [score-dist-11] max exp 515, different 15 (3%)
c [score-dist-11] median active exp 506, avg 506.8
c [simplification-11] removed 28281 variables 8.7% (297124 remain 19%)
c [simplification-11] removed 161747 irredundant clauses 7.2% (2100444 remain 33%)
c [simplification-11] maximum reduction of 9% = max (9%, 7%)
c [simplification-11] large reduction 9% >= 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 55688 (soft 45688 + delta 10000)
c [simplification-11] new conflict limit 45688 (hard 55688)
c 
c [simplification-12] limit 45688 conflicts (hard 55688) hit after 45688 conflicts
c [quatres-8] found 346696 quaternary clauses 46% in total
c [quatres-8-1] removed 760 duplicate quaternary clauses
c [quatres-8-1] added 34 double-self-subsuming ternary resolvents
c [quatres-8-2] added 934 single-self-subsuming ternary resolvents
c [quatres-8-2] added 5207 quaternary resolvents
c [ternres-8] limit 36787556 with penalty 1 = 0 + 1
c [ternres-8] 11 schedulable variables 0%
c [ternres-8] 35135 ternary resolvents (543 bin, 34592 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-28] removed 106 variables
c [treelook-5] limit 3678755 penalty 1 = 0 + 1 boost 1
c [treelook-5] scheduled 196482 literals 33%
c [treelook-5] scheduling used 3678760 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 3678755 penalty 1 = 0 + 1 boost 1
c [treelook-5] used 3720544 steps
c [treelook-5] 196029 literals remain 33%
c [treelook-5] 32940 variables remain to probed next time 11%
c [decomp-29] removed 29 variables
c [treelook-5] removed 45 variables, found 4983 hbrs
c [unhide-12] limit 1839377 with penalty 3 = 0 + 3
c [unhide-12-12] 106 units, 261 failed, 50344 tauts, 0 hbrs, 33341 literals
c [transred-8] limit 2098738 based on 2098738 irredundant clauses
c [transred-8] removed 1767 transitive binary clauses
c [transred-8] found 9 units
c [elim-10] 8241 variables 3% will be scheduled this time
c [elim-10] scheduled 8241 variables 3%
c [elim-10] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 614 not tried 0% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 112 = 1% variables out of 8241 scheduled
c [elim-10] 112 < 1/100 * 8241 = 82 considered unsuccessful
c [bca-8] limit of 10000000 steps and 4181021 added (scaled 2)
c [bca-8] 520309 out of 593166 literals actually usable 88%
c [bca-8] added 698 blocked clauses in 1630395 steps
c [sweep-8] limit 11036267 penalty 1 = 0 + 1
c [sweep-8-1] 109958 pos 38.2% + 177561 neg 61.8% = 287519 sched 96.9% ret 9063
c [sweep-8-1] 11046809 steps 227 queries 68779.33 avg class size
c [sweep-8-1] 3492 decisions 214 SAT calls 41.59 avg env size
c [sweep-8-1] 285411 variables remain 96% (11164 retained 4%)
c [decomp-30] removed 801 variables
c [sweep-8-1] removed 801 vars (0 failed, 41 eqs, 38 impls)
c [sweep-8] removed 801 vars in TOTAL (1 rounds, 226 queries)
c [phase-count-12] 1977512 negative 94.9% of 2084043 except 106531 5.1%
c [phase-count-12] 1954282 positive 93.8% of 2084043 except 129761 6.2%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 47 positive 60%, 31 negative 40%
c [sort-queue-12] sorted 232736 enqueued variables after 45688 conflicts
c [score-dist-12] active 63045 (21%), one 0 (0%), zero 232736 (79%)
c [score-dist-12] max exp 515, different 15 (3%)
c [score-dist-12] median active exp 506, avg 506.8
c [simplification-12] removed 1343 variables 0.5% (295781 remain 19%)
c [simplification-12] removed 16401 irredundant clauses 0.8% (2084043 remain 33%)
c [simplification-12] maximum reduction of 1% = max (0%, 1%)
c [simplification-12] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-12] new conflict interval 27332
c [simplification-12] penalized conflict interval 27332 = 1 * 27332
c [simplification-12] hard conflict limit 86686 (soft 73020 + delta 13666)
c [simplification-12] new conflict limit 73020 (hard 86686)
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  683.9  295780  2084043     47853   54402 183860 420979   42   128  238  33%    241   59    9   22   43%
c i  684.0  295779  2084043     47888   54432 183863 420979   42   129  238  32%    231   60    9   22   43%
c i  684.1  295778  2084043     47889   54432 183863 420979   42   129  238  32%    231   60    9   22   42%
c i  684.1  295777  2084043     47918   54459 183864 420979   41   131  238  32%    223   62    9   22   44%
c i  684.2  295776  2084043     47943   54480 183867 420979   41   132  238  31%    217   63    9   22   42%
c i  686.2  295775  2084043     48679   55133 183905 420993   36   157  238  23%     86   87   13   21   60%
c i  690.0  295774  2084043     49930   56328 183927 420998   34   175  238  19%      3  104   32   22  149%
c i  690.3  295773  2084043     49986   56381 183927 420998   34   176  238  19%      1  104   34   22  156%
c i  707.7  295772  2084043     53191   59454 183982 421017   35   240  242  15%     -6  162   12   22   52%
c i  758.2  295771  2084043     60163   66026 184059 421036   39   291  249  13%     50  191   33   23  140%
c i  826.2  295770  2084043     66285   71212 184131 421048   68   282  261  24%     36  167   43   28  150%
c i  833.5  295769  2084043     67570   72346 184142 421051   67   283  261  24%    -12  164   84   29  292%
c i  837.5  295768  2084043     68021   72657 184146 421051   72   282  261  26%    -22  163  141   29  479%
c 
c [simplification-13] limit 73030 conflicts (hard 86686) hit after 73030 conflicts
c [quatres-9] found 347490 quaternary clauses 46% in total
c [quatres-9-1] removed 38 duplicate quaternary clauses
c [quatres-9-1] added 32 double-self-subsuming ternary resolvents
c [quatres-9-2] added 274 single-self-subsuming ternary resolvents
c [quatres-9-2] added 1683 quaternary resolvents
c [ternres-9] limit 61505177 with penalty 1 = 0 + 1
c [ternres-9] all 295768 free variables schedulable
c [ternres-9] 51170 ternary resolvents (1285 bin, 49885 trn)
c [ternres-9] 3309 variables remain 1% (292459 retained 99%)
c [decomp-31] removed 212 variables
c [basicprobe-5] limit 200000000 penalty 1 = 0 + 1
c [basicprobe-5-0] 20901 sched 7%, 1091 failed, 82 lifted, 40237 hbrs
c [decomp-32] removed 4187 variables
c [basicprobe-5-1] 25347 probes remain 9% after last round
c [basicprobe-5-1] 5058 units = 4743 failed (94%) + 315 lifted (6%)
c [basicprobe-5-1] removed 19605 variables, found 140831 hbrs
c [bate-3] eliminated 7371 asymmetric tautologies during probing
c [unhide-13] limit 2500000 with penalty 3 = 0 + 3
c [unhide-13-13] 65 units, 141 failed, 24808 tauts, 0 hbrs, 101658 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1928 transitive binary clauses
c [transred-9] found 3 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 275781 variables 100%
c [block-5] limit of 400000000 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 14940 blocked clauses
c [block-5] 14940 < 1/100 * 1904085 = 19040 considered unsuccessful
c [bca-9] limit of 10000000 steps and 3785332 added (scaled 2)
c [bca-9] 474446 out of 550594 literals actually usable 86%
c [bca-9] added 602 blocked clauses in 1478122 steps
c [sweep-9] limit 36903106 penalty 0 = 0 + 0
c [sweep-9-1] 99091 pos 37.4% + 166027 neg 62.6% = 265118 sched 96.3% ret 10178
c [sweep-9-1] 36925739 steps 815 queries 40222.25 avg class size
c [sweep-9-1] 10897 decisions 791 SAT calls 36.23 avg env size
c [sweep-9-1] 256560 variables remain 93% (18688 retained 7%)
c [decomp-33] removed 4550 variables
c [sweep-9-1] removed 4550 vars (0 failed, 128 eqs, 134 impls)
c [sweep-9] removed 4550 vars in TOTAL (1 rounds, 814 queries)
c [phase-count-13] 1778804 negative 94.7% of 1878244 except 99440 5.3%
c [phase-count-13] 1752446 positive 93.3% of 1878244 except 125798 6.7%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 71 positive 65%, 39 negative 35%
c [sort-queue-13] sorted 198264 enqueued variables after 73030 conflicts
c [score-dist-13] active 72482 (27%), one 0 (0%), zero 198264 (73%)
c [score-dist-13] max exp 516, different 16 (3%)
c [score-dist-13] median active exp 508, avg 507.9
c [simplification-13] removed 25022 variables 8.5% (270746 remain 17%)
c [simplification-13] removed 205799 irredundant clauses 9.9% (1878244 remain 30%)
c [simplification-13] maximum reduction of 10% = max (8%, 10%)
c [simplification-13] large reduction 10% >= 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 85030 (soft 75030 + delta 10000)
c [simplification-13] new conflict limit 75030 (hard 85030)
c 
c [simplification-14] limit 75030 conflicts (hard 85030) hit after 75030 conflicts
c [quatres-10] found 315025 quaternary clauses 46% in total
c [quatres-10-1] removed 278 duplicate quaternary clauses
c [quatres-10-1] added 124 double-self-subsuming ternary resolvents
c [quatres-10-2] added 1734 single-self-subsuming ternary resolvents
c [quatres-10-2] added 2679 quaternary resolvents
c [ternres-10] limit 127795779 with penalty 0 = 0 + 0
c [ternres-10] 2690 schedulable variables 1%
c [ternres-10] 66003 ternary resolvents (1741 bin, 64262 trn)
c [ternres-10] 2 variables remain 0% (270744 retained 100%)
c [gauss-4] limit 3194894 penalty 3 = 3 + 0
c [gauss-4] extracted 7547 xors of average arity 3.0
c [gauss-4] connected 22513 occurrences of 8546 variables (average 2.6)
c [gauss-4] limit 3194894 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-34] removed 346 variables
c [simpleprobe-6] 113930 schedulable variables 42%
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-35] removed 6329 variables
c [simpleprobe-6] 60876 variables remain 23% (203195 retained 77%)
c [simpleprobe-6] removed 6329 variables, found 224184 hbrs, 362 units
c [unhide-14] limit 2500000 with penalty 3 = 0 + 3
c [unhide-14-14] 14 units, 81 failed, 96953 tauts, 0 hbrs, 181044 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 2323 transitive binary clauses
c [transred-10] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 798723623 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 2 clauses out of 524 (0%) of length 17
c [cce-4-1] eliminated 7 clauses out of 454 (2%) of length 16
c [cce-4-1] eliminated 12 clauses out of 1561 (1%) of length 15
c [cce-4-1] eliminated 41 clauses out of 1469 (3%) of length 14
c [cce-4-1] eliminated 66 clauses out of 2688 (2%) of length 13
c [cce-4-1] eliminated 1592 clauses out of 6661 (24%) of length 12
c [cce-4-1] eliminated 1178 clauses out of 8288 (14%) of length 11
c [cce-4-1] eliminated 10826 clauses out of 24186 (45%) of length 10
c [cce-4-1] eliminated 5492 clauses out of 17718 (31%) of length 9
c [cce-4-1] eliminated 7363 clauses out of 31070 (24%) of length 8
c [cce-4-1] eliminated 6842 clauses out of 40912 (17%) of length 7
c [cce-4-1] eliminated 10092 clauses out of 68326 (15%) of length 6
c [cce-4-1] eliminated 27886 clauses out of 144625 (19%) of length 5
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 19841 basic ate = 15916 trn 80% + 3925 lrg 20% in 3 updates
c bcas: 9 count, 18235 added (14755 skipped), 17419435 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: 5 bces, 80748 removed, 46801622 resolutions, 122779643 steps
c blkd: 36521 blocking literals 1%, 1970 pure
c bump: 77297 bumped seen, 115446001 lits 1493.5 on average
c card: 4 count, 0 units, 0 am1, 59492468 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 8395 subsumed
c card: 3980 at-most-one constraints found, average size 3.04
c card: 3980 at-most-one constraints used 100%, average size 3.04
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, 83527 eliminated, 82218 ate 98%, 1309 abce 2%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 22314271 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 99 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 35 decompositions, 157668 equivalent 10%
c deco: 7500 decision-only clauses 10%, 74% reduction
c decs: 1879122 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 10 elims, 904356 eliminated 56%, 12220 pure 1%
c elms: 10 rounds, 1.0 rounds/bve
c elms: 786216 small 87%, 103950 large 11%
c elms: 929226 tried small, 786216 succeeded 85%, 143010 failed 15%
c elms: 333693 subsumed, 445438 strengthened, 2521 blocked
c elms: 37138595 copies, 47279152 resolutions, 16248290 ipos
c elms: 25649263 subchks, 48708126 strchks
c gaus: 4 extractions, 25551 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 15610860 steps, 7805430 extr 50%, 7849273 elim 50%
c glue: 54.9 orig avg, 54.9 real avg, 5.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1770551 = 557912 simple 32% + 1206762 trn 68% + 5877 lrg 0%, 42987 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 77297 clauses, 116.0 length
c lrnd: 8965112 lits = 21762105 orig - 12796993 removed 59%
c lrnd: 23743 uips 31%, 32663 flips 42%
c mins: 65861 mins 85%, 1022 bin 1%, 2888 size 4%
c mins: 24536741 poisoned searches, 2943691 hits, 12% hit rate
c mins: 35686940 used twice searches, 1144051 hits, 3% hit rate
c move: moved 120452, 43433 bin 36%, 77019 trn 64%
c otfs: 609 driving 44%, 780 restarting 56%
c otfs: str 1389, 1077 red 78%, 312 irr 22%
c otfs: str 1389, 0 bin 0%, 357 trn 26%, 1032 lrg 74%
c otfs: sub 67, 43 red 64%, 24 irr 36%
c otfs: sub 67, 0 bin 0%, 25 trn 37%, 42 lrg 63%
c phas: 13 computed, 1231453 set, 571245 pos (46%), 660208 neg (54%)
c prbs: 5 basic, 1020135 probed, 22881 failed, 5077 lifted
c prbs: 6 simple, 2911121 probed, 1657 failed, 14931 eqs
c prbs: 5 treelook, 1220 probed, 73 failed, 0 lifted
c prom: 0 locked 0% out of 419094 tried
c prps: 2109224535 props, 1097 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 10 count, 50453 quat, 15179 self1, 570 self2, 3170 dup
c queu: 13 sorted, 1879122 next (115667 steps 0.06)
c queu: 123202212 enq (242104968 steps 1.97), 115446001 deq 94%
c redc: 2793 clauses 18%, 15822 tried 21%, 105 sat 1%
c redc: 5696 lits 4%, 127696 tried 1%, 105 sat 0%
c redc: 576 times jump level reduced, 70.7 levels on average
c reds: 0 count, 0.0 conflicts per reduce
c reds: 0 memlim 0%, 0 arith 0%
c reds: 0 collected 0%, 0 retired 0%
c rmbd: 398176 removed, 267736 red 67%
c rsts: 5477 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 14 count, 12 confs 86%, 0 vars 0%
c simp: 1 its 7%, 1 bin 7%, 0 trns 0%
c subl: 77297 count (144866 tried 1.9), 15134 sub out of 73055 (20.7%)
c swps: 9 count, 9 rounds, 2528 queries (280.9/round)
c swps: 2410 sat calls, 342 unsat (1.2% success rate)
c swps: 35462 decisions 14.7, 2876 conflicts 1.2
c swps; 69692.2 avg class size, 37.4 avg environment size
c swps: 0 failed, 491 impls, 443 equivs
c swp0: 839 type 0 queries, 33 unsat (3.9%), 836 sat (99.6%)
c swp1: 1689 type 1 queries, 1089 unsat (64.5%), 1249 sat (73.9%)
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: 3913130 calls to obtain time
c tops: 295917 fixed 18%, 43 its, 1744.88 confs/it
c trds: 10 transitive reductions, 16552 removed, 82 failed
c trds: 274998 nodes, 454179 edges, 23994871 steps
c trim: 749069 words, 2.9 MB
c trnr: 10 count, 16285 bin, 582951 trn, 353938889 steps
c unhd: 14 count, 14 rounds, 251610535 steps
c unhd: 47034 non-trivial sccs of average size 2.4
c unhd: 5366 units, 5342 bin, 20 trn, 4 lrg
c unhd: 6923 failed, 5945 stamp, 0 lits, 56 bin, 816 trn, 4 lrg
c unhd: 537045 tauts, 11293 bin 2%, 134016 trn 25%, 35215 lrg 7%
c unhd: 537045 tauts, 356521 stamp 66%, 361097 red 67%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 870691 str, 5342 bin 1%, 89243 trn 10%, 776106 lrg 89%, 332325 red 38%
c vars: 263821 remaining 16% and 1357941 removed 84% out of 1621762
c vars: 295917 fixed 18%, 904356 eliminated 56%, 157668 equivalent 10%
c vsts: 13198562812 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 6.2 search visits per propagation, 170326.2 per conflict
c wchs: 1294805519 pushed, 212850266 enlarged, 147 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         123508             0             0      10365679       3246583         25986
c 
c  0 0         61512  50         0   0<        0   0<  8305237  80   2076281  64     11991  46     1.0
c  1 5          2403   2         0   0         0   0    486844   5<   228007   7<     1109   4     0.1
c  2 6          5642   5         0   0         0   0    672032   6    357286  11      2606  10<    0.3
c  3 9          6628   5<        0   0         0   0    349647   3    212426   7      3600  14     0.6
c  4 14         6132   5         0   0         0   0    210993   2    142352   4      2154   8     0.9
c  5 21         4723   4         0   0         0   0     98995   1     66652   2      1426   5     0.9
c  6 30         4749   4         0   0         0   0     80048   1     54689   2      1105   4     1.6
c  7 41         4160   3         0   0         0   0     51795   0     33860   1       816   3     2.0
c  8 54         4130   3         0   0         0   0     32598   0     23495   1       382   1     3.2
c  9 69         4368   4         0   0         0   0     43026   0     27290   1       386   1     5.4
c 10 86        11778  10         0   0         0   0     23725   0     17604   1       374   1     5.9
c 11 126         694   1         0   0         0   0      1283   0       590   0        13   0     0.3
c 12 230        6589   5         0   0         0   0      9456   0      6051   0        24   0     5.3
c 
c avg                  3.4           0.0           0.0           0.6           1.2           2.2
c std                  4.1           0.0           0.0           1.5           2.0           2.6
c 
c   74.745   8% probe
c   73.433   7% elim
c   40.890   4% sweep
c   36.751   4% unhide
c   31.968   3% bump
c   22.739   2% cce
c   19.579   2% block
c   14.996   2% bca
c   11.837   1% quatres
c 
c   16.677 < 1% rest (below)
c 
c    8.069   1% gauss
c    4.168   0% ternres
c    2.264   0% decide
c    1.449   0% transred
c    0.727   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   19.616   2% preprocessing     5%
c  342.119  34% inprocessing     95%
c ==================================
c  361.734  36% simplifying
c  633.925  64% search
c ==================================
c  995.688 100% all
c 
c         75030 conflicts,          75.4 confs/sec
c          1763 ternaries,          42.6 confs/ternary
c           888 binaries,           84.5 confs/binary
c            43 iterations,       1744.9 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          5477 restarts,            5.5 rests/sec,     13.7 confs/restart
c       1879122 decisions,        1887.3 decis/sec,     25.0 decis/conflict
c    2109224535 propagations,  2118358.1 props/sec,   1122.5 props/decision
c 
c 995.7 seconds, 647.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
