Details of instance ltl2dpa_13_2_REAL.aag

Name: ltl2dpa_13_2_REAL.aag
md5: 9e5106cb3da6aa0138d1b1820e4d887a
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 (42.2 kB)
aag 2851 5 376 1 2470
2
4
6
8
10
12 0
14 3345
16 3349
18 3357
20 3731
22 3733
24 3735
26 3737
28 3811
30 3813
32 3815
34 3817
36 4517
38 4521
40 4525
42 4529
44 5187
46 5191
48 5195
50 5199
52 4501
54 4505
56 4509
58 4513
60 4441
62 4445
64 4449
66 4453
68 3545
70 3549
72 3553
74 3557
76 3583
78 3585
80 3587
82 3589
84 3567
86 3569
88 3571
90 3573
92 3639
94 3641
96 3643
98 3645
100 3505
102 3509
104 3513
106 3517
108 3893
110 3895
112 3897
114 3899
116 0
118 5139
120 5143
122 5151
124 0
126 5171
128 5175
1

... [truncated 41.2 kB]

tch348
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
l363 latch363
l364 latch364
l365 latch365
l366 latch366
l367 latch367
l368 latch368
l369 latch369
l370 latch370
l371 latch371
l372 latch372
l373 latch373
l374 latch374
l375 latch375
o0 error
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 6/8 [SYNTCOMP2014-RealSeq]
SOLVED_IN : 29.4618 [SYNTCOMP2014-RealSeq]
#.