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 |
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
#.