Details of instance bakery_sym1.aag

Name: bakery_sym1.aag
md5: e4c57192223104c0d1e7490fc1fa8d0e
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 (18.2 kB)
aag 1314 7 49 1 1258
2
4
6
8
10
12
14
16 1
18 124
20 126
22 211
24 235
26 373
28 461
30 493
32 521
34 655
36 743
38 775
40 803
42 1019
44 1043
46 1101
48 1125
50 1126
52 1128
54 1130
56 1132
58 1134
60 1136
62 803
64 1148
66 1150
68 1235
70 1259
72 1397
74 1485
76 1517
78 1545
80 1679
82 1767
84 1799
86 1827
88 2043
90 2067
92 2125
94 2149
96 2150
98 2152
100 2154
102 2156
104 2158
106 2160
108 2612
110 1
112 14
2628
114 5 3
116 4 2
118 117 115
120 118 2
122 121 115
124 123 2
126 123 4
128 29 27
130 128 31


... [truncated 17.2 kB]

33 pc<*1*>_out[1]_1
l34 pc<*1*>_out[2]_1
l35 pc<*1*>_out[3]_1
l36 ticket<*0*><0>_out[0]_1
l37 ticket<*1*><0>_out[0]_1
l38 ticket<*0*><1>_out[0]_1
l39 ticket<*1*><1>_out[0]_1
l40 j<*0*><0>_out[0]_1
l41 j<*1*><0>_out[0]_1
l42 j<*0*><1>_out[0]_1
l43 j<*1*><1>_out[0]_1
l44 k<0>_out[0]_1
l45 k<1>_out[0]_1
l46 sink
l47 init
l48 L: F 267
o0 AIGER_OR
c
aigor
disjunction of 1 original outputs
#!SYNTCOMP
STATUS : unrealizable
SOLVED_BY : 2/3 [2015-pre-classification]
SOLVED_IN : 0.107237 [2015-pre-classification]
#.