Name: |
ltl2dba_06_2_REAL.aag |
md5: |
89d05ed85f0acfcdec7ae69113937e83 |
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 856 5 128 1 723
2
4
6
8
10
12 1117
14 1119
16 1121
18 1123
20 1525
22 1529
24 1533
26 1537
28 577
30 581
32 585
34 589
36 0
38 751
40 755
42 763
44 0
46 977
48 981
50 989
52 0
54 945
56 949
58 957
60 935
62 937
64 939
66 941
68 1007
70 1009
72 1011
74 1013
76 967
78 969
80 971
82 973
84 959
86 961
88 963
90 965
92 927
94 929
96 931
98 933
100 1607
102 1611
104 1615
106 1619
108 0
110 865
112 869
114 877
116 522
118 0
120 0
122 0
124 993
126 997
128 1001
130 1005
132 1639
134 1643
136 1647
138 1651
140 1
... [truncated 10.6 kB]
ch100
l101 latch101
l102 latch102
l103 latch103
l104 latch104
l105 latch105
l106 latch106
l107 latch107
l108 latch108
l109 latch109
l110 latch110
l111 latch111
l112 latch112
l113 latch113
l114 latch114
l115 latch115
l116 latch116
l117 latch117
l118 latch118
l119 latch119
l120 latch120
l121 latch121
l122 latch122
l123 latch123
l124 latch124
l125 latch125
l126 latch126
l127 latch127
o0 error
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 6/8 [SYNTCOMP2014-RealSeq]
SOLVED_IN : 0.556034 [SYNTCOMP2014-RealSeq]
#.