| Name: |
ltl2dba_R4_comp3_UNREAL.aag |
| md5: |
1a4488fa96d3edf8996ada4469baa4a4 |
| 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 11450 5 1365 1 10080
2
4
6
8
10
12 15279
14 15283
16 15287
18 15291
20 15295
22 13217
24 13219
26 13221
28 13223
30 13225
32 16581
34 16585
36 16589
38 16593
40 16597
42 15639
44 15643
46 15647
48 15651
50 15655
52 16601
54 16605
56 16609
58 16613
60 16617
62 19051
64 19055
66 19059
68 19063
70 19067
72 13777
74 13779
76 13781
78 13783
80 13785
82 0
84 18381
86 18385
88 18389
90 18397
92 20451
94 20455
96 20459
98 20463
100 20467
102 21141
104 21145
106 21149
108 21153
110 21157
112 17191
114 17195
116
... [truncated 188.2 kB]
5 latch1355
l1356 latch1356
l1357 latch1357
l1358 latch1358
l1359 latch1359
l1360 latch1360
l1361 latch1361
l1362 latch1362
l1363 latch1363
l1364 latch1364
o0 error
c
#!SYNTCOMP
SOLVED_BY : 1/3 [2016-pre-classification], 2/4 [2017-pre-classification], 4/10 [SYNTCOMP2017-RealSeq], 1/6 [SYNTCOMP2017-RealPar], 3/6 [SYNTCOMP2017-SyntSeq], 1/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 864.328 [2016-pre-classification], 461.708 [SYNTCOMP2017-RealSeq], 255.269 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.