%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : TOP018-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:34:21 PM UTC 2026
% Result : Satisfiable 0.17s 0.29s
% Output : FiniteModel 0.17s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('declare_$i2',type,
'fmb_$i_2': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' ) ) ).
tff('distinct_domain_$i',axiom,
'fmb_$i_1' != 'fmb_$i_2' ).
tff(declare_empty_set,type,
empty_set: $i ).
tff(empty_set_definition,axiom,
empty_set = 'fmb_$i_1' ).
tff(declare_a,type,
a: $i ).
tff(a_definition,axiom,
a = 'fmb_$i_1' ).
tff(declare_cx,type,
cx: $i ).
tff(cx_definition,axiom,
cx = 'fmb_$i_2' ).
tff(declare_ct,type,
ct: $i ).
tff(ct_definition,axiom,
ct = 'fmb_$i_1' ).
tff(declare_b,type,
b: $i ).
tff(b_definition,axiom,
b = 'fmb_$i_2' ).
tff(declare_union_of_members,type,
union_of_members: $i > $i ).
tff(function_union_of_members,axiom,
( ( union_of_members('fmb_$i_1') = 'fmb_$i_2' )
& ( union_of_members('fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f1,type,
f1: ( $i * $i ) > $i ).
tff(function_f1,axiom,
( ( f1('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f1('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f1('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f1('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_intersection_of_members,type,
intersection_of_members: $i > $i ).
tff(function_intersection_of_members,axiom,
( ( intersection_of_members('fmb_$i_1') = 'fmb_$i_2' )
& ( intersection_of_members('fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f2,type,
f2: ( $i * $i ) > $i ).
tff(function_f2,axiom,
( ( f2('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f2('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f2('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f2('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_intersection_of_sets,type,
intersection_of_sets: ( $i * $i ) > $i ).
tff(function_intersection_of_sets,axiom,
( ( intersection_of_sets('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( intersection_of_sets('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( intersection_of_sets('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( intersection_of_sets('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f3,type,
f3: ( $i * $i ) > $i ).
tff(function_f3,axiom,
( ( f3('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f3('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f3('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f3('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f5,type,
f5: ( $i * $i ) > $i ).
tff(function_f5,axiom,
( ( f5('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f5('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f5('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f5('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f4,type,
f4: ( $i * $i ) > $i ).
tff(function_f4,axiom,
( ( f4('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f4('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f4('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f4('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_relative_complement_sets,type,
relative_complement_sets: ( $i * $i ) > $i ).
tff(function_relative_complement_sets,axiom,
( ( relative_complement_sets('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( relative_complement_sets('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( relative_complement_sets('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( relative_complement_sets('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f6,type,
f6: ( $i * $i * $i * $i * $i ) > $i ).
tff(function_f6,axiom,
( ( f6('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f6('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f7,type,
f7: ( $i * $i ) > $i ).
tff(function_f7,axiom,
( ( f7('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f7('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f7('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f7('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f8,type,
f8: ( $i * $i ) > $i ).
tff(function_f8,axiom,
( ( f8('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f8('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f8('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f8('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f9,type,
f9: ( $i * $i ) > $i ).
tff(function_f9,axiom,
( ( f9('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f9('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f9('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f9('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_top_of_basis,type,
top_of_basis: $i > $i ).
tff(function_top_of_basis,axiom,
( ( top_of_basis('fmb_$i_1') = 'fmb_$i_2' )
& ( top_of_basis('fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f10,type,
f10: ( $i * $i * $i ) > $i ).
tff(function_f10,axiom,
( ( f10('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f10('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f10('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f10('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f10('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f10('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f10('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f10('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f11,type,
f11: ( $i * $i ) > $i ).
tff(function_f11,axiom,
( ( f11('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f11('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f11('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f11('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_subspace_topology,type,
subspace_topology: ( $i * $i * $i ) > $i ).
tff(function_subspace_topology,axiom,
( ( subspace_topology('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( subspace_topology('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( subspace_topology('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( subspace_topology('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( subspace_topology('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( subspace_topology('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( subspace_topology('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( subspace_topology('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f12,type,
f12: ( $i * $i * $i * $i ) > $i ).
tff(function_f12,axiom,
( ( f12('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f12('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f12('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f12('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f12('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f12('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f12('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f12('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f12('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f12('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f12('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f12('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f12('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f12('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f12('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f12('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_interior,type,
interior: ( $i * $i * $i ) > $i ).
tff(function_interior,axiom,
( ( interior('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( interior('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( interior('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( interior('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( interior('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( interior('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( interior('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( interior('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f13,type,
f13: ( $i * $i * $i * $i ) > $i ).
tff(function_f13,axiom,
( ( f13('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f13('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f13('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f13('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f13('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f13('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f13('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f13('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f13('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f13('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f13('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f13('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f13('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f13('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f13('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f13('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_closure,type,
closure: ( $i * $i * $i ) > $i ).
tff(function_closure,axiom,
( ( closure('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( closure('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( closure('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( closure('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( closure('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( closure('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( closure('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( closure('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f14,type,
f14: ( $i * $i * $i * $i ) > $i ).
tff(function_f14,axiom,
( ( f14('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f14('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f14('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f14('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f14('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f14('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f14('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f14('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f14('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f14('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f14('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f14('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f14('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f14('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f14('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f14('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f15,type,
f15: ( $i * $i * $i * $i * $i ) > $i ).
tff(function_f15,axiom,
( ( f15('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f15('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f16,type,
f16: ( $i * $i * $i * $i ) > $i ).
tff(function_f16,axiom,
( ( f16('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f16('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f16('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f16('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f16('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f16('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f16('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f16('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f16('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f16('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f16('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f16('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f16('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f16('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f16('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f16('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_boundary,type,
boundary: ( $i * $i * $i ) > $i ).
tff(function_boundary,axiom,
( ( boundary('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( boundary('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( boundary('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( boundary('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( boundary('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( boundary('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( boundary('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( boundary('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f17,type,
f17: ( $i * $i * $i * $i ) > $i ).
tff(function_f17,axiom,
( ( f17('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f17('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f17('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f17('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f17('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f17('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f17('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f17('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f17('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f17('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f17('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f17('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f17('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f17('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f17('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f17('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f18,type,
f18: ( $i * $i * $i * $i ) > $i ).
tff(function_f18,axiom,
( ( f18('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f18('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f18('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f18('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f18('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f18('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f18('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f18('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f18('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f18('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f18('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f18('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f18('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f18('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f18('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f18('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f19,type,
f19: ( $i * $i ) > $i ).
tff(function_f19,axiom,
( ( f19('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f19('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f19('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f19('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f20,type,
f20: ( $i * $i ) > $i ).
tff(function_f20,axiom,
( ( f20('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f20('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f20('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f20('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_union_of_sets,type,
union_of_sets: ( $i * $i ) > $i ).
tff(function_union_of_sets,axiom,
( ( union_of_sets('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( union_of_sets('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( union_of_sets('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( union_of_sets('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' ) ) ).
tff(declare_f21,type,
f21: ( $i * $i ) > $i ).
tff(function_f21,axiom,
( ( f21('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f21('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f21('fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( f21('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' ) ) ).
tff(declare_f22,type,
f22: ( $i * $i ) > $i ).
tff(function_f22,axiom,
( ( f22('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f22('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f22('fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( f22('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' ) ) ).
tff(declare_f23,type,
f23: ( $i * $i * $i ) > $i ).
tff(function_f23,axiom,
( ( f23('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f23('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f23('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f23('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( f23('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f23('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f23('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f23('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_f24,type,
f24: ( $i * $i ) > $i ).
tff(function_f24,axiom,
( ( f24('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( f24('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( f24('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( f24('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_element_of_set,type,
element_of_set: ( $i * $i ) > $o ).
tff(predicate_element_of_set,axiom,
( ~ element_of_set('fmb_$i_1','fmb_$i_1')
& ~ element_of_set('fmb_$i_1','fmb_$i_2')
& ~ element_of_set('fmb_$i_2','fmb_$i_1')
& ~ element_of_set('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_element_of_collection,type,
element_of_collection: ( $i * $i ) > $o ).
tff(predicate_element_of_collection,axiom,
( element_of_collection('fmb_$i_1','fmb_$i_1')
& element_of_collection('fmb_$i_1','fmb_$i_2')
& element_of_collection('fmb_$i_2','fmb_$i_1')
& element_of_collection('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_topological_space,type,
topological_space: ( $i * $i ) > $o ).
tff(predicate_topological_space,axiom,
( topological_space('fmb_$i_1','fmb_$i_1')
& topological_space('fmb_$i_1','fmb_$i_2')
& topological_space('fmb_$i_2','fmb_$i_1')
& topological_space('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_equal_sets,type,
equal_sets: ( $i * $i ) > $o ).
tff(predicate_equal_sets,axiom,
( ~ equal_sets('fmb_$i_1','fmb_$i_1')
& equal_sets('fmb_$i_1','fmb_$i_2')
& equal_sets('fmb_$i_2','fmb_$i_1')
& equal_sets('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_subset_collections,type,
subset_collections: ( $i * $i ) > $o ).
tff(predicate_subset_collections,axiom,
( ~ subset_collections('fmb_$i_1','fmb_$i_1')
& ~ subset_collections('fmb_$i_1','fmb_$i_2')
& ~ subset_collections('fmb_$i_2','fmb_$i_1')
& ~ subset_collections('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_open,type,
open: ( $i * $i * $i ) > $o ).
tff(predicate_open,axiom,
( open('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& open('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& open('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& open('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& open('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& open('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& open('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& open('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_closed,type,
closed: ( $i * $i * $i ) > $o ).
tff(predicate_closed,axiom,
( closed('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& closed('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& closed('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& closed('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& closed('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& closed('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& closed('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& closed('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_finer,type,
finer: ( $i * $i * $i ) > $o ).
tff(predicate_finer,axiom,
( ~ finer('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ finer('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ finer('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& ~ finer('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ finer('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ finer('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ finer('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ finer('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_basis,type,
basis: ( $i * $i ) > $o ).
tff(predicate_basis,axiom,
( basis('fmb_$i_1','fmb_$i_1')
& basis('fmb_$i_1','fmb_$i_2')
& basis('fmb_$i_2','fmb_$i_1')
& basis('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_subset_sets,type,
subset_sets: ( $i * $i ) > $o ).
tff(predicate_subset_sets,axiom,
( subset_sets('fmb_$i_1','fmb_$i_1')
& subset_sets('fmb_$i_1','fmb_$i_2')
& subset_sets('fmb_$i_2','fmb_$i_1')
& subset_sets('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_neighborhood,type,
neighborhood: ( $i * $i * $i * $i ) > $o ).
tff(predicate_neighborhood,axiom,
( ~ neighborhood('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ neighborhood('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ neighborhood('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& ~ neighborhood('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ neighborhood('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ neighborhood('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ neighborhood('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ neighborhood('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& ~ neighborhood('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ neighborhood('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ neighborhood('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& ~ neighborhood('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ neighborhood('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ neighborhood('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ neighborhood('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ neighborhood('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_limit_point,type,
limit_point: ( $i * $i * $i * $i ) > $o ).
tff(predicate_limit_point,axiom,
( limit_point('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& limit_point('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& limit_point('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& limit_point('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& limit_point('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& limit_point('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& limit_point('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& limit_point('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& limit_point('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& limit_point('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& limit_point('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& limit_point('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& limit_point('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& limit_point('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& limit_point('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& limit_point('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_eq_p,type,
eq_p: ( $i * $i ) > $o ).
tff(predicate_eq_p,axiom,
( eq_p('fmb_$i_1','fmb_$i_1')
& eq_p('fmb_$i_1','fmb_$i_2')
& eq_p('fmb_$i_2','fmb_$i_1')
& eq_p('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_hausdorff,type,
hausdorff: ( $i * $i ) > $o ).
tff(predicate_hausdorff,axiom,
( hausdorff('fmb_$i_1','fmb_$i_1')
& hausdorff('fmb_$i_1','fmb_$i_2')
& hausdorff('fmb_$i_2','fmb_$i_1')
& hausdorff('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_disjoint_s,type,
disjoint_s: ( $i * $i ) > $o ).
tff(predicate_disjoint_s,axiom,
( disjoint_s('fmb_$i_1','fmb_$i_1')
& ~ disjoint_s('fmb_$i_1','fmb_$i_2')
& ~ disjoint_s('fmb_$i_2','fmb_$i_1')
& ~ disjoint_s('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_separation,type,
separation: ( $i * $i * $i * $i ) > $o ).
tff(predicate_separation,axiom,
( ~ separation('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ separation('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& separation('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& separation('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ separation('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ separation('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ separation('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ separation('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& ~ separation('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ separation('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ separation('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& ~ separation('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ separation('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ separation('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ separation('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ separation('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_connected_space,type,
connected_space: ( $i * $i ) > $o ).
tff(predicate_connected_space,axiom,
( connected_space('fmb_$i_1','fmb_$i_1')
& connected_space('fmb_$i_1','fmb_$i_2')
& ~ connected_space('fmb_$i_2','fmb_$i_1')
& ~ connected_space('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_connected_set,type,
connected_set: ( $i * $i * $i ) > $o ).
tff(predicate_connected_set,axiom,
( connected_set('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& connected_set('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& connected_set('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& connected_set('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ connected_set('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ connected_set('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ connected_set('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ connected_set('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_open_covering,type,
open_covering: ( $i * $i * $i ) > $o ).
tff(predicate_open_covering,axiom,
( ~ open_covering('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ open_covering('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ open_covering('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& ~ open_covering('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ open_covering('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ open_covering('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ open_covering('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ open_covering('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_compact_space,type,
compact_space: ( $i * $i ) > $o ).
tff(predicate_compact_space,axiom,
( compact_space('fmb_$i_1','fmb_$i_1')
& compact_space('fmb_$i_1','fmb_$i_2')
& compact_space('fmb_$i_2','fmb_$i_1')
& compact_space('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_finite,type,
finite: $i > $o ).
tff(predicate_finite,axiom,
( ~ finite('fmb_$i_1')
& ~ finite('fmb_$i_2') ) ).
tff(declare_compact_set,type,
compact_set: ( $i * $i * $i ) > $o ).
tff(predicate_compact_set,axiom,
( compact_set('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& compact_set('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& compact_set('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& compact_set('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& compact_set('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& compact_set('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& compact_set('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& compact_set('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : TOP018-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n015.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 18:51:47 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.29 % (2895639)Will run a generic schedule for satisfiability detection.
% 0.17/0.29 % (2895648)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=919396293:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.17/0.29 % (2895645)% WARNING: option uhcvi not known.
% 0.17/0.29 % (2895644)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3035848696_2999 on theBenchmark for (2999ds/0Mi)
% 0.17/0.29 % (2895645)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1890506875:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.17/0.29 % (2895646)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1548944668:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.17/0.29 % (2895647)dis+10_1_sil=32000:sp=arity:random_seed=777330123:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.17/0.29 % (2895649)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=52466789:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.17/0.29 % (2895650)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2006842515:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.17/0.29 % TRYING [1]
% 0.17/0.29 % TRYING [2]
% 0.17/0.29 % Finite Model Found!
% 0.17/0.29 % SZS status Satisfiable for theBenchmark
% 0.17/0.29 % (2895644) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2895639-2895644"...
% 0.17/0.29 % (2895644)...printing done.
% 0.17/0.29 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.17/0.29 % (2895644)------------------------------
% 0.17/0.29 % (2895644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.29 % (2895644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.29 % (2895644)CaDiCaL version: 2.1.3
% 0.17/0.29 % (2895644)Termination reason: Satisfiable
% 0.17/0.29 % (2895644)Time elapsed: 0.016 s
% 0.17/0.29 % (2895644)Peak memory usage: 12 MB
% 0.17/0.29 % (2895644)Instructions burned: 33 (million)
% 0.17/0.29 % (2895639)Success in time 0.06 s
% 0.17/0.29 % Vampire exiting
%------------------------------------------------------------------------------