Name: |
ltl2dpa_E4_comp2_REAL.aag |
md5: |
57665369bff9a56d99fb6b8cb306d168 |
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 11308 8 680 1 10620
2
4
6
8
10
12
14
16
18 0
20 1423
22 1427
24 1435
26 1397
28 28
30 30
32 32
34 0
36 21797
38 21801
40 21809
42 0
44 3567
46 3571
48 3579
50 19749
52 19753
54 19757
56 19761
58 19733
60 19737
62 19741
64 19745
66 19765
68 19769
70 19773
72 19777
74 12683
76 12685
78 12687
80 12689
82 12659
84 12661
86 12663
88 12665
90 12635
92 12637
94 12639
96 12641
98 19469
100 19473
102 19477
104 19481
106 12507
108 12509
110 12511
112 12513
114 12379
116 12381
118 12383
120 12385
122 12387
124 123
... [truncated 177.6 kB]
76
l677 latch677
l678 latch678
l679 latch679
o0 error
c
#!SYNTCOMP
SOLVED_BY : 0/3 [2016-pre-classification], 0/11 [SYNTCOMP2016-RealSeq], 1/6 [SYNTCOMP2016-RealPar], 0/4 [2017-pre-classification], 0/10 [SYNTCOMP2017-RealSeq], 1/6 [SYNTCOMP2017-RealPar], 0/6 [SYNTCOMP2017-SyntSeq], 1/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.0 [2016-pre-classification], 0.0 [SYNTCOMP2016-RealSeq], 818.471 [SYNTCOMP2016-RealPar], 0.0 [SYNTCOMP2017-RealSeq], 825.502 [SYNTCOMP2017-RealPar]
STATUS : realizable
REF_SIZE : 10864
#.