| Name: |
load_5c_comp_comp4_REAL.aag |
| md5: |
2e5209c204cc9e219036361e846e8f9c |
| 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 9487 11 708 1 8768
2
4
6
8
10
12
14
16
18
20
22
24 0
26 3481
28 3485
30 3489
32 3493
34 3501
36 0
38 3277
40 3281
42 3285
44 3289
46 3297
48 0
50 3151
52 3155
54 3159
56 3163
58 3171
60 3467
62 3469
64 3471
66 3473
68 3475
70 3477
72 3175
74 3179
76 3183
78 3187
80 3191
82 3195
84 0
86 2911
88 2915
90 2919
92 2923
94 2931
96 0
98 2887
100 2891
102 2895
104 2899
106 2907
108 2541
110 2545
112 2549
114 2553
116 2557
118 2561
120 0
122 3505
124 3509
126 3513
128 3517
130 3525
132 2517
134 2521
136 2525
138
... [truncated 148.8 kB]
tch706
l707 latch707
o0 error
c
#!SYNTCOMP
SOLVED_BY : 0/3 [2015-pre-classification], 0/4 [SYNTCOMP2015-SyntSeq], 0/3 [SYNTCOMP2015-SyntPar], 2/7 [SYNTCOMP2015-RealSeq], 1/4 [SYNTCOMP2015-RealPar], 0/7 [SYNTCOMP2016-SyntSeq], 0/4 [SYNTCOMP2016-SyntPar], 0/11 [SYNTCOMP2016-RealSeq], 1/6 [SYNTCOMP2016-RealPar]
SOLVED_IN : 0.0 [2015-pre-classification], 906.938 [SYNTCOMP2015-RealSeq], 1615.78 [SYNTCOMP2015-RealPar], 0.0 [SYNTCOMP2016-RealSeq], 1378.55 [SYNTCOMP2016-RealPar]
REF_SIZE : 0
STATUS : realizable
#.