Details of instance ltl2dba_07_2_REAL.aag

Name: ltl2dba_07_2_REAL.aag
md5: acf753c01a0ee96d9dab698a0e727f03
FractionOfBinaryClauses None
FractionOfNegativeLiteralsPerClauseEntropy None
FractionOfNegativeLiteralsPerClauseMax None
FractionOfNegativeLiteralsPerClauseMean None
FractionOfNegativeLiteralsPerClauseMin None
FractionOfNegativeLiteralsPerClauseVariationCoefficient None
FractionOfNegativeVariablesEntropy None
FractionOfNegativeVariablesMax None
FractionOfNegativeVariablesMean None
FractionOfNegativeVariablesMin None
FractionOfNegativeVariablesVariationCoefficient None
FractionOfPositiveLiteralsPerClauseEntropy None
FractionOfPositiveLiteralsPerClauseMax None
FractionOfPositiveLiteralsPerClauseMean None
FractionOfPositiveLiteralsPerClauseMin None
FractionOfPositiveLiteralsPerClauseVariationCoefficient None
FractionOfPositiveVariablesEntropy None
FractionOfPositiveVariablesMax None
FractionOfPositiveVariablesMean None
FractionOfPositiveVariablesMin None
FractionOfPositiveVariablesVariationCoefficient None
FractionOfTernaryClauses None
FractionOfUnaryClauses None
ClausesToVariablesRatio None
ClausesToVariablesRatioCubic None
ClausesToVariablesRatioQuadratic None
LinearizedClausesToVariablesRatio None
LinearizedClausesToVariablesRatioQuadratic None
LinearizedClaustesToVariablesRatioCubic None
NumberOfClauses None
NumberOfVariables None
VariablesToClausesRatio None
VariablesToClausesRatioCubic None
VariablesToClausesRatioQuadratic None
ClauseNodeDegreesEntropy None
ClauseNodeDegreesMax None
ClauseNodeDegreesMean None
ClauseNodeDegreesMin None
ClauseNodeDegreesVariationCoefficient None
VariableNodeDegreesEntropy None
VariableNodeDegreesMax None
VariableNodeDegreesMean None
VariableNodeDegreesMin None
VariableNodeDegreesVariationCoefficient None
DegreeEntropy None
DegreeMax None
DegreeMean None
DegreeMin None
DegreeVariationCoefficient None
Download instance (40.5 kB)
aag 2814 8 304 1 2502
2
4
6
8
10
12
14
16
18 3599
20 3603
22 3607
24 3611
26 3565
28 3569
30 3573
32 3577
34 4619
36 4623
38 4627
40 4631
42 1232
44 0
46 0
48 0
50 4943
52 4947
54 4951
56 4955
58 4685
60 4689
62 4693
64 4697
66 5467
68 5471
70 5475
72 5479
74 2459
76 2463
78 2467
80 2471
82 5297
84 5301
86 5305
88 5309
90 3631
92 3635
94 3639
96 3643
98 0
100 3343
102 3347
104 3355
106 0
108 2477
110 2481
112 2489
114 0
116 4185
118 4189
120 4197
122 4587
124 4591
126 4595
128 4599
130 2645
132 2647
134 264

... [truncated 39.5 kB]

atch276
l277 latch277
l278 latch278
l279 latch279
l280 latch280
l281 latch281
l282 latch282
l283 latch283
l284 latch284
l285 latch285
l286 latch286
l287 latch287
l288 latch288
l289 latch289
l290 latch290
l291 latch291
l292 latch292
l293 latch293
l294 latch294
l295 latch295
l296 latch296
l297 latch297
l298 latch298
l299 latch299
l300 latch300
l301 latch301
l302 latch302
l303 latch303
o0 error
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 6/8 [SYNTCOMP2014-RealSeq]
SOLVED_IN : 16.141 [SYNTCOMP2014-RealSeq]
#.