Name: |
load_full_3_comp1_UNREAL.aag |
md5: |
ba73b8d977bc2093343c83e8ec773213 |
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 3943 7 402 1 3534
2
4
6
8
10
12
14
16 3363
18 3365
20 3367
22 3363
24 3365
26 3367
28 2683
30 2685
32 2687
34 1987
36 1991
38 1995
40 1241
42 1245
44 1249
46 0
48 3347
50 3355
52 0
54 3347
56 3355
58 0
60 2623
62 2627
64 0
66 2623
68 2627
70 0
72 2623
74 2627
76 0
78 3267
80 3271
82 3233
84 3235
86 3237
88 3009
90 3013
92 3017
94 3287
96 3291
98 3295
100 3287
102 3291
104 3295
106 0
108 3339
110 3343
112 2601
114 2605
116 2609
118 2999
120 3001
122 3003
124 1130
126 0
128 0
130 0
132 2623
134 2627
136 3
... [truncated 57.5 kB]
375 latch375
l376 latch376
l377 latch377
l378 latch378
l379 latch379
l380 latch380
l381 latch381
l382 latch382
l383 latch383
l384 latch384
l385 latch385
l386 latch386
l387 latch387
l388 latch388
l389 latch389
l390 latch390
l391 latch391
l392 latch392
l393 latch393
l394 latch394
l395 latch395
l396 latch396
l397 latch397
l398 latch398
l399 latch399
l400 latch400
l401 latch401
o0 error
c
#!SYNTCOMP
STATUS : unrealizable
SOLVED_BY : 2/3 [2015-pre-classification]
SOLVED_IN : 81.9401 [2015-pre-classification]
#.