Details of instance atom_bakery_sym.aag

Name: atom_bakery_sym.aag
md5: 030667d9b524816b89d018ab88a7c02c
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 (27.9 kB) 
aag 1884 7 95 1 1782
2
4
6
8
10
12
14
16 1
18 206
20 211
22 212
24 214
26 216
28 221
30 226
32 228
34 337
36 361
38 385
40 575
42 691
44 753
46 789
48 975
50 1091
52 1153
54 1189
56 1375
58 1491
60 1553
62 1589
64 1590
66 1592
68 1594
70 1596
72 1619
74 1641
76 1663
78 1685
80 1707
82 1729
84 1730
86 1732
88 1734
90 1736
92 1738
94 1740
96 1742
98 1744
100 1746
102 1748
104 1750
106 1752
108 1589
110 1754
112 1759
114 1760
116 1762
118 1764
120 1769
122 1774
124 1776
126 1885
128 1909
130 1933
132 2123
134 

... [truncated 26.9 kB]

akery|defer<*0*><0>_out[0]_1
l84 bakery|defer<*1*><0>_out[0]_1
l85 bakery|defer<*2*><0>_out[0]_1
l86 bakery|defer<*0*><1>_out[0]_1
l87 bakery|defer<*1*><1>_out[0]_1
l88 bakery|defer<*2*><1>_out[0]_1
l89 bakery|defer<*0*><2>_out[0]_1
l90 bakery|defer<*1*><2>_out[0]_1
l91 bakery|defer<*2*><2>_out[0]_1
l92 sink
l93 init
l94 L: F 6363
o0 AIGER_OR
c
aigor
disjunction of 1 original outputs
#!SYNTCOMP
STATUS : unrealizable
SOLVED_BY : 2/3 [2015-pre-classification]
SOLVED_IN : 0.111362 [2015-pre-classification]
#.