% SZS status Satisfiable for NTF_Finite-Finite-Local
% SZS output start FiniteModel for NTF_Finite-Finite-Local
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,$false:$o).
tff(declare_bool2,type,$true:$o).
tff(finite_domain,axiom,
      ! [X:$o] : (
         X = $false | X = $true
      ) ).

tff(distinct_domain,axiom,
         $false != $true
).

tff('declare_$ki_world',type,'$ki_world':$tType).
tff('declare_$ki_world1',type,'$ki_local_world':'$ki_world').
tff(finite_domain,axiom,
      ! [X:'$ki_world'] : (
         X = '$ki_local_world'
      ) ).

tff(declare_person,type,person:$tType).
tff(declare_person1,type,alex:person).
tff(finite_domain,axiom,
      ! [X:person] : (
         X = alex
      ) ).

tff(declare_product,type,product:$tType).
tff(declare_product1,type,leo:product).
tff(finite_domain,axiom,
      ! [X:product] : (
         X = leo
      ) ).

tff(declare_d_person,type,d_person:$tType).
tff(declare_d_person1,type,d_alex:d_person).
tff(finite_domain,axiom,
      ! [X:d_person] : (
         X = d_alex
      ) ).

tff(declare_d_product,type,d_product:$tType).
tff(declare_d_product1,type,d_leo:d_product).
tff(finite_domain,axiom,
      ! [X:d_product] : (
         X = d_leo
      ) ).

tff(declare_chris,type,chris:person).
tff(chris_definition,axiom,chris = alex).
tff(declare_w2,type,w2:'$ki_world').
tff(w2_definition,axiom,w2 = '$ki_local_world').
tff(declare_d_chris,type,d_chris:d_person).
tff(d_chris_definition,axiom,d_chris = d_alex).
tff(declare_d2person,type,d2person: d_person > person).
tff(function_d2person,axiom,
           d2person(d_alex) = alex

).

tff(declare_d2product,type,d2product: d_product > product).
tff(function_d2product,axiom,
           d2product(d_leo) = leo

).

tff('declare_$ki_accessible',type,'$ki_accessible': '$ki_world' * '$ki_world' > $o ).
tff('predicate_$ki_accessible',axiom,
%         '$ki_accessible'('$ki_local_world','$ki_local_world') undefined in model

).

tff('declare_$ki_world_is',type,'$ki_world_is': '$ki_world' * $o > $o ).
tff('predicate_$ki_world_is',axiom,
%         '$ki_world_is'('$ki_local_world',$false) undefined in model
%         '$ki_world_is'('$ki_local_world',$true) undefined in model

).

tff(declare_work_hard,type,work_hard: person * product > $o ).
tff(predicate_work_hard,axiom,
           work_hard(alex,leo)

).

tff(declare_gets_rich,type,gets_rich: person > $o ).
tff(predicate_gets_rich,axiom,
           ~gets_rich(alex)

).

% SZS output end FiniteModel for NTF_Finite-Finite-Local