Details of instance ltl2dba_13_2_REAL.aag

Name: ltl2dba_13_2_REAL.aag
md5: 7ba9052c461fb563fd3e1eb6e8c955b8
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 (12.2 kB)
aag 914 4 108 1 802
2
4
6
8
10 0
12 853
14 857
16 865
18 1765
20 1769
22 1773
24 1777
26 487
28 491
30 495
32 499
34 0
36 1421
38 1425
40 1433
42 0
44 629
46 633
48 641
50 909
52 913
54 917
56 921
58 877
60 881
62 885
64 889
66 0
68 661
70 665
72 673
74 440
76 0
78 0
80 0
82 893
84 897
86 901
88 905
90 867
92 869
94 871
96 873
98 1221
100 1225
102 1229
104 1233
106 949
108 953
110 957
112 961
114 1373
116 1377
118 1381
120 1385
122 1389
124 1393
126 1397
128 1401
130 1739
132 1741
134 1743
136 1745
138 1717

... [truncated 11.2 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 : 7/8 [SYNTCOMP2014-RealSeq]
SOLVED_IN : 0.272016 [SYNTCOMP2014-RealSeq]
#.