%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV595-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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:05 PM UTC 2026
% Result : Satisfiable 2.02s 0.62s
% Output : FiniteModel 2.02s
% 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('declare_$i3',type,
'fmb_$i_3': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' )
| ( X = 'fmb_$i_3' ) ) ).
tff('distinct_domain_$i',axiom,
( ( 'fmb_$i_1' != 'fmb_$i_2' )
& ( 'fmb_$i_1' != 'fmb_$i_3' )
& ( 'fmb_$i_2' != 'fmb_$i_3' ) ) ).
tff(declare_tc_RealDef_Oreal,type,
tc_RealDef_Oreal: $i ).
tff(tc_RealDef_Oreal_definition,axiom,
tc_RealDef_Oreal = 'fmb_$i_1' ).
tff(declare_v_x,type,
v_x: $i ).
tff(v_x_definition,axiom,
v_x = 'fmb_$i_1' ).
tff(declare_t_a,type,
t_a: $i ).
tff(t_a_definition,axiom,
t_a = 'fmb_$i_1' ).
tff(declare_c_Transcendental_Opi,type,
c_Transcendental_Opi: $i ).
tff(c_Transcendental_Opi_definition,axiom,
c_Transcendental_Opi = 'fmb_$i_1' ).
tff(declare_c_HOL_Otimes__class_Otimes,type,
c_HOL_Otimes__class_Otimes: ( $i * $i * $i ) > $i ).
tff(function_c_HOL_Otimes__class_Otimes,axiom,
( ( c_HOL_Otimes__class_Otimes('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_3' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_1','fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_1','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_1','fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_1','fmb_$i_3','fmb_$i_2') = 'fmb_$i_1' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_1','fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_2','fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_2','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_2','fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_2','fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_2','fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_3','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_3','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_3','fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_3','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_3','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_3','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_3','fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_3','fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_HOL_Otimes__class_Otimes('fmb_$i_3','fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_HOL_Ouminus__class_Ouminus,type,
c_HOL_Ouminus__class_Ouminus: ( $i * $i ) > $i ).
tff(function_c_HOL_Ouminus__class_Ouminus,axiom,
( ( c_HOL_Ouminus__class_Ouminus('fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_HOL_Ouminus__class_Ouminus('fmb_$i_1','fmb_$i_2') = 'fmb_$i_3' )
& ( c_HOL_Ouminus__class_Ouminus('fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_HOL_Ouminus__class_Ouminus('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Ouminus__class_Ouminus('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Ouminus__class_Ouminus('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_HOL_Ouminus__class_Ouminus('fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( c_HOL_Ouminus__class_Ouminus('fmb_$i_3','fmb_$i_2') = 'fmb_$i_1' )
& ( c_HOL_Ouminus__class_Ouminus('fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' ) ) ).
tff(declare_c_Divides_Odiv__class_Odiv,type,
c_Divides_Odiv__class_Odiv: ( $i * $i * $i ) > $i ).
tff(function_c_Divides_Odiv__class_Odiv,axiom,
( ( c_Divides_Odiv__class_Odiv('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_1','fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_1','fmb_$i_2','fmb_$i_3') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_1','fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_1','fmb_$i_3','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_1','fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_2','fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_2','fmb_$i_2','fmb_$i_3') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_2','fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_2','fmb_$i_3','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_2','fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_3','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_3','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_3','fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_3','fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_3','fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_3','fmb_$i_2','fmb_$i_3') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_3','fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_3','fmb_$i_3','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Divides_Odiv__class_Odiv('fmb_$i_3','fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' ) ) ).
tff(declare_c_RealVector_Oof__real,type,
c_RealVector_Oof__real: ( $i * $i ) > $i ).
tff(function_c_RealVector_Oof__real,axiom,
( ( c_RealVector_Oof__real('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_RealVector_Oof__real('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_RealVector_Oof__real('fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_RealVector_Oof__real('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_RealVector_Oof__real('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_RealVector_Oof__real('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_RealVector_Oof__real('fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_RealVector_Oof__real('fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_RealVector_Oof__real('fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_HOL_Oone__class_Oone,type,
c_HOL_Oone__class_Oone: $i > $i ).
tff(function_c_HOL_Oone__class_Oone,axiom,
( ( c_HOL_Oone__class_Oone('fmb_$i_1') = 'fmb_$i_3' )
& ( c_HOL_Oone__class_Oone('fmb_$i_2') = 'fmb_$i_3' )
& ( c_HOL_Oone__class_Oone('fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_RealVector_OscaleR__class_OscaleR,type,
c_RealVector_OscaleR__class_OscaleR: ( $i * $i * $i ) > $i ).
tff(function_c_RealVector_OscaleR__class_OscaleR,axiom,
( ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_3' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_1','fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_1','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_1','fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_1','fmb_$i_3','fmb_$i_2') = 'fmb_$i_1' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_1','fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_2','fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_2','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_2','fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_2','fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_2','fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_3','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_3','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_3','fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_3','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_3','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_3','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_3','fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_3','fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_RealVector_OscaleR__class_OscaleR('fmb_$i_3','fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_HOL_Oinverse__class_Odivide,type,
c_HOL_Oinverse__class_Odivide: ( $i * $i * $i ) > $i ).
tff(function_c_HOL_Oinverse__class_Odivide,axiom,
( ( c_HOL_Oinverse__class_Odivide('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_3' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_1','fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_1','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_1','fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_1','fmb_$i_3','fmb_$i_2') = 'fmb_$i_1' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_1','fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_2','fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_2','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_2','fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_2','fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_2','fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_3','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_3','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_3','fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_3','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_3','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_3','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_3','fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_3','fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_HOL_Oinverse__class_Odivide('fmb_$i_3','fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_HOL_Ozero__class_Ozero,type,
c_HOL_Ozero__class_Ozero: $i > $i ).
tff(function_c_HOL_Ozero__class_Ozero,axiom,
( ( c_HOL_Ozero__class_Ozero('fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Ozero__class_Ozero('fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Ozero__class_Ozero('fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_HOL_Oinverse__class_Oinverse,type,
c_HOL_Oinverse__class_Oinverse: ( $i * $i ) > $i ).
tff(function_c_HOL_Oinverse__class_Oinverse,axiom,
( ( c_HOL_Oinverse__class_Oinverse('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_HOL_Oinverse__class_Oinverse('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_HOL_Oinverse__class_Oinverse('fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_HOL_Oinverse__class_Oinverse('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Oinverse('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Oinverse('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_HOL_Oinverse__class_Oinverse('fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_HOL_Oinverse__class_Oinverse('fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_HOL_Oinverse__class_Oinverse('fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_Power_Opower__class_Opower,type,
c_Power_Opower__class_Opower: ( $i * $i * $i ) > $i ).
tff(function_c_Power_Opower__class_Opower,axiom,
( ( c_Power_Opower__class_Opower('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_1','fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_1','fmb_$i_2','fmb_$i_3') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_1','fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_1','fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_1','fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_2','fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_2','fmb_$i_2','fmb_$i_3') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_2','fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_2','fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_2','fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_3','fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_3','fmb_$i_1','fmb_$i_2') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_3','fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_3','fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_3','fmb_$i_2','fmb_$i_2') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_3','fmb_$i_2','fmb_$i_3') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_3','fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_3','fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_Power_Opower__class_Opower('fmb_$i_3','fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_Log_Opowr,type,
c_Log_Opowr: ( $i * $i ) > $i ).
tff(function_c_Log_Opowr,axiom,
( ( c_Log_Opowr('fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_Log_Opowr('fmb_$i_1','fmb_$i_2') = 'fmb_$i_3' )
& ( c_Log_Opowr('fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_Log_Opowr('fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_Log_Opowr('fmb_$i_2','fmb_$i_2') = 'fmb_$i_3' )
& ( c_Log_Opowr('fmb_$i_2','fmb_$i_3') = 'fmb_$i_3' )
& ( c_Log_Opowr('fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_Log_Opowr('fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_Log_Opowr('fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_HOL_Osgn__class_Osgn,type,
c_HOL_Osgn__class_Osgn: ( $i * $i ) > $i ).
tff(function_c_HOL_Osgn__class_Osgn,axiom,
( ( c_HOL_Osgn__class_Osgn('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_HOL_Osgn__class_Osgn('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_HOL_Osgn__class_Osgn('fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_HOL_Osgn__class_Osgn('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Osgn__class_Osgn('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Osgn__class_Osgn('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_HOL_Osgn__class_Osgn('fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_HOL_Osgn__class_Osgn('fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_HOL_Osgn__class_Osgn('fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_RealVector_Onorm__class_Onorm,type,
c_RealVector_Onorm__class_Onorm: ( $i * $i ) > $i ).
tff(function_c_RealVector_Onorm__class_Onorm,axiom,
( ( c_RealVector_Onorm__class_Onorm('fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_RealVector_Onorm__class_Onorm('fmb_$i_1','fmb_$i_2') = 'fmb_$i_3' )
& ( c_RealVector_Onorm__class_Onorm('fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_RealVector_Onorm__class_Onorm('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_RealVector_Onorm__class_Onorm('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_RealVector_Onorm__class_Onorm('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_RealVector_Onorm__class_Onorm('fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_RealVector_Onorm__class_Onorm('fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_RealVector_Onorm__class_Onorm('fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_NthRoot_Osqrt,type,
c_NthRoot_Osqrt: $i > $i ).
tff(function_c_NthRoot_Osqrt,axiom,
( ( c_NthRoot_Osqrt('fmb_$i_1') = 'fmb_$i_1' )
& ( c_NthRoot_Osqrt('fmb_$i_2') = 'fmb_$i_2' )
& ( c_NthRoot_Osqrt('fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_HOL_Oabs__class_Oabs,type,
c_HOL_Oabs__class_Oabs: ( $i * $i ) > $i ).
tff(function_c_HOL_Oabs__class_Oabs,axiom,
( ( c_HOL_Oabs__class_Oabs('fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_HOL_Oabs__class_Oabs('fmb_$i_1','fmb_$i_2') = 'fmb_$i_3' )
& ( c_HOL_Oabs__class_Oabs('fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_HOL_Oabs__class_Oabs('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_HOL_Oabs__class_Oabs('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_HOL_Oabs__class_Oabs('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_HOL_Oabs__class_Oabs('fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_HOL_Oabs__class_Oabs('fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_HOL_Oabs__class_Oabs('fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_Transcendental_Osin,type,
c_Transcendental_Osin: $i > $i ).
tff(function_c_Transcendental_Osin,axiom,
( ( c_Transcendental_Osin('fmb_$i_1') = 'fmb_$i_2' )
& ( c_Transcendental_Osin('fmb_$i_2') = 'fmb_$i_2' )
& ( c_Transcendental_Osin('fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_Fun_Oid,type,
c_Fun_Oid: ( $i * $i ) > $i ).
tff(function_c_Fun_Oid,axiom,
( ( c_Fun_Oid('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_Fun_Oid('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_Fun_Oid('fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_Fun_Oid('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_Fun_Oid('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_Fun_Oid('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_Fun_Oid('fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_Fun_Oid('fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_Fun_Oid('fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_Transcendental_Ocos,type,
c_Transcendental_Ocos: $i > $i ).
tff(function_c_Transcendental_Ocos,axiom,
( ( c_Transcendental_Ocos('fmb_$i_1') = 'fmb_$i_3' )
& ( c_Transcendental_Ocos('fmb_$i_2') = 'fmb_$i_3' )
& ( c_Transcendental_Ocos('fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_class_Ring__and__Field_Ocomm__semiring__1,type,
class_Ring__and__Field_Ocomm__semiring__1: $i > $o ).
tff(predicate_class_Ring__and__Field_Ocomm__semiring__1,axiom,
( class_Ring__and__Field_Ocomm__semiring__1('fmb_$i_1')
& class_Ring__and__Field_Ocomm__semiring__1('fmb_$i_2')
& class_Ring__and__Field_Ocomm__semiring__1('fmb_$i_3') ) ).
tff(declare_class_OrderedGroup_Oab__semigroup__mult,type,
class_OrderedGroup_Oab__semigroup__mult: $i > $o ).
tff(predicate_class_OrderedGroup_Oab__semigroup__mult,axiom,
( class_OrderedGroup_Oab__semigroup__mult('fmb_$i_1')
& class_OrderedGroup_Oab__semigroup__mult('fmb_$i_2')
& class_OrderedGroup_Oab__semigroup__mult('fmb_$i_3') ) ).
tff(declare_class_Divides_Oring__div,type,
class_Divides_Oring__div: $i > $o ).
tff(predicate_class_Divides_Oring__div,axiom,
( ~ class_Divides_Oring__div('fmb_$i_1')
& ~ class_Divides_Oring__div('fmb_$i_2')
& ~ class_Divides_Oring__div('fmb_$i_3') ) ).
tff(declare_c_Ring__and__Field_Odvd__class_Odvd,type,
c_Ring__and__Field_Odvd__class_Odvd: ( $i * $i * $i ) > $o ).
tff(predicate_c_Ring__and__Field_Odvd__class_Odvd,axiom,
( c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_1','fmb_$i_1','fmb_$i_3')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_1','fmb_$i_2','fmb_$i_3')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_1','fmb_$i_3','fmb_$i_1')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_1','fmb_$i_3','fmb_$i_2')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_1','fmb_$i_3','fmb_$i_3')
& ~ c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_2','fmb_$i_1','fmb_$i_3')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_2','fmb_$i_2','fmb_$i_2')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_2','fmb_$i_2','fmb_$i_3')
& ~ c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_2','fmb_$i_3','fmb_$i_1')
& ~ c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_2','fmb_$i_3','fmb_$i_2')
& ~ c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_2','fmb_$i_3','fmb_$i_3')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_3','fmb_$i_1','fmb_$i_1')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_3','fmb_$i_1','fmb_$i_2')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_3','fmb_$i_1','fmb_$i_3')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_3','fmb_$i_2','fmb_$i_1')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_3','fmb_$i_2','fmb_$i_2')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_3','fmb_$i_2','fmb_$i_3')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_3','fmb_$i_3','fmb_$i_1')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_3','fmb_$i_3','fmb_$i_2')
& c_Ring__and__Field_Odvd__class_Odvd('fmb_$i_3','fmb_$i_3','fmb_$i_3') ) ).
tff(declare_class_RealVector_Oreal__algebra__1,type,
class_RealVector_Oreal__algebra__1: $i > $o ).
tff(predicate_class_RealVector_Oreal__algebra__1,axiom,
( class_RealVector_Oreal__algebra__1('fmb_$i_1')
& class_RealVector_Oreal__algebra__1('fmb_$i_2')
& class_RealVector_Oreal__algebra__1('fmb_$i_3') ) ).
tff(declare_class_Int_Onumber__ring,type,
class_Int_Onumber__ring: $i > $o ).
tff(predicate_class_Int_Onumber__ring,axiom,
( class_Int_Onumber__ring('fmb_$i_1')
& class_Int_Onumber__ring('fmb_$i_2')
& class_Int_Onumber__ring('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Ofield,type,
class_Ring__and__Field_Ofield: $i > $o ).
tff(predicate_class_Ring__and__Field_Ofield,axiom,
( class_Ring__and__Field_Ofield('fmb_$i_1')
& class_Ring__and__Field_Ofield('fmb_$i_2')
& class_Ring__and__Field_Ofield('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Opordered__cancel__semiring,type,
class_Ring__and__Field_Opordered__cancel__semiring: $i > $o ).
tff(predicate_class_Ring__and__Field_Opordered__cancel__semiring,axiom,
( class_Ring__and__Field_Opordered__cancel__semiring('fmb_$i_1')
& class_Ring__and__Field_Opordered__cancel__semiring('fmb_$i_2')
& class_Ring__and__Field_Opordered__cancel__semiring('fmb_$i_3') ) ).
tff(declare_c_lessequals,type,
c_lessequals: ( $i * $i * $i ) > $o ).
tff(predicate_c_lessequals,axiom,
( c_lessequals('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& c_lessequals('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& c_lessequals('fmb_$i_1','fmb_$i_1','fmb_$i_3')
& c_lessequals('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& c_lessequals('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& c_lessequals('fmb_$i_1','fmb_$i_2','fmb_$i_3')
& c_lessequals('fmb_$i_1','fmb_$i_3','fmb_$i_1')
& c_lessequals('fmb_$i_1','fmb_$i_3','fmb_$i_2')
& c_lessequals('fmb_$i_1','fmb_$i_3','fmb_$i_3')
& ~ c_lessequals('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ c_lessequals('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ c_lessequals('fmb_$i_2','fmb_$i_1','fmb_$i_3')
& c_lessequals('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& c_lessequals('fmb_$i_2','fmb_$i_2','fmb_$i_2')
& c_lessequals('fmb_$i_2','fmb_$i_2','fmb_$i_3')
& c_lessequals('fmb_$i_2','fmb_$i_3','fmb_$i_1')
& c_lessequals('fmb_$i_2','fmb_$i_3','fmb_$i_2')
& c_lessequals('fmb_$i_2','fmb_$i_3','fmb_$i_3')
& ~ c_lessequals('fmb_$i_3','fmb_$i_1','fmb_$i_1')
& ~ c_lessequals('fmb_$i_3','fmb_$i_1','fmb_$i_2')
& ~ c_lessequals('fmb_$i_3','fmb_$i_1','fmb_$i_3')
& ~ c_lessequals('fmb_$i_3','fmb_$i_2','fmb_$i_1')
& ~ c_lessequals('fmb_$i_3','fmb_$i_2','fmb_$i_2')
& ~ c_lessequals('fmb_$i_3','fmb_$i_2','fmb_$i_3')
& c_lessequals('fmb_$i_3','fmb_$i_3','fmb_$i_1')
& c_lessequals('fmb_$i_3','fmb_$i_3','fmb_$i_2')
& c_lessequals('fmb_$i_3','fmb_$i_3','fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Oordered__ring__strict,type,
class_Ring__and__Field_Oordered__ring__strict: $i > $o ).
tff(predicate_class_Ring__and__Field_Oordered__ring__strict,axiom,
( class_Ring__and__Field_Oordered__ring__strict('fmb_$i_1')
& class_Ring__and__Field_Oordered__ring__strict('fmb_$i_2')
& class_Ring__and__Field_Oordered__ring__strict('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Opordered__ring,type,
class_Ring__and__Field_Opordered__ring: $i > $o ).
tff(predicate_class_Ring__and__Field_Opordered__ring,axiom,
( class_Ring__and__Field_Opordered__ring('fmb_$i_1')
& class_Ring__and__Field_Opordered__ring('fmb_$i_2')
& class_Ring__and__Field_Opordered__ring('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Odivision__ring,type,
class_Ring__and__Field_Odivision__ring: $i > $o ).
tff(predicate_class_Ring__and__Field_Odivision__ring,axiom,
( class_Ring__and__Field_Odivision__ring('fmb_$i_1')
& class_Ring__and__Field_Odivision__ring('fmb_$i_2')
& class_Ring__and__Field_Odivision__ring('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Odivision__by__zero,type,
class_Ring__and__Field_Odivision__by__zero: $i > $o ).
tff(predicate_class_Ring__and__Field_Odivision__by__zero,axiom,
( class_Ring__and__Field_Odivision__by__zero('fmb_$i_1')
& class_Ring__and__Field_Odivision__by__zero('fmb_$i_2')
& class_Ring__and__Field_Odivision__by__zero('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Oordered__field,type,
class_Ring__and__Field_Oordered__field: $i > $o ).
tff(predicate_class_Ring__and__Field_Oordered__field,axiom,
( class_Ring__and__Field_Oordered__field('fmb_$i_1')
& class_Ring__and__Field_Oordered__field('fmb_$i_2')
& class_Ring__and__Field_Oordered__field('fmb_$i_3') ) ).
tff(declare_class_OrderedGroup_Ocomm__monoid__mult,type,
class_OrderedGroup_Ocomm__monoid__mult: $i > $o ).
tff(predicate_class_OrderedGroup_Ocomm__monoid__mult,axiom,
( class_OrderedGroup_Ocomm__monoid__mult('fmb_$i_1')
& class_OrderedGroup_Ocomm__monoid__mult('fmb_$i_2')
& class_OrderedGroup_Ocomm__monoid__mult('fmb_$i_3') ) ).
tff(declare_class_OrderedGroup_Oab__semigroup__idem__mult,type,
class_OrderedGroup_Oab__semigroup__idem__mult: $i > $o ).
tff(predicate_class_OrderedGroup_Oab__semigroup__idem__mult,axiom,
( ~ class_OrderedGroup_Oab__semigroup__idem__mult('fmb_$i_1')
& ~ class_OrderedGroup_Oab__semigroup__idem__mult('fmb_$i_2')
& ~ class_OrderedGroup_Oab__semigroup__idem__mult('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Omult__mono,type,
class_Ring__and__Field_Omult__mono: $i > $o ).
tff(predicate_class_Ring__and__Field_Omult__mono,axiom,
( class_Ring__and__Field_Omult__mono('fmb_$i_1')
& class_Ring__and__Field_Omult__mono('fmb_$i_2')
& class_Ring__and__Field_Omult__mono('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Omult__mono1,type,
class_Ring__and__Field_Omult__mono1: $i > $o ).
tff(predicate_class_Ring__and__Field_Omult__mono1,axiom,
( class_Ring__and__Field_Omult__mono1('fmb_$i_1')
& class_Ring__and__Field_Omult__mono1('fmb_$i_2')
& class_Ring__and__Field_Omult__mono1('fmb_$i_3') ) ).
tff(declare_class_RealVector_Oreal__normed__vector,type,
class_RealVector_Oreal__normed__vector: $i > $o ).
tff(predicate_class_RealVector_Oreal__normed__vector,axiom,
( class_RealVector_Oreal__normed__vector('fmb_$i_1')
& class_RealVector_Oreal__normed__vector('fmb_$i_2')
& class_RealVector_Oreal__normed__vector('fmb_$i_3') ) ).
tff(declare_class_OrderedGroup_Opordered__ab__group__add__abs,type,
class_OrderedGroup_Opordered__ab__group__add__abs: $i > $o ).
tff(predicate_class_OrderedGroup_Opordered__ab__group__add__abs,axiom,
( class_OrderedGroup_Opordered__ab__group__add__abs('fmb_$i_1')
& class_OrderedGroup_Opordered__ab__group__add__abs('fmb_$i_2')
& class_OrderedGroup_Opordered__ab__group__add__abs('fmb_$i_3') ) ).
tff(declare_class_Divides_Osemiring__div,type,
class_Divides_Osemiring__div: $i > $o ).
tff(predicate_class_Divides_Osemiring__div,axiom,
( ~ class_Divides_Osemiring__div('fmb_$i_1')
& ~ class_Divides_Osemiring__div('fmb_$i_2')
& ~ class_Divides_Osemiring__div('fmb_$i_3') ) ).
tff(declare_class_OrderedGroup_Opordered__ab__group__add,type,
class_OrderedGroup_Opordered__ab__group__add: $i > $o ).
tff(predicate_class_OrderedGroup_Opordered__ab__group__add,axiom,
( class_OrderedGroup_Opordered__ab__group__add('fmb_$i_1')
& class_OrderedGroup_Opordered__ab__group__add('fmb_$i_2')
& class_OrderedGroup_Opordered__ab__group__add('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Oring__1__no__zero__divisors,type,
class_Ring__and__Field_Oring__1__no__zero__divisors: $i > $o ).
tff(predicate_class_Ring__and__Field_Oring__1__no__zero__divisors,axiom,
( class_Ring__and__Field_Oring__1__no__zero__divisors('fmb_$i_1')
& class_Ring__and__Field_Oring__1__no__zero__divisors('fmb_$i_2')
& class_Ring__and__Field_Oring__1__no__zero__divisors('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Ozero__neq__one,type,
class_Ring__and__Field_Ozero__neq__one: $i > $o ).
tff(predicate_class_Ring__and__Field_Ozero__neq__one,axiom,
( class_Ring__and__Field_Ozero__neq__one('fmb_$i_1')
& class_Ring__and__Field_Ozero__neq__one('fmb_$i_2')
& class_Ring__and__Field_Ozero__neq__one('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Ono__zero__divisors,type,
class_Ring__and__Field_Ono__zero__divisors: $i > $o ).
tff(predicate_class_Ring__and__Field_Ono__zero__divisors,axiom,
( class_Ring__and__Field_Ono__zero__divisors('fmb_$i_1')
& class_Ring__and__Field_Ono__zero__divisors('fmb_$i_2')
& class_Ring__and__Field_Ono__zero__divisors('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Omult__zero,type,
class_Ring__and__Field_Omult__zero: $i > $o ).
tff(predicate_class_Ring__and__Field_Omult__zero,axiom,
( class_Ring__and__Field_Omult__zero('fmb_$i_1')
& class_Ring__and__Field_Omult__zero('fmb_$i_2')
& class_Ring__and__Field_Omult__zero('fmb_$i_3') ) ).
tff(declare_class_Power_Opower,type,
class_Power_Opower: $i > $o ).
tff(predicate_class_Power_Opower,axiom,
( class_Power_Opower('fmb_$i_1')
& class_Power_Opower('fmb_$i_2')
& class_Power_Opower('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Oring,type,
class_Ring__and__Field_Oring: $i > $o ).
tff(predicate_class_Ring__and__Field_Oring,axiom,
( class_Ring__and__Field_Oring('fmb_$i_1')
& class_Ring__and__Field_Oring('fmb_$i_2')
& class_Ring__and__Field_Oring('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Opordered__ring__abs,type,
class_Ring__and__Field_Opordered__ring__abs: $i > $o ).
tff(predicate_class_Ring__and__Field_Opordered__ring__abs,axiom,
( class_Ring__and__Field_Opordered__ring__abs('fmb_$i_1')
& class_Ring__and__Field_Opordered__ring__abs('fmb_$i_2')
& class_Ring__and__Field_Opordered__ring__abs('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Oordered__idom,type,
class_Ring__and__Field_Oordered__idom: $i > $o ).
tff(predicate_class_Ring__and__Field_Oordered__idom,axiom,
( class_Ring__and__Field_Oordered__idom('fmb_$i_1')
& class_Ring__and__Field_Oordered__idom('fmb_$i_2')
& class_Ring__and__Field_Oordered__idom('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Oidom,type,
class_Ring__and__Field_Oidom: $i > $o ).
tff(predicate_class_Ring__and__Field_Oidom,axiom,
( class_Ring__and__Field_Oidom('fmb_$i_1')
& class_Ring__and__Field_Oidom('fmb_$i_2')
& class_Ring__and__Field_Oidom('fmb_$i_3') ) ).
tff(declare_class_Orderings_Oorder,type,
class_Orderings_Oorder: $i > $o ).
tff(predicate_class_Orderings_Oorder,axiom,
( class_Orderings_Oorder('fmb_$i_1')
& class_Orderings_Oorder('fmb_$i_2')
& class_Orderings_Oorder('fmb_$i_3') ) ).
tff(declare_class_Lattices_Oboolean__algebra,type,
class_Lattices_Oboolean__algebra: $i > $o ).
tff(predicate_class_Lattices_Oboolean__algebra,axiom,
( ~ class_Lattices_Oboolean__algebra('fmb_$i_1')
& ~ class_Lattices_Oboolean__algebra('fmb_$i_2')
& ~ class_Lattices_Oboolean__algebra('fmb_$i_3') ) ).
tff(declare_class_OrderedGroup_Ogroup__add,type,
class_OrderedGroup_Ogroup__add: $i > $o ).
tff(predicate_class_OrderedGroup_Ogroup__add,axiom,
( class_OrderedGroup_Ogroup__add('fmb_$i_1')
& class_OrderedGroup_Ogroup__add('fmb_$i_2')
& class_OrderedGroup_Ogroup__add('fmb_$i_3') ) ).
tff(declare_class_OrderedGroup_Oordered__ab__group__add,type,
class_OrderedGroup_Oordered__ab__group__add: $i > $o ).
tff(predicate_class_OrderedGroup_Oordered__ab__group__add,axiom,
( class_OrderedGroup_Oordered__ab__group__add('fmb_$i_1')
& class_OrderedGroup_Oordered__ab__group__add('fmb_$i_2')
& class_OrderedGroup_Oordered__ab__group__add('fmb_$i_3') ) ).
tff(declare_class_RealVector_Oreal__normed__algebra,type,
class_RealVector_Oreal__normed__algebra: $i > $o ).
tff(predicate_class_RealVector_Oreal__normed__algebra,axiom,
( class_RealVector_Oreal__normed__algebra('fmb_$i_1')
& class_RealVector_Oreal__normed__algebra('fmb_$i_2')
& class_RealVector_Oreal__normed__algebra('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Opordered__semiring,type,
class_Ring__and__Field_Opordered__semiring: $i > $o ).
tff(predicate_class_Ring__and__Field_Opordered__semiring,axiom,
( class_Ring__and__Field_Opordered__semiring('fmb_$i_1')
& class_Ring__and__Field_Opordered__semiring('fmb_$i_2')
& class_Ring__and__Field_Opordered__semiring('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Ocomm__ring__1,type,
class_Ring__and__Field_Ocomm__ring__1: $i > $o ).
tff(predicate_class_Ring__and__Field_Ocomm__ring__1,axiom,
( class_Ring__and__Field_Ocomm__ring__1('fmb_$i_1')
& class_Ring__and__Field_Ocomm__ring__1('fmb_$i_2')
& class_Ring__and__Field_Ocomm__ring__1('fmb_$i_3') ) ).
tff(declare_class_RealVector_Oreal__vector,type,
class_RealVector_Oreal__vector: $i > $o ).
tff(predicate_class_RealVector_Oreal__vector,axiom,
( class_RealVector_Oreal__vector('fmb_$i_1')
& class_RealVector_Oreal__vector('fmb_$i_2')
& class_RealVector_Oreal__vector('fmb_$i_3') ) ).
tff(declare_class_RealVector_Oreal__algebra,type,
class_RealVector_Oreal__algebra: $i > $o ).
tff(predicate_class_RealVector_Oreal__algebra,axiom,
( class_RealVector_Oreal__algebra('fmb_$i_1')
& class_RealVector_Oreal__algebra('fmb_$i_2')
& class_RealVector_Oreal__algebra('fmb_$i_3') ) ).
tff(declare_class_RealVector_Oreal__normed__field,type,
class_RealVector_Oreal__normed__field: $i > $o ).
tff(predicate_class_RealVector_Oreal__normed__field,axiom,
( class_RealVector_Oreal__normed__field('fmb_$i_1')
& class_RealVector_Oreal__normed__field('fmb_$i_2')
& class_RealVector_Oreal__normed__field('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Oordered__semidom,type,
class_Ring__and__Field_Oordered__semidom: $i > $o ).
tff(predicate_class_Ring__and__Field_Oordered__semidom,axiom,
( class_Ring__and__Field_Oordered__semidom('fmb_$i_1')
& class_Ring__and__Field_Oordered__semidom('fmb_$i_2')
& class_Ring__and__Field_Oordered__semidom('fmb_$i_3') ) ).
tff(declare_class_OrderedGroup_Olordered__ab__group__add,type,
class_OrderedGroup_Olordered__ab__group__add: $i > $o ).
tff(predicate_class_OrderedGroup_Olordered__ab__group__add,axiom,
( class_OrderedGroup_Olordered__ab__group__add('fmb_$i_1')
& class_OrderedGroup_Olordered__ab__group__add('fmb_$i_2')
& class_OrderedGroup_Olordered__ab__group__add('fmb_$i_3') ) ).
tff(declare_class_RealVector_Oreal__normed__algebra__1,type,
class_RealVector_Oreal__normed__algebra__1: $i > $o ).
tff(predicate_class_RealVector_Oreal__normed__algebra__1,axiom,
( class_RealVector_Oreal__normed__algebra__1('fmb_$i_1')
& class_RealVector_Oreal__normed__algebra__1('fmb_$i_2')
& class_RealVector_Oreal__normed__algebra__1('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Oring__no__zero__divisors,type,
class_Ring__and__Field_Oring__no__zero__divisors: $i > $o ).
tff(predicate_class_Ring__and__Field_Oring__no__zero__divisors,axiom,
( class_Ring__and__Field_Oring__no__zero__divisors('fmb_$i_1')
& class_Ring__and__Field_Oring__no__zero__divisors('fmb_$i_2')
& class_Ring__and__Field_Oring__no__zero__divisors('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Olordered__ring,type,
class_Ring__and__Field_Olordered__ring: $i > $o ).
tff(predicate_class_Ring__and__Field_Olordered__ring,axiom,
( class_Ring__and__Field_Olordered__ring('fmb_$i_1')
& class_Ring__and__Field_Olordered__ring('fmb_$i_2')
& class_Ring__and__Field_Olordered__ring('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Odvd,type,
class_Ring__and__Field_Odvd: $i > $o ).
tff(predicate_class_Ring__and__Field_Odvd,axiom,
( class_Ring__and__Field_Odvd('fmb_$i_1')
& class_Ring__and__Field_Odvd('fmb_$i_2')
& class_Ring__and__Field_Odvd('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Oring__1,type,
class_Ring__and__Field_Oring__1: $i > $o ).
tff(predicate_class_Ring__and__Field_Oring__1,axiom,
( class_Ring__and__Field_Oring__1('fmb_$i_1')
& class_Ring__and__Field_Oring__1('fmb_$i_2')
& class_Ring__and__Field_Oring__1('fmb_$i_3') ) ).
tff(declare_class_RealVector_Oreal__normed__div__algebra,type,
class_RealVector_Oreal__normed__div__algebra: $i > $o ).
tff(predicate_class_RealVector_Oreal__normed__div__algebra,axiom,
( class_RealVector_Oreal__normed__div__algebra('fmb_$i_1')
& class_RealVector_Oreal__normed__div__algebra('fmb_$i_2')
& class_RealVector_Oreal__normed__div__algebra('fmb_$i_3') ) ).
tff(declare_class_OrderedGroup_Omonoid__mult,type,
class_OrderedGroup_Omonoid__mult: $i > $o ).
tff(predicate_class_OrderedGroup_Omonoid__mult,axiom,
( class_OrderedGroup_Omonoid__mult('fmb_$i_1')
& class_OrderedGroup_Omonoid__mult('fmb_$i_2')
& class_OrderedGroup_Omonoid__mult('fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Osemiring__1,type,
class_Ring__and__Field_Osemiring__1: $i > $o ).
tff(predicate_class_Ring__and__Field_Osemiring__1,axiom,
( class_Ring__and__Field_Osemiring__1('fmb_$i_1')
& class_Ring__and__Field_Osemiring__1('fmb_$i_2')
& class_Ring__and__Field_Osemiring__1('fmb_$i_3') ) ).
tff(declare_c_Int_Oiszero,type,
c_Int_Oiszero: ( $i * $i ) > $o ).
tff(predicate_c_Int_Oiszero,axiom,
( ~ c_Int_Oiszero('fmb_$i_1','fmb_$i_1')
& ~ c_Int_Oiszero('fmb_$i_1','fmb_$i_2')
& ~ c_Int_Oiszero('fmb_$i_1','fmb_$i_3')
& c_Int_Oiszero('fmb_$i_2','fmb_$i_1')
& c_Int_Oiszero('fmb_$i_2','fmb_$i_2')
& c_Int_Oiszero('fmb_$i_2','fmb_$i_3')
& ~ c_Int_Oiszero('fmb_$i_3','fmb_$i_1')
& ~ c_Int_Oiszero('fmb_$i_3','fmb_$i_2')
& ~ c_Int_Oiszero('fmb_$i_3','fmb_$i_3') ) ).
tff(declare_class_Ring__and__Field_Osgn__if,type,
class_Ring__and__Field_Osgn__if: $i > $o ).
tff(predicate_class_Ring__and__Field_Osgn__if,axiom,
( class_Ring__and__Field_Osgn__if('fmb_$i_1')
& class_Ring__and__Field_Osgn__if('fmb_$i_2')
& class_Ring__and__Field_Osgn__if('fmb_$i_3') ) ).
tff(declare_class_Orderings_Opreorder,type,
class_Orderings_Opreorder: $i > $o ).
tff(predicate_class_Orderings_Opreorder,axiom,
( class_Orderings_Opreorder('fmb_$i_1')
& class_Orderings_Opreorder('fmb_$i_2')
& class_Orderings_Opreorder('fmb_$i_3') ) ).
tff(declare_class_Orderings_Olinorder,type,
class_Orderings_Olinorder: $i > $o ).
tff(predicate_class_Orderings_Olinorder,axiom,
( class_Orderings_Olinorder('fmb_$i_1')
& class_Orderings_Olinorder('fmb_$i_2')
& class_Orderings_Olinorder('fmb_$i_3') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV595-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 % Computer : n020.cluster.edu
% 0.09/0.23 % Model : x86_64 x86_64
% 0.09/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.23 % Memory : 8046.5625MB
% 0.09/0.23 % OS : Linux 6.8.0-71-generic
% 0.09/0.23 % CPULimit : 300
% 0.09/0.23 % WCLimit : 300
% 0.09/0.23 % DateTime : Mon Sep 28 12:00:34 UTC 2026
% 0.09/0.23 % CPUTime :
% 0.09/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.24/0.29 Running first-order model finding
% 0.24/0.29 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
% 2.02/0.62 % (119220)Will run a generic schedule for satisfiability detection.
% 2.02/0.62 % (119227)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3302994410:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.02/0.62 % (119225)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=435484191_2999 on theBenchmark for (2999ds/0Mi)
% 2.02/0.62 % (119226)% WARNING: option uhcvi not known.
% 2.02/0.62 % (119229)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1092546737:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.02/0.62 % (119231)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2752647386:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.02/0.62 % (119228)dis+10_1_sil=32000:sp=arity:random_seed=2622814339:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.02/0.62 % (119230)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4246135199:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.02/0.62 % (119226)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1857950812:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.02/0.62 % TRYING [1]
% 2.02/0.62 % TRYING [2]
% 2.02/0.62 % TRYING [3]
% 2.02/0.62 % (119228)Instruction limit reached!
% 2.02/0.62 % (119228)------------------------------
% 2.02/0.62 % (119228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.02/0.62 % (119228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.02/0.62 % (119228)CaDiCaL version: 2.1.3
% 2.02/0.62 % (119228)Termination reason: Instruction limit
% 2.02/0.62 % (119228)Termination phase: Saturation
% 2.02/0.62 % (119228)Time elapsed: 0.112 s
% 2.02/0.62 % (119228)Peak memory usage: 12 MB
% 2.02/0.62 % (119228)Instructions burned: 103 (million)
% 2.02/0.62 % (119229)Instruction limit reached!
% 2.02/0.62 % (119229)------------------------------
% 2.02/0.62 % (119229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.02/0.62 % (119229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.02/0.62 % (119229)CaDiCaL version: 2.1.3
% 2.02/0.62 % (119229)Termination reason: Instruction limit
% 2.02/0.62 % (119229)Termination phase: Saturation
% 2.02/0.62 % (119229)Time elapsed: 0.133 s
% 2.02/0.62 % (119229)Peak memory usage: 13 MB
% 2.02/0.62 % (119229)Instructions burned: 118 (million)
% 2.02/0.62 % (119230)Instruction limit reached!
% 2.02/0.62 % (119230)------------------------------
% 2.02/0.62 % (119230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.02/0.62 % (119230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.02/0.62 % (119230)CaDiCaL version: 2.1.3
% 2.02/0.62 % (119230)Termination reason: Instruction limit
% 2.02/0.62 % (119230)Termination phase: Saturation
% 2.02/0.62 % (119230)Time elapsed: 0.143 s
% 2.02/0.62 % (119230)Peak memory usage: 13 MB
% 2.02/0.62 % (119230)Instructions burned: 132 (million)
% 2.02/0.62 % (119239)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1552355889:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 2.02/0.62 % (119231)Instruction limit reached!
% 2.02/0.62 % (119231)------------------------------
% 2.02/0.62 % (119231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.02/0.62 % (119231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.02/0.62 % (119231)CaDiCaL version: 2.1.3
% 2.02/0.62 % (119231)Termination reason: Instruction limit
% 2.02/0.62 % (119231)Termination phase: Saturation
% 2.02/0.62 % (119231)Time elapsed: 0.161 s
% 2.02/0.62 % (119231)Peak memory usage: 13 MB
% 2.02/0.62 % (119231)Instructions burned: 159 (million)
% 2.02/0.62 % (119240)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=636710215:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 2.02/0.62 % (119241)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1574284565:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 2.02/0.62 % (119243)ott-21_1_sil=16000:fs=off:random_seed=1963116940:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 2.02/0.62 % TRYING [1]
% 2.02/0.62 % TRYING [2]
% 2.02/0.62 % Finite Model Found!
% 2.02/0.62 % SZS status Satisfiable for theBenchmark
% 2.02/0.62 % (119225) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-119220-119225"...
% 2.02/0.62 % (119225)...printing done.
% 2.02/0.62 % SZS output start FiniteModel for theBenchmark
% See solution above
% 2.02/0.63 % (119225)------------------------------
% 2.02/0.63 % (119225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.02/0.63 % (119225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.02/0.63 % (119225)CaDiCaL version: 2.1.3
% 2.02/0.63 % (119225)Termination reason: Satisfiable
% 2.02/0.63 % (119225)Time elapsed: 0.258 s
% 2.02/0.63 % (119225)Peak memory usage: 27 MB
% 2.02/0.63 % (119225)Instructions burned: 324 (million)
% 2.02/0.63 % (119220)Success in time 0.323 s
% 2.02/0.63 % Vampire exiting
%------------------------------------------------------------------------------