| Name: |
load_full_4_comp1_REAL.aag |
| md5: |
bbd30f1097c9e0e42c475f193c8cb1b5 |
| 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 7689 9 807 1 6873
2
4
6
8
10
12
14
16
18
20 3414
22 3418
24 3422
26 3165
28 3167
30 3169
32 0
34 3661
36 3665
38 0
40 3661
42 3665
44 0
46 3661
48 3665
50 0
52 3661
54 3665
56 0
58 3651
60 3659
62 3517
64 3521
66 3525
68 3517
70 3521
72 3525
74 3517
76 3521
78 3525
80 3517
82 3521
84 3525
86 3517
88 3521
90 3525
92 1944
94 0
96 0
98 3414
100 3418
102 3422
104 3414
106 3418
108 3422
110 3597
112 3601
114 3605
116 3583
118 3587
120 3591
122 3597
124 3601
126 3605
128 3597
130 3601
132 3605
134 3414
136 34
... [truncated 122.2 kB]
05
l806 latch806
o0 error
c
#!SYNTCOMP
SOLVED_BY : 0/3 [2015-pre-classification], 1/4 [SYNTCOMP2015-SyntSeq], 1/3 [SYNTCOMP2015-SyntPar], 1/7 [SYNTCOMP2015-RealSeq], 1/4 [SYNTCOMP2015-RealPar], 1/7 [SYNTCOMP2016-SyntSeq], 1/4 [SYNTCOMP2016-SyntPar], 2/11 [SYNTCOMP2016-RealSeq], 1/6 [SYNTCOMP2016-RealPar]
SOLVED_IN : 0.0 [2015-pre-classification], 14.2763 [SYNTCOMP2015-RealSeq], 3.87656 [SYNTCOMP2015-RealPar], 13.316 [SYNTCOMP2016-RealSeq], 3.4438 [SYNTCOMP2016-RealPar]
REF_SIZE : 0
STATUS : unrealizable
#.