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

tff(declare_human,type,human:$tType).
tff(declare_human1,type,jon:human).
tff(finite_domain_human,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_cat,axiom,
      ! [X:cat] : (
         X = garfield | X = arlene | X = nermal
      ) ).

tff(distinct_domain_cat,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_d_human,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_d_cat,axiom,
      ! [X:d_cat] : (
         X = d_garfield | X = d_arlene | X = d_nermal
      ) ).

tff(distinct_domain_d_cat,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_SeparateDomains