c launch: /data/cnf/sc2014/app/blocks-blocks-36-0.120-NOTKNOWN.cnf.bz2
c host: atom24
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/blocks-blocks-36-0.120-NOTKNOWN.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/blocks-blocks-36-0.120-NOTKNOWN.cnf.bz2
c no embedded options
c found 'p cnf 489685 8779920' header
c read 489685 variables, 8779920 clauses, 19139520 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 441587 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  441587  7833796         0       0      0     0    0     0  179   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1958449 based on 7833796 irredundant clauses
c [card-1] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 148690 variables
c [simpleprobe-1] all 340995 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 11832370 based on 5916185 irredundant clauses
c [decomp-2] removed 6389 variables
c [simpleprobe-1] 319734 variables remain 96% (14872 retained 4%)
c [simpleprobe-1] removed 6389 variables, found 7 hbrs, 23 units
c [unhide-1] limit 362008 based on 5792138 irredundant clauses
c [unhide-1-1] 0 units, 109 failed, 157575 tauts, 0 hbrs, 98 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 329533 variables 100%
c [elim-1] limit of 5500000 steps based on 5500000 irredundant clauses
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 110260 not tried 33% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 64 = 0% variables out of 329533 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 5499781 negative 100.0% of 5499858 except 77 0.0%
c [phase-count-1] 1298004 positive 23.6% of 5499858 except 4201854 76.4%
c [phase-count-1] less non-negative clauses 77 than limit 549900 (10.0%)
c [phase-count-1] non-pos/non-neg = 4201854/77 = 54569.53 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 329469 negative 100%
c [sort-queue-1] sorted 329469 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 329469 (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 14434 variables 4.2% (329469 remain 75%)
c [simplification-1] removed 2333938 irredundant clauses 29.8% (5499858 remain 70%)
c [simplification-1] maximum reduction of 30% = max (4%, 30%)
c [simplification-1] large reduction 30% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   13.1  329468  5499858         1       0      0     2    0     0  178   0%      0    0    0    0    0%
c i   13.2  327642  5499858        19      16      0     2    0     1  178   5%      0    1    1    0 24860%
c i   13.2  327318  5499858        21      16      0     3    0     2  178   4%      0    2    1    0 24669%
c i   13.2  327109  5499858        22      16      0     3    0     2  178   4%      0    2    1    0 24573%
c i   13.2  326782  5499858        30      23      0     3    0     4  178   2%      0    4    2    0 24212%
c i   13.2  326191  5499858        33      24      0     4    0     5  178   2%      0    5    2    0 23952%
c i   13.2  325206  5499858        34      24      0     4    0     5  178   2%      0    5    2    0 23859%
c i   13.2  325027  5499858        35      24      0     4    0     5  178   2%      0    5    2    0 23766%
c i   13.2  324842  5499858        36      24      0     4    0     5  178   2%      0    5    2    0 23674%
c i   13.2  323721  5499858        37      24      0     4    0     5  178   2%      0    5    2    0 23581%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 9836 variables
c [simpleprobe-2] 305323 schedulable variables 96%
c [simpleprobe-2] limit 10670544 based on 5335272 irredundant clauses
c [decomp-4] removed 6399 variables
c [simpleprobe-2] 206903 variables remain 66% (106331 retained 34%)
c [simpleprobe-2] removed 6399 variables, found 2 hbrs, 301 units
c [treelook-1] limit 1305881 based on 5223525 irredundant clauses
c [treelook-1] scheduled 283577 literals 45%
c [treelook-1] scheduling used 1306096 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1305881 based on 5223525 irredundant clauses
c [treelook-1] used 1352121 steps
c [treelook-1] 283564 literals remain 45%
c [treelook-1] 281479 variables remain to probed next time 90%
c [treelook-1] removed 0 variables, found 2313 hbrs
c [basicprobe-1] limit 41788200 based on 5223525 irredundant clauses
c [basicprobe-1-0] 195815 probes remain 65% after last round
c [basicprobe-1-0] 34 units = 34 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 11595 variables, found 136066 hbrs
c [unhide-2] limit 326470 based on 5223525 irredundant clauses
c [unhide-2-2] 26 units, 90 failed, 184 tauts, 0 hbrs, 117 literals
c [elim-2] 100529 variables 34% will be scheduled this time
c [elim-2] scheduled 100529 variables 34%
c [elim-2] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 97735 not tried 33% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 66 = 0% variables out of 100529 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 4876429 negative 100.0% of 4876506 except 77 0.0%
c [phase-count-2] 1170260 positive 24.0% of 4876506 except 3706246 76.0%
c [phase-count-2] less non-negative clauses 77 than limit 487600 (10.0%)
c [phase-count-2] non-pos/non-neg = 3706246/77 = 48133.06 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 43271 negative 100%
c [sort-queue-2] sorted 290870 enqueued variables after 37 conflicts
c [score-dist-2] active 6201 (2%), one 0 (0%), zero 290870 (98%)
c [score-dist-2] max exp 504, different 4 (1%)
c [score-dist-2] median active exp 502, avg 502.1
c [simplification-2] removed 25185 variables 7.8% (297071 remain 67%)
c [simplification-2] removed 623352 irredundant clauses 11.3% (4876506 remain 62%)
c [simplification-2] maximum reduction of 11% = max (8%, 11%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1069 (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   27.5  297070  4876506        42      23      0 132876    0     5  161   2%      0    5    2    0 23251%
c i   27.5  296912  4876506        43      23      0 132876    0     5  161   2%      0    5    2    0 23160%
c i   27.5  296747  4876506        44      23      0 132876    0     5  161   2%      0    5    2    0 23070%
c i   27.5  296551  4876506        55      28      2 132879    0     5  161   3%      0    5    2    0 22553%
c i   27.5  295244  4876506        56      28      2 132879    0     5  161   3%      0    5    2    0 22465%
c i   27.5  295066  4876506        57      28      2 132879    0     5  161   3%      0    5    2    0 22378%
c i   27.5  294878  4876506        58      28      2 132879    0     5  161   3%      0    5    2    0 22291%
c i   27.5  294490  4876506        59      28      2 132879    0     5  161   3%      0    5    2    0 22204%
c i   27.5  293760  4876506        62      27      3 132880    0     5  161   3%      0    5    2    0 21965%
c i   27.5  293588  4876506        63      27      3 132880    0     5  161   3%      0    5    2    0 21879%
c i   27.5  293409  4876506        64      27      3 132880    0     5  161   3%      0    5    2    0 21794%
c i   27.5  293224  4876506        65      27      3 132880    0     5  161   3%      0    5    2    0 21709%
c i   27.5  293033  4876506        66      27      3 132880    0     5  161   3%      0    5    2    0 21625%
c i   27.5  292836  4876506        67      27      3 132880    0     5  161   3%      0    5    2    0 21541%
c i   27.5  291243  4876506        70      27      5 132880    0     5  161   3%      0    5    2    0 21320%
c i   27.5  291095  4876506        74      28      7 132880    0     5  161   3%      0    5    2    0 21098%
c i   27.6  290959  4876506        81      32      7 132882    0     6  161   3%      0    6    2    0 20676%
c i   27.6  289778  4876506        86      34      8 132882    0     6  161   3%      0    6    2    0 21138%
c i   27.6  289536  4876506        88      34      8 132883    0     6  161   3%      0    6    2    0 20980%
c i   27.6  289012  4876506        89      34      8 132883    0     6  161   3%      0    6    2    0 20899%
c i   27.6  288794  4876506        90      34      8 132883    0     6  161   3%      0    6    2    0 20817%
c i   27.6  288562  4876506        97      40      8 132883    0     6  161   3%      0    6    2    0 20563%
c i   27.6  288462  4876506        98      40      8 132883    0     6  161   3%      0    6    2    0 20483%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   27.6  288355  4876506        99      40      8 132883    0     6  161   3%      0    6    2    0 20404%
c i   27.6  287998  4876506       102      41      8 132883    0     6  161   4%      0    6    4    0 21792%
c i   27.7  283566  4876506       107      40      8 132886    0     6  161   5%      0    6    4    0 21579%
c i   27.7  283472  4876506       108      40      8 132886    0     6  161   5%      0    6    4    0 21495%
c i   27.7  283371  4876506       109      40      8 132886    0     6  161   5%      0    6    4    0 21411%
c i   27.7  283264  4876506       110      40      8 132886    0     6  161   5%      0    6    4    0 21328%
c i   27.7  281005  4876506       115      43      8 132887    0     6  161   5%      0    6    4    0 20956%
c i   27.7  280834  4876506       116      43      8 132887    0     6  161   5%      0    6    4    0 20874%
c i   27.7  280650  4876506       117      43      8 132887    0     6  161   5%      0    6    4    0 20793%
c i   27.7  280451  4876506       118      43      8 132887    0     6  161   5%      0    6    4    0 20712%
c i   27.8  280306  4876506       119      43      8 132887    0     6  161   5%      0    6    4    0 20631%
c i   27.8  280146  4876506       120      43      8 132887    0     6  161   5%      0    6    4    0 20551%
c i   27.8  279974  4876506       125      46      8 132888    0     6  161   5%      0    6    4    0 20301%
c i   27.8  279169  4876506       134      53      8 132889    0     6  161   5%      0    6    4    0 19891%
c i   27.8  278265  4876506       135      53      8 132889    0     6  161   5%      0    6    4    0 19813%
c i   27.8  267577  4876506       136      53      8 132889    0     6  161   5%      0    6    4    0 19736%
c i   27.8  267345  4876506       139      53      8 132891    0     6  161   5%      0    6    4    0 19516%
c i   27.8  265740  4876506       140      53      8 132891    0     6  161   5%      0    6    4    0 19440%
c i   27.8  265681  4876506       141      53      8 132891    0     6  161   5%      0    6    4    0 19365%
c i   27.8  265616  4876506       142      53      8 132891    0     6  161   5%      0    6    4    0 19289%
c i   27.9  265545  4876506       143      53      8 132891    0     6  161   5%      0    6    4    0 19214%
c i   27.9  265468  4876506       144      53      8 132891    0     6  161   5%      0    6    4    0 19139%
c i   27.9  265385  4876506       145      53      8 132891    0     6  161   5%      0    6    4    0 19065%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   27.9  265293  4876506       146      53      8 132891    0     6  161   5%      0    6    4    0 18991%
c i   27.9  265201  4876506       147      53      8 132891    0     6  161   5%      0    6    4    0 18917%
c i   27.9  265100  4876506       148      53      8 132891    0     6  161   5%      0    6    4    0 18843%
c i   27.9  264880  4876506       149      53      8 132891    0     6  161   5%      0    6    4    0 18770%
c i   27.9  264761  4876506       150      53      8 132891    0     6  161   5%      0    6    4    0 18697%
c i   27.9  257895  4876506       151      53      8 132891    0     6  161   5%      0    6    4    0 18624%
c i   27.9  257770  4876506       155      54      8 132893    0     6  161   5%      0    6    3    0 18364%
c i   27.9  257717  4876506       156      54      8 132893    0     6  161   5%      0    6    3    0 18293%
c i   27.9  257661  4876506       157      54      8 132893    0     6  161   5%      0    6    3    0 18222%
c i   27.9  257596  4876506       158      54      8 132893    0     6  161   5%      0    6    3    0 18151%
c i   27.9  257525  4876506       159      54      8 132893    0     6  161   5%      0    6    3    0 18080%
c i   27.9  257365  4876506       160      54      8 132893    0     6  161   5%      0    6    3    0 18010%
c i   27.9  257276  4876506       161      54      8 132893    0     6  161   5%      0    6    3    0 17940%
c i   27.9  257181  4876506       162      54      8 132893    0     6  161   5%      0    6    3    0 17870%
c i   27.9  257080  4876506       163      54      8 132893    0     6  161   5%      0    6    3    0 17800%
c i   27.9  256973  4876506       164      54      8 132893    0     6  161   5%      0    6    3    0 17731%
c i   27.9  256860  4876506       165      54      8 132893    0     6  161   5%      0    6    3    0 17662%
c i   27.9  256741  4876506       166      54      8 132893    0     6  161   5%      0    6    3    0 17593%
c i   27.9  255914  4876506       167      54      8 132893    0     6  161   5%      0    6    3    0 17525%
c i   27.9  249482  4876506       168      54      8 132893    0     6  161   5%      0    6    3    0 17457%
c i   27.9  249348  4876506       169      54      8 132893    0     6  161   5%      0    6    3    0 17389%
c i   28.0  249206  4876506       171      55      8 132893    0     6  162   5%      0    6    3    0 17423%
c i   28.4  249017  4876506       252     130     12 132893    1    20  162   4%      0   20    9    0 18422%
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   28.5  248995  4876506       266     142     13 132893    1    23  162   4%      0   23   10    0 18278%
c i   28.5  248788  4876506       268     143     13 132893    1    24  162   4%      0   24   10    0 18167%
c i   28.5  248591  4876506       269     143     13 132893    1    24  162   4%      0   24   10    0 18096%
c i   28.5  248390  4876506       270     143     13 132893    1    24  162   4%      0   24   10    0 18026%
c i   28.7  247857  4876506       320     182     13 132894    1    30  162   4%      0   30   13    0 17016%
c i   28.7  247674  4876506       321     182     13 132894    1    30  162   4%      0   30   13    0 16949%
c i   28.7  247483  4876506       322     182     13 132894    1    30  162   4%      0   30   13    0 16883%
c i   28.7  247289  4876506       323     182     13 132894    1    30  162   4%      0   30   13    0 16818%
c i   28.7  247086  4876506       324     182     13 132894    1    30  162   4%      0   30   13    0 16752%
c i   28.7  246550  4876506       325     182     13 132894    1    30  162   4%      0   30   13    0 16687%
c i   28.7  246373  4876506       326     182     13 132894    1    30  162   4%      0   30   13    0 16622%
c i   28.7  246188  4876506       327     182     13 132894    1    30  162   4%      0   30   13    0 16558%
c i   28.7  245997  4876506       328     182     13 132894    1    30  162   4%      0   30   13    0 16493%
c i   28.7  245800  4876506       329     182     13 132894    1    30  162   4%      0   30   13    0 16429%
c i   28.8  245597  4876506       351     196     16 132895    1    31  162   4%      0   31   13    0 15690%
c i   28.8  245441  4876506       352     196     16 132895    1    31  162   4%      0   31   13    0 15629%
c i   28.8  245279  4876506       353     196     16 132895    1    31  162   4%      0   31   13    0 15568%
c i   28.8  245108  4876506       354     196     16 132895    1    31  162   4%      0   31   13    0 15507%
c i   28.8  244929  4876506       355     196     16 132895    1    31  162   4%      0   31   13    0 15447%
c i   28.8  244744  4876506       356     196     16 132895    1    31  162   4%      0   31   13    0 15387%
c i   28.9  244553  4876506       357     196     16 132895    1    31  162   4%      0   31   13    0 15327%
c i   28.9  244356  4876506       358     196     16 132895    1    31  162   4%      0   31   13    0 15268%
c i   28.9  243614  4876506       359     196     16 132895    1    31  162   4%      0   31   13    0 15208%
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   28.9  243081  4876506       360     196     16 132895    1    31  162   4%      0   31   12    0 15149%
c i   28.9  242934  4876506       361     196     16 132895    1    31  162   4%      0   31   12    0 15090%
c i   28.9  242773  4876506       362     196     16 132895    1    31  162   4%      0   31   12    0 15031%
c i   28.9  242606  4876506       363     196     16 132895    1    31  162   4%      0   31   12    0 14973%
c i   28.9  242427  4876506       364     196     16 132895    1    31  162   4%      0   31   12    0 14915%
c i   28.9  242248  4876506       365     196     16 132895    1    31  162   4%      0   31   12    0 14857%
c i   28.9  242063  4876506       366     196     16 132895    1    31  162   4%      0   31   12    0 14799%
c i   28.9  241872  4876506       367     196     16 132895    1    31  162   4%      0   31   12    0 14741%
c 
c [simplification-3] limit of 110 iterations hit after 110 iterations
c [card-2] limit 1219126 based on 4876506 irredundant clauses
c [card-2] found 60 at-most-one constraints of average size 32.8
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1219126 for elimination
c [card-2] 60 out of 60 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 265 at-most-one constraints, 8 used 3%
c [card-2] exported 240 binary clauses, 30.0 per/constraint
c [decomp-6] removed 57998 variables
c [unhide-3] limit 237198 based on 3795181 irredundant clauses
c [unhide-3-3] 15 units, 74 failed, 67194 tauts, 0 hbrs, 1187 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 236850 variables 100%
c [elim-3] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 207265 not tried 88% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 35 = 0% variables out of 236850 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 3664432 negative 100.0% of 3664509 except 77 0.0%
c [phase-count-3] 931179 positive 25.4% of 3664509 except 2733330 74.6%
c [phase-count-3] less non-negative clauses 77 than limit 366400 (10.0%)
c [phase-count-3] non-pos/non-neg = 2733330/77 = 35497.79 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 6620 negative 100%
c [sort-queue-3] sorted 192329 enqueued variables after 367 conflicts
c [score-dist-3] active 44486 (19%), one 0 (0%), zero 192329 (81%)
c [score-dist-3] max exp 506, different 6 (1%)
c [score-dist-3] median active exp 503, avg 502.8
c [simplification-3] removed 4861 variables 2.0% (236815 remain 54%)
c [simplification-3] removed 1211997 irredundant clauses 24.9% (3664509 remain 47%)
c [simplification-3] maximum reduction of 25% = max (2%, 25%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 1893 (hard 11000)
c [simplification-3] new iteration interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   37.2  236814  3664509       369     147      7 90994    1    31  124   4%      0   31   12    0 14637%
c i   37.2  236673  3664509       378     152      8 90995    1    31  125   4%      0   31   12    0 14177%
c i   37.2  236577  3664509       379     152      8 90995    1    31  125   4%      0   31   12    0 14122%
c i   37.2  236475  3664509       380     152      8 90995    1    31  125   4%      0   31   12    0 14067%
c i   37.2  236371  3664509       381     152      8 90995    1    31  125   4%      0   31   12    0 14012%
c i   37.2  236263  3664509       382     152      8 90995    1    31  125   4%      0   31   12    0 13958%
c i   37.2  236155  3664509       383     152      8 90995    1    31  125   4%      0   31   11    0 13903%
c i   37.2  236041  3664509       384     152      8 90995    1    31  125   4%      0   31   11    0 13849%
c i   37.2  235923  3664509       385     152      8 90995    1    31  125   4%      0   31   11    0 13795%
c i   37.3  235799  3664509       386     152      8 90995    1    31  125   4%      0   31   11    0 13742%
c i   37.3  235668  3664509       387     152      8 90995    1    31  125   4%      0   31   11    0 13688%
c i   37.3  235465  3664509       388     152      8 90995    1    31  125   4%      0   31   11    0 13635%
c i   37.3  235373  3664509       389     152      8 90995    1    31  125   4%      0   31   11    0 13582%
c i   37.3  235224  3664509       390     152      8 90995    1    31  125   4%      0   31   11    0 13529%
c i   37.3  235069  3664509       391     152      8 90995    1    31  125   4%      0   31   11    0 13476%
c i   37.3  234905  3664509       392     152      8 90995    1    31  125   4%      0   31   11    0 13424%
c i   37.3  234738  3664509       393     152      8 90995    1    31  125   4%      0   31   11    0 13372%
c i   37.3  234567  3664509       394     152      8 90995    1    31  125   4%      0   31   11    0 13320%
c i   37.3  234388  3664509       395     152      8 90995    1    31  125   4%      0   31   11    0 13268%
c i   37.3  234203  3664509       396     152      8 90995    1    31  125   4%      0   31   11    0 13216%
c i   37.3  234012  3664509       397     152      8 90995    1    31  125   4%      0   31   11    0 13165%
c i   37.3  233818  3664509       398     152      8 90995    1    31  125   4%      0   31   11    0 13113%
c i   37.4  233083  3664509       429     175     10 90995    1    31  125   4%      0   31   10    0 11986%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   37.4  232970  3664509       430     175     10 90995    1    31  125   4%      0   31   10    0 11940%
c i   37.4  232824  3664509       431     175     10 90995    1    31  125   4%      0   31   10    0 11893%
c i   37.4  232675  3664509       432     175     10 90995    1    31  125   4%      0   31   10    0 11847%
c i   37.4  232520  3664509       433     175     10 90995    1    31  125   4%      0   31   10    0 11801%
c i   37.4  232362  3664509       434     175     10 90995    1    31  125   4%      0   31   10    0 11755%
c i   37.4  232195  3664509       435     175     10 90995    1    31  125   4%      0   31   10    0 11709%
c i   37.4  232022  3664509       436     175     10 90995    1    31  125   4%      0   31   10    0 11664%
c i   37.4  231840  3664509       437     175     10 90995    1    31  125   4%      0   31   10    0 11618%
c i   37.4  231655  3664509       438     175     10 90995    1    31  125   4%      0   30   10    0 11573%
c i   37.4  231464  3664509       439     175     10 90995    1    31  125   4%      0   30   10    0 11528%
c i   37.4  231267  3664509       440     175     10 90995    1    31  125   4%      0   30   10    0 11483%
c i   37.4  231148  3664509       441     175     10 90995    1    31  125   4%      0   30   10    0 11438%
c i   37.4  231014  3664509       442     175     10 90995    1    31  125   4%      0   30   10    0 11394%
c i   37.4  230874  3664509       443     175     10 90995    1    31  125   4%      0   30   10    0 11350%
c i   37.4  230725  3664509       444     175     10 90995    1    31  125   4%      0   30   10    0 11305%
c i   37.4  230570  3664509       445     175     10 90995    1    31  125   4%      0   30   10    0 11261%
c i   37.4  230409  3664509       446     175     10 90995    1    31  125   4%      0   30   10    0 11218%
c i   37.5  230242  3664509       447     175     10 90995    1    31  125   4%      0   30    9    0 11174%
c i   37.5  230069  3664509       448     175     10 90995    1    31  125   4%      0   30    9    0 11130%
c i   37.5  229893  3664509       449     175     10 90995    1    31  125   4%      0   30    9    0 11087%
c i   37.5  229708  3664509       450     175     10 90995    1    31  125   4%      0   30    9    0 11044%
c i   37.5  229517  3664509       451     175     10 90995    1    31  125   4%      0   30    9    0 11001%
c i   37.5  228581  3664509       458     181     10 90995    1    30  125   4%      0   30    9    0 10770%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   37.5  227514  3664509       459     181     10 90995    1    30  125   4%      0   30    9    0 10728%
c i   37.6  227511  3664509       489     207     10 90995    1    32  125   4%      0   32   10    0 10974%
c i   37.6  226021  3664509       490     207     10 90995    1    32  125   4%      0   32   10    0 10932%
c i   37.6  225849  3664509       491     207     10 90995    1    32  125   4%      0   32   10    0 10889%
c i   37.8  223240  3664509       525     235     12 90998    1    35  125   4%      0   34   10    0 9995%
c i   37.8  222307  3664509       526     235     12 90998    1    35  125   4%      0   34   10    0 9956%
c i   37.9  221571  3664509       548     246     15 90999    2    35  125   4%      0   35   10    0 9768%
c i   37.9  221386  3664509       549     246     15 90999    2    35  125   4%      0   35   10    0 9730%
c i   37.9  221195  3664509       550     246     15 90999    2    35  125   4%      0   35   10    0 9692%
c i   38.0  221192  3664509       551     246     15 90999    2    35  125   4%      0   35   10    0 9654%
c i   38.0  220998  3664509       557     251     15 90999    2    35  126   4%      0   35   10    0 9587%
c i   38.0  220971  3664509       558     251     15 90999    2    35  126   4%      0   35   10    0 9549%
c i   38.1  220942  3664509       559     251     15 90999    2    35  126   4%      0   35   10    0 9512%
c i   38.1  220907  3664509       560     251     15 90999    2    35  126   4%      0   35   10    0 9475%
c i   38.1  220867  3664509       561     251     15 90999    2    35  126   4%      0   35   10    0 9438%
c i   38.2  220824  3664509       562     251     15 90999    2    35  126   4%      0   35   10    0 9402%
c i   38.2  220774  3664509       563     251     15 90999    2    35  126   4%      0   35   10    0 9365%
c i   38.2  220722  3664509       564     251     15 90999    2    35  126   4%      0   35   10    0 9329%
c i   38.3  220669  3664509       565     251     15 90999    2    35  126   4%      0   35   10    0 9292%
c i   38.3  220616  3664509       566     251     15 90999    2    35  126   4%      0   35    9    0 9256%
c i   38.3  220555  3664509       567     251     15 90999    2    35  126   4%      0   35    9    0 9220%
c i   38.4  220490  3664509       568     251     15 90999    2    35  126   4%      0   35    9    0 9184%
c i   38.4  220417  3664509       569     251     15 90999    2    35  126   4%      0   35    9    0 9148%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   38.4  220342  3664509       570     251     15 90999    2    35  126   4%      0   35    9    0 9113%
c i   38.4  220263  3664509       571     251     15 90999    2    35  126   4%      0   35    9    0 9077%
c i   38.5  220184  3664509       572     251     15 90999    2    35  126   4%      0   35    9    0 9042%
c i   38.5  220095  3664509       573     251     15 90999    2    35  126   4%      0   35    9    0 9007%
c i   38.5  219193  3664509       579     256     15 90999    2    35  126   4%      0   35    9    0 9039%
c i   38.6  219002  3664509       583     259     15 90999    2    35  126   5%      0   35   10    0 9211%
c i   38.6  218811  3664509       584     259     15 90999    2    35  126   5%      0   35   10    0 9175%
c i   38.7  218798  3664509       585     259     15 90999    2    35  126   5%      0   35   10    0 9140%
c i   38.7  218777  3664509       586     259     15 90999    2    35  126   5%      0   35   10    0 9104%
c i   38.7  218737  3664509       587     259     15 90999    2    35  126   5%      0   35   10    0 9069%
c i   38.7  218690  3664509       588     259     15 90999    2    35  126   5%      0   35   10    0 9033%
c i   38.8  218637  3664509       589     259     15 90999    2    35  126   5%      0   35   10    0 8998%
c i   38.8  218578  3664509       590     259     15 90999    2    35  126   5%      0   35    9    0 8963%
c i   38.8  218513  3664509       591     259     15 90999    2    35  126   5%      0   35    9    0 8928%
c i   38.9  218442  3664509       592     259     15 90999    2    35  126   5%      0   35    9    0 8894%
c i   38.9  218365  3664509       593     259     15 90999    2    35  126   5%      0   35    9    0 8859%
c i   38.9  218282  3664509       594     259     15 90999    2    35  126   5%      0   35    9    0 8824%
c i   38.9  218194  3664509       595     259     15 90999    2    35  126   5%      0   35    9    0 8790%
c i   39.0  218099  3664509       596     259     15 90999    2    35  126   5%      0   35    9    0 8756%
c i   39.0  217998  3664509       597     259     15 90999    2    35  126   5%      0   35    9    0 8722%
c i   39.0  217891  3664509       598     259     15 90999    2    35  126   5%      0   35    9    0 8688%
c i   39.0  217778  3664509       599     259     15 90999    2    35  126   5%      0   35    9    0 8654%
c i   39.1  217659  3664509       600     259     15 90999    2    35  126   5%      0   35    9    0 8620%
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   39.1  217534  3664509       601     259     15 90999    2    35  126   5%      0   35    9    0 8587%
c i   39.1  217404  3664509       602     259     15 90999    2    35  126   5%      0   35    9    0 8554%
c i   39.1  217267  3664509       603     259     15 90999    2    35  126   5%      0   35    9    0 8520%
c i   39.1  217124  3664509       604     259     15 90999    2    35  126   5%      0   35    9    0 8487%
c i   39.2  216975  3664509       605     259     15 90999    2    35  126   5%      0   35    9    0 8454%
c i   39.2  216316  3664509       606     259     15 90999    2    35  126   5%      0   35    9    0 8421%
c i   39.3  215177  3664509       613     265     15 90999    2    35  126   5%      0   35    9    0 8425%
c i   39.3  214998  3664509       614     265     15 90999    2    35  126   5%      0   35    9    0 8392%
c i   39.9  214819  3664509       732     359     23 91003    3    38  127   8%      0   38   26    0 12890%
c i   43.7  214608  3664509      1398     871     79 91048    7    61  133  12%      3   60   35    1 6657%
c i   43.8  214607  3664509      1406     877     79 91048    7    61  133  12%      3   60   34    1 6527%
c i   47.9  214606  3664509      2004    1214    170 91054   24    90  135  26%      4   89  136    2 8207%
c i   47.9  214605  3664509      2006    1214    170 91055   24    90  135  26%      4   89  135    2 8143%
c i   47.9  214604  3664509      2012    1219    170 91055   24    90  135  26%      4   89  135    2 8080%
c 
c [simplification-4] limit 2802 conflicts (hard 11000) hit after 2803 conflicts
c [decomp-7] removed 24753 variables
c [treelook-2] limit 800151 based on 3200605 irredundant clauses
c [treelook-2] scheduled 187009 literals 44%
c [treelook-2] scheduling used 800388 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 800151 based on 3200605 irredundant clauses
c [treelook-2] used 867215 steps
c [treelook-2] 186998 literals remain 44%
c [treelook-2] 173261 variables remain to probed next time 82%
c [treelook-2] removed 1 variables, found 2452 hbrs
c [unhide-4] limit 200037 based on 3200599 irredundant clauses
c [unhide-4-4] 4 units, 76 failed, 306 tauts, 0 hbrs, 116703 literals
c [elim-4] 70532 variables 33% will be scheduled this time
c [elim-4] scheduled 70532 variables 33%
c [elim-4] boosting limit by 20
c [elim-4] limit of 296291870 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 9958 not tried 5% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 13 = 0% variables out of 70532 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 3164507 negative 100.0% of 3164584 except 77 0.0%
c [phase-count-4] 831881 positive 26.3% of 3164584 except 2332703 73.7%
c [phase-count-4] less non-negative clauses 77 than limit 316400 (10.0%)
c [phase-count-4] non-pos/non-neg = 2332703/77 = 30294.84 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 610 negative 100%
c [sort-queue-4] sorted 54701 enqueued variables after 2803 conflicts
c [score-dist-4] active 156152 (74%), one 0 (0%), zero 54701 (26%)
c [score-dist-4] max exp 511, different 11 (2%)
c [score-dist-4] median active exp 506, avg 505.9
c [simplification-4] removed 3751 variables 1.7% (210853 remain 48%)
c [simplification-4] removed 499925 irredundant clauses 13.6% (3164584 remain 40%)
c [simplification-4] maximum reduction of 14% = max (2%, 14%)
c [simplification-4] large reduction 14% >= 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 14803 (soft 4803 + delta 10000)
c [simplification-4] new conflict limit 4803 (hard 14803)
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   61.7  210852  3164584      2874    1596    301 77394   37   150  120  24%      6  147  112    3 3962%
c i   61.8  210849  3164584      2881    1600    303 77394   37   151  120  24%      6  148  109    3 3871%
c i   61.8  210847  3164584      2885    1603    303 77394   37   152  120  24%      6  149  108    3 3817%
c i   62.1  210845  3164584      2935    1642    311 77396   36   155  120  24%      6  152   92    3 3250%
c i   62.3  210843  3164584      2962    1660    313 77402   36   157  120  23%      5  154   85    3 2970%
c i   62.9  210840  3164584      3040    1714    317 77411   37   161  123  23%      5  158   80    3 2734%
c 
c [simplification-5] limit of 200 binary hit after 200 binaries
c [quatres-1] found 61 quaternary clauses 1% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 12658336 based on 3164584 irredundant clauses
c [ternres-1] all 210795 free variables schedulable
c [ternres-1] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-1] 85758 variables remain 41% (125037 retained 59%)
c [gauss-1] limit 1582292 based on 3164584 irredundant clauses
c [gauss-1] extracted 79 xors of average arity 2.0
c [gauss-1] connected 158 occurrences of 152 variables (average 1.0)
c [gauss-1] limit 1581618 based on 3163237 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 630 variables
c [basicprobe-2] limit 25295776 based on 3161972 irredundant clauses
c [basicprobe-2-0] 134689 probes remain 64% after last round
c [basicprobe-2-0] 11 units = 11 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 16 variables, found 108726 hbrs
c [unhide-5] limit 197623 based on 3161972 irredundant clauses
c [unhide-5-5] 2 units, 78 failed, 24137 tauts, 0 hbrs, 60101 literals
c [transred-1] limit 3137437 based on 3137437 irredundant clauses
c [transred-1] removed 96 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 209370 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 125000000 steps penalty 2 = 0 + 2
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 9 blocked clauses
c [block-1] 9 < 1/100 * 3137342 = 31373 considered unsuccessful
c [cce-1] limit of 7500000 steps penalty 2 = 0 + 2
c [cce-1-1] eliminated 9 clauses out of 19 (47%) of length 1334
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 9 large clauses in 7500004 steps
c [cce-1-1] allowing another 3750002 steps for small clauses
c [cce-1-1] scheduling 2973243 clauses = 2968316 binary + 4927 ternary
c [cce-1-1] tried to eliminate 231 small clauses 0%
c [cce-1-1] eliminated 42 binary clauses 0%
c [cce-1-1] eliminated 42 small clauses 0%
c [cce-1-1] eliminated 42 small clauses in 7500000 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 51 covered clauses in round 1
c [cce-1] eliminated 51 covered clauses in TOTAL during 1 rounds
c [cce-1] 51 < 1/100 * 3113744 = 31137 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 209370 variables 100%
c [elim-5] limit of 21739826 steps penalty 2 = 0 + 2
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 92548 not tried 44% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 33 = 0% variables out of 209370 scheduled
c [elim-5] 33 < 1/100 * 209370 = 2093 considered unsuccessful
c [bca-1] limit of 10000000 steps and 6227846 added (scaled 2)
c [bca-1] 317792 out of 418676 literals actually usable 76%
c [bca-1] added 1 blocked clauses in 688916 steps
c [sweep-1] limit 6227346 based on 3113673 irredundant clauses
c [sweep-1-1] 2248 pos 1.1% + 207089 neg 98.9% = 209337 sched 100.0% ret 0
c [sweep-1-1] 6298049 steps 50 queries 24665.16 avg class size
c [sweep-1-1] 1617 decisions 49 SAT calls 557.63 avg env size
c [sweep-1-1] 207203 variables remain 99% (2134 retained 1%)
c [decomp-10] removed 401 variables
c [sweep-1-1] removed 401 vars (0 failed, 0 eqs, 1 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 401 vars in TOTAL (1 rounds, 49 queries)
c [phase-count-5] 3112792 negative 100.0% of 3112869 except 77 0.0%
c [phase-count-5] 821525 positive 26.4% of 3112869 except 2291344 73.6%
c [phase-count-5] less non-negative clauses 77 than limit 311200 (10.0%)
c [phase-count-5] non-pos/non-neg = 2291344/77 = 29757.71 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 553 negative 100%
c [sort-queue-5] sorted 42556 enqueued variables after 4055 conflicts
c [score-dist-5] active 166380 (80%), one 0 (0%), zero 42556 (20%)
c [score-dist-5] max exp 512, different 12 (2%)
c [score-dist-5] median active exp 507, avg 506.3
c [simplification-5] removed 1859 variables 0.9% (208936 remain 47%)
c [simplification-5] removed 51715 irredundant clauses 1.6% (3112869 remain 40%)
c [simplification-5] maximum reduction of 2% = max (1%, 2%)
c [simplification-5] forced so keeping old conflict interval 0
c [simplification-5] conflict limit remains at 4806 (hard 14803)
c [simplification-5] 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   96.5  208935  3112869      4112    2186    463 194401   54   197  127  27%      8  191   99    5 2112%
c i   99.0  208933  3112869      4370    2319    480 194421   58   201  130  29%      7  194  118    5 2278%
c i  101.9  208885  3112869      4722    2490    509 194456   63   201  130  31%      5  193  107    6 1865%
c 
c [simplification-6] limit 4806 conflicts (hard 14803) hit after 4806 conflicts
c [ternres-2] limit 12451476 based on 3112869 irredundant clauses
c [ternres-2] 84973 schedulable variables 41%
c [ternres-2] 26 ternary resolvents (2 bin, 24 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 778217 based on 3112869 irredundant clauses
c [card-3] found 50 at-most-one constraints of average size 28.5
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 778217 for elimination
c [card-3] 50 out of 50 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 78 variables
c [simpleprobe-3] 137547 schedulable variables 66%
c [simpleprobe-3] limit 6223340 based on 3111670 irredundant clauses
c [decomp-12] removed 2101 variables
c [simpleprobe-3] 90101 variables remain 44% (116656 retained 56%)
c [simpleprobe-3] removed 2101 variables, found 196 hbrs, 533 units
c [unhide-6] limit 192013 based on 3072223 irredundant clauses
c [unhide-6-6] 63 units, 39 failed, 2148 tauts, 0 hbrs, 67057 literals
c [transred-2] limit 3072147 based on 3072147 irredundant clauses
c [transred-2] removed 156 transitive binary clauses
c [transred-2] found 2 units
c [bca-2] limit of 10000000 steps and 6122036 added (scaled 2)
c [bca-2] 311726 out of 412696 literals actually usable 76%
c [bca-2] added 0 blocked clauses in 676185 steps
c [sweep-2] limit 6121536 based on 3060768 irredundant clauses
c [sweep-2-1] 2155 pos 1.1% + 202128 neg 98.9% = 204283 sched 99.0% ret 2064
c [sweep-2-1] 6156764 steps 50 queries 22113.96 avg class size
c [sweep-2-1] 1212 decisions 48 SAT calls 1527.08 avg env size
c [sweep-2-1] 203025 variables remain 98% (3322 retained 2%)
c [decomp-13] removed 202 variables
c [sweep-2-1] removed 202 vars (0 failed, 1 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 202 vars in TOTAL (1 rounds, 49 queries)
c [phase-count-6] 3060293 negative 100.0% of 3060368 except 75 0.0%
c [phase-count-6] 811548 positive 26.5% of 3060368 except 2248820 73.5%
c [phase-count-6] less non-negative clauses 75 than limit 306000 (10.0%)
c [phase-count-6] non-pos/non-neg = 2248820/75 = 29984.27 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 553 negative 100%
c [sort-queue-6] sorted 37482 enqueued variables after 4806 conflicts
c [score-dist-6] active 168663 (82%), one 0 (0%), zero 37482 (18%)
c [score-dist-6] max exp 512, different 12 (2%)
c [score-dist-6] median active exp 507, avg 506.5
c [simplification-6] removed 2740 variables 1.3% (206145 remain 47%)
c [simplification-6] removed 52501 irredundant clauses 1.7% (3060368 remain 39%)
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 21472 (soft 11472 + delta 10000)
c [simplification-6] new conflict limit 11472 (hard 21472)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  110.3  206144  3060368      4814    2506    494 199740   64   200  122  32%      5  192  108    6 1830%
c i  118.9  206143  3060368      5874    3320    580 199791   62   180  146  35%      8  169   39    7  588%
c i  132.1  206141  3060368      7250    4533    671 199831   50   139  189  36%     11  125   13    7  187%
c i  133.8  206139  3060368      7398    4664    683 199831   49   136  196  36%     10  122   18    7  261%
c i  146.6  206137  3060368      8577    5760    718 199857   41   110  236  38%     10   93   16    7  216%
c i  153.0  206135  3060368      9058    6219    725 199862   38   100  251  39%      7   83   16    7  221%
c i  154.0  206133  3060368      9121    6232    726 199910   38   100  251  38%      7   82   18    7  251%
c i  154.3  206131  3060368      9164    6262    726 199920   40   101  251  40%      7   84   51    7  682%
c i  155.2  206129  3060368      9271    6325    739 199940   40   100  251  40%      6   83   42    7  568%
c i  155.8  206127  3060368      9325    6375    739 199942   40    99  251  40%      6   82   37    7  492%
c i  157.1  206125  3060368      9446    6473    750 199952   39    97  252  40%      5   80   28    7  379%
c i  161.8  206123  3060368      9881    6832    774 199995   36    90  288  40%      4   72   16    8  213%
c i  162.8  206122  3060368      9962    6879    804 199995   36    89  288  40%      4   71   14    8  184%
c i  165.8  206120  3060368     10247    7133    830 199998   34    84  319  41%      3   65   12    8  159%
c 
c [simplification-7] limit 11472 conflicts (hard 21472) hit after 11474 conflicts
c [quatres-2] found 127 quaternary clauses 1% in total
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [ternres-3] limit 12241472 based on 3060368 irredundant clauses
c [ternres-3] all 206119 free variables schedulable
c [ternres-3] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-3] 90318 variables remain 44% (115801 retained 56%)
c [gauss-2] limit 1530184 based on 3060368 irredundant clauses
c [gauss-2] extracted 3 xors of average arity 2.7
c [gauss-2] connected 8 occurrences of 5 variables (average 1.6)
c [gauss-2] limit 1529768 based on 3059536 irredundant clauses
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 13 variables
c [treelook-3] limit 764877 based on 3059511 irredundant clauses
c [treelook-3] scheduled 181524 literals 44%
c [treelook-3] scheduling used 765237 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 764877 based on 3059511 irredundant clauses
c [treelook-3] used 775276 steps
c [treelook-3] 181459 literals remain 44%
c [treelook-3] 156820 variables remain to probed next time 76%
c [treelook-3] removed 0 variables, found 8470 hbrs
c [unhide-7] limit 191219 based on 3059511 irredundant clauses
c [unhide-7-7] 7 units, 55 failed, 19078 tauts, 0 hbrs, 4359180 literals
c [transred-3] limit 3040492 based on 3040492 irredundant clauses
c [transred-3] removed 162 transitive binary clauses
c [transred-3] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 206004 variables 100%
c [block-2] limit of 16641238 steps penalty 3 = 1 + 2
c [block-2] incomplete 10105 not tried 5%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 4 blocked clauses
c [block-2] 4 < 1/100 * 3040332 = 30403 considered unsuccessful
c [cce-2] limit of 8320619 steps penalty 3 = 1 + 2
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 1333
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 1296
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 1294
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 1262
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 1225
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 1224
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 1220
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 1216
c [cce-2-1] eliminated 2 clauses out of 3 (67%) of length 1157
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 1146
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 11 large clauses in 8322326 steps
c [cce-2-1] allowing another 4161163 steps for small clauses
c [cce-2-1] scheduling 2899180 clauses = 2894254 binary + 4926 ternary
c [cce-2-1] tried to eliminate 77 small clauses 0%
c [cce-2-1] eliminated 36 binary clauses 0%
c [cce-2-1] eliminated 36 small clauses 0%
c [cce-2-1] eliminated 36 small clauses in 8320623 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 47 covered clauses in round 1
c [cce-2] eliminated 47 covered clauses in TOTAL during 1 rounds
c [cce-2] 47 < 1/100 * 3037721 = 30377 considered unsuccessful
c [elim-6] 9854 variables 5% will be scheduled this time
c [elim-6] scheduled 9854 variables 5%
c [elim-6] limit of 33282476 steps penalty 3 = 1 + 2
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 4973 not tried 2% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 9854 scheduled
c [sweep-3] limit 6075344 based on 3037672 irredundant clauses
c [sweep-3-1] 2246 pos 1.1% + 200457 neg 98.9% = 202703 sched 98.4% ret 3301
c [sweep-3-1] 6133454 steps 60 queries 20100.22 avg class size
c [sweep-3-1] 1216 decisions 59 SAT calls 972.03 avg env size
c [sweep-3-1] 200110 variables remain 97% (5894 retained 3%)
c [decomp-16] removed 51 variables
c [sweep-3-1] removed 51 vars (0 failed, 0 eqs, 2 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 51 vars in TOTAL (1 rounds, 59 queries)
c [phase-count-7] 3037495 negative 100.0% of 3037570 except 75 0.0%
c [phase-count-7] 808956 positive 26.6% of 3037570 except 2228614 73.4%
c [phase-count-7] less non-negative clauses 75 than limit 303700 (10.0%)
c [phase-count-7] non-pos/non-neg = 2228614/75 = 29714.85 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 535 negative 100%
c [sort-queue-7] sorted 32698 enqueued variables after 11474 conflicts
c [score-dist-7] active 173255 (84%), one 0 (0%), zero 32698 (16%)
c [score-dist-7] max exp 514, different 14 (3%)
c [score-dist-7] median active exp 509, avg 508.0
c [simplification-7] removed 166 variables 0.1% (205953 remain 47%)
c [simplification-7] removed 22798 irredundant clauses 0.7% (3037570 remain 39%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-7] new conflict interval 16666
c [simplification-7] penalized conflict interval 16666 = 1 * 16666
c [simplification-7] hard conflict limit 38140 (soft 28140 + delta 10000)
c [simplification-7] new conflict limit 28140 (hard 38140)
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  211.2  205952  3037570     11515    8281    870 223668   28    67  380  43%      9   47   11    8  150%
c i  215.5  205951  3037570     11880    8609    876 223690   27    62  393  43%      7   43   10    8  126%
c i  288.1  205949  3037570     21744   12620   1204 223757  369   456  434  81%    128  382  172   68  252%
c i  297.3  205947  3037570     22755   13365   1258 223770  319   424  466  75%     46  345  156   69  225%
c i  298.1  205945  3037570     22878   13471   1260 223770  318   433  466  74%     40  353  210   70  301%
c i  306.3  205943  3037570     24116   14267   1331 223790  300   431  466  70%     12  345  145   73  198%
c i  322.3  205942  3037570     25658   15094   1353 223800  249   360  482  69%      5  266  120   75  160%
c i  329.7  205940  3037570     26071   15376   1358 223801  234   339  482  69%      1  244  104   75  139%
c i  351.2  205938  3037570     27680   16618   1380 223824  180   266  613  68%      3  166   40   75   53%
c i  356.6  205937  3037570     28131   17029   1394 223838  165   246  634  67%     -1  144   31   74   42%
c i  356.6  205935  3037570     28133   17030   1394 223838  165   246  634  67%     -1  144   31   74   42%
c i  359.5  205933  3037570     28337   17208   1402 223845  158   236  634  67%     -2  134   25   74   34%
c 
c [simplification-8] limit 28145 conflicts (hard 38140) hit after 29668 conflicts
c [quatres-3] found 235 quaternary clauses 2% in total
c [quatres-3-2] added 3 single-self-subsuming ternary resolvents
c [ternres-4] limit 12150280 based on 3037570 irredundant clauses
c [ternres-4] 90241 schedulable variables 44%
c [ternres-4] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 28 variables
c [basicprobe-3] limit 37473448 penalty 2 = 0 + 2
c [basicprobe-3-0] 131083 probes remain 64% after last round
c [basicprobe-3-0] 17 units = 17 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 31 variables, found 122534 hbrs
c [unhide-8] limit 189811 based on 3036985 irredundant clauses
c [unhide-8-8] 10 units, 40 failed, 3330 tauts, 0 hbrs, 10307542 literals
c [transred-4] limit 3036229 based on 3036229 irredundant clauses
c [transred-4] removed 101 transitive binary clauses
c [transred-4] found 1 units
c [bca-3] limit of 10000000 steps and 6069018 added (scaled 2)
c [bca-3] 286367 out of 411634 literals actually usable 70%
c [bca-3] added 0 blocked clauses in 630060 steps
c [sweep-4] limit 6068518 based on 3034259 irredundant clauses
c [sweep-4-1] 2423 pos 1.2% + 197506 neg 98.8% = 199929 sched 97.1% ret 5887
c [sweep-4-1] 6082898 steps 54 queries 26973.96 avg class size
c [sweep-4-1] 895 decisions 51 SAT calls 1122.25 avg env size
c [sweep-4-1] 198451 variables remain 96% (7353 retained 4%)
c [decomp-18] removed 66 variables
c [sweep-4-1] removed 66 vars (0 failed, 4 eqs, 3 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 66 vars in TOTAL (1 rounds, 53 queries)
c [phase-count-8] 3033881 negative 100.0% of 3033956 except 75 0.0%
c [phase-count-8] 808301 positive 26.6% of 3033956 except 2225655 73.4%
c [phase-count-8] less non-negative clauses 75 than limit 303300 (10.0%)
c [phase-count-8] non-pos/non-neg = 2225655/75 = 29675.40 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 427 negative 100%
c [sort-queue-8] sorted 29743 enqueued variables after 29668 conflicts
c [score-dist-8] active 176007 (86%), one 0 (0%), zero 29743 (14%)
c [score-dist-8] max exp 515, different 15 (3%)
c [score-dist-8] median active exp 510, avg 509.0
c [simplification-8] removed 183 variables 0.1% (205750 remain 47%)
c [simplification-8] removed 3614 irredundant clauses 0.1% (3033956 remain 39%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 20000
c [simplification-8] new conflict interval 36666
c [simplification-8] penalized conflict interval 36666 = 1 * 36666
c [simplification-8] hard conflict limit 84667 (soft 66334 + delta 18333)
c [simplification-8] new conflict limit 66334 (hard 84667)
c 
c [simplification-9] limit 66334 conflicts (hard 84667) hit after 66334 conflicts
c [quatres-4] found 443 quaternary clauses 4% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 1 quaternary resolvents
c [ternres-5] limit 13604911 with penalty 2 = 0 + 2
c [ternres-5] all 205750 free variables schedulable
c [ternres-5] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-5] 85728 variables remain 42% (120022 retained 58%)
c [simpleprobe-4] 89597 schedulable variables 44%
c [simpleprobe-4] limit 50000000 penalty 2 = 0 + 2
c [decomp-20] removed 1830 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 1830 variables, found 2201 hbrs, 578 units
c [unhide-9] limit 340122 with penalty 5 = 0 + 5
c [unhide-9-9] 0 units, 3 failed, 12707 tauts, 0 hbrs, 14417647 literals
c [transred-5] limit 2988099 based on 2988099 irredundant clauses
c [transred-5] removed 83 transitive binary clauses
c [transred-5] found 1 units
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 81629465 penalty 1 = 0 + 1
c [sweep-5-1] 2106 pos 1.1% + 194548 neg 98.9% = 196654 sched 96.4% ret 7258
c [sweep-5-1] 81637876 steps 901 queries 2027.85 avg class size
c [sweep-5-1] 11494 decisions 886 SAT calls 824.59 avg env size
c [sweep-5-1] 57262 variables remain 28% (146633 retained 72%)
c [decomp-21] removed 61 variables
c [sweep-5-1] removed 61 vars (0 failed, 16 eqs, 34 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 61 vars in TOTAL (1 rounds, 900 queries)
c [phase-count-9] 2986821 negative 100.0% of 2986896 except 75 0.0%
c [phase-count-9] 800611 positive 26.8% of 2986896 except 2186285 73.2%
c [phase-count-9] less non-negative clauses 75 than limit 298600 (10.0%)
c [phase-count-9] non-pos/non-neg = 2186285/75 = 29150.47 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 271 negative 100%
c [sort-queue-9] sorted 7874 enqueued variables after 66334 conflicts
c [score-dist-9] active 195977 (96%), one 0 (0%), zero 7874 (4%)
c [score-dist-9] max exp 517, different 17 (3%)
c [score-dist-9] median active exp 510, avg 509.0
c [simplification-9] removed 1899 variables 0.9% (203851 remain 46%)
c [simplification-9] removed 47060 irredundant clauses 1.6% (2986896 remain 38%)
c [simplification-9] maximum reduction of 2% = max (1%, 2%)
c [simplification-9] geometric conflict interval increment 12222 = 36666 / 3
c [simplification-9] new conflict interval 48888
c [simplification-9] penalized conflict interval 48888 = 1 * 48888
c [simplification-9] hard conflict limit 139666 (soft 115222 + delta 24444)
c [simplification-9] new conflict limit 115222 (hard 139666)
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  763.6  203850  2986896     66361   43308   1993 497618   98   271 1355  36%    435  120  128   94  137%
c i  802.7  203848  2986896     72195   46730   2129 497700  427   845 1609  51%    -65  649  550  132  418%
c -  860.6  203847  2986896     82086   22042   2276 497743  690   851  206  81%      6  560  704  206  342%
c i  970.8  203846  2986896    100210   30172   2438 497812  462   621  355  74%    252  223  137  289   47%
c i  971.7  203844  2986896    100525   30405   2443 497817  457   687  355  66%    140  288  381  290  132%
c i  971.9  203842  2986896    100579   30426   2459 497817  457   692  355  66%    124  292  395  290  136%
c i  973.3  203840  2986896    100846   30596   2489 497824  457   748  356  61%     57  347  451  291  155%
c i  974.0  203838  2986896    100997   30692   2493 497827  465   779  357  60%     25  377  545  291  187%
c i  983.0  203836  2986896    103064   31611   2518 497829  626  1028  358  61%   -124  611  703  310  227%
c i  983.0  203834  2986896    103070   31616   2518 497829  626  1028  358  61%   -124  611  692  310  223%
c i  984.7  203832  2986896    103480   31791   2521 497833  651  1045  358  62%   -137  624  847  314  270%
c i  985.8  203830  2986896    103657   31933   2537 497836  633  1048  358  60%   -141  625  525  314  167%
c i  988.4  203828  2986896    104263   32378   2568 497845  590  1061  359  56%   -149  632  238  314   76%
c i  991.3  203827  2986896    105104   32959   2631 497853  538  1060  359  51%   -153  623  289  314   92%
c i  991.4  203825  2986896    105113   32966   2631 497853  538  1060  359  51%   -153  622  287  314   91%
c i  992.1  203823  2986896    105262   33070   2633 497856  529  1054  359  50%   -154  615  293  314   93%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 3 count, 1 added (12 skipped), 1995161 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: 2 bces, 13 removed, 13404958 resolutions, 38077701 steps
c blkd: 13 blocking literals 0%, 0 pure
c bump: 105480 bumped seen, 642392924 lits 6090.2 on average
c card: 3 count, 0 units, 240 am1, 7960241 steps
c card: 3 rescheduled, 17 eliminated, 3301 resolved, 539 subsumed
c card: 110 at-most-one constraints found, average size 30.84
c card: 110 at-most-one constraints used 100%, average size 30.84
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 2 cces, 98 eliminated, 98 ate 100%, 0 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 27919440 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 51 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 21 decompositions, 17739 equivalent 4%
c deco: 49421 decision-only clauses 47%, 89% reduction
c decs: 4670673 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 211 eliminated 0%, 0 pure 0%
c elms: 6 rounds, 1.0 rounds/bve
c elms: 126 small 60%, 85 large 40%
c elms: 222 tried small, 126 succeeded 57%, 96 failed 43%
c elms: 116 subsumed, 5840 strengthened, 0 blocked
c elms: 6917846 copies, 6976014 resolutions, 3903 ipos
c elms: 28183594 subchks, 5350445 strchks
c gaus: 2 extractions, 82 extracted, 2.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 6225482 steps, 3112741 extr 50%, 267 elim 0%
c glue: 319.4 orig avg, 319.4 real avg, 8.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 578411 = 2406 simple 0% + 575363 trn 99% + 642 lrg 0%, 88 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 105480 clauses, 2605.8 length
c lrnd: 274854990 lits = 516788835 orig - 241933845 removed 47%
c lrnd: 62647 uips 59%, 32939 flips 31%
c mins: 29248 mins 36%, 661 bin 1%, 2509 size 3%
c mins: 38616743 poisoned searches, 10951497 hits, 28% hit rate
c mins: 41885608 used twice searches, 655336 hits, 2% hit rate
c move: moved 91, 81 bin 89%, 10 trn 11%
c otfs: 894 driving 15%, 4951 restarting 85%
c otfs: str 5845, 5836 red 100%, 9 irr 0%
c otfs: str 5845, 0 bin 0%, 1 trn 0%, 5844 lrg 100%
c otfs: sub 40, 40 red 100%, 0 irr 0%
c otfs: sub 40, 0 bin 0%, 0 trn 0%, 40 lrg 100%
c phas: 9 computed, 382309 set, 0 pos (0%), 382309 neg (100%)
c prbs: 3 basic, 4477 probed, 62 failed, 0 lifted
c prbs: 4 simple, 856768 probed, 1435 failed, 1158 eqs
c prbs: 3 treelook, 89 probed, 1 failed, 0 lifted
c prom: 226 locked 0% out of 250661 tried
c prps: 1928846395 props, 407 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 4 count, 1 quat, 4 self1, 0 self2, 1 dup
c queu: 9 sorted, 4670673 next (22518 steps 0.00)
c queu: 643900331 enq (3069502440 steps 4.77), 642392924 deq 100%
c redc: 1077 clauses 33%, 3267 tried 3%, 1 sat 0%
c redc: 5148 lits 23%, 22813 tried 0%, 1 sat 0%
c redc: 327 times jump level reduced, 121.6 levels on average
c reds: 1 count, 106121.0 conflicts per reduce
c reds: 0 memlim 0%, 1 arith 100%
c reds: 25005 collected 83%, 5211 retired 17%
c rmbd: 5387 removed, 391 red 7%
c rsts: 5158 restarts 90%, 556 skipped 10%
c rsts: 556 saturating 100%, 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: 9 count, 6 confs 67%, 0 vars 0%
c simp: 2 its 22%, 1 bin 11%, 0 trns 0%
c subl: 105480 count (198107 tried 1.9), 36757 sub out of 101201 (36.3%)
c swps: 5 count, 5 rounds, 1110 queries (222.0/round)
c swps: 1093 sat calls, 5 unsat (0.2% success rate)
c swps: 16434 decisions 15.0, 254 conflicts 0.2
c swps; 6151.9 avg class size, 865.3 avg environment size
c swps: 0 failed, 43 impls, 21 equivs
c swp0: 368 type 0 queries, 19 unsat (5.2%), 363 sat (98.6%)
c swp1: 742 type 1 queries, 66 unsat (8.9%), 726 sat (97.8%)
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: 9552713 calls to obtain time
c tops: 267913 fixed 55%, 266 its, 398.95 confs/it
c trds: 5 transitive reductions, 598 removed, 5 failed
c trds: 3792 nodes, 24654 edges, 15285483 steps
c trim: 1111159 words, 4.2 MB
c trnr: 5 count, 2 bin, 40 trn, 57120920 steps
c unhd: 9 count, 9 rounds, 144789347 steps
c unhd: 3031 non-trivial sccs of average size 2.1
c unhd: 127 units, 127 bin, 0 trn, 0 lrg
c unhd: 564 failed, 563 stamp, 0 lits, 1 bin, 0 trn, 0 lrg
c unhd: 286659 tauts, 183 bin 0%, 11 trn 0%, 117 lrg 0%
c unhd: 286659 tauts, 286348 stamp 100%, 6138 red 2%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 29329632 str, 127 bin 0%, 5 trn 0%, 29329500 lrg 100%, 29329093 red 100%
c vars: 203822 remaining 42% and 285863 removed 58% out of 489685
c vars: 267913 fixed 55%, 211 eliminated 0%, 17739 equivalent 4%
c vsts: 8218757653 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 4.3 search visits per propagation, 76223.3 per conflict
c wchs: 285840148 pushed, 50921586 enlarged, 81 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         101202         25005          5211       7295460       1624273         51107
c 
c  0 0          2980   3        56   0         0   0   2196017  30    368493  23      2961   6     2.7
c  1 5           852   1        46   0        55   1    606509   8    177725  11      1658   3     2.2
c  2 6          3975   4       422   2       212   4   1219637  17    265976  16      3767   7    23.3
c  3 9          5928   6      2250   9       244   5   1017444  14<   212227  13      4936  10    88.3
c  4 14         6274   6      2690  11       358   7    461477   6    119280   7<     4753   9    90.0
c  5 21         3979   4      1742   7       311   6    292807   4     69849   4      2707   5    66.1
c  6 30         4065   4      1451   6       314   6    471862   6     72227   4      4063   8<   57.9
c  7 41         4576   5      2301   9<      224   4    259556   4     65248   4      3267   6    89.7
c  8 54         5980   6      4187  17       321   6    219573   3     68142   4      4793   9   152.0
c  9 69         5538   5<     3330  13       356   7<   180689   2     73929   5      4341   8   123.2
c 10 86         5979   6      3180  13       289   6    188218   3     68952   4      8193  16   113.7
c 11 126        5663   6       749   3       436   8     37425   1     14822   1      2043   4     3.5
c 12 230       16117  16      1873   7       755  14     54285   1     20598   1      1773   3    11.7
c 13 534       29017  29       728   3      1336  26     89186   1     26565   2      1815   4    53.5
c 14 1526        279   0         0   0         0   0       775   0       240   0        37   0     1.7
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                  9.1           7.5           9.1           3.0           3.5           6.5
c std                  4.0           2.9           3.7           3.1           3.4           3.6
c 
c  241.341  24% bump
c  108.719  11% unhide
c   28.492   3% probe
c   28.254   3% elim
c   26.712   3% sweep
c   11.582   1% block
c 
c   14.103 < 1% rest (below)
c 
c    5.691   1% decide
c    3.191   0% bca
c    2.109   0% gauss
c    1.971   0% cce
c    0.418   0% transred
c    0.352   0% card
c    0.334   0% ternres
c    0.038   0% quatres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   13.010   1% preprocessing     5%
c  230.681  23% inprocessing     95%
c ==================================
c  243.692  24% simplifying
c  752.154  76% search
c ==================================
c  995.855 100% all
c 
c        106121 conflicts,         106.6 confs/sec
c          2802 ternaries,          37.9 confs/ternary
c          1170 binaries,           90.7 confs/binary
c           266 iterations,        399.0 confs/iteration
c 
c             1 reductions,          0.0 redus/sec, 106121.0 confs/reduction
c          5158 restarts,            5.2 rests/sec,     20.6 confs/restart
c       4670673 decisions,        4690.1 decis/sec,     44.0 decis/conflict
c    1928846395 propagations,  1936875.5 props/sec,    413.0 props/decision
c 
c 995.9 seconds, 1630.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
