Name: |
cycle_sched_12_7_2.aag |
md5: |
f734017700fd9aa4e01043cdd81ae658 |
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 5098 38 587 1 4473
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42
44
46
48
50
52
54
56
58
60
62
64
66
68
70
72
74
76
78 1
80 3865
82 3871
84 3877
86 3886
88 3896
90 3906
92 3916
94 3926
96 3936
98 3947
100 3956
102 3963
104 3969
106 3978
108 3988
110 3998
112 4008
114 4018
116 4028
118 4039
120 4048
122 4055
124 4061
126 4070
128 4080
130 4090
132 4100
134 4110
136 4120
138 4131
140 4140
142 4147
144 4153
146 4162
148 4172
150 4182
152 4192
154 4202
156 4212
158 4223
160 4232
162 4239
164 42
... [truncated 74.6 kB]
>
l566 _state_40<0>
l567 _state_38<0>
l568 _state_37<0>
l569 _state_34<0>
l570 _state_32<0>
l571 _state_31<0>
l572 _state_28<0>
l573 _state_26<0>
l574 _state_25<0>
l575 _state_22<0>
l576 _state_20<0>
l577 _state_19<0>
l578 _state_16<0>
l579 _state_14<0>
l580 _state_13<0>
l581 _state_10<0>
l582 _state_8<0>
l583 _state_7<0>
l584 _state_4<0>
l585 _state_2<0>
l586 _state_1<0>
o0 accept<0>
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 1/3 [2015-pre-classification]
SOLVED_IN : 570.982 [2015-pre-classification]
#.