| Name: |
ltl2dpa_C26_comp2_REAL.aag |
| md5: |
9a8a456c7b1fad5840b57528ddf495b8 |
| 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 2687 10 320 1 2357
2
4
6
8
10
12
14
16
18
20
22 0
24 707
26 711
28 719
30 681
32 32
34 34
36 36
38 4851
40 4855
42 4859
44 4863
46 3215
48 3219
50 3223
52 3227
54 3231
56 3235
58 3239
60 3243
62 2983
64 2987
66 2991
68 2995
70 5207
72 5211
74 5215
76 5219
78 3837
80 3841
82 3845
84 3849
86 0
88 3375
90 3379
92 3387
94 3159
96 3163
98 3167
100 3171
102 4527
104 4531
106 4535
108 4539
110 4423
112 4427
114 4431
116 4435
118 5135
120 5139
122 5143
124 5147
126 4407
128 4411
130 4415
132 4419
134 3119
136 3
... [truncated 38.8 kB]
7 latch317
l318 latch318
l319 latch319
o0 error
c
#!SYNTCOMP
SOLVED_BY : 3/3 [2016-pre-classification], 11/11 [SYNTCOMP2016-RealSeq], 6/6 [SYNTCOMP2016-RealPar], 4/4 [2017-pre-classification], 10/10 [SYNTCOMP2017-RealSeq], 6/6 [SYNTCOMP2017-RealPar], 6/6 [SYNTCOMP2017-SyntSeq], 4/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 4.996 [2016-pre-classification], 3.296 [SYNTCOMP2016-RealSeq], 5.47412 [SYNTCOMP2016-RealPar], 2.964 [SYNTCOMP2017-RealSeq], 5.6532 [SYNTCOMP2017-RealPar]
STATUS : realizable
REF_SIZE : 2463
#.