%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU375+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:20 PM UTC 2026
% Result : Theorem 58.22s 8.05s
% Output : CNFRefutation 58.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 11
% Syntax : Number of formulae : 91 ( 27 unt; 0 def)
% Number of atoms : 364 ( 20 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 454 ( 181 ~; 165 |; 60 &)
% ( 10 <=>; 38 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-4 aty)
% Number of variables : 132 ( 125 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f105,axiom,
! [A] :
( one_sorted_str(A)
=> ( empty_carrier(A)
<=> empty(the_carrier(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f124,axiom,
! [A,B] :
( ( empty(A)
=> ( element(B,A)
<=> empty(B) ) )
& ( ~ empty(A)
=> ( element(B,A)
<=> in(B,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f181,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( net_str(C,A)
=> ( subnetstr(C,A,B)
<=> ( the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
& subrelstr(C,B) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f187,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( subnetstr(C,A,B)
=> ( full_subnetstr(C,A,B)
<=> ( subrelstr(C,B)
& full_subrelstr(C,B) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f269,axiom,
! [A] :
( rel_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f272,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> rel_str(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f279,axiom,
! [A,B] :
( ( net_str(B,A)
& one_sorted_str(A) )
=> ! [C] :
( subnetstr(C,A,B)
=> net_str(C,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f601,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f614,conjecture,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( ( net_str(B,A)
& ~ empty_carrier(B) )
=> ! [C] :
( ( subnetstr(C,A,B)
& full_subnetstr(C,A,B)
& ~ empty_carrier(C) )
=> ! [D] :
( element(D,the_carrier(B))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(C))
=> ! [G] :
( element(G,the_carrier(C))
=> ( ( related(B,D,E)
& E = G
& D = F )
=> related(C,F,G) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f615,negated_conjecture,
~ ! [A] :
( one_sorted_str(A)
=> ! [B] :
( ( net_str(B,A)
& ~ empty_carrier(B) )
=> ! [C] :
( ( subnetstr(C,A,B)
& full_subnetstr(C,A,B)
& ~ empty_carrier(C) )
=> ! [D] :
( element(D,the_carrier(B))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(C))
=> ! [G] :
( element(G,the_carrier(C))
=> ( ( related(B,D,E)
& E = G
& D = F )
=> related(C,F,G) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f614]) ).
fof(f729,lemma,
! [A] :
( rel_str(A)
=> ! [B] :
( ( subrelstr(B,A)
& full_subrelstr(B,A) )
=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(B))
=> ( ( in(F,the_carrier(B))
& in(E,the_carrier(B))
& related(A,C,D)
& F = D
& E = C )
=> related(B,E,F) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f747,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1279,plain,
! [A] :
( ( empty_carrier(A)
<=> empty(the_carrier(A)) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f105]) ).
fof(f1280,plain,
! [A] :
( ( ( ~ empty(the_carrier(A))
| empty_carrier(A) )
& ( empty(the_carrier(A))
| ~ empty_carrier(A) ) )
| ~ one_sorted_str(A) ),
inference(NNF_transformation,[status(thm)],[f1279]) ).
fof(f1282,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1280]) ).
fof(f1394,plain,
! [A,B] :
( ( ( element(B,A)
<=> empty(B) )
| ~ empty(A) )
& ( ( element(B,A)
<=> in(B,A) )
| empty(A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f124]) ).
fof(f1395,plain,
! [A,B] :
( ( ( ( ~ empty(B)
| element(B,A) )
& ( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ( ( ( ~ in(B,A)
| element(B,A) )
& ( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(NNF_transformation,[status(thm)],[f1394]) ).
fof(f1396,plain,
( ! [A] :
( ( ! [B] :
( ~ empty(B)
| element(B,A) )
& ! [B] :
( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ! [A] :
( ( ! [B] :
( ~ in(B,A)
| element(B,A) )
& ! [B] :
( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(miniscoping,[status(thm)],[f1395]) ).
fof(f1397,plain,
! [X0,X1] :
( in(X1,X0)
| ~ element(X1,X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f1396]) ).
fof(f1792,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( subnetstr(C,A,B)
<=> ( the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
& subrelstr(C,B) ) )
| ~ net_str(C,A) )
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f181]) ).
fof(f1793,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( the_mapping(A,C) != relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
| ~ subrelstr(C,B)
| subnetstr(C,A,B) )
& ( ( the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
& subrelstr(C,B) )
| ~ subnetstr(C,A,B) ) )
| ~ net_str(C,A) )
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(NNF_transformation,[status(thm)],[f1792]) ).
fof(f1794,plain,
! [X0,X1,X2] :
( subrelstr(X2,X1)
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X2,X0)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1793]) ).
fof(f1824,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( full_subnetstr(C,A,B)
<=> ( subrelstr(C,B)
& full_subrelstr(C,B) ) )
| ~ subnetstr(C,A,B) )
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f187]) ).
fof(f1825,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ subrelstr(C,B)
| ~ full_subrelstr(C,B)
| full_subnetstr(C,A,B) )
& ( ( subrelstr(C,B)
& full_subrelstr(C,B) )
| ~ full_subnetstr(C,A,B) ) )
| ~ subnetstr(C,A,B) )
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(NNF_transformation,[status(thm)],[f1824]) ).
fof(f1826,plain,
! [X0,X1,X2] :
( full_subrelstr(X2,X1)
| ~ full_subnetstr(X2,X0,X1)
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1825]) ).
fof(f1970,plain,
! [A] :
( one_sorted_str(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f269]) ).
fof(f1971,plain,
! [X0] :
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1970]) ).
fof(f1974,plain,
! [A] :
( ! [B] :
( rel_str(B)
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f272]) ).
fof(f1975,plain,
! [X0,X1] :
( rel_str(X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1974]) ).
fof(f1985,plain,
! [A,B] :
( ! [C] :
( net_str(C,A)
| ~ subnetstr(C,A,B) )
| ~ net_str(B,A)
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f279]) ).
fof(f1986,plain,
! [X0,X1,X2] :
( net_str(X2,X0)
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1985]) ).
fof(f3619,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f601]) ).
fof(f3620,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3619]) ).
fof(f3665,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ? [F] :
( ? [G] :
( ~ related(C,F,G)
& related(B,D,E)
& E = G
& D = F
& element(G,the_carrier(C)) )
& element(F,the_carrier(C)) )
& element(E,the_carrier(B)) )
& element(D,the_carrier(B)) )
& subnetstr(C,A,B)
& full_subnetstr(C,A,B)
& ~ empty_carrier(C) )
& net_str(B,A)
& ~ empty_carrier(B) )
& one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f615]) ).
fof(f3666,plain,
( ~ related(sK411_skl,sK414_skl,sK415_skl)
& related(sK410_skl,sK412_skl,sK413_skl)
& sK413_skl = sK415_skl
& sK412_skl = sK414_skl
& element(sK415_skl,the_carrier(sK411_skl))
& element(sK414_skl,the_carrier(sK411_skl))
& element(sK413_skl,the_carrier(sK410_skl))
& element(sK412_skl,the_carrier(sK410_skl))
& subnetstr(sK411_skl,sK409_skl,sK410_skl)
& full_subnetstr(sK411_skl,sK409_skl,sK410_skl)
& ~ empty_carrier(sK411_skl)
& net_str(sK410_skl,sK409_skl)
& ~ empty_carrier(sK410_skl)
& one_sorted_str(sK409_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK409_skl,sK410_skl,sK411_skl,sK412_skl,sK413_skl,sK414_skl,sK415_skl]),skolemize(A,sK409_skl),skolemize(B,sK410_skl),skolemize(C,sK411_skl),skolemize(D,sK412_skl),skolemize(E,sK413_skl),skolemize(F,sK414_skl),skolemize(G,sK415_skl)],[f3665]) ).
fof(f3667,plain,
one_sorted_str(sK409_skl),
inference(cnf_transformation,[status(thm)],[f3666]) ).
fof(f3669,plain,
net_str(sK410_skl,sK409_skl),
inference(cnf_transformation,[status(thm)],[f3666]) ).
fof(f3670,plain,
~ empty_carrier(sK411_skl),
inference(cnf_transformation,[status(thm)],[f3666]) ).
fof(f3671,plain,
full_subnetstr(sK411_skl,sK409_skl,sK410_skl),
inference(cnf_transformation,[status(thm)],[f3666]) ).
fof(f3672,plain,
subnetstr(sK411_skl,sK409_skl,sK410_skl),
inference(cnf_transformation,[status(thm)],[f3666]) ).
fof(f3673,plain,
element(sK412_skl,the_carrier(sK410_skl)),
inference(cnf_transformation,[status(thm)],[f3666]) ).
fof(f3674,plain,
element(sK413_skl,the_carrier(sK410_skl)),
inference(cnf_transformation,[status(thm)],[f3666]) ).
fof(f3675,plain,
element(sK414_skl,the_carrier(sK411_skl)),
inference(cnf_transformation,[status(thm)],[f3666]) ).
fof(f3676,plain,
element(sK415_skl,the_carrier(sK411_skl)),
inference(cnf_transformation,[status(thm)],[f3666]) ).
fof(f3677,plain,
sK412_skl = sK414_skl,
inference(cnf_transformation,[status(thm)],[f3666]) ).
fof(f3678,plain,
sK413_skl = sK415_skl,
inference(cnf_transformation,[status(thm)],[f3666]) ).
fof(f3679,plain,
related(sK410_skl,sK412_skl,sK413_skl),
inference(cnf_transformation,[status(thm)],[f3666]) ).
fof(f3680,plain,
~ related(sK411_skl,sK414_skl,sK415_skl),
inference(cnf_transformation,[status(thm)],[f3666]) ).
fof(f4067,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( related(B,E,F)
| ~ in(F,the_carrier(B))
| ~ in(E,the_carrier(B))
| ~ related(A,C,D)
| F != D
| E != C
| ~ element(F,the_carrier(B)) )
| ~ element(E,the_carrier(B)) )
| ~ element(D,the_carrier(A)) )
| ~ element(C,the_carrier(A)) )
| ~ subrelstr(B,A)
| ~ full_subrelstr(B,A) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f729]) ).
fof(f4068,plain,
! [X0,X1,X2,X3,X4,X5] :
( related(X1,X4,X5)
| ~ in(X5,the_carrier(X1))
| ~ in(X4,the_carrier(X1))
| ~ related(X0,X2,X3)
| X5 != X3
| X4 != X2
| ~ element(X5,the_carrier(X1))
| ~ element(X4,the_carrier(X1))
| ~ element(X3,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ subrelstr(X1,X0)
| ~ full_subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f4067]) ).
fof(f4127,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f747]) ).
fof(f4128,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f4127]) ).
fof(f4129,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4128]) ).
fof(f4939,plain,
! [X0,X1,X2] :
( subrelstr(X2,X1)
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1794,f1986]) ).
fof(f5060,plain,
element(sK412_skl,the_carrier(sK411_skl)),
inference(backward_demodulation,[status(thm)],[f3677,f3675]) ).
fof(f5061,plain,
element(sK413_skl,the_carrier(sK411_skl)),
inference(backward_demodulation,[status(thm)],[f3678,f3676]) ).
fof(f5062,plain,
~ related(sK411_skl,sK412_skl,sK415_skl),
inference(forward_demodulation,[status(thm)],[f3677,f3680]) ).
fof(f5063,plain,
~ related(sK411_skl,sK412_skl,sK413_skl),
inference(forward_demodulation,[status(thm)],[f3678,f5062]) ).
fof(f5112,plain,
! [X0,X1,X2,X3] :
( related(X1,X2,X3)
| ~ in(X3,the_carrier(X1))
| ~ in(X2,the_carrier(X1))
| ~ related(X0,X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ element(X3,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ subrelstr(X1,X0)
| ~ full_subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f4068]) ).
fof(f5113,plain,
! [X0,X1,X2,X3] :
( related(X1,X2,X3)
| ~ in(X3,the_carrier(X1))
| ~ in(X2,the_carrier(X1))
| ~ related(X0,X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ element(X3,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ subrelstr(X1,X0)
| ~ full_subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5112,f3620]) ).
fof(f5270,plain,
( full_subrelstr(sK411_skl,sK410_skl)
| ~ subnetstr(sK411_skl,sK409_skl,sK410_skl)
| ~ net_str(sK410_skl,sK409_skl)
| ~ one_sorted_str(sK409_skl) ),
inference(resolution,[status(thm)],[f1826,f3671]) ).
fof(f5271,plain,
( full_subrelstr(sK411_skl,sK410_skl)
| ~ subnetstr(sK411_skl,sK409_skl,sK410_skl)
| ~ net_str(sK410_skl,sK409_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f5270,f3667]) ).
fof(f5283,plain,
( rel_str(sK410_skl)
| ~ one_sorted_str(sK409_skl) ),
inference(resolution,[status(thm)],[f1975,f3669]) ).
fof(f5284,plain,
rel_str(sK410_skl),
inference(forward_subsumption_resolution,[status(thm)],[f5283,f3667]) ).
fof(f5287,plain,
( net_str(sK411_skl,sK409_skl)
| ~ net_str(sK410_skl,sK409_skl)
| ~ one_sorted_str(sK409_skl) ),
inference(resolution,[status(thm)],[f1986,f3672]) ).
fof(f5288,plain,
( net_str(sK411_skl,sK409_skl)
| ~ net_str(sK410_skl,sK409_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f5287,f3667]) ).
fof(f5303,plain,
( full_subrelstr(sK411_skl,sK410_skl)
| ~ net_str(sK410_skl,sK409_skl) ),
inference(resolution,[status(thm)],[f5271,f3672]) ).
fof(f5304,plain,
full_subrelstr(sK411_skl,sK410_skl),
inference(forward_subsumption_resolution,[status(thm)],[f5303,f3669]) ).
fof(f5307,plain,
! [X0,X1] :
( related(sK411_skl,X0,X1)
| ~ in(X1,the_carrier(sK411_skl))
| ~ in(X0,the_carrier(sK411_skl))
| ~ related(sK410_skl,X0,X1)
| ~ element(X1,the_carrier(sK411_skl))
| ~ element(X1,the_carrier(sK410_skl))
| ~ element(X0,the_carrier(sK410_skl))
| ~ subrelstr(sK411_skl,sK410_skl)
| ~ rel_str(sK410_skl) ),
inference(resolution,[status(thm)],[f5113,f5304]) ).
fof(f5308,plain,
! [X0,X1] :
( related(sK411_skl,X0,X1)
| ~ in(X1,the_carrier(sK411_skl))
| ~ in(X0,the_carrier(sK411_skl))
| ~ related(sK410_skl,X0,X1)
| ~ element(X1,the_carrier(sK411_skl))
| ~ element(X1,the_carrier(sK410_skl))
| ~ element(X0,the_carrier(sK410_skl))
| ~ subrelstr(sK411_skl,sK410_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f5307,f5284]) ).
fof(f5323,plain,
( subrelstr(sK411_skl,sK410_skl)
| ~ net_str(sK410_skl,sK409_skl)
| ~ one_sorted_str(sK409_skl) ),
inference(resolution,[status(thm)],[f4939,f3672]) ).
fof(f5324,plain,
( subrelstr(sK411_skl,sK410_skl)
| ~ net_str(sK410_skl,sK409_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f5323,f3667]) ).
fof(f5337,plain,
net_str(sK411_skl,sK409_skl),
inference(resolution,[status(thm)],[f5288,f3669]) ).
fof(f5338,plain,
( rel_str(sK411_skl)
| ~ one_sorted_str(sK409_skl) ),
inference(resolution,[status(thm)],[f5337,f1975]) ).
fof(f5339,plain,
rel_str(sK411_skl),
inference(forward_subsumption_resolution,[status(thm)],[f5338,f3667]) ).
fof(f5340,plain,
one_sorted_str(sK411_skl),
inference(resolution,[status(thm)],[f5339,f1971]) ).
fof(f5371,plain,
subrelstr(sK411_skl,sK410_skl),
inference(resolution,[status(thm)],[f5324,f3669]) ).
fof(f5372,plain,
! [X0,X1] :
( related(sK411_skl,X0,X1)
| ~ in(X1,the_carrier(sK411_skl))
| ~ in(X0,the_carrier(sK411_skl))
| ~ related(sK410_skl,X0,X1)
| ~ element(X1,the_carrier(sK411_skl))
| ~ element(X1,the_carrier(sK410_skl))
| ~ element(X0,the_carrier(sK410_skl)) ),
inference(backward_subsumption_resolution,[status(thm)],[f5308,f5371]) ).
fof(f5373,plain,
! [X0,X1] :
( related(sK411_skl,X0,X1)
| ~ in(X1,the_carrier(sK411_skl))
| ~ in(X0,the_carrier(sK411_skl))
| ~ related(sK410_skl,X0,X1)
| ~ element(X1,the_carrier(sK410_skl))
| ~ element(X0,the_carrier(sK410_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5372,f3620]) ).
fof(f5391,plain,
( related(sK411_skl,sK412_skl,sK413_skl)
| ~ in(sK413_skl,the_carrier(sK411_skl))
| ~ in(sK412_skl,the_carrier(sK411_skl))
| ~ element(sK413_skl,the_carrier(sK410_skl))
| ~ element(sK412_skl,the_carrier(sK410_skl)) ),
inference(resolution,[status(thm)],[f5373,f3679]) ).
fof(f5392,plain,
( related(sK411_skl,sK412_skl,sK413_skl)
| ~ in(sK413_skl,the_carrier(sK411_skl))
| ~ in(sK412_skl,the_carrier(sK411_skl))
| ~ element(sK413_skl,the_carrier(sK410_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5391,f3673]) ).
fof(f5393,plain,
( related(sK411_skl,sK412_skl,sK413_skl)
| ~ in(sK413_skl,the_carrier(sK411_skl))
| ~ in(sK412_skl,the_carrier(sK411_skl)) ),
inference(resolution,[status(thm)],[f5392,f3674]) ).
fof(f5394,plain,
( ~ in(sK413_skl,the_carrier(sK411_skl))
| ~ in(sK412_skl,the_carrier(sK411_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5393,f5063]) ).
fof(f13079,plain,
( in(sK413_skl,the_carrier(sK411_skl))
| empty(the_carrier(sK411_skl)) ),
inference(resolution,[status(thm)],[f1397,f5061]) ).
fof(f13081,plain,
( in(sK412_skl,the_carrier(sK411_skl))
| empty(the_carrier(sK411_skl)) ),
inference(resolution,[status(thm)],[f1397,f5060]) ).
fof(f13133,plain,
( ~ in(sK412_skl,the_carrier(sK411_skl))
| empty(the_carrier(sK411_skl)) ),
inference(resolution,[status(thm)],[f13079,f5394]) ).
fof(f13139,plain,
empty(the_carrier(sK411_skl)),
inference(backward_subsumption_resolution,[status(thm)],[f13081,f13140]) ).
fof(f13140,plain,
~ in(sK412_skl,the_carrier(sK411_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f13133,f4129]) ).
fof(f14295,plain,
( empty_carrier(sK411_skl)
| ~ one_sorted_str(sK411_skl) ),
inference(resolution,[status(thm)],[f13139,f1282]) ).
fof(f14312,plain,
empty_carrier(sK411_skl),
inference(forward_subsumption_resolution,[status(thm)],[f14295,f5340]) ).
fof(f14313,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f3670,f14312]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU375+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 06:16:56 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.13/0.48 % Drodi V4.1.1
% 58.22/8.05 % Refutation found
% 58.22/8.05 % SZS status Theorem for theBenchmark: Theorem is valid
% 58.22/8.05 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 58.22/8.16 % Elapsed time: 7.771517 seconds
% 58.22/8.16 % CPU time: 60.638886 seconds
% 58.22/8.16 % Total memory used: 466.221 MB
% 58.22/8.16 % Net memory used: 443.502 MB
%------------------------------------------------------------------------------