| Name: |
load_full_2_comp5_REAL.aag |
| md5: |
535dec3855ce9278cc0b14dd52e0ede3 |
| 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 4032 5 427 1 3600
2
4
6
8
10
12 0
14 4057
16 4059
18 4061
20 4063
22 4065
24 4069
26 3807
28 3811
30 3815
32 3819
34 3823
36 3827
38 3831
40 3735
42 3739
44 3743
46 3747
48 3751
50 3755
52 3759
54 0
56 4085
58 4087
60 4089
62 4091
64 4093
66 4097
68 1214
70 0
72 0
74 0
76 0
78 0
80 0
82 0
84 4071
86 4073
88 4075
90 4077
92 4079
94 4083
96 0
98 4031
100 4035
102 4039
104 4043
106 4047
108 4055
110 3537
112 3541
114 3545
116 3549
118 3553
120 3557
122 3561
124 3521
126 3523
128 3525
130 3527
132 3529
134
... [truncated 59.4 kB]
5
l416 latch416
l417 latch417
l418 latch418
l419 latch419
l420 latch420
l421 latch421
l422 latch422
l423 latch423
l424 latch424
l425 latch425
l426 latch426
o0 error
c
#!SYNTCOMP
SOLVED_BY : 2/3 [2015-pre-classification], 4/4 [2017-pre-classification], 10/10 [SYNTCOMP2017-RealSeq], 6/6 [SYNTCOMP2017-RealPar], 4/6 [SYNTCOMP2017-SyntSeq], 4/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 4.06076 [2015-pre-classification], 5.704 [SYNTCOMP2017-RealSeq], 1.14429 [SYNTCOMP2017-RealPar]
REF_SIZE : 3792
STATUS : realizable
#.