| Name: |
ltl2dba_Q4_comp2_REAL.aag |
| md5: |
c04cff74781206eb062d9d441be28f9d |
| 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 7447 5 720 1 6722
2
4
6
8
10
12 0
14 8925
16 8929
18 8937
20 13133
22 13137
24 13141
26 13145
28 8539
30 8541
32 8543
34 8545
36 13877
38 13881
40 13885
42 13889
44 13893
46 13897
48 13901
50 13905
52 13909
54 13913
56 13917
58 13921
60 13925
62 13929
64 13933
66 13937
68 13941
70 13945
72 13949
74 13953
76 13957
78 13961
80 13965
82 13969
84 13973
86 13977
88 13981
90 13985
92 12861
94 12865
96 12869
98 12873
100 3693
102 3697
104 3701
106 3705
108 4261
110 4265
112 4269
114 4273
116 8883
118 8885
120
... [truncated 115.2 kB]
latch702
l703 latch703
l704 latch704
l705 latch705
l706 latch706
l707 latch707
l708 latch708
l709 latch709
l710 latch710
l711 latch711
l712 latch712
l713 latch713
l714 latch714
l715 latch715
l716 latch716
l717 latch717
l718 latch718
l719 latch719
o0 error
c
#!SYNTCOMP
SOLVED_BY : 2/3 [2016-pre-classification], 6/11 [SYNTCOMP2016-RealSeq], 4/6 [SYNTCOMP2016-RealPar]
SOLVED_IN : 72.976 [2016-pre-classification], 45.052 [SYNTCOMP2016-RealSeq], 61.2704 [SYNTCOMP2016-RealPar]
REF_SIZE : 0
STATUS : realizable
#.