Details of instance interface-with-overflows-k8-liveness.aag
Name: |
interface-with-overflows-k8-liveness.aag |
md5: |
73ea1b1fc04ea440be4bc9d32f35c532 |
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.5 kB)
aag 1963 7 51 1 1905
2
4
6
8
10
12
14
16 960
18 964
20 968
22 972
24 976
26 980
28 984
30 988
32 992
34 13
36 1016
38 1022
40 1028
42 1034
44 1040
46 1056
48 1064
50 1072
52 1080
54 1088
56 1094
58 1100
60 1106
62 1112
64 1118
66 1134
68 1188
70 1238
72 1312
74 1380
76 1397
78 2286
80 2672
82 2952
84 3170
86 3408
88 3632
90 3673
92 3696
94 3720
96 3737
98 3738
100 3797
102 3834
104 3839
106 3850
108 3856
110 3862
112 3864
114 3871
116 3913
3927
118 34 33
120 118 31
122 120 28
124 122 27
126 124 25
128 126 2
... [truncated 26.5 kB]
2015-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 : 6.13313 [2015-pre-classification], 3.28477 [SYNTCOMP2015-RealSeq], 1.378 [SYNTCOMP2015-RealPar], 2.276 [SYNTCOMP2016-RealSeq], 1.22531 [SYNTCOMP2016-RealPar], 3.192 [SYNTCOMP2017-RealSeq], 1.31625 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.