%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW901+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 : n026.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:09 PM UTC 2026
% Result : CounterSatisfiable 14.60s 2.35s
% Output : FiniteModel 14.60s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('declare_$i2',type,
'fmb_$i_2': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' ) ) ).
tff('distinct_domain_$i',axiom,
'fmb_$i_1' != 'fmb_$i_2' ).
tff(declare_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_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_1' ).
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_1' ).
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_1' ).
tff(declare_c_27const_2ewordSem_2ekey__val__compare_27__00,type,
c_27const_2ewordSem_2ekey__val__compare_27__00: $i ).
tff(c_27const_2ewordSem_2ekey__val__compare_27__00_definition,axiom,
c_27const_2ewordSem_2ekey__val__compare_27__00 = 'fmb_$i_1' ).
tff(declare_c_27const_2enum_2e0_27__00,type,
c_27const_2enum_2e0_27__00: $i ).
tff(c_27const_2enum_2e0_27__00_definition,axiom,
c_27const_2enum_2e0_27__00 = 'fmb_$i_1' ).
tff(declare_c_27type_2estackLang_2estore__name_27__00,type,
c_27type_2estackLang_2estore__name_27__00: $i ).
tff(c_27type_2estackLang_2estore__name_27__00_definition,axiom,
c_27type_2estackLang_2estore__name_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_2','fmb_$i_1') = 'fmb_$i_1' )
& ( s__02('fmb_$i_2','fmb_$i_2') = '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_2','fmb_$i_1') = 'fmb_$i_2' )
& ( cfun__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
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_1' )
& ( chapp__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( chapp__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( chapp__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ebool_2eLET_27__02,type,
c_27const_2ebool_2eLET_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2ebool_2eLET_27__02,axiom,
( ( c_27const_2ebool_2eLET_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2ebool_2eLET_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2ebool_2eLET_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ebool_2eLET_27__02('fmb_$i_2','fmb_$i_2') = '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_1' )
& ( c_27const_2ecombin_2eI_27__01('fmb_$i_2') = '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_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27type_2epair_2eprod_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
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_1' )
& ( 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_2' ) ) ).
tff(declare_c_27const_2epair_2eUNCURRY_27__01,type,
c_27const_2epair_2eUNCURRY_27__01: $i > $i ).
tff(function_c_27const_2epair_2eUNCURRY_27__01,axiom,
( ( c_27const_2epair_2eUNCURRY_27__01('fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2epair_2eUNCURRY_27__01('fmb_$i_2') = '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_1' )
& ( c_27type_2eoption_2eoption_27__01('fmb_$i_2') = 'fmb_$i_2' ) ) ).
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_2' )
& ( c_27const_2eoption_2eSOME_27__01('fmb_$i_2') = 'fmb_$i_1' ) ) ).
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_1' )
& ( c_27const_2earithmetic_2eBIT1_27__01('fmb_$i_2') = 'fmb_$i_1' ) ) ).
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' ) ) ).
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_1' )
& ( 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_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2earithmetic_2e_2b_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
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_2' )
& ( c_27type_2ewordSem_2eword__loc_27__01('fmb_$i_2') = 'fmb_$i_2' ) ) ).
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_2' )
& ( c_27type_2elist_2elist_27__01('fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ewordSem_2elist__rearrange_27__02,type,
c_27const_2ewordSem_2elist__rearrange_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2ewordSem_2elist__rearrange_27__02,axiom,
( ( c_27const_2ewordSem_2elist__rearrange_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2elist__rearrange_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2elist__rearrange_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2elist__rearrange_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' ) ) ).
tff(declare_c_27const_2esorting_2eQSORT_27__02,type,
c_27const_2esorting_2eQSORT_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2esorting_2eQSORT_27__02,axiom,
( ( c_27const_2esorting_2eQSORT_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2esorting_2eQSORT_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2esorting_2eQSORT_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2esorting_2eQSORT_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' ) ) ).
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_1' ) ) ).
tff(declare_c_27const_2esptree_2etoAList_27__01,type,
c_27const_2esptree_2etoAList_27__01: $i > $i ).
tff(function_c_27const_2esptree_2etoAList_27__01,axiom,
( ( c_27const_2esptree_2etoAList_27__01('fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2esptree_2etoAList_27__01('fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ewordSem_2eenv__to__list_27__02,type,
c_27const_2ewordSem_2eenv__to__list_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2ewordSem_2eenv__to__list_27__02,axiom,
( ( c_27const_2ewordSem_2eenv__to__list_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2eenv__to__list_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2eenv__to__list_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2eenv__to__list_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' ) ) ).
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_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27type_2ewordSem_2estate_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' ) ) ).
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_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_1' )
& ( c_27const_2ewordSem_2eStackFrame_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2eStackFrame_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2eStackFrame_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' ) ) ).
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_1' ) ) ).
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_2' )
& ( 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' ) ) ).
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' ) ) ).
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' ) ) ).
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_1' )
& ( 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_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2estate__handler__fupd_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ewordSem_2estate__permute__fupd_27__02,type,
c_27const_2ewordSem_2estate__permute__fupd_27__02: ( $i * $i ) > $i ).
tff(function_c_27const_2ewordSem_2estate__permute__fupd_27__02,axiom,
( ( c_27const_2ewordSem_2estate__permute__fupd_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2estate__permute__fupd_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2estate__permute__fupd_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2estate__permute__fupd_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' ) ) ).
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_1' )
& ( c_27const_2ewordSem_2estate__stack__fupd_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2estate__stack__fupd_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2estate__stack__fupd_27__02('fmb_$i_2','fmb_$i_2') = '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_1' )
& ( c_27const_2ewordSem_2estate__handler_27__01('fmb_$i_2') = 'fmb_$i_1' ) ) ).
tff(declare_c_27type_2ewordLang_2eprog_27__01,type,
c_27type_2ewordLang_2eprog_27__01: $i > $i ).
tff(function_c_27type_2ewordLang_2eprog_27__01,axiom,
( ( c_27type_2ewordLang_2eprog_27__01('fmb_$i_1') = 'fmb_$i_2' )
& ( c_27type_2ewordLang_2eprog_27__01('fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_c_27const_2ewordSem_2epush__env_27__03,type,
c_27const_2ewordSem_2epush__env_27__03: ( $i * $i * $i ) > $i ).
tff(function_c_27const_2ewordSem_2epush__env_27__03,axiom,
( ( c_27const_2ewordSem_2epush__env_27__03('fmb_$i_1','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2epush__env_27__03('fmb_$i_1','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2epush__env_27__03('fmb_$i_1','fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2epush__env_27__03('fmb_$i_1','fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2epush__env_27__03('fmb_$i_2','fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2epush__env_27__03('fmb_$i_2','fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2epush__env_27__03('fmb_$i_2','fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2epush__env_27__03('fmb_$i_2','fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' ) ) ).
tff(declare_c_27const_2ewordSem_2estate__permute_27__01,type,
c_27const_2ewordSem_2estate__permute_27__01: $i > $i ).
tff(function_c_27const_2ewordSem_2estate__permute_27__01,axiom,
( ( c_27const_2ewordSem_2estate__permute_27__01('fmb_$i_1') = 'fmb_$i_2' )
& ( c_27const_2ewordSem_2estate__permute_27__01('fmb_$i_2') = 'fmb_$i_2' ) ) ).
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_1' )
& ( c_27type_2efcp_2ecart_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( 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' ) ) ).
tff(declare_c_27type_2efinite__map_2efmap_27__02,type,
c_27type_2efinite__map_2efmap_27__02: ( $i * $i ) > $i ).
tff(function_c_27type_2efinite__map_2efmap_27__02,axiom,
( ( c_27type_2efinite__map_2efmap_27__02('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27type_2efinite__map_2efmap_27__02('fmb_$i_1','fmb_$i_2') = 'fmb_$i_1' )
& ( c_27type_2efinite__map_2efmap_27__02('fmb_$i_2','fmb_$i_1') = 'fmb_$i_1' )
& ( c_27type_2efinite__map_2efmap_27__02('fmb_$i_2','fmb_$i_2') = 'fmb_$i_1' ) ) ).
tff(declare_c_27const_2ewordSem_2estate__gc__fun_27__01,type,
c_27const_2ewordSem_2estate__gc__fun_27__01: $i > $i ).
tff(function_c_27const_2ewordSem_2estate__gc__fun_27__01,axiom,
( ( c_27const_2ewordSem_2estate__gc__fun_27__01('fmb_$i_1') = 'fmb_$i_1' )
& ( c_27const_2ewordSem_2estate__gc__fun_27__01('fmb_$i_2') = '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') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW901+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n026.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 14:41:57 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 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
% 14.60/2.35 % (3896785)Will run a generic schedule for satisfiability detection.
% 14.60/2.35 % (3896792)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4250259881:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.60/2.35 % (3896791)% WARNING: option uhcvi not known.
% 14.60/2.35 % (3896790)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3552967223_2999 on theBenchmark for (2999ds/0Mi)
% 14.60/2.35 % (3896791)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2583911450:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.60/2.35 % (3896793)dis+10_1_sil=32000:sp=arity:random_seed=492175167:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.60/2.35 % (3896794)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3440754067:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.60/2.35 % (3896795)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1941068139:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.60/2.35 % (3896796)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1164959174:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.60/2.35 % (3896793)Instruction limit reached!
% 14.60/2.35 % (3896793)------------------------------
% 14.60/2.35 % (3896793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896793)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896793)Termination reason: Instruction limit
% 14.60/2.35 % (3896793)Termination phase: Saturation
% 14.60/2.35 % (3896793)Time elapsed: 0.054 s
% 14.60/2.35 % (3896793)Peak memory usage: 12 MB
% 14.60/2.35 % (3896793)Instructions burned: 105 (million)
% 14.60/2.35 % (3896794)Instruction limit reached!
% 14.60/2.35 % (3896794)------------------------------
% 14.60/2.35 % (3896794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896794)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896794)Termination reason: Instruction limit
% 14.60/2.35 % (3896794)Termination phase: Saturation
% 14.60/2.35 % (3896794)Time elapsed: 0.056 s
% 14.60/2.35 % (3896794)Peak memory usage: 13 MB
% 14.60/2.35 % (3896794)Instructions burned: 117 (million)
% 14.60/2.35 % (3896795)Instruction limit reached!
% 14.60/2.35 % (3896795)------------------------------
% 14.60/2.35 % (3896795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896795)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896795)Termination reason: Instruction limit
% 14.60/2.35 % (3896795)Termination phase: Saturation
% 14.60/2.35 % (3896795)Time elapsed: 0.063 s
% 14.60/2.35 % (3896795)Peak memory usage: 13 MB
% 14.60/2.35 % (3896795)Instructions burned: 133 (million)
% 14.60/2.35 % (3896804)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3974287427:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.60/2.35 % (3896805)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=792848676:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.60/2.35 % (3896796)Instruction limit reached!
% 14.60/2.35 % (3896796)------------------------------
% 14.60/2.35 % (3896796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896796)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896796)Termination reason: Instruction limit
% 14.60/2.35 % (3896796)Termination phase: Saturation
% 14.60/2.35 % (3896796)Time elapsed: 0.075 s
% 14.60/2.35 % (3896796)Peak memory usage: 12 MB
% 14.60/2.35 % (3896796)Instructions burned: 159 (million)
% 14.60/2.35 % (3896806)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=2404238629:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.60/2.35 % (3896809)ott-21_1_sil=16000:fs=off:random_seed=1033541276:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.60/2.35 % (3896805)Instruction limit reached!
% 14.60/2.35 % (3896805)------------------------------
% 14.60/2.35 % (3896805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896805)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896805)Termination reason: Instruction limit
% 14.60/2.35 % (3896805)Termination phase: Saturation
% 14.60/2.35 % (3896805)Time elapsed: 0.067 s
% 14.60/2.35 % (3896805)Peak memory usage: 13 MB
% 14.60/2.35 % (3896805)Instructions burned: 132 (million)
% 14.60/2.35 % (3896812)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4244258976:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 14.60/2.35 % (3896809)Instruction limit reached!
% 14.60/2.35 % (3896809)------------------------------
% 14.60/2.35 % (3896809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896809)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896809)Termination reason: Instruction limit
% 14.60/2.35 % (3896809)Termination phase: Saturation
% 14.60/2.35 % (3896809)Time elapsed: 0.076 s
% 14.60/2.35 % (3896809)Peak memory usage: 12 MB
% 14.60/2.35 % (3896809)Instructions burned: 182 (million)
% 14.60/2.35 % (3896814)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4240949334:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 14.60/2.35 % (3896812)Instruction limit reached!
% 14.60/2.35 % (3896812)------------------------------
% 14.60/2.35 % (3896812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896812)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896812)Termination reason: Instruction limit
% 14.60/2.35 % (3896812)Termination phase: Saturation
% 14.60/2.35 % (3896812)Time elapsed: 0.251 s
% 14.60/2.35 % (3896812)Peak memory usage: 16 MB
% 14.60/2.35 % (3896812)Instructions burned: 478 (million)
% 14.60/2.35 % (3896806)Instruction limit reached!
% 14.60/2.35 % (3896806)------------------------------
% 14.60/2.35 % (3896806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896806)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896816)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3644534824:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 14.60/2.35 % (3896806)Termination reason: Instruction limit
% 14.60/2.35 % (3896806)Termination phase: Saturation
% 14.60/2.35 % (3896806)Time elapsed: 0.351 s
% 14.60/2.35 % (3896806)Peak memory usage: 17 MB
% 14.60/2.35 % (3896806)Instructions burned: 684 (million)
% 14.60/2.35 % (3896818)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1517384436:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 14.60/2.35 % (3896804)Instruction limit reached!
% 14.60/2.35 % (3896804)------------------------------
% 14.60/2.35 % (3896804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896804)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896804)Termination reason: Instruction limit
% 14.60/2.35 % (3896804)Termination phase: Finite model building preprocessing
% 14.60/2.35 % (3896804)Time elapsed: 0.386 s
% 14.60/2.35 % (3896804)Peak memory usage: 12 MB
% 14.60/2.35 % (3896804)Instructions burned: 715 (million)
% 14.60/2.35 % (3896820)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=1328728439:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 14.60/2.35 % (3896814)Instruction limit reached!
% 14.60/2.35 % (3896814)------------------------------
% 14.60/2.35 % (3896814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896814)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896814)Termination reason: Instruction limit
% 14.60/2.35 % (3896814)Termination phase: Finite model building preprocessing
% 14.60/2.35 % (3896814)Time elapsed: 0.481 s
% 14.60/2.35 % (3896814)Peak memory usage: 12 MB
% 14.60/2.35 % (3896814)Instructions burned: 865 (million)
% 14.60/2.35 % (3896822)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2596980180:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 14.60/2.35 % (3896820)Instruction limit reached!
% 14.60/2.35 % (3896820)------------------------------
% 14.60/2.35 % (3896820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896820)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896820)Termination reason: Instruction limit
% 14.60/2.35 % (3896820)Termination phase: Saturation
% 14.60/2.35 % (3896820)Time elapsed: 0.368 s
% 14.60/2.35 % (3896820)Peak memory usage: 17 MB
% 14.60/2.35 % (3896820)Instructions burned: 692 (million)
% 14.60/2.35 % (3896824)fmb+10_1_sil=64000:random_seed=2776092305:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 14.60/2.35 % (3896818)Instruction limit reached!
% 14.60/2.35 % (3896818)------------------------------
% 14.60/2.35 % (3896818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896818)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896818)Termination reason: Instruction limit
% 14.60/2.35 % (3896818)Termination phase: Finite model building preprocessing
% 14.60/2.35 % (3896818)Time elapsed: 0.494 s
% 14.60/2.35 % (3896818)Peak memory usage: 12 MB
% 14.60/2.35 % (3896818)Instructions burned: 889 (million)
% 14.60/2.35 % (3896826)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1879676520:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 14.60/2.35 % (3896816)Instruction limit reached!
% 14.60/2.35 % (3896816)------------------------------
% 14.60/2.35 % (3896816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896816)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896816)Termination reason: Instruction limit
% 14.60/2.35 % (3896816)Termination phase: Saturation
% 14.60/2.35 % (3896816)Time elapsed: 0.573 s
% 14.60/2.35 % (3896816)Peak memory usage: 21 MB
% 14.60/2.35 % (3896816)Instructions burned: 1181 (million)
% 14.60/2.35 % (3896828)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=278762992:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 14.60/2.35 % (3896822)Instruction limit reached!
% 14.60/2.35 % (3896822)------------------------------
% 14.60/2.35 % (3896822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896822)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896822)Termination reason: Instruction limit
% 14.60/2.35 % (3896822)Termination phase: Saturation
% 14.60/2.35 % (3896822)Time elapsed: 0.460 s
% 14.60/2.35 % (3896822)Peak memory usage: 18 MB
% 14.60/2.35 % (3896822)Instructions burned: 879 (million)
% 14.60/2.35 % (3896830)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1118902399:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 14.60/2.35 % (3896828)Instruction limit reached!
% 14.60/2.35 % (3896828)------------------------------
% 14.60/2.35 % (3896828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.35 % (3896828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.35 % (3896828)CaDiCaL version: 2.1.3
% 14.60/2.35 % (3896828)Termination reason: Instruction limit
% 14.60/2.35 % (3896828)Termination phase: Finite model building preprocessing
% 14.60/2.35 % (3896828)Time elapsed: 0.513 s
% 14.60/2.35 % (3896828)Peak memory usage: 12 MB
% 14.60/2.35 % (3896828)Instructions burned: 921 (million)
% 14.60/2.35 % (3896832)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2895328760:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 14.60/2.35 % TRYING [1]
% 14.60/2.35 % TRYING [2]
% 14.60/2.35 % Finite Model Found!
% 14.60/2.35 % SZS status CounterSatisfiable for theBenchmark
% 14.60/2.35 % (3896824) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3896785-3896824"...
% 14.60/2.35 % (3896824)...printing done.
% 14.60/2.35 % SZS output start FiniteModel for theBenchmark
% See solution above
% 14.60/2.36 % (3896824)------------------------------
% 14.60/2.36 % (3896824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.60/2.36 % (3896824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.36 % (3896824)CaDiCaL version: 2.1.3
% 14.60/2.36 % (3896824)Termination reason: Satisfiable
% 14.60/2.36 % (3896824)Time elapsed: 1.197 s
% 14.60/2.36 % (3896824)Peak memory usage: 29 MB
% 14.60/2.36 % (3896824)Instructions burned: 2363 (million)
% 14.60/2.36 % (3896785)Success in time 2.119 s
% 14.60/2.36 % Vampire exiting
%------------------------------------------------------------------------------