%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU214+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 : n009.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:42 PM UTC 2026
% Result : Theorem 0.13s 0.41s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 24
% Syntax : Number of formulae : 110 ( 22 unt; 13 def)
% Number of atoms : 434 ( 43 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 535 ( 211 ~; 214 |; 66 &)
% ( 25 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 14 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 5 con; 0-5 aty)
% Number of variables : 164 ( 147 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [A] :
( empty(A)
=> function(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] :
( empty(A)
=> relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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(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(f62,axiom,
! [A] : relation(identity_relation(A)),
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(f111,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f149,lemma,
! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( in(A,relation_dom(relation_composition(C,B)))
<=> ( in(apply(C,A),relation_dom(B))
& in(A,relation_dom(C)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f151,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,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)],[f151]) ).
fof(f210,lemma,
! [A,B,C] :
( ( function(C)
& relation(C) )
=> ( in(ordered_pair(A,B),C)
<=> ( B = apply(C,A)
& in(A,relation_dom(C)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f224,plain,
! [A] :
( function(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f225,plain,
! [X0] :
( function(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f226,plain,
! [A] :
( relation(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f227,plain,
! [X0] :
( relation(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f388,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(f389,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)],[f388]) ).
fof(f390,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)],[f389]) ).
fof(f391,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)],[f390]) ).
fof(f447,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(f448,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)],[f447]) ).
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) )
& ! [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)],[f448]) ).
fof(f450,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))],[f449]) ).
fof(f453,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)],[f450]) ).
fof(f475,plain,
! [A,B] :
( relation(relation_composition(A,B))
| ~ relation(B)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f60]) ).
fof(f476,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f479,plain,
! [X0] : relation(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f500,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(f502,plain,
! [X0,X1] :
( function(relation_composition(X0,X1))
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f500]) ).
fof(f593,plain,
empty(sK56_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56_skl]),skolemize(A,sK56_skl)],[f111]) ).
fof(f594,plain,
empty(sK56_skl),
inference(cnf_transformation,[status(thm)],[f593]) ).
fof(f709,plain,
! [A,B] :
( ! [C] :
( ( in(A,relation_dom(relation_composition(C,B)))
<=> ( in(apply(C,A),relation_dom(B))
& in(A,relation_dom(C)) ) )
| ~ function(C)
| ~ relation(C) )
| ~ function(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f149]) ).
fof(f710,plain,
! [A,B] :
( ! [C] :
( ( ( ~ in(apply(C,A),relation_dom(B))
| ~ in(A,relation_dom(C))
| in(A,relation_dom(relation_composition(C,B))) )
& ( ( in(apply(C,A),relation_dom(B))
& in(A,relation_dom(C)) )
| ~ in(A,relation_dom(relation_composition(C,B))) ) )
| ~ function(C)
| ~ relation(C) )
| ~ function(B)
| ~ relation(B) ),
inference(NNF_transformation,[status(thm)],[f709]) ).
fof(f711,plain,
! [B] :
( ! [C] :
( ( ! [A] :
( ~ in(apply(C,A),relation_dom(B))
| ~ in(A,relation_dom(C))
| in(A,relation_dom(relation_composition(C,B))) )
& ! [A] :
( ( in(apply(C,A),relation_dom(B))
& in(A,relation_dom(C)) )
| ~ in(A,relation_dom(relation_composition(C,B))) ) )
| ~ function(C)
| ~ relation(C) )
| ~ function(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f710]) ).
fof(f712,plain,
! [X0,X1,X2] :
( in(X2,relation_dom(X1))
| ~ in(X2,relation_dom(relation_composition(X1,X0)))
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f711]) ).
fof(f713,plain,
! [X0,X1,X2] :
( in(apply(X1,X2),relation_dom(X0))
| ~ in(X2,relation_dom(relation_composition(X1,X0)))
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f711]) ).
fof(f717,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)],[f152]) ).
fof(f718,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)],[f717]) ).
fof(f719,plain,
( apply(relation_composition(sK65_skl,sK64_skl),sK66_skl) != apply(sK64_skl,apply(sK65_skl,sK66_skl))
& in(sK66_skl,relation_dom(relation_composition(sK65_skl,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)],[f718]) ).
fof(f720,plain,
relation(sK64_skl),
inference(cnf_transformation,[status(thm)],[f719]) ).
fof(f721,plain,
function(sK64_skl),
inference(cnf_transformation,[status(thm)],[f719]) ).
fof(f722,plain,
relation(sK65_skl),
inference(cnf_transformation,[status(thm)],[f719]) ).
fof(f723,plain,
function(sK65_skl),
inference(cnf_transformation,[status(thm)],[f719]) ).
fof(f724,plain,
in(sK66_skl,relation_dom(relation_composition(sK65_skl,sK64_skl))),
inference(cnf_transformation,[status(thm)],[f719]) ).
fof(f725,plain,
apply(relation_composition(sK65_skl,sK64_skl),sK66_skl) != apply(sK64_skl,apply(sK65_skl,sK66_skl)),
inference(cnf_transformation,[status(thm)],[f719]) ).
fof(f885,plain,
! [A,B,C] :
( ( in(ordered_pair(A,B),C)
<=> ( B = apply(C,A)
& in(A,relation_dom(C)) ) )
| ~ function(C)
| ~ relation(C) ),
inference(pre_NNF_transformation,[status(thm)],[f210]) ).
fof(f886,plain,
! [A,B,C] :
( ( ( B != apply(C,A)
| ~ in(A,relation_dom(C))
| in(ordered_pair(A,B),C) )
& ( ( B = apply(C,A)
& in(A,relation_dom(C)) )
| ~ in(ordered_pair(A,B),C) ) )
| ~ function(C)
| ~ relation(C) ),
inference(NNF_transformation,[status(thm)],[f885]) ).
fof(f887,plain,
! [C] :
( ( ! [A,B] :
( B != apply(C,A)
| ~ in(A,relation_dom(C))
| in(ordered_pair(A,B),C) )
& ! [A,B] :
( ( B = apply(C,A)
& in(A,relation_dom(C)) )
| ~ in(ordered_pair(A,B),C) ) )
| ~ function(C)
| ~ relation(C) ),
inference(miniscoping,[status(thm)],[f886]) ).
fof(f889,plain,
! [X0,X1,X2] :
( X2 = apply(X0,X1)
| ~ in(ordered_pair(X1,X2),X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f887]) ).
fof(f963,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)],[f391]) ).
fof(f980,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)],[f453]) ).
fof(f1036,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)],[f980,f476]) ).
fof(f1040,plain,
relation(sK56_skl),
inference(resolution,[status(thm)],[f594,f227]) ).
fof(f1041,plain,
function(sK56_skl),
inference(resolution,[status(thm)],[f594,f225]) ).
fof(f1083,plain,
! [X0,X1,X2,X3,X4] :
( ~ in(ordered_pair(X4,X2),X1)
| ~ in(ordered_pair(X3,X4),X0)
| ~ relation(X1)
| ~ relation(X0)
| X2 = apply(relation_composition(X0,X1),X3)
| ~ function(relation_composition(X0,X1))
| ~ relation(relation_composition(X0,X1)) ),
inference(resolution,[status(thm)],[f889,f1036]) ).
fof(f1084,plain,
! [X0,X1,X2,X3,X4] :
( ~ in(ordered_pair(X4,X2),X1)
| ~ in(ordered_pair(X3,X4),X0)
| ~ relation(X1)
| ~ relation(X0)
| X2 = apply(relation_composition(X0,X1),X3)
| ~ function(relation_composition(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1083,f476]) ).
fof(f1086,plain,
( in(sK66_skl,relation_dom(sK65_skl))
| ~ function(sK65_skl)
| ~ relation(sK65_skl)
| ~ function(sK64_skl)
| ~ relation(sK64_skl) ),
inference(resolution,[status(thm)],[f712,f724]) ).
fof(f1087,definition,
( sQ9_spl
<=> relation(sK64_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1089,plain,
( sQ9_spl
| ~ relation(sK64_skl) ),
inference(component_clause,[status(thm)],[f1087]) ).
fof(f1090,definition,
( sQ10_spl
<=> function(sK64_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1092,plain,
( sQ10_spl
| ~ function(sK64_skl) ),
inference(component_clause,[status(thm)],[f1090]) ).
fof(f1093,definition,
( sQ11_spl
<=> relation(sK65_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1095,plain,
( sQ11_spl
| ~ relation(sK65_skl) ),
inference(component_clause,[status(thm)],[f1093]) ).
fof(f1096,definition,
( sQ12_spl
<=> function(sK65_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f1098,plain,
( sQ12_spl
| ~ function(sK65_skl) ),
inference(component_clause,[status(thm)],[f1096]) ).
fof(f1099,definition,
( sQ13_spl
<=> in(sK66_skl,relation_dom(sK65_skl)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f1102,plain,
( sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1086,f1087,f1090,f1093,f1096,f1099]) ).
fof(f1104,plain,
( in(apply(sK65_skl,sK66_skl),relation_dom(sK64_skl))
| ~ function(sK65_skl)
| ~ relation(sK65_skl)
| ~ function(sK64_skl)
| ~ relation(sK64_skl) ),
inference(resolution,[status(thm)],[f713,f724]) ).
fof(f1105,definition,
( sQ14_spl
<=> in(apply(sK65_skl,sK66_skl),relation_dom(sK64_skl)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f1108,plain,
( sQ14_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1104,f1087,f1090,f1093,f1096,f1105]) ).
fof(f1109,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1098,f723]) ).
fof(f1110,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f1109]) ).
fof(f1111,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1095,f722]) ).
fof(f1112,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f1111]) ).
fof(f1113,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1092,f721]) ).
fof(f1114,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f1113]) ).
fof(f1115,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1089,f720]) ).
fof(f1116,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f1115]) ).
fof(f1235,definition,
( sQ18_spl
<=> relation(sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1237,plain,
( sQ18_spl
| ~ relation(sK56_skl) ),
inference(component_clause,[status(thm)],[f1235]) ).
fof(f1238,definition,
( sQ19_spl
<=> function(sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f1240,plain,
( sQ19_spl
| ~ function(sK56_skl) ),
inference(component_clause,[status(thm)],[f1238]) ).
fof(f1298,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1237,f1040]) ).
fof(f1299,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f1298]) ).
fof(f1300,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1240,f1041]) ).
fof(f1301,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f1300]) ).
fof(f1348,definition,
( sQ27_spl
<=> empty(sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f1350,plain,
( sQ27_spl
| ~ empty(sK56_skl) ),
inference(component_clause,[status(thm)],[f1348]) ).
fof(f1364,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1350,f594]) ).
fof(f1365,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f1364]) ).
fof(f1383,definition,
( sQ29_spl
<=> relation(identity_relation(sK56_skl)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f1385,plain,
( sQ29_spl
| ~ relation(identity_relation(sK56_skl)) ),
inference(component_clause,[status(thm)],[f1383]) ).
fof(f1393,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1385,f479]) ).
fof(f1394,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f1393]) ).
fof(f1424,plain,
! [X0] :
( ~ in(ordered_pair(X0,apply(sK64_skl,apply(sK65_skl,sK66_skl))),sK64_skl)
| ~ in(ordered_pair(sK66_skl,X0),sK65_skl)
| ~ relation(sK64_skl)
| ~ relation(sK65_skl)
| ~ function(relation_composition(sK65_skl,sK64_skl)) ),
inference(resolution,[status(thm)],[f1084,f725]) ).
fof(f1425,definition,
( sQ33_spl
<=> function(relation_composition(sK65_skl,sK64_skl)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f1427,plain,
( sQ33_spl
| ~ function(relation_composition(sK65_skl,sK64_skl)) ),
inference(component_clause,[status(thm)],[f1425]) ).
fof(f1428,definition,
! [X0] :
( sQ34_spl
<=> ( ~ in(ordered_pair(X0,apply(sK64_skl,apply(sK65_skl,sK66_skl))),sK64_skl)
| ~ in(ordered_pair(sK66_skl,X0),sK65_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f1429,plain,
! [X0] :
( ~ sQ34_spl
| ~ in(ordered_pair(X0,apply(sK64_skl,apply(sK65_skl,sK66_skl))),sK64_skl)
| ~ in(ordered_pair(sK66_skl,X0),sK65_skl) ),
inference(component_clause,[status(thm)],[f1428]) ).
fof(f1431,plain,
( sQ34_spl
| ~ sQ9_spl
| ~ sQ11_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f1424,f1425,f1093,f1087,f1428]) ).
fof(f1477,plain,
( sQ33_spl
| ~ function(sK64_skl)
| ~ relation(sK64_skl)
| ~ function(sK65_skl)
| ~ relation(sK65_skl) ),
inference(resolution,[status(thm)],[f1427,f502]) ).
fof(f1480,plain,
( sQ33_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f1477,f1093,f1096,f1087,f1090,f1425]) ).
fof(f1489,plain,
( ~ sQ34_spl
| ~ in(apply(sK65_skl,sK66_skl),relation_dom(sK64_skl))
| ~ function(sK64_skl)
| ~ relation(sK64_skl)
| ~ in(ordered_pair(sK66_skl,apply(sK65_skl,sK66_skl)),sK65_skl) ),
inference(resolution,[status(thm)],[f1429,f963]) ).
fof(f1490,definition,
( sQ38_spl
<=> in(ordered_pair(sK66_skl,apply(sK65_skl,sK66_skl)),sK65_skl) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1492,plain,
( sQ38_spl
| ~ in(ordered_pair(sK66_skl,apply(sK65_skl,sK66_skl)),sK65_skl) ),
inference(component_clause,[status(thm)],[f1490]) ).
fof(f1493,plain,
( ~ sQ34_spl
| ~ sQ14_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f1489,f1490,f1087,f1090,f1105,f1428]) ).
fof(f1494,plain,
( sQ38_spl
| ~ in(sK66_skl,relation_dom(sK65_skl))
| ~ function(sK65_skl)
| ~ relation(sK65_skl) ),
inference(resolution,[status(thm)],[f1492,f963]) ).
fof(f1495,plain,
( sQ38_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f1494,f1093,f1096,f1099,f1490]) ).
fof(f1496,plain,
$false,
inference(sat_refutation,[status(thm)],[f1102,f1108,f1110,f1112,f1114,f1116,f1299,f1301,f1365,f1394,f1431,f1480,f1493,f1495]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU214+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.36 % Computer : n009.cluster.edu
% 0.07/0.36 % Model : x86_64 x86_64
% 0.07/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36 % Memory : 8046.5625MB
% 0.07/0.36 % OS : Linux 6.8.0-71-generic
% 0.07/0.36 % CPULimit : 300
% 0.07/0.36 % WCLimit : 300
% 0.07/0.36 % DateTime : Mon Sep 21 05:58:58 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 0.13/0.41 % Refutation found
% 0.13/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.45 % Elapsed time: 0.081985 seconds
% 0.13/0.45 % CPU time: 0.245683 seconds
% 0.13/0.45 % Total memory used: 91.647 MB
% 0.13/0.45 % Net memory used: 91.224 MB
%------------------------------------------------------------------------------