%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET959+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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 02:12:55 PM UTC 2026
% Result : Theorem 0.10s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET959+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n009.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 05:45:42 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.40 % Refutation found
% 0.10/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.40 fof(f7,conjecture,(
% 0.10/0.40 (! [A,B] :( ( (! [C] :~ ( in(C,A)& (! [D,E] : C != ordered_pair(D,E) )))& (! [C] :~ ( in(C,B)& (! [D,E] : C != ordered_pair(D,E) )))& (! [C,D] :( in(ordered_pair(C,D),A)<=> in(ordered_pair(C,D),B) ) ))=> A = B ) )),
% 0.10/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f8,negated_conjecture,(
% 0.10/0.40 ~((! [A,B] :( ( (! [C] :~ ( in(C,A)& (! [D,E] : C != ordered_pair(D,E) )))& (! [C] :~ ( in(C,B)& (! [D,E] : C != ordered_pair(D,E) )))& (! [C,D] :( in(ordered_pair(C,D),A)<=> in(ordered_pair(C,D),B) ) ))=> A = B ) ))),
% 0.10/0.40 inference(negated_conjecture,[status(cth)],[f7])).
% 0.10/0.40 fof(f9,axiom,(
% 0.10/0.40 (! [A,B] :( (! [C] :( in(C,A)<=> in(C,B) ))=> A = B ) )),
% 0.10/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f19,plain,(
% 0.10/0.40 (?[A,B]: ((((![C]: (~in(C,A)|(?[D,E]: C=ordered_pair(D,E))))&(![C]: (~in(C,B)|(?[D,E]: C=ordered_pair(D,E)))))&(![C,D]: (in(ordered_pair(C,D),A)<=>in(ordered_pair(C,D),B))))&~A=B))),
% 0.10/0.40 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.10/0.40 fof(f20,plain,(
% 0.10/0.40 ?[A,B]: ((((![C]: (~in(C,A)|(?[D,E]: C=ordered_pair(D,E))))&(![C]: (~in(C,B)|(?[D,E]: C=ordered_pair(D,E)))))&(![C,D]: ((~in(ordered_pair(C,D),A)|in(ordered_pair(C,D),B))&(in(ordered_pair(C,D),A)|~in(ordered_pair(C,D),B)))))&~A=B)),
% 0.10/0.40 inference(NNF_transformation,[status(thm)],[f19])).
% 0.10/0.40 fof(f21,plain,(
% 0.10/0.40 ?[A,B]: ((((![C]: (~in(C,A)|(?[D,E]: C=ordered_pair(D,E))))&(![C]: (~in(C,B)|(?[D,E]: C=ordered_pair(D,E)))))&((![C,D]: (~in(ordered_pair(C,D),A)|in(ordered_pair(C,D),B)))&(![C,D]: (in(ordered_pair(C,D),A)|~in(ordered_pair(C,D),B)))))&~A=B)),
% 0.10/0.40 inference(miniscoping,[status(thm)],[f20])).
% 0.10/0.40 fof(f22,plain,(
% 0.10/0.40 ((((![C]: (~in(C,sK2_skl)|C=ordered_pair(sK4_skl(C),sK5_skl(C))))&(![C]: (~in(C,sK3_skl)|C=ordered_pair(sK6_skl(C),sK7_skl(C)))))&((![C,D]: (~in(ordered_pair(C,D),sK2_skl)|in(ordered_pair(C,D),sK3_skl)))&(![C,D]: (in(ordered_pair(C,D),sK2_skl)|~in(ordered_pair(C,D),sK3_skl)))))&~sK2_skl=sK3_skl)),
% 0.10/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl]),skolemize(A,sK2_skl),skolemize(B,sK3_skl),skolemize(D,sK4_skl(C)),skolemize(E,sK5_skl(C)),skolemize(D,sK6_skl(C)),skolemize(E,sK7_skl(C))],[f21])).
% 0.10/0.40 fof(f23,plain,(
% 0.10/0.40 ![X0]: (~in(X0,sK2_skl)|X0=ordered_pair(sK4_skl(X0),sK5_skl(X0)))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f22])).
% 0.10/0.40 fof(f24,plain,(
% 0.10/0.40 ![X0]: (~in(X0,sK3_skl)|X0=ordered_pair(sK6_skl(X0),sK7_skl(X0)))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f22])).
% 0.10/0.40 fof(f25,plain,(
% 0.10/0.40 ![X0,X1]: (~in(ordered_pair(X0,X1),sK2_skl)|in(ordered_pair(X0,X1),sK3_skl))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f22])).
% 0.10/0.40 fof(f26,plain,(
% 0.10/0.40 ![X0,X1]: (in(ordered_pair(X0,X1),sK2_skl)|~in(ordered_pair(X0,X1),sK3_skl))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f22])).
% 0.10/0.40 fof(f27,plain,(
% 0.10/0.40 ~sK2_skl=sK3_skl),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f22])).
% 0.10/0.40 fof(f28,plain,(
% 0.10/0.40 ![A,B]: ((?[C]: (in(C,A)<~>in(C,B)))|A=B)),
% 0.10/0.40 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.10/0.40 fof(f29,plain,(
% 0.10/0.40 ![A,B]: ((?[C]: ((in(C,A)|in(C,B))&(~in(C,A)|~in(C,B))))|A=B)),
% 0.10/0.40 inference(NNF_transformation,[status(thm)],[f28])).
% 0.10/0.40 fof(f30,plain,(
% 0.10/0.40 ![A,B]: (((in(sK8_skl(B,A),A)|in(sK8_skl(B,A),B))&(~in(sK8_skl(B,A),A)|~in(sK8_skl(B,A),B)))|A=B)),
% 0.10/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(C,sK8_skl(B,A))],[f29])).
% 0.10/0.40 fof(f31,plain,(
% 0.10/0.40 ![X0,X1]: (in(sK8_skl(X0,X1),X1)|in(sK8_skl(X0,X1),X0)|X1=X0)),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f30])).
% 0.10/0.40 fof(f32,plain,(
% 0.10/0.40 ![X0,X1]: (~in(sK8_skl(X0,X1),X1)|~in(sK8_skl(X0,X1),X0)|X1=X0)),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f30])).
% 0.10/0.40 fof(f34,plain,(
% 0.10/0.40 ![X0,X1]: (~in(ordered_pair(X0,X1),sK2_skl)|ordered_pair(X0,X1)=ordered_pair(sK6_skl(ordered_pair(X0,X1)),sK7_skl(ordered_pair(X0,X1))))),
% 0.10/0.40 inference(resolution,[status(thm)],[f25,f24])).
% 0.10/0.40 fof(f60,plain,(
% 0.10/0.40 ![X0]: (in(sK8_skl(X0,sK3_skl),X0)|sK3_skl=X0|sK8_skl(X0,sK3_skl)=ordered_pair(sK6_skl(sK8_skl(X0,sK3_skl)),sK7_skl(sK8_skl(X0,sK3_skl))))),
% 0.10/0.40 inference(resolution,[status(thm)],[f31,f24])).
% 0.10/0.40 fof(f95,plain,(
% 0.10/0.40 sK3_skl=sK2_skl|sK8_skl(sK2_skl,sK3_skl)=ordered_pair(sK6_skl(sK8_skl(sK2_skl,sK3_skl)),sK7_skl(sK8_skl(sK2_skl,sK3_skl)))|sK8_skl(sK2_skl,sK3_skl)=ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl)))),
% 0.10/0.40 inference(resolution,[status(thm)],[f60,f23])).
% 0.10/0.40 fof(f106,definition,(
% 0.10/0.40 sQ5_spl <=> (sK3_skl=sK2_skl)),
% 0.10/0.40 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.10/0.40 fof(f107,plain,(
% 0.10/0.40 sK3_skl=sK2_skl|~sQ5_spl),
% 0.10/0.40 inference(component_clause,[status(thm)],[f106])).
% 0.10/0.40 fof(f109,definition,(
% 0.10/0.40 sQ6_spl <=> (sK8_skl(sK2_skl,sK3_skl)=ordered_pair(sK6_skl(sK8_skl(sK2_skl,sK3_skl)),sK7_skl(sK8_skl(sK2_skl,sK3_skl))))),
% 0.10/0.40 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.10/0.40 fof(f110,plain,(
% 0.10/0.40 sK8_skl(sK2_skl,sK3_skl)=ordered_pair(sK6_skl(sK8_skl(sK2_skl,sK3_skl)),sK7_skl(sK8_skl(sK2_skl,sK3_skl)))|~sQ6_spl),
% 0.10/0.40 inference(component_clause,[status(thm)],[f109])).
% 0.10/0.40 fof(f111,plain,(
% 0.10/0.40 ~sK8_skl(sK2_skl,sK3_skl)=ordered_pair(sK6_skl(sK8_skl(sK2_skl,sK3_skl)),sK7_skl(sK8_skl(sK2_skl,sK3_skl)))|sQ6_spl),
% 0.10/0.40 inference(component_clause,[status(thm)],[f109])).
% 0.10/0.40 fof(f112,definition,(
% 0.10/0.40 sQ7_spl <=> (sK8_skl(sK2_skl,sK3_skl)=ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl))))),
% 0.10/0.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.10/0.40 fof(f113,plain,(
% 0.10/0.40 sK8_skl(sK2_skl,sK3_skl)=ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl)))|~sQ7_spl),
% 0.10/0.40 inference(component_clause,[status(thm)],[f112])).
% 0.10/0.40 fof(f115,plain,(
% 0.10/0.40 sQ5_spl|sQ6_spl|sQ7_spl),
% 0.10/0.40 inference(split_clause,[status(thm)],[f95,f106,f109,f112])).
% 0.10/0.40 fof(f139,plain,(
% 0.10/0.40 $false|~sQ5_spl),
% 0.10/0.40 inference(forward_subsumption_resolution,[status(thm)],[f107,f27])).
% 0.10/0.40 fof(f140,plain,(
% 0.10/0.40 ~sQ5_spl),
% 0.10/0.40 inference(contradiction_clause,[status(thm)],[f139])).
% 0.10/0.40 fof(f190,plain,(
% 0.10/0.40 in(ordered_pair(sK6_skl(sK8_skl(sK2_skl,sK3_skl)),sK7_skl(sK8_skl(sK2_skl,sK3_skl))),sK2_skl)|~in(sK8_skl(sK2_skl,sK3_skl),sK3_skl)|~sQ6_spl),
% 0.10/0.40 inference(paramodulation,[status(thm)],[f110,f26])).
% 0.10/0.40 fof(f192,plain,(
% 0.10/0.40 ~in(sK8_skl(sK2_skl,sK3_skl),sK2_skl)|in(ordered_pair(sK6_skl(sK8_skl(sK2_skl,sK3_skl)),sK7_skl(sK8_skl(sK2_skl,sK3_skl))),sK3_skl)|~sQ6_spl),
% 0.10/0.40 inference(paramodulation,[status(thm)],[f110,f25])).
% 0.10/0.40 fof(f193,definition,(
% 0.10/0.40 sQ11_spl <=> (in(sK8_skl(sK2_skl,sK3_skl),sK2_skl))),
% 0.10/0.40 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.10/0.40 fof(f195,plain,(
% 0.10/0.40 ~in(sK8_skl(sK2_skl,sK3_skl),sK2_skl)|sQ11_spl),
% 0.10/0.40 inference(component_clause,[status(thm)],[f193])).
% 0.10/0.40 fof(f204,definition,(
% 0.10/0.40 sQ14_spl <=> (in(ordered_pair(sK6_skl(sK8_skl(sK2_skl,sK3_skl)),sK7_skl(sK8_skl(sK2_skl,sK3_skl))),sK2_skl))),
% 0.10/0.40 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.10/0.40 fof(f205,plain,(
% 0.10/0.40 in(ordered_pair(sK6_skl(sK8_skl(sK2_skl,sK3_skl)),sK7_skl(sK8_skl(sK2_skl,sK3_skl))),sK2_skl)|~sQ14_spl),
% 0.10/0.40 inference(component_clause,[status(thm)],[f204])).
% 0.10/0.40 fof(f207,definition,(
% 0.10/0.40 sQ15_spl <=> (in(sK8_skl(sK2_skl,sK3_skl),sK3_skl))),
% 0.10/0.40 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.10/0.40 fof(f210,plain,(
% 0.10/0.40 sQ14_spl|~sQ15_spl|~sQ6_spl),
% 0.10/0.40 inference(split_clause,[status(thm)],[f190,f204,f207,f109])).
% 0.10/0.40 fof(f212,definition,(
% 0.10/0.40 sQ16_spl <=> (in(ordered_pair(sK6_skl(sK8_skl(sK2_skl,sK3_skl)),sK7_skl(sK8_skl(sK2_skl,sK3_skl))),sK3_skl))),
% 0.10/0.40 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.10/0.40 fof(f213,plain,(
% 0.10/0.40 in(ordered_pair(sK6_skl(sK8_skl(sK2_skl,sK3_skl)),sK7_skl(sK8_skl(sK2_skl,sK3_skl))),sK3_skl)|~sQ16_spl),
% 0.10/0.40 inference(component_clause,[status(thm)],[f212])).
% 0.10/0.40 fof(f215,plain,(
% 0.10/0.40 ~sQ11_spl|sQ16_spl|~sQ6_spl),
% 0.10/0.40 inference(split_clause,[status(thm)],[f192,f193,f212,f109])).
% 0.10/0.40 fof(f216,plain,(
% 0.10/0.40 in(sK8_skl(sK2_skl,sK3_skl),sK2_skl)|~sQ6_spl|~sQ14_spl),
% 0.10/0.40 inference(forward_demodulation,[status(thm)],[f110,f205])).
% 0.10/0.40 fof(f217,plain,(
% 0.10/0.40 sK3_skl=sK2_skl|sK8_skl(sK2_skl,sK3_skl)=ordered_pair(sK6_skl(sK8_skl(sK2_skl,sK3_skl)),sK7_skl(sK8_skl(sK2_skl,sK3_skl)))|sQ11_spl),
% 0.10/0.40 inference(resolution,[status(thm)],[f195,f60])).
% 0.10/0.40 fof(f219,plain,(
% 0.10/0.40 in(sK8_skl(sK2_skl,sK3_skl),sK3_skl)|sK3_skl=sK2_skl|sQ11_spl),
% 0.10/0.40 inference(resolution,[status(thm)],[f195,f31])).
% 0.10/0.40 fof(f220,plain,(
% 0.10/0.40 sQ5_spl|sQ6_spl|sQ11_spl),
% 0.10/0.40 inference(split_clause,[status(thm)],[f217,f106,f109,f193])).
% 0.10/0.40 fof(f225,plain,(
% 0.10/0.40 sQ15_spl|sQ5_spl|sQ11_spl),
% 0.10/0.40 inference(split_clause,[status(thm)],[f219,f207,f106,f193])).
% 0.10/0.40 fof(f230,plain,(
% 0.10/0.40 in(sK8_skl(sK2_skl,sK3_skl),sK3_skl)|~sQ6_spl|~sQ16_spl),
% 0.10/0.40 inference(forward_demodulation,[status(thm)],[f110,f213])).
% 0.10/0.40 fof(f262,plain,(
% 0.10/0.40 ~in(sK8_skl(sK2_skl,sK3_skl),sK2_skl)|sK3_skl=sK2_skl|~sQ6_spl|~sQ16_spl),
% 0.10/0.40 inference(resolution,[status(thm)],[f230,f32])).
% 0.10/0.40 fof(f266,plain,(
% 0.10/0.40 ~sQ11_spl|sQ5_spl|~sQ6_spl|~sQ16_spl),
% 0.10/0.40 inference(split_clause,[status(thm)],[f262,f193,f106,f109,f212])).
% 0.10/0.40 fof(f267,plain,(
% 0.10/0.40 sQ11_spl|~sQ6_spl|~sQ14_spl),
% 0.10/0.40 inference(split_clause,[status(thm)],[f216,f193,f109,f204])).
% 0.10/0.40 fof(f270,plain,(
% 0.10/0.40 ~in(sK8_skl(sK2_skl,sK3_skl),sK2_skl)|ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl)))=ordered_pair(sK6_skl(ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl)))),sK7_skl(ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl)))))|~sQ7_spl),
% 0.10/0.40 inference(paramodulation,[status(thm)],[f113,f34])).
% 0.10/0.40 fof(f278,definition,(
% 0.10/0.40 sQ25_spl <=> (ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl)))=ordered_pair(sK6_skl(ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl)))),sK7_skl(ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl))))))),
% 0.10/0.40 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.10/0.40 fof(f279,plain,(
% 0.10/0.40 ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl)))=ordered_pair(sK6_skl(ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl)))),sK7_skl(ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl)))))|~sQ25_spl),
% 0.10/0.40 inference(component_clause,[status(thm)],[f278])).
% 0.10/0.40 fof(f281,plain,(
% 0.10/0.40 ~sQ11_spl|sQ25_spl|~sQ7_spl),
% 0.10/0.40 inference(split_clause,[status(thm)],[f270,f193,f278,f112])).
% 0.10/0.40 fof(f292,plain,(
% 0.10/0.40 sK8_skl(sK2_skl,sK3_skl)=ordered_pair(sK6_skl(ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl)))),sK7_skl(ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl)))))|~sQ7_spl|~sQ25_spl),
% 0.10/0.40 inference(forward_demodulation,[status(thm)],[f113,f279])).
% 0.10/0.40 fof(f293,plain,(
% 0.10/0.40 sK8_skl(sK2_skl,sK3_skl)=ordered_pair(sK6_skl(sK8_skl(sK2_skl,sK3_skl)),sK7_skl(ordered_pair(sK4_skl(sK8_skl(sK2_skl,sK3_skl)),sK5_skl(sK8_skl(sK2_skl,sK3_skl)))))|~sQ7_spl|~sQ25_spl),
% 0.10/0.40 inference(forward_demodulation,[status(thm)],[f113,f292])).
% 0.10/0.40 fof(f294,plain,(
% 0.10/0.40 sK8_skl(sK2_skl,sK3_skl)=ordered_pair(sK6_skl(sK8_skl(sK2_skl,sK3_skl)),sK7_skl(sK8_skl(sK2_skl,sK3_skl)))|~sQ7_spl|~sQ25_spl),
% 0.10/0.40 inference(forward_demodulation,[status(thm)],[f113,f293])).
% 0.10/0.40 fof(f317,plain,(
% 0.10/0.40 $false|sQ6_spl|~sQ7_spl|~sQ25_spl),
% 0.10/0.40 inference(forward_subsumption_resolution,[status(thm)],[f294,f111])).
% 0.10/0.40 fof(f318,plain,(
% 0.10/0.40 sQ6_spl|~sQ7_spl|~sQ25_spl),
% 0.10/0.40 inference(contradiction_clause,[status(thm)],[f317])).
% 0.10/0.40 fof(f319,plain,(
% 0.10/0.40 $false),
% 0.10/0.40 inference(sat_refutation,[status(thm)],[f115,f140,f210,f215,f220,f225,f266,f267,f281,f318])).
% 0.10/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.43 % Elapsed time: 0.055516 seconds
% 0.10/0.43 % CPU time: 0.174111 seconds
% 0.10/0.43 % Total memory used: 102.705 MB
% 0.10/0.43 % Net memory used: 102.317 MB
%------------------------------------------------------------------------------