%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP015^4 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.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 : Wed Sep 30 08:04:03 AM UTC 2026
% Result : Theorem 23.93s 17.32s
% Output : CNFRefutation 23.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 6
% Syntax : Number of formulae : 21 ( 19 unt; 0 typ; 0 def)
% Number of atoms : 31 ( 30 equ; 0 cnn)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 777 ( 3 ~; 0 |; 10 &; 764 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Number of types : 5 ( 5 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 23 ( 21 usr; 7 con; 0-2 aty)
% Number of variables : 32 ( 0 ^; 32 !; 0 ?; 32 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
d: $tType ).
thf(decl_sort2,type,
u: $tType ).
thf(decl_sort3,type,
du: $tType ).
thf(decl_sort4,type,
mono_2Etyop_2Enum_2Enum: $tType ).
thf(decl_sort5,type,
mono_2Etyop_2Einteger_2Eint: $tType ).
thf(decl_23,type,
tyop_2Emin_2Ebool: d ).
thf(decl_25,type,
s: d > u > du ).
thf(decl_190,type,
tyop_2Enum_2Enum: d ).
thf(decl_211,type,
mono_2Ec_2Enum_2E0: mono_2Etyop_2Enum_2Enum ).
thf(decl_226,type,
i_mono_2Etyop_2Enum_2Enum: mono_2Etyop_2Enum_2Enum > u ).
thf(decl_646,type,
mono_2Ec_2Earithmetic_2EBIT1: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(decl_662,type,
mono_2Ec_2Earithmetic_2ENUMERAL: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(decl_673,type,
mono_2Ec_2Earithmetic_2EZERO: mono_2Etyop_2Enum_2Enum ).
thf(decl_2469,type,
tyop_2Efcp_2Ecart: d > d > d ).
thf(decl_4634,type,
tyop_2Einteger_2Eint: d ).
thf(decl_4747,type,
mono_2Ec_2Einteger_2Eint__mul: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint ).
thf(decl_4749,type,
mono_2Ec_2Einteger_2Eint__of__num: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Einteger_2Eint ).
thf(decl_4782,type,
i_mono_2Etyop_2Einteger_2Eint: mono_2Etyop_2Einteger_2Eint > u ).
thf(decl_4804,type,
j_mono_2Etyop_2Einteger_2Eint: du > mono_2Etyop_2Einteger_2Eint ).
thf(decl_5206,type,
c_2Ewords_2En2w_2E1: du > u ).
thf(decl_5259,type,
c_2Ewords_2Eword__add_2E2: du > du > u ).
thf(decl_5333,type,
c_2Ewords_2Eword__mul_2E2: du > du > u ).
thf(decl_5372,type,
c_2Ewords_2Eword__sub_2E2: du > du > u ).
thf(decl_7391,type,
c_2Einteger__word_2Ei2w_2E1: du > u ).
thf(decl_7409,type,
c_2Einteger__word_2Ew2i_2E1: du > u ).
thf(decl_7461,type,
esk1_0: d ).
thf(thm_2Einteger__word_2Ei2w__0,conjecture,
! [X1: d] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.GU6I0dsIO9/E---3.1_3803216.p',thm_2Einteger__word_2Ei2w__0) ).
thf(thm_2Einteger__word_2Eword__mul__i2w,axiom,
! [X1: d,X125: u,X243: u] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( mono_2Ec_2Einteger_2Eint__mul @ ( j_mono_2Etyop_2Einteger_2Eint @ ( s @ tyop_2Einteger_2Eint @ ( c_2Einteger__word_2Ew2i_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X125 ) ) ) ) @ ( j_mono_2Etyop_2Einteger_2Eint @ ( s @ tyop_2Einteger_2Eint @ ( c_2Einteger__word_2Ew2i_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X243 ) ) ) ) ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X125 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X243 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.GU6I0dsIO9/E---3.1_3803216.p',thm_2Einteger__word_2Eword__mul__i2w) ).
thf(thm_2Ewords_2EWORD__SUB__REFL,axiom,
! [X1: d,X19285: u] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__sub_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X19285 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X19285 ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.GU6I0dsIO9/E---3.1_3803216.p',thm_2Ewords_2EWORD__SUB__REFL) ).
thf(thm_2Einteger__word_2Eword__0__w2i,axiom,
! [X1: d] :
( ( j_mono_2Etyop_2Einteger_2Eint @ ( s @ tyop_2Einteger_2Eint @ ( c_2Einteger__word_2Ew2i_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ) ) )
= ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ),
file('/export/starexec/sandbox/tmp/tmp.GU6I0dsIO9/E---3.1_3803216.p',thm_2Einteger__word_2Eword__0__w2i) ).
thf(thm_2Einteger_2EINT__MUL__RZERO,axiom,
! [X24419: mono_2Etyop_2Einteger_2Eint] :
( ( mono_2Ec_2Einteger_2Eint__mul @ X24419 @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) )
= ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ),
file('/export/starexec/sandbox/tmp/tmp.GU6I0dsIO9/E---3.1_3803216.p',thm_2Einteger_2EINT__MUL__RZERO) ).
thf(thm_2Ewords_2EWORD__MULT__CLAUSES,axiom,
! [X1: d,X264: u,X19286: u] :
( ( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X264 ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) )
& ( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X264 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) )
& ( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X264 ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X264 ) )
& ( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X264 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X264 ) )
& ( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__add_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X264 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ) ) ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X19286 ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__add_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X264 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X19286 ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X19286 ) ) ) )
& ( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X264 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__add_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X19286 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ) ) ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__add_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X264 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X264 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X19286 ) ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.GU6I0dsIO9/E---3.1_3803216.p',thm_2Ewords_2EWORD__MULT__CLAUSES) ).
thf(c_0_6,negated_conjecture,
~ ! [X1: d] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
inference(assume_negation,[status(cth)],[thm_2Einteger__word_2Ei2w__0]) ).
thf(c_0_7,plain,
! [X35167: d,X35168: u,X35169: u] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X35167 ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( mono_2Ec_2Einteger_2Eint__mul @ ( j_mono_2Etyop_2Einteger_2Eint @ ( s @ tyop_2Einteger_2Eint @ ( c_2Einteger__word_2Ew2i_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X35167 ) @ X35168 ) ) ) ) @ ( j_mono_2Etyop_2Einteger_2Eint @ ( s @ tyop_2Einteger_2Eint @ ( c_2Einteger__word_2Ew2i_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X35167 ) @ X35169 ) ) ) ) ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X35167 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X35167 ) @ X35168 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X35167 ) @ X35169 ) ) ) ),
inference(variable_rename,[status(thm)],[thm_2Einteger__word_2Eword__mul__i2w]) ).
thf(c_0_8,plain,
! [X36683: d,X36684: u] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36683 ) @ ( c_2Ewords_2Eword__sub_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36683 ) @ X36684 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36683 ) @ X36684 ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36683 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
inference(variable_rename,[status(thm)],[thm_2Ewords_2EWORD__SUB__REFL]) ).
thf(c_0_9,plain,
! [X35638: d] :
( ( j_mono_2Etyop_2Einteger_2Eint @ ( s @ tyop_2Einteger_2Eint @ ( c_2Einteger__word_2Ew2i_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X35638 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ) ) )
= ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ),
inference(variable_rename,[status(thm)],[thm_2Einteger__word_2Eword__0__w2i]) ).
thf(c_0_10,plain,
! [X36980: mono_2Etyop_2Einteger_2Eint] :
( ( mono_2Ec_2Einteger_2Eint__mul @ X36980 @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) )
= ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ),
inference(variable_rename,[status(thm)],[thm_2Einteger_2EINT__MUL__RZERO]) ).
thf(c_0_11,plain,
! [X36890: d,X36891: u,X36892: u] :
( ( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36891 ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) )
& ( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36891 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) )
& ( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36891 ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36891 ) )
& ( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36891 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36891 ) )
& ( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2Eword__add_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36891 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ) ) ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36892 ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2Eword__add_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36891 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36892 ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36892 ) ) ) )
& ( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36891 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2Eword__add_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36892 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Earithmetic_2ENUMERAL @ ( mono_2Ec_2Earithmetic_2EBIT1 @ mono_2Ec_2Earithmetic_2EZERO ) ) ) ) ) ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2Eword__add_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36891 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36891 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X36890 ) @ X36892 ) ) ) ) ) ) ),
inference(variable_rename,[status(thm)],[thm_2Ewords_2EWORD__MULT__CLAUSES]) ).
thf(c_0_12,negated_conjecture,
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ esk1_0 ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ) ) ) )
!= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ esk1_0 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_6])])])]) ).
thf(c_0_13,plain,
! [X1: d,X3: u,X4: u] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( mono_2Ec_2Einteger_2Eint__mul @ ( j_mono_2Etyop_2Einteger_2Eint @ ( s @ tyop_2Einteger_2Eint @ ( c_2Einteger__word_2Ew2i_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X3 ) ) ) ) @ ( j_mono_2Etyop_2Einteger_2Eint @ ( s @ tyop_2Einteger_2Eint @ ( c_2Einteger__word_2Ew2i_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X4 ) ) ) ) ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X3 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X4 ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_7]) ).
thf(c_0_14,plain,
! [X3: u,X1: d] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__sub_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X3 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X3 ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
thf(c_0_15,plain,
! [X1: d] :
( ( j_mono_2Etyop_2Einteger_2Eint @ ( s @ tyop_2Einteger_2Eint @ ( c_2Einteger__word_2Ew2i_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ) ) )
= ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
thf(c_0_16,plain,
! [X24062: mono_2Etyop_2Einteger_2Eint] :
( ( mono_2Ec_2Einteger_2Eint__mul @ X24062 @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) )
= ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
thf(c_0_17,plain,
! [X3: u,X1: d] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2Eword__mul_2E2 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ X3 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
thf(c_0_18,negated_conjecture,
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ esk1_0 ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ) ) ) )
!= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ esk1_0 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
thf(c_0_19,plain,
! [X1: d] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1 ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_13,c_0_14]),c_0_15]),c_0_16]),c_0_17]) ).
thf(c_0_20,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18,c_0_19])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP015^4 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n007.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Tue Sep 29 19:27:56 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running higher-order theorem proving
% 6.36/6.46 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.GU6I0dsIO9/E---3.1_3803216.p
% 23.93/17.32 % Version: 3.5.1-ho
% 23.93/17.32 % partial match(2): HMLMSLSLSSSCHFA
% 23.93/17.32 % Preprocessing class: HMLLSLLLSSSCHFA.
% 23.93/17.32 % Scheduled 4 strats onto 8 cores with 292 seconds (2336 total)
% 23.93/17.32 % Starting new_ho_2 with 1168s (4) cores
% 23.93/17.32 % Starting sh3l with 584s (2) cores
% 23.93/17.32 % Starting lpo5_rw_fix with 292s (1) cores
% 23.93/17.32 % Starting full_lambda_7 with 292s (1) cores
% 23.93/17.32 % sh3l with pid 3803250 completed with status 0
% 23.93/17.32 % Result found by sh3l
% 23.93/17.32 % partial match(2): HMLMSLSLSSSCHFA
% 23.93/17.32 % Preprocessing class: HMLLSLLLSSSCHFA.
% 23.93/17.32 % Scheduled 4 strats onto 8 cores with 292 seconds (2336 total)
% 23.93/17.32 % Starting new_ho_2 with 1168s (4) cores
% 23.93/17.32 % Starting sh3l with 584s (2) cores
% 23.93/17.32 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 0, sine = gf120_gu_RUU_F100_L01000)
% 23.93/17.32 % SinE strategy is gf120_gu_RUU_F100_L01000
% 23.93/17.32 % Search class: HGHSM-SMLM33-DHFFFSBC
% 23.93/17.32 % partial match(1): HGHSM-SMLM33-MHFFFSBC
% 23.93/17.32 % Scheduled 7 strats onto 2 cores with 584 seconds (584 total)
% 23.93/17.32 % Starting SubtermCWHack with 53s (1) cores
% 23.93/17.32 % Starting sh3l with 59s (1) cores
% 23.93/17.32 % sh3l with pid 3803254 completed with status 0
% 23.93/17.32 % Result found by sh3l
% 23.93/17.32 % partial match(2): HMLMSLSLSSSCHFA
% 23.93/17.32 % Preprocessing class: HMLLSLLLSSSCHFA.
% 23.93/17.32 % Scheduled 4 strats onto 8 cores with 292 seconds (2336 total)
% 23.93/17.32 % Starting new_ho_2 with 1168s (4) cores
% 23.93/17.32 % Starting sh3l with 584s (2) cores
% 23.93/17.32 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 0, sine = gf120_gu_RUU_F100_L01000)
% 23.93/17.32 % SinE strategy is gf120_gu_RUU_F100_L01000
% 23.93/17.32 % Search class: HGHSM-SMLM33-DHFFFSBC
% 23.93/17.32 % partial match(1): HGHSM-SMLM33-MHFFFSBC
% 23.93/17.32 % Scheduled 7 strats onto 2 cores with 584 seconds (584 total)
% 23.93/17.32 % Starting SubtermCWHack with 53s (1) cores
% 23.93/17.32 % Starting sh3l with 59s (1) cores
% 23.93/17.32 % Preprocessing time : 0.125 s
% 23.93/17.32 % Presaturation interreduction done
% 23.93/17.32
% 23.93/17.32 % Proof found!
% 23.93/17.32 % SZS status Theorem
% 23.93/17.32 % SZS output start CNFRefutation
% See solution above
% 23.93/17.33 % Parsed axioms : 48436
% 23.93/17.33 % Removed by relevancy pruning/SinE : 47435
% 23.93/17.33 % Initial clauses : 2347
% 23.93/17.33 % Removed in clause preprocessing : 197
% 23.93/17.33 % Initial clauses in saturation : 2150
% 23.93/17.33 % Processed clauses : 3533
% 23.93/17.33 % ...of these trivial : 255
% 23.93/17.33 % ...subsumed : 668
% 23.93/17.33 % ...remaining for further processing : 2610
% 23.93/17.33 % Other redundant clauses eliminated : 231
% 23.93/17.33 % Clauses deleted for lack of memory : 0
% 23.93/17.33 % Backward-subsumed : 17
% 23.93/17.33 % Backward-rewritten : 37
% 23.93/17.33 % Generated clauses : 21166
% 23.93/17.33 % ...of the previous two non-redundant : 16027
% 23.93/17.33 % ...aggressively subsumed : 0
% 23.93/17.33 % Contextual simplify-reflections : 16
% 23.93/17.33 % Paramodulations : 20289
% 23.93/17.33 % Factorizations : 12
% 23.93/17.33 % NegExts : 0
% 23.93/17.33 % Equation resolutions : 320
% 23.93/17.33 % Disequality decompositions : 0
% 23.93/17.33 % Total rewrite steps : 11784
% 23.93/17.33 % ...of those cached : 9558
% 23.93/17.33 % Propositional unsat checks : 0
% 23.93/17.33 % Propositional check models : 0
% 23.93/17.33 % Propositional check unsatisfiable : 0
% 23.93/17.33 % Propositional clauses : 0
% 23.93/17.33 % Propositional clauses after purity: 0
% 23.93/17.33 % Propositional unsat core size : 0
% 23.93/17.33 % Propositional preprocessing time : 0.000
% 23.93/17.33 % Propositional encoding time : 0.000
% 23.93/17.33 % Propositional solver time : 0.000
% 23.93/17.33 % Success case prop preproc time : 0.000
% 23.93/17.33 % Success case prop encoding time : 0.000
% 23.93/17.33 % Success case prop solver time : 0.000
% 23.93/17.33 % Current number of processed clauses : 846
% 23.93/17.33 % Positive orientable unit clauses : 197
% 23.93/17.33 % Positive unorientable unit clauses: 6
% 23.93/17.33 % Negative unit clauses : 65
% 23.93/17.33 % Non-unit-clauses : 578
% 23.93/17.33 % Current number of unprocessed clauses: 16226
% 23.93/17.33 % ...number of literals in the above : 41907
% 23.93/17.33 % Current number of archived formulas : 0
% 23.93/17.33 % Current number of archived clauses : 1656
% 23.93/17.33 % Clause-clause subsumption calls (NU) : 1752673
% 23.93/17.33 % Rec. Clause-clause subsumption calls : 222672
% 23.93/17.33 % Non-unit clause-clause subsumptions : 312
% 23.93/17.33 % Unit Clause-clause subsumption calls : 9273
% 23.93/17.33 % Rewrite failures with RHS unbound : 14
% 23.93/17.33 % BW rewrite match attempts : 2768
% 23.93/17.33 % BW rewrite match successes : 207
% 23.93/17.33 % Condensation attempts : 0
% 23.93/17.33 % Condensation successes : 0
% 23.93/17.33 % Termbank termtop insertions : 3881090
% 23.93/17.33 % Search garbage collected termcells : 408995
% 23.93/17.33
% 23.93/17.33 % -------------------------------------------------
% 23.93/17.33 % User time : 2.305 s
% 23.93/17.33 % System time : 0.154 s
% 23.93/17.33 % Total time : 2.459 s
% 23.93/17.33 % Maximum resident set size: 101604 pages
% 23.93/17.33
% 23.93/17.33 % -------------------------------------------------
% 23.93/17.33 % User time : 12.030 s
% 23.93/17.33 % System time : 0.469 s
% 23.93/17.33 % Total time : 12.498 s
% 23.93/17.33 % Maximum resident set size: 89060 pages
% 23.93/17.33 % E exiting
%------------------------------------------------------------------------------