Name: |
amba2match5.aag |
md5: |
f13e3a70094b9b7164e60cf7a6b7c079 |
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 4228 19 55 1 4154
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40 1
42 4
44 749
46 12
48 1130
50 1554
52 14
54 1758
56 3006
58 3074
60 3078
62 3087
64 10
66 2
68 6
70 3228
72 3326
74 3693
76 3723
78 3867
80 3908
82 3995
84 8
86 4124
88 3909
90 18
92 4725
94 26
96 5106
98 5530
100 28
102 5734
104 6982
106 7050
108 7054
110 7063
112 24
114 16
116 20
118 7204
120 7302
122 7669
124 7699
126 7843
128 7884
130 7971
132 22
134 8100
136 8416
138 1
140 30
142 32
144 34
146 36
148 38
8456
150 80 40
152 50
... [truncated 58.6 kB]
8 sink
l49 init
l50 L: F 5337
l51 L: X 9150
l52 L: X 7103
l53 L: X 6695
l54 L: X 404
c
#!SYNTCOMP
SOLVED_BY : 7/7 [SYNTCOMP2016-SyntSeq], 4/4 [SYNTCOMP2016-SyntPar], 11/11 [SYNTCOMP2016-RealSeq], 6/6 [SYNTCOMP2016-RealPar], 10/10 [SYNTCOMP2017-RealSeq], 6/6 [SYNTCOMP2017-RealPar], 6/6 [SYNTCOMP2017-SyntSeq], 4/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.288 [SYNTCOMP2016-RealSeq], 0.049547 [SYNTCOMP2016-RealPar], 0.284 [SYNTCOMP2017-RealSeq], 0.049658 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.