%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU363+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 : n012.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:18 PM UTC 2026
% Result : Theorem 0.12s 0.34s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 29
% Syntax : Number of formulae : 144 ( 31 unt; 15 def)
% Number of atoms : 394 ( 33 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 401 ( 151 ~; 152 |; 48 &)
% ( 22 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 16 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-2 aty)
% Number of variables : 151 ( 144 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
=> relation(C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( subrelstr(B,A)
=> ( full_subrelstr(B,A)
<=> the_InternalRel(B) = relation_restriction_as_relation_of(the_InternalRel(A),the_carrier(B)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( related(A,B,C)
<=> in(ordered_pair(B,C),the_InternalRel(A)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( subrelstr(B,A)
=> rel_str(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> element(C,powerset(cartesian_product2(A,B))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( rel_str(A)
=> relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [A,B] :
( relation(A)
=> relation_restriction_as_relation_of(A,B) = relation_restriction(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [A,B,C,D] :
( in(ordered_pair(A,B),cartesian_product2(C,D))
<=> ( in(B,D)
& in(A,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A,B,C] :
( relation(C)
=> ( in(A,relation_restriction(C,B))
<=> ( in(A,cartesian_product2(B,B))
& in(A,C) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,conjecture,
! [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/sandbox/benchmark/theBenchmark.p') ).
fof(f45,negated_conjecture,
~ ! [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) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f44]) ).
fof(f46,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,plain,
! [A,B,C] :
( relation(C)
| ~ element(C,powerset(cartesian_product2(A,B))) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f54,plain,
! [C] :
( relation(C)
| ! [A,B] : ~ element(C,powerset(cartesian_product2(A,B))) ),
inference(miniscoping,[status(thm)],[f53]) ).
fof(f55,plain,
! [X0,X1,X2] :
( relation(X0)
| ~ element(X0,powerset(cartesian_product2(X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f58,plain,
! [A] :
( ! [B] :
( ( full_subrelstr(B,A)
<=> the_InternalRel(B) = relation_restriction_as_relation_of(the_InternalRel(A),the_carrier(B)) )
| ~ subrelstr(B,A) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f59,plain,
! [A] :
( ! [B] :
( ( ( the_InternalRel(B) != relation_restriction_as_relation_of(the_InternalRel(A),the_carrier(B))
| full_subrelstr(B,A) )
& ( the_InternalRel(B) = relation_restriction_as_relation_of(the_InternalRel(A),the_carrier(B))
| ~ full_subrelstr(B,A) ) )
| ~ subrelstr(B,A) )
| ~ rel_str(A) ),
inference(NNF_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
! [X0,X1] :
( the_InternalRel(X1) = relation_restriction_as_relation_of(the_InternalRel(X0),the_carrier(X1))
| ~ full_subrelstr(X1,X0)
| ~ subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f62,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( related(A,B,C)
<=> in(ordered_pair(B,C),the_InternalRel(A)) )
| ~ element(C,the_carrier(A)) )
| ~ element(B,the_carrier(A)) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f63,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ in(ordered_pair(B,C),the_InternalRel(A))
| related(A,B,C) )
& ( in(ordered_pair(B,C),the_InternalRel(A))
| ~ related(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ element(B,the_carrier(A)) )
| ~ rel_str(A) ),
inference(NNF_transformation,[status(thm)],[f62]) ).
fof(f64,plain,
! [X0,X1,X2] :
( in(ordered_pair(X1,X2),the_InternalRel(X0))
| ~ related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f65,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,X2),the_InternalRel(X0))
| related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f74,plain,
! [A] :
( ! [B] :
( rel_str(B)
| ~ subrelstr(B,A) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f75,plain,
! [X0,X1] :
( rel_str(X1)
| ~ subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f76,plain,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
| ~ relation_of2_as_subset(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f77,plain,
! [X0,X1,X2] :
( element(X0,powerset(cartesian_product2(X1,X2)))
| ~ relation_of2_as_subset(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
! [A] :
( relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A))
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f79,plain,
! [X0] :
( relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f99,plain,
empty(sK7_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(A,sK7_skl)],[f30]) ).
fof(f100,plain,
empty(sK7_skl),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f113,plain,
! [A,B] :
( relation_restriction_as_relation_of(A,B) = relation_restriction(A,B)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f114,plain,
! [A] :
( ! [B] : relation_restriction_as_relation_of(A,B) = relation_restriction(A,B)
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f113]) ).
fof(f115,plain,
! [X0,X1] :
( relation_restriction_as_relation_of(X0,X1) = relation_restriction(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f122,plain,
! [A,B,C,D] :
( ( ~ in(B,D)
| ~ in(A,C)
| in(ordered_pair(A,B),cartesian_product2(C,D)) )
& ( ( in(B,D)
& in(A,C) )
| ~ in(ordered_pair(A,B),cartesian_product2(C,D)) ) ),
inference(NNF_transformation,[status(thm)],[f37]) ).
fof(f123,plain,
( ! [A,B,C,D] :
( ~ in(B,D)
| ~ in(A,C)
| in(ordered_pair(A,B),cartesian_product2(C,D)) )
& ! [A,B,C,D] :
( ( in(B,D)
& in(A,C) )
| ~ in(ordered_pair(A,B),cartesian_product2(C,D)) ) ),
inference(miniscoping,[status(thm)],[f122]) ).
fof(f126,plain,
! [X0,X1,X2,X3] :
( ~ in(X1,X3)
| ~ in(X0,X2)
| in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f127,plain,
! [A,B,C] :
( ( in(A,relation_restriction(C,B))
<=> ( in(A,cartesian_product2(B,B))
& in(A,C) ) )
| ~ relation(C) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f128,plain,
! [A,B,C] :
( ( ( ~ in(A,cartesian_product2(B,B))
| ~ in(A,C)
| in(A,relation_restriction(C,B)) )
& ( ( in(A,cartesian_product2(B,B))
& in(A,C) )
| ~ in(A,relation_restriction(C,B)) ) )
| ~ relation(C) ),
inference(NNF_transformation,[status(thm)],[f127]) ).
fof(f129,plain,
! [C] :
( ( ! [A,B] :
( ~ in(A,cartesian_product2(B,B))
| ~ in(A,C)
| in(A,relation_restriction(C,B)) )
& ! [A,B] :
( ( in(A,cartesian_product2(B,B))
& in(A,C) )
| ~ in(A,relation_restriction(C,B)) ) )
| ~ relation(C) ),
inference(miniscoping,[status(thm)],[f128]) ).
fof(f132,plain,
! [X0,X1,X2] :
( ~ in(X1,cartesian_product2(X2,X2))
| ~ in(X1,X0)
| in(X1,relation_restriction(X0,X2))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f135,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f136,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f147,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)],[f45]) ).
fof(f148,plain,
( ~ related(sK12_skl,sK15_skl,sK16_skl)
& in(sK16_skl,the_carrier(sK12_skl))
& in(sK15_skl,the_carrier(sK12_skl))
& related(sK11_skl,sK13_skl,sK14_skl)
& sK16_skl = sK14_skl
& sK15_skl = sK13_skl
& element(sK16_skl,the_carrier(sK12_skl))
& element(sK15_skl,the_carrier(sK12_skl))
& element(sK14_skl,the_carrier(sK11_skl))
& element(sK13_skl,the_carrier(sK11_skl))
& subrelstr(sK12_skl,sK11_skl)
& full_subrelstr(sK12_skl,sK11_skl)
& rel_str(sK11_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl,sK16_skl]),skolemize(A,sK11_skl),skolemize(B,sK12_skl),skolemize(C,sK13_skl),skolemize(D,sK14_skl),skolemize(E,sK15_skl),skolemize(F,sK16_skl)],[f147]) ).
fof(f149,plain,
rel_str(sK11_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f150,plain,
full_subrelstr(sK12_skl,sK11_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f151,plain,
subrelstr(sK12_skl,sK11_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f152,plain,
element(sK13_skl,the_carrier(sK11_skl)),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f153,plain,
element(sK14_skl,the_carrier(sK11_skl)),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f154,plain,
element(sK15_skl,the_carrier(sK12_skl)),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f155,plain,
element(sK16_skl,the_carrier(sK12_skl)),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f156,plain,
sK15_skl = sK13_skl,
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f157,plain,
sK16_skl = sK14_skl,
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f158,plain,
related(sK11_skl,sK13_skl,sK14_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f159,plain,
in(sK15_skl,the_carrier(sK12_skl)),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f160,plain,
in(sK16_skl,the_carrier(sK12_skl)),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f161,plain,
~ related(sK12_skl,sK15_skl,sK16_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f162,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f163,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f164,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f165,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f164]) ).
fof(f166,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f170,plain,
( the_InternalRel(sK12_skl) = relation_restriction_as_relation_of(the_InternalRel(sK11_skl),the_carrier(sK12_skl))
| ~ full_subrelstr(sK12_skl,sK11_skl)
| ~ rel_str(sK11_skl) ),
inference(resolution,[status(thm)],[f151,f60]) ).
fof(f171,definition,
( sQ0_spl
<=> rel_str(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f173,plain,
( sQ0_spl
| ~ rel_str(sK11_skl) ),
inference(component_clause,[status(thm)],[f171]) ).
fof(f174,definition,
( sQ1_spl
<=> full_subrelstr(sK12_skl,sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f176,plain,
( sQ1_spl
| ~ full_subrelstr(sK12_skl,sK11_skl) ),
inference(component_clause,[status(thm)],[f174]) ).
fof(f177,definition,
( sQ2_spl
<=> the_InternalRel(sK12_skl) = relation_restriction_as_relation_of(the_InternalRel(sK11_skl),the_carrier(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f178,plain,
( ~ sQ2_spl
| the_InternalRel(sK12_skl) = relation_restriction_as_relation_of(the_InternalRel(sK11_skl),the_carrier(sK12_skl)) ),
inference(component_clause,[status(thm)],[f177]) ).
fof(f180,plain,
( sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f170,f171,f174,f177]) ).
fof(f181,plain,
element(sK15_skl,the_carrier(sK11_skl)),
inference(forward_demodulation,[status(thm)],[f156,f152]) ).
fof(f182,plain,
element(sK16_skl,the_carrier(sK11_skl)),
inference(forward_demodulation,[status(thm)],[f157,f153]) ).
fof(f183,plain,
related(sK11_skl,sK15_skl,sK14_skl),
inference(forward_demodulation,[status(thm)],[f156,f158]) ).
fof(f184,plain,
related(sK11_skl,sK15_skl,sK16_skl),
inference(forward_demodulation,[status(thm)],[f157,f183]) ).
fof(f185,plain,
( in(ordered_pair(sK15_skl,sK16_skl),the_InternalRel(sK11_skl))
| ~ element(sK16_skl,the_carrier(sK11_skl))
| ~ element(sK15_skl,the_carrier(sK11_skl))
| ~ rel_str(sK11_skl) ),
inference(resolution,[status(thm)],[f184,f64]) ).
fof(f186,definition,
( sQ3_spl
<=> element(sK15_skl,the_carrier(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f188,plain,
( sQ3_spl
| ~ element(sK15_skl,the_carrier(sK11_skl)) ),
inference(component_clause,[status(thm)],[f186]) ).
fof(f189,definition,
( sQ4_spl
<=> element(sK16_skl,the_carrier(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f191,plain,
( sQ4_spl
| ~ element(sK16_skl,the_carrier(sK11_skl)) ),
inference(component_clause,[status(thm)],[f189]) ).
fof(f192,definition,
( sQ5_spl
<=> in(ordered_pair(sK15_skl,sK16_skl),the_InternalRel(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f193,plain,
( ~ sQ5_spl
| in(ordered_pair(sK15_skl,sK16_skl),the_InternalRel(sK11_skl)) ),
inference(component_clause,[status(thm)],[f192]) ).
fof(f195,plain,
( sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f185,f171,f186,f189,f192]) ).
fof(f196,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f173,f149]) ).
fof(f197,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f196]) ).
fof(f198,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f176,f150]) ).
fof(f199,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f198]) ).
fof(f208,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f191,f182]) ).
fof(f209,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f208]) ).
fof(f210,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f188,f181]) ).
fof(f211,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f210]) ).
fof(f223,definition,
( sQ9_spl
<=> relation(the_InternalRel(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f224,plain,
( ~ sQ9_spl
| relation(the_InternalRel(sK11_skl)) ),
inference(component_clause,[status(thm)],[f223]) ).
fof(f225,plain,
( sQ9_spl
| ~ relation(the_InternalRel(sK11_skl)) ),
inference(component_clause,[status(thm)],[f223]) ).
fof(f233,plain,
sK7_skl = empty_set,
inference(resolution,[status(thm)],[f163,f100]) ).
fof(f235,plain,
! [X0] :
( X0 = sK7_skl
| ~ empty(X0) ),
inference(backward_demodulation,[status(thm)],[f233,f163]) ).
fof(f239,plain,
! [X0,X1] :
( sQ9_spl
| ~ element(the_InternalRel(sK11_skl),powerset(cartesian_product2(X0,X1))) ),
inference(resolution,[status(thm)],[f225,f55]) ).
fof(f240,plain,
! [X0,X1] :
( sQ9_spl
| ~ relation_of2_as_subset(the_InternalRel(sK11_skl),X0,X1) ),
inference(resolution,[status(thm)],[f239,f77]) ).
fof(f242,plain,
( sQ9_spl
| ~ rel_str(sK11_skl) ),
inference(resolution,[status(thm)],[f240,f79]) ).
fof(f243,plain,
( sQ9_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f242,f171,f223]) ).
fof(f245,plain,
! [X0] : ~ in(X0,sK7_skl),
inference(resolution,[status(thm)],[f166,f100]) ).
fof(f246,plain,
! [X0] :
( ~ sQ9_spl
| relation_restriction_as_relation_of(the_InternalRel(sK11_skl),X0) = relation_restriction(the_InternalRel(sK11_skl),X0) ),
inference(resolution,[status(thm)],[f115,f224]) ).
fof(f261,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| the_InternalRel(sK12_skl) = relation_restriction(the_InternalRel(sK11_skl),the_carrier(sK12_skl)) ),
inference(backward_demodulation,[status(thm)],[f246,f178]) ).
fof(f281,definition,
( sQ16_spl
<=> rel_str(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f283,plain,
( sQ16_spl
| ~ rel_str(sK12_skl) ),
inference(component_clause,[status(thm)],[f281]) ).
fof(f297,plain,
! [X0] :
( sQ16_spl
| ~ subrelstr(sK12_skl,X0)
| ~ rel_str(X0) ),
inference(resolution,[status(thm)],[f283,f75]) ).
fof(f316,plain,
! [X0,X1] :
( X1 = sK7_skl
| in(X0,X1)
| ~ element(X0,X1) ),
inference(resolution,[status(thm)],[f136,f235]) ).
fof(f317,plain,
( sQ16_spl
| ~ rel_str(sK11_skl) ),
inference(resolution,[status(thm)],[f297,f151]) ).
fof(f318,plain,
( sQ16_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f317,f171,f281]) ).
fof(f329,plain,
! [X0,X1,X2,X3] :
( ~ in(ordered_pair(X0,X2),X3)
| in(ordered_pair(X0,X2),relation_restriction(X3,X1))
| ~ relation(X3)
| ~ in(X2,X1)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f126,f132]) ).
fof(f438,plain,
( the_carrier(sK12_skl) = sK7_skl
| in(sK15_skl,the_carrier(sK12_skl)) ),
inference(resolution,[status(thm)],[f316,f154]) ).
fof(f447,definition,
( sQ34_spl
<=> the_carrier(sK12_skl) = sK7_skl ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f448,plain,
( ~ sQ34_spl
| the_carrier(sK12_skl) = sK7_skl ),
inference(component_clause,[status(thm)],[f447]) ).
fof(f458,definition,
( sQ37_spl
<=> in(sK15_skl,the_carrier(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f461,plain,
( sQ34_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f438,f458,f447]) ).
fof(f483,plain,
( ~ sQ34_spl
| in(sK15_skl,sK7_skl) ),
inference(backward_demodulation,[status(thm)],[f448,f159]) ).
fof(f497,plain,
( ~ sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f483,f245]) ).
fof(f498,plain,
~ sQ34_spl,
inference(contradiction_clause,[status(thm)],[f497]) ).
fof(f589,plain,
! [X0] :
( ~ sQ5_spl
| in(ordered_pair(sK15_skl,sK16_skl),relation_restriction(the_InternalRel(sK11_skl),X0))
| ~ relation(the_InternalRel(sK11_skl))
| ~ in(sK16_skl,X0)
| ~ in(sK15_skl,X0) ),
inference(resolution,[status(thm)],[f329,f193]) ).
fof(f593,definition,
! [X0] :
( sQ49_spl
<=> ( in(ordered_pair(sK15_skl,sK16_skl),relation_restriction(the_InternalRel(sK11_skl),X0))
| ~ in(sK16_skl,X0)
| ~ in(sK15_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f594,plain,
! [X0] :
( ~ sQ49_spl
| in(ordered_pair(sK15_skl,sK16_skl),relation_restriction(the_InternalRel(sK11_skl),X0))
| ~ in(sK16_skl,X0)
| ~ in(sK15_skl,X0) ),
inference(component_clause,[status(thm)],[f593]) ).
fof(f596,plain,
( ~ sQ5_spl
| ~ sQ9_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f589,f593,f223,f192]) ).
fof(f787,plain,
( ~ sQ49_spl
| in(ordered_pair(sK15_skl,sK16_skl),relation_restriction(the_InternalRel(sK11_skl),the_carrier(sK12_skl)))
| ~ in(sK15_skl,the_carrier(sK12_skl)) ),
inference(resolution,[status(thm)],[f594,f160]) ).
fof(f794,definition,
( sQ75_spl
<=> in(ordered_pair(sK15_skl,sK16_skl),relation_restriction(the_InternalRel(sK11_skl),the_carrier(sK12_skl))) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f795,plain,
( ~ sQ75_spl
| in(ordered_pair(sK15_skl,sK16_skl),relation_restriction(the_InternalRel(sK11_skl),the_carrier(sK12_skl))) ),
inference(component_clause,[status(thm)],[f794]) ).
fof(f797,plain,
( ~ sQ49_spl
| sQ75_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f787,f458,f794,f593]) ).
fof(f808,plain,
( ~ sQ75_spl
| ~ sQ2_spl
| ~ sQ9_spl
| in(ordered_pair(sK15_skl,sK16_skl),the_InternalRel(sK12_skl)) ),
inference(forward_demodulation,[status(thm)],[f261,f795]) ).
fof(f999,plain,
( ~ sQ75_spl
| ~ sQ2_spl
| ~ sQ9_spl
| related(sK12_skl,sK15_skl,sK16_skl)
| ~ element(sK16_skl,the_carrier(sK12_skl))
| ~ element(sK15_skl,the_carrier(sK12_skl))
| ~ rel_str(sK12_skl) ),
inference(resolution,[status(thm)],[f808,f65]) ).
fof(f1005,definition,
( sQ91_spl
<=> element(sK15_skl,the_carrier(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1007,plain,
( sQ91_spl
| ~ element(sK15_skl,the_carrier(sK12_skl)) ),
inference(component_clause,[status(thm)],[f1005]) ).
fof(f1008,definition,
( sQ92_spl
<=> element(sK16_skl,the_carrier(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1010,plain,
( sQ92_spl
| ~ element(sK16_skl,the_carrier(sK12_skl)) ),
inference(component_clause,[status(thm)],[f1008]) ).
fof(f1011,definition,
( sQ93_spl
<=> related(sK12_skl,sK15_skl,sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1012,plain,
( ~ sQ93_spl
| related(sK12_skl,sK15_skl,sK16_skl) ),
inference(component_clause,[status(thm)],[f1011]) ).
fof(f1014,plain,
( ~ sQ75_spl
| ~ sQ2_spl
| ~ sQ9_spl
| sQ93_spl
| ~ sQ92_spl
| ~ sQ91_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f999,f281,f1005,f1008,f1011,f223,f177,f794]) ).
fof(f1019,plain,
( ~ sQ93_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1012,f161]) ).
fof(f1020,plain,
~ sQ93_spl,
inference(contradiction_clause,[status(thm)],[f1019]) ).
fof(f1021,plain,
( sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1010,f155]) ).
fof(f1022,plain,
sQ92_spl,
inference(contradiction_clause,[status(thm)],[f1021]) ).
fof(f1023,plain,
( sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1007,f154]) ).
fof(f1024,plain,
sQ91_spl,
inference(contradiction_clause,[status(thm)],[f1023]) ).
fof(f1025,plain,
$false,
inference(sat_refutation,[status(thm)],[f180,f195,f197,f199,f209,f211,f243,f318,f461,f498,f596,f797,f1014,f1020,f1022,f1024]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU363+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 06:15:06 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.03/0.30 % Drodi V4.1.1
% 0.12/0.34 % Refutation found
% 0.12/0.34 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.34 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.35 % Elapsed time: 0.056872 seconds
% 0.12/0.35 % CPU time: 0.265535 seconds
% 0.12/0.35 % Total memory used: 111.193 MB
% 0.12/0.35 % Net memory used: 110.342 MB
%------------------------------------------------------------------------------