| Name: |
load_full_4_comp2_REAL.aag |
| md5: |
501a4f8a74bf73967ae7219dd48f72d9 |
| 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 10070 9 1076 1 8985
2
4
6
8
10
12
14
16
18
20 4516
22 4520
24 4524
26 4528
28 4185
30 4187
32 4189
34 4191
36 0
38 4843
40 4845
42 4849
44 0
46 4843
48 4845
50 4849
52 0
54 4843
56 4845
58 4849
60 0
62 4843
64 4845
66 4849
68 0
70 4829
72 4833
74 4841
76 4651
78 4655
80 4659
82 4663
84 4651
86 4655
88 4659
90 4663
92 4651
94 4655
96 4659
98 4663
100 4651
102 4655
104 4659
106 4663
108 4651
110 4655
112 4659
114 4663
116 2586
118 0
120 0
122 0
124 4516
126 4520
128 4524
130 4528
132 4516
134 4520
136 452
... [truncated 165.4 kB]
h1067
l1068 latch1068
l1069 latch1069
l1070 latch1070
l1071 latch1071
l1072 latch1072
l1073 latch1073
l1074 latch1074
l1075 latch1075
o0 error
c
#!SYNTCOMP
SOLVED_BY : 1/11 [SYNTCOMP2016-RealSeq], 1/6 [SYNTCOMP2016-RealPar], 1/10 [SYNTCOMP2017-RealSeq], 1/6 [SYNTCOMP2017-RealPar], 1/6 [SYNTCOMP2017-SyntSeq], 1/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 88.388 [SYNTCOMP2016-RealSeq], 13.0127 [SYNTCOMP2016-RealPar], 92.668 [SYNTCOMP2017-RealSeq], 11.0336 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.