| Name: |
demo-v18_2_UNREAL.aag |
| md5: |
9be42f46d1ee5bea617947a5ce790ff3 |
| 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 436 7 76 1 353
2
4
6
8
10
12
14
16 673
18 677
20 681
22 685
24 0
26 825
28 829
30 837
32 491
34 493
36 495
38 497
40 523
42 525
44 527
46 529
48 445
50 447
52 449
54 451
56 483
58 485
60 487
62 489
64 499
66 501
68 503
70 505
72 318
74 0
76 0
78 0
80 0
82 553
84 557
86 565
88 0
90 745
92 749
94 757
96 595
98 597
100 599
102 601
104 619
106 621
108 623
110 625
112 0
114 777
116 781
118 789
120 0
122 689
124 693
126 701
128 703
130 705
132 707
134 709
136 729
138 733
140 737
142 741
144 761
146 765
148 76
... [truncated 4.8 kB]
l60 latch60
l61 latch61
l62 latch62
l63 latch63
l64 latch64
l65 latch65
l66 latch66
l67 latch67
l68 latch68
l69 latch69
l70 latch70
l71 latch71
l72 latch72
l73 latch73
l74 latch74
l75 latch75
o0 error
c
#!SYNTCOMP
SOLVED_BY : 7/8 [SYNTCOMP2014-RealSeq], 4/4 [SYNTCOMP2015-SyntSeq], 3/3 [SYNTCOMP2015-SyntPar], 7/7 [SYNTCOMP2015-RealSeq], 4/4 [SYNTCOMP2015-RealPar]
SOLVED_IN : 2.02013 [SYNTCOMP2014-RealSeq], 1.35833 [SYNTCOMP2015-RealSeq], 0.093013 [SYNTCOMP2015-RealPar]
REF_SIZE : 0
STATUS : unrealizable
#.