Details of instance ltl2dba_08_2_REAL.aag

Name: ltl2dba_08_2_REAL.aag
md5: f9542a95b65d22666cecd49e65c31d7d
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 (10.7 kB)
aag 802 6 108 1 688
2
4
6
8
10
12
14 1267
16 1271
18 1275
20 1279
22 444
24 0
26 0
28 0
30 1331
32 1335
34 1339
36 1343
38 1493
40 1497
42 1501
44 1505
46 1141
48 1145
50 1149
52 1153
54 1125
56 1129
58 1133
60 1137
62 0
64 657
66 661
68 669
70 0
72 689
74 693
76 701
78 0
80 1541
82 1545
84 1553
86 1299
88 1303
90 1307
92 1311
94 0
96 931
98 935
100 943
102 1157
104 1161
106 1165
108 1169
110 0
112 899
114 903
116 911
118 1173
120 1177
122 1181
124 1185
126 1189
128 1193
130 1197
132 1201
134 0
136 991
138 

... [truncated 9.7 kB]

latch77
l78 latch78
l79 latch79
l80 latch80
l81 latch81
l82 latch82
l83 latch83
l84 latch84
l85 latch85
l86 latch86
l87 latch87
l88 latch88
l89 latch89
l90 latch90
l91 latch91
l92 latch92
l93 latch93
l94 latch94
l95 latch95
l96 latch96
l97 latch97
l98 latch98
l99 latch99
l100 latch100
l101 latch101
l102 latch102
l103 latch103
l104 latch104
l105 latch105
l106 latch106
l107 latch107
o0 error
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 6/8 [SYNTCOMP2014-RealSeq]
SOLVED_IN : 0.348021 [SYNTCOMP2014-RealSeq]
#.