Details of instance ltl2dba_02_1_REAL.aag

Name: ltl2dba_02_1_REAL.aag
md5: ef2e2c400bda55d23945ddd93b3bda4c
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 (65.1 kB)
aag 4521 4 363 1 4154
2
4
6
8
10 8105
12 8109
14 8113
16 4179
18 4183
20 4187
22 7949
24 7953
26 7957
28 6821
30 6825
32 6829
34 8511
36 8513
38 8515
40 8403
42 8405
44 8407
46 1651
48 1655
50 1659
52 1743
54 1747
56 1751
58 5441
60 5445
62 5449
64 5429
66 5433
68 5437
70 7985
72 7989
74 7993
76 8489
78 8493
80 8497
82 8603
84 8607
86 8611
88 8615
90 8619
92 8623
94 8363
96 8367
98 8371
100 8315
102 8319
104 8323
106 4705
108 4709
110 4713
112 6989
114 6993
116 6997
118 2229
120 2233
122 2237
124 3365
126 3

... [truncated 64.1 kB]

tch335
l336 latch336
l337 latch337
l338 latch338
l339 latch339
l340 latch340
l341 latch341
l342 latch342
l343 latch343
l344 latch344
l345 latch345
l346 latch346
l347 latch347
l348 latch348
l349 latch349
l350 latch350
l351 latch351
l352 latch352
l353 latch353
l354 latch354
l355 latch355
l356 latch356
l357 latch357
l358 latch358
l359 latch359
l360 latch360
l361 latch361
l362 latch362
o0 error
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 6/8 [SYNTCOMP2014-RealSeq]
SOLVED_IN : 19.5492 [SYNTCOMP2014-RealSeq]
#.