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