%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU201+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:19:39 PM UTC 2026
% Result : Theorem 0.13s 5.87s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 20
% Syntax : Number of formulae : 106 ( 10 unt; 11 def)
% Number of atoms : 382 ( 45 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 453 ( 177 ~; 187 |; 56 &)
% ( 24 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 12 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 2 con; 0-3 aty)
% Number of variables : 203 ( 183 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [A,B] :
( A = B
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,B] :
( relation(B)
=> ! [C] :
( relation(C)
=> ( C = relation_rng_restriction(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ( in(ordered_pair(D,E),B)
& in(E,A) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B,C] :
( C = set_intersection2(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(D,C),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A,B] :
( relation(B)
=> relation(relation_rng_restriction(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A,B] :
( relation(B)
=> subset(relation_rng(relation_rng_restriction(A,B)),A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [A,B] :
( relation(B)
=> subset(relation_rng(relation_rng_restriction(A,B)),relation_rng(B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,conjecture,
! [A,B] :
( relation(B)
=> relation_rng(relation_rng_restriction(A,B)) = set_intersection2(relation_rng(B),A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,negated_conjecture,
~ ! [A,B] :
( relation(B)
=> relation_rng(relation_rng_restriction(A,B)) = set_intersection2(relation_rng(B),A) ),
inference(negated_conjecture,[status(cth)],[f40]) ).
fof(f58,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(NNF_transformation,[status(thm)],[f5]) ).
fof(f59,plain,
( ! [A,B] :
( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ! [A,B] :
( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(miniscoping,[status(thm)],[f58]) ).
fof(f60,plain,
! [X0,X1] :
( subset(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f63,plain,
! [A,B] :
( ! [C] :
( ( C = relation_rng_restriction(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ( in(ordered_pair(D,E),B)
& in(E,A) ) ) )
| ~ relation(C) )
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f64,plain,
! [A,B] :
( ! [C] :
( ( ( ? [D,E] :
( ( ( in(ordered_pair(D,E),B)
& in(E,A) )
| in(ordered_pair(D,E),C) )
& ( ~ in(ordered_pair(D,E),B)
| ~ in(E,A)
| ~ in(ordered_pair(D,E),C) ) )
| C = relation_rng_restriction(A,B) )
& ( ! [D,E] :
( ( ~ in(ordered_pair(D,E),B)
| ~ in(E,A)
| in(ordered_pair(D,E),C) )
& ( ( in(ordered_pair(D,E),B)
& in(E,A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_rng_restriction(A,B) ) )
| ~ relation(C) )
| ~ relation(B) ),
inference(NNF_transformation,[status(thm)],[f63]) ).
fof(f65,plain,
! [B] :
( ! [C] :
( ( ! [A] :
( ? [D,E] :
( ( ( in(ordered_pair(D,E),B)
& in(E,A) )
| in(ordered_pair(D,E),C) )
& ( ~ in(ordered_pair(D,E),B)
| ~ in(E,A)
| ~ in(ordered_pair(D,E),C) ) )
| C = relation_rng_restriction(A,B) )
& ! [A] :
( ( ! [D,E] :
( ~ in(ordered_pair(D,E),B)
| ~ in(E,A)
| in(ordered_pair(D,E),C) )
& ! [D,E] :
( ( in(ordered_pair(D,E),B)
& in(E,A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_rng_restriction(A,B) ) )
| ~ relation(C) )
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f64]) ).
fof(f66,plain,
! [B] :
( ! [C] :
( ( ! [A] :
( ( ( ( in(ordered_pair(sK0_skl(A,C,B),sK1_skl(A,C,B)),B)
& in(sK1_skl(A,C,B),A) )
| in(ordered_pair(sK0_skl(A,C,B),sK1_skl(A,C,B)),C) )
& ( ~ in(ordered_pair(sK0_skl(A,C,B),sK1_skl(A,C,B)),B)
| ~ in(sK1_skl(A,C,B),A)
| ~ in(ordered_pair(sK0_skl(A,C,B),sK1_skl(A,C,B)),C) ) )
| C = relation_rng_restriction(A,B) )
& ! [A] :
( ( ! [D,E] :
( ~ in(ordered_pair(D,E),B)
| ~ in(E,A)
| in(ordered_pair(D,E),C) )
& ! [D,E] :
( ( in(ordered_pair(D,E),B)
& in(E,A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_rng_restriction(A,B) ) )
| ~ relation(C) )
| ~ relation(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(D,sK0_skl(A,C,B)),skolemize(E,sK1_skl(A,C,B))],[f65]) ).
fof(f69,plain,
! [X0,X1,X2,X3,X4] :
( ~ in(ordered_pair(X3,X4),X0)
| ~ in(X4,X2)
| in(ordered_pair(X3,X4),X1)
| X1 != relation_rng_restriction(X2,X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f73,plain,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,B)
| ~ in(C,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f74,plain,
! [A,B] :
( ( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f73]) ).
fof(f75,plain,
( ! [A,B] :
( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ! [A,B] :
( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(miniscoping,[status(thm)],[f74]) ).
fof(f76,plain,
( ! [A,B] :
( ( ~ in(sK2_skl(B,A),B)
& in(sK2_skl(B,A),A) )
| subset(A,B) )
& ! [A,B] :
( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(C,sK2_skl(B,A))],[f75]) ).
fof(f77,plain,
! [X0,X1,X2] :
( in(X2,X1)
| ~ in(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f80,plain,
! [A,B,C] :
( ( ? [D] :
( ( ( in(D,B)
& in(D,A) )
| in(D,C) )
& ( ~ in(D,B)
| ~ in(D,A)
| ~ in(D,C) ) )
| C = set_intersection2(A,B) )
& ( ! [D] :
( ( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f81,plain,
( ! [A,B,C] :
( ? [D] :
( ( ( in(D,B)
& in(D,A) )
| in(D,C) )
& ( ~ in(D,B)
| ~ in(D,A)
| ~ in(D,C) ) )
| C = set_intersection2(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ! [D] :
( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(miniscoping,[status(thm)],[f80]) ).
fof(f82,plain,
( ! [A,B,C] :
( ( ( ( in(sK3_skl(C,B,A),B)
& in(sK3_skl(C,B,A),A) )
| in(sK3_skl(C,B,A),C) )
& ( ~ in(sK3_skl(C,B,A),B)
| ~ in(sK3_skl(C,B,A),A)
| ~ in(sK3_skl(C,B,A),C) ) )
| C = set_intersection2(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ! [D] :
( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(D,sK3_skl(C,B,A))],[f81]) ).
fof(f86,plain,
! [X0,X1,X2] :
( ~ in(sK3_skl(X0,X2,X1),X2)
| ~ in(sK3_skl(X0,X2,X1),X1)
| ~ in(sK3_skl(X0,X2,X1),X0)
| X0 = set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f87,plain,
! [X0,X1,X2] :
( in(sK3_skl(X0,X2,X1),X1)
| in(sK3_skl(X0,X2,X1),X0)
| X0 = set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f88,plain,
! [X0,X1,X2] :
( in(sK3_skl(X0,X2,X1),X2)
| in(sK3_skl(X0,X2,X1),X0)
| X0 = set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f89,plain,
! [A] :
( ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(D,C),A) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f90,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ? [D] : in(ordered_pair(D,C),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B = relation_rng(A) )
& ( ! [C] :
( ( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ( ? [D] : in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f89]) ).
fof(f91,plain,
! [A] :
( ( ! [B] :
( ? [C] :
( ( ? [D] : in(ordered_pair(D,C),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ! [C] :
( ? [D] : in(ordered_pair(D,C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f90]) ).
fof(f92,plain,
! [A] :
( ( ! [B] :
( ( ( in(ordered_pair(sK6_skl(B,A),sK5_skl(B,A)),A)
| in(sK5_skl(B,A),B) )
& ( ! [D] : ~ in(ordered_pair(D,sK5_skl(B,A)),A)
| ~ in(sK5_skl(B,A),B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(D,C),A)
| in(C,B) )
& ! [C] :
( in(ordered_pair(sK4_skl(C,B,A),C),A)
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(D,sK4_skl(C,B,A)),skolemize(C,sK5_skl(B,A)),skolemize(D,sK6_skl(B,A))],[f91]) ).
fof(f93,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK4_skl(X2,X1,X0),X2),X0)
| ~ in(X2,X1)
| X1 != relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f94,plain,
! [X0,X1,X2,X3] :
( ~ in(ordered_pair(X3,X2),X0)
| in(X2,X1)
| X1 != relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f98,plain,
! [A,B] :
( relation(relation_rng_restriction(A,B))
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f99,plain,
! [B] :
( ! [A] : relation(relation_rng_restriction(A,B))
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f98]) ).
fof(f100,plain,
! [X0,X1] :
( relation(relation_rng_restriction(X1,X0))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f138,plain,
! [A,B] :
( subset(relation_rng(relation_rng_restriction(A,B)),A)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f139,plain,
! [B] :
( ! [A] : subset(relation_rng(relation_rng_restriction(A,B)),A)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f138]) ).
fof(f140,plain,
! [X0,X1] :
( subset(relation_rng(relation_rng_restriction(X1,X0)),X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f141,plain,
! [A,B] :
( subset(relation_rng(relation_rng_restriction(A,B)),relation_rng(B))
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f142,plain,
! [B] :
( ! [A] : subset(relation_rng(relation_rng_restriction(A,B)),relation_rng(B))
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f141]) ).
fof(f143,plain,
! [X0,X1] :
( subset(relation_rng(relation_rng_restriction(X1,X0)),relation_rng(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f144,plain,
? [A,B] :
( relation_rng(relation_rng_restriction(A,B)) != set_intersection2(relation_rng(B),A)
& relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f145,plain,
? [B] :
( ? [A] : relation_rng(relation_rng_restriction(A,B)) != set_intersection2(relation_rng(B),A)
& relation(B) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f146,plain,
( relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)) != set_intersection2(relation_rng(sK14_skl),sK15_skl)
& relation(sK14_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl]),skolemize(B,sK14_skl),skolemize(A,sK15_skl)],[f145]) ).
fof(f147,plain,
relation(sK14_skl),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f148,plain,
relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)) != set_intersection2(relation_rng(sK14_skl),sK15_skl),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f174,plain,
! [X0] : subset(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f60]) ).
fof(f178,plain,
! [X0,X1,X2,X3] :
( ~ in(ordered_pair(X2,X3),X0)
| ~ in(X3,X1)
| in(ordered_pair(X2,X3),relation_rng_restriction(X1,X0))
| ~ relation(relation_rng_restriction(X1,X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f69]) ).
fof(f182,plain,
! [X0,X1] :
( in(ordered_pair(sK4_skl(X1,relation_rng(X0),X0),X1),X0)
| ~ in(X1,relation_rng(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f93]) ).
fof(f183,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X2,X1),X0)
| in(X1,relation_rng(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f94]) ).
fof(f184,plain,
! [X0,X1,X2,X3] :
( ~ in(ordered_pair(X1,X2),X0)
| ~ in(X2,X3)
| in(ordered_pair(X1,X2),relation_rng_restriction(X3,X0))
| ~ relation(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f178,f100]) ).
fof(f798,definition,
( sQ2_spl
<=> subset(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),relation_rng(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f800,plain,
( sQ2_spl
| ~ subset(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),relation_rng(sK14_skl)) ),
inference(component_clause,[status(thm)],[f798]) ).
fof(f801,definition,
( sQ3_spl
<=> subset(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f803,plain,
( sQ3_spl
| ~ subset(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl) ),
inference(component_clause,[status(thm)],[f801]) ).
fof(f805,plain,
( sQ3_spl
| ~ relation(sK14_skl) ),
inference(resolution,[status(thm)],[f803,f140]) ).
fof(f806,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f805,f147]) ).
fof(f807,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f806]) ).
fof(f810,plain,
( sQ2_spl
| ~ relation(sK14_skl) ),
inference(resolution,[status(thm)],[f800,f143]) ).
fof(f811,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f810,f147]) ).
fof(f812,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f811]) ).
fof(f880,definition,
( sQ4_spl
<=> relation(relation_rng_restriction(sK15_skl,sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f882,plain,
( sQ4_spl
| ~ relation(relation_rng_restriction(sK15_skl,sK14_skl)) ),
inference(component_clause,[status(thm)],[f880]) ).
fof(f894,plain,
( sQ4_spl
| ~ relation(sK14_skl) ),
inference(resolution,[status(thm)],[f882,f100]) ).
fof(f896,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f894,f147]) ).
fof(f897,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f896]) ).
fof(f905,definition,
( sQ8_spl
<=> relation(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f907,plain,
( sQ8_spl
| ~ relation(sK14_skl) ),
inference(component_clause,[status(thm)],[f905]) ).
fof(f943,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f907,f147]) ).
fof(f944,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f943]) ).
fof(f1167,plain,
( ~ in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),sK15_skl)
| ~ in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),relation_rng(sK14_skl))
| ~ in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),relation_rng(relation_rng_restriction(sK15_skl,sK14_skl))) ),
inference(resolution,[status(thm)],[f86,f148]) ).
fof(f1171,definition,
( sQ40_spl
<=> in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),relation_rng(relation_rng_restriction(sK15_skl,sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1173,plain,
( sQ40_spl
| ~ in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),relation_rng(relation_rng_restriction(sK15_skl,sK14_skl))) ),
inference(component_clause,[status(thm)],[f1171]) ).
fof(f1174,definition,
( sQ41_spl
<=> in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),relation_rng(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1176,plain,
( sQ41_spl
| ~ in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),relation_rng(sK14_skl)) ),
inference(component_clause,[status(thm)],[f1174]) ).
fof(f1177,definition,
( sQ42_spl
<=> in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1179,plain,
( sQ42_spl
| ~ in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),sK15_skl) ),
inference(component_clause,[status(thm)],[f1177]) ).
fof(f1180,plain,
( ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f1167,f1171,f1174,f1177]) ).
fof(f1217,plain,
! [X0] :
( sQ42_spl
| ~ in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),X0)
| ~ subset(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f1179,f77]) ).
fof(f1222,definition,
( sQ43_spl
<=> relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)) = set_intersection2(relation_rng(sK14_skl),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1223,plain,
( ~ sQ43_spl
| relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)) = set_intersection2(relation_rng(sK14_skl),sK15_skl) ),
inference(component_clause,[status(thm)],[f1222]) ).
fof(f1236,plain,
( ~ sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1223,f148]) ).
fof(f1237,plain,
~ sQ43_spl,
inference(contradiction_clause,[status(thm)],[f1236]) ).
fof(f1240,plain,
! [X0] :
( sQ41_spl
| ~ in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),X0)
| ~ subset(X0,relation_rng(sK14_skl)) ),
inference(resolution,[status(thm)],[f1176,f77]) ).
fof(f1246,definition,
! [X0] :
( sQ47_spl
<=> ~ in(ordered_pair(X0,sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl))),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1247,plain,
! [X0] :
( ~ sQ47_spl
| ~ in(ordered_pair(X0,sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl))),sK14_skl) ),
inference(component_clause,[status(thm)],[f1246]) ).
fof(f1259,plain,
! [X0] :
( sQ40_spl
| ~ in(ordered_pair(X0,sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl))),relation_rng_restriction(sK15_skl,sK14_skl))
| ~ relation(relation_rng_restriction(sK15_skl,sK14_skl)) ),
inference(resolution,[status(thm)],[f1173,f183]) ).
fof(f1267,definition,
! [X0] :
( sQ50_spl
<=> ~ in(ordered_pair(X0,sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl))),relation_rng_restriction(sK15_skl,sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1268,plain,
! [X0] :
( ~ sQ50_spl
| ~ in(ordered_pair(X0,sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl))),relation_rng_restriction(sK15_skl,sK14_skl)) ),
inference(component_clause,[status(thm)],[f1267]) ).
fof(f1270,plain,
( sQ40_spl
| sQ50_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1259,f880,f1267,f1171]) ).
fof(f1329,plain,
( ~ sQ47_spl
| ~ in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),relation_rng(sK14_skl))
| ~ relation(sK14_skl) ),
inference(resolution,[status(thm)],[f1247,f182]) ).
fof(f1336,plain,
( ~ sQ47_spl
| ~ sQ41_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1329,f905,f1174,f1246]) ).
fof(f1349,plain,
( sQ41_spl
| in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),relation_rng(sK14_skl))
| relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)) = set_intersection2(relation_rng(sK14_skl),sK15_skl)
| ~ subset(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),relation_rng(sK14_skl)) ),
inference(resolution,[status(thm)],[f1240,f87]) ).
fof(f1367,plain,
( sQ41_spl
| sQ43_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1349,f798,f1222,f1174]) ).
fof(f1471,plain,
( sQ42_spl
| in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),sK15_skl)
| relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)) = set_intersection2(relation_rng(sK14_skl),sK15_skl)
| ~ subset(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl) ),
inference(resolution,[status(thm)],[f1217,f88]) ).
fof(f1481,definition,
( sQ64_spl
<=> subset(sK15_skl,sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1483,plain,
( sQ64_spl
| ~ subset(sK15_skl,sK15_skl) ),
inference(component_clause,[status(thm)],[f1481]) ).
fof(f1489,plain,
( sQ42_spl
| sQ43_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1471,f801,f1222,f1177]) ).
fof(f1491,plain,
( sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1483,f174]) ).
fof(f1492,plain,
sQ64_spl,
inference(contradiction_clause,[status(thm)],[f1491]) ).
fof(f1517,plain,
! [X0] :
( ~ sQ50_spl
| ~ in(ordered_pair(X0,sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl))),sK14_skl)
| ~ in(sK3_skl(relation_rng(relation_rng_restriction(sK15_skl,sK14_skl)),sK15_skl,relation_rng(sK14_skl)),sK15_skl)
| ~ relation(sK14_skl) ),
inference(resolution,[status(thm)],[f1268,f184]) ).
fof(f1525,plain,
( ~ sQ50_spl
| sQ47_spl
| ~ sQ42_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1517,f905,f1177,f1246,f1267]) ).
fof(f1534,plain,
$false,
inference(sat_refutation,[status(thm)],[f807,f812,f897,f944,f1180,f1237,f1270,f1336,f1367,f1489,f1492,f1525]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU201+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n012.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Mon Sep 21 05:57:14 UTC 2026
% 0.09/5.36 % CPUTime :
% 0.09/5.37 % Drodi V4.1.1
% 0.13/5.87 % Refutation found
% 0.13/5.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/5.87 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/5.89 % Elapsed time: 0.520511 seconds
% 0.13/5.89 % CPU time: 3.897098 seconds
% 0.13/5.89 % Total memory used: 156.061 MB
% 0.13/5.89 % Net memory used: 147.943 MB
%------------------------------------------------------------------------------