Details of instance good_bakery.wuntil.aag

Name: good_bakery.wuntil.aag
md5: 2f4e4bbf6b78348d007a660ef7462f82
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 (81.0 kB)
aag 5467 12 195 1 5260
2
4
6
8
10
12
14
16
18
20
22
24
26 1
28 420
30 422
32 1105
34 1153
36 1235
38 1325
40 1357
42 1385
44 1413
46 1535
48 1603
50 1671
52 1739
54 1807
56 1875
58 1943
60 2011
62 2079
64 2141
66 2203
68 2265
70 2313
72 2359
74 2405
76 2453
78 2521
80 2583
82 2645
84 2721
86 2785
88 2849
90 2917
92 2985
94 3053
96 3054
98 3056
100 3107
102 3173
104 3233
106 3291
108 3351
110 3413
112 3471
114 3531
116 3591
118 3651
120 1
122 3656
124 3658
126 4341
128 4389
130 4471
132 4561
134 4593
136 462

... [truncated 80.0 kB]


l173 l75_copy
l174 l76_copy
l175 l77_copy
l176 l78_copy
l177 l79_copy
l178 l80_copy
l179 l81_copy
l180 l82_copy
l181 l83_copy
l182 l84_copy
l183 l85_copy
l184 l86_copy
l185 l87_copy
l186 l88_copy
l187 l89_copy
l188 l90_copy
l189 l91_copy
l190 l92_copy
l191 l93_copy
l192 l94_copy
l193 l95_copy
l194 L_MH:U(And(Neg(select<1>0))(Neg(...
o0 AIGER_OR
c
aigor
disjunction of 2 original outputs
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 2/3 [2015-pre-classification]
SOLVED_IN : 2.98604 [2015-pre-classification]
#.