Name: |
lilydemo21.tlsf |
md5: |
9904d99464ba9aa9255514f56c49ea8a |
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 |
INFO {
TITLE: "Lily Demo V21"
DESCRIPTION: "One of the Lily demo files"
SEMANTICS: Mealy
TARGET: Mealy
}
MAIN {
INPUTS {
r1;
r2;
r3;
r4;
}
OUTPUTS {
g1;
g2;
g3;
g4;
}
ASSUMPTIONS {
G (!r1 || !r2);
G (!r1 || !r3);
G (!r1 || !r4);
G (!r2 || !r3);
G (!r2 || !r4);
G (!r3 || !r4);
}
INVARIANTS {
G (r1 -> (X g1 || X X g1 || X X X g1));
G (r2 -> (X g2 || X X g2 || X X X g2));
G (r3 -> (X g3 || X X g3 || X X X g3));
G (r4 -> (X g4 || X X g4 || X X X g4));
!g1 || !g2;
!g1 || !g3;
!g1 || !g4;
!g2 || !g3;
!g2 || !g4;
!g3 || !g4;
}
}
//#!SYNTCOMP
//STATUS : realizable
//REF_SIZE : 14
//#.