Details of instance demo-v25_5_UNREAL.aag

Name: demo-v25_5_UNREAL.aag
md5: a905caca24dd7a4c34e7982675319845
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 (20.0 kB)
aag 1340 4 280 1 1056
2
4
6
8
10 0
12 2155
14 2159
16 2163
18 2167
20 2171
22 2179
24 0
26 1955
28 1959
30 1963
32 1967
34 1971
36 1979
38 1857
40 1859
42 1861
44 1863
46 1865
48 1867
50 1869
52 1857
54 1859
56 1861
58 1863
60 1865
62 1867
64 1869
66 1857
68 1859
70 1861
72 1863
74 1865
76 1867
78 1869
80 0
82 1905
84 1909
86 1913
88 1917
90 1921
92 1947
94 0
96 2135
98 2137
100 2139
102 2141
104 2143
106 2151
108 0
110 1905
112 1909
114 1913
116 1917
118 1921
120 1947
122 0
124 1857
126 1859
128 1861
130 1

... [truncated 19.0 kB]

h252
l253 latch253
l254 latch254
l255 latch255
l256 latch256
l257 latch257
l258 latch258
l259 latch259
l260 latch260
l261 latch261
l262 latch262
l263 latch263
l264 latch264
l265 latch265
l266 latch266
l267 latch267
l268 latch268
l269 latch269
l270 latch270
l271 latch271
l272 latch272
l273 latch273
l274 latch274
l275 latch275
l276 latch276
l277 latch277
l278 latch278
l279 latch279
o0 error
c
#!SYNTCOMP
STATUS : unrealizable
SOLVED_BY : 7/8 [SYNTCOMP2014-RealSeq]
SOLVED_IN : 4.32827 [SYNTCOMP2014-RealSeq]
#.