| Name: |
demo-v24_5_REAL.aag |
| md5: |
40ed926d2bd78188a867aeb380f68e23 |
| 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 2343 8 280 1 2055
2
4
6
8
10
12
14
16
18 1136
20 0
22 0
24 0
26 0
28 0
30 0
32 1713
34 1715
36 1717
38 1719
40 1721
42 1723
44 1725
46 4221
48 4225
50 4229
52 4233
54 4237
56 4241
58 4245
60 1475
62 1477
64 1479
66 1481
68 1483
70 1485
72 1487
74 3913
76 3917
78 3921
80 3925
82 3929
84 3933
86 3937
88 1491
90 1495
92 1499
94 1503
96 1507
98 1511
100 1515
102 3519
104 3521
106 3523
108 3525
110 3527
112 3529
114 3531
116 3703
118 3707
120 3711
122 3715
124 3719
126 3723
128 3727
130 1729
132 1733
134 173
... [truncated 33.6 kB]
4
l275 latch275
l276 latch276
l277 latch277
l278 latch278
l279 latch279
o0 error
c
#!SYNTCOMP
SOLVED_BY : 6/8 [SYNTCOMP2014-RealSeq], 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 : 3.98025 [SYNTCOMP2014-RealSeq], 0.248 [SYNTCOMP2016-RealSeq], 0.61459 [SYNTCOMP2016-RealPar], 0.164 [SYNTCOMP2017-RealSeq], 0.618378 [SYNTCOMP2017-RealPar]
STATUS : realizable
REF_SIZE : 2059
#.