%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU215+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 0.12s 0.64s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 7
% Syntax : Number of formulae : 75 ( 10 unt; 0 def)
% Number of atoms : 380 ( 58 equ)
% Maximal formula atoms : 17 ( 5 avg)
% Number of connectives : 534 ( 229 ~; 213 |; 62 &)
% ( 12 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 4 con; 0-5 aty)
% Number of variables : 185 ( 161 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f27,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A] :
( relation(A)
=> ! [B] :
( B = relation_dom(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(C,D),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [A,B] :
( ( relation(B)
& relation(A) )
=> relation(relation_composition(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [A,B] :
( ( function(B)
& relation(B)
& function(A)
& relation(A) )
=> ( function(relation_composition(A,B))
& relation(relation_composition(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f151,lemma,
! [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/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,conjecture,
! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( in(A,relation_dom(B))
=> apply(relation_composition(B,C),A) = apply(C,apply(B,A)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f153,negated_conjecture,
~ ! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( in(A,relation_dom(B))
=> apply(relation_composition(B,C),A) = apply(C,apply(B,A)) ) ) ),
inference(negated_conjecture,[status(cth)],[f152]) ).
fof(f389,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)],[f27]) ).
fof(f390,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)],[f389]) ).
fof(f391,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)],[f390]) ).
fof(f392,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)],[f391]) ).
fof(f394,plain,
! [X0,X1,X2] :
( X2 = empty_set
| X2 != apply(X0,X1)
| in(X1,relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f396,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)],[f28]) ).
fof(f397,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)],[f396]) ).
fof(f398,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)],[f397]) ).
fof(f399,plain,
! [A] :
( ( ! [B] :
( ( ( in(ordered_pair(sK35_skl(B,A),sK36_skl(B,A)),A)
| in(sK35_skl(B,A),B) )
& ( ! [D] : ~ in(ordered_pair(sK35_skl(B,A),D),A)
| ~ in(sK35_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,sK34_skl(C,B,A)),A)
| ~ in(C,B) ) )
| B != relation_dom(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl,sK35_skl,sK36_skl]),skolemize(D,sK34_skl(C,B,A)),skolemize(C,sK35_skl(B,A)),skolemize(D,sK36_skl(B,A))],[f398]) ).
fof(f401,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)],[f399]) ).
fof(f448,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)],[f38]) ).
fof(f449,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)],[f448]) ).
fof(f450,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)],[f449]) ).
fof(f451,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ( ( ( in(ordered_pair(sK49_skl(C,B,A),sK48_skl(C,B,A)),B)
& in(ordered_pair(sK47_skl(C,B,A),sK49_skl(C,B,A)),A) )
| in(ordered_pair(sK47_skl(C,B,A),sK48_skl(C,B,A)),C) )
& ( ! [F] :
( ~ in(ordered_pair(F,sK48_skl(C,B,A)),B)
| ~ in(ordered_pair(sK47_skl(C,B,A),F),A) )
| ~ in(ordered_pair(sK47_skl(C,B,A),sK48_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(sK46_skl(E,D,C,B,A),E),B)
& in(ordered_pair(D,sK46_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,[sK46_skl,sK47_skl,sK48_skl,sK49_skl]),skolemize(F,sK46_skl(E,D,C,B,A)),skolemize(D,sK47_skl(C,B,A)),skolemize(E,sK48_skl(C,B,A)),skolemize(F,sK49_skl(C,B,A))],[f450]) ).
fof(f454,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ in(ordered_pair(X5,X4),X1)
| ~ in(ordered_pair(X3,X5),X0)
| in(ordered_pair(X3,X4),X2)
| X2 != relation_composition(X0,X1)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f451]) ).
fof(f476,plain,
! [A,B] :
( relation(relation_composition(A,B))
| ~ relation(B)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f60]) ).
fof(f477,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f476]) ).
fof(f501,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)],[f73]) ).
fof(f503,plain,
! [X0,X1] :
( function(relation_composition(X0,X1))
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f501]) ).
fof(f718,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)],[f151]) ).
fof(f719,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)],[f718]) ).
fof(f720,plain,
! [X0,X1,X2] :
( apply(relation_composition(X1,X0),X2) = apply(X0,apply(X1,X2))
| ~ in(X2,relation_dom(relation_composition(X1,X0)))
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f719]) ).
fof(f721,plain,
? [A,B] :
( ? [C] :
( apply(relation_composition(B,C),A) != apply(C,apply(B,A))
& in(A,relation_dom(B))
& function(C)
& relation(C) )
& function(B)
& relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f153]) ).
fof(f722,plain,
? [B] :
( ? [C] :
( ? [A] :
( apply(relation_composition(B,C),A) != apply(C,apply(B,A))
& in(A,relation_dom(B)) )
& function(C)
& relation(C) )
& function(B)
& relation(B) ),
inference(miniscoping,[status(thm)],[f721]) ).
fof(f723,plain,
( apply(relation_composition(sK64_skl,sK65_skl),sK66_skl) != apply(sK65_skl,apply(sK64_skl,sK66_skl))
& in(sK66_skl,relation_dom(sK64_skl))
& function(sK65_skl)
& relation(sK65_skl)
& function(sK64_skl)
& relation(sK64_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64_skl,sK65_skl,sK66_skl]),skolemize(B,sK64_skl),skolemize(C,sK65_skl),skolemize(A,sK66_skl)],[f722]) ).
fof(f724,plain,
relation(sK64_skl),
inference(cnf_transformation,[status(thm)],[f723]) ).
fof(f725,plain,
function(sK64_skl),
inference(cnf_transformation,[status(thm)],[f723]) ).
fof(f726,plain,
relation(sK65_skl),
inference(cnf_transformation,[status(thm)],[f723]) ).
fof(f727,plain,
function(sK65_skl),
inference(cnf_transformation,[status(thm)],[f723]) ).
fof(f728,plain,
in(sK66_skl,relation_dom(sK64_skl)),
inference(cnf_transformation,[status(thm)],[f723]) ).
fof(f729,plain,
apply(relation_composition(sK64_skl,sK65_skl),sK66_skl) != apply(sK65_skl,apply(sK64_skl,sK66_skl)),
inference(cnf_transformation,[status(thm)],[f723]) ).
fof(f967,plain,
! [X0,X1] :
( in(ordered_pair(X1,apply(X0,X1)),X0)
| ~ in(X1,relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f392]) ).
fof(f968,plain,
! [X0,X1] :
( apply(X0,X1) = empty_set
| in(X1,relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f394]) ).
fof(f971,plain,
! [X0,X1,X2] :
( ~ in(ordered_pair(X1,X2),X0)
| in(X1,relation_dom(X0))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f401]) ).
fof(f984,plain,
! [X0,X1,X2,X3,X4] :
( ~ in(ordered_pair(X4,X3),X1)
| ~ in(ordered_pair(X2,X4),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)],[f454]) ).
fof(f1030,plain,
! [X0,X1,X2,X3,X4] :
( ~ in(ordered_pair(X4,X3),X1)
| ~ in(ordered_pair(X2,X4),X0)
| in(ordered_pair(X2,X3),relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f984,f477]) ).
fof(f1031,plain,
! [X0,X1,X2,X3,X4] :
( in(X2,relation_dom(relation_composition(X0,X1)))
| ~ relation(relation_composition(X0,X1))
| ~ in(ordered_pair(X3,X4),X1)
| ~ in(ordered_pair(X2,X3),X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f1030,f971]) ).
fof(f1033,plain,
! [X0,X1,X2,X3,X4] :
( in(X2,relation_dom(relation_composition(X0,X1)))
| ~ in(ordered_pair(X3,X4),X1)
| ~ in(ordered_pair(X2,X3),X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1031,f477]) ).
fof(f1085,plain,
( ~ in(sK66_skl,relation_dom(relation_composition(sK64_skl,sK65_skl)))
| ~ function(sK64_skl)
| ~ relation(sK64_skl)
| ~ function(sK65_skl)
| ~ relation(sK65_skl) ),
inference(resolution,[status(thm)],[f720,f729]) ).
fof(f1086,plain,
( ~ in(sK66_skl,relation_dom(relation_composition(sK64_skl,sK65_skl)))
| ~ function(sK64_skl)
| ~ relation(sK64_skl)
| ~ function(sK65_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1085,f726]) ).
fof(f1120,plain,
( ~ in(sK66_skl,relation_dom(relation_composition(sK64_skl,sK65_skl)))
| ~ function(sK64_skl)
| ~ relation(sK64_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1086,f727]) ).
fof(f1121,plain,
( apply(relation_composition(sK64_skl,sK65_skl),sK66_skl) = empty_set
| ~ function(relation_composition(sK64_skl,sK65_skl))
| ~ relation(relation_composition(sK64_skl,sK65_skl))
| ~ function(sK64_skl)
| ~ relation(sK64_skl) ),
inference(resolution,[status(thm)],[f1120,f968]) ).
fof(f1122,plain,
( apply(relation_composition(sK64_skl,sK65_skl),sK66_skl) = empty_set
| ~ function(relation_composition(sK64_skl,sK65_skl))
| ~ relation(relation_composition(sK64_skl,sK65_skl))
| ~ function(sK64_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1121,f724]) ).
fof(f1123,plain,
( apply(relation_composition(sK64_skl,sK65_skl),sK66_skl) = empty_set
| ~ function(relation_composition(sK64_skl,sK65_skl))
| ~ relation(relation_composition(sK64_skl,sK65_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1122,f725]) ).
fof(f1386,plain,
! [X0,X1] :
( ~ function(sK64_skl)
| ~ relation(sK64_skl)
| ~ in(ordered_pair(X0,X1),sK65_skl)
| ~ in(ordered_pair(sK66_skl,X0),sK64_skl)
| ~ relation(sK65_skl)
| ~ relation(sK64_skl) ),
inference(resolution,[status(thm)],[f1033,f1120]) ).
fof(f1395,plain,
! [X0,X1] :
( ~ function(sK64_skl)
| ~ in(ordered_pair(X0,X1),sK65_skl)
| ~ in(ordered_pair(sK66_skl,X0),sK64_skl)
| ~ relation(sK65_skl)
| ~ relation(sK64_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f1386]) ).
fof(f1396,plain,
! [X0,X1] :
( ~ function(sK64_skl)
| ~ in(ordered_pair(X0,X1),sK65_skl)
| ~ in(ordered_pair(sK66_skl,X0),sK64_skl)
| ~ relation(sK65_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1395,f724]) ).
fof(f1489,plain,
! [X0,X1] :
( ~ function(sK64_skl)
| ~ in(ordered_pair(X0,X1),sK65_skl)
| ~ in(ordered_pair(sK66_skl,X0),sK64_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1396,f726]) ).
fof(f1490,plain,
! [X0] :
( ~ in(sK66_skl,relation_dom(sK64_skl))
| ~ function(sK64_skl)
| ~ relation(sK64_skl)
| ~ function(sK64_skl)
| ~ in(ordered_pair(apply(sK64_skl,sK66_skl),X0),sK65_skl) ),
inference(resolution,[status(thm)],[f1489,f967]) ).
fof(f1491,plain,
! [X0] :
( ~ in(sK66_skl,relation_dom(sK64_skl))
| ~ relation(sK64_skl)
| ~ function(sK64_skl)
| ~ in(ordered_pair(apply(sK64_skl,sK66_skl),X0),sK65_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f1490]) ).
fof(f1492,plain,
! [X0] :
( ~ in(sK66_skl,relation_dom(sK64_skl))
| ~ relation(sK64_skl)
| ~ in(ordered_pair(apply(sK64_skl,sK66_skl),X0),sK65_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1491,f725]) ).
fof(f1493,plain,
! [X0] :
( ~ in(sK66_skl,relation_dom(sK64_skl))
| ~ in(ordered_pair(apply(sK64_skl,sK66_skl),X0),sK65_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1492,f724]) ).
fof(f1494,plain,
( ~ in(apply(sK64_skl,sK66_skl),relation_dom(sK65_skl))
| ~ function(sK65_skl)
| ~ relation(sK65_skl)
| ~ in(sK66_skl,relation_dom(sK64_skl)) ),
inference(resolution,[status(thm)],[f1493,f967]) ).
fof(f1495,plain,
( ~ in(apply(sK64_skl,sK66_skl),relation_dom(sK65_skl))
| ~ function(sK65_skl)
| ~ relation(sK65_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1494,f728]) ).
fof(f1496,plain,
( ~ in(apply(sK64_skl,sK66_skl),relation_dom(sK65_skl))
| ~ function(sK65_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1495,f726]) ).
fof(f1498,plain,
( apply(sK65_skl,apply(sK64_skl,sK66_skl)) = empty_set
| ~ function(sK65_skl)
| ~ relation(sK65_skl)
| ~ function(sK65_skl) ),
inference(resolution,[status(thm)],[f1496,f968]) ).
fof(f1500,plain,
( apply(sK65_skl,apply(sK64_skl,sK66_skl)) = empty_set
| ~ relation(sK65_skl)
| ~ function(sK65_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f1498]) ).
fof(f1501,plain,
( apply(sK65_skl,apply(sK64_skl,sK66_skl)) = empty_set
| ~ relation(sK65_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1500,f727]) ).
fof(f1502,plain,
apply(relation_composition(sK64_skl,sK65_skl),sK66_skl) != empty_set,
inference(backward_demodulation,[status(thm)],[f1503,f729]) ).
fof(f1503,plain,
apply(sK65_skl,apply(sK64_skl,sK66_skl)) = empty_set,
inference(forward_subsumption_resolution,[status(thm)],[f1501,f726]) ).
fof(f1534,plain,
( ~ function(relation_composition(sK64_skl,sK65_skl))
| ~ relation(relation_composition(sK64_skl,sK65_skl)) ),
inference(backward_subsumption_resolution,[status(thm)],[f1123,f1502]) ).
fof(f1637,plain,
( ~ function(sK65_skl)
| ~ relation(sK65_skl)
| ~ function(sK64_skl)
| ~ relation(sK64_skl)
| ~ relation(relation_composition(sK64_skl,sK65_skl)) ),
inference(resolution,[status(thm)],[f1534,f503]) ).
fof(f1639,plain,
( ~ function(sK65_skl)
| ~ relation(sK65_skl)
| ~ function(sK64_skl)
| ~ relation(sK64_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1637,f477]) ).
fof(f1640,plain,
( ~ function(sK65_skl)
| ~ relation(sK65_skl)
| ~ function(sK64_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1639,f724]) ).
fof(f1641,plain,
( ~ relation(sK65_skl)
| ~ function(sK64_skl) ),
inference(resolution,[status(thm)],[f1640,f727]) ).
fof(f1643,plain,
~ relation(sK65_skl),
inference(forward_subsumption_resolution,[status(thm)],[f1641,f725]) ).
fof(f1644,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1643,f726]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU215+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 06:00:43 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.39 % Drodi V4.1.1
% 0.12/0.64 % Refutation found
% 0.12/0.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.67 % Elapsed time: 0.307903 seconds
% 0.12/0.67 % CPU time: 1.921119 seconds
% 0.12/0.67 % Total memory used: 135.779 MB
% 0.12/0.67 % Net memory used: 133.196 MB
%------------------------------------------------------------------------------