Name: |
driver_d7y.aag |
md5: |
a09043aa9b3551597cf9ef717d2419d7 |
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 530 40 55 1 435
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 229
86 237
88 245
90 257
92 265
94 279
96 287
98 295
100 303
102 311
104 319
106 327
108 335
110 405
112 417
114 424
116 439
118 447
120 455
122 463
124 471
126 479
128 495
130 505
132 515
134 12
136 8
138 631
140 643
142 649
144 655
146 661
148 921
150 941
152 951
154 959
156 965
158 971
160 977
162 983
164 989
166 10
168 990
170 996
172 1002
174 1013
176 1019
178
... [truncated 22.8 kB]
= next_state_os_lba0_abs ;
state_os_lba1_abs = next_state_os_lba1_abs ;
state_os_sect0_abs = next_state_os_sect0_abs ;
state_os_sect1_abs = next_state_os_sect1_abs ;
state_os_buf_abs = next_state_os_buf_abs ;
state_osState_conc = next_state_osState_conc ;
end
endmodule
-------------------------------
#!SYNTCOMP
STATUS : unrealizable
SOLVED_BY : 3/3 [2015-pre-classification]
SOLVED_IN : 4.77608 [2015-pre-classification]
#.