% SZS status Satisfiable for NTF_Finite-Finite
% SZS output start FiniteModel for NTF_Finite-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,$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_fruit,type,fruit:$tType).
tff(declare_fruit1,type,apple:fruit).
tff(finite_domain,axiom,
      ! [X:fruit] : (
         X = apple
      ) ).

tff(declare_d_fruit,type,d_fruit:$tType).
tff(declare_d_fruit1,type,d_apple:d_fruit).
tff(finite_domain,axiom,
      ! [X:d_fruit] : (
         X = d_apple
      ) ).

tff(declare_banana,type,banana:fruit).
tff(banana_definition,axiom,banana = apple).
tff(declare_w2,type,w2:'$ki_world').
tff(w2_definition,axiom,w2 = '$ki_local_world').
tff(declare_d_banana,type,d_banana:d_fruit).
tff(d_banana_definition,axiom,d_banana = d_apple).
tff(declare_d2fruit,type,d2fruit: d_fruit > fruit).
tff(function_d2fruit,axiom,
           d2fruit(d_apple) = apple

).

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_healthy,type,healthy: fruit > $o ).
tff(predicate_healthy,axiom,
           healthy(apple)

).

tff(declare_rotten,type,rotten: fruit > $o ).
tff(predicate_rotten,axiom,
           ~rotten(apple)

).

% SZS output end FiniteModel for NTF_Finite-Finite