Details of instance load_full_2_comp1_UNREAL.aag

Name: load_full_2_comp1_UNREAL.aag
md5: b379aa18e364e811a925ecf31d53dc69
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 (25.7 kB)
aag 1804 5 183 1 1616
2
4
6
8
10
12 0
14 1785
16 1789
18 1679
20 1683
22 1687
24 1647
26 1651
28 1655
30 0
32 1797
34 1801
36 526
38 0
40 0
42 0
44 1791
46 1795
48 0
50 1775
52 1783
54 1561
56 1565
58 1569
60 1553
62 1555
64 1557
66 1679
68 1683
70 1687
72 1421
74 1423
76 1425
78 1631
80 1633
82 1635
84 1381
86 1385
88 1389
90 1277
92 1279
94 1281
96 1403
98 1405
100 1407
102 1249
104 1253
106 1257
108 1609
110 1613
112 1617
114 1393
116 1397
118 1401
120 1504
122 1508
124 1512
126 1679
128 1683
130 1687
13

... [truncated 24.7 kB]

56 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
l172 latch172
l173 latch173
l174 latch174
l175 latch175
l176 latch176
l177 latch177
l178 latch178
l179 latch179
l180 latch180
l181 latch181
l182 latch182
o0 error
c
#!SYNTCOMP
STATUS : unrealizable
SOLVED_BY : 3/3 [2015-pre-classification]
SOLVED_IN : 0.472782 [2015-pre-classification]
#.