%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW935+1 : 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 : n005.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:45:12 PM UTC 2026
% Result : CounterSatisfiable 31.94s 10.41s
% Output : FiniteModel 31.94s
% 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_cbool__00,type,
cbool__00: $i ).
tff(cbool__00_definition,axiom,
cbool__00 = 'fmb_$i_1' ).
tff(declare_cT__00,type,
cT__00: $i ).
tff(cT__00_definition,axiom,
cT__00 = 'fmb_$i_1' ).
tff(declare_cF__00,type,
cF__00: $i ).
tff(cF__00_definition,axiom,
cF__00 = 'fmb_$i_2' ).
tff(declare_c_27const_2erelation_2eEMPTY__REL_27__00,type,
c_27const_2erelation_2eEMPTY__REL_27__00: $i ).
tff(c_27const_2erelation_2eEMPTY__REL_27__00_definition,axiom,
c_27const_2erelation_2eEMPTY__REL_27__00 = 'fmb_$i_2' ).
tff(declare_c_27const_2eoption_2eNONE_27__00,type,
c_27const_2eoption_2eNONE_27__00: $i ).
tff(c_27const_2eoption_2eNONE_27__00_definition,axiom,
c_27const_2eoption_2eNONE_27__00 = 'fmb_$i_3' ).
tff(declare_c_27const_2elist_2eNIL_27__00,type,
c_27const_2elist_2eNIL_27__00: $i ).
tff(c_27const_2elist_2eNIL_27__00_definition,axiom,
c_27const_2elist_2eNIL_27__00 = 'fmb_$i_3' ).
tff(declare_c_27type_2enum_2enum_27__00,type,
c_27type_2enum_2enum_27__00: $i ).
tff(c_27type_2enum_2enum_27__00_definition,axiom,
c_27type_2enum_2enum_27__00 = 'fmb_$i_2' ).
tff(declare_c_27const_2earithmetic_2eZERO_27__00,type,
c_27const_2earithmetic_2eZERO_27__00: $i ).
tff(c_27const_2earithmetic_2eZERO_27__00_definition,axiom,
c_27const_2earithmetic_2eZERO_27__00 = 'fmb_$i_2' ).
tff(declare_c_27const_2ebool_2eARB_27__00,type,
c_27const_2ebool_2eARB_27__00: $i ).
tff(c_27const_2ebool_2eARB_27__00_definition,axiom,
c_27const_2ebool_2eARB_27__00 = 'fmb_$i_2' ).
tff(declare_c_27const_2edata__to__word__gcProof_2emk__loc_27__00,type,
c_27const_2edata__to__word__gcProof_2emk__loc_27__00: $i ).
tff(c_27const_2edata__to__word__gcProof_2emk__loc_27__00_definition,axiom,
c_27const_2edata__to__word__gcProof_2emk__loc_27__00 = 'fmb_$i_1' ).
tff(declare_s__02,type,
s__02: ( $i * $i ) > $i ).
tff(function_s__02,axiom,
( ( s__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( s__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( s__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( s__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( s__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( s__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( s__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( s__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( s__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' ) ) ).
tff(declare_cfun__02,type,
cfun__02: ( $i * $i ) > $i ).
tff(function_cfun__02,axiom,
( ( cfun__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( cfun__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( cfun__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( cfun__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( cfun__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( cfun__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( cfun__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( cfun__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( cfun__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' ) ) ).
tff(declare_chapp__02,type,
chapp__02: ( $i * $i ) > $i ).
tff(function_chapp__02,axiom,
( ( chapp__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( chapp__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_3' )
& ( chapp__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( chapp__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( chapp__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( chapp__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( chapp__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( chapp__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( chapp__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' ) ) ).
tff(declare_c_27const_2emin_2e_40_27__01,type,
c_27const_2emin_2e_40_27__01: $i > $i ).
tff(function_c_27const_2emin_2e_40_27__01,axiom,
( ( c_27const_2emin_2e_40_27__01('fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2emin_2e_40_27__01('fmb_$i_2') = 'fmb_$i_3' )
& ( c_27const_2emin_2e_40_27__01('fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_27const_2ebool_2eCOND_27__03,type,
c_27const_2ebool_2eCOND_27__03: ( $i * $i * $i ) > $i ).
tff(function_c_27const_2ebool_2eCOND_27__03,axiom,
( ( c_27const_2ebool_2eCOND_27__03('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_3' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_1','fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_1','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_1','fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_1','fmb_$i_3','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_1','fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_2','fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_2','fmb_$i_2','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_2','fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_2','fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_2','fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_3','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_3','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_3','fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_3','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_3','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_3','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_3','fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_3','fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eCOND_27__03('fmb_$i_3','fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ecombin_2eI_27__01,type,
c_27const_2ecombin_2eI_27__01: $i > $i ).
tff(function_c_27const_2ecombin_2eI_27__01,axiom,
( ( c_27const_2ecombin_2eI_27__01('fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2ecombin_2eI_27__01('fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ecombin_2eI_27__01('fmb_$i_3') = 'fmb_$i_1' ) ) ).
tff(declare_c_27const_2erelation_2eWF_27__01,type,
c_27const_2erelation_2eWF_27__01: $i > $i ).
tff(function_c_27const_2erelation_2eWF_27__01,axiom,
( ( c_27const_2erelation_2eWF_27__01('fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eWF_27__01('fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2erelation_2eWF_27__01('fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2erelation_2eWFREC_27__02,type,
c_27const_2erelation_2eWFREC_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2erelation_2eWFREC_27__02,axiom,
( ( c_27const_2erelation_2eWFREC_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eWFREC_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eWFREC_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eWFREC_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2erelation_2eWFREC_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eWFREC_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eWFREC_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eWFREC_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eWFREC_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2erelation_2eRESTRICT_27__03,type,
c_27const_2erelation_2eRESTRICT_27__03: ( $i * $i * $i ) > $i ).
tff(function_c_27const_2erelation_2eRESTRICT_27__03,axiom,
( ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_1','fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_1','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_1','fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_1','fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_1','fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_2','fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_3' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_2','fmb_$i_2','fmb_$i_3') = 'fmb_$i_3' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_2','fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_2','fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_2','fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_3','fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_3','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_3','fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_3','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_3','fmb_$i_2','fmb_$i_2') = 'fmb_$i_3' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_3','fmb_$i_2','fmb_$i_3') = 'fmb_$i_3' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_3','fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_3','fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2erelation_2eRESTRICT_27__03('fmb_$i_3','fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27type_2epair_2eprod_27__02,type,
c_27type_2epair_2eprod_27__02: ( $i * $i ) > $i ).
tff(function_c_27type_2epair_2eprod_27__02,axiom,
( ( c_27type_2epair_2eprod_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27type_2epair_2eprod_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27type_2epair_2eprod_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27type_2epair_2eprod_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27type_2epair_2eprod_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27type_2epair_2eprod_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27type_2epair_2eprod_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27type_2epair_2eprod_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_27type_2epair_2eprod_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_27const_2epair_2e_2c_27__02,type,
c_27const_2epair_2e_2c_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2epair_2e_2c_27__02,axiom,
( ( c_27const_2epair_2e_2c_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2epair_2e_2c_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2epair_2e_2c_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2epair_2e_2c_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2epair_2e_2c_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2epair_2e_2c_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27const_2epair_2e_2c_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2epair_2e_2c_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_27const_2epair_2e_2c_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_27const_2epair_2epair__CASE_27__02,type,
c_27const_2epair_2epair__CASE_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2epair_2epair__CASE_27__02,axiom,
( ( c_27const_2epair_2epair__CASE_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2epair_2epair__CASE_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2epair_2epair__CASE_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_27const_2epair_2epair__CASE_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2epair_2epair__CASE_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2epair_2epair__CASE_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_3' )
& ( c_27const_2epair_2epair__CASE_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2epair_2epair__CASE_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2epair_2epair__CASE_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27type_2eoption_2eoption_27__01,type,
c_27type_2eoption_2eoption_27__01: $i > $i ).
tff(function_c_27type_2eoption_2eoption_27__01,axiom,
( ( c_27type_2eoption_2eoption_27__01('fmb_$i_1') = 'fmb_$i_3' )
& ( c_27type_2eoption_2eoption_27__01('fmb_$i_2') = 'fmb_$i_1' )
& ( c_27type_2eoption_2eoption_27__01('fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_27const_2eoption_2eSOME_27__01,type,
c_27const_2eoption_2eSOME_27__01: $i > $i ).
tff(function_c_27const_2eoption_2eSOME_27__01,axiom,
( ( c_27const_2eoption_2eSOME_27__01('fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2eoption_2eSOME_27__01('fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2eoption_2eSOME_27__01('fmb_$i_3') = 'fmb_$i_1' ) ) ).
tff(declare_c_27const_2eoption_2eoption__CASE_27__03,type,
c_27const_2eoption_2eoption__CASE_27__03: ( $i * $i * $i ) > $i ).
tff(function_c_27const_2eoption_2eoption__CASE_27__03,axiom,
( ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_3' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_1','fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_1','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_1','fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_1','fmb_$i_3','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_1','fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_2','fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_2','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_2','fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_2','fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_2','fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_3','fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_3','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_3','fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_3','fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_3','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_3','fmb_$i_2','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_3','fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_3','fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2eoption_2eoption__CASE_27__03('fmb_$i_3','fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_27type_2elist_2elist_27__01,type,
c_27type_2elist_2elist_27__01: $i > $i ).
tff(function_c_27type_2elist_2elist_27__01,axiom,
( ( c_27type_2elist_2elist_27__01('fmb_$i_1') = 'fmb_$i_3' )
& ( c_27type_2elist_2elist_27__01('fmb_$i_2') = 'fmb_$i_1' )
& ( c_27type_2elist_2elist_27__01('fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_27const_2elist_2elist__CASE_27__03,type,
c_27const_2elist_2elist__CASE_27__03: ( $i * $i * $i ) > $i ).
tff(function_c_27const_2elist_2elist__CASE_27__03,axiom,
( ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_3' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_1','fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_1','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_1','fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_1','fmb_$i_3','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_1','fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_2','fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_2','fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_2','fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_2','fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_2','fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_3','fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_3','fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_3','fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_3','fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_3','fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_3','fmb_$i_2','fmb_$i_3') = 'fmb_$i_3' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_3','fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_3','fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2elist_2elist__CASE_27__03('fmb_$i_3','fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_27const_2elist_2eCONS_27__02,type,
c_27const_2elist_2eCONS_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2elist_2eCONS_27__02,axiom,
( ( c_27const_2elist_2eCONS_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2elist_2eCONS_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2elist_2eCONS_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27const_2elist_2eCONS_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2elist_2eCONS_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2elist_2eCONS_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2elist_2eCONS_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2elist_2eCONS_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2elist_2eCONS_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' ) ) ).
tff(declare_c_27type_2ewordSem_2eword__loc_27__01,type,
c_27type_2ewordSem_2eword__loc_27__01: $i > $i ).
tff(function_c_27type_2ewordSem_2eword__loc_27__01,axiom,
( ( c_27type_2ewordSem_2eword__loc_27__01('fmb_$i_1') = 'fmb_$i_1' )
& ( c_27type_2ewordSem_2eword__loc_27__01('fmb_$i_2') = 'fmb_$i_1' )
& ( c_27type_2ewordSem_2eword__loc_27__01('fmb_$i_3') = 'fmb_$i_1' ) ) ).
tff(declare_c_27type_2efcp_2ecart_27__02,type,
c_27type_2efcp_2ecart_27__02: ( $i * $i ) > $i ).
tff(function_c_27type_2efcp_2ecart_27__02,axiom,
( ( c_27type_2efcp_2ecart_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27type_2efcp_2ecart_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27type_2efcp_2ecart_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27type_2efcp_2ecart_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27type_2efcp_2ecart_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27type_2efcp_2ecart_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27type_2efcp_2ecart_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27type_2efcp_2ecart_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27type_2efcp_2ecart_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' ) ) ).
tff(declare_c_27const_2ewordSem_2eWord_27__01,type,
c_27const_2ewordSem_2eWord_27__01: $i > $i ).
tff(function_c_27const_2ewordSem_2eWord_27__01,axiom,
( ( c_27const_2ewordSem_2eWord_27__01('fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2ewordSem_2eWord_27__01('fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2eWord_27__01('fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ewordSem_2eLoc_27__02,type,
c_27const_2ewordSem_2eLoc_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2ewordSem_2eLoc_27__02,axiom,
( ( c_27const_2ewordSem_2eLoc_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2ewordSem_2eLoc_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2eLoc_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2eLoc_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2ewordSem_2eLoc_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2eLoc_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2eLoc_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2eLoc_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2eLoc_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_27type_2ewordSem_2estack__frame_27__01,type,
c_27type_2ewordSem_2estack__frame_27__01: $i > $i ).
tff(function_c_27type_2ewordSem_2estack__frame_27__01,axiom,
( ( c_27type_2ewordSem_2estack__frame_27__01('fmb_$i_1') = 'fmb_$i_1' )
& ( c_27type_2ewordSem_2estack__frame_27__01('fmb_$i_2') = 'fmb_$i_3' )
& ( c_27type_2ewordSem_2estack__frame_27__01('fmb_$i_3') = 'fmb_$i_1' ) ) ).
tff(declare_c_27const_2ewordSem_2eStackFrame_27__02,type,
c_27const_2ewordSem_2eStackFrame_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2ewordSem_2eStackFrame_27__02,axiom,
( ( c_27const_2ewordSem_2eStackFrame_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2eStackFrame_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2eStackFrame_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2eStackFrame_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2ewordSem_2eStackFrame_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_3' )
& ( c_27const_2ewordSem_2eStackFrame_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_3' )
& ( c_27const_2ewordSem_2eStackFrame_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2ewordSem_2eStackFrame_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_3' )
& ( c_27const_2ewordSem_2eStackFrame_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_27const_2ewordSem_2estack__frame__CASE_27__02,type,
c_27const_2ewordSem_2estack__frame__CASE_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2ewordSem_2estack__frame__CASE_27__02,axiom,
( ( c_27const_2ewordSem_2estack__frame__CASE_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2ewordSem_2estack__frame__CASE_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estack__frame__CASE_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_3' )
& ( c_27const_2ewordSem_2estack__frame__CASE_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2ewordSem_2estack__frame__CASE_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estack__frame__CASE_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_3' )
& ( c_27const_2ewordSem_2estack__frame__CASE_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2ewordSem_2estack__frame__CASE_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estack__frame__CASE_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' ) ) ).
tff(declare_c_27type_2ewordSem_2estate_27__02,type,
c_27type_2ewordSem_2estate_27__02: ( $i * $i ) > $i ).
tff(function_c_27type_2ewordSem_2estate_27__02,axiom,
( ( c_27type_2ewordSem_2estate_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27type_2ewordSem_2estate_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27type_2ewordSem_2estate_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27type_2ewordSem_2estate_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_3' )
& ( c_27type_2ewordSem_2estate_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_3' )
& ( c_27type_2ewordSem_2estate_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_3' )
& ( c_27type_2ewordSem_2estate_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27type_2ewordSem_2estate_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27type_2ewordSem_2estate_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_1' ) ) ).
tff(declare_c_27const_2ecombin_2eK_27__01,type,
c_27const_2ecombin_2eK_27__01: $i > $i ).
tff(function_c_27const_2ecombin_2eK_27__01,axiom,
( ( c_27const_2ecombin_2eK_27__01('fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ecombin_2eK_27__01('fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ecombin_2eK_27__01('fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27type_2esptree_2espt_27__01,type,
c_27type_2esptree_2espt_27__01: $i > $i ).
tff(function_c_27type_2esptree_2espt_27__01,axiom,
( ( c_27type_2esptree_2espt_27__01('fmb_$i_1') = 'fmb_$i_2' )
& ( c_27type_2esptree_2espt_27__01('fmb_$i_2') = 'fmb_$i_2' )
& ( c_27type_2esptree_2espt_27__01('fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2esptree_2efromAList_27__01,type,
c_27const_2esptree_2efromAList_27__01: $i > $i ).
tff(function_c_27const_2esptree_2efromAList_27__01,axiom,
( ( c_27const_2esptree_2efromAList_27__01('fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2esptree_2efromAList_27__01('fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2esptree_2efromAList_27__01('fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ewordSem_2estate__stack__fupd_27__02,type,
c_27const_2ewordSem_2estate__stack__fupd_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2ewordSem_2estate__stack__fupd_27__02,axiom,
( ( c_27const_2ewordSem_2estate__stack__fupd_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__stack__fupd_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__stack__fupd_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__stack__fupd_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__stack__fupd_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__stack__fupd_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__stack__fupd_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__stack__fupd_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__stack__fupd_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ewordSem_2estate__locals__fupd_27__02,type,
c_27const_2ewordSem_2estate__locals__fupd_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2ewordSem_2estate__locals__fupd_27__02,axiom,
( ( c_27const_2ewordSem_2estate__locals__fupd_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__locals__fupd_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__locals__fupd_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__locals__fupd_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__locals__fupd_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__locals__fupd_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__locals__fupd_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__locals__fupd_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__locals__fupd_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ewordSem_2estate__handler__fupd_27__02,type,
c_27const_2ewordSem_2estate__handler__fupd_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2ewordSem_2estate__handler__fupd_27__02,axiom,
( ( c_27const_2ewordSem_2estate__handler__fupd_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__handler__fupd_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2estate__handler__fupd_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2estate__handler__fupd_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__handler__fupd_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2estate__handler__fupd_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2estate__handler__fupd_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__handler__fupd_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__handler__fupd_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ewordSem_2ejump__exc_27__01,type,
c_27const_2ewordSem_2ejump__exc_27__01: $i > $i ).
tff(function_c_27const_2ewordSem_2ejump__exc_27__01,axiom,
( ( c_27const_2ewordSem_2ejump__exc_27__01('fmb_$i_1') = 'fmb_$i_3' )
& ( c_27const_2ewordSem_2ejump__exc_27__01('fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2ejump__exc_27__01('fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ewordSem_2estate__handler_27__01,type,
c_27const_2ewordSem_2estate__handler_27__01: $i > $i ).
tff(function_c_27const_2ewordSem_2estate__handler_27__01,axiom,
( ( c_27const_2ewordSem_2estate__handler_27__01('fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__handler_27__01('fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__handler_27__01('fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ewordSem_2estate__stack_27__01,type,
c_27const_2ewordSem_2estate__stack_27__01: $i > $i ).
tff(function_c_27const_2ewordSem_2estate__stack_27__01,axiom,
( ( c_27const_2ewordSem_2estate__stack_27__01('fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__stack_27__01('fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__stack_27__01('fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2elist_2eLENGTH_27__01,type,
c_27const_2elist_2eLENGTH_27__01: $i > $i ).
tff(function_c_27const_2elist_2eLENGTH_27__01,axiom,
( ( c_27const_2elist_2eLENGTH_27__01('fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2elist_2eLENGTH_27__01('fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2elist_2eLENGTH_27__01('fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2eprim__rec_2e_3c_27__02,type,
c_27const_2eprim__rec_2e_3c_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2eprim__rec_2e_3c_27__02,axiom,
( ( c_27const_2eprim__rec_2e_3c_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2eprim__rec_2e_3c_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2eprim__rec_2e_3c_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2eprim__rec_2e_3c_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2eprim__rec_2e_3c_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2eprim__rec_2e_3c_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2eprim__rec_2e_3c_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2eprim__rec_2e_3c_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2eprim__rec_2e_3c_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2earithmetic_2eBIT1_27__01,type,
c_27const_2earithmetic_2eBIT1_27__01: $i > $i ).
tff(function_c_27const_2earithmetic_2eBIT1_27__01,axiom,
( ( c_27const_2earithmetic_2eBIT1_27__01('fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2earithmetic_2eBIT1_27__01('fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2earithmetic_2eBIT1_27__01('fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2earithmetic_2eNUMERAL_27__01,type,
c_27const_2earithmetic_2eNUMERAL_27__01: $i > $i ).
tff(function_c_27const_2earithmetic_2eNUMERAL_27__01,axiom,
( ( c_27const_2earithmetic_2eNUMERAL_27__01('fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2earithmetic_2eNUMERAL_27__01('fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2earithmetic_2eNUMERAL_27__01('fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2earithmetic_2e_2b_27__02,type,
c_27const_2earithmetic_2e_2b_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2earithmetic_2e_2b_27__02,axiom,
( ( c_27const_2earithmetic_2e_2b_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2earithmetic_2e_2b_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2earithmetic_2e_2b_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2earithmetic_2e_2b_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2earithmetic_2e_2b_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2earithmetic_2e_2b_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2earithmetic_2e_2b_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2earithmetic_2e_2b_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2earithmetic_2e_2b_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2erich__list_2eLASTN_27__02,type,
c_27const_2erich__list_2eLASTN_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2erich__list_2eLASTN_27__02,axiom,
( ( c_27const_2erich__list_2eLASTN_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2erich__list_2eLASTN_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2erich__list_2eLASTN_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2erich__list_2eLASTN_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2erich__list_2eLASTN_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2erich__list_2eLASTN_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2erich__list_2eLASTN_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2erich__list_2eLASTN_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2erich__list_2eLASTN_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2edata__to__word__gcProof_2einc__clock_27__02,type,
c_27const_2edata__to__word__gcProof_2einc__clock_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2edata__to__word__gcProof_2einc__clock_27__02,axiom,
( ( c_27const_2edata__to__word__gcProof_2einc__clock_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2edata__to__word__gcProof_2einc__clock_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2edata__to__word__gcProof_2einc__clock_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2edata__to__word__gcProof_2einc__clock_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2edata__to__word__gcProof_2einc__clock_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2edata__to__word__gcProof_2einc__clock_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2edata__to__word__gcProof_2einc__clock_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2edata__to__word__gcProof_2einc__clock_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2edata__to__word__gcProof_2einc__clock_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ewordSem_2estate__clock_27__01,type,
c_27const_2ewordSem_2estate__clock_27__01: $i > $i ).
tff(function_c_27const_2ewordSem_2estate__clock_27__01,axiom,
( ( c_27const_2ewordSem_2estate__clock_27__01('fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__clock_27__01('fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__clock_27__01('fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ewordSem_2estate__clock__fupd_27__02,type,
c_27const_2ewordSem_2estate__clock__fupd_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2ewordSem_2estate__clock__fupd_27__02,axiom,
( ( c_27const_2ewordSem_2estate__clock__fupd_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__clock__fupd_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__clock__fupd_27__02('fmb_$i_1','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__clock__fupd_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__clock__fupd_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__clock__fupd_27__02('fmb_$i_2','fmb_$i_3') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__clock__fupd_27__02('fmb_$i_3','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__clock__fupd_27__02('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__clock__fupd_27__02('fmb_$i_3','fmb_$i_3') = 'fmb_$i_2' ) ) ).
tff(declare_p__01,type,
p__01: $i > $o ).
tff(predicate_p__01,axiom,
( p__01('fmb_$i_1')
& ~ p__01('fmb_$i_2')
& ~ p__01('fmb_$i_3') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW935+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 % Computer : n005.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Mon Sep 28 14:45:01 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 Running first-order model finding
% 0.10/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
% 23.86/3.63 % (835140)Will run a generic schedule for satisfiability detection.
% 23.86/3.63 % (835148)dis+10_1_sil=32000:sp=arity:random_seed=417269718:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 23.86/3.63 % (835146)% WARNING: option uhcvi not known.
% 23.86/3.63 % (835145)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=10095102_2999 on theBenchmark for (2999ds/0Mi)
% 23.86/3.63 % (835147)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2837320695:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 23.86/3.63 % (835146)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2411777833:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 23.86/3.63 % (835149)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=182218360:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 23.86/3.63 % (835150)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1079264273:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 23.86/3.63 % (835151)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2980967412:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 23.86/3.63 % (835148)Instruction limit reached!
% 23.86/3.63 % (835148)------------------------------
% 23.86/3.63 % (835148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.86/3.63 % (835148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.86/3.63 % (835148)CaDiCaL version: 2.1.3
% 23.86/3.63 % (835148)Termination reason: Instruction limit
% 23.86/3.63 % (835148)Termination phase: Saturation
% 23.86/3.63 % (835148)Time elapsed: 0.028 s
% 23.86/3.63 % (835148)Peak memory usage: 12 MB
% 23.86/3.63 % (835148)Instructions burned: 107 (million)
% 23.86/3.63 % (835159)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2671876967:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 23.86/3.63 % (835149)Instruction limit reached!
% 23.86/3.63 % (835149)------------------------------
% 23.86/3.63 % (835149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.86/3.63 % (835149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.86/3.63 % (835149)CaDiCaL version: 2.1.3
% 23.86/3.63 % (835149)Termination reason: Instruction limit
% 23.86/3.63 % (835149)Termination phase: Saturation
% 23.86/3.63 % (835149)Time elapsed: 0.054 s
% 23.86/3.63 % (835149)Peak memory usage: 12 MB
% 23.86/3.63 % (835149)Instructions burned: 116 (million)
% 23.86/3.63 % (835150)Instruction limit reached!
% 23.86/3.63 % (835150)------------------------------
% 23.86/3.63 % (835150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.86/3.63 % (835150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.86/3.63 % (835150)CaDiCaL version: 2.1.3
% 23.86/3.63 % (835150)Termination reason: Instruction limit
% 23.86/3.63 % (835150)Termination phase: Saturation
% 23.86/3.63 % (835150)Time elapsed: 0.063 s
% 23.86/3.63 % (835150)Peak memory usage: 12 MB
% 23.86/3.63 % (835150)Instructions burned: 131 (million)
% 23.86/3.63 % (835161)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3772878795:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 23.86/3.63 % (835151)Instruction limit reached!
% 23.86/3.63 % (835151)------------------------------
% 23.86/3.63 % (835151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.86/3.63 % (835151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.86/3.63 % (835151)CaDiCaL version: 2.1.3
% 23.86/3.63 % (835151)Termination reason: Instruction limit
% 23.86/3.63 % (835151)Termination phase: Saturation
% 23.86/3.63 % (835151)Time elapsed: 0.075 s
% 23.86/3.63 % (835151)Peak memory usage: 12 MB
% 23.86/3.63 % (835151)Instructions burned: 160 (million)
% 23.86/3.63 % (835162)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=3987171878:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 23.86/3.63 % (835164)ott-21_1_sil=16000:fs=off:random_seed=3965626516:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 23.86/3.63 % (835161)Instruction limit reached!
% 23.86/3.63 % (835161)------------------------------
% 23.86/3.63 % (835161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.86/3.63 % (835161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.86/3.63 % (835161)CaDiCaL version: 2.1.3
% 23.86/3.63 % (835161)Termination reason: Instruction limit
% 42.30/6.28 % (835161)Termination phase: Saturation
% 42.30/6.28 % (835161)Time elapsed: 0.065 s
% 42.30/6.28 % (835161)Peak memory usage: 12 MB
% 42.30/6.28 % (835161)Instructions burned: 133 (million)
% 42.30/6.28 % (835167)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1967639664:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 42.30/6.28 % (835164)Instruction limit reached!
% 42.30/6.28 % (835164)------------------------------
% 42.30/6.28 % (835164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.30/6.28 % (835164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.30/6.28 % (835164)CaDiCaL version: 2.1.3
% 42.30/6.28 % (835164)Termination reason: Instruction limit
% 42.30/6.28 % (835164)Termination phase: Saturation
% 42.30/6.28 % (835164)Time elapsed: 0.089 s
% 42.30/6.28 % (835164)Peak memory usage: 13 MB
% 42.30/6.28 % (835164)Instructions burned: 182 (million)
% 42.30/6.28 % (835169)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4119112082:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 42.30/6.28 % (835159)Instruction limit reached!
% 42.30/6.28 % (835159)------------------------------
% 42.30/6.28 % (835159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.30/6.28 % (835159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.30/6.28 % (835159)CaDiCaL version: 2.1.3
% 42.30/6.28 % (835159)Termination reason: Instruction limit
% 42.30/6.28 % (835159)Termination phase: Finite model building preprocessing
% 42.30/6.28 % (835159)Time elapsed: 0.203 s
% 42.30/6.28 % (835159)Peak memory usage: 13 MB
% 42.30/6.28 % (835159)Instructions burned: 715 (million)
% 42.30/6.28 % (835171)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1705221270:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 42.30/6.28 % (835167)Instruction limit reached!
% 42.30/6.28 % (835167)------------------------------
% 42.30/6.28 % (835167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.30/6.28 % (835167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.30/6.28 % (835167)CaDiCaL version: 2.1.3
% 42.30/6.28 % (835167)Termination reason: Instruction limit
% 42.30/6.28 % (835167)Termination phase: Saturation
% 42.30/6.28 % (835167)Time elapsed: 0.254 s
% 42.30/6.28 % (835167)Peak memory usage: 16 MB
% 42.30/6.28 % (835167)Instructions burned: 477 (million)
% 42.30/6.28 % (835162)Instruction limit reached!
% 42.30/6.28 % (835162)------------------------------
% 42.30/6.28 % (835162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.30/6.28 % (835162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.30/6.28 % (835162)CaDiCaL version: 2.1.3
% 42.30/6.28 % (835162)Termination reason: Instruction limit
% 42.30/6.28 % (835162)Termination phase: Saturation
% 42.30/6.28 % (835162)Time elapsed: 0.344 s
% 42.30/6.28 % (835162)Peak memory usage: 16 MB
% 42.30/6.28 % (835162)Instructions burned: 685 (million)
% 42.30/6.28 % (835174)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2345317049:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 42.30/6.28 % (835175)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1120742363:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 42.30/6.28 % (835171)Instruction limit reached!
% 42.30/6.28 % (835171)------------------------------
% 42.30/6.28 % (835171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.30/6.28 % (835171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.30/6.28 % (835171)CaDiCaL version: 2.1.3
% 42.30/6.28 % (835171)Termination reason: Instruction limit
% 42.30/6.28 % (835171)Termination phase: Saturation
% 42.30/6.28 % (835171)Time elapsed: 0.316 s
% 42.30/6.28 % (835171)Peak memory usage: 18 MB
% 42.30/6.28 % (835171)Instructions burned: 1183 (million)
% 42.30/6.28 % (835178)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1997297397:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 42.30/6.28 % (835169)Instruction limit reached!
% 42.30/6.28 % (835169)------------------------------
% 42.30/6.28 % (835169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.30/6.28 % (835169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.30/6.28 % (835169)CaDiCaL version: 2.1.3
% 42.30/6.28 % (835169)Termination reason: Instruction limit
% 42.30/6.28 % (835169)Termination phase: Finite model building preprocessing
% 31.94/10.41 % (835169)Time elapsed: 0.468 s
% 31.94/10.41 % (835169)Peak memory usage: 13 MB
% 31.94/10.41 % (835169)Instructions burned: 865 (million)
% 31.94/10.41 % (835180)fmb+10_1_sil=64000:random_seed=3281372516:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 31.94/10.41 % (835175)Instruction limit reached!
% 31.94/10.41 % (835175)------------------------------
% 31.94/10.41 % (835175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835175)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835175)Termination reason: Instruction limit
% 31.94/10.41 % (835175)Termination phase: Saturation
% 31.94/10.41 % (835175)Time elapsed: 0.379 s
% 31.94/10.41 % (835175)Peak memory usage: 14 MB
% 31.94/10.41 % (835175)Instructions burned: 694 (million)
% 31.94/10.41 % (835178)Instruction limit reached!
% 31.94/10.41 % (835178)------------------------------
% 31.94/10.41 % (835178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835178)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835178)Termination reason: Instruction limit
% 31.94/10.41 % (835178)Termination phase: Saturation
% 31.94/10.41 % (835178)Time elapsed: 0.254 s
% 31.94/10.41 % (835178)Peak memory usage: 18 MB
% 31.94/10.41 % (835178)Instructions burned: 882 (million)
% 31.94/10.41 % (835183)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=901588992:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 31.94/10.41 % (835182)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2732231617:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 31.94/10.41 % (835174)Instruction limit reached!
% 31.94/10.41 % (835174)------------------------------
% 31.94/10.41 % (835174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835174)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835174)Termination reason: Instruction limit
% 31.94/10.41 % (835174)Termination phase: Finite model building preprocessing
% 31.94/10.41 % (835174)Time elapsed: 0.483 s
% 31.94/10.41 % (835174)Peak memory usage: 13 MB
% 31.94/10.41 % (835174)Instructions burned: 889 (million)
% 31.94/10.41 % (835186)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3460697190:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 31.94/10.41 % (835183)Instruction limit reached!
% 31.94/10.41 % (835183)------------------------------
% 31.94/10.41 % (835183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835183)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835183)Termination reason: Instruction limit
% 31.94/10.41 % (835183)Termination phase: Finite model building preprocessing
% 31.94/10.41 % (835183)Time elapsed: 0.266 s
% 31.94/10.41 % (835183)Peak memory usage: 13 MB
% 31.94/10.41 % (835183)Instructions burned: 920 (million)
% 31.94/10.41 % (835188)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3000248916:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 31.94/10.41 % TRYING [1]
% 31.94/10.41 % TRYING [2]
% 31.94/10.41 % (835188)Instruction limit reached!
% 31.94/10.41 % (835188)------------------------------
% 31.94/10.41 % (835188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835188)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835188)Termination reason: Instruction limit
% 31.94/10.41 % (835188)Termination phase: Saturation
% 31.94/10.41 % (835188)Time elapsed: 0.404 s
% 31.94/10.41 % (835188)Peak memory usage: 33 MB
% 31.94/10.41 % (835188)Instructions burned: 1475 (million)
% 31.94/10.41 % (835190)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3095678107:i=6324_2984 on theBenchmark for (2984ds/6324Mi)
% 31.94/10.41 % TRYING [3]
% 31.94/10.41 % (835186)Instruction limit reached!
% 31.94/10.41 % (835186)------------------------------
% 31.94/10.41 % (835186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835186)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835186)Termination reason: Instruction limit
% 31.94/10.41 % (835186)Termination phase: Saturation
% 31.94/10.41 % (835186)Time elapsed: 2.426 s
% 31.94/10.41 % (835186)Peak memory usage: 25 MB
% 31.94/10.41 % (835186)Instructions burned: 5132 (million)
% 31.94/10.41 % (835192)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3996772542:fmbsr=2.30978:i=2174_2965 on theBenchmark for (2965ds/2174Mi)
% 31.94/10.41 % (835190)Instruction limit reached!
% 31.94/10.41 % (835190)------------------------------
% 31.94/10.41 % (835190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835190)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835190)Termination reason: Instruction limit
% 31.94/10.41 % (835190)Termination phase: Finite model building preprocessing
% 31.94/10.41 % (835190)Time elapsed: 1.876 s
% 31.94/10.41 % (835190)Peak memory usage: 22 MB
% 31.94/10.41 % (835190)Instructions burned: 6325 (million)
% 31.94/10.41 % (835194)ott-2_1_sil=16000:newcnf=on:random_seed=3534534054:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2965 on theBenchmark for (2965ds/869Mi)
% 31.94/10.41 % (835194)Instruction limit reached!
% 31.94/10.41 % (835194)------------------------------
% 31.94/10.41 % (835194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835194)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835194)Termination reason: Instruction limit
% 31.94/10.41 % (835194)Termination phase: Saturation
% 31.94/10.41 % (835194)Time elapsed: 0.206 s
% 31.94/10.41 % (835194)Peak memory usage: 13 MB
% 31.94/10.41 % (835194)Instructions burned: 874 (million)
% 31.94/10.41 % (835196)ott+10_1_sil=32000:tgt=ground:random_seed=965514624:i=5114:av=off_2963 on theBenchmark for (2963ds/5114Mi)
% 31.94/10.41 % (835192)Instruction limit reached!
% 31.94/10.41 % (835192)------------------------------
% 31.94/10.41 % (835192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835192)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835192)Termination reason: Instruction limit
% 31.94/10.41 % (835192)Termination phase: Finite model building preprocessing
% 31.94/10.41 % (835192)Time elapsed: 1.188 s
% 31.94/10.41 % (835192)Peak memory usage: 15 MB
% 31.94/10.41 % (835192)Instructions burned: 2175 (million)
% 31.94/10.41 % (835198)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1843475633:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 31.94/10.41 % TRYING [1]
% 31.94/10.41 % TRYING [2]
% 31.94/10.41 % TRYING [3]
% 31.94/10.41 % (835196)Instruction limit reached!
% 31.94/10.41 % (835196)------------------------------
% 31.94/10.41 % (835196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835196)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835196)Termination reason: Instruction limit
% 31.94/10.41 % (835196)Termination phase: Saturation
% 31.94/10.41 % (835196)Time elapsed: 1.387 s
% 31.94/10.41 % (835196)Peak memory usage: 38 MB
% 31.94/10.41 % (835196)Instructions burned: 5116 (million)
% 31.94/10.41 % (835200)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3811422284:i=3512:aac=none_2949 on theBenchmark for (2949ds/3512Mi)
% 31.94/10.41 % (835182)Cannot represent all propositional literals internally
% 31.94/10.41 % (835182)Refutation not found, incomplete strategy
% 31.94/10.41 % (835182)------------------------------
% 31.94/10.41 % (835182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835182)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835182)Termination reason: Refutation not found, incomplete strategy
% 31.94/10.41 % (835182)Time elapsed: 4.699 s
% 31.94/10.41 % (835182)Peak memory usage: 28 MB
% 31.94/10.41 % (835182)Instructions burned: 8310 (million)
% 31.94/10.41 % (835182)------------------------------
% 31.94/10.41 % (835182)------------------------------
% 31.94/10.41 % (835202)dis+21_1_sil=32000:sas=cadical:random_seed=3901712757:i=3773:amm=off_2944 on theBenchmark for (2944ds/3773Mi)
% 31.94/10.41 % (835200)Instruction limit reached!
% 31.94/10.41 % (835200)------------------------------
% 31.94/10.41 % (835200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835200)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835200)Termination reason: Instruction limit
% 31.94/10.41 % (835200)Termination phase: Saturation
% 31.94/10.41 % (835200)Time elapsed: 0.943 s
% 31.94/10.41 % (835200)Peak memory usage: 30 MB
% 31.94/10.41 % (835200)Instructions burned: 3515 (million)
% 31.94/10.41 % (835204)ott+11_1_sil=16000:gs=on:random_seed=265870623:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2939 on theBenchmark for (2939ds/2251Mi)
% 31.94/10.41 % (835204)Instruction limit reached!
% 31.94/10.41 % (835204)------------------------------
% 31.94/10.41 % (835204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835204)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835204)Termination reason: Instruction limit
% 31.94/10.41 % (835204)Termination phase: Saturation
% 31.94/10.41 % (835204)Time elapsed: 0.631 s
% 31.94/10.41 % (835204)Peak memory usage: 26 MB
% 31.94/10.41 % (835204)Instructions burned: 2251 (million)
% 31.94/10.41 % (835206)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2203360313:fmbsr=1.6:i=67534_2933 on theBenchmark for (2933ds/67534Mi)
% 31.94/10.41 % (835202)Instruction limit reached!
% 31.94/10.41 % (835202)------------------------------
% 31.94/10.41 % (835202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835202)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835202)Termination reason: Instruction limit
% 31.94/10.41 % (835202)Termination phase: Saturation
% 31.94/10.41 % (835202)Time elapsed: 1.924 s
% 31.94/10.41 % (835202)Peak memory usage: 31 MB
% 31.94/10.41 % (835202)Instructions burned: 3775 (million)
% 31.94/10.41 % (835208)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=133116449:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2924 on theBenchmark for (2924ds/4591Mi)
% 31.94/10.41 % (835208)Instruction limit reached!
% 31.94/10.41 % (835208)------------------------------
% 31.94/10.41 % (835208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.41 % (835208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.41 % (835208)CaDiCaL version: 2.1.3
% 31.94/10.41 % (835208)Termination reason: Instruction limit
% 31.94/10.41 % (835208)Termination phase: Saturation
% 31.94/10.41 % (835208)Time elapsed: 1.678 s
% 31.94/10.41 % (835208)Peak memory usage: 25 MB
% 31.94/10.41 % (835208)Instructions burned: 4592 (million)
% 31.94/10.41 % (835210)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=889628173:i=29340_2907 on theBenchmark for (2907ds/29340Mi)
% 31.94/10.41 % TRYING [1]
% 31.94/10.41 % TRYING [2]
% 31.94/10.41 % TRYING [3]
% 31.94/10.41 % Finite Model Found!
% 31.94/10.41 % SZS status CounterSatisfiable for theBenchmark
% 31.94/10.41 % (835145) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-835140-835145"...
% 31.94/10.41 % (835145)...printing done.
% 31.94/10.41 % SZS output start FiniteModel for theBenchmark
% See solution above
% 31.94/10.42 % (835145)------------------------------
% 31.94/10.42 % (835145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.94/10.42 % (835145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.94/10.42 % (835145)CaDiCaL version: 2.1.3
% 31.94/10.42 % (835145)Termination reason: Satisfiable
% 31.94/10.42 % (835145)Time elapsed: 10.089 s
% 31.94/10.42 % (835145)Peak memory usage: 144 MB
% 31.94/10.42 % (835145)Instructions burned: 19759 (million)
% 31.94/10.42 % (835140)Success in time 10.185 s
% 31.94/10.42 % Vampire exiting
%------------------------------------------------------------------------------