%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU214+3 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:43 PM UTC 2026
% Result : Theorem 19.15s 2.99s
% Output : CNFRefutation 19.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 38
% Syntax : Number of formulae : 172 ( 31 unt; 22 def)
% Number of atoms : 534 ( 56 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 588 ( 226 ~; 236 |; 74 &)
% ( 34 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 23 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 9 con; 0-5 aty)
% Number of variables : 182 ( 152 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [A] :
( empty(A)
=> function(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A] :
( empty(A)
=> relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B,C] :
( ( ~ in(B,relation_dom(A))
=> ( C = apply(A,B)
<=> C = empty_set ) )
& ( in(B,relation_dom(A))
=> ( C = apply(A,B)
<=> in(ordered_pair(B,C),A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_dom(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(C,D),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ! [C] :
( relation(C)
=> ( C = relation_composition(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B] :
( ( relation(B)
& relation(A) )
=> relation(relation_composition(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A,B] :
( ( function(B)
& relation(B)
& function(A)
& relation(A) )
=> ( function(relation_composition(A,B))
& relation(relation_composition(A,B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A] :
( empty(A)
=> ( relation(relation_dom(A))
& empty(relation_dom(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
? [A] :
( function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
? [A] :
( relation_empty_yielding(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,conjecture,
! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( in(A,relation_dom(relation_composition(C,B)))
=> apply(relation_composition(C,B),A) = apply(B,apply(C,A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
~ ! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( in(A,relation_dom(relation_composition(C,B)))
=> apply(relation_composition(C,B),A) = apply(B,apply(C,A)) ) ) ),
inference(negated_conjecture,[status(cth)],[f33]) ).
fof(f44,plain,
! [A] :
( function(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f45,plain,
! [X0] :
( function(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f46,plain,
! [A] :
( relation(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f47,plain,
! [X0] :
( relation(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f49,plain,
! [A] :
( ! [B,C] :
( ( ( C = apply(A,B)
<=> C = empty_set )
| in(B,relation_dom(A)) )
& ( ( C = apply(A,B)
<=> in(ordered_pair(B,C),A) )
| ~ in(B,relation_dom(A)) ) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f50,plain,
! [A] :
( ! [B,C] :
( ( ( ( C != empty_set
| C = apply(A,B) )
& ( C = empty_set
| C != apply(A,B) ) )
| in(B,relation_dom(A)) )
& ( ( ( ~ in(ordered_pair(B,C),A)
| C = apply(A,B) )
& ( in(ordered_pair(B,C),A)
| C != apply(A,B) ) )
| ~ in(B,relation_dom(A)) ) )
| ~ function(A)
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f49]) ).
fof(f51,plain,
! [A] :
( ( ! [B] :
( ( ! [C] :
( C != empty_set
| C = apply(A,B) )
& ! [C] :
( C = empty_set
| C != apply(A,B) ) )
| in(B,relation_dom(A)) )
& ! [B] :
( ( ! [C] :
( ~ in(ordered_pair(B,C),A)
| C = apply(A,B) )
& ! [C] :
( in(ordered_pair(B,C),A)
| C != apply(A,B) ) )
| ~ in(B,relation_dom(A)) ) )
| ~ function(A)
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f50]) ).
fof(f53,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,X2),X0)
| X2 = apply(X0,X1)
| ~ in(X1,relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f56,plain,
! [A] :
( ! [B] :
( B = relation_dom(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(C,D),A) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f57,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ? [D] : in(ordered_pair(C,D),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B = relation_dom(A) )
& ( ! [C] :
( ( ! [D] : ~ in(ordered_pair(C,D),A)
| in(C,B) )
& ( ? [D] : in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f56]) ).
fof(f58,plain,
! [A] :
( ( ! [B] :
( ? [C] :
( ( ? [D] : in(ordered_pair(C,D),A)
| in(C,B) )
& ( ! [D] : ~ in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B = relation_dom(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(C,D),A)
| in(C,B) )
& ! [C] :
( ? [D] : in(ordered_pair(C,D),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f57]) ).
fof(f59,plain,
! [A] :
( ( ! [B] :
( ( ( in(ordered_pair(sK1_skl(B,A),sK2_skl(B,A)),A)
| in(sK1_skl(B,A),B) )
& ( ! [D] : ~ in(ordered_pair(sK1_skl(B,A),D),A)
| ~ in(sK1_skl(B,A),B) ) )
| B = relation_dom(A) )
& ! [B] :
( ( ! [C] :
( ! [D] : ~ in(ordered_pair(C,D),A)
| in(C,B) )
& ! [C] :
( in(ordered_pair(C,sK0_skl(C,B,A)),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(D,sK0_skl(C,B,A)),skolemize(C,sK1_skl(B,A)),skolemize(D,sK2_skl(B,A))],[f58]) ).
fof(f60,plain,
! [X0,X1,X2] :
( in(ordered_pair(X2,sK0_skl(X2,X1,X0)),X0)
| ~ in(X2,X1)
| X1 != relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f61,plain,
! [X0,X1,X2,X3] :
( ~ in(ordered_pair(X2,X3),X0)
| in(X2,X1)
| X1 != relation_dom(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f65,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( C = relation_composition(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) ) ) )
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f66,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ? [D,E] :
( ( ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C = relation_composition(A,B) )
& ( ! [D,E] :
( ( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ( ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_composition(A,B) ) )
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ? [D,E] :
( ( ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C = relation_composition(A,B) )
& ( ( ! [D,E] :
( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ! [D,E] :
( ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_composition(A,B) ) )
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f66]) ).
fof(f68,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ( ( ( in(ordered_pair(sK6_skl(C,B,A),sK5_skl(C,B,A)),B)
& in(ordered_pair(sK4_skl(C,B,A),sK6_skl(C,B,A)),A) )
| in(ordered_pair(sK4_skl(C,B,A),sK5_skl(C,B,A)),C) )
& ( ! [F] :
( ~ in(ordered_pair(F,sK5_skl(C,B,A)),B)
| ~ in(ordered_pair(sK4_skl(C,B,A),F),A) )
| ~ in(ordered_pair(sK4_skl(C,B,A),sK5_skl(C,B,A)),C) ) )
| C = relation_composition(A,B) )
& ( ( ! [D,E] :
( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| in(ordered_pair(D,E),C) )
& ! [D,E] :
( ( in(ordered_pair(sK3_skl(E,D,C,B,A),E),B)
& in(ordered_pair(D,sK3_skl(E,D,C,B,A)),A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_composition(A,B) ) )
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl,sK6_skl]),skolemize(F,sK3_skl(E,D,C,B,A)),skolemize(D,sK4_skl(C,B,A)),skolemize(E,sK5_skl(C,B,A)),skolemize(F,sK6_skl(C,B,A))],[f67]) ).
fof(f69,plain,
! [X0,X1,X2,X3,X4] :
( in(ordered_pair(X3,sK3_skl(X4,X3,X2,X1,X0)),X0)
| ~ in(ordered_pair(X3,X4),X2)
| X2 != relation_composition(X0,X1)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f70,plain,
! [X0,X1,X2,X3,X4] :
( in(ordered_pair(sK3_skl(X4,X3,X2,X1,X0),X4),X1)
| ~ in(ordered_pair(X3,X4),X2)
| X2 != relation_composition(X0,X1)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f75,plain,
! [A,B] :
( relation(relation_composition(A,B))
| ~ relation(B)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f76,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f83,plain,
relation(empty_set),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f85,plain,
! [A,B] :
( ( function(relation_composition(A,B))
& relation(relation_composition(A,B)) )
| ~ function(B)
| ~ relation(B)
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f87,plain,
! [X0,X1] :
( function(relation_composition(X0,X1))
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f97,plain,
! [A] :
( ( relation(relation_dom(A))
& empty(relation_dom(A)) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f99,plain,
! [X0] :
( relation(relation_dom(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f103,plain,
( function(sK8_skl)
& relation(sK8_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f23]) ).
fof(f104,plain,
relation(sK8_skl),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f106,plain,
( relation(sK9_skl)
& empty(sK9_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f24]) ).
fof(f107,plain,
empty(sK9_skl),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f108,plain,
relation(sK9_skl),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f113,plain,
empty(sK11_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f26]) ).
fof(f114,plain,
empty(sK11_skl),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
( relation(sK12_skl)
& ~ empty(sK12_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f27]) ).
fof(f117,plain,
relation(sK12_skl),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f118,plain,
! [A] :
( empty(sK13_skl(A))
& element(sK13_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(B,sK13_skl(A))],[f28]) ).
fof(f120,plain,
! [X0] : empty(sK13_skl(X0)),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f123,plain,
( relation_empty_yielding(sK15_skl)
& relation(sK15_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(A,sK15_skl)],[f30]) ).
fof(f124,plain,
relation(sK15_skl),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f130,plain,
? [A,B] :
( ? [C] :
( apply(relation_composition(C,B),A) != apply(B,apply(C,A))
& in(A,relation_dom(relation_composition(C,B)))
& function(C)
& relation(C) )
& function(B)
& relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f131,plain,
? [B] :
( ? [C] :
( ? [A] :
( apply(relation_composition(C,B),A) != apply(B,apply(C,A))
& in(A,relation_dom(relation_composition(C,B))) )
& function(C)
& relation(C) )
& function(B)
& relation(B) ),
inference(miniscoping,[status(thm)],[f130]) ).
fof(f132,plain,
( apply(relation_composition(sK17_skl,sK16_skl),sK18_skl) != apply(sK16_skl,apply(sK17_skl,sK18_skl))
& in(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)))
& function(sK17_skl)
& relation(sK17_skl)
& function(sK16_skl)
& relation(sK16_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl]),skolemize(B,sK16_skl),skolemize(C,sK17_skl),skolemize(A,sK18_skl)],[f131]) ).
fof(f133,plain,
relation(sK16_skl),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f134,plain,
function(sK16_skl),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f135,plain,
relation(sK17_skl),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f136,plain,
function(sK17_skl),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f137,plain,
in(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl))),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f138,plain,
apply(relation_composition(sK17_skl,sK16_skl),sK18_skl) != apply(sK16_skl,apply(sK17_skl,sK18_skl)),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f162,plain,
! [X0,X1] :
( in(ordered_pair(X1,sK0_skl(X1,relation_dom(X0),X0)),X0)
| ~ in(X1,relation_dom(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f60]) ).
fof(f163,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,X2),X0)
| in(X1,relation_dom(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f61]) ).
fof(f164,plain,
! [X0,X1,X2,X3] :
( in(ordered_pair(X2,sK3_skl(X3,X2,relation_composition(X0,X1),X1,X0)),X0)
| ~ in(ordered_pair(X2,X3),relation_composition(X0,X1))
| ~ relation(relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f69]) ).
fof(f165,plain,
! [X0,X1,X2,X3] :
( in(ordered_pair(sK3_skl(X3,X2,relation_composition(X0,X1),X1,X0),X3),X1)
| ~ in(ordered_pair(X2,X3),relation_composition(X0,X1))
| ~ relation(relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f70]) ).
fof(f171,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X2,X1),X0)
| X1 = apply(X0,X2)
| ~ function(X0)
| ~ relation(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f53,f163]) ).
fof(f172,plain,
( in(ordered_pair(sK18_skl,sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl))),relation_composition(sK17_skl,sK16_skl))
| ~ relation(relation_composition(sK17_skl,sK16_skl)) ),
inference(resolution,[status(thm)],[f137,f162]) ).
fof(f175,definition,
( sQ0_spl
<=> relation(relation_composition(sK17_skl,sK16_skl)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f177,plain,
( sQ0_spl
| ~ relation(relation_composition(sK17_skl,sK16_skl)) ),
inference(component_clause,[status(thm)],[f175]) ).
fof(f178,definition,
( sQ1_spl
<=> in(ordered_pair(sK18_skl,sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl))),relation_composition(sK17_skl,sK16_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f179,plain,
( ~ sQ1_spl
| in(ordered_pair(sK18_skl,sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl))),relation_composition(sK17_skl,sK16_skl)) ),
inference(component_clause,[status(thm)],[f178]) ).
fof(f181,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f172,f175,f178]) ).
fof(f182,definition,
( sQ2_spl
<=> function(relation_composition(sK17_skl,sK16_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f184,plain,
( sQ2_spl
| ~ function(relation_composition(sK17_skl,sK16_skl)) ),
inference(component_clause,[status(thm)],[f182]) ).
fof(f191,plain,
( sQ0_spl
| ~ relation(sK16_skl)
| ~ relation(sK17_skl) ),
inference(resolution,[status(thm)],[f76,f177]) ).
fof(f192,definition,
( sQ4_spl
<=> relation(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f194,plain,
( sQ4_spl
| ~ relation(sK17_skl) ),
inference(component_clause,[status(thm)],[f192]) ).
fof(f195,definition,
( sQ5_spl
<=> relation(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f197,plain,
( sQ5_spl
| ~ relation(sK16_skl) ),
inference(component_clause,[status(thm)],[f195]) ).
fof(f198,plain,
( sQ0_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f191,f192,f195,f175]) ).
fof(f199,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f194,f135]) ).
fof(f200,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f199]) ).
fof(f201,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f197,f133]) ).
fof(f202,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f201]) ).
fof(f215,plain,
! [X0,X1,X2,X3] :
( in(ordered_pair(X2,sK3_skl(X3,X2,relation_composition(X0,X1),X1,X0)),X0)
| ~ in(ordered_pair(X2,X3),relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f164,f76]) ).
fof(f218,plain,
! [X0,X1,X2,X3] :
( in(ordered_pair(sK3_skl(X3,X2,relation_composition(X0,X1),X1,X0),X3),X1)
| ~ in(ordered_pair(X2,X3),relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f165,f76]) ).
fof(f231,plain,
( ~ sQ1_spl
| in(ordered_pair(sK3_skl(sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl)),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl),sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl))),sK16_skl)
| ~ relation(sK16_skl)
| ~ relation(sK17_skl) ),
inference(resolution,[status(thm)],[f179,f218]) ).
fof(f232,plain,
( ~ sQ1_spl
| in(ordered_pair(sK18_skl,sK3_skl(sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl)),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl)),sK17_skl)
| ~ relation(sK16_skl)
| ~ relation(sK17_skl) ),
inference(resolution,[status(thm)],[f179,f215]) ).
fof(f235,definition,
( sQ6_spl
<=> in(ordered_pair(sK3_skl(sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl)),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl),sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl))),sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f236,plain,
( ~ sQ6_spl
| in(ordered_pair(sK3_skl(sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl)),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl),sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl))),sK16_skl) ),
inference(component_clause,[status(thm)],[f235]) ).
fof(f238,plain,
( ~ sQ1_spl
| sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f231,f192,f195,f235,f178]) ).
fof(f239,definition,
( sQ7_spl
<=> in(ordered_pair(sK18_skl,sK3_skl(sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl)),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl)),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f240,plain,
( ~ sQ7_spl
| in(ordered_pair(sK18_skl,sK3_skl(sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl)),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl)),sK17_skl) ),
inference(component_clause,[status(thm)],[f239]) ).
fof(f242,plain,
( ~ sQ1_spl
| sQ7_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f232,f192,f195,f239,f178]) ).
fof(f247,plain,
( sQ2_spl
| ~ function(sK16_skl)
| ~ relation(sK16_skl)
| ~ function(sK17_skl)
| ~ relation(sK17_skl) ),
inference(resolution,[status(thm)],[f87,f184]) ).
fof(f248,definition,
( sQ9_spl
<=> function(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f250,plain,
( sQ9_spl
| ~ function(sK17_skl) ),
inference(component_clause,[status(thm)],[f248]) ).
fof(f251,definition,
( sQ10_spl
<=> function(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f253,plain,
( sQ10_spl
| ~ function(sK16_skl) ),
inference(component_clause,[status(thm)],[f251]) ).
fof(f254,plain,
( sQ2_spl
| ~ sQ10_spl
| ~ sQ5_spl
| ~ sQ9_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f247,f192,f248,f195,f251,f182]) ).
fof(f255,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f253,f134]) ).
fof(f256,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f255]) ).
fof(f257,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f250,f136]) ).
fof(f258,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f257]) ).
fof(f284,plain,
( ~ sQ1_spl
| sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl)) = apply(relation_composition(sK17_skl,sK16_skl),sK18_skl)
| ~ function(relation_composition(sK17_skl,sK16_skl))
| ~ relation(relation_composition(sK17_skl,sK16_skl)) ),
inference(resolution,[status(thm)],[f171,f179]) ).
fof(f292,definition,
( sQ14_spl
<=> sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl)) = apply(relation_composition(sK17_skl,sK16_skl),sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f293,plain,
( ~ sQ14_spl
| sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl)) = apply(relation_composition(sK17_skl,sK16_skl),sK18_skl) ),
inference(component_clause,[status(thm)],[f292]) ).
fof(f295,plain,
( ~ sQ1_spl
| sQ14_spl
| ~ sQ2_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f284,f175,f182,f292,f178]) ).
fof(f328,plain,
( ~ sQ6_spl
| ~ sQ14_spl
| in(ordered_pair(sK3_skl(apply(relation_composition(sK17_skl,sK16_skl),sK18_skl),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl),sK0_skl(sK18_skl,relation_dom(relation_composition(sK17_skl,sK16_skl)),relation_composition(sK17_skl,sK16_skl))),sK16_skl) ),
inference(forward_demodulation,[status(thm)],[f293,f236]) ).
fof(f329,plain,
( ~ sQ6_spl
| ~ sQ14_spl
| in(ordered_pair(sK3_skl(apply(relation_composition(sK17_skl,sK16_skl),sK18_skl),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl),apply(relation_composition(sK17_skl,sK16_skl),sK18_skl)),sK16_skl) ),
inference(forward_demodulation,[status(thm)],[f293,f328]) ).
fof(f331,plain,
( ~ sQ6_spl
| ~ sQ14_spl
| apply(relation_composition(sK17_skl,sK16_skl),sK18_skl) = apply(sK16_skl,sK3_skl(apply(relation_composition(sK17_skl,sK16_skl),sK18_skl),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl))
| ~ function(sK16_skl)
| ~ relation(sK16_skl) ),
inference(resolution,[status(thm)],[f329,f171]) ).
fof(f338,definition,
( sQ18_spl
<=> apply(relation_composition(sK17_skl,sK16_skl),sK18_skl) = apply(sK16_skl,sK3_skl(apply(relation_composition(sK17_skl,sK16_skl),sK18_skl),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f339,plain,
( ~ sQ18_spl
| apply(relation_composition(sK17_skl,sK16_skl),sK18_skl) = apply(sK16_skl,sK3_skl(apply(relation_composition(sK17_skl,sK16_skl),sK18_skl),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl)) ),
inference(component_clause,[status(thm)],[f338]) ).
fof(f341,plain,
( ~ sQ6_spl
| ~ sQ14_spl
| sQ18_spl
| ~ sQ10_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f331,f195,f251,f338,f292,f235]) ).
fof(f346,plain,
( ~ sQ7_spl
| ~ sQ14_spl
| in(ordered_pair(sK18_skl,sK3_skl(apply(relation_composition(sK17_skl,sK16_skl),sK18_skl),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl)),sK17_skl) ),
inference(forward_demodulation,[status(thm)],[f293,f240]) ).
fof(f348,plain,
( ~ sQ7_spl
| ~ sQ14_spl
| sK3_skl(apply(relation_composition(sK17_skl,sK16_skl),sK18_skl),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl) = apply(sK17_skl,sK18_skl)
| ~ function(sK17_skl)
| ~ relation(sK17_skl) ),
inference(resolution,[status(thm)],[f346,f171]) ).
fof(f355,definition,
( sQ21_spl
<=> sK3_skl(apply(relation_composition(sK17_skl,sK16_skl),sK18_skl),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl) = apply(sK17_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f356,plain,
( ~ sQ21_spl
| sK3_skl(apply(relation_composition(sK17_skl,sK16_skl),sK18_skl),sK18_skl,relation_composition(sK17_skl,sK16_skl),sK16_skl,sK17_skl) = apply(sK17_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f355]) ).
fof(f358,plain,
( ~ sQ7_spl
| ~ sQ14_spl
| sQ21_spl
| ~ sQ9_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f348,f192,f248,f355,f292,f239]) ).
fof(f456,definition,
( sQ27_spl
<=> relation(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f458,plain,
( sQ27_spl
| ~ relation(sK11_skl) ),
inference(component_clause,[status(thm)],[f456]) ).
fof(f466,definition,
( sQ30_spl
<=> relation(relation_dom(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f468,plain,
( sQ30_spl
| ~ relation(relation_dom(sK11_skl)) ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f517,plain,
( sQ27_spl
| ~ empty(sK11_skl) ),
inference(resolution,[status(thm)],[f458,f47]) ).
fof(f518,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f517,f114]) ).
fof(f519,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f518]) ).
fof(f531,definition,
( sQ38_spl
<=> relation(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f533,plain,
( sQ38_spl
| ~ relation(empty_set) ),
inference(component_clause,[status(thm)],[f531]) ).
fof(f555,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f533,f83]) ).
fof(f556,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f555]) ).
fof(f587,plain,
( sQ30_spl
| ~ empty(sK11_skl) ),
inference(resolution,[status(thm)],[f468,f99]) ).
fof(f589,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f587,f114]) ).
fof(f590,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f589]) ).
fof(f601,definition,
( sQ46_spl
<=> function(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f603,plain,
( sQ46_spl
| ~ function(sK11_skl) ),
inference(component_clause,[status(thm)],[f601]) ).
fof(f657,plain,
( sQ46_spl
| ~ empty(sK11_skl) ),
inference(resolution,[status(thm)],[f603,f45]) ).
fof(f658,plain,
( sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f657,f114]) ).
fof(f659,plain,
sQ46_spl,
inference(contradiction_clause,[status(thm)],[f658]) ).
fof(f672,definition,
( sQ52_spl
<=> relation(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f674,plain,
( sQ52_spl
| ~ relation(sK8_skl) ),
inference(component_clause,[status(thm)],[f672]) ).
fof(f693,plain,
( sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f674,f104]) ).
fof(f694,plain,
sQ52_spl,
inference(contradiction_clause,[status(thm)],[f693]) ).
fof(f797,definition,
( sQ70_spl
<=> relation(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f799,plain,
( sQ70_spl
| ~ relation(sK9_skl) ),
inference(component_clause,[status(thm)],[f797]) ).
fof(f812,definition,
( sQ74_spl
<=> relation(relation_dom(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f814,plain,
( sQ74_spl
| ~ relation(relation_dom(sK9_skl)) ),
inference(component_clause,[status(thm)],[f812]) ).
fof(f840,plain,
( sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f799,f108]) ).
fof(f841,plain,
sQ70_spl,
inference(contradiction_clause,[status(thm)],[f840]) ).
fof(f986,plain,
( sQ74_spl
| ~ empty(sK9_skl) ),
inference(resolution,[status(thm)],[f814,f99]) ).
fof(f988,plain,
( sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f986,f107]) ).
fof(f989,plain,
sQ74_spl,
inference(contradiction_clause,[status(thm)],[f988]) ).
fof(f1204,definition,
! [X0] :
( sQ124_spl
<=> ~ empty(sK13_skl(X0)) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f1205,plain,
! [X0] :
( ~ sQ124_spl
| ~ empty(sK13_skl(X0)) ),
inference(component_clause,[status(thm)],[f1204]) ).
fof(f1214,plain,
( ~ sQ124_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1205,f120]) ).
fof(f1215,plain,
~ sQ124_spl,
inference(contradiction_clause,[status(thm)],[f1214]) ).
fof(f1377,definition,
( sQ129_spl
<=> relation(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f1379,plain,
( sQ129_spl
| ~ relation(sK15_skl) ),
inference(component_clause,[status(thm)],[f1377]) ).
fof(f1469,plain,
( sQ129_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1379,f124]) ).
fof(f1470,plain,
sQ129_spl,
inference(contradiction_clause,[status(thm)],[f1469]) ).
fof(f1619,definition,
( sQ152_spl
<=> relation(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f1621,plain,
( sQ152_spl
| ~ relation(sK12_skl) ),
inference(component_clause,[status(thm)],[f1619]) ).
fof(f1711,plain,
( sQ152_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1621,f117]) ).
fof(f1712,plain,
sQ152_spl,
inference(contradiction_clause,[status(thm)],[f1711]) ).
fof(f7335,plain,
( ~ sQ18_spl
| ~ sQ21_spl
| apply(relation_composition(sK17_skl,sK16_skl),sK18_skl) = apply(sK16_skl,apply(sK17_skl,sK18_skl)) ),
inference(backward_demodulation,[status(thm)],[f356,f339]) ).
fof(f7340,plain,
( ~ sQ18_spl
| ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7335,f138]) ).
fof(f7341,plain,
( ~ sQ18_spl
| ~ sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f7340]) ).
fof(f7342,plain,
$false,
inference(sat_refutation,[status(thm)],[f181,f198,f200,f202,f238,f242,f254,f256,f258,f295,f341,f358,f519,f556,f590,f659,f694,f841,f989,f1215,f1470,f1712,f7341]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU214+3 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n001.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 06:04:30 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 19.15/2.99 % Refutation found
% 19.15/2.99 % SZS status Theorem for theBenchmark: Theorem is valid
% 19.15/2.99 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.73/3.04 % Elapsed time: 2.572671 seconds
% 8.73/3.04 % CPU time: 19.948881 seconds
% 8.73/3.04 % Total memory used: 226.181 MB
% 8.73/3.04 % Net memory used: 212.263 MB
%------------------------------------------------------------------------------