Name: |
cycle_sched_6_5_3.aag |
md5: |
b3319486de219eb26e0be1cc315e7821 |
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 3601 20 233 1 3348
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42 1
44 4881
46 4887
48 4893
50 4902
52 4912
54 4922
56 4932
58 4943
60 4952
62 4959
64 4965
66 4974
68 4984
70 4994
72 5004
74 5015
76 5024
78 5031
80 5037
82 5046
84 5056
86 5066
88 5076
90 5087
92 5096
94 5103
96 5109
98 5118
100 5128
102 5138
104 5148
106 5159
108 5168
110 5175
112 5181
114 5190
116 5200
118 5210
120 5220
122 5231
124 5240
126 5247
128 5253
130 5262
132 5272
134 5282
136 5292
138 5303
140 5312
142 5319
144 53
... [truncated 49.2 kB]
>
l212 _state_48<0>
l213 _state_46<0>
l214 _state_45<0>
l215 _state_44<0>
l216 _state_41<0>
l217 _state_38<0>
l218 _state_36<0>
l219 _state_33<0>
l220 _state_28<0>
l221 _state_23<0>
l222 _state_20<0>
l223 _state_19<0>
l224 _state_16<0>
l225 _state_14<0>
l226 _state_13<0>
l227 _state_10<0>
l228 _state_8<0>
l229 _state_7<0>
l230 _state_4<0>
l231 _state_2<0>
l232 _state_1<0>
o0 accept<0>
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 2/3 [2015-pre-classification]
SOLVED_IN : 4.63406 [2015-pre-classification]
#.