%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU360+1 : 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 0.15s 0.40s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 25
% Syntax : Number of formulae : 126 ( 9 unt; 16 def)
% Number of atoms : 649 ( 0 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 905 ( 382 ~; 407 |; 74 &)
% ( 24 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 30 ( 29 usr; 17 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 2 con; 0-3 aty)
% Number of variables : 199 ( 181 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [A] :
( rel_str(A)
=> ( lower_bounded_relstr(A)
<=> ? [B] :
( relstr_element_smaller(A,the_carrier(A),B)
& element(B,the_carrier(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] :
( rel_str(A)
=> ! [B,C] :
( element(C,the_carrier(A))
=> ( relstr_element_smaller(A,B,C)
<=> ! [D] :
( element(D,the_carrier(A))
=> ( in(D,B)
=> related(A,C,D) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( rel_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ~ empty(the_carrier(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( ( rel_str(A)
& antisymmetric_relstr(A) )
=> ! [B] :
( ex_sup_of_relstr_set(A,B)
<=> ? [C] :
( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_set_smaller(A,B,D)
=> related(A,C,D) ) )
& relstr_set_smaller(A,B,C)
& element(C,the_carrier(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A] :
( ( rel_str(A)
& antisymmetric_relstr(A) )
=> ! [B] :
( ex_inf_of_relstr_set(A,B)
<=> ? [C] :
( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_element_smaller(A,B,D)
=> related(A,D,C) ) )
& relstr_element_smaller(A,B,C)
& element(C,the_carrier(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,conjecture,
! [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(f24,negated_conjecture,
~ ! [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) ) ),
inference(negated_conjecture,[status(cth)],[f23]) ).
fof(f26,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( element(B,the_carrier(A))
=> ( relstr_element_smaller(A,empty_set,B)
& relstr_set_smaller(A,empty_set,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,plain,
! [A] :
( ( lower_bounded_relstr(A)
<=> ? [B] :
( relstr_element_smaller(A,the_carrier(A),B)
& element(B,the_carrier(A)) ) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f34,plain,
! [A] :
( ( ( ! [B] :
( ~ relstr_element_smaller(A,the_carrier(A),B)
| ~ element(B,the_carrier(A)) )
| lower_bounded_relstr(A) )
& ( ? [B] :
( relstr_element_smaller(A,the_carrier(A),B)
& element(B,the_carrier(A)) )
| ~ lower_bounded_relstr(A) ) )
| ~ rel_str(A) ),
inference(NNF_transformation,[status(thm)],[f33]) ).
fof(f35,plain,
! [A] :
( ( ( ! [B] :
( ~ relstr_element_smaller(A,the_carrier(A),B)
| ~ element(B,the_carrier(A)) )
| lower_bounded_relstr(A) )
& ( ( relstr_element_smaller(A,the_carrier(A),sK0_skl(A))
& element(sK0_skl(A),the_carrier(A)) )
| ~ lower_bounded_relstr(A) ) )
| ~ rel_str(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f34]) ).
fof(f36,plain,
! [X0] :
( element(sK0_skl(X0),the_carrier(X0))
| ~ lower_bounded_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f37,plain,
! [X0] :
( relstr_element_smaller(X0,the_carrier(X0),sK0_skl(X0))
| ~ lower_bounded_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f39,plain,
! [A] :
( ! [B,C] :
( ( relstr_element_smaller(A,B,C)
<=> ! [D] :
( related(A,C,D)
| ~ in(D,B)
| ~ element(D,the_carrier(A)) ) )
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f40,plain,
! [A] :
( ! [B,C] :
( ( ( ? [D] :
( ~ related(A,C,D)
& in(D,B)
& element(D,the_carrier(A)) )
| relstr_element_smaller(A,B,C) )
& ( ! [D] :
( related(A,C,D)
| ~ in(D,B)
| ~ element(D,the_carrier(A)) )
| ~ relstr_element_smaller(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(NNF_transformation,[status(thm)],[f39]) ).
fof(f41,plain,
! [A] :
( ! [C] :
( ( ! [B] :
( ? [D] :
( ~ related(A,C,D)
& in(D,B)
& element(D,the_carrier(A)) )
| relstr_element_smaller(A,B,C) )
& ! [B] :
( ! [D] :
( related(A,C,D)
| ~ in(D,B)
| ~ element(D,the_carrier(A)) )
| ~ relstr_element_smaller(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(miniscoping,[status(thm)],[f40]) ).
fof(f42,plain,
! [A] :
( ! [C] :
( ( ! [B] :
( ( ~ related(A,C,sK1_skl(B,C,A))
& in(sK1_skl(B,C,A),B)
& element(sK1_skl(B,C,A),the_carrier(A)) )
| relstr_element_smaller(A,B,C) )
& ! [B] :
( ! [D] :
( related(A,C,D)
| ~ in(D,B)
| ~ element(D,the_carrier(A)) )
| ~ relstr_element_smaller(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(D,sK1_skl(B,C,A))],[f41]) ).
fof(f43,plain,
! [X0,X1,X2,X3] :
( related(X0,X1,X3)
| ~ in(X3,X2)
| ~ element(X3,the_carrier(X0))
| ~ relstr_element_smaller(X0,X2,X1)
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f47,plain,
! [A] :
( one_sorted_str(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f48,plain,
! [X0] :
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f55,plain,
! [A] :
( ~ empty(the_carrier(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f56,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f68,plain,
! [A] :
( ! [B] :
( ex_sup_of_relstr_set(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)
& element(C,the_carrier(A)) ) )
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f69,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)
| ~ element(C,the_carrier(A)) )
| ex_sup_of_relstr_set(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)
& element(C,the_carrier(A)) )
| ~ ex_sup_of_relstr_set(A,B) ) )
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(NNF_transformation,[status(thm)],[f68]) ).
fof(f70,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)
| ~ element(C,the_carrier(A)) )
| ex_sup_of_relstr_set(A,B) )
& ! [B] :
( ? [C] :
( ! [D] :
( related(A,C,D)
| ~ relstr_set_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(A,B,C)
& element(C,the_carrier(A)) )
| ~ ex_sup_of_relstr_set(A,B) ) )
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(miniscoping,[status(thm)],[f69]) ).
fof(f71,plain,
! [A] :
( ( ! [B] :
( ! [C] :
( ( ~ related(A,C,sK10_skl(C,B,A))
& relstr_set_smaller(A,B,sK10_skl(C,B,A))
& element(sK10_skl(C,B,A),the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A)) )
| ex_sup_of_relstr_set(A,B) )
& ! [B] :
( ( ! [D] :
( related(A,sK9_skl(B,A),D)
| ~ relstr_set_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(A,B,sK9_skl(B,A))
& element(sK9_skl(B,A),the_carrier(A)) )
| ~ ex_sup_of_relstr_set(A,B) ) )
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl]),skolemize(C,sK9_skl(B,A)),skolemize(D,sK10_skl(C,B,A))],[f70]) ).
fof(f75,plain,
! [X0,X1,X2] :
( element(sK10_skl(X2,X1,X0),the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0)
| ~ antisymmetric_relstr(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ related(X0,X2,sK10_skl(X2,X1,X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0)
| ~ antisymmetric_relstr(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f78,plain,
! [A] :
( ! [B] :
( ex_inf_of_relstr_set(A,B)
<=> ? [C] :
( ! [D] :
( related(A,D,C)
| ~ relstr_element_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_element_smaller(A,B,C)
& element(C,the_carrier(A)) ) )
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f79,plain,
! [A] :
( ! [B] :
( ( ! [C] :
( ? [D] :
( ~ related(A,D,C)
& relstr_element_smaller(A,B,D)
& element(D,the_carrier(A)) )
| ~ relstr_element_smaller(A,B,C)
| ~ element(C,the_carrier(A)) )
| ex_inf_of_relstr_set(A,B) )
& ( ? [C] :
( ! [D] :
( related(A,D,C)
| ~ relstr_element_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_element_smaller(A,B,C)
& element(C,the_carrier(A)) )
| ~ ex_inf_of_relstr_set(A,B) ) )
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(NNF_transformation,[status(thm)],[f78]) ).
fof(f80,plain,
! [A] :
( ( ! [B] :
( ! [C] :
( ? [D] :
( ~ related(A,D,C)
& relstr_element_smaller(A,B,D)
& element(D,the_carrier(A)) )
| ~ relstr_element_smaller(A,B,C)
| ~ element(C,the_carrier(A)) )
| ex_inf_of_relstr_set(A,B) )
& ! [B] :
( ? [C] :
( ! [D] :
( related(A,D,C)
| ~ relstr_element_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_element_smaller(A,B,C)
& element(C,the_carrier(A)) )
| ~ ex_inf_of_relstr_set(A,B) ) )
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(miniscoping,[status(thm)],[f79]) ).
fof(f81,plain,
! [A] :
( ( ! [B] :
( ! [C] :
( ( ~ related(A,sK12_skl(C,B,A),C)
& relstr_element_smaller(A,B,sK12_skl(C,B,A))
& element(sK12_skl(C,B,A),the_carrier(A)) )
| ~ relstr_element_smaller(A,B,C)
| ~ element(C,the_carrier(A)) )
| ex_inf_of_relstr_set(A,B) )
& ! [B] :
( ( ! [D] :
( related(A,D,sK11_skl(B,A))
| ~ relstr_element_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_element_smaller(A,B,sK11_skl(B,A))
& element(sK11_skl(B,A),the_carrier(A)) )
| ~ ex_inf_of_relstr_set(A,B) ) )
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl]),skolemize(C,sK11_skl(B,A)),skolemize(D,sK12_skl(C,B,A))],[f80]) ).
fof(f85,plain,
! [X0,X1,X2] :
( element(sK12_skl(X2,X1,X0),the_carrier(X0))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0)
| ~ antisymmetric_relstr(X0) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f86,plain,
! [X0,X1,X2] :
( relstr_element_smaller(X0,X1,sK12_skl(X2,X1,X0))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0)
| ~ antisymmetric_relstr(X0) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f87,plain,
! [X0,X1,X2] :
( ~ related(X0,sK12_skl(X2,X1,X0),X2)
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0)
| ~ antisymmetric_relstr(X0) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f90,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f91,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f92,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)],[f24]) ).
fof(f93,plain,
( ( ~ ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl))
| ~ ex_sup_of_relstr_set(sK13_skl,empty_set) )
& rel_str(sK13_skl)
& lower_bounded_relstr(sK13_skl)
& antisymmetric_relstr(sK13_skl)
& ~ empty_carrier(sK13_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f92]) ).
fof(f94,plain,
~ empty_carrier(sK13_skl),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f95,plain,
antisymmetric_relstr(sK13_skl),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f96,plain,
lower_bounded_relstr(sK13_skl),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f97,plain,
rel_str(sK13_skl),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f98,plain,
( ~ ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl))
| ~ ex_sup_of_relstr_set(sK13_skl,empty_set) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f101,plain,
! [A] :
( ! [B] :
( ( relstr_element_smaller(A,empty_set,B)
& relstr_set_smaller(A,empty_set,B) )
| ~ element(B,the_carrier(A)) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f102,plain,
! [X0,X1] :
( relstr_set_smaller(X0,empty_set,X1)
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f110,definition,
( sQ0_spl
<=> ex_sup_of_relstr_set(sK13_skl,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f112,plain,
( sQ0_spl
| ~ ex_sup_of_relstr_set(sK13_skl,empty_set) ),
inference(component_clause,[status(thm)],[f110]) ).
fof(f113,definition,
( sQ1_spl
<=> ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f115,plain,
( sQ1_spl
| ~ ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl)) ),
inference(component_clause,[status(thm)],[f113]) ).
fof(f116,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f98,f110,f113]) ).
fof(f118,plain,
! [X0] :
( relstr_set_smaller(X0,empty_set,sK0_skl(X0))
| ~ rel_str(X0)
| ~ lower_bounded_relstr(X0)
| ~ rel_str(X0) ),
inference(resolution,[status(thm)],[f36,f102]) ).
fof(f119,plain,
! [X0] :
( relstr_set_smaller(X0,empty_set,sK0_skl(X0))
| ~ lower_bounded_relstr(X0)
| ~ rel_str(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f118]) ).
fof(f130,plain,
! [X0,X1,X2,X3] :
( related(X2,X3,X0)
| ~ element(X0,the_carrier(X2))
| ~ relstr_element_smaller(X2,X1,X3)
| ~ element(X3,the_carrier(X2))
| ~ rel_str(X2)
| empty(X1)
| ~ element(X0,X1) ),
inference(resolution,[status(thm)],[f91,f43]) ).
fof(f134,plain,
! [X0,X1,X2] :
( related(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,X1,X2)
| ~ element(X2,the_carrier(sK13_skl))
| empty(X1)
| ~ element(X0,X1) ),
inference(resolution,[status(thm)],[f130,f97]) ).
fof(f163,plain,
! [X0,X1,X2] :
( ~ relstr_element_smaller(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_inf_of_relstr_set(sK13_skl,X2)
| ~ rel_str(sK13_skl)
| ~ antisymmetric_relstr(sK13_skl)
| ~ element(X0,the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,X1,sK12_skl(X0,X2,sK13_skl))
| ~ element(sK12_skl(X0,X2,sK13_skl),the_carrier(sK13_skl))
| empty(X1)
| ~ element(X0,X1) ),
inference(resolution,[status(thm)],[f134,f87]) ).
fof(f164,plain,
! [X0,X1,X2] :
( ~ relstr_set_smaller(sK13_skl,X1,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ rel_str(sK13_skl)
| ~ antisymmetric_relstr(sK13_skl)
| ~ element(sK10_skl(X0,X1,sK13_skl),the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| empty(X2)
| ~ element(sK10_skl(X0,X1,sK13_skl),X2) ),
inference(resolution,[status(thm)],[f134,f77]) ).
fof(f166,definition,
! [X0,X1,X2] :
( sQ7_spl
<=> ( ~ relstr_element_smaller(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_inf_of_relstr_set(sK13_skl,X2)
| ~ element(X0,the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,X1,sK12_skl(X0,X2,sK13_skl))
| ~ element(sK12_skl(X0,X2,sK13_skl),the_carrier(sK13_skl))
| empty(X1)
| ~ element(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f167,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_inf_of_relstr_set(sK13_skl,X2)
| ~ element(X0,the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,X1,sK12_skl(X0,X2,sK13_skl))
| ~ element(sK12_skl(X0,X2,sK13_skl),the_carrier(sK13_skl))
| empty(X1)
| ~ element(X0,X1) ),
inference(component_clause,[status(thm)],[f166]) ).
fof(f169,definition,
( sQ8_spl
<=> antisymmetric_relstr(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f171,plain,
( sQ8_spl
| ~ antisymmetric_relstr(sK13_skl) ),
inference(component_clause,[status(thm)],[f169]) ).
fof(f172,definition,
( sQ9_spl
<=> rel_str(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f174,plain,
( sQ9_spl
| ~ rel_str(sK13_skl) ),
inference(component_clause,[status(thm)],[f172]) ).
fof(f175,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f163,f166,f169,f172]) ).
fof(f176,definition,
! [X0,X1,X2] :
( sQ10_spl
<=> ( ~ relstr_set_smaller(sK13_skl,X1,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ element(sK10_skl(X0,X1,sK13_skl),the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| empty(X2)
| ~ element(sK10_skl(X0,X1,sK13_skl),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f177,plain,
! [X0,X1,X2] :
( ~ sQ10_spl
| ~ relstr_set_smaller(sK13_skl,X1,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ element(sK10_skl(X0,X1,sK13_skl),the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| empty(X2)
| ~ element(sK10_skl(X0,X1,sK13_skl),X2) ),
inference(component_clause,[status(thm)],[f176]) ).
fof(f179,plain,
( ~ sQ9_spl
| ~ sQ8_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f164,f176,f169,f172]) ).
fof(f184,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f174,f97]) ).
fof(f185,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f184]) ).
fof(f186,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f171,f95]) ).
fof(f187,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f186]) ).
fof(f189,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ex_inf_of_relstr_set(sK13_skl,X2)
| ~ element(X0,the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,X1,sK12_skl(X0,X2,sK13_skl))
| ~ element(sK12_skl(X0,X2,sK13_skl),the_carrier(sK13_skl))
| empty(X1)
| ~ element(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f167]) ).
fof(f190,plain,
! [X0,X1,X2] :
( ~ sQ10_spl
| ~ relstr_set_smaller(sK13_skl,X1,X0)
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ element(sK10_skl(X0,X1,sK13_skl),the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| empty(X2)
| ~ element(sK10_skl(X0,X1,sK13_skl),X2) ),
inference(duplicate_literals_removal,[status(thm)],[f177]) ).
fof(f191,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_inf_of_relstr_set(sK13_skl,X2)
| ~ rel_str(sK13_skl)
| ~ antisymmetric_relstr(sK13_skl)
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ex_inf_of_relstr_set(sK13_skl,X2)
| ~ element(X0,the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,X1,sK12_skl(X0,X2,sK13_skl))
| empty(X1)
| ~ element(X0,X1) ),
inference(resolution,[status(thm)],[f189,f85]) ).
fof(f192,definition,
! [X0,X1,X2] :
( sQ12_spl
<=> ( ~ relstr_element_smaller(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_inf_of_relstr_set(sK13_skl,X2)
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ex_inf_of_relstr_set(sK13_skl,X2)
| ~ element(X0,the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,X1,sK12_skl(X0,X2,sK13_skl))
| empty(X1)
| ~ element(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f193,plain,
! [X0,X1,X2] :
( ~ sQ12_spl
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_inf_of_relstr_set(sK13_skl,X2)
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ex_inf_of_relstr_set(sK13_skl,X2)
| ~ element(X0,the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,X1,sK12_skl(X0,X2,sK13_skl))
| empty(X1)
| ~ element(X0,X1) ),
inference(component_clause,[status(thm)],[f192]) ).
fof(f195,plain,
( ~ sQ7_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f191,f192,f169,f172,f166]) ).
fof(f196,plain,
! [X0,X1,X2] :
( ~ sQ12_spl
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ex_inf_of_relstr_set(sK13_skl,X2)
| ~ element(X0,the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,X1,sK12_skl(X0,X2,sK13_skl))
| empty(X1)
| ~ element(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f193]) ).
fof(f212,plain,
! [X0,X1,X2] :
( ~ sQ10_spl
| ~ relstr_set_smaller(sK13_skl,X1,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ rel_str(sK13_skl)
| ~ antisymmetric_relstr(sK13_skl)
| ~ relstr_set_smaller(sK13_skl,X1,X0)
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| empty(X2)
| ~ element(sK10_skl(X0,X1,sK13_skl),X2) ),
inference(resolution,[status(thm)],[f190,f75]) ).
fof(f213,definition,
! [X0,X1,X2] :
( sQ16_spl
<=> ( ~ relstr_set_smaller(sK13_skl,X1,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ relstr_set_smaller(sK13_skl,X1,X0)
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| empty(X2)
| ~ element(sK10_skl(X0,X1,sK13_skl),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f214,plain,
! [X0,X1,X2] :
( ~ sQ16_spl
| ~ relstr_set_smaller(sK13_skl,X1,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ relstr_set_smaller(sK13_skl,X1,X0)
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| empty(X2)
| ~ element(sK10_skl(X0,X1,sK13_skl),X2) ),
inference(component_clause,[status(thm)],[f213]) ).
fof(f216,plain,
( ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f212,f213,f169,f172,f176]) ).
fof(f217,plain,
! [X0,X1,X2] :
( ~ sQ16_spl
| ~ relstr_set_smaller(sK13_skl,X1,X0)
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ relstr_element_smaller(sK13_skl,X2,X0)
| ~ element(X0,the_carrier(sK13_skl))
| empty(X2)
| ~ element(sK10_skl(X0,X1,sK13_skl),X2) ),
inference(duplicate_literals_removal,[status(thm)],[f214]) ).
fof(f218,plain,
! [X0,X1] :
( ~ sQ16_spl
| ~ relstr_set_smaller(sK13_skl,X1,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ rel_str(sK13_skl)
| ~ antisymmetric_relstr(sK13_skl)
| ~ relstr_set_smaller(sK13_skl,X1,X0)
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)
| ~ element(X0,the_carrier(sK13_skl))
| empty(the_carrier(sK13_skl)) ),
inference(resolution,[status(thm)],[f217,f75]) ).
fof(f219,definition,
( sQ17_spl
<=> empty(the_carrier(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f220,plain,
( ~ sQ17_spl
| empty(the_carrier(sK13_skl)) ),
inference(component_clause,[status(thm)],[f219]) ).
fof(f222,definition,
! [X0,X1] :
( sQ18_spl
<=> ( ~ relstr_set_smaller(sK13_skl,X1,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ relstr_set_smaller(sK13_skl,X1,X0)
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)
| ~ element(X0,the_carrier(sK13_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f223,plain,
! [X0,X1] :
( ~ sQ18_spl
| ~ relstr_set_smaller(sK13_skl,X1,X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ relstr_set_smaller(sK13_skl,X1,X0)
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)
| ~ element(X0,the_carrier(sK13_skl)) ),
inference(component_clause,[status(thm)],[f222]) ).
fof(f225,plain,
( ~ sQ16_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ18_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f218,f219,f222,f169,f172,f213]) ).
fof(f241,plain,
( ~ sQ17_spl
| ~ one_sorted_str(sK13_skl)
| empty_carrier(sK13_skl) ),
inference(resolution,[status(thm)],[f220,f56]) ).
fof(f244,definition,
( sQ22_spl
<=> empty_carrier(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f245,plain,
( ~ sQ22_spl
| empty_carrier(sK13_skl) ),
inference(component_clause,[status(thm)],[f244]) ).
fof(f247,definition,
( sQ23_spl
<=> one_sorted_str(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f249,plain,
( sQ23_spl
| ~ one_sorted_str(sK13_skl) ),
inference(component_clause,[status(thm)],[f247]) ).
fof(f250,plain,
( ~ sQ17_spl
| ~ sQ23_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f241,f244,f247,f219]) ).
fof(f251,plain,
( ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f245,f94]) ).
fof(f252,plain,
~ sQ22_spl,
inference(contradiction_clause,[status(thm)],[f251]) ).
fof(f253,plain,
( sQ23_spl
| ~ rel_str(sK13_skl) ),
inference(resolution,[status(thm)],[f249,f48]) ).
fof(f254,plain,
( sQ23_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f253,f172,f247]) ).
fof(f255,plain,
! [X0,X1] :
( ~ sQ18_spl
| ~ relstr_set_smaller(sK13_skl,X1,X0)
| ex_sup_of_relstr_set(sK13_skl,X1)
| ~ relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)
| ~ element(X0,the_carrier(sK13_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f223]) ).
fof(f256,plain,
! [X0] :
( sQ0_spl
| ~ sQ18_spl
| ~ relstr_set_smaller(sK13_skl,empty_set,X0)
| ~ relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)
| ~ element(X0,the_carrier(sK13_skl)) ),
inference(resolution,[status(thm)],[f255,f112]) ).
fof(f276,plain,
( sQ0_spl
| ~ sQ18_spl
| ~ lower_bounded_relstr(sK13_skl)
| ~ rel_str(sK13_skl)
| ~ relstr_set_smaller(sK13_skl,empty_set,sK0_skl(sK13_skl))
| ~ element(sK0_skl(sK13_skl),the_carrier(sK13_skl)) ),
inference(resolution,[status(thm)],[f256,f37]) ).
fof(f290,definition,
( sQ30_spl
<=> element(sK0_skl(sK13_skl),the_carrier(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f292,plain,
( sQ30_spl
| ~ element(sK0_skl(sK13_skl),the_carrier(sK13_skl)) ),
inference(component_clause,[status(thm)],[f290]) ).
fof(f293,definition,
( sQ31_spl
<=> relstr_set_smaller(sK13_skl,empty_set,sK0_skl(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f295,plain,
( sQ31_spl
| ~ relstr_set_smaller(sK13_skl,empty_set,sK0_skl(sK13_skl)) ),
inference(component_clause,[status(thm)],[f293]) ).
fof(f296,definition,
( sQ32_spl
<=> lower_bounded_relstr(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f298,plain,
( sQ32_spl
| ~ lower_bounded_relstr(sK13_skl) ),
inference(component_clause,[status(thm)],[f296]) ).
fof(f299,plain,
( sQ0_spl
| ~ sQ18_spl
| ~ sQ32_spl
| ~ sQ9_spl
| ~ sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f276,f290,f293,f172,f296,f222,f110]) ).
fof(f322,plain,
! [X0,X1] :
( ~ sQ12_spl
| sQ1_spl
| ~ relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)
| ~ element(X0,the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,X1,sK12_skl(X0,the_carrier(sK13_skl),sK13_skl))
| empty(X1)
| ~ element(X0,X1) ),
inference(resolution,[status(thm)],[f115,f196]) ).
fof(f374,plain,
! [X0] :
( ~ sQ12_spl
| sQ1_spl
| ~ relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)
| ~ element(X0,the_carrier(sK13_skl))
| ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl))
| ~ rel_str(sK13_skl)
| ~ antisymmetric_relstr(sK13_skl)
| ~ relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)
| ~ element(X0,the_carrier(sK13_skl))
| empty(the_carrier(sK13_skl))
| ~ element(X0,the_carrier(sK13_skl)) ),
inference(resolution,[status(thm)],[f322,f86]) ).
fof(f384,definition,
! [X0] :
( sQ49_spl
<=> ( ~ relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)
| ~ element(X0,the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)
| ~ element(X0,the_carrier(sK13_skl))
| ~ element(X0,the_carrier(sK13_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f385,plain,
! [X0] :
( ~ sQ49_spl
| ~ relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)
| ~ element(X0,the_carrier(sK13_skl))
| ~ relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)
| ~ element(X0,the_carrier(sK13_skl))
| ~ element(X0,the_carrier(sK13_skl)) ),
inference(component_clause,[status(thm)],[f384]) ).
fof(f387,plain,
( ~ sQ12_spl
| sQ1_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ17_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f374,f384,f219,f169,f172,f113,f192]) ).
fof(f396,plain,
! [X0] :
( ~ sQ49_spl
| ~ relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)
| ~ element(X0,the_carrier(sK13_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f385]) ).
fof(f398,plain,
( ~ sQ49_spl
| ~ lower_bounded_relstr(sK13_skl)
| ~ rel_str(sK13_skl)
| ~ element(sK0_skl(sK13_skl),the_carrier(sK13_skl)) ),
inference(resolution,[status(thm)],[f396,f37]) ).
fof(f403,plain,
( ~ sQ49_spl
| ~ sQ32_spl
| ~ sQ9_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f398,f290,f172,f296,f384]) ).
fof(f418,plain,
( sQ30_spl
| ~ lower_bounded_relstr(sK13_skl)
| ~ rel_str(sK13_skl) ),
inference(resolution,[status(thm)],[f292,f36]) ).
fof(f419,plain,
( sQ30_spl
| ~ sQ32_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f418,f172,f296,f290]) ).
fof(f420,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f298,f96]) ).
fof(f421,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f420]) ).
fof(f441,plain,
( sQ31_spl
| ~ lower_bounded_relstr(sK13_skl)
| ~ rel_str(sK13_skl) ),
inference(resolution,[status(thm)],[f295,f119]) ).
fof(f442,plain,
( sQ31_spl
| ~ sQ32_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f441,f172,f296,f293]) ).
fof(f443,plain,
$false,
inference(sat_refutation,[status(thm)],[f116,f175,f179,f185,f187,f195,f216,f225,f250,f252,f254,f299,f387,f403,f419,f421,f442]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU360+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:10:26 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.15/0.40 % Refutation found
% 0.15/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.43 % Elapsed time: 0.058025 seconds
% 0.15/0.43 % CPU time: 0.171565 seconds
% 0.15/0.43 % Total memory used: 82.828 MB
% 0.15/0.43 % Net memory used: 82.661 MB
%------------------------------------------------------------------------------