%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU037+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:19:07 PM UTC 2026
% Result : Theorem 0.11s 0.41s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 19
% Syntax : Number of formulae : 95 ( 21 unt; 8 def)
% Number of atoms : 270 ( 51 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 299 ( 124 ~; 118 |; 37 &)
% ( 10 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 9 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-3 aty)
% Number of variables : 115 ( 104 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [A,B] :
( relation(A)
=> relation(relation_dom_restriction(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A,B] :
( ( function(A)
& relation(A) )
=> ( function(relation_dom_restriction(A,B))
& relation(relation_dom_restriction(A,B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
? [A] :
( function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
? [A] :
( one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( B = relation_dom_restriction(C,A)
<=> ( ! [D] :
( in(D,relation_dom(B))
=> apply(B,D) = apply(C,D) )
& relation_dom(B) = set_intersection2(relation_dom(C),A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,conjecture,
! [A,B,C] :
( ( function(C)
& relation(C) )
=> ( in(B,set_intersection2(relation_dom(C),A))
=> apply(relation_dom_restriction(C,A),B) = apply(C,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,negated_conjecture,
~ ! [A,B,C] :
( ( function(C)
& relation(C) )
=> ( in(B,set_intersection2(relation_dom(C),A))
=> apply(relation_dom_restriction(C,A),B) = apply(C,B) ) ),
inference(negated_conjecture,[status(cth)],[f37]) ).
fof(f39,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,plain,
! [A,B] :
( relation(relation_dom_restriction(A,B))
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f53,plain,
! [A] :
( ! [B] : relation(relation_dom_restriction(A,B))
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f52]) ).
fof(f54,plain,
! [X0,X1] :
( relation(relation_dom_restriction(X0,X1))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f55,plain,
! [A] : element(sK0_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f7]) ).
fof(f56,plain,
! [X0] : element(sK0_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f66,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f68,plain,
! [A,B] :
( ( function(relation_dom_restriction(A,B))
& relation(relation_dom_restriction(A,B)) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f69,plain,
! [A] :
( ( ! [B] : function(relation_dom_restriction(A,B))
& ! [B] : relation(relation_dom_restriction(A,B)) )
| ~ function(A)
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f68]) ).
fof(f71,plain,
! [X0,X1] :
( function(relation_dom_restriction(X0,X1))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f81,plain,
( function(sK1_skl)
& relation(sK1_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(A,sK1_skl)],[f18]) ).
fof(f83,plain,
function(sK1_skl),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f105,plain,
( one_to_one(sK9_skl)
& function(sK9_skl)
& relation(sK9_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f26]) ).
fof(f107,plain,
function(sK9_skl),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f117,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f118,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f129,plain,
! [A,B] :
( ! [C] :
( ( B = relation_dom_restriction(C,A)
<=> ( ! [D] :
( apply(B,D) = apply(C,D)
| ~ in(D,relation_dom(B)) )
& relation_dom(B) = set_intersection2(relation_dom(C),A) ) )
| ~ function(C)
| ~ relation(C) )
| ~ function(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f130,plain,
! [A,B] :
( ! [C] :
( ( ( ? [D] :
( apply(B,D) != apply(C,D)
& in(D,relation_dom(B)) )
| relation_dom(B) != set_intersection2(relation_dom(C),A)
| B = relation_dom_restriction(C,A) )
& ( ( ! [D] :
( apply(B,D) = apply(C,D)
| ~ in(D,relation_dom(B)) )
& relation_dom(B) = set_intersection2(relation_dom(C),A) )
| B != relation_dom_restriction(C,A) ) )
| ~ function(C)
| ~ relation(C) )
| ~ function(B)
| ~ relation(B) ),
inference(NNF_transformation,[status(thm)],[f129]) ).
fof(f131,plain,
! [B] :
( ! [C] :
( ( ! [A] :
( ? [D] :
( apply(B,D) != apply(C,D)
& in(D,relation_dom(B)) )
| relation_dom(B) != set_intersection2(relation_dom(C),A)
| B = relation_dom_restriction(C,A) )
& ! [A] :
( ( ! [D] :
( apply(B,D) = apply(C,D)
| ~ in(D,relation_dom(B)) )
& relation_dom(B) = set_intersection2(relation_dom(C),A) )
| B != relation_dom_restriction(C,A) ) )
| ~ function(C)
| ~ relation(C) )
| ~ function(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f130]) ).
fof(f132,plain,
! [B] :
( ! [C] :
( ( ! [A] :
( ( apply(B,sK11_skl(A,C,B)) != apply(C,sK11_skl(A,C,B))
& in(sK11_skl(A,C,B),relation_dom(B)) )
| relation_dom(B) != set_intersection2(relation_dom(C),A)
| B = relation_dom_restriction(C,A) )
& ! [A] :
( ( ! [D] :
( apply(B,D) = apply(C,D)
| ~ in(D,relation_dom(B)) )
& relation_dom(B) = set_intersection2(relation_dom(C),A) )
| B != relation_dom_restriction(C,A) ) )
| ~ function(C)
| ~ relation(C) )
| ~ function(B)
| ~ relation(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(D,sK11_skl(A,C,B))],[f131]) ).
fof(f133,plain,
! [X0,X1,X2] :
( relation_dom(X0) = set_intersection2(relation_dom(X1),X2)
| X0 != relation_dom_restriction(X1,X2)
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f134,plain,
! [X0,X1,X2,X3] :
( apply(X0,X3) = apply(X1,X3)
| ~ in(X3,relation_dom(X0))
| X0 != relation_dom_restriction(X1,X2)
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f139,plain,
? [A,B,C] :
( apply(relation_dom_restriction(C,A),B) != apply(C,B)
& in(B,set_intersection2(relation_dom(C),A))
& function(C)
& relation(C) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f140,plain,
? [C] :
( ? [A,B] :
( apply(relation_dom_restriction(C,A),B) != apply(C,B)
& in(B,set_intersection2(relation_dom(C),A)) )
& function(C)
& relation(C) ),
inference(miniscoping,[status(thm)],[f139]) ).
fof(f141,plain,
( apply(relation_dom_restriction(sK12_skl,sK13_skl),sK14_skl) != apply(sK12_skl,sK14_skl)
& in(sK14_skl,set_intersection2(relation_dom(sK12_skl),sK13_skl))
& function(sK12_skl)
& relation(sK12_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(C,sK12_skl),skolemize(A,sK13_skl),skolemize(B,sK14_skl)],[f140]) ).
fof(f142,plain,
relation(sK12_skl),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f143,plain,
function(sK12_skl),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f144,plain,
in(sK14_skl,set_intersection2(relation_dom(sK12_skl),sK13_skl)),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f145,plain,
apply(relation_dom_restriction(sK12_skl,sK13_skl),sK14_skl) != apply(sK12_skl,sK14_skl),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f146,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f147,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f146]) ).
fof(f148,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f152,plain,
! [X0,X1] :
( relation_dom(relation_dom_restriction(X0,X1)) = set_intersection2(relation_dom(X0),X1)
| ~ function(X0)
| ~ relation(X0)
| ~ function(relation_dom_restriction(X0,X1))
| ~ relation(relation_dom_restriction(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f133]) ).
fof(f153,plain,
! [X0,X1,X2] :
( apply(relation_dom_restriction(X0,X1),X2) = apply(X0,X2)
| ~ in(X2,relation_dom(relation_dom_restriction(X0,X1)))
| ~ function(X0)
| ~ relation(X0)
| ~ function(relation_dom_restriction(X0,X1))
| ~ relation(relation_dom_restriction(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f134]) ).
fof(f165,plain,
! [X0] : ~ in(X0,empty_set),
inference(resolution,[status(thm)],[f57,f148]) ).
fof(f209,plain,
! [X0,X1] :
( in(X0,powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(resolution,[status(thm)],[f118,f66]) ).
fof(f216,plain,
! [X0,X1] :
( relation_dom(relation_dom_restriction(X0,X1)) = set_intersection2(relation_dom(X0),X1)
| ~ function(X0)
| ~ relation(X0)
| ~ function(relation_dom_restriction(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f152,f54]) ).
fof(f217,plain,
! [X0,X1] :
( ~ function(X0)
| ~ relation(X0)
| relation_dom(relation_dom_restriction(X0,X1)) = set_intersection2(relation_dom(X0),X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f216,f71]) ).
fof(f219,plain,
! [X0,X1] :
( relation_dom(relation_dom_restriction(X0,X1)) = set_intersection2(relation_dom(X0),X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f217]) ).
fof(f220,plain,
! [X0,X1,X2] :
( apply(relation_dom_restriction(X0,X1),X2) = apply(X0,X2)
| ~ in(X2,relation_dom(relation_dom_restriction(X0,X1)))
| ~ function(X0)
| ~ relation(X0)
| ~ function(relation_dom_restriction(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f153,f54]) ).
fof(f221,plain,
! [X0,X1,X2] :
( ~ function(X0)
| ~ relation(X0)
| apply(relation_dom_restriction(X0,X2),X1) = apply(X0,X1)
| ~ in(X1,relation_dom(relation_dom_restriction(X0,X2)))
| ~ function(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f220,f71]) ).
fof(f223,plain,
! [X0,X1,X2] :
( apply(relation_dom_restriction(X0,X2),X1) = apply(X0,X1)
| ~ in(X1,relation_dom(relation_dom_restriction(X0,X2)))
| ~ function(X0)
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f221]) ).
fof(f247,plain,
! [X0] : in(sK0_skl(powerset(X0)),powerset(X0)),
inference(resolution,[status(thm)],[f209,f56]) ).
fof(f394,plain,
! [X0] :
( relation_dom(relation_dom_restriction(sK12_skl,X0)) = set_intersection2(relation_dom(sK12_skl),X0)
| ~ function(sK12_skl) ),
inference(resolution,[status(thm)],[f219,f142]) ).
fof(f403,definition,
( sQ20_spl
<=> function(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f405,plain,
( sQ20_spl
| ~ function(sK9_skl) ),
inference(component_clause,[status(thm)],[f403]) ).
fof(f417,definition,
( sQ24_spl
<=> function(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f419,plain,
( sQ24_spl
| ~ function(sK1_skl) ),
inference(component_clause,[status(thm)],[f417]) ).
fof(f428,definition,
( sQ27_spl
<=> function(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f430,plain,
( sQ27_spl
| ~ function(sK12_skl) ),
inference(component_clause,[status(thm)],[f428]) ).
fof(f431,definition,
! [X0] :
( sQ28_spl
<=> relation_dom(relation_dom_restriction(sK12_skl,X0)) = set_intersection2(relation_dom(sK12_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f432,plain,
! [X0] :
( ~ sQ28_spl
| relation_dom(relation_dom_restriction(sK12_skl,X0)) = set_intersection2(relation_dom(sK12_skl),X0) ),
inference(component_clause,[status(thm)],[f431]) ).
fof(f434,plain,
( sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f394,f428,f431]) ).
fof(f438,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f430,f143]) ).
fof(f439,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f438]) ).
fof(f440,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f419,f83]) ).
fof(f441,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f440]) ).
fof(f442,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f405,f107]) ).
fof(f443,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f442]) ).
fof(f448,plain,
( ~ sQ28_spl
| in(sK14_skl,relation_dom(relation_dom_restriction(sK12_skl,sK13_skl))) ),
inference(backward_demodulation,[status(thm)],[f432,f144]) ).
fof(f501,plain,
! [X0,X1] :
( apply(relation_dom_restriction(sK12_skl,X1),X0) = apply(sK12_skl,X0)
| ~ in(X0,relation_dom(relation_dom_restriction(sK12_skl,X1)))
| ~ function(sK12_skl) ),
inference(resolution,[status(thm)],[f223,f142]) ).
fof(f523,definition,
! [X0,X1] :
( sQ38_spl
<=> ( apply(relation_dom_restriction(sK12_skl,X1),X0) = apply(sK12_skl,X0)
| ~ in(X0,relation_dom(relation_dom_restriction(sK12_skl,X1))) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f524,plain,
! [X0,X1] :
( ~ sQ38_spl
| apply(relation_dom_restriction(sK12_skl,X1),X0) = apply(sK12_skl,X0)
| ~ in(X0,relation_dom(relation_dom_restriction(sK12_skl,X1))) ),
inference(component_clause,[status(thm)],[f523]) ).
fof(f526,plain,
( sQ38_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f501,f428,f523]) ).
fof(f552,definition,
( sQ39_spl
<=> relation(relation_dom_restriction(sK12_skl,empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f554,plain,
( sQ39_spl
| ~ relation(relation_dom_restriction(sK12_skl,empty_set)) ),
inference(component_clause,[status(thm)],[f552]) ).
fof(f568,plain,
( sQ39_spl
| ~ relation(sK12_skl) ),
inference(resolution,[status(thm)],[f554,f54]) ).
fof(f570,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f568,f142]) ).
fof(f571,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f570]) ).
fof(f574,definition,
( sQ43_spl
<=> relation(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f576,plain,
( sQ43_spl
| ~ relation(sK12_skl) ),
inference(component_clause,[status(thm)],[f574]) ).
fof(f580,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f576,f142]) ).
fof(f581,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f580]) ).
fof(f705,definition,
( sQ53_spl
<=> powerset(empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f706,plain,
( ~ sQ53_spl
| powerset(empty_set) = empty_set ),
inference(component_clause,[status(thm)],[f705]) ).
fof(f721,plain,
( ~ sQ53_spl
| in(sK0_skl(powerset(empty_set)),empty_set) ),
inference(paramodulation,[status(thm)],[f706,f247]) ).
fof(f742,plain,
( ~ sQ53_spl
| in(sK0_skl(empty_set),empty_set) ),
inference(forward_demodulation,[status(thm)],[f706,f721]) ).
fof(f743,plain,
( ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f742,f165]) ).
fof(f744,plain,
~ sQ53_spl,
inference(contradiction_clause,[status(thm)],[f743]) ).
fof(f802,plain,
( ~ sQ28_spl
| ~ sQ38_spl
| apply(relation_dom_restriction(sK12_skl,sK13_skl),sK14_skl) = apply(sK12_skl,sK14_skl) ),
inference(resolution,[status(thm)],[f524,f448]) ).
fof(f806,plain,
( ~ sQ28_spl
| ~ sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f802,f145]) ).
fof(f807,plain,
( ~ sQ28_spl
| ~ sQ38_spl ),
inference(contradiction_clause,[status(thm)],[f806]) ).
fof(f808,plain,
$false,
inference(sat_refutation,[status(thm)],[f434,f439,f441,f443,f526,f571,f581,f744,f807]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU037+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n017.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 05:42:27 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 0.11/0.41 % Refutation found
% 0.11/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.11/0.43 % Elapsed time: 0.060084 seconds
% 0.11/0.43 % CPU time: 0.224085 seconds
% 0.11/0.43 % Total memory used: 105.619 MB
% 0.11/0.43 % Net memory used: 105.343 MB
%------------------------------------------------------------------------------