FeatureModel.prf

(FeatureModel)
(FeatureModelFinite
 (names_TCC1 0
  (names_TCC1-1 nil 3658745567
   ("" (skolem 1 fm)
    (("" (typepred "features(fm)")
      (("" (expand is_finite) (("" (grind) nil nil)) nil)) nil))
    nil)
   ((FFM type-eq-decl nil FeatureModelFinite nil)
    (Formula_ type-decl nil Formula__adt nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil) (Name type-decl nil Name nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (injective? const-decl "bool" functions nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil))
   nil)))