Details of instance ltl2dba_06_2_REAL.aag

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
Download instance (11.6 kB)
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]
#.