Name: |
load_4c_comp_comp7_REAL.aag |
md5: |
07c4a09b5d394cd2af3eb98e6139ac9b |
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 11089 9 864 1 10216
2
4
6
8
10
12
14
16
18
20 0
22 4685
24 4689
26 4693
28 4697
30 4701
32 4705
34 4709
36 4717
38 0
40 4379
42 4383
44 4387
46 4391
48 4395
50 4399
52 4403
54 4411
56 0
58 4195
60 4199
62 4203
64 4207
66 4211
68 4215
70 4219
72 4227
74 4665
76 4667
78 4669
80 4671
82 4673
84 4675
86 4677
88 4679
90 4681
92 4231
94 4235
96 4239
98 4243
100 4247
102 4251
104 4255
106 4259
108 4263
110 0
112 3835
114 3839
116 3843
118 3847
120 3851
122 3855
124 3859
126 3867
128 0
130 3799
132 3803
134 380
... [truncated 177.5 kB]
863 latch863
o0 error
c
#!SYNTCOMP
SOLVED_BY : 0/3 [2015-pre-classification], 0/4 [SYNTCOMP2015-SyntSeq], 0/3 [SYNTCOMP2015-SyntPar], 3/7 [SYNTCOMP2015-RealSeq], 2/4 [SYNTCOMP2015-RealPar], 3/7 [SYNTCOMP2016-SyntSeq], 2/4 [SYNTCOMP2016-SyntPar], 6/11 [SYNTCOMP2016-RealSeq], 2/6 [SYNTCOMP2016-RealPar]
SOLVED_IN : 0.0 [2015-pre-classification], 76.1761 [SYNTCOMP2015-RealSeq], 87.8889 [SYNTCOMP2015-RealPar], 122.316 [SYNTCOMP2016-RealSeq], 107.342 [SYNTCOMP2016-RealPar]
REF_SIZE : 11530
STATUS : realizable
#.