%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP006_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 : n008.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:30 PM UTC 2026
% Result : Theorem 69.47s 20.58s
% Output : CNFRefutation 69.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 8
% Syntax : Number of formulae : 55 ( 17 unt; 0 typ; 0 def)
% Number of atoms : 393 ( 24 equ)
% Maximal formula atoms : 132 ( 7 avg)
% Number of connectives : 519 ( 181 ~; 182 |; 58 &)
% ( 20 <=>; 78 =>; 0 <=; 0 <~>)
% Maximal formula depth : 54 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 3 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-4 aty)
% Number of functors : 25 ( 25 usr; 7 con; 0-7 aty)
% Number of variables : 198 ( 0 sgn 186 !; 12 ?; 46 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
del: $tType ).
tff(decl_23,type,
bool: del ).
tff(decl_25,type,
arr: ( del * del ) > del ).
tff(decl_26,type,
mem: ( del * $i ) > $o ).
tff(decl_27,type,
ap: ( $i * $i ) > $i ).
tff(decl_30,type,
p: $i > $o ).
tff(decl_35,type,
c_2EquantHeuristics_2EGUESS__FORALL__GAP: ( del * del ) > $i ).
tff(decl_36,type,
c_2EquantHeuristics_2EGUESS__EXISTS__GAP: ( del * del ) > $i ).
tff(decl_37,type,
c_2EquantHeuristics_2EGUESS__FORALL__POINT: ( del * del ) > $i ).
tff(decl_38,type,
c_2EquantHeuristics_2EGUESS__EXISTS__POINT: ( del * del ) > $i ).
tff(decl_39,type,
c_2EquantHeuristics_2EGUESS__FORALL: ( del * del ) > $i ).
tff(decl_41,type,
c_2EquantHeuristics_2EGUESS__EXISTS: ( del * del ) > $i ).
tff(decl_42,type,
c_2Ebool_2EF: $i ).
tff(decl_54,type,
epred1_4: ( $i * ( $i * ( del * del ) ) ) > $o ).
tff(decl_59,type,
esk4_0: del ).
tff(decl_60,type,
esk5_0: del ).
tff(decl_61,type,
esk6_0: $i ).
tff(decl_62,type,
esk7_0: $i ).
tff(decl_63,type,
esk8_0: $i ).
tff(decl_64,type,
esk9_5: ( $i * ( del * ( del * ( $i * $i ) ) ) ) > $i ).
tff(decl_65,type,
esk10_4: ( del * ( del * ( $i * $i ) ) ) > $i ).
tff(decl_66,type,
esk11_5: ( $i * ( del * ( del * ( $i * $i ) ) ) ) > $i ).
tff(decl_67,type,
esk12_4: ( del * ( del * ( $i * $i ) ) ) > $i ).
tff(decl_68,type,
esk13_6: ( $i * ( $i * ( del * ( del * ( $i * $i ) ) ) ) ) > $i ).
tff(decl_69,type,
esk14_6: ( $i * ( $i * ( del * ( del * ( $i * $i ) ) ) ) ) > $i ).
tff(decl_70,type,
esk15_7: ( $i * ( $i * ( $i * ( del * ( del * ( $i * $i ) ) ) ) ) ) > $i ).
tff(decl_71,type,
esk16_6: ( $i * ( $i * ( del * ( del * ( $i * $i ) ) ) ) ) > $i ).
tff(decl_72,type,
esk17_7: ( $i * ( $i * ( $i * ( del * ( del * ( $i * $i ) ) ) ) ) ) > $i ).
tff(decl_73,type,
esk18_6: ( $i * ( $i * ( del * ( del * ( $i * $i ) ) ) ) ) > $i ).
fof(ax_false_p,axiom,
~ p(c_2Ebool_2EF),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_false_p) ).
tff(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT,conjecture,
! [X11: del,X12: del,X25] :
( mem(X25,arr(X12,X11))
=> ! [X26] :
( mem(X26,arr(X11,bool))
=> ! [X50] :
( mem(X50,arr(X11,bool))
=> ( ! [X51] :
( mem(X51,X11)
=> ( p(ap(X50,X51))
=> p(ap(X26,X51)) ) )
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X12,X11),X25),X26))
=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X12,X11),X25),X50)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT) ).
tff(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) ).
tff(ap_tp,axiom,
! [X1: del,X2: del,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) ).
tff(mem_c_2Ebool_2EF,axiom,
mem(c_2Ebool_2EF,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2EF) ).
tff(conj_thm_2EquantHeuristics_2EGUESS__REWRITES,axiom,
! [X11: del,X12: del,X25] :
( mem(X25,arr(X11,X12))
=> ! [X26] :
( mem(X26,arr(X12,bool))
=> ( ! [X41] :
( mem(X41,arr(X11,X12))
=> ! [X42] :
( mem(X42,arr(X12,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X11,X12),X41),X42))
<=> ! [X43] :
( mem(X43,X12)
=> ( ~ p(ap(X42,X43))
=> ? [X44] :
( ( X43 = ap(X41,X44) )
& mem(X44,X11) ) ) ) ) ) )
& ! [X37] :
( mem(X37,arr(X11,X12))
=> ! [X38] :
( mem(X38,arr(X12,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X11,X12),X37),X38))
<=> ! [X39] :
( mem(X39,X12)
=> ( p(ap(X38,X39))
=> ? [X40] :
( ( X39 = ap(X37,X40) )
& mem(X40,X11) ) ) ) ) ) )
& ! [X34] :
( mem(X34,arr(X11,X12))
=> ! [X35] :
( mem(X35,arr(X12,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X11,X12),X34),X35))
<=> ! [X36] :
( mem(X36,X11)
=> ~ p(ap(X35,ap(X34,X36))) ) ) ) )
& ! [X31] :
( mem(X31,arr(X11,X12))
=> ! [X32] :
( mem(X32,arr(X12,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X11,X12),X31),X32))
<=> ! [X33] :
( mem(X33,X11)
=> p(ap(X32,ap(X31,X33))) ) ) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X11,X12),X25),X26))
<=> ! [X29] :
( mem(X29,X12)
=> ( ~ p(ap(X26,X29))
=> ? [X30] :
( ~ p(ap(X26,ap(X25,X30)))
& mem(X30,X11) ) ) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X11,X12),X25),X26))
<=> ! [X27] :
( mem(X27,X12)
=> ( p(ap(X26,X27))
=> ? [X28] :
( p(ap(X26,ap(X25,X28)))
& mem(X28,X11) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2EquantHeuristics_2EGUESS__REWRITES) ).
tff(mem_c_2EquantHeuristics_2EGUESS__FORALL__POINT,axiom,
! [X11: del,X12: del] : mem(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X11,X12),arr(arr(X11,X12),arr(arr(X12,bool),bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2EquantHeuristics_2EGUESS__FORALL__POINT) ).
fof(c_0_7,plain,
~ p(c_2Ebool_2EF),
inference(fof_simplification,[status(thm)],[ax_false_p]) ).
tff(c_0_8,negated_conjecture,
~ ! [X11: del,X12: del,X25] :
( mem(X25,arr(X12,X11))
=> ! [X26] :
( mem(X26,arr(X11,bool))
=> ! [X50] :
( mem(X50,arr(X11,bool))
=> ( ! [X51] :
( mem(X51,X11)
=> ( p(ap(X50,X51))
=> p(ap(X26,X51)) ) )
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X12,X11),X25),X26))
=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X12,X11),X25),X50)) ) ) ) ) ),
inference(assume_negation,[status(cth)],[conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT]) ).
tff(c_0_9,plain,
! [X56,X57] :
( ( ~ mem(X56,bool)
| ~ mem(X57,bool)
| ( X56 = X57 )
| p(X57)
| p(X56) )
& ( ~ mem(X56,bool)
| ~ mem(X57,bool)
| ( X56 = X57 )
| ~ p(X57)
| ~ p(X56) ) ),
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_10,plain,
~ p(c_2Ebool_2EF),
inference(fof_nnf,[status(thm)],[c_0_7]) ).
tff(c_0_11,plain,
! [X52: del,X53: del,X54,X55] :
( mem(ap(X54,X55),X53)
| ~ mem(X55,X52)
| ~ mem(X54,arr(X52,X53)) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ap_tp])])])]) ).
tff(c_0_12,negated_conjecture,
! [X153] :
( ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(esk5_0,esk4_0),esk6_0),esk8_0))
& p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(esk5_0,esk4_0),esk6_0),esk7_0))
& ( p(ap(esk7_0,X153))
| ~ p(ap(esk8_0,X153))
| ~ mem(X153,esk4_0) )
& mem(esk8_0,arr(esk4_0,bool))
& mem(esk7_0,arr(esk4_0,bool))
& mem(esk6_0,arr(esk5_0,esk4_0)) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_8])])])])]) ).
tff(c_0_13,plain,
! [X26,X25,X12: del,X11: del] :
( epred1_4(X11,X12,X25,X26)
<=> ( ! [X41] :
( mem(X41,arr(X11,X12))
=> ! [X42] :
( mem(X42,arr(X12,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X11,X12),X41),X42))
<=> ! [X43] :
( mem(X43,X12)
=> ( ~ p(ap(X42,X43))
=> ? [X44] :
( ( X43 = ap(X41,X44) )
& mem(X44,X11) ) ) ) ) ) )
& ! [X37] :
( mem(X37,arr(X11,X12))
=> ! [X38] :
( mem(X38,arr(X12,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X11,X12),X37),X38))
<=> ! [X39] :
( mem(X39,X12)
=> ( p(ap(X38,X39))
=> ? [X40] :
( ( X39 = ap(X37,X40) )
& mem(X40,X11) ) ) ) ) ) )
& ! [X34] :
( mem(X34,arr(X11,X12))
=> ! [X35] :
( mem(X35,arr(X12,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X11,X12),X34),X35))
<=> ! [X36] :
( mem(X36,X11)
=> ~ p(ap(X35,ap(X34,X36))) ) ) ) )
& ! [X31] :
( mem(X31,arr(X11,X12))
=> ! [X32] :
( mem(X32,arr(X12,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X11,X12),X31),X32))
<=> ! [X33] :
( mem(X33,X11)
=> p(ap(X32,ap(X31,X33))) ) ) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X11,X12),X25),X26))
<=> ! [X29] :
( mem(X29,X12)
=> ( ~ p(ap(X26,X29))
=> ? [X30] :
( ~ p(ap(X26,ap(X25,X30)))
& mem(X30,X11) ) ) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X11,X12),X25),X26))
<=> ! [X27] :
( mem(X27,X12)
=> ( p(ap(X26,X27))
=> ? [X28] :
( p(ap(X26,ap(X25,X28)))
& mem(X28,X11) ) ) ) ) ) ),
introduced(definition) ).
tcf(c_0_14,plain,
! [X4,X3] :
( ~ mem(X3,bool)
| ~ mem(X4,bool)
| ( X3 = X4 )
| p(X4)
| p(X3) ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
tcf(c_0_15,plain,
mem(c_2Ebool_2EF,bool),
inference(split_conjunct,[status(thm)],[mem_c_2Ebool_2EF]) ).
cnf(c_0_16,plain,
~ p(c_2Ebool_2EF),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
tcf(c_0_17,plain,
! [X2: del,X4,X3,X1: del] :
( ~ mem(X4,X1)
| ~ mem(X3,arr(X1,X2))
| mem(ap(X3,X4),X2) ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
tcf(c_0_18,negated_conjecture,
mem(esk8_0,arr(esk4_0,bool)),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
tff(c_0_19,plain,
! [X26,X25,X12: del,X11: del] :
( epred1_4(X11,X12,X25,X26)
=> ( ! [X41] :
( mem(X41,arr(X11,X12))
=> ! [X42] :
( mem(X42,arr(X12,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X11,X12),X41),X42))
<=> ! [X43] :
( mem(X43,X12)
=> ( ~ p(ap(X42,X43))
=> ? [X44] :
( ( X43 = ap(X41,X44) )
& mem(X44,X11) ) ) ) ) ) )
& ! [X37] :
( mem(X37,arr(X11,X12))
=> ! [X38] :
( mem(X38,arr(X12,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X11,X12),X37),X38))
<=> ! [X39] :
( mem(X39,X12)
=> ( p(ap(X38,X39))
=> ? [X40] :
( ( X39 = ap(X37,X40) )
& mem(X40,X11) ) ) ) ) ) )
& ! [X34] :
( mem(X34,arr(X11,X12))
=> ! [X35] :
( mem(X35,arr(X12,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X11,X12),X34),X35))
<=> ! [X36] :
( mem(X36,X11)
=> ~ p(ap(X35,ap(X34,X36))) ) ) ) )
& ! [X31] :
( mem(X31,arr(X11,X12))
=> ! [X32] :
( mem(X32,arr(X12,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X11,X12),X31),X32))
<=> ! [X33] :
( mem(X33,X11)
=> p(ap(X32,ap(X31,X33))) ) ) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X11,X12),X25),X26))
<=> ! [X29] :
( mem(X29,X12)
=> ( ~ p(ap(X26,X29))
=> ? [X30] :
( ~ p(ap(X26,ap(X25,X30)))
& mem(X30,X11) ) ) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X11,X12),X25),X26))
<=> ! [X27] :
( mem(X27,X12)
=> ( p(ap(X26,X27))
=> ? [X28] :
( p(ap(X26,ap(X25,X28)))
& mem(X28,X11) ) ) ) ) ) ),
inference(split_equiv,[status(thm)],[c_0_13]) ).
tcf(c_0_20,negated_conjecture,
mem(esk6_0,arr(esk5_0,esk4_0)),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
tcf(c_0_21,plain,
! [X3] :
( ~ mem(X3,bool)
| p(X3)
| ( X3 = c_2Ebool_2EF ) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_14,c_0_15]),c_0_16]) ).
tcf(c_0_22,negated_conjecture,
! [X3] :
( ~ mem(X3,esk4_0)
| mem(ap(esk8_0,X3),bool) ),
inference(spm,[status(thm)],[c_0_17,c_0_18]) ).
tff(c_0_23,plain,
! [X154,X155,X156: del,X157: del,X158,X161,X162,X165,X166,X167,X168,X170,X171,X172,X174,X175,X176,X179,X180,X181,X182,X185] :
( ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X180,arr(X157,X156))
| ~ mem(X181,arr(X156,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X157,X156),X180),X181))
| ( esk18_6(X154,X155,X156,X157,X180,X181) != ap(X180,X185) )
| ~ mem(X185,X157) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X180,arr(X157,X156))
| ~ mem(X181,arr(X156,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X157,X156),X180),X181))
| ~ p(ap(X181,esk18_6(X154,X155,X156,X157,X180,X181))) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X180,arr(X157,X156))
| ~ mem(X181,arr(X156,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X157,X156),X180),X181))
| mem(esk18_6(X154,X155,X156,X157,X180,X181),X156) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X180,arr(X157,X156))
| ~ mem(X181,arr(X156,bool))
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X157,X156),X180),X181))
| ~ mem(X182,X156)
| p(ap(X181,X182))
| ( X182 = ap(X180,esk17_7(X154,X155,X156,X157,X180,X181,X182)) ) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X180,arr(X157,X156))
| ~ mem(X181,arr(X156,bool))
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X157,X156),X180),X181))
| ~ mem(X182,X156)
| p(ap(X181,X182))
| mem(esk17_7(X154,X155,X156,X157,X180,X181,X182),X157) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X174,arr(X157,X156))
| ~ mem(X175,arr(X156,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X157,X156),X174),X175))
| ( esk16_6(X154,X155,X156,X157,X174,X175) != ap(X174,X179) )
| ~ mem(X179,X157) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X174,arr(X157,X156))
| ~ mem(X175,arr(X156,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X157,X156),X174),X175))
| p(ap(X175,esk16_6(X154,X155,X156,X157,X174,X175))) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X174,arr(X157,X156))
| ~ mem(X175,arr(X156,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X157,X156),X174),X175))
| mem(esk16_6(X154,X155,X156,X157,X174,X175),X156) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X174,arr(X157,X156))
| ~ mem(X175,arr(X156,bool))
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X157,X156),X174),X175))
| ~ mem(X176,X156)
| ~ p(ap(X175,X176))
| ( X176 = ap(X174,esk15_7(X154,X155,X156,X157,X174,X175,X176)) ) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X174,arr(X157,X156))
| ~ mem(X175,arr(X156,bool))
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X157,X156),X174),X175))
| ~ mem(X176,X156)
| ~ p(ap(X175,X176))
| mem(esk15_7(X154,X155,X156,X157,X174,X175,X176),X157) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X170,arr(X157,X156))
| ~ mem(X171,arr(X156,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X157,X156),X170),X171))
| p(ap(X171,ap(X170,esk14_6(X154,X155,X156,X157,X170,X171)))) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X170,arr(X157,X156))
| ~ mem(X171,arr(X156,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X157,X156),X170),X171))
| mem(esk14_6(X154,X155,X156,X157,X170,X171),X157) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X170,arr(X157,X156))
| ~ mem(X171,arr(X156,bool))
| ~ p(ap(X171,ap(X170,X172)))
| ~ mem(X172,X157)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X157,X156),X170),X171)) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X166,arr(X157,X156))
| ~ mem(X167,arr(X156,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X157,X156),X166),X167))
| ~ p(ap(X167,ap(X166,esk13_6(X154,X155,X156,X157,X166,X167)))) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X166,arr(X157,X156))
| ~ mem(X167,arr(X156,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X157,X156),X166),X167))
| mem(esk13_6(X154,X155,X156,X157,X166,X167),X157) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ mem(X166,arr(X157,X156))
| ~ mem(X167,arr(X156,bool))
| p(ap(X167,ap(X166,X168)))
| ~ mem(X168,X157)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X157,X156),X166),X167)) )
& ( ~ epred1_4(X157,X156,X155,X154)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X157,X156),X155),X154))
| p(ap(X154,ap(X155,X165)))
| ~ mem(X165,X157) )
& ( ~ epred1_4(X157,X156,X155,X154)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X157,X156),X155),X154))
| ~ p(ap(X154,esk12_4(X154,X155,X156,X157))) )
& ( ~ epred1_4(X157,X156,X155,X154)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X157,X156),X155),X154))
| mem(esk12_4(X154,X155,X156,X157),X156) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X157,X156),X155),X154))
| ~ mem(X162,X156)
| p(ap(X154,X162))
| ~ p(ap(X154,ap(X155,esk11_5(X154,X155,X156,X157,X162)))) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X157,X156),X155),X154))
| ~ mem(X162,X156)
| p(ap(X154,X162))
| mem(esk11_5(X154,X155,X156,X157,X162),X157) )
& ( ~ epred1_4(X157,X156,X155,X154)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X157,X156),X155),X154))
| ~ p(ap(X154,ap(X155,X161)))
| ~ mem(X161,X157) )
& ( ~ epred1_4(X157,X156,X155,X154)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X157,X156),X155),X154))
| p(ap(X154,esk10_4(X154,X155,X156,X157))) )
& ( ~ epred1_4(X157,X156,X155,X154)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X157,X156),X155),X154))
| mem(esk10_4(X154,X155,X156,X157),X156) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X157,X156),X155),X154))
| ~ mem(X158,X156)
| ~ p(ap(X154,X158))
| p(ap(X154,ap(X155,esk9_5(X154,X155,X156,X157,X158)))) )
& ( ~ epred1_4(X157,X156,X155,X154)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X157,X156),X155),X154))
| ~ mem(X158,X156)
| ~ p(ap(X154,X158))
| mem(esk9_5(X154,X155,X156,X157,X158),X157) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_19])])])])])]) ).
tcf(c_0_24,negated_conjecture,
! [X3] :
( ~ p(ap(esk8_0,X3))
| ~ mem(X3,esk4_0)
| p(ap(esk7_0,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
tcf(c_0_25,negated_conjecture,
! [X3] :
( ~ mem(X3,esk5_0)
| mem(ap(esk6_0,X3),esk4_0) ),
inference(spm,[status(thm)],[c_0_17,c_0_20]) ).
tcf(c_0_26,negated_conjecture,
! [X3] :
( ~ mem(X3,esk4_0)
| p(ap(esk8_0,X3))
| ( ap(esk8_0,X3) = c_2Ebool_2EF ) ),
inference(spm,[status(thm)],[c_0_21,c_0_22]) ).
tcf(c_0_27,plain,
! [X1: del,X2: del,X4,X3,X5,X6,X7] :
( ~ epred1_4(X1,X2,X6,X7)
| ~ mem(X3,arr(X1,X2))
| ~ mem(X4,arr(X2,bool))
| ~ p(ap(X4,ap(X3,X5)))
| ~ mem(X5,X1)
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X2),X3),X4)) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
tcf(c_0_28,negated_conjecture,
p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(esk5_0,esk4_0),esk6_0),esk7_0)),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
tcf(c_0_29,negated_conjecture,
mem(esk7_0,arr(esk4_0,bool)),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
tcf(c_0_30,negated_conjecture,
! [X3] :
( ~ mem(X3,esk5_0)
| ~ p(ap(esk8_0,ap(esk6_0,X3)))
| p(ap(esk7_0,ap(esk6_0,X3))) ),
inference(spm,[status(thm)],[c_0_24,c_0_25]) ).
tcf(c_0_31,negated_conjecture,
! [X3] :
( ~ mem(X3,esk5_0)
| p(ap(esk8_0,ap(esk6_0,X3)))
| ( ap(esk8_0,ap(esk6_0,X3)) = c_2Ebool_2EF ) ),
inference(spm,[status(thm)],[c_0_26,c_0_25]) ).
tff(c_0_32,plain,
! [X11: del,X12: del,X25] :
( mem(X25,arr(X11,X12))
=> ! [X26] :
( mem(X26,arr(X12,bool))
=> epred1_4(X11,X12,X25,X26) ) ),
inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[conj_thm_2EquantHeuristics_2EGUESS__REWRITES]),c_0_13]) ).
tcf(c_0_33,negated_conjecture,
! [X3,X4,X5] :
( ~ mem(X5,esk5_0)
| ~ p(ap(esk7_0,ap(esk6_0,X5)))
| ~ epred1_4(esk5_0,esk4_0,X3,X4) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27,c_0_28]),c_0_29]),c_0_20])]) ).
tcf(c_0_34,negated_conjecture,
! [X3] :
( ~ mem(X3,esk5_0)
| p(ap(esk7_0,ap(esk6_0,X3)))
| ( ap(esk8_0,ap(esk6_0,X3)) = c_2Ebool_2EF ) ),
inference(spm,[status(thm)],[c_0_30,c_0_31]) ).
tff(c_0_35,plain,
! [X123: del,X124: del,X125,X126] :
( epred1_4(X123,X124,X125,X126)
| ~ mem(X126,arr(X124,bool))
| ~ mem(X125,arr(X123,X124)) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_32])])])]) ).
tcf(c_0_36,negated_conjecture,
! [X5,X4,X3] :
( ~ mem(X3,esk5_0)
| ~ epred1_4(esk5_0,esk4_0,X4,X5)
| ( ap(esk8_0,ap(esk6_0,X3)) = c_2Ebool_2EF ) ),
inference(spm,[status(thm)],[c_0_33,c_0_34]) ).
tcf(c_0_37,plain,
! [X1: del,X4,X3,X2: del] :
( ~ mem(X4,arr(X2,bool))
| ~ mem(X3,arr(X1,X2))
| epred1_4(X1,X2,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
tcf(c_0_38,negated_conjecture,
! [X5,X4,X3] :
( ~ mem(X3,esk5_0)
| ~ mem(X5,arr(esk5_0,esk4_0))
| ~ mem(X4,arr(esk4_0,bool))
| ( ap(esk8_0,ap(esk6_0,X3)) = c_2Ebool_2EF ) ),
inference(spm,[status(thm)],[c_0_36,c_0_37]) ).
tff(c_0_39,plain,
! [X75: del,X76: del] : mem(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X75,X76),arr(arr(X75,X76),arr(arr(X76,bool),bool))),
inference(variable_rename,[status(thm)],[mem_c_2EquantHeuristics_2EGUESS__FORALL__POINT]) ).
tcf(c_0_40,negated_conjecture,
! [X4,X3] :
( ~ mem(X3,esk5_0)
| ~ mem(X4,arr(esk5_0,esk4_0))
| ( ap(esk8_0,ap(esk6_0,X3)) = c_2Ebool_2EF ) ),
inference(spm,[status(thm)],[c_0_38,c_0_18]) ).
tcf(c_0_41,plain,
! [X1: del,X2: del] : mem(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X2),arr(arr(X1,X2),arr(arr(X2,bool),bool))),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
tcf(c_0_42,plain,
! [X1: del,X3,X4,X2: del,X6,X5] :
( ~ epred1_4(X2,X1,X6,X5)
| ~ mem(X4,arr(X2,X1))
| ~ mem(X3,arr(X1,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X2,X1),X4),X3))
| p(ap(X3,ap(X4,esk14_6(X5,X6,X1,X2,X4,X3)))) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
tcf(c_0_43,negated_conjecture,
! [X3] :
( ~ mem(X3,esk5_0)
| ( ap(esk8_0,ap(esk6_0,X3)) = c_2Ebool_2EF ) ),
inference(spm,[status(thm)],[c_0_40,c_0_20]) ).
tcf(c_0_44,plain,
! [X1: del,X3,X2: del] :
( ~ mem(X3,arr(X1,X2))
| mem(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X2),X3),arr(arr(X2,bool),bool)) ),
inference(spm,[status(thm)],[c_0_17,c_0_41]) ).
tcf(c_0_45,plain,
! [X1: del,X4,X3,X2: del] :
( ~ mem(esk6_0,arr(X1,X2))
| ~ mem(esk8_0,arr(X2,bool))
| ~ mem(esk14_6(X4,X3,X2,X1,esk6_0,esk8_0),esk5_0)
| ~ epred1_4(X1,X2,X3,X4)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X2),esk6_0),esk8_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_43]),c_0_16]) ).
tcf(c_0_46,plain,
! [X1: del,X2: del,X6,X5,X4,X3] :
( ~ epred1_4(X2,X1,X4,X3)
| ~ mem(X5,arr(X2,X1))
| ~ mem(X6,arr(X1,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X2,X1),X5),X6))
| mem(esk14_6(X3,X4,X1,X2,X5,X6),X2) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
tcf(c_0_47,plain,
! [X1: del,X4,X3,X2: del] :
( ~ mem(X3,arr(X1,X2))
| ~ mem(X4,arr(X2,bool))
| mem(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X2),X3),X4),bool) ),
inference(spm,[status(thm)],[c_0_17,c_0_44]) ).
tcf(c_0_48,plain,
! [X4,X3,X1: del] :
( ~ mem(esk6_0,arr(esk5_0,X1))
| ~ mem(esk8_0,arr(X1,bool))
| ~ epred1_4(esk5_0,X1,X3,X4)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(esk5_0,X1),esk6_0),esk8_0)) ),
inference(spm,[status(thm)],[c_0_45,c_0_46]) ).
tcf(c_0_49,negated_conjecture,
~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(esk5_0,esk4_0),esk6_0),esk8_0)),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
tcf(c_0_50,plain,
! [X1: del,X4,X3,X2: del] :
( ~ mem(X3,arr(X1,X2))
| ~ mem(X4,arr(X2,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X2),X3),X4))
| ( ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X2),X3),X4) = c_2Ebool_2EF ) ),
inference(spm,[status(thm)],[c_0_21,c_0_47]) ).
tcf(c_0_51,plain,
! [X4,X3,X1: del] :
( ~ mem(X4,arr(esk5_0,X1))
| ~ mem(X3,arr(X1,bool))
| ~ mem(esk6_0,arr(esk5_0,X1))
| ~ mem(esk8_0,arr(X1,bool))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(esk5_0,X1),esk6_0),esk8_0)) ),
inference(spm,[status(thm)],[c_0_48,c_0_37]) ).
tcf(c_0_52,negated_conjecture,
ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(esk5_0,esk4_0),esk6_0),esk8_0) = c_2Ebool_2EF,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49,c_0_50]),c_0_18]),c_0_20])]) ).
tcf(c_0_53,negated_conjecture,
! [X3] : ~ mem(X3,arr(esk5_0,esk4_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_18]),c_0_52]),c_0_18]),c_0_20])]),c_0_16]) ).
cnf(c_0_54,negated_conjecture,
$false,
inference(sr,[status(thm)],[c_0_20,c_0_53]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP006_2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/10.38 % Computer : n008.cluster.edu
% 0.09/10.38 % Model : x86_64 x86_64
% 0.09/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.38 % Memory : 8046.5625MB
% 0.09/10.38 % OS : Linux 6.8.0-71-generic
% 0.09/10.38 % CPULimit : 300
% 0.09/10.38 % WCLimit : 300
% 0.09/10.38 % DateTime : Sun Sep 20 21:42:36 UTC 2026
% 0.09/10.38 % CPUTime :
% 0.09/10.38 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/10.42 Running first-order theorem proving
% 0.15/10.42 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
% 69.47/20.58 % Version: 3.5.1
% 69.47/20.58 % Preprocessing class: FSLSSMSMSSSNFFN.
% 69.47/20.58 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 69.47/20.58 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 69.47/20.58 % Starting new_bool_3 with 300s (1) cores
% 69.47/20.58 % Starting new_bool_1 with 300s (1) cores
% 69.47/20.58 % Starting sh5l with 300s (1) cores
% 69.47/20.58 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 3630891 completed with status 0
% 69.47/20.58 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 69.47/20.58 % Preprocessing class: FSLSSMSMSSSNFFN.
% 69.47/20.58 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 69.47/20.58 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 69.47/20.58 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 69.47/20.58 % No SInE strategy applied
% 69.47/20.58 % Search class: FGHSM-FFLM32-MFFFFFNN
% 69.47/20.58 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 69.47/20.58 % Starting SubtermCWHack with 136s (1) cores
% 69.47/20.58 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 69.47/20.58 % Starting G-E--_301_C18_F1_URBAN_S0Y with 136s (1) cores
% 69.47/20.58 % Starting new_bool_3 with 136s (1) cores
% 69.47/20.58 % Starting new_bool_1 with 136s (1) cores
% 69.47/20.58 % G-E--_301_C18_F1_URBAN_S0Y with pid 3630900 completed with status 0
% 69.47/20.58 % Result found by G-E--_301_C18_F1_URBAN_S0Y
% 69.47/20.58 % Preprocessing class: FSLSSMSMSSSNFFN.
% 69.47/20.58 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 69.47/20.58 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 69.47/20.58 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 69.47/20.58 % No SInE strategy applied
% 69.47/20.58 % Search class: FGHSM-FFLM32-MFFFFFNN
% 69.47/20.58 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 69.47/20.58 % Starting SubtermCWHack with 136s (1) cores
% 69.47/20.58 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 69.47/20.58 % Starting G-E--_301_C18_F1_URBAN_S0Y with 136s (1) cores
% 69.47/20.58 % Preprocessing time : 0.006 s
% 69.47/20.58
% 69.47/20.58 % Proof found!
% 69.47/20.58 % SZS status Theorem
% 69.47/20.58 % SZS output start CNFRefutation
% See solution above
% 69.47/20.58 % Parsed axioms : 91
% 69.47/20.58 % Removed by relevancy pruning/SinE : 0
% 69.47/20.58 % Initial clauses : 357
% 69.47/20.58 % Removed in clause preprocessing : 247
% 69.47/20.58 % Initial clauses in saturation : 110
% 69.47/20.58 % Processed clauses : 11733
% 69.47/20.58 % ...of these trivial : 48
% 69.47/20.58 % ...subsumed : 7528
% 69.47/20.58 % ...remaining for further processing : 4157
% 69.47/20.58 % Other redundant clauses eliminated : 1940
% 69.47/20.58 % Clauses deleted for lack of memory : 0
% 69.47/20.58 % Backward-subsumed : 232
% 69.47/20.58 % Backward-rewritten : 102
% 69.47/20.58 % Generated clauses : 258168
% 69.47/20.58 % ...of the previous two non-redundant : 240264
% 69.47/20.58 % ...aggressively subsumed : 0
% 69.47/20.58 % Contextual simplify-reflections : 60
% 69.47/20.58 % Paramodulations : 255623
% 69.47/20.58 % Factorizations : 563
% 69.47/20.58 % NegExts : 0
% 69.47/20.58 % Equation resolutions : 1981
% 69.47/20.58 % Disequality decompositions : 0
% 69.47/20.58 % Total rewrite steps : 105736
% 69.47/20.58 % ...of those cached : 104845
% 69.47/20.58 % Propositional unsat checks : 0
% 69.47/20.58 % Propositional check models : 0
% 69.47/20.58 % Propositional check unsatisfiable : 0
% 69.47/20.58 % Propositional clauses : 0
% 69.47/20.58 % Propositional clauses after purity: 0
% 69.47/20.58 % Propositional unsat core size : 0
% 69.47/20.58 % Propositional preprocessing time : 0.000
% 69.47/20.58 % Propositional encoding time : 0.000
% 69.47/20.58 % Propositional solver time : 0.000
% 69.47/20.58 % Success case prop preproc time : 0.000
% 69.47/20.58 % Success case prop encoding time : 0.000
% 69.47/20.58 % Success case prop solver time : 0.000
% 69.47/20.58 % Current number of processed clauses : 3821
% 69.47/20.58 % Positive orientable unit clauses : 282
% 69.47/20.58 % Positive unorientable unit clauses: 0
% 69.47/20.58 % Negative unit clauses : 4
% 69.47/20.58 % Non-unit-clauses : 3535
% 69.47/20.58 % Current number of unprocessed clauses: 226361
% 69.47/20.58 % ...number of literals in the above : 1117701
% 69.47/20.58 % Current number of archived formulas : 0
% 69.47/20.58 % Current number of archived clauses : 335
% 69.47/20.58 % Clause-clause subsumption calls (NU) : 1484683
% 69.47/20.58 % Rec. Clause-clause subsumption calls : 163067
% 69.47/20.58 % Non-unit clause-clause subsumptions : 4921
% 69.47/20.58 % Unit Clause-clause subsumption calls : 14327
% 69.47/20.58 % Rewrite failures with RHS unbound : 0
% 69.47/20.58 % BW rewrite match attempts : 4634
% 69.47/20.58 % BW rewrite match successes : 43
% 69.47/20.58 % Condensation attempts : 0
% 69.47/20.58 % Condensation successes : 0
% 69.47/20.58 % Termbank termtop insertions : 7153493
% 69.47/20.58 % Search garbage collected termcells : 3248
% 69.47/20.58
% 69.47/20.58 % -------------------------------------------------
% 69.47/20.58 % User time : 9.589 s
% 69.47/20.58 % System time : 0.275 s
% 69.47/20.58 % Total time : 9.863 s
% 69.47/20.58 % Maximum resident set size: 4268 pages
% 69.47/20.58
% 69.47/20.58 % -------------------------------------------------
% 69.47/20.58 % User time : 47.843 s
% 69.47/20.58 % System time : 1.844 s
% 69.47/20.58 % Total time : 49.687 s
% 69.47/20.58 % Maximum resident set size: 4864 pages
% 69.47/20.58 % E exiting
%------------------------------------------------------------------------------