| Name: |
demo-v3_5_REAL.aag |
| md5: |
f9be0f8aee6b1ccc39fc024fc55b849c |
| 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 556 4 84 1 468
2
4
6
8
10 0
12 1079
14 1081
16 1083
18 1085
20 1087
22 1091
24 0
26 773
28 779
30 785
32 791
34 797
36 809
38 0
40 887
42 893
44 899
46 905
48 911
50 923
52 0
54 509
56 515
58 521
60 527
62 533
64 545
66 0
68 811
70 813
72 815
74 817
76 819
78 823
80 829
82 835
84 841
86 847
88 853
90 859
92 865
94 0
96 969
98 973
100 977
102 981
104 985
106 993
108 0
110 941
112 945
114 949
116 953
118 957
120 965
122 0
124 925
126 927
128 929
130 931
132 933
134 937
136 867
138 869
140 871
142 873
144
... [truncated 6.3 kB]
7
l68 latch68
l69 latch69
l70 latch70
l71 latch71
l72 latch72
l73 latch73
l74 latch74
l75 latch75
l76 latch76
l77 latch77
l78 latch78
l79 latch79
l80 latch80
l81 latch81
l82 latch82
l83 latch83
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 : 0.016 [SYNTCOMP2014-RealSeq], 0.021805 [SYNTCOMP2015-RealSeq], 0.019158 [SYNTCOMP2015-RealPar]
REF_SIZE : 473
STATUS : realizable
#.