c launch: /data/cnf/sc2014/app/post-cbmc-aes-d-r2.cnf.bz2
c host: atom19
c Lingeling SAT Solver
c 
c Version b7ztzud 55d9a3e9649fc56eacf3e72d8e2e2d5c615d5f18
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Fri May  1 11:44:04 CEST 2015
c compiled Fri May  1 11:44:04 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/post-cbmc-aes-d-r2.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/post-cbmc-aes-d-r2.cnf.bz2
c no embedded options
c found 'p cnf 279119 1607567' header
c read 279119 variables, 1607567 clauses, 4321960 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 172218 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  172218  1356467         0       0      0     0    0     0   66   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 152399 variables
c [simpleprobe-1] all 124496 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 2155 variables
c [simpleprobe-1] 73174 variables remain 60% (49167 retained 40%)
c [simpleprobe-1] removed 2155 variables, found 18008 hbrs, 60 units
c [unhide-1] limit 59065 based on 945051 irredundant clauses
c [unhide-1-1] 42 units, 180 failed, 1986 tauts, 0 hbrs, 2392 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 117565 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 68230 not tried 58% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 44650 = 38% variables out of 117565 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 783129 negative 99.8% of 784795 except 1666 0.2%
c [phase-count-1] 490206 positive 62.5% of 784795 except 294589 37.5%
c [phase-count-1] less non-negative clauses 1666 than limit 78400 (10.0%)
c [phase-count-1] non-pos/non-neg = 294589/1666 = 176.82 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 72915 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 72915 zero 100.00%
c [score-distribution-1] 1 different 0.00% out of total 72915 variables
c [simplification-1] removed 86509 variables 54.3% (72915 remain 42%)
c [simplification-1] removed 571672 irredundant clauses 42.1% (784795 remain 58%)
c [simplification-1] maximum reduction of 54% = max (54%, 42%)
c [simplification-1] large reduction 54% >= 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    4.3   72914   784794         1       0      0  2185    0     0   43   0%      0    0    0    0    0%
c i    4.3   72912   784793         2       0      0  2185    0     0   43   0%      0    0    0    0    0%
c i    4.3   72910   784792         3       0      0  2185    0     0   43   0%      0    0    0    0    0%
c i    4.3   72908   784791         4       0      0  2185    0     0   43   0%      0    0    0    0    0%
c i    4.3   72906   784790         5       0      0  2185    0     0   43   0%      0    0    0    0    0%
c i    4.3   72904   784789         6       0      0  2185    0     0   43   0%      0    0    0    0    0%
c i    4.3   72902   784788         7       0      0  2185    0     0   43   0%      0    0    0    0    0%
c i    4.3   72900   784787         8       0      0  2185    0     0   43   0%      0    0    0    0    0%
c i    4.3   72898   784786         9       0      0  2185    0     0   43   0%      0    0    0    0    0%
c i    4.3   72896   784785        10       0      0  2185    0     0   43   0%      0    0    0    0    0%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 584 variables
c [simpleprobe-2] 40380 schedulable variables 56%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 956 variables
c [simpleprobe-2] 37013 variables remain 52% (34362 retained 48%)
c [simpleprobe-2] removed 956 variables, found 1465 hbrs, 70 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 40239 literals 28%
c [treelook-1] scheduling used 305474 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 315292 steps
c [treelook-1] 40228 literals remain 28%
c [treelook-1] 40002 variables remain to probed next time 56%
c [decomp-5] removed 237 variables
c [treelook-1] removed 237 variables, found 169 hbrs
c [basicprobe-1] limit 6178832 based on 772354 irredundant clauses
c [basicprobe-1-0] 36914 probes remain 52% after last round
c [basicprobe-1-0] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 7 variables, found 2950 hbrs
c [unhide-2] limit 50000 with penalty 1 = 0 + 1
c [unhide-2-2] 26 units, 408 failed, 45 tauts, 0 hbrs, 2725 literals
c [elim-2] 64059 variables 92% will be scheduled this time
c [elim-2] scheduled 64059 variables 92%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 43947 not tried 63% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 20129 = 31% variables out of 64059 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 664288 negative 99.8% of 665849 except 1561 0.2%
c [phase-count-2] 427875 positive 64.3% of 665849 except 237974 35.7%
c [phase-count-2] less non-negative clauses 1561 than limit 66500 (10.0%)
c [phase-count-2] non-pos/non-neg = 237974/1561 = 152.45 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 45845 negative 100%
c [score-distribution-2] 80 pos 0.16%, 0 min 0.00%, 49279 zero 99.84%
c [score-distribution-2] 10 different 0.02% out of total 49359 variables
c [simplification-2] removed 23536 variables 32.3% (49359 remain 29%)
c [simplification-2] removed 118936 irredundant clauses 15.2% (665849 remain 49%)
c [simplification-2] maximum reduction of 32% = max (32%, 15%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1100 (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    7.0   49358   665849        11       0      0  3839    0     0   40   0%      0    0    0    0    0%
c i    7.0   49356   665848        12       0      0  3839    0     0   40   0%      0    0    0    0    0%
c i    7.0   49354   665847        13       0      0  3839    0     0   40   0%      0    0    0    0    0%
c i    7.0   49352   665846        14       0      0  3839    0     0   40   0%      0    0    0    0    0%
c i    7.0   49350   665846        15       0      0  3839    0     0   40   0%      0    0    0    0    0%
c i    7.0   49348   665845        16       0      0  3839    0     0   40   0%      0    0    0    0    0%
c i    7.0   49346   665844        17       0      0  3839    0     0   40   0%      0    0    0    0    0%
c i    7.0   49344   665844        18       0      0  3839    0     0   40   0%      0    0    0    0    0%
c i    7.0   49342   665843        19       0      0  3839    0     0   40   0%      0    0    0    0    0%
c i    7.0   49340   665842        20       0      0  3839    0     0   40   0%      0    0    0    0    0%
c i    7.0   49338   665842        21       0      0  3839    0     0   40   0%      0    0    0    0    0%
c i    7.0   49336   665841        22       0      0  3839    0     0   40   0%      0    0    0    0    0%
c i    7.0   49334   665840        23       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.0   49332   665840        24       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.0   49330   665840        25       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.0   49328   665839        26       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.0   49326   665839        27       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49325   665839        28       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49324   665839        29       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49323   665839        30       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49322   665839        31       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49321   665839        32       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49320   665839        33       0      0  3839    0     0   41   0%      0    0    0    0    0%
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    7.1   49319   665839        34       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49318   665839        35       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49317   665839        36       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49316   665839        37       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49315   665839        38       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49314   665839        39       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49313   665839        40       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49312   665839        41       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49311   665839        42       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49310   665839        43       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49309   665839        44       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49308   665839        45       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49307   665839        46       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49306   665839        47       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49305   665839        48       0      0  3839    0     0   41   0%      0    0    0    0    0%
c i    7.1   49304   665838        93      36      6  3839    0     1   41  10%      0    1    1    0 23516%
c i    7.1   49303   665838       105      43      9  3840    0     1   41  10%      0    1    1    0 22654%
c i    7.1   49289   665834       134      57     19  3841    0     1   41  12%      0    1    1    0 21748%
c i    7.1   49288   665834       135      57     19  3841    0     1   41  12%      0    1    1    0 21663%
c i    7.1   49287   665834       136      57     19  3841    0     1   41  12%      0    1    1    0 21579%
c i    7.1   49286   665834       155      71     21  3841    0     1   41   9%      0    1    1    0 20935%
c i    7.1   49281   665833       162      72     23  3843    0     1   41   9%      0    1    1    0 20580%
c i    7.1   49280   665833       182      78     31  3846    0     1   41   9%      0    1    1    0 19552%
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    7.1   49279   665833       183      78     31  3846    0     1   41   9%      0    1    1    0 19476%
c i    7.1   49273   665833       184      78     31  3846    0     1   41   9%      0    1    1    0 19400%
c i    7.1   49138   665833       188      79     32  3847    0     1   41   9%      0    1    1    0 19156%
c i    7.1   49103   665833       191      79     32  3848    0     1   41   9%      0    1    1    0 19022%
c i    7.1   49102   665833       192      79     32  3848    0     1   41   9%      0    1    1    0 18948%
c i    7.1   49101   665833       193      79     32  3848    0     1   41   9%      0    1    1    0 18874%
c i    7.1   49100   665833       194      79     32  3848    0     1   41   9%      0    1    1    0 18801%
c i    7.1   49099   665833       195      79     32  3848    0     1   41   9%      0    1    1    0 18727%
c i    7.1   49098   665833       196      79     32  3848    0     1   41   9%      0    1    1    0 18655%
c i    7.1   49097   665833       197      79     32  3848    0     1   41   9%      0    1    1    0 18582%
c i    7.1   49095   665833       198      79     32  3848    0     1   41   9%      0    1    1    0 18510%
c i    7.1   49093   665833       221      86     43  3849    0     1   41  10%      0    1    1    0 17718%
c i    7.1   49068   665831       265     112     53  3850    0     2   41   9%      0    2    2    0 17071%
c i    7.1   49067   665827       391     185     84  3858    0     4   41   6%      0    4    3    0 14982%
c i    7.1   49065   665825       451     223     96  3861    0     4   41   7%      0    4    3    0 13955%
c i    7.2   49055   665823       512     261    107  3866    0     5   41   8%      0    5    3    0 12784%
c i    7.2   49054   665823       526     269    112  3866    0     5   41   8%      0    5    3    0 12302%
c i    7.2   49047   665823       528     269    113  3866    0     5   41   8%      0    5    3    0 12223%
c i    7.2   49021   665823       529     269    113  3866    0     5   41   8%      0    5    3    0 12176%
c i    7.2   49007   665823       530     269    113  3866    0     5   41   8%      0    5    3    0 12128%
c i    7.2   48994   665823       531     269    113  3866    0     5   41   8%      0    5    3    0 12081%
c i    7.2   48952   665823       532     269    113  3866    0     5   41   8%      0    5    3    0 12034%
c i    7.2   48951   665822       659     368    136  3867    1     6   41   8%      0    6    4    0 10624%
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    7.2   48950   665822       663     368    139  3867    1     6   41   8%      0    6    4    0 10493%
c i    7.2   48949   665822       665     368    139  3867    1     6   41   8%      0    6    4    0 10452%
c i    7.2   48923   665822       666     368    139  3867    1     6   41   8%      0    6    4    0 10412%
c i    7.2   48915   665822       667     368    139  3867    1     6   41   8%      0    6    4    0 10371%
c i    7.2   48869   665822       668     368    139  3867    1     6   41   8%      0    6    4    0 10331%
c i    7.2   48868   665822       670     368    140  3867    1     6   41   8%      0    6    3    0 10264%
c i    7.2   48859   665822       671     368    140  3867    1     6   41   8%      0    6    3    0 10224%
c i    7.2   48844   665822       755     426    156  3870    1     8   41   8%      0    8    4    0 9607%
c i    7.2   48834   665822       765     433    157  3871    1     8   41   8%      0    8    4    0 9430%
c i    7.2   48791   665822       766     433    157  3871    1     8   41   8%      0    8    4    0 9394%
c i    7.2   48780   665822       769     435    157  3871    1     8   41   8%      0    8    4    0 9321%
c i    7.2   48779   665822       773     435    158  3871    1     8   41   8%      0    8    4    0 9261%
c i    7.2   48778   665822       774     435    158  3871    1     8   41   8%      0    8    4    0 9225%
c i    7.2   48769   665822       901     514    190  3874    1    10   41   7%      0    9    4    0 7963%
c i    7.2   48768   665821       910     517    192  3874    1    10   41   7%      0    9    4    0 7840%
c i    7.2   48766   665821       912     517    192  3874    1    10   41   7%      0    9    4    0 7810%
c i    7.2   48765   665821       915     517    192  3875    1    10   41   7%      0    9    4    0 7755%
c i    7.2   48753   665821       936     530    197  3876    1    10   41   8%      0   10    4    0 7707%
c i    7.2   48741   665821       966     548    202  3881    1    10   41   7%      0   10    4    0 7470%
c i    7.2   48734   665821       970     547    204  3882    1    10   41   7%      0   10    4    0 7399%
c i    7.2   48732   665821       989     556    212  3882    1    10   41   7%      0   10    4    0 7114%
c i    7.2   48719   665821       990     556    212  3882    1    10   41   7%      0   10    4    0 7086%
c i    7.2   48696   665821       992     556    212  3883    1    10   41   7%      0   10    4    0 7036%
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    7.2   48687   665820      1048     595    221  3888    1    13   41   6%      0   13    4    0 6974%
c i    7.3   48683   665819      1132     643    242  3898    1    14   41   6%      0   14    4    0 6408%
c i    7.3   48668   665819      1165     665    247  3899    1    15   41   6%      0   14    4    0 6405%
c i    7.3   48645   665819      1166     665    247  3899    1    15   41   6%      0   14    4    0 6380%
c i    7.3   48585   665819      1167     665    247  3899    1    15   41   6%      0   14    4    0 6355%
c i    7.3   48577   665818      1216     698    257  3901    1    15   41   6%      0   15    4    0 6195%
c i    7.3   48560   665818      1222     699    259  3903    1    15   41   6%      0   15    4    0 6087%
c i    7.3   48551   665815      1270     733    268  3904    1    18   41   5%      0   18    4    0 5798%
c 
c [simplification-3] limit of 110 iterations hit after 110 iterations
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3 out of 3 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 1176 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 18213 literals 19%
c [treelook-2] scheduling used 301484 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 375808 steps
c [treelook-2] 18208 literals remain 19%
c [treelook-2] 15843 variables remain to probed next time 33%
c [decomp-7] removed 381 variables
c [treelook-2] removed 381 variables, found 66 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 9 units, 70 failed, 1865 tauts, 0 hbrs, 1412 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 47393 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 21701 not tried 46% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 19306 = 41% variables out of 47393 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 550046 negative 99.9% of 550848 except 802 0.1%
c [phase-count-3] 362512 positive 65.8% of 550848 except 188336 34.2%
c [phase-count-3] less non-negative clauses 802 than limit 55000 (10.0%)
c [phase-count-3] non-pos/non-neg = 188336/802 = 234.83 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 3851 negative 100%
c [score-distribution-3] 1958 pos 6.97%, 0 min 0.00%, 26129 zero 93.03%
c [score-distribution-3] 996 different 3.55% out of total 28087 variables
c [simplification-3] removed 20464 variables 42.1% (28087 remain 16%)
c [simplification-3] removed 114967 irredundant clauses 17.3% (550848 remain 41%)
c [simplification-3] maximum reduction of 42% = max (42%, 17%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 1766 (hard 11000)
c [simplification-3] new iteration interval 1000
c 
c [simplification-4] limit 1766 conflicts (hard 11000) hit after 1767 conflicts
c [decomp-8] removed 1 variables
c [basicprobe-2] limit 4406592 based on 550824 irredundant clauses
c [basicprobe-2-0] 22881 probes remain 81% after last round
c [basicprobe-2-0] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 2 variables, found 1372 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 15 units, 30 failed, 48 tauts, 0 hbrs, 570 literals
c [elim-4] 21238 variables 76% will be scheduled this time
c [elim-4] scheduled 21238 variables 76%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 18260 variables 65% in round 1 in 255967492 steps
c [elim-4-1] backward subsumption/strengthening limit 144032508
c [elim-4-1-1] backward checking 2992 touched variables 11%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 77 and strengthened 137 clauses in 64681424 steps
c [elim-4-1] rescheduled 549 variables 2% by backward subsumption
c [elim-4-2] eliminated 84 variables 0% in round 2 in 2676053 steps
c [elim-4-2] backward subsumption/strengthening limit 2676000
c [elim-4-2-1] backward checking 477 touched variables 2%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 25 and strengthened 19 clauses in 2331810 steps
c [elim-4-2] rescheduled 133 variables 0% by backward subsumption
c [elim-4-3] eliminated 21 variables 0% in round 3 in 152962 steps
c [elim-4-3] backward subsumption/strengthening limit 152900
c [elim-4-3-1] backward checking 59 touched variables 0%
c [elim-4-3-1] incomplete backward checking 22 remain 37%
c [elim-4-3] subsumed 14 and strengthened 8 clauses in 154476 steps
c [elim-4] incomplete 35 not tried 0% in round 3
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 18370 = 86% variables out of 21238 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 388667 negative 99.8% of 389426 except 759 0.2%
c [phase-count-4] 380645 positive 97.7% of 389426 except 8781 2.3%
c [phase-count-4] less non-negative clauses 759 than limit 38900 (10.0%)
c [phase-count-4] non-pos/non-neg = 8781/759 = 11.57 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 77 negative 100%
c [score-distribution-4] 2075 pos 21.54%, 0 min 0.00%, 7560 zero 78.46%
c [score-distribution-4] 758 different 7.87% out of total 9635 variables
c [simplification-4] removed 18452 variables 65.7% (9635 remain 6%)
c [simplification-4] removed 161402 irredundant clauses 29.3% (389426 remain 29%)
c [simplification-4] maximum reduction of 66% = max (66%, 29%)
c [simplification-4] large reduction 66% >= 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 13767 (soft 3767 + delta 10000)
c [simplification-4] new conflict limit 3767 (hard 13767)
c 
c [simplification-5] limit 3767 conflicts (hard 13767) hit after 3768 conflicts
c [quatres-1] found 5130 quaternary clauses 1% in total
c [quatres-1-2] added 20 single-self-subsuming ternary resolvents
c [quatres-1-2] added 34 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 9635 free variables schedulable
c [ternres-1] 45338 ternary resolvents (5211 bin, 40127 trn)
c [ternres-1] 230 variables remain 2% (9405 retained 98%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 45614 xors of average arity 2.9
c [gauss-1] connected 130765 occurrences of 7011 variables (average 18.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 1111 variables
c [simpleprobe-3] 4099 schedulable variables 48%
c [simpleprobe-3] limit 2000000 penalty 0 = 0 + 0
c [decomp-10] removed 3 variables
c [simpleprobe-3] 4110 variables remain 48% (4411 retained 52%)
c [simpleprobe-3] removed 3 variables, found 41 hbrs, 0 units
c [unhide-5] limit 100000 with penalty 0 = 0 + 0
c [unhide-5-5] 1 units, 1 failed, 88 tauts, 0 hbrs, 228 literals
c [transred-1] limit 470063 with penalty 0 = 0 + 0
c [transred-1] removed 47 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 8519 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] incomplete 19 not tried 0%
c [block-1] transition to [ all 1 rem 1 ] state
c [block-1] eliminated 33415 blocked clauses
c [block-1] considered successful since not run to completion yet
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 20
c [cce-1-1] eliminated 5 clauses out of 7 (71%) of length 19
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 15
c [cce-1-1] eliminated 4 clauses out of 12 (33%) of length 14
c [cce-1-1] eliminated 8 clauses out of 16 (50%) of length 13
c [cce-1-1] eliminated 8 clauses out of 12 (67%) of length 12
c [cce-1-1] eliminated 28 clauses out of 500 (6%) of length 10
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 58 large clauses in 30000121 steps
c [cce-1-1] allowing another 15000060 steps for small clauses
c [cce-1-1] scheduling 8451 clauses = 4178 binary + 4273 ternary
c [cce-1-1] tried to eliminate 1566 small clauses 19%
c [cce-1-1] eliminated 237 binary clauses 6%
c [cce-1-1] eliminated 92 ternary clauses 2%
c [cce-1-1] eliminated 329 small clauses 4%
c [cce-1-1] eliminated 329 small clauses in 30001267 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 387 covered clauses in round 1
c [cce-1] eliminated 387 covered clauses in TOTAL during 1 rounds
c [cce-1] 387 < 1/100 * 355520 = 3555 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 3905 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 1740 not tried 45% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 310 = 8% variables out of 3905 scheduled
c [bca-1] limit of 10000000 steps and 709268 added (scaled 2)
c [bca-1] 4455 out of 7192 literals actually usable 62%
c [bca-1] added 82 blocked clauses in 34720 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1438 pos 40.0% + 2157 neg 60.0% = 3595 sched 100.0% ret 0
c [sweep-1-1] 1009691 steps 53 queries 718.09 avg class size
c [sweep-1-1] 1404 decisions 51 SAT calls 27.49 avg env size
c [sweep-1-1] 3380 variables remain 94% (215 retained 6%)
c [decomp-11] removed 10 variables
c [sweep-1-1] removed 10 vars (0 failed, 1 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 10 vars in TOTAL (1 rounds, 52 queries)
c [score-distribution-5] 2471 pos 68.93%, 438 min 12.22%, 676 zero 18.86%
c [score-distribution-5] 1115 different 31.10% out of total 3585 variables
c [simplification-5] removed 6050 variables 62.8% (3585 remain 2%)
c [simplification-5] removed 34975 irredundant clauses 9.0% (354129 remain 26%)
c [simplification-5] maximum reduction of 63% = max (63%, 9%)
c [simplification-5] large reduction 63% >= 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 15768 (soft 5768 + delta 10000)
c [simplification-5] new conflict limit 5768 (hard 15768)
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.9    3584   354125      3800    2028    422   565    4    63   46   6%     25   61    8    0 2483%
c i   40.1    3583   353895      4943    2862    443   570    5    72   61   7%     15   70    9    0 1991%
c 
c [simplification-6] limit 5768 conflicts (hard 15768) hit after 5768 conflicts
c [quatres-2] found 4414 quaternary clauses 1% in total
c [quatres-2-2] added 99 single-self-subsuming ternary resolvents
c [quatres-2-2] added 157 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 88 schedulable variables 2%
c [ternres-2] 851 ternary resolvents (46 bin, 805 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 91 at-most-one constraints of average size 3.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 91 out of 91 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 15 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 904 literals 13%
c [treelook-3] scheduling used 300126 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 368488 steps
c [treelook-3] 901 literals remain 13%
c [treelook-3] 517 variables remain to probed next time 14%
c [treelook-3] removed 0 variables, found 130 hbrs
c [unhide-6] limit 142594 with penalty 0 = 0 + 0
c [unhide-6-6] 2 units, 16 failed, 302 tauts, 0 hbrs, 255 literals
c [transred-2] limit 712972 with penalty 0 = 0 + 0
c [transred-2] removed 22 transitive binary clauses
c [transred-2] found 4 units
c [block-2] 19 variables 1% will be scheduled this time
c [block-2] scheduled 19 variables 1%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] incomplete 8 not tried 0%
c [block-2] transition to [ all 0 rem 1 ] state
c [block-2] eliminated 0 blocked clauses
c [block-2] considered successful since not run to completion yet
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 3555 variables 100%
c [elim-6] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 1738 not tried 49% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 153 = 4% variables out of 3555 scheduled
c [bca-2] limit of 10000000 steps and 706749 added (scaled 2)
c [bca-2] 3189 out of 6806 literals actually usable 47%
c [bca-2] added 0 blocked clauses in 22031 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1400 pos 43.9% + 1792 neg 56.1% = 3192 sched 93.8% ret 210
c [sweep-2-1] 1122548 steps 25 queries 687.28 avg class size
c [sweep-2-1] 842 decisions 24 SAT calls 28.46 avg env size
c [sweep-2-1] 3086 variables remain 91% (315 retained 9%)
c [decomp-14] removed 12 variables
c [sweep-2-1] removed 12 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 12 vars in TOTAL (1 rounds, 24 queries)
c [score-distribution-6] 2731 pos 80.56%, 412 min 12.15%, 247 zero 7.29%
c [score-distribution-6] 1179 different 34.78% out of total 3390 variables
c [simplification-6] removed 193 variables 5.4% (3390 remain 2%)
c [simplification-6] removed 783 irredundant clauses 0.2% (352982 remain 26%)
c [simplification-6] maximum reduction of 5% = max (5%, 0%)
c [simplification-6] large reduction 5% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 17768 (soft 7768 + delta 10000)
c [simplification-6] new conflict limit 7768 (hard 17768)
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   44.2    3389   352922      6189    4285    715   738    5    92   46   6%     12   89    8    1 1403%
c 
c [simplification-7] limit 7768 conflicts (hard 17768) hit after 7768 conflicts
c [quatres-3] found 4244 quaternary clauses 1% in total
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 283 single-self-subsuming ternary resolvents
c [quatres-3-2] added 351 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3389 free variables schedulable
c [ternres-3] 3465 ternary resolvents (114 bin, 3351 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 6866 xors of average arity 3.3
c [gauss-2] connected 22682 occurrences of 1824 variables (average 12.4)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] connected 3667 occurrences of 1824 variables (average 2.0)
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 6 variables
c [basicprobe-3] limit 4719951 penalty 0 = 0 + 0
c [basicprobe-3-0] 689 sched 20%, 10 failed, 0 lifted, 2863 hbrs
c [decomp-16] removed 39 variables
c [basicprobe-3-1] 572 sched 17%, 0 failed, 0 lifted, 213 hbrs
c [decomp-17] removed 7 variables
c [basicprobe-3-2] 100 probes remain 3% after last round
c [basicprobe-3-2] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-3-2] removed 46 variables, found 3098 hbrs
c [bate-1] eliminated 56 asymmetric tautologies during probing
c [unhide-7] limit 188798 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 0 failed, 102 tauts, 0 hbrs, 230 literals
c [transred-3] limit 943990 with penalty 0 = 0 + 0
c [transred-3] removed 149 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 3337 variables 100%
c [block-3] limit of 50000000 steps penalty 0 = 0 + 0
c [block-3] incomplete 126 not tried 4%
c [block-3] transition to [ all 1 rem 1 ] state
c [block-3] eliminated 2 blocked clauses
c [block-3] considered successful since not run to completion yet
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 7500252 steps for small clauses
c [cce-2-1] scheduling 4179 clauses = 3389 binary + 790 ternary
c [cce-2-1] tried to eliminate 404 small clauses 10%
c [cce-2-1] eliminated 58 binary clauses 2%
c [cce-2-1] eliminated 5 ternary clauses 1%
c [cce-2-1] eliminated 63 small clauses 2%
c [cce-2-1] eliminated 63 small clauses in 15000431 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 63 covered clauses in round 1
c [cce-2] eliminated 63 covered clauses in TOTAL during 1 rounds
c [cce-2] 63 < 1/100 * 352351 = 3523 considered unsuccessful
c [elim-7] 1738 variables 52% will be scheduled this time
c [elim-7] scheduled 1738 variables 52%
c [elim-7] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 1455 not tried 44% in round 1
c [elim-7] transition to [ all 0 rem 1 ] state
c [elim-7] eliminated 1 = 0% variables out of 1738 scheduled
c [elim-7] 1 < 1/100 * 1738 = 17 considered unsuccessful
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1369 pos 45.3% + 1653 neg 54.7% = 3022 sched 90.6% ret 314
c [sweep-3-1] 1090999 steps 51 queries 491.71 avg class size
c [sweep-3-1] 1066 decisions 50 SAT calls 29.72 avg env size
c [sweep-3-1] 2796 variables remain 84% (540 retained 16%)
c [decomp-18] removed 3 variables
c [sweep-3-1] removed 3 vars (0 failed, 1 eqs, 1 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 3 vars in TOTAL (1 rounds, 50 queries)
c [score-distribution-7] 2659 pos 79.78%, 542 min 16.26%, 132 zero 3.96%
c [score-distribution-7] 1146 different 34.38% out of total 3333 variables
c [simplification-7] removed 56 variables 1.7% (3333 remain 2%)
c [simplification-7] removed 593 irredundant clauses 0.2% (352069 remain 26%)
c [simplification-7] maximum reduction of 2% = max (2%, 0%)
c [simplification-7] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-7] new conflict interval 6666
c [simplification-7] penalized conflict interval 6666 = 1 * 6666
c [simplification-7] hard conflict limit 24434 (soft 14434 + delta 10000)
c [simplification-7] new conflict limit 14434 (hard 24434)
c 
c [simplification-8] limit 14434 conflicts (hard 24434) hit after 14434 conflicts
c [quatres-4] found 4097 quaternary clauses 1% in total
c [quatres-4-1] added 6 double-self-subsuming ternary resolvents
c [quatres-4-2] added 199 single-self-subsuming ternary resolvents
c [quatres-4-2] added 29 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 3333 free variables schedulable
c [ternres-4] 1472 ternary resolvents (90 bin, 1382 trn)
c [ternres-4] 1 variables remain 0% (3332 retained 100%)
c [decomp-19] removed 3 variables
c [simpleprobe-4] 1701 schedulable variables 51%
c [simpleprobe-4] limit 6516166 penalty 0 = 0 + 0
c [decomp-20] removed 6 variables
c [simpleprobe-4] 1430 variables remain 43% (1894 retained 57%)
c [simpleprobe-4] removed 6 variables, found 324 hbrs, 0 units
c [transred-4] limit 1629041 with penalty 0 = 0 + 0
c [transred-4] removed 183 transitive binary clauses
c [block-4] 8 variables 0% will be scheduled this time
c [block-4] scheduled 8 variables 0%
c [block-4] limit of 50000000 steps penalty 0 = 0 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [bca-3] limit of 10000000 steps and 702255 added (scaled 2)
c [bca-3] 1583 out of 6650 literals actually usable 24%
c [bca-3] added 0 blocked clauses in 18298 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1251 pos 44.9% + 1533 neg 55.1% = 2784 sched 83.8% ret 540
c [sweep-4-1] 1017854 steps 9 queries 878.56 avg class size
c [sweep-4-1] 320 decisions 8 SAT calls 33.12 avg env size
c [sweep-4-1] 2763 variables remain 83% (561 retained 17%)
c [decomp-21] removed 1 variables
c [sweep-4-1] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 1 vars in TOTAL (1 rounds, 8 queries)
c [score-distribution-8] 2206 pos 66.39%, 1072 min 32.26%, 45 zero 1.35%
c [score-distribution-8] 1052 different 31.66% out of total 3323 variables
c [simplification-8] removed 10 variables 0.3% (3323 remain 2%)
c [simplification-8] removed 73 irredundant clauses 0.0% (350818 remain 26%)
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 26666
c [simplification-8] penalized conflict interval 26666 = 1 * 26666
c [simplification-8] hard conflict limit 54433 (soft 41100 + delta 13333)
c [simplification-8] new conflict limit 41100 (hard 54433)
c 
c [simplification-9] limit 41100 conflicts (hard 54433) hit after 41100 conflicts
c [quatres-5] found 3913 quaternary clauses 1% in total
c [quatres-5-2] added 155 single-self-subsuming ternary resolvents
c [quatres-5-2] added 12 quaternary resolvents
c [ternres-5] limit 4631544 with penalty 0 = 0 + 0
c [ternres-5] 1 schedulable variables 0%
c [ternres-5] 156 ternary resolvents (2 bin, 154 trn)
c [ternres-5] fully completed ternary resolution
c [unhide-8] limit 463154 with penalty 1 = 1 + 0
c [unhide-8-8] 0 units, 4 failed, 1279 tauts, 0 hbrs, 1198 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 177 transitive binary clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 3320 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 926308950 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8] incomplete 264 not tried 8% in round 1
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 106 = 3% variables out of 3320 scheduled
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 13894630 penalty 0 = 0 + 0
c [sweep-5-1] 1163 pos 43.5% + 1509 neg 56.5% = 2672 sched 83.1% ret 542
c [sweep-5-1] 13894845 steps 280 queries 76.80 avg class size
c [sweep-5-1] 12300 decisions 281 SAT calls 48.01 avg env size
c [sweep-5-1] 658 variables remain 20% (2556 retained 80%)
c [decomp-23] removed 2 variables
c [sweep-5-1] removed 2 vars (0 failed, 1 eqs, 5 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 2 vars in TOTAL (1 rounds, 279 queries)
c [score-distribution-9] 1058 pos 32.94%, 2154 min 67.06%, 0 zero 0.00%
c [score-distribution-9] 486 different 15.13% out of total 3212 variables
c [simplification-9] removed 111 variables 3.3% (3212 remain 2%)
c [simplification-9] removed 44092 irredundant clauses 12.7% (302366 remain 22%)
c [simplification-9] maximum reduction of 13% = max (3%, 13%)
c [simplification-9] large reduction 13% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 53100 (soft 43100 + delta 10000)
c [simplification-9] new conflict limit 43100 (hard 53100)
c 
c [simplification-10] limit 43100 conflicts (hard 53100) hit after 43102 conflicts
c [quatres-6] found 3874 quaternary clauses 1% in total
c [quatres-6-2] added 51 single-self-subsuming ternary resolvents
c [quatres-6-2] added 91 quaternary resolvents
c [ternres-6] limit 4871530 with penalty 0 = 0 + 0
c [ternres-6] all 3212 free variables schedulable
c [ternres-6] 895 ternary resolvents (28 bin, 867 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 304470 penalty 3 = 3 + 0
c [card-4] found 25 at-most-one constraints of average size 3.7
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 304470 for elimination
c [card-4] 25 out of 25 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 3090 xors of average arity 3.0
c [gauss-3] connected 9270 occurrences of 872 variables (average 10.6)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-4] limit 243576 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 1141 literals 18%
c [treelook-4] scheduling used 244771 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 243576 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 267345 steps
c [treelook-4] 1136 literals remain 18%
c [treelook-4] 394 variables remain to probed next time 12%
c [treelook-4] removed 0 variables, found 80 hbrs
c [unhide-9] limit 974306 with penalty 0 = 0 + 0
c [unhide-9-9] 0 units, 0 failed, 205 tauts, 0 hbrs, 472 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 155 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 3212 variables 100%
c [block-5] limit of 25000000 steps penalty 1 = 1 + 0
c [block-5] incomplete 122 not tried 4%
c [block-5] transition to [ all 1 rem 1 ] state
c [block-5] eliminated 0 blocked clauses
c [cce-3] limit of 7500000 steps penalty 2 = 2 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 3750000 steps for small clauses
c [cce-3-1] scheduling 4293 clauses = 3448 binary + 845 ternary
c [cce-3-1] tried to eliminate 121 small clauses 3%
c [cce-3-1] eliminated 13 binary clauses 0%
c [cce-3-1] eliminated 3 ternary clauses 0%
c [cce-3-1] eliminated 16 small clauses 0%
c [cce-3-1] eliminated 16 small clauses in 7504106 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 16 covered clauses in round 1
c [cce-3] eliminated 16 covered clauses in TOTAL during 1 rounds
c [cce-3] 16 < 1/100 * 302065 = 3020 considered unsuccessful
c [elim-9] 264 variables 8% will be scheduled this time
c [elim-9] scheduled 264 variables 8%
c [elim-9] limit of 97430609 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] no variable eliminated in round 1 in 14953224 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 0 = 0% variables out of 264 scheduled
c [sweep-6] limit 1461459 penalty 0 = 0 + 0
c [sweep-6-1] 226 pos 34.4% + 431 neg 65.6% = 657 sched 20.5% ret 2555
c [sweep-6-1] 1502145 steps 101 queries 63.77 avg class size
c [sweep-6-1] 2721 decisions 96 SAT calls 42.81 avg env size
c [sweep-6-1] 398 variables remain 12% (2814 retained 88%)
c [decomp-26] removed 4 variables
c [sweep-6-1] removed 4 vars (0 failed, 4 eqs, 3 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 4 vars in TOTAL (1 rounds, 100 queries)
c [score-distribution-10] 2420 pos 75.44%, 788 min 24.56%, 0 zero 0.00%
c [score-distribution-10] 1105 different 34.45% out of total 3208 variables
c [simplification-10] removed 4 variables 0.1% (3208 remain 2%)
c [simplification-10] removed 1217 irredundant clauses 0.4% (300891 remain 22%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 26666
c [simplification-10] new conflict interval 53332
c [simplification-10] penalized conflict interval 53332 = 1 * 53332
c [simplification-10] hard conflict limit 123100 (soft 96434 + delta 26666)
c [simplification-10] new conflict limit 96434 (hard 123100)
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 -   79.6    3208   298011     65382   18711   3171  3501    9   113   60   8%    602   55    8    5  170%
c 
c [simplification-11] limit of 340 binary hit after 340 binaries
c [quatres-7] found 3887 quaternary clauses 1% in total
c [quatres-7-2] added 54 single-self-subsuming ternary resolvents
c [quatres-7-2] added 31 quaternary resolvents
c [ternres-7] limit 8220365 with penalty 0 = 0 + 0
c [ternres-7] all 3208 free variables schedulable
c [ternres-7] 485 ternary resolvents (31 bin, 454 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-27] removed 1 variables
c [basicprobe-4] limit 41101827 penalty 0 = 0 + 0
c [basicprobe-4-0] 238 sched 7%, 0 failed, 0 lifted, 75 hbrs
c [basicprobe-4-1] 634 sched 20%, 0 failed, 0 lifted, 286 hbrs
c [basicprobe-4-2] 614 sched 19%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-4-3] 614 sched 19%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-4-4] 614 sched 19%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-4-5] 614 sched 19%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-4-6] 614 sched 19%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-7] 614 sched 19%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-7] fully completed probing
c [basicprobe-4-7] removed 0 variables, found 385 hbrs
c [bate-2] eliminated 23 asymmetric tautologies during probing
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 125 transitive binary clauses
c [bca-4] limit of 10000000 steps and 593639 added (scaled 2)
c [bca-4] 1046 out of 6416 literals actually usable 16%
c [bca-4] added 0 blocked clauses in 30973 steps
c [sweep-7] limit 2466109 penalty 0 = 0 + 0
c [sweep-7-1] 134 pos 33.8% + 263 neg 66.2% = 397 sched 12.4% ret 2810
c [sweep-7-1] 2116376 steps 198 queries 21.36 avg class size
c [sweep-7-1] 4306 decisions 182 SAT calls 36.16 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-35] removed 17 variables
c [sweep-7-1] removed 17 vars (0 failed, 16 eqs, 14 impls)
c [sweep-7-2] 1419 pos 44.5% + 1771 neg 55.5% = 3190 sched 100.0% ret 0
c [sweep-7-2] 1206992 steps 35 queries 700.09 avg class size
c [sweep-7-2] 883 decisions 34 SAT calls 40.47 avg env size
c [sweep-7-2] 3079 variables remain 97% (111 retained 3%)
c [sweep-7-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7] removed 17 vars in TOTAL (2 rounds, 231 queries)
c [score-distribution-11] 2404 pos 75.36%, 786 min 24.64%, 0 zero 0.00%
c [score-distribution-11] 1234 different 38.68% out of total 3190 variables
c [simplification-11] removed 18 variables 0.6% (3190 remain 2%)
c [simplification-11] removed 249 irredundant clauses 0.1% (296331 remain 22%)
c [simplification-11] maximum reduction of 1% = max (1%, 0%)
c [simplification-11] forced so keeping old conflict interval 53332
c [simplification-11] conflict limit remains at 96434 (hard 123100)
c [simplification-11] new binary interval 1000
c 
c [simplification-12] limit 96434 conflicts (hard 123100) hit after 96435 conflicts
c [quatres-8] found 3855 quaternary clauses 1% in total
c [quatres-8-1] removed 2 duplicate quaternary clauses
c [quatres-8-1] added 4 double-self-subsuming ternary resolvents
c [quatres-8-2] added 81 single-self-subsuming ternary resolvents
c [quatres-8-2] added 23 quaternary resolvents
c [ternres-8] limit 10378285 with penalty 0 = 0 + 0
c [ternres-8] all 3190 free variables schedulable
c [ternres-8] 436 ternary resolvents (25 bin, 411 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-37] removed 1 variables
c [simpleprobe-5] 1348 schedulable variables 42%
c [simpleprobe-5] limit 41513141 penalty 0 = 0 + 0
c [simpleprobe-5] 1418 variables remain 44% (1771 retained 56%)
c [simpleprobe-5] removed 0 variables, found 263 hbrs, 0 units
c [unhide-10] limit 1037828 with penalty 1 = 1 + 0
c [unhide-10-10] 0 units, 0 failed, 736 tauts, 0 hbrs, 948 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 164 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 3189 variables 100%
c [elim-10] limit of 103782854 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 744 not tried 23% in round 1
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 66 = 2% variables out of 3189 scheduled
c [sweep-8] limit 3113485 penalty 0 = 0 + 0
c [sweep-8-1] 1327 pos 44.0% + 1689 neg 56.0% = 3016 sched 96.6% ret 107
c [sweep-8-1] 3327448 steps 76 queries 338.57 avg class size
c [sweep-8-1] 2967 decisions 75 SAT calls 53.48 avg env size
c [sweep-8-1] 2411 variables remain 77% (712 retained 23%)
c [sweep-8-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-8] removed 0 vars in TOTAL (1 rounds, 75 queries)
c [score-distribution-12] 2473 pos 79.19%, 650 min 20.81%, 0 zero 0.00%
c [score-distribution-12] 1265 different 40.51% out of total 3123 variables
c [simplification-12] removed 67 variables 2.1% (3123 remain 2%)
c [simplification-12] removed 423 irredundant clauses 0.1% (293566 remain 22%)
c [simplification-12] maximum reduction of 2% = max (2%, 0%)
c [simplification-12] geometric conflict interval increment 17777 = 53332 / 3
c [simplification-12] new conflict interval 71109
c [simplification-12] penalized conflict interval 71109 = 1 * 71109
c [simplification-12] hard conflict limit 203098 (soft 167544 + delta 35554)
c [simplification-12] new conflict limit 167544 (hard 203098)
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 -   94.2    3123   291753    112759   22970   2667  3695    9   115   60   8%    819   32    9    6  132%
c -  102.7    3123   287354    160845   29486   2770  3844    7    95   44   8%    926   -2    7    7   94%
c 
c [simplification-13] limit 167544 conflicts (hard 203098) hit after 167545 conflicts
c [quatres-9] found 4104 quaternary clauses 1% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 83 single-self-subsuming ternary resolvents
c [quatres-9-2] added 32 quaternary resolvents
c [ternres-9] limit 16216036 with penalty 0 = 0 + 0
c [ternres-9] all 3123 free variables schedulable
c [ternres-9] 246 ternary resolvents (19 bin, 227 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-40] removed 8 variables
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 153 transitive binary clauses
c [block-6] 122 variables 4% will be scheduled this time
c [block-6] scheduled 122 variables 4%
c [block-6] limit of 40540091 steps penalty 2 = 2 + 0
c [block-6] incomplete 96 not tried 3%
c [block-6] transition to [ all 0 rem 1 ] state
c [block-6] eliminated 0 blocked clauses
c [elim-11] 738 variables 24% will be scheduled this time
c [elim-11] scheduled 738 variables 24%
c [elim-11] limit of 324320728 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 311 not tried 10% in round 1
c [elim-11] transition to [ all 0 rem 1 ] state
c [elim-11] eliminated 0 = 0% variables out of 738 scheduled
c [score-distribution-13] 1651 pos 53.00%, 1464 min 47.00%, 0 zero 0.00%
c [score-distribution-13] 902 different 28.96% out of total 3115 variables
c [simplification-13] removed 8 variables 0.3% (3115 remain 2%)
c [simplification-13] removed 28 irredundant clauses 0.0% (286776 remain 21%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 71109
c [simplification-13] new conflict interval 142218
c [simplification-13] penalized conflict interval 142218 = 1 * 142218
c [simplification-13] hard conflict limit 380872 (soft 309763 + delta 71109)
c [simplification-13] new conflict limit 309763 (hard 380872)
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 -  116.3    3115   282958    216199   39270   3202  3845    7   112   60   6%    982    1    7    7   96%
c -  124.5    3115   279514    266691   45839   3337  3987    7   153   61   5%   1004   38    8    7  107%
c 
c [simplification-14] limit 309763 conflicts (hard 380872) hit after 310763 conflicts
c [quatres-10] found 4704 quaternary clauses 2% in total
c [quatres-10-1] added 6 double-self-subsuming ternary resolvents
c [quatres-10-2] added 216 single-self-subsuming ternary resolvents
c [quatres-10-2] added 32 quaternary resolvents
c [ternres-10] limit 25253783 with penalty 0 = 0 + 0
c [ternres-10] all 3115 free variables schedulable
c [ternres-10] 230 ternary resolvents (29 bin, 201 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 631344 penalty 3 = 3 + 0
c [gauss-4] extracted 2573 xors of average arity 3.0
c [gauss-4] connected 7594 occurrences of 817 variables (average 9.3)
c [gauss-4] limit 631344 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-41] removed 45 variables
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 67 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 157836146 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 208 clauses out of 158093 (0%) of length 9
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 208 large clauses in 157836221 steps
c [cce-4-1] allowing another 78918110 steps for small clauses
c [cce-4-1] scheduling 4406 clauses = 3528 binary + 878 ternary
c [cce-4-1] tried to eliminate 4406 small clauses 100%
c [cce-4-1] eliminated 208 binary clauses 6%
c [cce-4-1] eliminated 112 ternary clauses 13%
c [cce-4-1] eliminated 320 small clauses 7%
c [cce-4-1] eliminated 320 small clauses in 149873416 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 528 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 3981458 steps for small clauses
c [cce-4-2] scheduling 4086 clauses = 3320 binary + 766 ternary
c [cce-4-2] tried to eliminate 235 small clauses 6%
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 528 covered clauses in TOTAL during 2 rounds
c [cce-4] 528 < 1/100 * 277082 = 2770 considered unsuccessful
c [sweep-9] limit 3788067 penalty 1 = 1 + 0
c [sweep-9-1] 1053 pos 44.3% + 1326 neg 55.7% = 2379 sched 77.5% ret 691
c [sweep-9-1] 3790726 steps 63 queries 239.52 avg class size
c [sweep-9-1] 3322 decisions 62 SAT calls 62.92 avg env size
c [sweep-9-1] 1899 variables remain 62% (1171 retained 38%)
c [sweep-9-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-9] removed 0 vars in TOTAL (1 rounds, 62 queries)
c [score-distribution-14] 1256 pos 40.91%, 1814 min 59.09%, 0 zero 0.00%
c [score-distribution-14] 729 different 23.75% out of total 3070 variables
c [simplification-14] removed 45 variables 1.4% (3070 remain 2%)
c [simplification-14] removed 696 irredundant clauses 0.3% (276389 remain 20%)
c [simplification-14] maximum reduction of 1% = max (1%, 0%)
c [simplification-14] geometric conflict interval increment 71109 = 142218 / 2
c [simplification-14] new conflict interval 213327
c [simplification-14] penalized conflict interval 213327 = 1 * 213327
c [simplification-14] hard conflict limit 630753 (soft 524090 + delta 106663)
c [simplification-14] new conflict limit 524090 (hard 630753)
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 -  134.8    3070   276026    318748   52131   3589  4146    7   161   45   5%   1015   39    9    7  122%
c -  143.2    3070   273292    372670   60841   3740  4297    7    96   62   8%   1020  -23    8    7  108%
c -  150.9    3070   271151    423140   68405   3913  4462    8   103   63   8%   1022  -29    9    7  122%
c -  158.8    3070   269280    476772   77133   4115  4624    7   148   63   5%   1023    9    9    7  117%
c 
c [simplification-15] limit 524090 conflicts (hard 630753) hit after 526167 conflicts
c [quatres-11] found 5380 quaternary clauses 2% in total
c [quatres-11-2] added 252 single-self-subsuming ternary resolvents
c [quatres-11-2] added 71 quaternary resolvents
c [ternres-11] limit 38230880 with penalty 0 = 0 + 0
c [ternres-11] all 3070 free variables schedulable
c [ternres-11] 242 ternary resolvents (42 bin, 200 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1194715 penalty 4 = 4 + 0
c [card-5] found 27 at-most-one constraints of average size 3.7
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1194715 for elimination
c [card-5] 27 out of 27 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-43] removed 96 variables
c [treelook-5] limit 955772 penalty 2 = 2 + 0 boost 1
c [treelook-5] scheduled 2074 literals 35%
c [treelook-5] scheduling used 731212 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 955772 penalty 2 = 2 + 0 boost 1
c [treelook-5] used 1037190 steps
c [treelook-5] 2063 literals remain 35%
c [treelook-5] 344 variables remain to probed next time 12%
c [treelook-5] removed 0 variables, found 113 hbrs
c [unhide-11] limit 1911544 with penalty 2 = 2 + 0
c [unhide-11-12] 0 units, 0 failed, 2524 tauts, 0 hbrs, 9522 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 89 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 2974 variables 100%
c [elim-12] limit of 382308807 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 342 not tried 11% in round 1
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 101 = 3% variables out of 2974 scheduled
c [bca-5] limit of 10000000 steps and 531533 added (scaled 2)
c [bca-5] 476 out of 5748 literals actually usable 8%
c [bca-5] added 0 blocked clauses in 102291 steps
c [score-distribution-15] 1674 pos 58.27%, 1199 min 41.73%, 0 zero 0.00%
c [score-distribution-15] 1036 different 36.06% out of total 2873 variables
c [simplification-15] removed 197 variables 6.4% (2873 remain 2%)
c [simplification-15] removed 2092 irredundant clauses 0.8% (265496 remain 20%)
c [simplification-15] maximum reduction of 6% = max (6%, 1%)
c [simplification-15] large reduction 6% >= 5% limit
c [simplification-15] next conflict interval 5261 = min (526167/100, 213327)
c [simplification-15] penalized conflict interval 5261 = 1 * 5261
c [simplification-15] hard conflict limit 541428 (soft 531428 + delta 10000)
c [simplification-15] new conflict limit 531428 (hard 541428)
c 
c [simplification-16] limit 531428 conflicts (hard 541428) hit after 532313 conflicts
c [quatres-12] found 4836 quaternary clauses 2% in total
c [quatres-12-1] removed 9 duplicate quaternary clauses
c [quatres-12-1] added 11 double-self-subsuming ternary resolvents
c [quatres-12-2] added 44 single-self-subsuming ternary resolvents
c [quatres-12-2] added 59 quaternary resolvents
c [ternres-12] limit 38579947 with penalty 0 = 0 + 0
c [ternres-12] all 2873 free variables schedulable
c [ternres-12] 203 ternary resolvents (19 bin, 184 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-5] limit 1928997 penalty 2 = 2 + 0
c [gauss-5] extracted 4306 xors of average arity 3.4
c [gauss-5] connected 14554 occurrences of 1233 variables (average 11.8)
c [gauss-5] limit 1928997 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-45] removed 9 variables
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 67 transitive binary clauses
c [elim-13] 247 variables 9% will be scheduled this time
c [elim-13] scheduled 247 variables 9%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] no variable eliminated in round 1 in 4489789882 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 0 = 0% variables out of 247 scheduled
c [score-distribution-16] 1767 pos 61.70%, 1097 min 38.30%, 0 zero 0.00%
c [score-distribution-16] 980 different 34.22% out of total 2864 variables
c [simplification-16] removed 9 variables 0.3% (2864 remain 2%)
c [simplification-16] removed 60809 irredundant clauses 22.9% (204412 remain 15%)
c [simplification-16] maximum reduction of 23% = max (0%, 23%)
c [simplification-16] large reduction 23% >= 5% limit
c [simplification-16] next conflict interval 5323 = min (532313/100, 213327)
c [simplification-16] penalized conflict interval 5323 = 1 * 5323
c [simplification-16] hard conflict limit 547636 (soft 537636 + delta 10000)
c [simplification-16] new conflict limit 537636 (hard 547636)
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 -  224.9    2864   204397    542124   78560   3161  4332    7    87   40   8%   1024  -49    7    7   90%
c 
c [simplification-17] limit 537636 conflicts (hard 547636) hit after 544461 conflicts
c [quatres-13] found 4785 quaternary clauses 2% in total
c [quatres-13-1] added 5 double-self-subsuming ternary resolvents
c [quatres-13-2] added 21 single-self-subsuming ternary resolvents
c [quatres-13-2] added 6 quaternary resolvents
c [ternres-13] limit 39180866 with penalty 0 = 0 + 0
c [ternres-13] all 2864 free variables schedulable
c [ternres-13] 41 ternary resolvents (11 bin, 30 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-46] removed 3 variables
c [basicprobe-5] limit 97952165 penalty 1 = 1 + 0
c [basicprobe-5-0] 641 sched 22%, 0 failed, 0 lifted, 346 hbrs
c [basicprobe-5-1] 608 sched 21%, 0 failed, 0 lifted, 10 hbrs
c [basicprobe-5-2] 607 sched 21%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-5-3] 607 sched 21%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-3] fully completed probing
c [basicprobe-5-3] removed 0 variables, found 357 hbrs
c [bate-3] eliminated 4 asymmetric tautologies during probing
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 99 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 2861 variables 100%
c [block-7] limit of 48976082 steps penalty 3 = 3 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 8 blocked clauses
c [block-7] 8 < 1/100 * 204341 = 2043 considered unsuccessful
c [sweep-10] limit 2938564 penalty 2 = 2 + 0
c [sweep-10-1] 761 pos 42.5% + 1028 neg 57.5% = 1789 sched 62.6% ret 1071
c [sweep-10-1] 2940940 steps 63 queries 218.98 avg class size
c [sweep-10-1] 2408 decisions 63 SAT calls 47.46 avg env size
c [sweep-10-1] 1514 variables remain 53% (1346 retained 47%)
c [decomp-50] removed 3 variables
c [sweep-10-1] removed 3 vars (0 failed, 3 eqs, 1 impls)
c [sweep-10] removed 3 vars in TOTAL (1 rounds, 62 queries)
c [score-distribution-17] 1504 pos 52.64%, 1353 min 47.36%, 0 zero 0.00%
c [score-distribution-17] 794 different 27.79% out of total 2857 variables
c [simplification-17] removed 7 variables 0.2% (2857 remain 2%)
c [simplification-17] removed 115 irredundant clauses 0.1% (204262 remain 15%)
c [simplification-17] maximum reduction of 0% = max (0%, 0%)
c [simplification-17] full geometric conflict interval increment 213327
c [simplification-17] new conflict interval 426654
c [simplification-17] penalized conflict interval 426654 = 1 * 426654
c [simplification-17] hard conflict limit 1184442 (soft 971115 + delta 213327)
c [simplification-17] new conflict limit 971115 (hard 1184442)
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 -  235.9    2857   204236    598937   87495   3486  4770    8    95   56   8%   1024  -26    9    7  118%
c i  237.2    2856   204233    609395   94628   3583  4816    7   113   60   6%   1024   -6    4    7   61%
c -  244.2    2850   204196    659448   97945   3853  5005    7    85   56   8%  -3437  -27    6    7   83%
c i  248.7    2849   204170    694277  124522   3995  5101    7   138   62   5%  -1598   17    5    7   66%
c -  251.6    2843   204133    715517  106627   4091  5179    8   157   43   5%  -1846   31    8    7  106%
c -  260.1    2843   204051    776396  116714   4403  5377    8   150   44   5%   -110   14    8    7  113%
c 
c [simplification-18] limit of 2745 ternary hit after 2820 ternaries
c [quatres-14] found 6550 quaternary clauses 2% in total
c [quatres-14-1] added 4 double-self-subsuming ternary resolvents
c [quatres-14-2] added 393 single-self-subsuming ternary resolvents
c [quatres-14-2] added 82 quaternary resolvents
c [ternres-14] limit 52284099 with penalty 0 = 0 + 0
c [ternres-14] all 2843 free variables schedulable
c [ternres-14] 245 ternary resolvents (34 bin, 211 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-51] removed 211 variables
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 116 transitive binary clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 2646 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14] incomplete 272 not tried 10% in round 1
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 90 = 3% variables out of 2646 scheduled
c [score-distribution-18] 1478 pos 57.82%, 1078 min 42.18%, 0 zero 0.00%
c [score-distribution-18] 913 different 35.72% out of total 2556 variables
c [simplification-18] removed 287 variables 10.1% (2556 remain 1%)
c [simplification-18] removed 5908 irredundant clauses 2.9% (198141 remain 15%)
c [simplification-18] maximum reduction of 10% = max (10%, 3%)
c [simplification-18] forced so keeping old conflict interval 426654
c [simplification-18] conflict limit remains at 971115 (hard 1184442)
c [simplification-18] new ternary interval 10000
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  265.5    2555   198141    784651  104023   3690  4544    8   134   45   6%     24   -4    6    7   83%
c i  265.8    2554   198141    786685  105271   3716  4558    7   121   59   6%  -1139  -16    5    7   65%
c -  272.0    2548   198087    839935  111030   3927  4681    7    91   44   8%    -37  -51    8    7  112%
c i  272.4    2547   198087    844436  114030   3966  4702    7   134   48   5%     33   -6    4    7   62%
c i  276.8    2540   198052    879368  141209   4098  4802    8   143   51   5%    -95    2    8    7  111%
c -  279.9    2534   198039    899394  119364   4175  4842    7   175   44   4%   -209   33    8    7  117%
c i  283.4    2533   198008    928482  140537   4273  4895    7   126   65   5%    233  -20    5    7   69%
c i  284.0    2526   197997    933146  143779   4321  4915    7    96   49   7%   -431  -49    5    7   72%
c i  285.3    2519   197992    944140  151899   4383  4956    7    80   66   9%   -276  -58    5    7   70%
c i  285.8    2512   197984    948140  154624   4400  4969    7    93   66   7%   -359  -43    5    7   65%
c i  286.7    2505   197984    954689  159109   4444  4986    7    54   66  12%   -288  -76    4    7   59%
c -  288.2    2499   197984    964915  129503   4472  5003    7    44   45  15%   -188  -77    6    7   81%
c i  288.5    2498   197981    967252  130962   4507  5012    6    44   50  14%   -145  -75    5    7   68%
c i  289.1    2490   197979    975187  136379   4544  5022    7    43   50  16%   -188  -71    5    7   67%
c i  289.1    2489   197979    975897  136609   4571  5026    7    37   50  18%   -237  -76    5    7   70%
c i  289.2    2488   197979    976350  136730   4589  5032    7    34   50  19%   -254  -78    5    7   69%
c i  289.2    2487   197979    976488  136743   4602  5036    7    33   50  20%   -259  -79    5    7   65%
c i  289.2    2485   197979    976520  136744   4608  5038    7    33   50  20%   -259  -79    5    7   64%
c i  289.2    2484   197979    976531  136742   4611  5041    7    33   50  20%   -260  -79    4    7   63%
c i  289.2    2476   197979    976535  136741   4611  5041    7    33   50  20%   -260  -79    4    7   62%
c i  289.2    2474   197979    976537  136741   4611  5041    7    33   50  20%   -260  -79    4    7   62%
c i  289.2    2472   197979    976538  136741   4611  5041    7    33   50  20%   -260  -79    4    7   62%
c 0  289.2    2451   197979    976538  136741   4611  5041    7    33   50  20%   -260  -79    4    7   62%
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 
s UNSATISFIABLE
c
c bate: 83 basic ate = 62 trn 75% + 21 lrg 25% in 3 updates
c bcas: 5 count, 82 added (2 skipped), 208313 steps
c bkwd: tried 29400 clauses, 58569 lits, 1.99 lits/clause
c bkwd: checked 30684268 occs, 1043.68 occs/clause, 523.90 occs/lit
c bkwd: subsumed 0 binary, 17 ternary, 99 large
c bkwd: strengthened 0 binary, 1 ternary (100% self), 163 large (0% self)
c blkd: 7 bces, 33425 removed, 688740986 resolutions, 725121989 steps
c blkd: 8495 blocking literals 2%, 4615 pure
c bump: 889924 bumped seen, 20753277 lits 23.3 on average
c card: 5 count, 0 units, 0 am1, 8652325 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 222 subsumed
c card: 146 at-most-one constraints found, average size 3.37
c card: 146 at-most-one constraints used 100%, average size 3.37
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, 994 eliminated, 994 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: 5929527 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 87 gcs, 0 rescored clauses, 468 rescored vars
c dcps: 51 decompositions, 39466 equivalent 14%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 4999054 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 16878317 push, 16602232 pop (16602232 dec 100%)
c dsch: 218165018 swaps, 0 down, 69160030 up
c elms: 14 elims, 105729 eliminated 38%, 847 pure 1%
c elms: 17 rounds, 1.2 rounds/bve
c elms: 64824 small 61%, 35443 large 34%
c elms: 70682 tried small, 64825 succeeded 92%, 5857 failed 8%
c elms: 19999 subsumed, 222854 strengthened, 0 blocked
c elms: 6353001 copies, 87234505 resolutions, 1105287 ipos
c elms: 5281845 subchks, 3948954 strchks
c gaus: 5 extractions, 62449 extracted, 3.0 size, 4 max
c gaus: exported 0 units, 0 binary and 1 ternary equations
c gaus: 1 gc, 12126630 steps, 6063315 extr 50%, 3290086 elim 27%
c glue: 7.4 orig avg, 7.4 real avg, 1.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 29137 = 20101 simple 69% + 8770 trn 30% + 266 lrg 1%, 410 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 889924 clauses, 12.8 length
c lrnd: 11390411 lits = 12348172 orig - 957761 removed 8%
c lrnd: 40824 uips 5%, 818622 flips 92%
c mins: 843295 mins 95%, 1774 bin 0%, 44855 size 5%
c mins: 6711535 poisoned searches, 621261 hits, 9% hit rate
c mins: 17178276 used twice searches, 3872132 hits, 23% hit rate
c move: moved 23048, 715 bin 3%, 22333 trn 97%
c otfs: 99777 driving 44%, 124527 restarting 56%
c otfs: str 224304, 164439 red 73%, 59865 irr 27%
c otfs: str 224304, 0 bin 0%, 1099 trn 0%, 223205 lrg 100%
c otfs: sub 49261, 7360 red 15%, 41901 irr 85%
c otfs: sub 49261, 0 bin 0%, 516 trn 1%, 48745 lrg 99%
c phas: 4 computed, 122688 set, 0 pos (0%), 122688 neg (100%)
c prbs: 5 basic, 19562 probed, 18 failed, 0 lifted
c prbs: 5 simple, 195181 probed, 130 failed, 1060 eqs
c prbs: 5 treelook, 35 probed, 0 failed, 0 lifted
c prom: 144426 locked 30% out of 479374 tried
c prps: 65915337 props, 13 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 14 count, 1010 quat, 1951 self1, 38 self2, 70 dup
c redc: 9336 clauses 2%, 437992 tried 45%, 5 sat 0%
c redc: 10497 lits 0%, 4082315 tried 33%, 5 sat 0%
c redc: 165 times jump level reduced, 10.6 levels on average
c reds: 17 count, 57443.4 conflicts per reduce
c reds: 0 memlim 0%, 17 arith 100%
c reds: 493062 collected 88%, 68338 retired 12%
c rmbd: 3202 removed, 1061 red 33%
c rsts: 26935 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 18 count, 14 confs 78%, 0 vars 0%
c simp: 2 its 11%, 1 bin 6%, 1 trns 6%
c subl: 889924 count (275229 tried 0.3), 131141 sub out of 884075 (14.8%)
c swps: 10 count, 11 rounds, 943 queries (85.7/round)
c swps: 926 sat calls, 9 unsat (14.2% success rate)
c swps: 32539 decisions 35.1, 13163 conflicts 14.2
c swps; 211.6 avg class size, 43.5 avg environment size
c swps: 0 failed, 27 impls, 26 equivs
c swp0: 310 type 0 queries, 23 unsat (7.4%), 304 sat (98.1%)
c swp1: 633 type 1 queries, 72 unsat (11.4%), 613 sat (96.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: 11779351 calls to obtain time
c tops: 129249 fixed 46%, 134 its, 7287.60 confs/it
c trds: 14 transitive reductions, 1613 removed, 4 failed
c trds: 94640 nodes, 90075 edges, 3347243 steps
c trim: 723858 words, 2.8 MB
c trnr: 14 count, 5701 bin, 48604 trn, 54350324 steps
c unhd: 11 count, 12 rounds, 27504139 steps
c unhd: 1542 non-trivial sccs of average size 2.0
c unhd: 95 units, 42 bin, 53 trn, 0 lrg
c unhd: 709 failed, 689 stamp, 0 lits, 1 bin, 18 trn, 0 lrg
c unhd: 9180 tauts, 39 bin 0%, 5124 trn 56%, 2551 lrg 28%
c unhd: 9180 tauts, 1466 stamp 16%, 6339 red 69%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 19952 str, 42 bin 0%, 4188 trn 21%, 15722 lrg 79%, 11807 red 59%
c vars: 4675 remaining 2% and 274444 removed 98% out of 279119
c vars: 129249 fixed 46%, 105729 eliminated 38%, 39466 equivalent 14%
c vsts: 6249541912 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 95.3 search visits per propagation, 6339.3 per conflict
c wchs: 3456770135 pushed, 12343142 enlarged, 256 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         885085        493062         68338       4718586       2383606        344544
c 
c  0 0        171712  19      5909   1         0   0   2135649  45    790075  33     98900  29     4.0
c  1 5        127788  14     75919  15     11610  17    748172  16<   397220  17<    54267  16     0.8
c  2 6        357098  40<   252487  51<    30890  45<  1466940  31    838285  35    127996  37<    1.8
c  3 9        162779  18    114981  23     15300  22    271474   6    268564  11     46755  14     1.0
c  4 14        54080   6     36692   7      7877  12     79808   2     76150   3     14172   4     0.4
c  5 21         9416   1      5823   1      2048   3     13646   0     11200   0      2145   1     0.1
c  6 30         1704   0       990   0       445   1      2245   0      1699   0       266   0     0.0
c  7 41          366   0       188   0       120   0       474   0       299   0        31   0     0.0
c  8 54          102   0        54   0        34   0       132   0        84   0         8   0     0.0
c  9 69           22   0         7   0         8   0        24   0        16   0         2   0     0.0
c 10 86           18   0        12   0         6   0        22   0        14   0         2   0     0.0
c 
c avg                  1.8           2.3           2.4           1.0           1.4           1.5
c std                  1.2           0.9           1.1           1.1           1.2           1.2
c 
c   86.636  30% elim
c   30.845  11% block
c    7.134   2% probe
c    4.359   2% decide
c    3.209   1% cce
c    2.483   1% sweep
c    2.352   1% unhide
c    1.121   0% gauss
c 
c    3.629 < 1% rest (below)
c 
c    1.098   0% bump
c    0.810   0% bca
c    0.639   0% transred
c    0.495   0% quatres
c    0.430   0% ternres
c    0.097   0% card
c    0.062   0% rescore
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    4.263   1% preprocessing     3%
c  137.802  48% inprocessing     97%
c ==================================
c  142.065  49% simplifying
c  147.123  51% search
c ==================================
c  289.194 100% all
c 
c        976538 conflicts,        3376.8 confs/sec
c          3616 ternaries,         270.1 confs/ternary
c          1994 binaries,          489.7 confs/binary
c           134 iterations,       7287.6 confs/iteration
c 
c            17 reductions,          0.1 redus/sec,  57443.4 confs/reduction
c         26935 restarts,           93.1 rests/sec,     36.3 confs/restart
c       4999054 decisions,       17286.2 decis/sec,      5.1 decis/conflict
c      65915337 propagations,   227928.0 props/sec,     13.2 props/decision
c 
c 289.2 seconds, 147.5 MB
c launch: done
