| Name: |
load_3c_comp_comp4_REAL.aag |
| md5: |
fd4643e3172f4503c8a1f9616d16dd58 |
| 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 5671 7 444 1 5220
2
4
6
8
10
12
14
16 0
18 2877
20 2881
22 2885
24 2889
26 2897
28 0
30 2673
32 2677
34 2681
36 2685
38 2693
40 0
42 2551
44 2555
46 2559
48 2563
50 2571
52 2863
54 2865
56 2867
58 2869
60 2871
62 2873
64 2575
66 2579
68 2583
70 2587
72 2591
74 2595
76 0
78 2311
80 2315
82 2319
84 2323
86 2331
88 0
90 2287
92 2291
94 2295
96 2299
98 2307
100 1945
102 1949
104 1953
106 1957
108 1961
110 1965
112 0
114 2901
116 2905
118 2909
120 2913
122 2921
124 1921
126 1925
128 1929
130 1933
132 1937
13
... [truncated 83.1 kB]
32
l433 latch433
l434 latch434
l435 latch435
l436 latch436
l437 latch437
l438 latch438
l439 latch439
l440 latch440
l441 latch441
l442 latch442
l443 latch443
o0 error
c
#!SYNTCOMP
SOLVED_BY : 2/3 [2015-pre-classification], 4/4 [2017-pre-classification], 9/10 [SYNTCOMP2017-RealSeq], 6/6 [SYNTCOMP2017-RealPar], 6/6 [SYNTCOMP2017-SyntSeq], 4/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 6.04914 [2015-pre-classification], 9.156 [SYNTCOMP2017-RealSeq], 6.71649 [SYNTCOMP2017-RealPar]
REF_SIZE : 5285
STATUS : realizable
#.