Details of instance ltl2dba_15_2_UNREAL.aag

Name: ltl2dba_15_2_UNREAL.aag
md5: 869fedd7537e66acb6237f8251d21be3
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 (12.8 kB)
aag 913 3 172 1 738
2
4
6
8 1296
10 1298
12 1300
14 1302
16 1483
18 1487
20 1491
22 1495
24 1283
26 1287
28 1291
30 1295
32 0
34 1611
36 1615
38 1623
40 1611
42 1615
44 1625
46 1627
48 1539
50 1543
52 1553
54 1555
56 0
58 1395
60 1399
62 1407
64 1343
66 1347
68 1351
70 1355
72 0
74 1411
76 1415
78 1423
80 0
82 1631
84 1635
86 1663
88 0
90 1647
92 1651
94 1659
96 1559
98 1563
100 1567
102 1571
104 1221
106 1223
108 1225
110 1227
112 1221
114 1223
116 1225
118 1227
120 694
122 0
124 0
126 0
128 1631
130 1635


... [truncated 11.8 kB]

h144
l145 latch145
l146 latch146
l147 latch147
l148 latch148
l149 latch149
l150 latch150
l151 latch151
l152 latch152
l153 latch153
l154 latch154
l155 latch155
l156 latch156
l157 latch157
l158 latch158
l159 latch159
l160 latch160
l161 latch161
l162 latch162
l163 latch163
l164 latch164
l165 latch165
l166 latch166
l167 latch167
l168 latch168
l169 latch169
l170 latch170
l171 latch171
o0 error
c
#!SYNTCOMP
STATUS : unrealizable
SOLVED_BY : 6/8 [SYNTCOMP2014-RealSeq]
SOLVED_IN : 1.10807 [SYNTCOMP2014-RealSeq]
#.