| Name: |
load_full_5_comp1_REAL.aag |
| md5: |
326a3eedcae62a294f3e427002978bd4 |
| 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 11971 11 1203 1 10757
2
4
6
8
10
12
14
16
18
20
22
24 4644
26 4648
28 4652
30 4644
32 4648
34 4652
36 5129
38 5133
40 5137
42 0
44 5109
46 5113
48 0
50 5109
52 5113
54 0
56 5109
58 5113
60 0
62 5109
64 5113
66 5163
68 5165
70 5167
72 5163
74 5165
76 5167
78 5139
80 5141
82 5143
84 0
86 5109
88 5113
90 5079
92 5081
94 5083
96 5063
98 5067
100 5071
102 5079
104 5081
106 5083
108 5063
110 5067
112 5071
114 5129
116 5133
118 5137
120 5129
122 5133
124 5137
126 5079
128 5081
130 5083
132 2848
134 0
136 0
138
... [truncated 198.6 kB]
2
l1193 latch1193
l1194 latch1194
l1195 latch1195
l1196 latch1196
l1197 latch1197
l1198 latch1198
l1199 latch1199
l1200 latch1200
l1201 latch1201
l1202 latch1202
o0 error
c
#!SYNTCOMP
SOLVED_BY : 0/3 [2015-pre-classification], 1/4 [2017-pre-classification], 1/10 [SYNTCOMP2017-RealSeq], 1/6 [SYNTCOMP2017-RealPar], 1/6 [SYNTCOMP2017-SyntSeq], 1/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.0 [2015-pre-classification], 30.72 [SYNTCOMP2017-RealSeq], 6.06483 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.