Details of instance load_full_6_comp1_UNREAL.aag

Name: load_full_6_comp1_UNREAL.aag
md5: 0497190788c202e3afc98680117a63eb
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 (217.1 kB)
aag 12910 11 1335 1 11564
2
4
6
8
10
12
14
16
18
20
22
24 4908
26 4912
28 4916
30 4908
32 4912
34 4916
36 5393
38 5397
40 5401
42 0
44 5373
46 5377
48 0
50 5373
52 5377
54 0
56 5373
58 5377
60 0
62 5373
64 5377
66 5427
68 5429
70 5431
72 5427
74 5429
76 5431
78 5403
80 5405
82 5407
84 0
86 5373
88 5377
90 5343
92 5345
94 5347
96 5327
98 5331
100 5335
102 5343
104 5345
106 5347
108 5327
110 5331
112 5335
114 5393
116 5397
118 5401
120 5393
122 5397
124 5401
126 5343
128 5345
130 5347
132 3112
134 0
136 0
138

... [truncated 216.1 kB]


l1325 latch1325
l1326 latch1326
l1327 latch1327
l1328 latch1328
l1329 latch1329
l1330 latch1330
l1331 latch1331
l1332 latch1332
l1333 latch1333
l1334 latch1334
o0 error
c
#!SYNTCOMP
SOLVED_BY : 0/3 [2015-pre-classification], 1/4 [2017-pre-classification], 1/10 [SYNTCOMP2017-RealSeq], 1/6 [SYNTCOMP2017-RealPar], 1/6 [SYNTCOMP2017-SyntSeq], 1/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.0 [2015-pre-classification], 43.464 [SYNTCOMP2017-RealSeq], 8.50021 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.