%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU252+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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:19:54 PM UTC 2026
% Result : Theorem 0.14s 0.54s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 28
% Syntax : Number of formulae : 131 ( 23 unt; 16 def)
% Number of atoms : 338 ( 16 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 363 ( 156 ~; 145 |; 29 &)
% ( 21 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 17 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 161 ( 155 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A] :
( relation(A)
=> ! [B] : relation_restriction(A,B) = set_intersection2(A,cartesian_product2(B,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A,B] :
( relation(A)
=> relation(relation_restriction(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
( relation(A)
=> ( reflexive(A)
<=> ! [B] :
( in(B,relation_field(A))
=> in(ordered_pair(B,B),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,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(f36,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(f37,axiom,
! [A,B,C] :
( relation(C)
=> ( in(A,relation_field(relation_restriction(C,B)))
=> ( in(A,B)
& in(A,relation_field(C)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,conjecture,
! [A,B] :
( relation(B)
=> ( reflexive(B)
=> reflexive(relation_restriction(B,A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,negated_conjecture,
~ ! [A,B] :
( relation(B)
=> ( reflexive(B)
=> reflexive(relation_restriction(B,A)) ) ),
inference(negated_conjecture,[status(cth)],[f40]) ).
fof(f42,axiom,
! [A] : set_intersection2(A,empty_set) = empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f61,plain,
! [A] :
( ! [B] : relation_restriction(A,B) = set_intersection2(A,cartesian_product2(B,B))
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f62,plain,
! [X0,X1] :
( relation_restriction(X0,X1) = set_intersection2(X0,cartesian_product2(X1,X1))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
! [A,B] :
( relation(relation_restriction(A,B))
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f64,plain,
! [A] :
( ! [B] : relation(relation_restriction(A,B))
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f63]) ).
fof(f65,plain,
! [X0,X1] :
( relation(relation_restriction(X0,X1))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f80,plain,
! [A] :
( ( reflexive(A)
<=> ! [B] :
( in(ordered_pair(B,B),A)
| ~ in(B,relation_field(A)) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f81,plain,
! [A] :
( ( ( ? [B] :
( ~ in(ordered_pair(B,B),A)
& in(B,relation_field(A)) )
| reflexive(A) )
& ( ! [B] :
( in(ordered_pair(B,B),A)
| ~ in(B,relation_field(A)) )
| ~ reflexive(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f80]) ).
fof(f82,plain,
! [A] :
( ( ( ( ~ in(ordered_pair(sK1_skl(A),sK1_skl(A)),A)
& in(sK1_skl(A),relation_field(A)) )
| reflexive(A) )
& ( ! [B] :
( in(ordered_pair(B,B),A)
| ~ in(B,relation_field(A)) )
| ~ reflexive(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B,sK1_skl(A))],[f81]) ).
fof(f83,plain,
! [X0,X1] :
( in(ordered_pair(X1,X1),X0)
| ~ in(X1,relation_field(X0))
| ~ reflexive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f84,plain,
! [X0] :
( in(sK1_skl(X0),relation_field(X0))
| reflexive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f85,plain,
! [X0] :
( ~ in(ordered_pair(sK1_skl(X0),sK1_skl(X0)),X0)
| reflexive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f91,plain,
( function(sK4_skl)
& empty(sK4_skl)
& relation(sK4_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f32]) ).
fof(f92,plain,
relation(sK4_skl),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f93,plain,
empty(sK4_skl),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f101,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)],[f35]) ).
fof(f102,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)],[f101]) ).
fof(f104,plain,
! [X0,X1,X2,X3] :
( in(X1,X3)
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f105,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)],[f102]) ).
fof(f106,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)],[f36]) ).
fof(f107,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)],[f106]) ).
fof(f108,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)],[f107]) ).
fof(f111,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)],[f108]) ).
fof(f112,plain,
! [A,B,C] :
( ( in(A,B)
& in(A,relation_field(C)) )
| ~ in(A,relation_field(relation_restriction(C,B)))
| ~ relation(C) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f113,plain,
! [C] :
( ! [A,B] :
( ( in(A,B)
& in(A,relation_field(C)) )
| ~ in(A,relation_field(relation_restriction(C,B))) )
| ~ relation(C) ),
inference(miniscoping,[status(thm)],[f112]) ).
fof(f114,plain,
! [X0,X1,X2] :
( in(X1,relation_field(X0))
| ~ in(X1,relation_field(relation_restriction(X0,X2)))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [X0,X1,X2] :
( in(X1,X2)
| ~ in(X1,relation_field(relation_restriction(X0,X2)))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f119,plain,
? [A,B] :
( ~ reflexive(relation_restriction(B,A))
& reflexive(B)
& relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f120,plain,
? [B] :
( ? [A] : ~ reflexive(relation_restriction(B,A))
& reflexive(B)
& relation(B) ),
inference(miniscoping,[status(thm)],[f119]) ).
fof(f121,plain,
( ~ reflexive(relation_restriction(sK7_skl,sK8_skl))
& reflexive(sK7_skl)
& relation(sK7_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(B,sK7_skl),skolemize(A,sK8_skl)],[f120]) ).
fof(f122,plain,
relation(sK7_skl),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
reflexive(sK7_skl),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f124,plain,
~ reflexive(relation_restriction(sK7_skl,sK8_skl)),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f125,plain,
! [X0] : set_intersection2(X0,empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f128,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f129,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f131,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f130]) ).
fof(f132,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f147,definition,
( sQ1_spl
<=> relation(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f149,plain,
( sQ1_spl
| ~ relation(sK7_skl) ),
inference(component_clause,[status(thm)],[f147]) ).
fof(f177,plain,
! [X0] : relation_restriction(sK4_skl,X0) = set_intersection2(sK4_skl,cartesian_product2(X0,X0)),
inference(resolution,[status(thm)],[f62,f92]) ).
fof(f201,plain,
sK4_skl = empty_set,
inference(resolution,[status(thm)],[f129,f93]) ).
fof(f241,plain,
! [X0,X1,X2] :
( reflexive(X1)
| ~ relation(X1)
| ~ in(X0,X2)
| in(ordered_pair(X0,sK1_skl(X1)),cartesian_product2(X2,relation_field(X1))) ),
inference(resolution,[status(thm)],[f105,f84]) ).
fof(f242,plain,
! [X0,X1,X2,X3] :
( ~ in(X1,relation_field(X3))
| ~ reflexive(X3)
| ~ relation(X3)
| ~ in(X0,X2)
| in(ordered_pair(X0,ordered_pair(X1,X1)),cartesian_product2(X2,X3)) ),
inference(resolution,[status(thm)],[f105,f83]) ).
fof(f244,plain,
! [X0,X1,X2] :
( ~ in(X1,relation_field(sK7_skl))
| ~ relation(sK7_skl)
| ~ in(X0,X2)
| in(ordered_pair(X0,ordered_pair(X1,X1)),cartesian_product2(X2,sK7_skl)) ),
inference(resolution,[status(thm)],[f242,f123]) ).
fof(f245,definition,
! [X0,X1,X2] :
( sQ2_spl
<=> ( ~ in(X1,relation_field(sK7_skl))
| ~ in(X0,X2)
| in(ordered_pair(X0,ordered_pair(X1,X1)),cartesian_product2(X2,sK7_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f246,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ in(X1,relation_field(sK7_skl))
| ~ in(X0,X2)
| in(ordered_pair(X0,ordered_pair(X1,X1)),cartesian_product2(X2,sK7_skl)) ),
inference(component_clause,[status(thm)],[f245]) ).
fof(f248,plain,
( ~ sQ1_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f244,f245,f147]) ).
fof(f249,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f149,f122]) ).
fof(f250,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f249]) ).
fof(f271,definition,
( sQ4_spl
<=> reflexive(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f273,plain,
( sQ4_spl
| ~ reflexive(sK7_skl) ),
inference(component_clause,[status(thm)],[f271]) ).
fof(f310,plain,
! [X0,X1] :
( reflexive(relation_restriction(X0,X1))
| ~ relation(relation_restriction(X0,X1))
| in(sK1_skl(relation_restriction(X0,X1)),X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f115,f84]) ).
fof(f314,plain,
! [X0,X1] :
( reflexive(relation_restriction(X0,X1))
| in(sK1_skl(relation_restriction(X0,X1)),X1)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f310,f65]) ).
fof(f316,plain,
! [X0] : set_intersection2(X0,sK4_skl) = empty_set,
inference(forward_demodulation,[status(thm)],[f201,f125]) ).
fof(f317,plain,
! [X0] : set_intersection2(X0,sK4_skl) = sK4_skl,
inference(forward_demodulation,[status(thm)],[f201,f316]) ).
fof(f319,plain,
! [X0] : set_intersection2(sK4_skl,X0) = sK4_skl,
inference(paramodulation,[status(thm)],[f57,f317]) ).
fof(f328,plain,
! [X0] :
( reflexive(relation_restriction(sK7_skl,X0))
| in(sK1_skl(relation_restriction(sK7_skl,X0)),X0) ),
inference(resolution,[status(thm)],[f314,f122]) ).
fof(f356,plain,
! [X0] : ~ in(X0,sK4_skl),
inference(resolution,[status(thm)],[f132,f93]) ).
fof(f362,plain,
in(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),sK8_skl),
inference(resolution,[status(thm)],[f328,f124]) ).
fof(f481,plain,
! [X0] : relation_restriction(sK4_skl,X0) = sK4_skl,
inference(forward_demodulation,[status(thm)],[f319,f177]) ).
fof(f504,definition,
! [X0] :
( sQ28_spl
<=> in(sK1_skl(relation_restriction(sK4_skl,X0)),X0) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f505,plain,
! [X0] :
( ~ sQ28_spl
| in(sK1_skl(relation_restriction(sK4_skl,X0)),X0) ),
inference(component_clause,[status(thm)],[f504]) ).
fof(f632,plain,
! [X0] :
( ~ sQ28_spl
| in(sK1_skl(sK4_skl),X0) ),
inference(forward_demodulation,[status(thm)],[f481,f505]) ).
fof(f652,definition,
! [X0,X1] :
( sQ52_spl
<=> ~ in(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f653,plain,
! [X0,X1] :
( ~ sQ52_spl
| ~ in(X0,X1) ),
inference(component_clause,[status(thm)],[f652]) ).
fof(f655,definition,
( sQ53_spl
<=> in(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f668,plain,
( ~ sQ52_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f362,f653]) ).
fof(f670,plain,
~ sQ52_spl,
inference(contradiction_clause,[status(thm)],[f668]) ).
fof(f679,plain,
( ~ sQ28_spl
| $false ),
inference(resolution,[status(thm)],[f632,f356]) ).
fof(f680,plain,
~ sQ28_spl,
inference(contradiction_clause,[status(thm)],[f679]) ).
fof(f737,definition,
! [X0] :
( sQ61_spl
<=> ~ empty(X0) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f738,plain,
! [X0] :
( ~ sQ61_spl
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f737]) ).
fof(f749,plain,
( ~ in(ordered_pair(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),sK1_skl(relation_restriction(sK7_skl,sK8_skl))),relation_restriction(sK7_skl,sK8_skl))
| ~ relation(relation_restriction(sK7_skl,sK8_skl)) ),
inference(resolution,[status(thm)],[f85,f124]) ).
fof(f756,definition,
( sQ63_spl
<=> relation(relation_restriction(sK7_skl,sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f758,plain,
( sQ63_spl
| ~ relation(relation_restriction(sK7_skl,sK8_skl)) ),
inference(component_clause,[status(thm)],[f756]) ).
fof(f759,definition,
( sQ64_spl
<=> in(ordered_pair(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),sK1_skl(relation_restriction(sK7_skl,sK8_skl))),relation_restriction(sK7_skl,sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f761,plain,
( sQ64_spl
| ~ in(ordered_pair(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),sK1_skl(relation_restriction(sK7_skl,sK8_skl))),relation_restriction(sK7_skl,sK8_skl)) ),
inference(component_clause,[status(thm)],[f759]) ).
fof(f762,plain,
( ~ sQ64_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f749,f756,f759]) ).
fof(f768,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ in(X0,relation_field(sK7_skl))
| ~ in(X1,X2)
| in(ordered_pair(X0,X0),sK7_skl) ),
inference(resolution,[status(thm)],[f104,f246]) ).
fof(f772,definition,
! [X0] :
( sQ66_spl
<=> ( ~ in(X0,relation_field(sK7_skl))
| in(ordered_pair(X0,X0),sK7_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f773,plain,
! [X0] :
( ~ sQ66_spl
| ~ in(X0,relation_field(sK7_skl))
| in(ordered_pair(X0,X0),sK7_skl) ),
inference(component_clause,[status(thm)],[f772]) ).
fof(f775,plain,
( ~ sQ2_spl
| sQ52_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f768,f772,f652,f245]) ).
fof(f789,plain,
( sQ63_spl
| ~ relation(sK7_skl) ),
inference(resolution,[status(thm)],[f758,f65]) ).
fof(f790,plain,
( sQ63_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f789,f147,f756]) ).
fof(f791,plain,
( sQ64_spl
| ~ in(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),relation_field(relation_restriction(sK7_skl,sK8_skl)))
| ~ reflexive(relation_restriction(sK7_skl,sK8_skl))
| ~ relation(relation_restriction(sK7_skl,sK8_skl)) ),
inference(resolution,[status(thm)],[f761,f83]) ).
fof(f792,plain,
( sQ64_spl
| ~ in(ordered_pair(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),sK1_skl(relation_restriction(sK7_skl,sK8_skl))),cartesian_product2(sK8_skl,sK8_skl))
| ~ in(ordered_pair(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),sK1_skl(relation_restriction(sK7_skl,sK8_skl))),sK7_skl)
| ~ relation(sK7_skl) ),
inference(resolution,[status(thm)],[f761,f111]) ).
fof(f794,definition,
( sQ69_spl
<=> reflexive(relation_restriction(sK7_skl,sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f797,definition,
( sQ70_spl
<=> in(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),relation_field(relation_restriction(sK7_skl,sK8_skl))) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f800,plain,
( sQ64_spl
| ~ sQ70_spl
| ~ sQ69_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f791,f756,f794,f797,f759]) ).
fof(f801,definition,
( sQ71_spl
<=> in(ordered_pair(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),sK1_skl(relation_restriction(sK7_skl,sK8_skl))),sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f803,plain,
( sQ71_spl
| ~ in(ordered_pair(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),sK1_skl(relation_restriction(sK7_skl,sK8_skl))),sK7_skl) ),
inference(component_clause,[status(thm)],[f801]) ).
fof(f804,definition,
( sQ72_spl
<=> in(ordered_pair(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),sK1_skl(relation_restriction(sK7_skl,sK8_skl))),cartesian_product2(sK8_skl,sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f806,plain,
( sQ72_spl
| ~ in(ordered_pair(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),sK1_skl(relation_restriction(sK7_skl,sK8_skl))),cartesian_product2(sK8_skl,sK8_skl)) ),
inference(component_clause,[status(thm)],[f804]) ).
fof(f807,plain,
( sQ64_spl
| ~ sQ72_spl
| ~ sQ71_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f792,f147,f801,f804,f759]) ).
fof(f896,plain,
! [X0,X1] :
( ~ relation(relation_restriction(sK7_skl,sK8_skl))
| ~ in(X0,X1)
| in(ordered_pair(X0,sK1_skl(relation_restriction(sK7_skl,sK8_skl))),cartesian_product2(X1,relation_field(relation_restriction(sK7_skl,sK8_skl)))) ),
inference(resolution,[status(thm)],[f241,f124]) ).
fof(f899,definition,
! [X0,X1] :
( sQ78_spl
<=> ( ~ in(X0,X1)
| in(ordered_pair(X0,sK1_skl(relation_restriction(sK7_skl,sK8_skl))),cartesian_product2(X1,relation_field(relation_restriction(sK7_skl,sK8_skl)))) ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f900,plain,
! [X0,X1] :
( ~ sQ78_spl
| ~ in(X0,X1)
| in(ordered_pair(X0,sK1_skl(relation_restriction(sK7_skl,sK8_skl))),cartesian_product2(X1,relation_field(relation_restriction(sK7_skl,sK8_skl)))) ),
inference(component_clause,[status(thm)],[f899]) ).
fof(f902,plain,
( ~ sQ63_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f896,f899,f756]) ).
fof(f960,plain,
( ~ sQ66_spl
| sQ71_spl
| ~ in(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),relation_field(sK7_skl)) ),
inference(resolution,[status(thm)],[f803,f773]) ).
fof(f971,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f273,f123]) ).
fof(f972,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f971]) ).
fof(f973,plain,
! [X0] :
( ~ sQ66_spl
| sQ71_spl
| ~ in(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),relation_field(relation_restriction(sK7_skl,X0)))
| ~ relation(sK7_skl) ),
inference(resolution,[status(thm)],[f960,f114]) ).
fof(f975,definition,
! [X0] :
( sQ87_spl
<=> ~ in(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),relation_field(relation_restriction(sK7_skl,X0))) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f976,plain,
! [X0] :
( ~ sQ87_spl
| ~ in(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),relation_field(relation_restriction(sK7_skl,X0))) ),
inference(component_clause,[status(thm)],[f975]) ).
fof(f978,plain,
( ~ sQ66_spl
| sQ71_spl
| sQ87_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f973,f147,f975,f801,f772]) ).
fof(f1031,plain,
! [X0,X1] :
( ~ sQ78_spl
| in(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),relation_field(relation_restriction(sK7_skl,sK8_skl)))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f900,f104]) ).
fof(f1033,plain,
( ~ sQ78_spl
| sQ70_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f1031,f652,f797,f899]) ).
fof(f1054,plain,
( ~ sQ61_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f93,f738]) ).
fof(f1055,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f1054]) ).
fof(f1061,plain,
( ~ sQ87_spl
| reflexive(relation_restriction(sK7_skl,sK8_skl))
| ~ relation(relation_restriction(sK7_skl,sK8_skl)) ),
inference(resolution,[status(thm)],[f976,f84]) ).
fof(f1064,plain,
( ~ sQ87_spl
| sQ69_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f1061,f756,f794,f975]) ).
fof(f1078,plain,
( in(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),sK8_skl)
| ~ relation(sK7_skl) ),
inference(resolution,[status(thm)],[f314,f124]) ).
fof(f1081,plain,
( sQ53_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f1078,f147,f655]) ).
fof(f1141,plain,
( sQ72_spl
| ~ in(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),sK8_skl)
| ~ in(sK1_skl(relation_restriction(sK7_skl,sK8_skl)),sK8_skl) ),
inference(resolution,[status(thm)],[f806,f105]) ).
fof(f1153,plain,
( sQ72_spl
| ~ sQ53_spl ),
inference(split_clause,[status(thm)],[f1141,f655,f804]) ).
fof(f1168,plain,
$false,
inference(sat_refutation,[status(thm)],[f248,f250,f670,f680,f762,f775,f790,f800,f807,f902,f972,f978,f1033,f1055,f1064,f1081,f1153]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU252+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n008.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:03:54 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.14/0.39 % Drodi V4.1.1
% 0.14/0.54 % Refutation found
% 0.14/0.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.88/0.57 % Elapsed time: 0.181511 seconds
% 0.88/0.57 % CPU time: 1.080185 seconds
% 0.88/0.57 % Total memory used: 131.801 MB
% 0.88/0.57 % Net memory used: 129.065 MB
%------------------------------------------------------------------------------