| Name: |
load_4c_comp_comp1_UNREAL.aag |
| md5: |
43906af8f6731b85796fe57b6ee22a0c |
| 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 4027 9 288 1 3730
2
4
6
8
10
12
14
16
18
20 0
22 1673
24 1681
26 0
28 1571
30 1579
32 0
34 1507
36 1515
38 1665
40 1667
42 1669
44 1519
46 1523
48 1527
50 0
52 1387
54 1395
56 0
58 1375
60 1383
62 1199
64 1203
66 1207
68 0
70 1685
72 1693
74 1187
76 1191
78 1195
80 1547
82 1551
84 1555
86 1531
88 1535
90 1539
92 1655
94 1659
96 1663
98 1697
100 1701
102 1705
104 1559
106 1563
108 1567
110 1643
112 1647
114 1651
116 1631
118 1635
120 1639
122 0
124 3429
126 3437
128 0
130 3417
132 3425
134 0
136 3075
138
... [truncated 56.2 kB]
latch287
o0 error
c
#!SYNTCOMP
SOLVED_BY : 2/3 [2015-pre-classification], 4/4 [SYNTCOMP2015-SyntSeq], 3/3 [SYNTCOMP2015-SyntPar], 7/7 [SYNTCOMP2015-RealSeq], 4/4 [SYNTCOMP2015-RealPar], 7/7 [SYNTCOMP2016-SyntSeq], 4/4 [SYNTCOMP2016-SyntPar], 11/11 [SYNTCOMP2016-RealSeq], 6/6 [SYNTCOMP2016-RealPar]
SOLVED_IN : 4.66452 [2015-pre-classification], 4.05872 [SYNTCOMP2015-RealSeq], 0.978301 [SYNTCOMP2015-RealPar], 5.132 [SYNTCOMP2016-RealSeq], 0.905955 [SYNTCOMP2016-RealPar]
REF_SIZE : 0
STATUS : unrealizable
#.