%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP015+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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 : Thu Sep 24 12:53:41 PM UTC 2026
% Result : Theorem 0.56s 0.59s
% Output : CNFRefutation 0.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 18
% Syntax : Number of formulae : 71 ( 21 unt; 0 def)
% Number of atoms : 363 ( 70 equ)
% Maximal formula atoms : 96 ( 5 avg)
% Number of connectives : 494 ( 202 ~; 209 |; 29 &)
% ( 11 <=>; 43 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 5 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 6 ( 3 usr; 2 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 12 con; 0-2 aty)
% Number of variables : 112 ( 0 sgn 65 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(conj_thm_2Einteger_2EINT__LT__CALCULATE,axiom,
! [X26] :
( mem(X26,ty_2Enum_2Enum)
=> ! [X27] :
( mem(X27,ty_2Enum_2Enum)
=> ( ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X26)),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X27))))
<=> ~ $true )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X26))),ap(c_2Einteger_2Eint__of__num,X27)))
<=> ( X27 != c_2Enum_2E0
| X26 != c_2Enum_2E0 ) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X26))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X27))))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X27),X26)) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X26)),ap(c_2Einteger_2Eint__of__num,X27)))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X26),X27)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger_2EINT__LT__CALCULATE) ).
fof(ax_false_p,axiom,
~ p(c_2Ebool_2EF),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_false_p) ).
fof(boolext,axiom,
! [X5] :
( mem(X5,bool)
=> ! [X6] :
( mem(X6,bool)
=> ( ( p(X5)
<=> p(X6) )
=> X5 = X6 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',boolext) ).
fof(ap_tp,axiom,
! [X1,X2,X3] :
( mem(X3,arr(X1,X2))
=> ! [X4] :
( mem(X4,X1)
=> mem(ap(X3,X4),X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',ap_tp) ).
fof(conj_thm_2Einteger_2EINT__NEG__0,axiom,
ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger_2EINT__NEG__0) ).
fof(mem_c_2Enum_2E0,axiom,
mem(c_2Enum_2E0,ty_2Enum_2Enum),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Enum_2E0) ).
fof(mem_c_2Ebool_2EF,axiom,
mem(c_2Ebool_2EF,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2EF) ).
fof(mem_c_2Einteger_2Eint__lt,axiom,
mem(c_2Einteger_2Eint__lt,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Einteger_2Eint__lt) ).
fof(conj_thm_2Ebool_2ECOND__CONG,axiom,
! [X9] :
( ne(X9)
=> ! [X18] :
( mem(X18,bool)
=> ! [X19] :
( mem(X19,bool)
=> ! [X20] :
( mem(X20,X9)
=> ! [X21] :
( mem(X21,X9)
=> ! [X22] :
( mem(X22,X9)
=> ! [X23] :
( mem(X23,X9)
=> ( ( ( ~ p(X19)
=> X22 = X23 )
& ( p(X19)
=> X20 = X21 )
& ( p(X18)
<=> p(X19) ) )
=> ap(ap(ap(c_2Ebool_2ECOND(X9),X18),X20),X22) = ap(ap(ap(c_2Ebool_2ECOND(X9),X19),X21),X23) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ebool_2ECOND__CONG) ).
fof(ax_thm_2Einteger__word_2Ei2w__def,axiom,
! [X9] :
( ne(X9)
=> ! [X28] :
( mem(X28,ty_2Einteger_2Eint)
=> ap(c_2Einteger__word_2Ei2w(X9),X28) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X9)),ap(ap(c_2Einteger_2Eint__lt,X28),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Ewords_2Eword__2comp(X9),ap(c_2Ewords_2En2w(X9),ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__neg,X28))))),ap(c_2Ewords_2En2w(X9),ap(c_2Einteger_2ENum,X28))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_thm_2Einteger__word_2Ei2w__def) ).
fof(conj_thm_2Einteger_2ENUM__OF__INT,axiom,
! [X26] :
( mem(X26,ty_2Enum_2Enum)
=> ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,X26)) = X26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger_2ENUM__OF__INT) ).
fof(conj_thm_2Ebool_2Ebool__case__thm,axiom,
! [X9] :
( ne(X9)
=> ( ! [X24] :
( mem(X24,X9)
=> ! [X25] :
( mem(X25,X9)
=> ap(ap(ap(c_2Ebool_2ECOND(X9),c_2Ebool_2EF),X24),X25) = X25 ) )
& ! [X12] :
( mem(X12,X9)
=> ! [X13] :
( mem(X13,X9)
=> ap(ap(ap(c_2Ebool_2ECOND(X9),c_2Ebool_2ET),X12),X13) = X12 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ebool_2Ebool__case__thm) ).
fof(conj_thm_2Ewords_2EWORD__NEG__0,axiom,
! [X9] :
( ne(X9)
=> ap(c_2Ewords_2Eword__2comp(X9),ap(c_2Ewords_2En2w(X9),c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X9),c_2Enum_2E0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ewords_2EWORD__NEG__0) ).
fof(mem_c_2Ewords_2En2w,axiom,
! [X9] :
( ne(X9)
=> mem(c_2Ewords_2En2w(X9),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,X9))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ewords_2En2w) ).
fof(conj_thm_2Einteger__word_2Ei2w__0,conjecture,
! [X9] :
( ne(X9)
=> ap(c_2Einteger__word_2Ei2w(X9),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X9),c_2Enum_2E0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger__word_2Ei2w__0) ).
fof(ne_ty_2Efcp_2Ecart,axiom,
! [X10] :
( ne(X10)
=> ! [X11] :
( ne(X11)
=> ne(ty_2Efcp_2Ecart(X10,X11)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ne_ty_2Efcp_2Ecart) ).
fof(bool_ne,axiom,
ne(bool),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',bool_ne) ).
fof(mem_c_2Einteger_2Eint__of__num,axiom,
mem(c_2Einteger_2Eint__of__num,arr(ty_2Enum_2Enum,ty_2Einteger_2Eint)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Einteger_2Eint__of__num) ).
fof(c_0_18,plain,
! [X26] :
( mem(X26,ty_2Enum_2Enum)
=> ! [X27] :
( mem(X27,ty_2Enum_2Enum)
=> ( ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X26)),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X27))))
<=> ~ $true )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X26))),ap(c_2Einteger_2Eint__of__num,X27)))
<=> ( X27 != c_2Enum_2E0
| X26 != c_2Enum_2E0 ) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X26))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X27))))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X27),X26)) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X26)),ap(c_2Einteger_2Eint__of__num,X27)))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X26),X27)) ) ) ) ),
inference(fof_simplification,[status(thm)],[conj_thm_2Einteger_2EINT__LT__CALCULATE]) ).
fof(c_0_19,plain,
~ p(c_2Ebool_2EF),
inference(fof_simplification,[status(thm)],[ax_false_p]) ).
fof(c_0_20,plain,
! [X54,X55] :
( ( ~ mem(X54,ty_2Enum_2Enum)
| ~ mem(X55,ty_2Enum_2Enum)
| p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X54)),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X55))))
| $true )
& ( ~ mem(X54,ty_2Enum_2Enum)
| ~ mem(X55,ty_2Enum_2Enum)
| ~ $true
| ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X54)),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X55)))) )
& ( ~ mem(X54,ty_2Enum_2Enum)
| ~ mem(X55,ty_2Enum_2Enum)
| p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X54))),ap(c_2Einteger_2Eint__of__num,X55)))
| X55 = c_2Enum_2E0 )
& ( ~ mem(X54,ty_2Enum_2Enum)
| ~ mem(X55,ty_2Enum_2Enum)
| p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X54))),ap(c_2Einteger_2Eint__of__num,X55)))
| X54 = c_2Enum_2E0 )
& ( ~ mem(X54,ty_2Enum_2Enum)
| ~ mem(X55,ty_2Enum_2Enum)
| X55 != c_2Enum_2E0
| X54 != c_2Enum_2E0
| ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X54))),ap(c_2Einteger_2Eint__of__num,X55))) )
& ( ~ mem(X54,ty_2Enum_2Enum)
| ~ mem(X55,ty_2Enum_2Enum)
| p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X54))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X55))))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X55),X54)) )
& ( ~ mem(X54,ty_2Enum_2Enum)
| ~ mem(X55,ty_2Enum_2Enum)
| p(ap(ap(c_2Eprim__rec_2E_3C,X55),X54))
| ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X54))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X55)))) )
& ( ~ mem(X54,ty_2Enum_2Enum)
| ~ mem(X55,ty_2Enum_2Enum)
| p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X54)),ap(c_2Einteger_2Eint__of__num,X55)))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X54),X55)) )
& ( ~ mem(X54,ty_2Enum_2Enum)
| ~ mem(X55,ty_2Enum_2Enum)
| p(ap(ap(c_2Eprim__rec_2E_3C,X54),X55))
| ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X54)),ap(c_2Einteger_2Eint__of__num,X55))) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_18])])])])]) ).
fof(c_0_21,plain,
! [X72,X73] :
( ( ~ mem(X72,bool)
| ~ mem(X73,bool)
| X72 = X73
| p(X73)
| p(X72) )
& ( ~ mem(X72,bool)
| ~ mem(X73,bool)
| X72 = X73
| ~ p(X73)
| ~ p(X72) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[boolext])])])])]) ).
fof(c_0_22,plain,
~ p(c_2Ebool_2EF),
inference(fof_nnf,[status(thm)],[c_0_19]) ).
fof(c_0_23,plain,
! [X32,X33,X34,X35] :
( mem(ap(X34,X35),X33)
| ~ mem(X35,X32)
| ~ mem(X34,arr(X32,X33)) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ap_tp])])])]) ).
cnf(c_0_24,plain,
( ~ mem(X1,ty_2Enum_2Enum)
| ~ mem(X2,ty_2Enum_2Enum)
| X2 != c_2Enum_2E0
| X1 != c_2Enum_2E0
| ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1))),ap(c_2Einteger_2Eint__of__num,X2))) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
cnf(c_0_25,plain,
ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),
inference(split_conjunct,[status(thm)],[conj_thm_2Einteger_2EINT__NEG__0]) ).
cnf(c_0_26,plain,
mem(c_2Enum_2E0,ty_2Enum_2Enum),
inference(split_conjunct,[status(thm)],[mem_c_2Enum_2E0]) ).
cnf(c_0_27,plain,
( ~ mem(X1,bool)
| ~ mem(X2,bool)
| X1 = X2
| p(X2)
| p(X1) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_28,plain,
mem(c_2Ebool_2EF,bool),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2EF]) ).
cnf(c_0_29,plain,
~ p(c_2Ebool_2EF),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_30,plain,
( ~ mem(X4,X2)
| ~ mem(X1,arr(X2,X3))
| mem(ap(X1,X4),X3) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_31,plain,
mem(c_2Einteger_2Eint__lt,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool))),
inference(split_conjunct,[status(thm)],[mem_c_2Einteger_2Eint__lt]) ).
cnf(c_0_32,plain,
~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_24])]),c_0_25]),c_0_26])]) ).
cnf(c_0_33,plain,
( ~ mem(X1,bool)
| p(X1)
| X1 = c_2Ebool_2EF ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_27,c_0_28]),c_0_29]) ).
cnf(c_0_34,plain,
( ~ mem(X1,ty_2Einteger_2Eint)
| mem(ap(c_2Einteger_2Eint__lt,X1),arr(ty_2Einteger_2Eint,bool)) ),
inference(spm,[status(thm)],[c_0_30,c_0_31]) ).
fof(c_0_35,plain,
! [X9] :
( ne(X9)
=> ! [X18] :
( mem(X18,bool)
=> ! [X19] :
( mem(X19,bool)
=> ! [X20] :
( mem(X20,X9)
=> ! [X21] :
( mem(X21,X9)
=> ! [X22] :
( mem(X22,X9)
=> ! [X23] :
( mem(X23,X9)
=> ( ( ( ~ p(X19)
=> X22 = X23 )
& ( p(X19)
=> X20 = X21 )
& ( p(X18)
<=> p(X19) ) )
=> ap(ap(ap(c_2Ebool_2ECOND(X9),X18),X20),X22) = ap(ap(ap(c_2Ebool_2ECOND(X9),X19),X21),X23) ) ) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[conj_thm_2Ebool_2ECOND__CONG]) ).
fof(c_0_36,plain,
! [X43,X44] :
( ap(c_2Einteger__word_2Ei2w(X43),X44) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X43)),ap(ap(c_2Einteger_2Eint__lt,X44),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Ewords_2Eword__2comp(X43),ap(c_2Ewords_2En2w(X43),ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__neg,X44))))),ap(c_2Ewords_2En2w(X43),ap(c_2Einteger_2ENum,X44)))
| ~ mem(X44,ty_2Einteger_2Eint)
| ~ ne(X43) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_thm_2Einteger__word_2Ei2w__def])])])]) ).
cnf(c_0_37,plain,
( ~ mem(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),bool)
| ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = c_2Ebool_2EF ),
inference(spm,[status(thm)],[c_0_32,c_0_33]) ).
cnf(c_0_38,plain,
( ~ mem(X1,ty_2Einteger_2Eint)
| ~ mem(X2,ty_2Einteger_2Eint)
| mem(ap(ap(c_2Einteger_2Eint__lt,X1),X2),bool) ),
inference(spm,[status(thm)],[c_0_30,c_0_34]) ).
fof(c_0_39,plain,
! [X60,X61,X62,X63,X64,X65,X66] :
( ( ~ ne(X60)
| ~ mem(X61,bool)
| ~ mem(X62,bool)
| ~ mem(X63,X60)
| ~ mem(X64,X60)
| ~ mem(X65,X60)
| ~ mem(X66,X60)
| ap(ap(ap(c_2Ebool_2ECOND(X60),X61),X63),X65) = ap(ap(ap(c_2Ebool_2ECOND(X60),X62),X64),X66)
| p(X62)
| p(X61)
| X63 != X64
| X65 != X66 )
& ( ~ ne(X60)
| ~ mem(X61,bool)
| ~ mem(X62,bool)
| ~ mem(X63,X60)
| ~ mem(X64,X60)
| ~ mem(X65,X60)
| ~ mem(X66,X60)
| ap(ap(ap(c_2Ebool_2ECOND(X60),X61),X63),X65) = ap(ap(ap(c_2Ebool_2ECOND(X60),X62),X64),X66)
| p(X62)
| p(X61)
| X63 != X64
| ~ p(X62) )
& ( ~ ne(X60)
| ~ mem(X61,bool)
| ~ mem(X62,bool)
| ~ mem(X63,X60)
| ~ mem(X64,X60)
| ~ mem(X65,X60)
| ~ mem(X66,X60)
| ap(ap(ap(c_2Ebool_2ECOND(X60),X61),X63),X65) = ap(ap(ap(c_2Ebool_2ECOND(X60),X62),X64),X66)
| p(X62)
| p(X61)
| p(X62)
| X65 != X66 )
& ( ~ ne(X60)
| ~ mem(X61,bool)
| ~ mem(X62,bool)
| ~ mem(X63,X60)
| ~ mem(X64,X60)
| ~ mem(X65,X60)
| ~ mem(X66,X60)
| ap(ap(ap(c_2Ebool_2ECOND(X60),X61),X63),X65) = ap(ap(ap(c_2Ebool_2ECOND(X60),X62),X64),X66)
| p(X62)
| p(X61)
| p(X62)
| ~ p(X62) )
& ( ~ ne(X60)
| ~ mem(X61,bool)
| ~ mem(X62,bool)
| ~ mem(X63,X60)
| ~ mem(X64,X60)
| ~ mem(X65,X60)
| ~ mem(X66,X60)
| ap(ap(ap(c_2Ebool_2ECOND(X60),X61),X63),X65) = ap(ap(ap(c_2Ebool_2ECOND(X60),X62),X64),X66)
| ~ p(X62)
| ~ p(X61)
| X63 != X64
| X65 != X66 )
& ( ~ ne(X60)
| ~ mem(X61,bool)
| ~ mem(X62,bool)
| ~ mem(X63,X60)
| ~ mem(X64,X60)
| ~ mem(X65,X60)
| ~ mem(X66,X60)
| ap(ap(ap(c_2Ebool_2ECOND(X60),X61),X63),X65) = ap(ap(ap(c_2Ebool_2ECOND(X60),X62),X64),X66)
| ~ p(X62)
| ~ p(X61)
| X63 != X64
| ~ p(X62) )
& ( ~ ne(X60)
| ~ mem(X61,bool)
| ~ mem(X62,bool)
| ~ mem(X63,X60)
| ~ mem(X64,X60)
| ~ mem(X65,X60)
| ~ mem(X66,X60)
| ap(ap(ap(c_2Ebool_2ECOND(X60),X61),X63),X65) = ap(ap(ap(c_2Ebool_2ECOND(X60),X62),X64),X66)
| ~ p(X62)
| ~ p(X61)
| p(X62)
| X65 != X66 )
& ( ~ ne(X60)
| ~ mem(X61,bool)
| ~ mem(X62,bool)
| ~ mem(X63,X60)
| ~ mem(X64,X60)
| ~ mem(X65,X60)
| ~ mem(X66,X60)
| ap(ap(ap(c_2Ebool_2ECOND(X60),X61),X63),X65) = ap(ap(ap(c_2Ebool_2ECOND(X60),X62),X64),X66)
| ~ p(X62)
| ~ p(X61)
| p(X62)
| ~ p(X62) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_35])])])])]) ).
cnf(c_0_40,plain,
( ~ mem(X2,ty_2Einteger_2Eint)
| ~ ne(X1)
| ap(c_2Einteger__word_2Ei2w(X1),X2) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X1)),ap(ap(c_2Einteger_2Eint__lt,X2),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Ewords_2Eword__2comp(X1),ap(c_2Ewords_2En2w(X1),ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__neg,X2))))),ap(c_2Ewords_2En2w(X1),ap(c_2Einteger_2ENum,X2))) ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_41,plain,
( ~ mem(ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),ty_2Einteger_2Eint)
| ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = c_2Ebool_2EF ),
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
fof(c_0_42,plain,
! [X56] :
( ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,X56)) = X56
| ~ mem(X56,ty_2Enum_2Enum) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[conj_thm_2Einteger_2ENUM__OF__INT])])]) ).
fof(c_0_43,plain,
! [X67,X68,X69,X70,X71] :
( ( ~ ne(X67)
| ap(ap(ap(c_2Ebool_2ECOND(X67),c_2Ebool_2EF),X70),X71) = X71
| ~ mem(X71,X67)
| ~ mem(X70,X67) )
& ( ~ ne(X67)
| ap(ap(ap(c_2Ebool_2ECOND(X67),c_2Ebool_2ET),X68),X69) = X68
| ~ mem(X69,X67)
| ~ mem(X68,X67) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[conj_thm_2Ebool_2Ebool__case__thm])])])])]) ).
cnf(c_0_44,plain,
( ~ ne(X7)
| ~ mem(X5,bool)
| ~ mem(X6,bool)
| ~ mem(X3,X7)
| ~ mem(X4,X7)
| ~ mem(X1,X7)
| ~ mem(X2,X7)
| X3 != X4
| X1 != X2
| ap(ap(ap(c_2Ebool_2ECOND(X7),X5),X3),X1) = ap(ap(ap(c_2Ebool_2ECOND(X7),X6),X4),X2)
| p(X6)
| p(X5) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_45,plain,
( ~ ne(X1)
| ~ mem(ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),ty_2Einteger_2Eint)
| ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X1)),c_2Ebool_2EF),ap(c_2Ewords_2Eword__2comp(X1),ap(c_2Ewords_2En2w(X1),ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))))),ap(c_2Ewords_2En2w(X1),ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)))) = ap(c_2Einteger__word_2Ei2w(X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40,c_0_41]),c_0_25]) ).
cnf(c_0_46,plain,
( ~ mem(X1,ty_2Enum_2Enum)
| ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,X1)) = X1 ),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
fof(c_0_47,plain,
! [X58] :
( ap(c_2Ewords_2Eword__2comp(X58),ap(c_2Ewords_2En2w(X58),c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X58),c_2Enum_2E0)
| ~ ne(X58) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[conj_thm_2Ewords_2EWORD__NEG__0])])]) ).
cnf(c_0_48,plain,
( ~ ne(X2)
| ~ mem(X3,X2)
| ~ mem(X1,X2)
| ap(ap(ap(c_2Ebool_2ECOND(X2),c_2Ebool_2EF),X1),X3) = X3 ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_49,plain,
( ~ ne(X1)
| ~ mem(X4,X1)
| ~ mem(X3,X1)
| ~ mem(X2,bool)
| ~ mem(X5,bool)
| p(X2)
| p(X5)
| ap(ap(ap(c_2Ebool_2ECOND(X1),X2),X3),X4) = ap(ap(ap(c_2Ebool_2ECOND(X1),X5),X3),X4) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_44])]) ).
cnf(c_0_50,plain,
( ~ ne(X1)
| ~ mem(ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),ty_2Einteger_2Eint)
| ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X1)),c_2Ebool_2EF),ap(c_2Ewords_2Eword__2comp(X1),ap(c_2Ewords_2En2w(X1),c_2Enum_2E0))),ap(c_2Ewords_2En2w(X1),c_2Enum_2E0)) = ap(c_2Einteger__word_2Ei2w(X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45,c_0_46]),c_0_26])]) ).
cnf(c_0_51,plain,
( ~ ne(X1)
| ap(c_2Ewords_2Eword__2comp(X1),ap(c_2Ewords_2En2w(X1),c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X1),c_2Enum_2E0) ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
fof(c_0_52,plain,
! [X41] :
( mem(c_2Ewords_2En2w(X41),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,X41)))
| ~ ne(X41) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mem_c_2Ewords_2En2w])])]) ).
cnf(c_0_53,plain,
( ~ ne(X1)
| ~ mem(X3,X1)
| ~ mem(X4,X1)
| ~ mem(X2,bool)
| p(X2)
| ap(ap(ap(c_2Ebool_2ECOND(X1),X2),X3),X4) = X4 ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_49]),c_0_28])]),c_0_29]) ).
cnf(c_0_54,plain,
( ~ ne(X1)
| ~ mem(ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),ty_2Einteger_2Eint)
| ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X1)),c_2Ebool_2EF),ap(c_2Ewords_2En2w(X1),c_2Enum_2E0)),ap(c_2Ewords_2En2w(X1),c_2Enum_2E0)) = ap(c_2Einteger__word_2Ei2w(X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) ),
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
cnf(c_0_55,plain,
( ~ ne(X1)
| mem(c_2Ewords_2En2w(X1),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,X1))) ),
inference(split_conjunct,[status(thm)],[c_0_52]) ).
fof(c_0_56,negated_conjecture,
~ ! [X9] :
( ne(X9)
=> ap(c_2Einteger__word_2Ei2w(X9),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X9),c_2Enum_2E0) ),
inference(assume_negation,[status(cth)],[conj_thm_2Einteger__word_2Ei2w__0]) ).
cnf(c_0_57,plain,
( ~ ne(X1)
| ~ ne(ty_2Efcp_2Ecart(bool,X1))
| ~ mem(ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),ty_2Einteger_2Eint)
| ~ mem(ap(c_2Ewords_2En2w(X1),c_2Enum_2E0),ty_2Efcp_2Ecart(bool,X1))
| ap(c_2Einteger__word_2Ei2w(X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X1),c_2Enum_2E0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_54]),c_0_28])]),c_0_29]) ).
cnf(c_0_58,plain,
( ~ ne(X1)
| ~ mem(X2,ty_2Enum_2Enum)
| mem(ap(c_2Ewords_2En2w(X1),X2),ty_2Efcp_2Ecart(bool,X1)) ),
inference(spm,[status(thm)],[c_0_30,c_0_55]) ).
fof(c_0_59,plain,
! [X52,X53] :
( ne(ty_2Efcp_2Ecart(X52,X53))
| ~ ne(X53)
| ~ ne(X52) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ne_ty_2Efcp_2Ecart])])])]) ).
fof(c_0_60,negated_conjecture,
( ap(c_2Einteger__word_2Ei2w(esk1_0),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) != ap(c_2Ewords_2En2w(esk1_0),c_2Enum_2E0)
& ne(esk1_0) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_56])])])]) ).
cnf(c_0_61,plain,
( ~ ne(X1)
| ~ ne(ty_2Efcp_2Ecart(bool,X1))
| ~ mem(ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),ty_2Einteger_2Eint)
| ap(c_2Einteger__word_2Ei2w(X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X1),c_2Enum_2E0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_58]),c_0_26])]) ).
cnf(c_0_62,plain,
( ~ ne(X2)
| ~ ne(X1)
| ne(ty_2Efcp_2Ecart(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_59]) ).
cnf(c_0_63,plain,
ne(bool),
inference(split_conjunct,[status(thm)],[bool_ne]) ).
cnf(c_0_64,negated_conjecture,
ap(c_2Einteger__word_2Ei2w(esk1_0),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) != ap(c_2Ewords_2En2w(esk1_0),c_2Enum_2E0),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_65,plain,
( ~ ne(X1)
| ~ mem(ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),ty_2Einteger_2Eint)
| ap(c_2Einteger__word_2Ei2w(X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X1),c_2Enum_2E0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61,c_0_62]),c_0_63])]) ).
cnf(c_0_66,negated_conjecture,
ne(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_67,plain,
mem(c_2Einteger_2Eint__of__num,arr(ty_2Enum_2Enum,ty_2Einteger_2Eint)),
inference(split_conjunct,[status(thm)],[mem_c_2Einteger_2Eint__of__num]) ).
cnf(c_0_68,negated_conjecture,
~ mem(ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),ty_2Einteger_2Eint),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64,c_0_65]),c_0_66])]) ).
cnf(c_0_69,plain,
( ~ mem(X1,ty_2Enum_2Enum)
| mem(ap(c_2Einteger_2Eint__of__num,X1),ty_2Einteger_2Eint) ),
inference(spm,[status(thm)],[c_0_30,c_0_67]) ).
cnf(c_0_70,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68,c_0_69]),c_0_26])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP015+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.36 % Computer : n016.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 21:52:52 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.41 Running first-order theorem proving
% 0.13/0.41 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.56/0.59 % Version: 3.5.1
% 0.56/0.59 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.56/0.59 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.56/0.59 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.56/0.59 % Starting new_bool_3 with 300s (1) cores
% 0.56/0.59 % Starting new_bool_1 with 300s (1) cores
% 0.56/0.59 % Starting sh5l with 300s (1) cores
% 0.56/0.59 % new_bool_1 with pid 847694 completed with status 0
% 0.56/0.59 % Result found by new_bool_1
% 0.56/0.59 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.56/0.59 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.56/0.59 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.56/0.59 % Starting new_bool_3 with 300s (1) cores
% 0.56/0.59 % Starting new_bool_1 with 300s (1) cores
% 0.56/0.59 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.56/0.59 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.56/0.59 % Search class: FGHSF-FFMM31-DFFFFFNN
% 0.56/0.59 % partial match(1): FGHSF-FFMM31-SFFFFFNN
% 0.56/0.59 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 0.56/0.59 % Starting SubtermCWHack with 31s (1) cores
% 0.56/0.59 % SubtermCWHack with pid 847697 completed with status 0
% 0.56/0.59 % Result found by SubtermCWHack
% 0.56/0.59 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.56/0.59 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.56/0.59 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.56/0.59 % Starting new_bool_3 with 300s (1) cores
% 0.56/0.59 % Starting new_bool_1 with 300s (1) cores
% 0.56/0.59 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.56/0.59 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.56/0.59 % Search class: FGHSF-FFMM31-DFFFFFNN
% 0.56/0.59 % partial match(1): FGHSF-FFMM31-SFFFFFNN
% 0.56/0.59 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 0.56/0.59 % Starting SubtermCWHack with 31s (1) cores
% 0.56/0.59 % Preprocessing time : 0.002 s
% 0.56/0.59
% 0.56/0.59 % Proof found!
% 0.56/0.59 % SZS status Theorem
% 0.56/0.59 % SZS output start CNFRefutation
% See solution above
% 0.56/0.59 % Parsed axioms : 57
% 0.56/0.59 % Removed by relevancy pruning/SinE : 21
% 0.56/0.59 % Initial clauses : 69
% 0.56/0.59 % Removed in clause preprocessing : 24
% 0.56/0.59 % Initial clauses in saturation : 45
% 0.56/0.59 % Processed clauses : 942
% 0.56/0.59 % ...of these trivial : 0
% 0.56/0.59 % ...subsumed : 504
% 0.56/0.59 % ...remaining for further processing : 438
% 0.56/0.59 % Other redundant clauses eliminated : 8
% 0.56/0.59 % Clauses deleted for lack of memory : 0
% 0.56/0.59 % Backward-subsumed : 51
% 0.56/0.59 % Backward-rewritten : 4
% 0.56/0.59 % Generated clauses : 3349
% 0.56/0.59 % ...of the previous two non-redundant : 3046
% 0.56/0.59 % ...aggressively subsumed : 0
% 0.56/0.59 % Contextual simplify-reflections : 20
% 0.56/0.59 % Paramodulations : 3331
% 0.56/0.59 % Factorizations : 12
% 0.56/0.59 % NegExts : 0
% 0.56/0.59 % Equation resolutions : 9
% 0.56/0.59 % Disequality decompositions : 0
% 0.56/0.59 % Total rewrite steps : 1343
% 0.56/0.59 % ...of those cached : 1332
% 0.56/0.59 % Propositional unsat checks : 0
% 0.56/0.59 % Propositional check models : 0
% 0.56/0.59 % Propositional check unsatisfiable : 0
% 0.56/0.59 % Propositional clauses : 0
% 0.56/0.59 % Propositional clauses after purity: 0
% 0.56/0.59 % Propositional unsat core size : 0
% 0.56/0.59 % Propositional preprocessing time : 0.000
% 0.56/0.59 % Propositional encoding time : 0.000
% 0.56/0.59 % Propositional solver time : 0.000
% 0.56/0.59 % Success case prop preproc time : 0.000
% 0.56/0.59 % Success case prop encoding time : 0.000
% 0.56/0.59 % Success case prop solver time : 0.000
% 0.56/0.59 % Current number of processed clauses : 378
% 0.56/0.59 % Positive orientable unit clauses : 16
% 0.56/0.59 % Positive unorientable unit clauses: 0
% 0.56/0.59 % Negative unit clauses : 5
% 0.56/0.59 % Non-unit-clauses : 357
% 0.56/0.59 % Current number of unprocessed clauses: 2099
% 0.56/0.59 % ...number of literals in the above : 16176
% 0.56/0.59 % Current number of archived formulas : 0
% 0.56/0.59 % Current number of archived clauses : 55
% 0.56/0.59 % Clause-clause subsumption calls (NU) : 26323
% 0.56/0.59 % Rec. Clause-clause subsumption calls : 3384
% 0.56/0.59 % Non-unit clause-clause subsumptions : 485
% 0.56/0.59 % Unit Clause-clause subsumption calls : 174
% 0.56/0.59 % Rewrite failures with RHS unbound : 0
% 0.56/0.59 % BW rewrite match attempts : 7
% 0.56/0.59 % BW rewrite match successes : 2
% 0.56/0.59 % Condensation attempts : 0
% 0.56/0.59 % Condensation successes : 0
% 0.56/0.59 % Termbank termtop insertions : 127437
% 0.56/0.59 % Search garbage collected termcells : 1331
% 0.56/0.59
% 0.56/0.59 % -------------------------------------------------
% 0.56/0.59 % User time : 0.148 s
% 0.56/0.59 % System time : 0.011 s
% 0.56/0.59 % Total time : 0.159 s
% 0.56/0.59 % Maximum resident set size: 3980 pages
% 0.56/0.59
% 0.56/0.59 % -------------------------------------------------
% 0.56/0.59 % User time : 0.153 s
% 0.56/0.59 % System time : 0.014 s
% 0.56/0.59 % Total time : 0.167 s
% 0.56/0.59 % Maximum resident set size: 4608 pages
% 0.56/0.59 % E exiting
%------------------------------------------------------------------------------