Name: |
stay20n.aag |
md5: |
e86dc4134611cf47cb7f8512ebd7c34f |
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 2851 41 22 1 2788
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 1
86 303
88 5551
90 5559
92 5567
94 5575
96 5583
98 5591
100 5599
102 5607
104 5615
106 5623
108 5631
110 5639
112 5647
114 5655
116 5663
118 5671
120 5679
122 5687
124 5695
126 5703
292
128 87 84
130 86 84
132 129 84
134 89 84
136 88 84
138 135 84
140 91 84
142 90 84
144 141 84
146 93 84
148 92 84
150 147 84
152 95 84
154 94 84
156 153 84
158 97 84
160 96 84
162 15
... [truncated 41.7 kB]
4:0],15'b000000000000000} : 0;
assign s16 = b[16] ? {a[3:0],16'b0000000000000000} : 0;
assign s17 = b[17] ? {a[2:0],17'b00000000000000000} : 0;
assign s18 = b[18] ? {a[1:0],18'b000000000000000000} : 0;
assign s19 = b[19] ? {a[0:0],19'b0000000000000000000} : 0;
assign r = s0+s1+s2+s3+s4+s5+s6+s7+s8+s9+s10+s11+s12+s13+s14+s15+s16+s17+s18+s19;
endmodule
-------------------------------
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 1/8 [SYNTCOMP2014-RealSeq]
SOLVED_IN : 5.08432 [SYNTCOMP2014-RealSeq]
#.