% SZS status Satisfiable for TFF_Finite
% SZS output start FiniteModel for TFF_Finite
tff(declare_$i,type,$i:$tType).
tff(declare_$i1,type,fmb_$i_1:$i).
tff(finite_domain,axiom,
      ! [X:$i] : (
         X = fmb_$i_1
      ) ).

tff(declare_bool,type,$o:$tType).
tff(declare_bool1,type,fmb_bool_1:$o).
tff(finite_domain,axiom,
      ! [X:$o] : (
         X = fmb_bool_1
      ) ).

tff(declare_human,type,human:$tType).
tff(declare_human1,type,jon:human).
tff(finite_domain,axiom,
      ! [X:human] : (
         X = jon
      ) ).

tff(declare_cat,type,cat:$tType).
tff(declare_cat1,type,garfield:cat).
tff(declare_cat2,type,arlene:cat).
tff(declare_cat3,type,nermal:cat).
tff(finite_domain,axiom,
      ! [X:cat] : (
         X = garfield | X = arlene | X = nermal
      ) ).

tff(distinct_domain,axiom,
         garfield != arlene & garfield != nermal & arlene != nermal
).

tff(declare_d_human,type,d_human:$tType).
tff(declare_d_human1,type,d_jon:d_human).
tff(finite_domain,axiom,
      ! [X:d_human] : (
         X = d_jon
      ) ).

tff(declare_d_cat,type,d_cat:$tType).
tff(declare_d_cat1,type,d_garfield:d_cat).
tff(declare_d_cat2,type,d_arlene:d_cat).
tff(declare_d_cat3,type,d_nermal:d_cat).
tff(finite_domain,axiom,
      ! [X:d_cat] : (
         X = d_garfield | X = d_arlene | X = d_nermal
      ) ).

tff(distinct_domain,axiom,
         d_garfield != d_arlene & d_garfield != d_nermal & d_arlene != d_nermal
).

tff(declare_loves,type,loves: cat > cat).
tff(function_loves,axiom,
           loves(garfield) = garfield
         & loves(arlene) = garfield
         & loves(nermal) = garfield

).

tff(declare_d2human,type,d2human: d_human > human).
tff(function_d2human,axiom,
           d2human(d_jon) = jon

).

tff(declare_d2cat,type,d2cat: d_cat > cat).
tff(function_d2cat,axiom,
           d2cat(d_garfield) = garfield
         & d2cat(d_arlene) = arlene
         & d2cat(d_nermal) = nermal

).

tff(declare_owns,type,owns: human * cat > $o ).
tff(predicate_owns,axiom,
           owns(jon,garfield)
         & ~owns(jon,arlene)
         & ~owns(jon,nermal)

).

% SZS output end FiniteModel for TFF_Finite