Details of instance driver_d7y.aag

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
Download instance (23.8 kB)
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]
#.