| Name: |
amba2match3.aag |
| md5: |
c7a2abb5ef2b53df1bef1aa7e1df24c3 |
| 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 |
aag 4132 15 51 1 4066
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32 1
34 4
36 733
38 12
40 1114
42 1538
44 14
46 1742
48 2990
50 3058
52 3062
54 3071
56 10
58 2
60 6
62 3212
64 3310
66 3677
68 3707
70 3851
72 3892
74 3979
76 8
78 4108
80 3893
82 18
84 4709
86 26
88 5090
90 5514
92 28
94 5718
96 6966
98 7034
100 7038
102 7047
104 24
106 16
108 20
110 7188
112 7286
114 7653
116 7683
118 7827
120 7868
122 7955
124 22
126 8084
128 8248
130 1
132 30
8264
134 72 32
136 42 32
138 54 32
140 58 32
142 70 32
144 34 32
... [truncated 57.2 kB]
eq_p_out_1
l43 hgrant1_p_out_1
l44 jx1_p_out_1
l45 hmastlock_p_out_1
l46 hlock0_p_out_1
l47 stateG3_1_p_out_1
l48 sink
l49 init
l50 L: F 7364
o0 AIGER_OR
c
aigor
disjunction of 1 original outputs
#!SYNTCOMP
SOLVED_BY : 2/3 [2015-pre-classification], 4/4 [SYNTCOMP2015-SyntSeq], 3/3 [SYNTCOMP2015-SyntPar], 7/7 [SYNTCOMP2015-RealSeq], 4/4 [SYNTCOMP2015-RealPar]
SOLVED_IN : 0.280648 [2015-pre-classification], 0.220403 [SYNTCOMP2015-RealSeq], 0.045523 [SYNTCOMP2015-RealPar]
REF_SIZE : 0
STATUS : unrealizable
#.