% SZS status Satisfiable
% SZS output start Model
tff(d_level_val_1_type, type, (
   d_level_val_1: d_level)).
tff(d_middle_type, type, (
   d_middle: d_level)).
tff(d_level_val_3_type, type, (
   d_level_val_3: d_level)).
tff(d_space_type, type, (
   d_space: d_level)).
tff(d_level_val_0_type, type, (
   d_level_val_0: d_level)).
tff(d_ground_type, type, (
   d_ground: d_level)).
tff(d_level_val_2_type, type, (
   d_level_val_2: d_level)).
tff(d_top_type, type, (
   d_top: d_level)).
tff(level_val_0_type, type, (
   level_val_0: level)).
tff(level_val_1_type, type, (
   level_val_1: level)).
tff(level_val_2_type, type, (
   level_val_2: level)).
tff(possible_position_type, type, (
   possible_position: ( $int * $int * level ) > $o)).
tff(level_val_3_type, type, (
   level_val_3: level)).
tff(d2level_type, type, (
   d2level: d_level > level)).
tff(formula1, axiom,
    d_middle = d_level!val!1).
tff(formula2, axiom,
    d_space = d_level!val!3).
tff(formula3, axiom,
    d_ground = d_level!val!0).
tff(formula4, axiom,
    d_top = d_level!val!2).
tff(formula5, axiom,
    ![X0: $int, X1: $int, X2: level] : (possible_position(X0, X1, X2) <=> ((X0 = level!val!2) | (X0 = level!val!1) | (X0 = level!val!0)))).
tff(formula6, axiom,
    ![X0: d_level] : (d2level(X0) = ite_t((ite_t((X0 = d_level!val!2), d_level!val!2, ite_t((X0 = d_level!val!0), d_level!val!0, ite_t((X0 = d_level!val!3), d_level!val!3, d_level!val!1))) = d_level!val!3), level!val!3, ite_t((ite_t((X0 = d_level!val!2), d_level!val!2, ite_t((X0 = d_level!val!0), d_level!val!0, ite_t((X0 = d_level!val!3), d_level!val!3, d_level!val!1))) = d_level!val!2), level!val!0, ite_t((ite_t((X0 = d_level!val!2), d_level!val!2, ite_t((X0 = d_level!val!0), d_level!val!0, ite_t((X0 = d_level!val!3), d_level!val!3, d_level!val!1))) = d_level!val!1), level!val!2, level!val!1))))).
% SZS output end Model