%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV918-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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 01:26:39 PM UTC 2026
% Result : Satisfiable 0.07s 0.25s
% Output : FiniteModel 0.07s
% 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_true,type,
true: $i ).
tff(true_definition,axiom,
true = 'fmb_$i_1' ).
tff(declare_v_P,type,
v_P: $i ).
tff(v_P_definition,axiom,
v_P = 'fmb_$i_1' ).
tff(declare_v_ha____,type,
v_ha____: $i ).
tff(v_ha_____definition,axiom,
v_ha____ = 'fmb_$i_1' ).
tff(declare_tc_String_Ochar,type,
tc_String_Ochar: $i ).
tff(tc_String_Ochar_definition,axiom,
tc_String_Ochar = 'fmb_$i_1' ).
tff(declare_t_a,type,
t_a: $i ).
tff(t_a_definition,axiom,
t_a = 'fmb_$i_1' ).
tff(declare_v_h_Ha____,type,
v_h_Ha____: $i ).
tff(v_h_Ha_____definition,axiom,
v_h_Ha____ = 'fmb_$i_2' ).
tff(declare_v_a____,type,
v_a____: $i ).
tff(v_a_____definition,axiom,
v_a____ = 'fmb_$i_1' ).
tff(declare_v_C____,type,
v_C____: $i ).
tff(v_C_____definition,axiom,
v_C____ = 'fmb_$i_1' ).
tff(declare_v_FDTs____,type,
v_FDTs____: $i ).
tff(v_FDTs_____definition,axiom,
v_FDTs____ = 'fmb_$i_1' ).
tff(declare_tc_Value_Oval,type,
tc_Value_Oval: $i ).
tff(tc_Value_Oval_definition,axiom,
tc_Value_Oval = 'fmb_$i_1' ).
tff(declare_tc_nat,type,
tc_nat: $i ).
tff(tc_nat_definition,axiom,
tc_nat = 'fmb_$i_1' ).
tff(declare_ifeq2,type,
ifeq2: ( $i * $i * $i * $i ) > $i ).
tff(function_ifeq2,axiom,
( ( ifeq2('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( ifeq2('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( ifeq2('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( ifeq2('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq2('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( ifeq2('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq2('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( ifeq2('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq2('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( ifeq2('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq2('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( ifeq2('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq2('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( ifeq2('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( ifeq2('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( ifeq2('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_ifeq,type,
ifeq: ( $i * $i * $i * $i ) > $i ).
tff(function_ifeq,axiom,
( ( ifeq('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( ifeq('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( ifeq('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( ifeq('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( ifeq('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( ifeq('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( ifeq('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_c_COMBI,type,
c_COMBI: ( $i * $i ) > $i ).
tff(function_c_COMBI,axiom,
( ( c_COMBI('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_COMBI('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_COMBI('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_COMBI('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_c_Conform_Ohconf,type,
c_Conform_Ohconf: ( $i * $i * $i ) > $i ).
tff(function_c_Conform_Ohconf,axiom,
( ( c_Conform_Ohconf('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_Conform_Ohconf('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Conform_Ohconf('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Conform_Ohconf('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Conform_Ohconf('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_Conform_Ohconf('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Conform_Ohconf('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Conform_Ohconf('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_c_Exceptions_Opreallocated,type,
c_Exceptions_Opreallocated: $i > $i ).
tff(function_c_Exceptions_Opreallocated,axiom,
( ( c_Exceptions_Opreallocated('fmb_$i_1') = 'fmb_$i_1' )
& ( c_Exceptions_Opreallocated('fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_tc_List_Olist,type,
tc_List_Olist: $i > $i ).
tff(function_tc_List_Olist,axiom,
( ( tc_List_Olist('fmb_$i_1') = 'fmb_$i_2' )
& ( tc_List_Olist('fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_tc_Expr_Oexp,type,
tc_Expr_Oexp: $i > $i ).
tff(function_tc_Expr_Oexp,axiom,
( ( tc_Expr_Oexp('fmb_$i_1') = 'fmb_$i_2' )
& ( tc_Expr_Oexp('fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_tc_prod,type,
tc_prod: ( $i * $i ) > $i ).
tff(function_tc_prod,axiom,
( ( tc_prod('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( tc_prod('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( tc_prod('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( tc_prod('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_c_Objects_Oinit__fields,type,
c_Objects_Oinit__fields: $i > $i ).
tff(function_c_Objects_Oinit__fields,axiom,
( ( c_Objects_Oinit__fields('fmb_$i_1') = 'fmb_$i_1' )
& ( c_Objects_Oinit__fields('fmb_$i_2') = 'fmb_$i_1' ) ) ).
tff(declare_tc_Option_Ooption,type,
tc_Option_Ooption: $i > $i ).
tff(function_tc_Option_Ooption,axiom,
( ( tc_Option_Ooption('fmb_$i_1') = 'fmb_$i_1' )
& ( tc_Option_Ooption('fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_tc_fun,type,
tc_fun: ( $i * $i ) > $i ).
tff(function_tc_fun,axiom,
( ( tc_fun('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( tc_fun('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( tc_fun('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( tc_fun('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_c_Pair,type,
c_Pair: ( $i * $i * $i * $i ) > $i ).
tff(function_c_Pair,axiom,
( ( c_Pair('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Pair('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Pair('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Pair('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Pair('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Pair('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Pair('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Pair('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Pair('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Pair('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Pair('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Pair('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Pair('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Pair('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Pair('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Pair('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_c_Option_Ooption_OSome,type,
c_Option_Ooption_OSome: ( $i * $i ) > $i ).
tff(function_c_Option_Ooption_OSome,axiom,
( ( c_Option_Ooption_OSome('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Option_Ooption_OSome('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Option_Ooption_OSome('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Option_Ooption_OSome('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_c_Fun_Ofun__upd,type,
c_Fun_Ofun__upd: ( $i * $i * $i * $i * $i ) > $i ).
tff(function_c_Fun_Ofun__upd,axiom,
( ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Ofun__upd('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_c_Conform_Ooconf,type,
c_Conform_Ooconf: ( $i * $i * $i * $i ) > $i ).
tff(function_c_Conform_Ooconf,axiom,
( ( c_Conform_Ooconf('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Conform_Ooconf('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Conform_Ooconf('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Conform_Ooconf('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Conform_Ooconf('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Conform_Ooconf('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Conform_Ooconf('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Conform_Ooconf('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Conform_Ooconf('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Conform_Ooconf('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Conform_Ooconf('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Conform_Ooconf('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Conform_Ooconf('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Conform_Ooconf('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Conform_Ooconf('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Conform_Ooconf('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_hAPP,type,
hAPP: ( $i * $i ) > $i ).
tff(function_hAPP,axiom,
( ( hAPP('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( hAPP('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( hAPP('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( hAPP('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_c_Option_Ooption_ONone,type,
c_Option_Ooption_ONone: $i > $i ).
tff(function_c_Option_Ooption_ONone,axiom,
( ( c_Option_Ooption_ONone('fmb_$i_1') = 'fmb_$i_2' )
& ( c_Option_Ooption_ONone('fmb_$i_2') = 'fmb_$i_1' ) ) ).
tff(declare_c_fequal,type,
c_fequal: ( $i * $i * $i ) > $i ).
tff(function_c_fequal,axiom,
( ( c_fequal('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_fequal('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_fequal('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_fequal('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_fequal('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_fequal('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_fequal('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_fequal('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' ) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV918-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n013.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 12:52:51 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.22 Running first-order model finding
% 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.25 % (1155406)Will run a generic schedule for satisfiability detection.
% 0.07/0.25 % (1155411)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1126502407_2999 on theBenchmark for (2999ds/0Mi)
% 0.07/0.25 % TRYING [1]
% 0.07/0.25 % TRYING [2]
% 0.07/0.25 % Finite Model Found!
% 0.07/0.25 % SZS status Satisfiable for theBenchmark
% 0.07/0.25 % (1155411) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1155406-1155411"...
% 0.07/0.25 % (1155411)...printing done.
% 0.07/0.25 % (1155412)% WARNING: option uhcvi not known.
% 0.07/0.25 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.07/0.26 % (1155411)------------------------------
% 0.07/0.26 % (1155411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.07/0.26 % (1155411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.07/0.26 % (1155411)CaDiCaL version: 2.1.3
% 0.07/0.26 % (1155411)Termination reason: Satisfiable
% 0.07/0.26 % (1155411)Time elapsed: 0.002 s
% 0.07/0.26 % (1155411)Peak memory usage: 11 MB
% 0.07/0.26 % (1155411)Instructions burned: 6 (million)
% 0.07/0.26 % (1155406)Success in time 0.029 s
% 0.07/0.26 % Vampire exiting
%------------------------------------------------------------------------------