c launch: /data/cnf/sc2014/app/post-cbmc-aes-ee-r2-noholes.cnf.bz2
c host: atom18
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 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 fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/post-cbmc-aes-ee-r2-noholes.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/post-cbmc-aes-ee-r2-noholes.cnf.bz2
c no embedded options
c found 'p cnf 266199 1575975' header
c read 266199 variables, 1575975 clauses, 4240496 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 --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 163710 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 
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  163710  1328859         0       0      0     0    0     0   64   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 145467 variables
c [simpleprobe-1] all 120732 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 2785 variables
c [simpleprobe-1] 69724 variables remain 59% (48223 retained 41%)
c [simpleprobe-1] removed 2785 variables, found 14386 hbrs, 30 units
c [unhide-1] limit 58152 based on 930438 irredundant clauses
c [unhide-1-1] 32 units, 216 failed, 1758 tauts, 0 hbrs, 1849 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 111231 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 66246 not tried 60% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 39985 = 36% variables out of 111231 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 777050 negative 99.9% of 777975 except 925 0.1%
c [phase-count-1] 483029 positive 62.1% of 777975 except 294946 37.9%
c [phase-count-1] less non-negative clauses 925 than limit 77700 (10.0%)
c [phase-count-1] non-pos/non-neg = 294946/925 = 318.86 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 71246 negative 100%
c [sort-queue-1] sorted 71246 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 71246 (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 81458 variables 53.3% (71246 remain 44%)
c [simplification-1] removed 550884 irredundant clauses 41.5% (777975 remain 59%)
c [simplification-1] maximum reduction of 53% = max (53%, 41%)
c [simplification-1] large reduction 53% >= 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.5   71245   777975        31      25      0  1851    0     1   42   6%      0    1    1    0 24228%
c i    4.5   71234   777975        60      30      1  1853    0     1   42   9%      0    1    1    0 22677%
c i    4.5   71132   777975        61      30      1  1853    0     1   42   9%      0    1    1    0 22589%
c i    4.5   71117   777975        79      35     12  1854    0     1   42   9%      0    1    1    0 21432%
c i    4.5   71103   777975        80      35     12  1854    0     1   42   9%      0    1    1    0 21348%
c i    4.5   71090   777975        85      36     12  1855    0     1   42  10%      0    1    1    0 21163%
c i    4.5   71048   777975       125      55     15  1859    0     1   42  10%      0    1    2    0 19947%
c i    4.5   71039   777975       151      63     27  1861    0     1   42  10%      0    1    2    0 18559%
c i    4.5   71037   777975       152      63     27  1861    0     1   42  10%      0    1    2    0 18487%
c i    4.5   71025   777975       156      65     28  1861    0     1   42  10%      0    1    2    0 18235%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 949 variables
c [simpleprobe-2] 38945 schedulable variables 55%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 897 variables
c [simpleprobe-2] 37029 variables remain 53% (32371 retained 47%)
c [simpleprobe-2] removed 897 variables, found 572 hbrs, 46 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 27089 literals 20%
c [treelook-1] scheduling used 304010 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 302686 steps
c [treelook-1] 27063 literals remain 19%
c [treelook-1] 26140 variables remain to probed next time 38%
c [decomp-5] removed 226 variables
c [treelook-1] removed 226 variables, found 9 hbrs
c [basicprobe-1] limit 6111560 based on 763945 irredundant clauses
c [basicprobe-1-0] 36098 probes remain 52% after last round
c [basicprobe-1-0] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 11 variables, found 1849 hbrs
c [unhide-2] limit 50000 with penalty 1 = 0 + 1
c [unhide-2-2] 40 units, 365 failed, 58 tauts, 0 hbrs, 2474 literals
c [elim-2] 62681 variables 92% will be scheduled this time
c [elim-2] scheduled 62681 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 42618 not tried 63% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 20089 = 32% variables out of 62681 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 657216 negative 99.9% of 658031 except 815 0.1%
c [phase-count-2] 420648 positive 63.9% of 658031 except 237383 36.1%
c [phase-count-2] less non-negative clauses 815 than limit 65800 (10.0%)
c [phase-count-2] non-pos/non-neg = 237383/815 = 291.27 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 18546 negative 100%
c [sort-queue-2] sorted 47715 enqueued variables after 156 conflicts
c [score-dist-2] active 0 (0%), one 140 (0%), zero 47575 (100%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 23170 variables 32.7% (47715 remain 29%)
c [simplification-2] removed 119944 irredundant clauses 15.4% (658031 remain 50%)
c [simplification-2] maximum reduction of 33% = max (33%, 15%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1034 (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.3   47714   658031       216      54     15  2185    0     4   39   6%      0    4    2    0 17139%
c i    7.3   47713   658031       217      54     15  2185    0     4   39   6%      0    4    2    0 17073%
c i    7.3   47701   658031       247      70     22  2186    0     4   39   6%      0    4    2    0 15923%
c i    7.3   47693   658031       256      75     24  2187    0     4   39   6%      0    4    2    0 15536%
c i    7.3   47670   658031       257      75     24  2187    0     4   39   6%      0    4    2    0 15476%
c i    7.3   47590   658031       260      76     25  2187    0     4   39   6%      0    4    2    0 15326%
c i    7.3   47581   658031       261      76     25  2187    0     4   39   6%      0    4    2    0 15266%
c i    7.3   47567   658031       330     120     37  2192    0     5   39   7%      0    5    3    0 14224%
c i    7.3   47560   658031       331     120     37  2192    0     5   39   7%      0    5    3    0 14169%
c i    7.3   47552   658031       355     127     47  2194    0     5   39   7%      0    5    3    0 13482%
c i    7.3   47543   658030       395     156     53  2195    0     6   39   6%      0    6    3    0 13491%
c i    7.3   47538   658029       405     160     55  2196    0     6   39   6%      0    6    3    0 13234%
c i    7.3   47530   658029       433     165     68  2200    0     6   39   7%      0    6    3    0 12357%
c i    7.3   47522   658028       463     175     81  2203    0     8   39   5%      0    8    3    0 11677%
c i    7.3   47521   658028       469     176     83  2204    0     8   39   5%      0    8    3    0 11499%
c i    7.3   47508   658028       482     179     91  2205    0     8   39   5%      0    8    3    0 11065%
c i    7.3   47507   658027       505     184    107  2205    0     9   39   5%      0    9    3    0 10472%
c i    7.3   47505   658027       513     187    111  2205    0     9   39   5%      0    9    3    0 10461%
c i    7.3   47500   658027       539     195    120  2210    0     9   39   5%      0    9    3    0 9920%
c i    7.3   47494   658027       549     198    122  2212    0     9   39   5%      0    9    3    0 9697%
c i    7.4   47391   658027       669     280    139  2224    1    20   39   3%      0   20    3    0 9118%
c i    7.4   47390   658027       670     280    139  2224    1    20   39   3%      0   20    3    0 9083%
c i    7.4   47381   658027       674     280    140  2225    1    20   39   3%      0   20    3    0 8983%
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.4   47380   658027       676     280    140  2226    1    20   39   3%      0   20    3    0 8920%
c i    7.4   47378   658027       677     280    140  2226    1    20   39   3%      0   20    3    0 8886%
c i    7.4   47370   658027       679     280    140  2226    1    20   39   3%      0   20    3    0 8851%
c i    7.4   47361   658027       814     359    176  2232    1    22   39   3%      0   22    3    0 7292%
c i    7.4   47360   658020       957     469    195  2236    1    30   39   3%      0   30    4    0 7564%
c i    7.4   47338   658018      1073     543    224  2241    1    30   39   3%      0   30    4    0 6374%
c 
c [simplification-3] limit 1114 conflicts (hard 11000) hit after 1114 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1 at-most-one constraints of average size 4.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 1 out of 1 constraints (100%) meet size limits
c [card-2] found 5 units
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 777 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 19254 literals 21%
c [treelook-2] scheduling used 300156 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 318972 steps
c [treelook-2] 19238 literals remain 20%
c [treelook-2] 16964 variables remain to probed next time 36%
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 16 units, 200 failed, 1930 tauts, 0 hbrs, 1394 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 46329 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 21137 not tried 46% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 19445 = 42% variables out of 46329 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 26884 enqueued variables after 1114 conflicts
c [score-dist-3] active 0 (0%), one 1273 (5%), zero 25611 (95%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 20422 variables 43.2% (26884 remain 16%)
c [simplification-3] removed 114801 irredundant clauses 17.4% (543217 remain 41%)
c [simplification-3] maximum reduction of 43% = max (43%, 17%)
c [simplification-3] large reduction 43% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13114 (soft 3114 + delta 10000)
c [simplification-3] new conflict limit 3114 (hard 13114)
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    9.7   26883   543215      1154     244     40   494    1    33   37   3%      0   33    4    0 6112%
c i    9.9   26877   543181      1909     889     77   517    2    71   37   3%      4   70    6    0 4690%
c i   10.0   26858   543148      2769    1583     87   559    3    63   37   4%      6   62    7    0 3151%
c 
c [simplification-4] limit 3114 conflicts (hard 13114) hit after 3115 conflicts
c [decomp-7] removed 62 variables
c [basicprobe-2] limit 4342128 based on 542766 irredundant clauses
c [basicprobe-2-0] 22302 probes remain 83% after last round
c [basicprobe-2-0] removed 0 variables, found 1184 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 13 units, 34 failed, 43 tauts, 0 hbrs, 576 literals
c [elim-4] 20604 variables 77% will be scheduled this time
c [elim-4] scheduled 20604 variables 77%
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 17693 variables 66% in round 1 in 239203274 steps
c [elim-4-1] backward subsumption/strengthening limit 160796726
c [elim-4-1-1] backward checking 2867 touched variables 11%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 11 and strengthened 61 clauses in 64202534 steps
c [elim-4-1] rescheduled 326 variables 1% by backward subsumption
c [elim-4-2] eliminated 32 variables 0% in round 2 in 3327271 steps
c [elim-4-2] backward subsumption/strengthening limit 3327200
c [elim-4-2-1] backward checking 268 touched variables 1%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 3 and strengthened 6 clauses in 1519017 steps
c [elim-4-2] rescheduled 20 variables 0% by backward subsumption
c [elim-4-3] eliminated 2 variables 0% in round 3 in 84134 steps
c [elim-4-3] backward subsumption/strengthening limit 84100
c [elim-4-3-1] backward checking 12 touched variables 0%
c [elim-4-3-1] incomplete backward checking 0 remain 0%
c [elim-4-3] subsumed 0 and strengthened 0 clauses in 84101 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 17731 = 86% variables out of 20604 scheduled
c [sort-queue-4] sorted 9033 enqueued variables after 3115 conflicts
c [score-dist-4] active 0 (0%), one 1975 (22%), zero 7058 (78%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 17821 variables 66.4% (9033 remain 6%)
c [simplification-4] removed 155536 irredundant clauses 28.6% (387602 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 15115 (soft 5115 + delta 10000)
c [simplification-4] new conflict limit 5115 (hard 15115)
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   17.4    9032   387377      4670    1701    122   191    4    87   47   5%     17   84    8    0 1980%
c 
c [simplification-5] limit 5115 conflicts (hard 15115) hit after 5116 conflicts
c [quatres-1] found 4457 quaternary clauses 1% in total
c [quatres-1-2] added 59 single-self-subsuming ternary resolvents
c [quatres-1-2] added 33 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 9031 free variables schedulable
c [ternres-1] 44230 ternary resolvents (4914 bin, 39316 trn)
c [ternres-1] 215 variables remain 2% (8816 retained 98%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 48611 xors of average arity 2.9
c [gauss-1] connected 139410 occurrences of 6558 variables (average 21.3)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-8] removed 1103 variables
c [simpleprobe-3] 4131 schedulable variables 52%
c [simpleprobe-3] limit 2411738 penalty 0 = 0 + 0
c [decomp-9] removed 8 variables
c [simpleprobe-3] 4116 variables remain 52% (3804 retained 48%)
c [simpleprobe-3] removed 8 variables, found 52 hbrs, 1 units
c [unhide-5] limit 120586 with penalty 0 = 0 + 0
c [unhide-5-5] 1 units, 5 failed, 39 tauts, 0 hbrs, 89 literals
c [transred-1] limit 602934 with penalty 0 = 0 + 0
c [transred-1] removed 14 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 7915 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] incomplete 25 not tried 0%
c [block-1] transition to [ all 1 rem 1 ] state
c [block-1] eliminated 31214 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 24 clauses out of 406 (6%) of length 10
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 24 large clauses in 30002657 steps
c [cce-1-1] allowing another 15001328 steps for small clauses
c [cce-1-1] scheduling 5030 clauses = 4401 binary + 629 ternary
c [cce-1-1] tried to eliminate 1031 small clauses 20%
c [cce-1-1] eliminated 305 binary clauses 7%
c [cce-1-1] eliminated 10 ternary clauses 2%
c [cce-1-1] eliminated 315 small clauses 6%
c [cce-1-1] eliminated 315 small clauses in 30000279 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 339 covered clauses in round 1
c [cce-1] eliminated 339 covered clauses in TOTAL during 1 rounds
c [cce-1] 339 < 1/100 * 355887 = 3558 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 3677 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 1745 not tried 47% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 128 = 3% variables out of 3677 scheduled
c [bca-1] limit of 10000000 steps and 710732 added (scaled 2)
c [bca-1] 4535 out of 7100 literals actually usable 64%
c [bca-1] added 248 blocked clauses in 35029 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1429 pos 40.3% + 2120 neg 59.7% = 3549 sched 100.0% ret 0
c [sweep-1-1] 1004444 steps 59 queries 704.78 avg class size
c [sweep-1-1] 1108 decisions 54 SAT calls 23.69 avg env size
c [sweep-1-1] 3350 variables remain 94% (198 retained 6%)
c [decomp-10] removed 19 variables
c [sweep-1-1] removed 19 vars (0 failed, 4 eqs, 6 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 19 vars in TOTAL (1 rounds, 58 queries)
c [sort-queue-5] sorted 3530 enqueued variables after 5116 conflicts
c [score-dist-5] active 0 (0%), one 2903 (82%), zero 627 (18%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 5501 variables 60.9% (3530 remain 2%)
c [simplification-5] removed 32331 irredundant clauses 8.3% (354989 remain 27%)
c [simplification-5] maximum reduction of 61% = max (61%, 8%)
c [simplification-5] large reduction 61% >= 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 17116 (soft 7116 + delta 10000)
c [simplification-5] new conflict limit 7116 (hard 17116)
c 
c [simplification-6] limit 7116 conflicts (hard 17116) hit after 7116 conflicts
c [quatres-2] found 4186 quaternary clauses 1% in total
c [quatres-2-2] added 165 single-self-subsuming ternary resolvents
c [quatres-2-2] added 167 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] 102 schedulable variables 3%
c [ternres-2] 166 ternary resolvents (7 bin, 159 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 66 at-most-one constraints of average size 3.9
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 66 out of 66 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [unhide-6] limit 153847 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 9 failed, 50 tauts, 0 hbrs, 267 literals
c [transred-2] limit 769235 with penalty 0 = 0 + 0
c [transred-2] removed 11 transitive binary clauses
c [block-2] 25 variables 1% will be scheduled this time
c [block-2] scheduled 25 variables 1%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] incomplete 14 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] 1745 variables 49% will be scheduled this time
c [elim-6] scheduled 1745 variables 49%
c [elim-6] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 1464 not tried 42% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 2 = 0% variables out of 1745 scheduled
c [elim-6] 2 < 1/100 * 1745 = 17 considered unsuccessful
c [bca-2] limit of 10000000 steps and 709488 added (scaled 2)
c [bca-2] 3582 out of 7050 literals actually usable 51%
c [bca-2] added 0 blocked clauses in 28351 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1410 pos 42.3% + 1922 neg 57.7% = 3332 sched 94.6% ret 192
c [sweep-2-1] 1084971 steps 63 queries 513.95 avg class size
c [sweep-2-1] 1431 decisions 62 SAT calls 28.58 avg env size
c [sweep-2-1] 3067 variables remain 87% (457 retained 13%)
c [decomp-12] removed 20 variables
c [sweep-2-1] removed 20 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 20 vars in TOTAL (1 rounds, 62 queries)
c [sort-queue-6] sorted 3504 enqueued variables after 7116 conflicts
c [score-dist-6] active 0 (0%), one 3168 (90%), zero 336 (10%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 26 variables 0.7% (3504 remain 2%)
c [simplification-6] removed 339 irredundant clauses 0.1% (354282 remain 27%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 10000
c [simplification-6] penalized conflict interval 10000 = 1 * 10000
c [simplification-6] hard conflict limit 27116 (soft 17116 + delta 10000)
c [simplification-6] new conflict limit 17116 (hard 27116)
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   42.1    3503   354179      7683    4471    583  1025    6    90   46   7%     32   84    9    1 1229%
c i   42.6    3502   353572     11814    7801    614  1045    7    79   46   9%     47   69    8    1  730%
c 
c [simplification-7] limit 17116 conflicts (hard 27116) hit after 17117 conflicts
c [quatres-3] found 4153 quaternary clauses 1% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 73 single-self-subsuming ternary resolvents
c [quatres-3-2] added 32 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3502 free variables schedulable
c [ternres-3] 2554 ternary resolvents (123 bin, 2431 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 7511 xors of average arity 3.3
c [gauss-2] connected 24995 occurrences of 2019 variables (average 12.4)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] connected 4857 occurrences of 2019 variables (average 2.4)
c [gauss-2] fully completed
c [decomp-13] removed 20 variables
c [gauss-2] exported 0 unary, 2 binary and 0 ternary equations
c [treelook-3] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 586 literals 8%
c [treelook-3] scheduling used 150068 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 309894 steps
c [treelook-3] 571 literals remain 8%
c [treelook-3] 366 variables remain to probed next time 11%
c [treelook-3] removed 0 variables, found 75 hbrs
c [unhide-7] limit 303023 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 0 failed, 152 tauts, 0 hbrs, 154 literals
c [transred-3] limit 1515118 with penalty 0 = 0 + 0
c [transred-3] removed 48 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 3482 variables 100%
c [block-3] limit of 50000000 steps penalty 0 = 0 + 0
c [block-3] incomplete 120 not tried 3%
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] eliminated 3 clauses out of 312632 (0%) of length 9
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 3 large clauses in 15002428 steps
c [cce-2-1] allowing another 7501214 steps for small clauses
c [cce-2-1] scheduling 4642 clauses = 3827 binary + 815 ternary
c [cce-2-1] tried to eliminate 473 small clauses 10%
c [cce-2-1] eliminated 45 binary clauses 1%
c [cce-2-1] eliminated 13 ternary clauses 2%
c [cce-2-1] eliminated 58 small clauses 1%
c [cce-2-1] eliminated 58 small clauses in 15000892 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 61 covered clauses in round 1
c [cce-2] eliminated 61 covered clauses in TOTAL during 1 rounds
c [cce-2] 61 < 1/100 * 352660 = 3526 considered unsuccessful
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1196 pos 39.5% + 1829 neg 60.5% = 3025 sched 86.9% ret 457
c [sweep-3-1] 1613190 steps 40 queries 606.33 avg class size
c [sweep-3-1] 1425 decisions 39 SAT calls 43.49 avg env size
c [sweep-3-1] 2876 variables remain 83% (606 retained 17%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 39 queries)
c [sort-queue-7] sorted 3482 enqueued variables after 17117 conflicts
c [score-dist-7] active 0 (0%), one 3363 (97%), zero 119 (3%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 20 variables 0.6% (3482 remain 2%)
c [simplification-7] removed 286 irredundant clauses 0.1% (352537 remain 27%)
c [simplification-7] maximum reduction of 1% = max (1%, 0%)
c [simplification-7] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-7] new conflict interval 20000
c [simplification-7] penalized conflict interval 20000 = 1 * 20000
c [simplification-7] hard conflict limit 47117 (soft 37117 + delta 10000)
c [simplification-7] new conflict limit 37117 (hard 47117)
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   48.1    3481   351792     21558   15989   3020  1326    8    88   64   9%    124   69    8    2  437%
c i   49.3    3480   350674     29222   22083   3031  1349    8    94   48   9%     86   69    8    3  307%
c i   50.3    3479   349759     35362   26817   3047  1383    8    91   66   9%     59   60    8    3  281%
c 
c [simplification-8] limit 37117 conflicts (hard 47117) hit after 37118 conflicts
c [quatres-4] found 4071 quaternary clauses 1% in total
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 94 single-self-subsuming ternary resolvents
c [quatres-4-2] added 40 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 3479 free variables schedulable
c [ternres-4] 617 ternary resolvents (48 bin, 569 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 7389 xors of average arity 3.3
c [gauss-3] connected 24491 occurrences of 1969 variables (average 12.4)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] connected 4576 occurrences of 1969 variables (average 2.3)
c [gauss-3] fully completed
c [decomp-17] removed 21 variables
c [gauss-3] exported 0 unary, 3 binary and 0 ternary equations
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 50 transitive binary clauses
c [block-4] 14 variables 0% will be scheduled this time
c [block-4] scheduled 14 variables 0%
c [block-4] limit of 50000000 steps penalty 0 = 0 + 0
c [block-4] incomplete 2 not tried 0%
c [block-4] transition to [ all 0 rem 1 ] state
c [block-4] eliminated 0 blocked clauses
c [block-4] considered successful since not run to completion yet
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 3458 variables 100%
c [elim-7] limit of 34514737 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 1521 not tried 44% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 88 = 3% variables out of 3458 scheduled
c [bca-3] limit of 10000000 steps and 698860 added (scaled 2)
c [bca-3] 1221 out of 6742 literals actually usable 18%
c [bca-3] added 0 blocked clauses in 35188 steps
c [sweep-4] limit 1035442 penalty 0 = 0 + 0
c [sweep-4-1] 1129 pos 40.8% + 1639 neg 59.2% = 2768 sched 82.1% ret 602
c [sweep-4-1] 1037937 steps 29 queries 605.86 avg class size
c [sweep-4-1] 1008 decisions 28 SAT calls 41.57 avg env size
c [sweep-4-1] 2656 variables remain 79% (714 retained 21%)
c [decomp-19] removed 4 variables
c [sweep-4-1] removed 4 vars (0 failed, 0 eqs, 1 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 4 vars in TOTAL (1 rounds, 28 queries)
c [sort-queue-8] sorted 3366 enqueued variables after 37118 conflicts
c [score-dist-8] active 0 (0%), one 3345 (99%), zero 21 (1%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 113 variables 3.2% (3366 remain 2%)
c [simplification-8] removed 585 irredundant clauses 0.2% (348955 remain 26%)
c [simplification-8] maximum reduction of 3% = max (3%, 0%)
c [simplification-8] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-8] new conflict interval 25000
c [simplification-8] penalized conflict interval 25000 = 1 * 25000
c [simplification-8] hard conflict limit 74618 (soft 62118 + delta 12500)
c [simplification-8] new conflict limit 62118 (hard 74618)
c 
c [simplification-9] limit 62118 conflicts (hard 74618) hit after 62119 conflicts
c [quatres-5] found 4027 quaternary clauses 1% in total
c [quatres-5-1] added 3 double-self-subsuming ternary resolvents
c [quatres-5-2] added 159 single-self-subsuming ternary resolvents
c [quatres-5-2] added 168 quaternary resolvents
c [ternres-5] limit 5750025 with penalty 0 = 0 + 0
c [ternres-5] all 3366 free variables schedulable
c [ternres-5] 1597 ternary resolvents (93 bin, 1504 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] extracted 6887 xors of average arity 3.3
c [gauss-4] connected 22784 occurrences of 1816 variables (average 12.5)
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] connected 3693 occurrences of 1816 variables (average 2.0)
c [gauss-4] fully completed
c [decomp-20] removed 3 variables
c [gauss-4] exported 0 unary, 2 binary and 0 ternary equations
c [basicprobe-3] limit 14375064 penalty 1 = 1 + 0
c [basicprobe-3-0] 765 sched 23%, 5 failed, 0 lifted, 2965 hbrs
c [decomp-22] removed 26 variables
c [basicprobe-3-1] 654 sched 20%, 0 failed, 0 lifted, 147 hbrs
c [decomp-23] removed 5 variables
c [basicprobe-3-2] 638 sched 19%, 0 failed, 0 lifted, 20 hbrs
c [basicprobe-3-3] 634 sched 19%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-3-4] 636 sched 19%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-5] 636 sched 19%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-6] 636 sched 19%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-6] fully completed probing
c [basicprobe-3-6] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-3-6] removed 31 variables, found 3137 hbrs
c [bate-1] eliminated 56 asymmetric tautologies during probing
c [unhide-8] limit 575002 with penalty 1 = 1 + 0
c [unhide-8-8] 0 units, 0 failed, 1227 tauts, 0 hbrs, 1155 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 179 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 3332 variables 100%
c [block-5] limit of 57500259 steps penalty 0 = 0 + 0
c [block-5] incomplete 115 not tried 3%
c [block-5] transition to [ all 1 rem 1 ] state
c [block-5] eliminated 9 blocked clauses
c [block-5] considered successful since not run to completion yet
c [elim-8] 1332 variables 40% will be scheduled this time
c [elim-8] scheduled 1332 variables 40%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2300010360 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 878981891 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 1332 scheduled
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 17250070 penalty 0 = 0 + 0
c [sweep-5-1] 1121 pos 42.8% + 1497 neg 57.2% = 2618 sched 78.6% ret 714
c [sweep-5-1] 13858647 steps 482 queries 46.99 avg class size
c [sweep-5-1] 16162 decisions 445 SAT calls 46.69 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-28] removed 41 variables
c [sweep-5-1] removed 41 vars (0 failed, 42 eqs, 40 impls)
c [sweep-5-2] 1438 pos 43.7% + 1853 neg 56.3% = 3291 sched 100.0% ret 0
c [sweep-5-2] 3402311 steps 111 queries 191.29 avg class size
c [sweep-5-2] 4200 decisions 110 SAT calls 50.41 avg env size
c [sweep-5-2] 2343 variables remain 71% (948 retained 29%)
c [decomp-29] removed 1 variables
c [sweep-5-2] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 42 vars in TOTAL (2 rounds, 591 queries)
c [sort-queue-9] sorted 3290 enqueued variables after 62119 conflicts
c [score-dist-9] active 0 (0%), one 3290 (100%), zero 0 (0%)
c [score-dist-9] max exp 1, different 1 (50%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 76 variables 2.3% (3290 remain 2%)
c [simplification-9] removed 44590 irredundant clauses 12.9% (300789 remain 23%)
c [simplification-9] maximum reduction of 13% = max (2%, 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 74119 (soft 64119 + delta 10000)
c [simplification-9] new conflict limit 64119 (hard 74119)
c 
c [simplification-10] limit 64119 conflicts (hard 74119) hit after 64121 conflicts
c [quatres-6] found 3632 quaternary clauses 1% in total
c [quatres-6-1] removed 6 duplicate quaternary clauses
c [quatres-6-2] added 218 single-self-subsuming ternary resolvents
c [quatres-6-2] added 28 quaternary resolvents
c [ternres-6] limit 5981610 with penalty 0 = 0 + 0
c [ternres-6] all 3290 free variables schedulable
c [ternres-6] 769 ternary resolvents (48 bin, 721 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 373850 penalty 3 = 3 + 0
c [card-4] found 10 at-most-one constraints of average size 5.6
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 373850 for elimination
c [card-4] 10 out of 10 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-5] limit 2000000 penalty 0 = 0 + 0
c [gauss-5] extracted 6931 xors of average arity 3.3
c [gauss-5] connected 22715 occurrences of 1778 variables (average 12.8)
c [gauss-5] limit 2000000 penalty 0 = 0 + 0
c [gauss-5] connected 3676 occurrences of 1778 variables (average 2.1)
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-30] removed 1 variables
c [simpleprobe-4] 1825 schedulable variables 55%
c [simpleprobe-4] limit 23926442 penalty 0 = 0 + 0
c [simpleprobe-4] 1794 variables remain 55% (1495 retained 45%)
c [simpleprobe-4] removed 0 variables, found 197 hbrs, 0 units
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 210 transitive binary clauses
c [block-6] 2 variables 0% will be scheduled this time
c [block-6] scheduled 2 variables 0%
c [block-6] limit of 59816105 steps penalty 0 = 0 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] 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 3751187 steps for small clauses
c [cce-3-1] scheduling 4735 clauses = 3732 binary + 1003 ternary
c [cce-3-1] tried to eliminate 145 small clauses 3%
c [cce-3-1] eliminated 7 binary clauses 0%
c [cce-3-1] eliminated 11 ternary clauses 1%
c [cce-3-1] eliminated 18 small clauses 0%
c [cce-3-1] eliminated 18 small clauses in 7500289 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 18 covered clauses in round 1
c [cce-3] eliminated 18 covered clauses in TOTAL during 1 rounds
c [cce-3] 18 < 1/100 * 300513 = 3005 considered unsuccessful
c [sweep-6] limit 1794483 penalty 0 = 0 + 0
c [sweep-6-1] 1068 pos 45.6% + 1273 neg 54.4% = 2341 sched 71.2% ret 948
c [sweep-6-1] 1812351 steps 35 queries 377.66 avg class size
c [sweep-6-1] 1545 decisions 34 SAT calls 56.76 avg env size
c [sweep-6-1] 2174 variables remain 66% (1115 retained 34%)
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 34 queries)
c [sort-queue-10] sorted 3289 enqueued variables after 64121 conflicts
c [score-dist-10] active 0 (0%), one 3289 (100%), zero 0 (0%)
c [score-dist-10] max exp 1, different 1 (50%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 1 variables 0.0% (3289 remain 2%)
c [simplification-10] removed 171 irredundant clauses 0.1% (300365 remain 23%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 25000
c [simplification-10] new conflict interval 50000
c [simplification-10] penalized conflict interval 50000 = 1 * 50000
c [simplification-10] hard conflict limit 139121 (soft 114121 + delta 25000)
c [simplification-10] new conflict limit 114121 (hard 139121)
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 -   77.5    3289   300330     64433   21792   2530  4149    9    87   44  10%    342   41   10    5  203%
c 
c [simplification-11] limit of 451 binary hit after 451 binaries
c [quatres-7] found 3468 quaternary clauses 1% in total
c [quatres-7-2] added 87 single-self-subsuming ternary resolvents
c [quatres-7-2] added 5 quaternary resolvents
c [ternres-7] limit 8727121 with penalty 0 = 0 + 0
c [ternres-7] all 3289 free variables schedulable
c [ternres-7] 202 ternary resolvents (27 bin, 175 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-33] removed 3 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 136 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 3286 variables 100%
c [elim-9] limit of 87271214 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 775 not tried 24% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 64 = 2% variables out of 3286 scheduled
c [bca-4] limit of 10000000 steps and 593310 added (scaled 2)
c [bca-4] 896 out of 6446 literals actually usable 14%
c [bca-4] added 0 blocked clauses in 48172 steps
c [sort-queue-11] sorted 3222 enqueued variables after 95134 conflicts
c [score-dist-11] active 0 (0%), one 3222 (100%), zero 0 (0%)
c [score-dist-11] max exp 1, different 1 (50%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 67 variables 2.0% (3222 remain 2%)
c [simplification-11] removed 329 irredundant clauses 0.1% (296343 remain 22%)
c [simplification-11] maximum reduction of 2% = max (2%, 0%)
c [simplification-11] forced so keeping old conflict interval 50000
c [simplification-11] conflict limit remains at 114121 (hard 139121)
c [simplification-11] 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 -   86.5    3222   294610    113935   29242   2395  3983    8    73   60  11%    704   13    7    6  118%
c 
c [simplification-12] limit 114121 conflicts (hard 139121) hit after 114122 conflicts
c [quatres-8] found 3670 quaternary clauses 1% in total
c [quatres-8-1] removed 2 duplicate quaternary clauses
c [quatres-8-1] added 2 double-self-subsuming ternary resolvents
c [quatres-8-2] added 39 single-self-subsuming ternary resolvents
c [quatres-8-2] added 58 quaternary resolvents
c [ternres-8] limit 10000698 with penalty 0 = 0 + 0
c [ternres-8] all 3222 free variables schedulable
c [ternres-8] 223 ternary resolvents (21 bin, 202 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-6] limit 1000069 penalty 1 = 1 + 0
c [gauss-6] extracted 6159 xors of average arity 3.3
c [gauss-6] connected 20349 occurrences of 1629 variables (average 12.5)
c [gauss-6] limit 1000069 penalty 1 = 1 + 0
c [gauss-6] connected 2478 occurrences of 1629 variables (average 1.5)
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-9] limit 500034 with penalty 2 = 2 + 0
c [unhide-9-9] 0 units, 0 failed, 287 tauts, 0 hbrs, 660 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 130 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 3222 variables 100%
c [block-7] limit of 50003492 steps penalty 1 = 1 + 0
c [block-7] incomplete 110 not tried 3%
c [block-7] transition to [ all 1 rem 1 ] state
c [block-7] eliminated 0 blocked clauses
c [elim-10] 775 variables 24% will be scheduled this time
c [elim-10] scheduled 775 variables 24%
c [elim-10] limit of 200013968 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 474 not tried 15% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 0 = 0% variables out of 775 scheduled
c [sweep-7] limit 1500104 penalty 1 = 1 + 0
c [sweep-7-1] 859 pos 40.5% + 1260 neg 59.5% = 2119 sched 65.8% ret 1103
c [sweep-7-1] 1543539 steps 42 queries 349.17 avg class size
c [sweep-7-1] 1281 decisions 41 SAT calls 29.59 avg env size
c [sweep-7-1] 1981 variables remain 61% (1241 retained 39%)
c [sweep-7-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7] removed 0 vars in TOTAL (1 rounds, 41 queries)
c [sort-queue-12] sorted 3222 enqueued variables after 114122 conflicts
c [score-dist-12] active 0 (0%), one 3222 (100%), zero 0 (0%)
c [score-dist-12] max exp 1, different 1 (50%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 0 variables 0.0% (3222 remain 2%)
c [simplification-12] removed 161 irredundant clauses 0.1% (294406 remain 22%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 50000
c [simplification-12] new conflict interval 100000
c [simplification-12] penalized conflict interval 100000 = 1 * 100000
c [simplification-12] hard conflict limit 264122 (soft 214122 + delta 50000)
c [simplification-12] new conflict limit 214122 (hard 264122)
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 -   99.2    3222   290244    161430   36906   2489  4010    8    95   60   8%    869   16    9    7  128%
c -  106.1    3222   286819    209484   44869   2612  4125    7   106   61   6%    949   10    6    7   89%
c 
c [simplification-13] limit 214122 conflicts (hard 264122) hit after 222315 conflicts
c [quatres-9] found 3921 quaternary clauses 1% in total
c [quatres-9-1] added 3 double-self-subsuming ternary resolvents
c [quatres-9-2] added 86 single-self-subsuming ternary resolvents
c [quatres-9-2] added 31 quaternary resolvents
c [ternres-9] limit 17391931 with penalty 0 = 0 + 0
c [ternres-9] all 3222 free variables schedulable
c [ternres-9] 539 ternary resolvents (41 bin, 498 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-36] removed 14 variables
c [treelook-4] limit 434798 penalty 2 = 2 + 0 boost 1
c [treelook-4] scheduled 1254 literals 20%
c [treelook-4] scheduling used 434844 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 434798 penalty 2 = 2 + 0 boost 1
c [treelook-4] used 471740 steps
c [treelook-4] 1248 literals remain 19%
c [treelook-4] 342 variables remain to probed next time 11%
c [treelook-4] removed 0 variables, found 109 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 142 transitive binary clauses
c [sort-queue-13] sorted 3208 enqueued variables after 222315 conflicts
c [score-dist-13] active 0 (0%), one 3208 (100%), zero 0 (0%)
c [score-dist-13] max exp 1, different 1 (50%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 14 variables 0.4% (3208 remain 2%)
c [simplification-13] removed 3 irredundant clauses 0.0% (286110 remain 22%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 100000
c [simplification-13] new conflict interval 200000
c [simplification-13] penalized conflict interval 200000 = 1 * 200000
c [simplification-13] hard conflict limit 522315 (soft 422315 + delta 100000)
c [simplification-13] new conflict limit 422315 (hard 522315)
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  112.0    3207   284704    245080   71085   3185  4200    7    88   64   8%    981   -5    5    7   68%
c -  114.3    3207   283748    260102   52416   3236  4244    7    73   62  10%  -1657  -21    9    7  130%
c -  121.3    3207   281503    310958   62321   3427  4388    7   105   46   7%   -210   13    8    7  109%
c -  128.3    3207   279291    362323   71130   3617  4534    6   100   63   6%    460    7    6    7   91%
c -  134.4    3207   277200    410312   78724   3758  4694    7    74   47   9%    753  -22    7    7  101%
c 
c [simplification-14] limit 422315 conflicts (hard 522315) hit after 422316 conflicts
c [quatres-10] found 4753 quaternary clauses 1% in total
c [quatres-10-2] added 206 single-self-subsuming ternary resolvents
c [quatres-10-2] added 66 quaternary resolvents
c [ternres-10] limit 28898291 with penalty 0 = 0 + 0
c [ternres-10] all 3207 free variables schedulable
c [ternres-10] 507 ternary resolvents (49 bin, 458 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-38] removed 78 variables
c [basicprobe-4] limit 144491459 penalty 0 = 0 + 0
c [basicprobe-4-0] 694 sched 22%, 2 failed, 0 lifted, 627 hbrs
c [decomp-39] removed 2 variables
c [basicprobe-4-1] 655 sched 21%, 1 failed, 0 lifted, 40 hbrs
c [decomp-40] removed 1 variables
c [basicprobe-4-2] 654 sched 21%, 0 failed, 0 lifted, 21 hbrs
c [basicprobe-4-3] 655 sched 21%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-4] 655 sched 21%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-5] 655 sched 21%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-6] 655 sched 21%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-6] fully completed probing
c [basicprobe-4-6] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-4-6] removed 3 variables, found 691 hbrs
c [bate-2] eliminated 19 asymmetric tautologies during probing
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 197 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 180614323 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 351 clauses out of 164045 (0%) of length 9
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 351 large clauses in 180614575 steps
c [cce-4-1] allowing another 90307287 steps for small clauses
c [cce-4-1] scheduling 6761 clauses = 3777 binary + 2984 ternary
c [cce-4-1] tried to eliminate 6761 small clauses 100%
c [cce-4-1] eliminated 196 binary clauses 5%
c [cce-4-1] eliminated 375 ternary clauses 13%
c [cce-4-1] eliminated 571 small clauses 8%
c [cce-4-1] eliminated 571 small clauses in 174190317 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 922 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 3212037 steps for small clauses
c [cce-4-2] scheduling 6190 clauses = 3581 binary + 2609 ternary
c [cce-4-2] tried to eliminate 285 small clauses 5%
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 922 covered clauses in TOTAL during 2 rounds
c [cce-4] 922 < 1/100 * 276788 = 2767 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 3127 variables 100%
c [elim-11] limit of 288982918 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 462 not tried 15% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 130 = 4% variables out of 3127 scheduled
c [sort-queue-14] sorted 2997 enqueued variables after 422316 conflicts
c [score-dist-14] active 0 (0%), one 2997 (100%), zero 0 (0%)
c [score-dist-14] max exp 1, different 1 (50%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 210 variables 6.5% (2997 remain 2%)
c [simplification-14] removed 1209 irredundant clauses 0.4% (275644 remain 21%)
c [simplification-14] maximum reduction of 7% = max (7%, 0%)
c [simplification-14] large reduction 7% >= 5% limit
c [simplification-14] next conflict interval 4223 = min (422316/100, 200000)
c [simplification-14] penalized conflict interval 4223 = 1 * 4223
c [simplification-14] hard conflict limit 436539 (soft 426539 + delta 10000)
c [simplification-14] new conflict limit 426539 (hard 436539)
c 
c [simplification-15] limit 426539 conflicts (hard 436539) hit after 426539 conflicts
c [quatres-11] found 4474 quaternary clauses 1% in total
c [quatres-11-1] removed 5 duplicate quaternary clauses
c [quatres-11-1] added 3 double-self-subsuming ternary resolvents
c [quatres-11-2] added 42 single-self-subsuming ternary resolvents
c [quatres-11-2] added 15 quaternary resolvents
c [ternres-11] limit 29162121 with penalty 0 = 0 + 0
c [ternres-11] all 2997 free variables schedulable
c [ternres-11] 325 ternary resolvents (39 bin, 286 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 911316 penalty 4 = 4 + 0
c [card-5] found 43 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 911316 for elimination
c [card-5] 43 out of 43 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-7] limit 1458106 penalty 2 = 2 + 0
c [gauss-7] extracted 4884 xors of average arity 3.4
c [gauss-7] connected 16484 occurrences of 1377 variables (average 12.0)
c [gauss-7] limit 1458106 penalty 2 = 2 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-45] removed 2 variables
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 159 transitive binary clauses
c [block-8] 110 variables 4% will be scheduled this time
c [block-8] scheduled 110 variables 4%
c [block-8] limit of 72905303 steps penalty 2 = 2 + 0
c [block-8] incomplete 56 not tried 2%
c [block-8] transition to [ all 0 rem 1 ] state
c [block-8] eliminated 0 blocked clauses
c [elim-12] 410 variables 14% will be scheduled this time
c [elim-12] scheduled 410 variables 14%
c [elim-12] limit of 583242430 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 165 not tried 6% in round 1
c [elim-12] transition to [ all 0 rem 1 ] state
c [elim-12] eliminated 0 = 0% variables out of 410 scheduled
c [bca-5] limit of 10000000 steps and 527404 added (scaled 2)
c [bca-5] 837 out of 5992 literals actually usable 14%
c [bca-5] added 0 blocked clauses in 84099 steps
c [sweep-8] limit 2187159 penalty 2 = 2 + 0
c [sweep-8-1] 843 pos 44.9% + 1035 neg 55.1% = 1878 sched 62.7% ret 1117
c [sweep-8-1] 2191546 steps 63 queries 258.29 avg class size
c [sweep-8-1] 2334 decisions 63 SAT calls 54.21 avg env size
c [sweep-8-1] 1594 variables remain 53% (1401 retained 47%)
c [sweep-8-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-8] removed 0 vars in TOTAL (1 rounds, 62 queries)
c [sort-queue-15] sorted 2995 enqueued variables after 426539 conflicts
c [score-dist-15] active 0 (0%), one 2995 (100%), zero 0 (0%)
c [score-dist-15] max exp 1, different 1 (50%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 2 variables 0.1% (2995 remain 2%)
c [simplification-15] removed 12229 irredundant clauses 4.4% (263248 remain 20%)
c [simplification-15] maximum reduction of 4% = max (0%, 4%)
c [simplification-15] geometric conflict interval increment 40000 = 200000 / 5
c [simplification-15] new conflict interval 240000
c [simplification-15] penalized conflict interval 240000 = 1 * 240000
c [simplification-15] hard conflict limit 786539 (soft 666539 + delta 120000)
c [simplification-15] new conflict limit 666539 (hard 786539)
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  160.2    2994   261967    463808  108544   4032  4979    7    62   50  11%    904  -34    4    7   59%
c -  161.2    2994   261706    469998   81288   4057  5000    7    56   62  12%  -2236  -38    5    7   74%
c i  161.6    2993   261579    473065   83555   4104  5021    7    72   66   9%  -2094  -20    7    7  101%
c i  161.7    2992   261574    473324   83673   4124  5027    7    72   48   9%  -2114  -20    6    7   88%
c i  163.0    2991   261297    483844   91976   4171  5066    7    83   64   9%  -1750  -13    7    7   95%
c i  163.3    2990   261247    486090   93606   4183  5075    7    75   64  10%  -1799  -21    8    7  109%
c i  165.2    2989   260795    498243  102614   4233  5117    7    67   66  10%  -1366  -26    8    7  114%
c -  168.2    2989   260172    524009   90433   4321  5182    7    95   47   7%   -719   -3    7    7   98%
c i  169.2    2988   259973    531014   95958   4344  5203    7   125   67   6%   -543   25    8    7  108%
c i  170.6    2987   259524    545129  107531   4415  5238    7   129   66   5%   -659   20    7    7   99%
c i  171.4    2986   259281    550530  111676   4454  5255    7   101   51   7%   -731   -9    6    7   91%
c -  174.7    2986   258425    575369   97968   4532  5316    8   108   64   7%   -237   -0    9    7  124%
c -  183.1    2986   256877    629649  105872   4794  5506    7   101   65   7%    473    3    6    7   91%
c i  185.1    2985   256548    644354  117010   4856  5544    7   122   52   6%    584   24    7    7  104%
c i  188.7    2984   255938    668652  134850   4982  5645    6    38   54  16%   -308  -58    4    7   60%
c i  191.8    2977   255442    687897  149061   5080  5713    7   127   73   5%   -256   36    5    7   72%
c -  192.2    2971   255369    690703  116641   5095  5725    7   123   67   6%   -476   31    6    7   93%
c 
c [simplification-16] limit 666539 conflicts (hard 786539) hit after 729754 conflicts
c [quatres-12] found 6238 quaternary clauses 2% in total
c [quatres-12-1] added 3 double-self-subsuming ternary resolvents
c [quatres-12-2] added 351 single-self-subsuming ternary resolvents
c [quatres-12-2] added 70 quaternary resolvents
c [ternres-12] limit 48009552 with penalty 0 = 0 + 0
c [ternres-12] all 2971 free variables schedulable
c [ternres-12] 468 ternary resolvents (53 bin, 415 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-47] removed 210 variables
c [simpleprobe-5] 1539 schedulable variables 55%
c [simpleprobe-5] limit 96019105 penalty 1 = 1 + 0
c [simpleprobe-5] 1136 variables remain 41% (1649 retained 59%)
c [simpleprobe-5] removed 0 variables, found 458 hbrs, 0 units
c [unhide-10] limit 1200238 with penalty 3 = 3 + 0
c [unhide-10-10] 0 units, 0 failed, 3948 tauts, 0 hbrs, 11268 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 207 transitive binary clauses
c [sort-queue-16] sorted 2785 enqueued variables after 729754 conflicts
c [score-dist-16] active 0 (0%), one 2785 (100%), zero 0 (0%)
c [score-dist-16] max exp 1, different 1 (50%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 186 variables 6.3% (2785 remain 2%)
c [simplification-16] removed 2360 irredundant clauses 0.9% (252170 remain 19%)
c [simplification-16] maximum reduction of 6% = max (6%, 1%)
c [simplification-16] large reduction 6% >= 5% limit
c [simplification-16] next conflict interval 7297 = min (729754/100, 240000)
c [simplification-16] penalized conflict interval 7297 = 1 * 7297
c [simplification-16] hard conflict limit 747051 (soft 737051 + delta 10000)
c [simplification-16] new conflict limit 737051 (hard 747051)
c 
c [simplification-17] limit 737051 conflicts (hard 747051) hit after 738503 conflicts
c [quatres-13] found 4975 quaternary clauses 2% in total
c [quatres-13-1] removed 12 duplicate quaternary clauses
c [quatres-13-1] added 4 double-self-subsuming ternary resolvents
c [quatres-13-2] added 101 single-self-subsuming ternary resolvents
c [quatres-13-2] added 125 quaternary resolvents
c [ternres-13] limit 48631864 with penalty 0 = 0 + 0
c [ternres-13] all 2785 free variables schedulable
c [ternres-13] 299 ternary resolvents (47 bin, 252 trn)
c [ternres-13] fully completed ternary resolution
c [gauss-8] limit 4863186 penalty 1 = 1 + 0
c [gauss-8] extracted 5383 xors of average arity 3.3
c [gauss-8] connected 17928 occurrences of 1334 variables (average 13.4)
c [gauss-8] limit 4863186 penalty 1 = 1 + 0
c [gauss-8] fully completed
c [decomp-49] removed 13 variables
c [gauss-8] exported 0 unary, 2 binary and 2 ternary equations
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 117 transitive binary clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 2772 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 114 variables 4% in round 1 in 4250389339 steps
c [elim-13-1] backward subsumption/strengthening limit 4250389300
c [elim-13-1-1] backward checking 1094 touched variables 39%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 2 and strengthened 2 clauses in 5393809 steps
c [elim-13-1] rescheduled 12 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 1372281 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 115 = 4% variables out of 2772 scheduled
c [sort-queue-17] sorted 2657 enqueued variables after 738503 conflicts
c [score-dist-17] active 0 (0%), one 2657 (100%), zero 0 (0%)
c [score-dist-17] max exp 1, different 1 (50%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 128 variables 4.6% (2657 remain 2%)
c [simplification-17] removed 72544 irredundant clauses 28.8% (179339 remain 13%)
c [simplification-17] maximum reduction of 29% = max (5%, 29%)
c [simplification-17] large reduction 29% >= 5% limit
c [simplification-17] next conflict interval 7385 = min (738503/100, 240000)
c [simplification-17] penalized conflict interval 7385 = 1 * 7385
c [simplification-17] hard conflict limit 755888 (soft 745888 + delta 10000)
c [simplification-17] new conflict limit 745888 (hard 755888)
c 
c [simplification-18] limit 745888 conflicts (hard 755888) hit after 745889 conflicts
c [quatres-14] found 4680 quaternary clauses 2% in total
c [quatres-14-1] removed 9 duplicate quaternary clauses
c [quatres-14-1] added 2 double-self-subsuming ternary resolvents
c [quatres-14-2] added 31 single-self-subsuming ternary resolvents
c [quatres-14-2] added 25 quaternary resolvents
c [ternres-14] limit 49048658 with penalty 0 = 0 + 0
c [ternres-14] all 2657 free variables schedulable
c [ternres-14] 124 ternary resolvents (26 bin, 98 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-9] limit 9809731 penalty 0 = 0 + 0
c [gauss-9] extracted 4454 xors of average arity 3.4
c [gauss-9] connected 15038 occurrences of 1180 variables (average 12.7)
c [gauss-9] limit 9809731 penalty 0 = 0 + 0
c [gauss-9] fully completed
c [gauss-9] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-51] removed 6 variables
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 90 transitive binary clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 2651 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14] incomplete 143 not tried 5% in round 1
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 33 = 1% variables out of 2651 scheduled
c [sort-queue-18] sorted 2618 enqueued variables after 745889 conflicts
c [score-dist-18] active 0 (0%), one 2618 (100%), zero 0 (0%)
c [score-dist-18] max exp 1, different 1 (50%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 39 variables 1.5% (2618 remain 2%)
c [simplification-18] removed 1182 irredundant clauses 0.7% (178157 remain 13%)
c [simplification-18] maximum reduction of 1% = max (1%, 1%)
c [simplification-18] geometric conflict interval increment 120000 = 240000 / 2
c [simplification-18] new conflict interval 360000
c [simplification-18] penalized conflict interval 360000 = 1 * 360000
c [simplification-18] hard conflict limit 1285889 (soft 1105889 + delta 180000)
c [simplification-18] new conflict limit 1105889 (hard 1285889)
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 -  259.9    2618   178157    759806  106515   3827  4624    8   151   54   5%    495   51    8    7  116%
c i  260.3    2617   178157    763762  109441   3854  4652    6   107   44   6%    526    6    4    7   63%
c i  265.1    2610   178155    802774  138738   4048  4766    6    33   61  18%     85  -65    4    7   63%
c -  267.9    2604   178155    824722  119428   4144  4829    7   129   56   5%    -91   24    7    7  107%
c i  269.1    2603   178155    835044  126909   4181  4866    7   117   59   6%     72   10    8    7  118%
c i  269.4    2596   178155    837561  128351   4212  4881    6    74   59   8%   -341  -33    5    7   71%
c i  270.9    2589   178155    849142  137233   4271  4921    7    74   47  10%   -190  -29    7    7  104%
c -  275.2    2583   178155    882381  127787   4398  5011    8    74   56  10%    182  -17    8    7  117%
c i  280.8    2582   178155    925356  161506   4609  5159    7    67   64  11%    587  -11    5    7   64%
c -  283.3    2576   178155    941999  137171   4687  5209    7    39   43  18%   -253  -33    7    7   96%
c i  283.9    2575   178155    947933  141612   4728  5225    6    53   49  12%   -143  -18    4    7   59%
c i  284.2    2568   178155    952556  145166   4752  5231    6    73   49   9%   -393    3    5    7   67%
c i  285.3    2561   178155    961566  151133   4809  5259    6    64   49   9%   -279   -6    4    7   59%
c i  288.7    2554   178155    987485  171366   4915  5310    7    25   66  28%     51  -36    7    7   95%
c i  289.2    2547   178155    991528  174020   4928  5317    6    16   66  41%   -270  -43    5    7   67%
c i  289.4    2533   178155    992781  174801   4953  5323    6    14   66  42%   -295  -44    4    7   63%
c i  289.5    2529   178147    992857  174808   4963  5325    6    14   66  42%   -297  -44    4    7   61%
c i  289.5    2528   178143    992901  174813   4974  5328    6    14   66  43%   -297  -44    4    7   58%
c i  289.5    2527   178142    992924  174812   4979  5331    6    14   66  43%   -298  -44    4    7   56%
c i  289.5    2526   178142    992934  174812   4982  5334    6    14   66  43%   -298  -44    4    7   55%
c i  289.5    2525   178141    992938  174812   4982  5335    6    14   66  43%   -298  -44    4    7   55%
c i  289.5    2524   178141    992941  174811   4984  5336    6    14   66  43%   -298  -44    4    7   55%
c i  289.5    2523   178141    992943  174811   4984  5336    6    14   66  43%   -298  -44    4    7   54%
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  289.5    2469   178141    992943  174811   4984  5336    6    14   66  43%   -298  -44    4    7   54%
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: 75 basic ate = 58 trn 77% + 17 lrg 23% in 2 updates
c bcas: 5 count, 248 added (1 skipped), 230839 steps
c bkwd: tried 30517 clauses, 60978 lits, 2.00 lits/clause
c bkwd: checked 31612285 occs, 1035.89 occs/clause, 518.42 occs/lit
c bkwd: subsumed 0 binary, 6 ternary, 10 large
c bkwd: strengthened 0 binary, 5 ternary (100% self), 64 large (0% self)
c blkd: 8 bces, 31225 removed, 801007931 resolutions, 838877776 steps
c blkd: 8110 blocking literals 2%, 4238 pure
c bump: 918417 bumped seen, 22060733 lits 24.0 on average
c card: 5 count, 5 units, 0 am1, 7658775 steps
c card: 1 rescheduled, 3 eliminated, 355 resolved, 151 subsumed
c card: 120 at-most-one constraints found, average size 4.12
c card: 120 at-most-one constraints used 100%, average size 4.12
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, 1340 eliminated, 1339 ate 100%, 1 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: 5816471 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 94 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 51 decompositions, 36480 equivalent 14%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 4220444 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 14 elims, 100349 eliminated 38%, 10 pure 0%
c elms: 18 rounds, 1.3 rounds/bve
c elms: 61173 small 61%, 34928 large 35%
c elms: 66842 tried small, 61173 succeeded 92%, 5669 failed 8%
c elms: 31108 subsumed, 244979 strengthened, 203 blocked
c elms: 7095666 copies, 95994372 resolutions, 1037455 ipos
c elms: 6589002 subchks, 5138861 strchks
c gaus: 9 extractions, 98209 extracted, 3.1 size, 4 max
c gaus: exported 0 units, 9 binary and 4 ternary equations
c gaus: 5 gc, 52272474 steps, 26136237 extr 50%, 6359682 elim 12%
c glue: 7.2 orig avg, 7.2 real avg, 1.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 23193 = 15665 simple 68% + 7423 trn 32% + 105 lrg 0%, 421 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 918417 clauses, 13.3 length
c lrnd: 12180412 lits = 13249023 orig - 1068611 removed 8%
c lrnd: 41954 uips 5%, 848837 flips 92%
c mins: 876045 mins 95%, 1823 bin 0%, 40549 size 4%
c mins: 8170057 poisoned searches, 825328 hits, 10% hit rate
c mins: 19330534 used twice searches, 3746827 hits, 19% hit rate
c move: moved 22404, 650 bin 3%, 21754 trn 97%
c otfs: 85911 driving 40%, 130273 restarting 60%
c otfs: str 216184, 165699 red 77%, 50485 irr 23%
c otfs: str 216184, 0 bin 0%, 1071 trn 0%, 215113 lrg 100%
c otfs: sub 50693, 7374 red 15%, 43319 irr 85%
c otfs: sub 50693, 0 bin 0%, 470 trn 1%, 50223 lrg 99%
c phas: 2 computed, 89792 set, 0 pos (0%), 89792 neg (100%)
c prbs: 4 basic, 20415 probed, 12 failed, 0 lifted
c prbs: 5 simple, 191078 probed, 77 failed, 1171 eqs
c prbs: 4 treelook, 63 probed, 0 failed, 0 lifted
c prom: 165598 locked 29% out of 571816 tried
c prps: 61369713 props, 14 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 14 count, 863 quat, 1711 self1, 22 self2, 68 dup
c queu: 18 sorted, 4220444 next (115 steps 0.00)
c queu: 22525975 enq (0 steps 0.00), 22060733 deq 98%
c redc: 9603 clauses 2%, 470418 tried 47%, 9 sat 0%
c redc: 11167 lits 0%, 4544355 tried 34%, 9 sat 0%
c redc: 424 times jump level reduced, 4.4 levels on average
c reds: 17 count, 58408.4 conflicts per reduce
c reds: 0 memlim 0%, 17 arith 100%
c reds: 493046 collected 89%, 63342 retired 11%
c rmbd: 1946 removed, 642 red 33%
c rsts: 29609 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 18 count, 16 confs 89%, 0 vars 0%
c simp: 1 its 6%, 1 bin 6%, 0 trns 0%
c subl: 918417 count (273827 tried 0.3), 127166 sub out of 912077 (13.9%)
c swps: 8 count, 9 rounds, 915 queries (101.7/round)
c swps: 876 sat calls, 7 unsat (13.0% success rate)
c swps: 30494 decisions 34.8, 11385 conflicts 13.0
c swps; 222.8 avg class size, 44.3 avg environment size
c swps: 0 failed, 48 impls, 46 equivs
c swp0: 301 type 0 queries, 56 unsat (18.6%), 280 sat (93.0%)
c swp1: 614 type 1 queries, 88 unsat (14.3%), 589 sat (95.9%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 10278129 calls to obtain time
c tops: 126901 fixed 48%, 80 its, 12411.79 confs/it
c trds: 14 transitive reductions, 1690 removed, 0 failed
c trds: 94558 nodes, 92961 edges, 3501344 steps
c trim: 714269 words, 2.7 MB
c trnr: 14 count, 5536 bin, 47084 trn, 58026248 steps
c unhd: 10 count, 10 rounds, 24011536 steps
c unhd: 1353 non-trivial sccs of average size 2.0
c unhd: 102 units, 70 bin, 32 trn, 0 lrg
c unhd: 829 failed, 815 stamp, 0 lits, 1 bin, 12 trn, 0 lrg
c unhd: 9492 tauts, 39 bin 0%, 4206 trn 44%, 3518 lrg 37%
c unhd: 9492 tauts, 1729 stamp 18%, 6574 red 69%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 19886 str, 70 bin 0%, 3180 trn 16%, 16636 lrg 84%, 12866 red 65%
c vars: 2469 remaining 1% and 263730 removed 99% out of 266199
c vars: 126901 fixed 48%, 100349 eliminated 38%, 36480 equivalent 14%
c vsts: 6237976733 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 102.4 search visits per propagation, 6222.6 per conflict
c wchs: 3548243203 pushed, 10672377 enlarged, 224 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         912940        493046         63342       5401160       2738250        372153
c 
c  0 0        188654  21      7515   2         0   0   2570070  48    985329  36    111237  30     4.7
c  1 5        137943  15     82169  17     11060  17    837854  16<   453164  17<    56441  15<    0.8
c  2 6        361862  40<   251575  51<    28347  45<  1630466  30    931429  34    134863  36     1.8
c  3 9        161254  18    109525  22     14618  23    268434   5    276361  10     50695  14     1.0
c  4 14        50828   6     34608   7      6964  11     75230   1     76058   3     15692   4     0.4
c  5 21        10187   1      6350   1      1840   3     15524   0     13285   0      2702   1     0.1
c  6 30         1851   0      1119   0       406   1      3006   0      2233   0       439   0     0.0
c  7 41          319   0       169   0        90   0       512   0       354   0        77   0     0.0
c  8 54           27   0         9   0        11   0        46   0        27   0         6   0     0.0
c  9 69           15   0         7   0         6   0        18   0        10   0         1   0     0.0
c 
c avg                  1.8           2.2           2.4           1.0           1.3           1.5
c std                  1.2           0.9           1.0           1.1           1.2           1.2
c 
c   89.039  31% elim
c   35.414  12% block
c    7.047   2% probe
c    3.336   1% cce
c    2.780   1% gauss
c    2.585   1% decide
c    2.162   1% sweep
c    1.997   1% unhide
c 
c    3.735 < 1% rest (below)
c 
c    1.249   0% bump
c    0.817   0% bca
c    0.625   0% transred
c    0.516   0% quatres
c    0.443   0% ternres
c    0.083   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    4.480   2% preprocessing     3%
c  146.002  50% inprocessing     97%
c ==================================
c  150.482  52% simplifying
c  138.983  48% search
c ==================================
c  289.469 100% all
c 
c        992943 conflicts,        3430.2 confs/sec
c          3840 ternaries,         258.6 confs/ternary
c          2335 binaries,          425.2 confs/binary
c            80 iterations,      12411.8 confs/iteration
c 
c            17 reductions,          0.1 redus/sec,  58408.4 confs/reduction
c         29609 restarts,          102.3 rests/sec,     33.5 confs/restart
c       4220444 decisions,       14579.9 decis/sec,      4.3 decis/conflict
c      61369713 propagations,   212007.6 props/sec,     14.5 props/decision
c 
c 289.5 seconds, 147.2 MB
c launch: done
