Name: |
ltl2dba_U1-4_comp3_REAL.aag |
md5: |
cee84057dbaf75f996143f1612870529 |
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 2880 5 255 1 2620
2
4
6
8
10
12 4545
14 4549
16 4553
18 4557
20 4561
22 4565
24 4569
26 4573
28 4577
30 4581
32 0
34 2543
36 2547
38 2551
40 2559
42 3473
44 3477
46 3481
48 3485
50 3489
52 5525
54 5529
56 5533
58 5537
60 5541
62 4605
64 4609
66 4613
68 4617
70 4621
72 4525
74 4529
76 4533
78 4537
80 4541
82 0
84 2413
86 2417
88 2421
90 2429
92 2493
94 2497
96 2501
98 2505
100 2509
102 3653
104 3657
106 3661
108 3665
110 3669
112 2433
114 2437
116 2441
118 2445
120 2449
122 4275
124 4279
126 4283
128 428
... [truncated 40.2 kB]
27
l228 latch228
l229 latch229
l230 latch230
l231 latch231
l232 latch232
l233 latch233
l234 latch234
l235 latch235
l236 latch236
l237 latch237
l238 latch238
l239 latch239
l240 latch240
l241 latch241
l242 latch242
l243 latch243
l244 latch244
l245 latch245
l246 latch246
l247 latch247
l248 latch248
l249 latch249
l250 latch250
l251 latch251
l252 latch252
l253 latch253
l254 latch254
o0 error
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 3/3 [2016-pre-classification]
SOLVED_IN : 10.38 [2016-pre-classification]
#.