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 |
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]
#.