%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU361+2 : TPTP v9.3.1. Released v3.3.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:20:17 PM UTC 2026
% Result : Theorem 150.32s 19.90s
% Output : CNFRefutation 150.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 13
% Syntax : Number of formulae : 74 ( 14 unt; 6 def)
% Number of atoms : 292 ( 21 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 362 ( 144 ~; 144 |; 47 &)
% ( 11 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 7 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-3 aty)
% Number of variables : 98 ( 90 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f56,axiom,
! [A] :
( rel_str(A)
=> bottom_of_relstr(A) = join_on_relstr(A,empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f91,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f158,axiom,
! [A] :
( rel_str(A)
=> ! [B,C] :
( element(C,the_carrier(A))
=> ( relstr_set_smaller(A,B,C)
<=> ! [D] :
( element(D,the_carrier(A))
=> ( in(D,B)
=> related(A,D,C) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f161,axiom,
! [A] :
( rel_str(A)
=> ! [B,C] :
( element(C,the_carrier(A))
=> ( ex_sup_of_relstr_set(A,B)
=> ( C = join_on_relstr(A,B)
<=> ( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_set_smaller(A,B,D)
=> related(A,C,D) ) )
& relstr_set_smaller(A,B,C) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f206,axiom,
! [A] :
( rel_str(A)
=> element(bottom_of_relstr(A),the_carrier(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f605,lemma,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) )
=> ( ex_inf_of_relstr_set(A,the_carrier(A))
& ex_sup_of_relstr_set(A,empty_set) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f610,conjecture,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> related(A,bottom_of_relstr(A),B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f611,negated_conjecture,
~ ! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> related(A,bottom_of_relstr(A),B) ) ),
inference(negated_conjecture,[status(cth)],[f610]) ).
fof(f885,plain,
! [A] :
( bottom_of_relstr(A) = join_on_relstr(A,empty_set)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f886,plain,
! [X0] :
( bottom_of_relstr(X0) = join_on_relstr(X0,empty_set)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f885]) ).
fof(f1144,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f91]) ).
fof(f1145,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f1144]) ).
fof(f1146,plain,
( ! [A] :
( in(sK49_skl(A),A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49_skl]),skolemize(B,sK49_skl(A))],[f1145]) ).
fof(f1147,plain,
! [X0,X1] :
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f1146]) ).
fof(f1602,plain,
! [A] :
( ! [B,C] :
( ( relstr_set_smaller(A,B,C)
<=> ! [D] :
( related(A,D,C)
| ~ in(D,B)
| ~ element(D,the_carrier(A)) ) )
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f158]) ).
fof(f1603,plain,
! [A] :
( ! [B,C] :
( ( ( ? [D] :
( ~ related(A,D,C)
& in(D,B)
& element(D,the_carrier(A)) )
| relstr_set_smaller(A,B,C) )
& ( ! [D] :
( related(A,D,C)
| ~ in(D,B)
| ~ element(D,the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(NNF_transformation,[status(thm)],[f1602]) ).
fof(f1604,plain,
! [A] :
( ! [C] :
( ( ! [B] :
( ? [D] :
( ~ related(A,D,C)
& in(D,B)
& element(D,the_carrier(A)) )
| relstr_set_smaller(A,B,C) )
& ! [B] :
( ! [D] :
( related(A,D,C)
| ~ in(D,B)
| ~ element(D,the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(miniscoping,[status(thm)],[f1603]) ).
fof(f1605,plain,
! [A] :
( ! [C] :
( ( ! [B] :
( ( ~ related(A,sK123_skl(B,C,A),C)
& in(sK123_skl(B,C,A),B)
& element(sK123_skl(B,C,A),the_carrier(A)) )
| relstr_set_smaller(A,B,C) )
& ! [B] :
( ! [D] :
( related(A,D,C)
| ~ in(D,B)
| ~ element(D,the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK123_skl]),skolemize(D,sK123_skl(B,C,A))],[f1604]) ).
fof(f1608,plain,
! [X0,X1,X2] :
( in(sK123_skl(X2,X1,X0),X2)
| relstr_set_smaller(X0,X2,X1)
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1605]) ).
fof(f1618,plain,
! [A] :
( ! [B,C] :
( ( C = join_on_relstr(A,B)
<=> ( ! [D] :
( related(A,C,D)
| ~ relstr_set_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(A,B,C) ) )
| ~ ex_sup_of_relstr_set(A,B)
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f161]) ).
fof(f1619,plain,
! [A] :
( ! [B,C] :
( ( ( ? [D] :
( ~ related(A,C,D)
& relstr_set_smaller(A,B,D)
& element(D,the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C)
| C = join_on_relstr(A,B) )
& ( ( ! [D] :
( related(A,C,D)
| ~ relstr_set_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(A,B,C) )
| C != join_on_relstr(A,B) ) )
| ~ ex_sup_of_relstr_set(A,B)
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(NNF_transformation,[status(thm)],[f1618]) ).
fof(f1620,plain,
! [A] :
( ! [C] :
( ! [B] :
( ( ( ? [D] :
( ~ related(A,C,D)
& relstr_set_smaller(A,B,D)
& element(D,the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C)
| C = join_on_relstr(A,B) )
& ( ( ! [D] :
( related(A,C,D)
| ~ relstr_set_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(A,B,C) )
| C != join_on_relstr(A,B) ) )
| ~ ex_sup_of_relstr_set(A,B) )
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(miniscoping,[status(thm)],[f1619]) ).
fof(f1621,plain,
! [A] :
( ! [C] :
( ! [B] :
( ( ( ( ~ related(A,C,sK124_skl(B,C,A))
& relstr_set_smaller(A,B,sK124_skl(B,C,A))
& element(sK124_skl(B,C,A),the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C)
| C = join_on_relstr(A,B) )
& ( ( ! [D] :
( related(A,C,D)
| ~ relstr_set_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(A,B,C) )
| C != join_on_relstr(A,B) ) )
| ~ ex_sup_of_relstr_set(A,B) )
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK124_skl]),skolemize(D,sK124_skl(B,C,A))],[f1620]) ).
fof(f1623,plain,
! [X0,X1,X2,X3] :
( related(X0,X1,X3)
| ~ relstr_set_smaller(X0,X2,X3)
| ~ element(X3,the_carrier(X0))
| X1 != join_on_relstr(X0,X2)
| ~ ex_sup_of_relstr_set(X0,X2)
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1621]) ).
fof(f1689,plain,
! [A] :
( element(bottom_of_relstr(A),the_carrier(A))
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f206]) ).
fof(f1690,plain,
! [X0] :
( element(bottom_of_relstr(X0),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1689]) ).
fof(f3382,plain,
! [A] :
( ( ex_inf_of_relstr_set(A,the_carrier(A))
& ex_sup_of_relstr_set(A,empty_set) )
| ~ rel_str(A)
| ~ lower_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f605]) ).
fof(f3383,plain,
! [X0] :
( ex_sup_of_relstr_set(X0,empty_set)
| ~ rel_str(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f3382]) ).
fof(f3398,plain,
? [A] :
( ? [B] :
( ~ related(A,bottom_of_relstr(A),B)
& element(B,the_carrier(A)) )
& rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f611]) ).
fof(f3399,plain,
( ~ related(sK392_skl,bottom_of_relstr(sK392_skl),sK393_skl)
& element(sK393_skl,the_carrier(sK392_skl))
& rel_str(sK392_skl)
& lower_bounded_relstr(sK392_skl)
& antisymmetric_relstr(sK392_skl)
& ~ empty_carrier(sK392_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK392_skl,sK393_skl]),skolemize(A,sK392_skl),skolemize(B,sK393_skl)],[f3398]) ).
fof(f3400,plain,
~ empty_carrier(sK392_skl),
inference(cnf_transformation,[status(thm)],[f3399]) ).
fof(f3401,plain,
antisymmetric_relstr(sK392_skl),
inference(cnf_transformation,[status(thm)],[f3399]) ).
fof(f3402,plain,
lower_bounded_relstr(sK392_skl),
inference(cnf_transformation,[status(thm)],[f3399]) ).
fof(f3403,plain,
rel_str(sK392_skl),
inference(cnf_transformation,[status(thm)],[f3399]) ).
fof(f3404,plain,
element(sK393_skl,the_carrier(sK392_skl)),
inference(cnf_transformation,[status(thm)],[f3399]) ).
fof(f3405,plain,
~ related(sK392_skl,bottom_of_relstr(sK392_skl),sK393_skl),
inference(cnf_transformation,[status(thm)],[f3399]) ).
fof(f4520,plain,
! [X0] : ~ in(X0,empty_set),
inference(destructive_equality_resolution,[status(thm)],[f1147]) ).
fof(f4576,plain,
! [X0,X1,X2] :
( related(X0,join_on_relstr(X0,X1),X2)
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ rel_str(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f1623]) ).
fof(f4795,plain,
bottom_of_relstr(sK392_skl) = join_on_relstr(sK392_skl,empty_set),
inference(resolution,[status(thm)],[f3403,f886]) ).
fof(f6203,definition,
( sQ71_spl
<=> rel_str(sK392_skl) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f6205,plain,
( sQ71_spl
| ~ rel_str(sK392_skl) ),
inference(component_clause,[status(thm)],[f6203]) ).
fof(f6211,plain,
( sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6205,f3403]) ).
fof(f6212,plain,
sQ71_spl,
inference(contradiction_clause,[status(thm)],[f6211]) ).
fof(f6337,definition,
( sQ96_spl
<=> lower_bounded_relstr(sK392_skl) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f6339,plain,
( sQ96_spl
| ~ lower_bounded_relstr(sK392_skl) ),
inference(component_clause,[status(thm)],[f6337]) ).
fof(f6341,plain,
( sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6339,f3402]) ).
fof(f6342,plain,
sQ96_spl,
inference(contradiction_clause,[status(thm)],[f6341]) ).
fof(f6345,definition,
( sQ97_spl
<=> empty_carrier(sK392_skl) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f6346,plain,
( ~ sQ97_spl
| empty_carrier(sK392_skl) ),
inference(component_clause,[status(thm)],[f6345]) ).
fof(f6348,definition,
( sQ98_spl
<=> antisymmetric_relstr(sK392_skl) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f6350,plain,
( sQ98_spl
| ~ antisymmetric_relstr(sK392_skl) ),
inference(component_clause,[status(thm)],[f6348]) ).
fof(f6352,plain,
( sQ98_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6350,f3401]) ).
fof(f6353,plain,
sQ98_spl,
inference(contradiction_clause,[status(thm)],[f6352]) ).
fof(f6354,plain,
( ~ sQ97_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6346,f3400]) ).
fof(f6355,plain,
~ sQ97_spl,
inference(contradiction_clause,[status(thm)],[f6354]) ).
fof(f8301,plain,
! [X0,X1] :
( in(sK123_skl(X1,X0,sK392_skl),X1)
| relstr_set_smaller(sK392_skl,X1,X0)
| ~ element(X0,the_carrier(sK392_skl)) ),
inference(resolution,[status(thm)],[f1608,f3403]) ).
fof(f8771,plain,
! [X0,X1] :
( ~ rel_str(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| empty_carrier(X0)
| related(X0,join_on_relstr(X0,empty_set),X1)
| ~ relstr_set_smaller(X0,empty_set,X1)
| ~ element(X1,the_carrier(X0))
| ~ element(join_on_relstr(X0,empty_set),the_carrier(X0))
| ~ rel_str(X0) ),
inference(resolution,[status(thm)],[f4576,f3383]) ).
fof(f8772,plain,
! [X0,X1] :
( ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| empty_carrier(X0)
| related(X0,join_on_relstr(X0,empty_set),X1)
| ~ relstr_set_smaller(X0,empty_set,X1)
| ~ element(X1,the_carrier(X0))
| ~ element(join_on_relstr(X0,empty_set),the_carrier(X0))
| ~ rel_str(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f8771]) ).
fof(f8896,definition,
( sQ410_spl
<=> element(join_on_relstr(sK392_skl,empty_set),the_carrier(sK392_skl)) ),
introduced(definition,[new_symbols(definition,[sQ410_spl])],[split_symbol_definition]) ).
fof(f8898,plain,
( sQ410_spl
| ~ element(join_on_relstr(sK392_skl,empty_set),the_carrier(sK392_skl)) ),
inference(component_clause,[status(thm)],[f8896]) ).
fof(f8904,plain,
( sQ410_spl
| ~ element(bottom_of_relstr(sK392_skl),the_carrier(sK392_skl)) ),
inference(forward_demodulation,[status(thm)],[f4795,f8898]) ).
fof(f8906,plain,
! [X0] :
( in(sK123_skl(empty_set,X0,sK392_skl),empty_set)
| ~ element(X0,the_carrier(sK392_skl))
| ~ lower_bounded_relstr(sK392_skl)
| ~ antisymmetric_relstr(sK392_skl)
| empty_carrier(sK392_skl)
| related(sK392_skl,join_on_relstr(sK392_skl,empty_set),X0)
| ~ element(X0,the_carrier(sK392_skl))
| ~ element(join_on_relstr(sK392_skl,empty_set),the_carrier(sK392_skl))
| ~ rel_str(sK392_skl) ),
inference(resolution,[status(thm)],[f8772,f8301]) ).
fof(f8907,definition,
! [X0] :
( sQ412_spl
<=> ( in(sK123_skl(empty_set,X0,sK392_skl),empty_set)
| ~ element(X0,the_carrier(sK392_skl))
| related(sK392_skl,join_on_relstr(sK392_skl,empty_set),X0)
| ~ element(X0,the_carrier(sK392_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ412_spl])],[split_symbol_definition]) ).
fof(f8908,plain,
! [X0] :
( ~ sQ412_spl
| in(sK123_skl(empty_set,X0,sK392_skl),empty_set)
| ~ element(X0,the_carrier(sK392_skl))
| related(sK392_skl,join_on_relstr(sK392_skl,empty_set),X0)
| ~ element(X0,the_carrier(sK392_skl)) ),
inference(component_clause,[status(thm)],[f8907]) ).
fof(f8910,plain,
( ~ sQ96_spl
| ~ sQ98_spl
| sQ97_spl
| sQ412_spl
| ~ sQ410_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f8906,f6203,f8896,f8907,f6345,f6348,f6337]) ).
fof(f8911,plain,
! [X0] :
( ~ sQ412_spl
| in(sK123_skl(empty_set,X0,sK392_skl),empty_set)
| ~ element(X0,the_carrier(sK392_skl))
| related(sK392_skl,bottom_of_relstr(sK392_skl),X0)
| ~ element(X0,the_carrier(sK392_skl)) ),
inference(forward_demodulation,[status(thm)],[f4795,f8908]) ).
fof(f8912,plain,
! [X0] :
( ~ sQ412_spl
| in(sK123_skl(empty_set,X0,sK392_skl),empty_set)
| related(sK392_skl,bottom_of_relstr(sK392_skl),X0)
| ~ element(X0,the_carrier(sK392_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f8911]) ).
fof(f8913,plain,
! [X0] :
( ~ sQ412_spl
| related(sK392_skl,bottom_of_relstr(sK392_skl),X0)
| ~ element(X0,the_carrier(sK392_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f8912,f4520]) ).
fof(f8914,plain,
( sQ410_spl
| ~ rel_str(sK392_skl) ),
inference(resolution,[status(thm)],[f8904,f1690]) ).
fof(f8917,plain,
( sQ410_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f8914,f6203,f8896]) ).
fof(f8919,plain,
( ~ sQ412_spl
| ~ element(sK393_skl,the_carrier(sK392_skl)) ),
inference(resolution,[status(thm)],[f8913,f3405]) ).
fof(f8927,plain,
( ~ sQ412_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8919,f3404]) ).
fof(f8928,plain,
~ sQ412_spl,
inference(contradiction_clause,[status(thm)],[f8927]) ).
fof(f8929,plain,
$false,
inference(sat_refutation,[status(thm)],[f6212,f6342,f6353,f6355,f8910,f8917,f8928]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU361+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n017.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 06:10:56 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.21/0.56 % Drodi V4.1.1
% 150.32/19.90 % Refutation found
% 150.32/19.90 % SZS status Theorem for theBenchmark: Theorem is valid
% 150.32/19.90 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 19.01/20.04 % Elapsed time: 19.568060 seconds
% 19.01/20.04 % CPU time: 153.911526 seconds
% 19.01/20.04 % Total memory used: 672.365 MB
% 19.01/20.04 % Net memory used: 619.277 MB
%------------------------------------------------------------------------------