Details of instance amba9match5.aag

Name: amba9match5.aag
md5: 17035bbf0467ede017613e14f7ee8ba8
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 (2.8 MB) 
aag 158542 48 243 1 158251
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42
44
46
48
50
52
54
56
58
60
62
64
66
68
70
72
74
76
78
80
82
84
86
88
90
92
94
96
98 1
100 690
102 5552
104 40
106 10030
108 10034
110 10
112 14923
114 17380
116 17418
118 32
120 18
122 21799
124 21832
126 25644
128 30264
130 62992
132 42
134 8
136 86447
138 90553
140 34
142 90586
144 90614
146 92197
148 16
150 95262
152 96073
154 26
156 6
158 96216
160 20
162 36
164 102910
166 102925
168 102964
170 14
172 105604
174 105837

... [truncated 2.8 MB]

224 l102_copy
l225 l103_copy
l226 l104_copy
l227 l105_copy
l228 l106_copy
l229 l107_copy
l230 l108_copy
l231 l109_copy
l232 l110_copy
l233 l111_copy
l234 l112_copy
l235 l113_copy
l236 l114_copy
l237 l115_copy
l238 l116_copy
l239 l117_copy
l240 l118_copy
l241 l119_copy
l242 L_MH:F(And(And(Neg(hbusreq00))(And(Neg(hburst00))(Neg(hburst10...401
o0 AIGER_OR
c
aigor
disjunction of 2 original outputs
#!SYNTCOMP
STATUS : unknown
SOLVED_BY : 0/3 [2015-pre-classification]
SOLVED_IN : 0.0 [2015-pre-classification]
#.