Name: |
cycle_sched_2_3_1.aag |
md5: |
ada6790449cfc2cabb2dd8d8baeac0a8 |
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 529 7 59 1 463
2
4
6
8
10
12
14
16 1
18 517
20 523
22 529
24 538
26 548
28 559
30 568
32 575
34 581
36 590
38 600
40 611
42 620
44 627
46 633
48 643
50 652
52 662
54 672
56 679
58 685
60 695
62 704
64 714
66 724
68 731
70 737
72 747
74 753
76 759
78 765
80 774
82 784
84 794
86 801
88 807
90 817
92 823
94 833
96 845
98 851
100 857
102 867
104 873
106 879
108 885
110 894
112 904
114 914
116 921
118 927
120 937
122 943
124 953
126 965
128 971
130 994
132 1001
1059
134 17 1
136 43 1
138 10 137
140 139 10
14
... [truncated 5.6 kB]
te_49<0>
l37 _state_47<0>
l38 _state_44<0>
l39 _state_41<0>
l40 _state_40<0>
l41 _state_37<0>
l42 _state_34<0>
l43 _state_32<0>
l44 _state_30<0>
l45 _state_28<0>
l46 _state_26<0>
l47 _state_24<0>
l48 _state_23<0>
l49 _state_22<0>
l50 _state_19<0>
l51 _state_16<0>
l52 _state_14<0>
l53 _state_11<0>
l54 _state_8<0>
l55 _state_7<0>
l56 _state_4<0>
l57 _state_2<0>
l58 _state_1<0>
o0 accept<0>
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 3/3 [2015-pre-classification]
SOLVED_IN : 0.03 [2015-pre-classification]
#.