\* SPECIFICATION definition
SPECIFICATION
spec_157543427551222000
\* PROPERTY definition
PROPERTY
prop_157543427551223000
\* Generated on Wed Dec 04 12:37:55 CST 2019