Details of instance interface-with-overflows-k5-liveness.aag

Name: interface-with-overflows-k5-liveness.aag
md5: 4cf9df8e2be141e5ef8ee50967e91dae
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 (27.4 kB)
aag 1958 7 50 1 1901
2
4
6
8
10
12
14
16 958
18 962
20 966
22 970
24 974
26 978
28 982
30 986
32 990
34 13
36 1014
38 1020
40 1026
42 1032
44 1038
46 1054
48 1062
50 1070
52 1078
54 1086
56 1092
58 1098
60 1104
62 1110
64 1116
66 1132
68 1186
70 1236
72 1310
74 1378
76 1395
78 2284
80 2670
82 2950
84 3168
86 3406
88 3630
90 3671
92 3694
94 3718
96 3735
98 3736
100 3795
102 3832
104 3837
106 3846
108 3852
110 3854
112 3859
114 3901
3917
116 34 33
118 116 31
120 118 28
122 120 27
124 122 25
126 124 23
128 126

... [truncated 26.4 kB]

-RealPar], 7/7 [SYNTCOMP2016-SyntSeq], 4/4 [SYNTCOMP2016-SyntPar], 11/11 [SYNTCOMP2016-RealSeq], 6/6 [SYNTCOMP2016-RealPar], 10/10 [SYNTCOMP2017-RealSeq], 6/6 [SYNTCOMP2017-RealPar], 6/6 [SYNTCOMP2017-SyntSeq], 4/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 2.52992 [2015-pre-classification], 2.55133 [SYNTCOMP2015-RealSeq], 0.426354 [SYNTCOMP2015-RealPar], 1.172 [SYNTCOMP2016-RealSeq], 0.376617 [SYNTCOMP2016-RealPar], 2.04 [SYNTCOMP2017-RealSeq], 0.375851 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.