Details of instance amba7match5.aag

Name: amba7match5.aag
md5: 0d09447de8fa958f4c1a53bdef3561a4
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 (1.1 MB)
aag 67520 40 207 1 67273
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 1
84 30
86 9035
88 9098
90 4
92 20
94 9120
96 26
98 9124
100 14558
102 22
104 17733
106 21430
108 6
110 10
112 21897
114 38140
116 38159
118 40048
120 42678
122 14
124 42717
126 42750
128 43502
130 2
132 18
134 43524
136 32
138 45641
140 45668
142 46380
144 28
146 24
148 49301
150 49496
152 56678
154 58430
156 8
158 12
160 60285
162 61616
164 61634
166 64310
168 650

... [truncated 1.1 MB]


l187 l83_copy
l188 l84_copy
l189 l85_copy
l190 l86_copy
l191 l87_copy
l192 l88_copy
l193 l89_copy
l194 l90_copy
l195 l91_copy
l196 l92_copy
l197 l93_copy
l198 l94_copy
l199 l95_copy
l200 l96_copy
l201 l97_copy
l202 l98_copy
l203 l99_copy
l204 l100_copy
l205 l101_copy
l206 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]
#.