% 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