%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU191+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 : 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:36 PM UTC 2026
% Result : Theorem 0.16s 0.77s
% Output : CNFRefutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 52
% Syntax : Number of formulae : 232 ( 30 unt; 35 def)
% Number of atoms : 722 ( 121 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 833 ( 343 ~; 362 |; 62 &)
% ( 47 <=>; 18 =>; 0 <=; 1 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 41 ( 39 usr; 36 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 7 con; 0-5 aty)
% Number of variables : 295 ( 265 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [A,B] :
( relation(B)
=> ( B = identity_relation(A)
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
<=> ( C = D
& in(C,A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B] :
( A = B
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,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(f50,axiom,
! [A,B] :
( ( relation(B)
& relation(A) )
=> relation(relation_composition(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [A] : relation(identity_relation(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
( relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f92,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f94,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,lemma,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> subset(relation_dom(relation_composition(A,B)),relation_dom(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,lemma,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> subset(relation_rng(relation_composition(A,B)),relation_rng(B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f143,lemma,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ( subset(relation_rng(A),relation_dom(B))
=> relation_dom(relation_composition(A,B)) = relation_dom(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f146,lemma,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ( subset(relation_dom(A),relation_rng(B))
=> relation_rng(relation_composition(B,A)) = relation_rng(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f157,lemma,
( relation_rng(empty_set) = empty_set
& relation_dom(empty_set) = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f164,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f166,lemma,
! [A] :
( relation_rng(identity_relation(A)) = A
& relation_dom(identity_relation(A)) = A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f167,conjecture,
! [A,B,C,D] :
( relation(D)
=> ( in(ordered_pair(A,B),relation_composition(identity_relation(C),D))
<=> ( in(ordered_pair(A,B),D)
& in(A,C) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f168,negated_conjecture,
~ ! [A,B,C,D] :
( relation(D)
=> ( in(ordered_pair(A,B),relation_composition(identity_relation(C),D))
<=> ( in(ordered_pair(A,B),D)
& in(A,C) ) ) ),
inference(negated_conjecture,[status(cth)],[f167]) ).
fof(f188,plain,
! [A,B] :
( ( B = identity_relation(A)
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
<=> ( C = D
& in(C,A) ) ) )
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f189,plain,
! [A,B] :
( ( ( ? [C,D] :
( ( ( C = D
& in(C,A) )
| in(ordered_pair(C,D),B) )
& ( C != D
| ~ in(C,A)
| ~ in(ordered_pair(C,D),B) ) )
| B = identity_relation(A) )
& ( ! [C,D] :
( ( C != D
| ~ in(C,A)
| in(ordered_pair(C,D),B) )
& ( ( C = D
& in(C,A) )
| ~ in(ordered_pair(C,D),B) ) )
| B != identity_relation(A) ) )
| ~ relation(B) ),
inference(NNF_transformation,[status(thm)],[f188]) ).
fof(f190,plain,
! [B] :
( ( ! [A] :
( ? [C,D] :
( ( ( C = D
& in(C,A) )
| in(ordered_pair(C,D),B) )
& ( C != D
| ~ in(C,A)
| ~ in(ordered_pair(C,D),B) ) )
| B = identity_relation(A) )
& ! [A] :
( ( ! [C,D] :
( C != D
| ~ in(C,A)
| in(ordered_pair(C,D),B) )
& ! [C,D] :
( ( C = D
& in(C,A) )
| ~ in(ordered_pair(C,D),B) ) )
| B != identity_relation(A) ) )
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f189]) ).
fof(f191,plain,
! [B] :
( ( ! [A] :
( ( ( ( sK0_skl(A,B) = sK1_skl(A,B)
& in(sK0_skl(A,B),A) )
| in(ordered_pair(sK0_skl(A,B),sK1_skl(A,B)),B) )
& ( sK0_skl(A,B) != sK1_skl(A,B)
| ~ in(sK0_skl(A,B),A)
| ~ in(ordered_pair(sK0_skl(A,B),sK1_skl(A,B)),B) ) )
| B = identity_relation(A) )
& ! [A] :
( ( ! [C,D] :
( C != D
| ~ in(C,A)
| in(ordered_pair(C,D),B) )
& ! [C,D] :
( ( C = D
& in(C,A) )
| ~ in(ordered_pair(C,D),B) ) )
| B != identity_relation(A) ) )
| ~ relation(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(C,sK0_skl(A,B)),skolemize(D,sK1_skl(A,B))],[f190]) ).
fof(f192,plain,
! [X0,X1,X2,X3] :
( in(X2,X1)
| ~ in(ordered_pair(X2,X3),X0)
| X0 != identity_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f193,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ in(ordered_pair(X2,X3),X0)
| X0 != identity_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f194,plain,
! [X0,X1,X2,X3] :
( X2 != X3
| ~ in(X2,X1)
| in(ordered_pair(X2,X3),X0)
| X0 != identity_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f196,plain,
! [X0,X1] :
( in(sK0_skl(X1,X0),X1)
| in(ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)),X0)
| X0 = identity_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f197,plain,
! [X0,X1] :
( sK0_skl(X1,X0) = sK1_skl(X1,X0)
| in(ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)),X0)
| X0 = identity_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f198,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f199,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)],[f198]) ).
fof(f200,plain,
! [X0,X1] :
( subset(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f229,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f12]) ).
fof(f230,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f229]) ).
fof(f231,plain,
( ! [A] :
( in(sK9_skl(A),A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(B,sK9_skl(A))],[f230]) ).
fof(f232,plain,
! [X0,X1] :
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f343,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)],[f30]) ).
fof(f344,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)],[f343]) ).
fof(f345,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)],[f344]) ).
fof(f346,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ( ( ( in(ordered_pair(sK35_skl(C,B,A),sK34_skl(C,B,A)),B)
& in(ordered_pair(sK33_skl(C,B,A),sK35_skl(C,B,A)),A) )
| in(ordered_pair(sK33_skl(C,B,A),sK34_skl(C,B,A)),C) )
& ( ! [F] :
( ~ in(ordered_pair(F,sK34_skl(C,B,A)),B)
| ~ in(ordered_pair(sK33_skl(C,B,A),F),A) )
| ~ in(ordered_pair(sK33_skl(C,B,A),sK34_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(sK32_skl(E,D,C,B,A),E),B)
& in(ordered_pair(D,sK32_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,[sK32_skl,sK33_skl,sK34_skl,sK35_skl]),skolemize(F,sK32_skl(E,D,C,B,A)),skolemize(D,sK33_skl(C,B,A)),skolemize(E,sK34_skl(C,B,A)),skolemize(F,sK35_skl(C,B,A))],[f345]) ).
fof(f347,plain,
! [X0,X1,X2,X3,X4] :
( in(ordered_pair(X3,sK32_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)],[f346]) ).
fof(f348,plain,
! [X0,X1,X2,X3,X4] :
( in(ordered_pair(sK32_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)],[f346]) ).
fof(f349,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)],[f346]) ).
fof(f371,plain,
! [A,B] :
( relation(relation_composition(A,B))
| ~ relation(B)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f372,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f371]) ).
fof(f375,plain,
! [X0] : relation(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f401,plain,
relation(empty_set),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f465,plain,
( relation(sK39_skl)
& empty(sK39_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39_skl]),skolemize(A,sK39_skl)],[f92]) ).
fof(f466,plain,
empty(sK39_skl),
inference(cnf_transformation,[status(thm)],[f465]) ).
fof(f467,plain,
relation(sK39_skl),
inference(cnf_transformation,[status(thm)],[f465]) ).
fof(f472,plain,
empty(sK41_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl]),skolemize(A,sK41_skl)],[f94]) ).
fof(f473,plain,
empty(sK41_skl),
inference(cnf_transformation,[status(thm)],[f472]) ).
fof(f599,plain,
! [A] :
( ! [B] :
( subset(relation_dom(relation_composition(A,B)),relation_dom(A))
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f140]) ).
fof(f600,plain,
! [X0,X1] :
( subset(relation_dom(relation_composition(X0,X1)),relation_dom(X0))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f599]) ).
fof(f601,plain,
! [A] :
( ! [B] :
( subset(relation_rng(relation_composition(A,B)),relation_rng(B))
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f141]) ).
fof(f602,plain,
! [X0,X1] :
( subset(relation_rng(relation_composition(X0,X1)),relation_rng(X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f601]) ).
fof(f605,plain,
! [A] :
( ! [B] :
( relation_dom(relation_composition(A,B)) = relation_dom(A)
| ~ subset(relation_rng(A),relation_dom(B))
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f143]) ).
fof(f606,plain,
! [X0,X1] :
( relation_dom(relation_composition(X0,X1)) = relation_dom(X0)
| ~ subset(relation_rng(X0),relation_dom(X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f605]) ).
fof(f611,plain,
! [A] :
( ! [B] :
( relation_rng(relation_composition(B,A)) = relation_rng(A)
| ~ subset(relation_dom(A),relation_rng(B))
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f146]) ).
fof(f612,plain,
! [X0,X1] :
( relation_rng(relation_composition(X1,X0)) = relation_rng(X0)
| ~ subset(relation_dom(X0),relation_rng(X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f611]) ).
fof(f638,plain,
relation_dom(empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f639,plain,
relation_rng(empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f657,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f164]) ).
fof(f658,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f657]) ).
fof(f661,plain,
( ! [A] : relation_rng(identity_relation(A)) = A
& ! [A] : relation_dom(identity_relation(A)) = A ),
inference(miniscoping,[status(thm)],[f166]) ).
fof(f662,plain,
! [X0] : relation_dom(identity_relation(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f661]) ).
fof(f663,plain,
! [X0] : relation_rng(identity_relation(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f661]) ).
fof(f664,plain,
? [A,B,C,D] :
( ( in(ordered_pair(A,B),relation_composition(identity_relation(C),D))
<~> ( in(ordered_pair(A,B),D)
& in(A,C) ) )
& relation(D) ),
inference(pre_NNF_transformation,[status(thm)],[f168]) ).
fof(f665,plain,
? [A,B,C,D] :
( ( ~ in(ordered_pair(A,B),D)
| ~ in(A,C)
| ~ in(ordered_pair(A,B),relation_composition(identity_relation(C),D)) )
& ( ( in(ordered_pair(A,B),D)
& in(A,C) )
| in(ordered_pair(A,B),relation_composition(identity_relation(C),D)) )
& relation(D) ),
inference(NNF_transformation,[status(thm)],[f664]) ).
fof(f666,plain,
? [D] :
( ? [A,B,C] :
( ( ~ in(ordered_pair(A,B),D)
| ~ in(A,C)
| ~ in(ordered_pair(A,B),relation_composition(identity_relation(C),D)) )
& ( ( in(ordered_pair(A,B),D)
& in(A,C) )
| in(ordered_pair(A,B),relation_composition(identity_relation(C),D)) ) )
& relation(D) ),
inference(miniscoping,[status(thm)],[f665]) ).
fof(f667,plain,
( ( ~ in(ordered_pair(sK52_skl,sK53_skl),sK51_skl)
| ~ in(sK52_skl,sK54_skl)
| ~ in(ordered_pair(sK52_skl,sK53_skl),relation_composition(identity_relation(sK54_skl),sK51_skl)) )
& ( ( in(ordered_pair(sK52_skl,sK53_skl),sK51_skl)
& in(sK52_skl,sK54_skl) )
| in(ordered_pair(sK52_skl,sK53_skl),relation_composition(identity_relation(sK54_skl),sK51_skl)) )
& relation(sK51_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51_skl,sK52_skl,sK53_skl,sK54_skl]),skolemize(D,sK51_skl),skolemize(A,sK52_skl),skolemize(B,sK53_skl),skolemize(C,sK54_skl)],[f666]) ).
fof(f668,plain,
relation(sK51_skl),
inference(cnf_transformation,[status(thm)],[f667]) ).
fof(f669,plain,
( in(sK52_skl,sK54_skl)
| in(ordered_pair(sK52_skl,sK53_skl),relation_composition(identity_relation(sK54_skl),sK51_skl)) ),
inference(cnf_transformation,[status(thm)],[f667]) ).
fof(f670,plain,
( in(ordered_pair(sK52_skl,sK53_skl),sK51_skl)
| in(ordered_pair(sK52_skl,sK53_skl),relation_composition(identity_relation(sK54_skl),sK51_skl)) ),
inference(cnf_transformation,[status(thm)],[f667]) ).
fof(f671,plain,
( ~ in(ordered_pair(sK52_skl,sK53_skl),sK51_skl)
| ~ in(sK52_skl,sK54_skl)
| ~ in(ordered_pair(sK52_skl,sK53_skl),relation_composition(identity_relation(sK54_skl),sK51_skl)) ),
inference(cnf_transformation,[status(thm)],[f667]) ).
fof(f708,definition,
( sQ0_spl
<=> in(ordered_pair(sK52_skl,sK53_skl),relation_composition(identity_relation(sK54_skl),sK51_skl)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f709,plain,
( ~ sQ0_spl
| in(ordered_pair(sK52_skl,sK53_skl),relation_composition(identity_relation(sK54_skl),sK51_skl)) ),
inference(component_clause,[status(thm)],[f708]) ).
fof(f710,plain,
( sQ0_spl
| ~ in(ordered_pair(sK52_skl,sK53_skl),relation_composition(identity_relation(sK54_skl),sK51_skl)) ),
inference(component_clause,[status(thm)],[f708]) ).
fof(f711,definition,
( sQ1_spl
<=> in(sK52_skl,sK54_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f712,plain,
( ~ sQ1_spl
| in(sK52_skl,sK54_skl) ),
inference(component_clause,[status(thm)],[f711]) ).
fof(f714,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f669,f708,f711]) ).
fof(f715,definition,
( sQ2_spl
<=> in(ordered_pair(sK52_skl,sK53_skl),sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f716,plain,
( ~ sQ2_spl
| in(ordered_pair(sK52_skl,sK53_skl),sK51_skl) ),
inference(component_clause,[status(thm)],[f715]) ).
fof(f718,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f670,f708,f715]) ).
fof(f719,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f671,f708,f711,f715]) ).
fof(f720,plain,
! [X0,X1,X2] :
( in(X1,X0)
| ~ in(ordered_pair(X1,X2),identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f192]) ).
fof(f721,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ in(ordered_pair(X1,X2),identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f193]) ).
fof(f722,plain,
! [X0,X1] :
( ~ in(X1,X0)
| in(ordered_pair(X1,X1),identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f194]) ).
fof(f723,plain,
! [X0] : subset(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f200]) ).
fof(f732,plain,
! [X0] : ~ in(X0,empty_set),
inference(destructive_equality_resolution,[status(thm)],[f232]) ).
fof(f759,plain,
! [X0,X1,X2,X3] :
( in(ordered_pair(X2,sK32_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)],[f347]) ).
fof(f760,plain,
! [X0,X1,X2,X3] :
( in(ordered_pair(sK32_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)],[f348]) ).
fof(f761,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)],[f349]) ).
fof(f768,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(backward_subsumption_resolution,[status(thm)],[f761,f372]) ).
fof(f769,plain,
! [X0,X1,X2,X3] :
( in(ordered_pair(sK32_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(backward_subsumption_resolution,[status(thm)],[f760,f372]) ).
fof(f770,plain,
! [X0,X1,X2,X3] :
( in(ordered_pair(X2,sK32_skl(X3,X2,relation_composition(X0,X1),X1,X0)),X0)
| ~ in(ordered_pair(X2,X3),relation_composition(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f759,f372]) ).
fof(f771,plain,
! [X0,X1] :
( ~ in(X0,X1)
| in(ordered_pair(X0,X0),identity_relation(X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[f722,f375]) ).
fof(f772,plain,
! [X0,X1,X2] :
( X0 = X1
| ~ in(ordered_pair(X0,X1),identity_relation(X2)) ),
inference(backward_subsumption_resolution,[status(thm)],[f721,f375]) ).
fof(f773,plain,
! [X0,X1,X2] :
( in(X0,X2)
| ~ in(ordered_pair(X0,X1),identity_relation(X2)) ),
inference(backward_subsumption_resolution,[status(thm)],[f720,f375]) ).
fof(f791,plain,
! [X0,X1] :
( subset(relation_dom(relation_composition(identity_relation(X0),X1)),X0)
| ~ relation(X1)
| ~ relation(identity_relation(X0)) ),
inference(paramodulation,[status(thm)],[f662,f600]) ).
fof(f792,plain,
! [X0,X1] :
( subset(relation_dom(relation_composition(identity_relation(X1),X0)),X1)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f791,f375]) ).
fof(f813,plain,
! [X0,X1] :
( relation_dom(relation_composition(identity_relation(X0),X1)) = relation_dom(identity_relation(X0))
| ~ subset(X0,relation_dom(X1))
| ~ relation(X1)
| ~ relation(identity_relation(X0)) ),
inference(paramodulation,[status(thm)],[f663,f606]) ).
fof(f814,plain,
! [X0,X1] :
( relation_dom(relation_composition(X0,identity_relation(X1))) = relation_dom(X0)
| ~ subset(relation_rng(X0),X1)
| ~ relation(identity_relation(X1))
| ~ relation(X0) ),
inference(paramodulation,[status(thm)],[f662,f606]) ).
fof(f815,plain,
! [X0,X1] :
( relation_dom(relation_composition(identity_relation(X0),X1)) = X0
| ~ subset(X0,relation_dom(X1))
| ~ relation(X1)
| ~ relation(identity_relation(X0)) ),
inference(forward_demodulation,[status(thm)],[f662,f813]) ).
fof(f816,plain,
! [X0,X1] :
( relation_dom(relation_composition(identity_relation(X1),X0)) = X1
| ~ subset(X1,relation_dom(X0))
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f815,f375]) ).
fof(f817,plain,
! [X0,X1] :
( relation_dom(relation_composition(X0,identity_relation(X1))) = relation_dom(X0)
| ~ subset(relation_rng(X0),X1)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f814,f375]) ).
fof(f820,plain,
! [X0,X1] :
( relation_rng(relation_composition(identity_relation(X1),X0)) = relation_rng(X0)
| ~ subset(relation_dom(X0),X1)
| ~ relation(identity_relation(X1))
| ~ relation(X0) ),
inference(paramodulation,[status(thm)],[f663,f612]) ).
fof(f823,plain,
! [X0,X1] :
( relation_rng(relation_composition(identity_relation(X1),X0)) = relation_rng(X0)
| ~ subset(relation_dom(X0),X1)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f820,f375]) ).
fof(f828,plain,
! [X0] :
( in(sK0_skl(X0,empty_set),X0)
| empty_set = identity_relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f196,f732]) ).
fof(f833,definition,
( sQ3_spl
<=> relation(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f835,plain,
( sQ3_spl
| ~ relation(empty_set) ),
inference(component_clause,[status(thm)],[f833]) ).
fof(f836,definition,
! [X0] :
( sQ4_spl
<=> ( in(sK0_skl(X0,empty_set),X0)
| empty_set = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f839,plain,
( sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f828,f833,f836]) ).
fof(f840,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f835,f401]) ).
fof(f841,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f840]) ).
fof(f844,plain,
! [X0] :
( sK0_skl(X0,empty_set) = sK1_skl(X0,empty_set)
| empty_set = identity_relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f197,f732]) ).
fof(f850,definition,
! [X0] :
( sQ5_spl
<=> ( sK0_skl(X0,empty_set) = sK1_skl(X0,empty_set)
| empty_set = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f853,plain,
( sQ5_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f844,f833,f850]) ).
fof(f866,plain,
! [X0] :
( relation_dom(relation_composition(identity_relation(relation_dom(X0)),X0)) = relation_dom(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f816,f723]) ).
fof(f890,plain,
relation_dom(relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl)) = relation_dom(sK51_skl),
inference(resolution,[status(thm)],[f866,f668]) ).
fof(f898,plain,
( ~ sQ0_spl
| in(ordered_pair(sK32_skl(sK53_skl,sK52_skl,relation_composition(identity_relation(sK54_skl),sK51_skl),sK51_skl,identity_relation(sK54_skl)),sK53_skl),sK51_skl)
| ~ relation(sK51_skl)
| ~ relation(identity_relation(sK54_skl)) ),
inference(resolution,[status(thm)],[f769,f709]) ).
fof(f902,definition,
( sQ6_spl
<=> relation(identity_relation(sK54_skl)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f904,plain,
( sQ6_spl
| ~ relation(identity_relation(sK54_skl)) ),
inference(component_clause,[status(thm)],[f902]) ).
fof(f905,definition,
( sQ7_spl
<=> relation(sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f907,plain,
( sQ7_spl
| ~ relation(sK51_skl) ),
inference(component_clause,[status(thm)],[f905]) ).
fof(f908,definition,
( sQ8_spl
<=> in(ordered_pair(sK32_skl(sK53_skl,sK52_skl,relation_composition(identity_relation(sK54_skl),sK51_skl),sK51_skl,identity_relation(sK54_skl)),sK53_skl),sK51_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f909,plain,
( ~ sQ8_spl
| in(ordered_pair(sK32_skl(sK53_skl,sK52_skl,relation_composition(identity_relation(sK54_skl),sK51_skl),sK51_skl,identity_relation(sK54_skl)),sK53_skl),sK51_skl) ),
inference(component_clause,[status(thm)],[f908]) ).
fof(f911,plain,
( ~ sQ0_spl
| sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f898,f902,f905,f908,f708]) ).
fof(f915,plain,
( ~ sQ0_spl
| in(ordered_pair(sK52_skl,sK32_skl(sK53_skl,sK52_skl,relation_composition(identity_relation(sK54_skl),sK51_skl),sK51_skl,identity_relation(sK54_skl))),identity_relation(sK54_skl))
| ~ relation(sK51_skl)
| ~ relation(identity_relation(sK54_skl)) ),
inference(resolution,[status(thm)],[f770,f709]) ).
fof(f919,definition,
( sQ9_spl
<=> in(ordered_pair(sK52_skl,sK32_skl(sK53_skl,sK52_skl,relation_composition(identity_relation(sK54_skl),sK51_skl),sK51_skl,identity_relation(sK54_skl))),identity_relation(sK54_skl)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f920,plain,
( ~ sQ9_spl
| in(ordered_pair(sK52_skl,sK32_skl(sK53_skl,sK52_skl,relation_composition(identity_relation(sK54_skl),sK51_skl),sK51_skl,identity_relation(sK54_skl))),identity_relation(sK54_skl)) ),
inference(component_clause,[status(thm)],[f919]) ).
fof(f922,plain,
( ~ sQ0_spl
| sQ9_spl
| ~ sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f915,f902,f905,f919,f708]) ).
fof(f924,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f907,f668]) ).
fof(f925,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f924]) ).
fof(f926,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f904,f375]) ).
fof(f927,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f926]) ).
fof(f943,definition,
( sQ10_spl
<=> relation(identity_relation(identity_relation(identity_relation(relation_composition(identity_relation(sK54_skl),sK51_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f945,plain,
( sQ10_spl
| ~ relation(identity_relation(identity_relation(identity_relation(relation_composition(identity_relation(sK54_skl),sK51_skl))))) ),
inference(component_clause,[status(thm)],[f943]) ).
fof(f950,definition,
( sQ12_spl
<=> relation(identity_relation(identity_relation(relation_composition(identity_relation(sK54_skl),sK51_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f952,plain,
( sQ12_spl
| ~ relation(identity_relation(identity_relation(relation_composition(identity_relation(sK54_skl),sK51_skl)))) ),
inference(component_clause,[status(thm)],[f950]) ).
fof(f957,definition,
( sQ14_spl
<=> relation(identity_relation(relation_composition(identity_relation(sK54_skl),sK51_skl))) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f959,plain,
( sQ14_spl
| ~ relation(identity_relation(relation_composition(identity_relation(sK54_skl),sK51_skl))) ),
inference(component_clause,[status(thm)],[f957]) ).
fof(f964,definition,
( sQ16_spl
<=> relation(relation_composition(identity_relation(sK54_skl),sK51_skl)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f966,plain,
( sQ16_spl
| ~ relation(relation_composition(identity_relation(sK54_skl),sK51_skl)) ),
inference(component_clause,[status(thm)],[f964]) ).
fof(f978,plain,
( ~ sQ1_spl
| in(ordered_pair(sK52_skl,sK52_skl),identity_relation(sK54_skl)) ),
inference(resolution,[status(thm)],[f712,f771]) ).
fof(f989,plain,
! [X0] :
( sQ0_spl
| ~ in(ordered_pair(X0,sK53_skl),sK51_skl)
| ~ in(ordered_pair(sK52_skl,X0),identity_relation(sK54_skl))
| ~ relation(sK51_skl)
| ~ relation(identity_relation(sK54_skl)) ),
inference(resolution,[status(thm)],[f710,f768]) ).
fof(f990,definition,
! [X0] :
( sQ20_spl
<=> ( ~ in(ordered_pair(X0,sK53_skl),sK51_skl)
| ~ in(ordered_pair(sK52_skl,X0),identity_relation(sK54_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f991,plain,
! [X0] :
( ~ sQ20_spl
| ~ in(ordered_pair(X0,sK53_skl),sK51_skl)
| ~ in(ordered_pair(sK52_skl,X0),identity_relation(sK54_skl)) ),
inference(component_clause,[status(thm)],[f990]) ).
fof(f993,plain,
( sQ0_spl
| sQ20_spl
| ~ sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f989,f902,f905,f990,f708]) ).
fof(f1018,plain,
! [X0] :
( relation_dom(relation_composition(identity_relation(X0),empty_set)) = X0
| ~ subset(X0,empty_set)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f638,f816]) ).
fof(f1019,plain,
! [X0] :
( relation_rng(relation_composition(X0,empty_set)) = relation_rng(empty_set)
| ~ subset(empty_set,relation_rng(X0))
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f638,f612]) ).
fof(f1020,plain,
! [X0] :
( relation_dom(relation_composition(X0,empty_set)) = relation_dom(X0)
| ~ subset(relation_rng(X0),empty_set)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(paramodulation,[status(thm)],[f638,f606]) ).
fof(f1021,plain,
! [X0] :
( subset(relation_dom(relation_composition(empty_set,X0)),empty_set)
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f638,f600]) ).
fof(f1022,definition,
! [X0] :
( sQ22_spl
<=> ( relation_dom(relation_composition(identity_relation(X0),empty_set)) = X0
| ~ subset(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f1025,plain,
( sQ22_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1018,f833,f1022]) ).
fof(f1026,definition,
! [X0] :
( sQ23_spl
<=> ( relation_rng(relation_composition(X0,empty_set)) = relation_rng(empty_set)
| ~ subset(empty_set,relation_rng(X0))
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f1029,plain,
( sQ23_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1019,f833,f1026]) ).
fof(f1030,definition,
! [X0] :
( sQ24_spl
<=> ( relation_dom(relation_composition(X0,empty_set)) = relation_dom(X0)
| ~ subset(relation_rng(X0),empty_set)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f1033,plain,
( ~ sQ3_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f1020,f1030,f833]) ).
fof(f1034,definition,
! [X0] :
( sQ25_spl
<=> ( subset(relation_dom(relation_composition(empty_set,X0)),empty_set)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f1037,plain,
( sQ25_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1021,f833,f1034]) ).
fof(f1040,plain,
! [X0] :
( relation_dom(relation_composition(empty_set,identity_relation(X0))) = relation_dom(empty_set)
| ~ subset(empty_set,X0)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f639,f817]) ).
fof(f1041,plain,
! [X0] :
( relation_rng(relation_composition(empty_set,X0)) = relation_rng(X0)
| ~ subset(relation_dom(X0),empty_set)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(paramodulation,[status(thm)],[f639,f612]) ).
fof(f1042,plain,
! [X0] :
( relation_dom(relation_composition(empty_set,X0)) = relation_dom(empty_set)
| ~ subset(empty_set,relation_dom(X0))
| ~ relation(X0)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f639,f606]) ).
fof(f1043,plain,
! [X0] :
( subset(relation_rng(relation_composition(X0,empty_set)),empty_set)
| ~ relation(empty_set)
| ~ relation(X0) ),
inference(paramodulation,[status(thm)],[f639,f602]) ).
fof(f1044,definition,
! [X0] :
( sQ26_spl
<=> ( relation_dom(relation_composition(empty_set,identity_relation(X0))) = relation_dom(empty_set)
| ~ subset(empty_set,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f1047,plain,
( sQ26_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1040,f833,f1044]) ).
fof(f1048,definition,
! [X0] :
( sQ27_spl
<=> ( relation_rng(relation_composition(empty_set,X0)) = relation_rng(X0)
| ~ subset(relation_dom(X0),empty_set)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f1051,plain,
( ~ sQ3_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f1041,f1048,f833]) ).
fof(f1052,definition,
! [X0] :
( sQ28_spl
<=> ( relation_dom(relation_composition(empty_set,X0)) = relation_dom(empty_set)
| ~ subset(empty_set,relation_dom(X0))
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f1055,plain,
( sQ28_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1042,f833,f1052]) ).
fof(f1056,definition,
! [X0] :
( sQ29_spl
<=> ( subset(relation_rng(relation_composition(X0,empty_set)),empty_set)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f1059,plain,
( ~ sQ3_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f1043,f1056,f833]) ).
fof(f1103,plain,
( ~ sQ1_spl
| ~ sQ20_spl
| ~ in(ordered_pair(sK52_skl,sK53_skl),sK51_skl) ),
inference(resolution,[status(thm)],[f991,f978]) ).
fof(f1104,plain,
( ~ sQ1_spl
| ~ sQ20_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1103,f716]) ).
fof(f1105,plain,
( ~ sQ1_spl
| ~ sQ20_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f1104]) ).
fof(f1106,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f945,f375]) ).
fof(f1107,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f1106]) ).
fof(f1108,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f952,f375]) ).
fof(f1109,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f1108]) ).
fof(f1110,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f959,f375]) ).
fof(f1111,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f1110]) ).
fof(f1114,plain,
( sQ16_spl
| ~ relation(sK51_skl)
| ~ relation(identity_relation(sK54_skl)) ),
inference(resolution,[status(thm)],[f966,f372]) ).
fof(f1125,plain,
( sQ16_spl
| ~ sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1114,f902,f905,f964]) ).
fof(f1135,plain,
sK41_skl = empty_set,
inference(resolution,[status(thm)],[f658,f473]) ).
fof(f1136,plain,
sK39_skl = empty_set,
inference(resolution,[status(thm)],[f658,f466]) ).
fof(f1153,plain,
! [X0] : ~ in(X0,sK41_skl),
inference(backward_demodulation,[status(thm)],[f1135,f732]) ).
fof(f1202,plain,
sK39_skl = sK41_skl,
inference(forward_demodulation,[status(thm)],[f1135,f1136]) ).
fof(f1222,plain,
! [X0] : ~ in(X0,sK39_skl),
inference(forward_demodulation,[status(thm)],[f1202,f1153]) ).
fof(f1310,plain,
! [X0] :
( sK0_skl(X0,sK39_skl) = sK1_skl(X0,sK39_skl)
| sK39_skl = identity_relation(X0)
| ~ relation(sK39_skl) ),
inference(resolution,[status(thm)],[f1222,f197]) ).
fof(f1311,plain,
! [X0] :
( in(sK0_skl(X0,sK39_skl),X0)
| sK39_skl = identity_relation(X0)
| ~ relation(sK39_skl) ),
inference(resolution,[status(thm)],[f1222,f196]) ).
fof(f1312,definition,
( sQ38_spl
<=> relation(sK39_skl) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1314,plain,
( sQ38_spl
| ~ relation(sK39_skl) ),
inference(component_clause,[status(thm)],[f1312]) ).
fof(f1315,definition,
! [X0] :
( sQ39_spl
<=> ( sK0_skl(X0,sK39_skl) = sK1_skl(X0,sK39_skl)
| sK39_skl = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1318,plain,
( sQ39_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f1310,f1312,f1315]) ).
fof(f1319,definition,
! [X0] :
( sQ40_spl
<=> ( in(sK0_skl(X0,sK39_skl),X0)
| sK39_skl = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1322,plain,
( sQ40_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f1311,f1312,f1319]) ).
fof(f1323,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1314,f467]) ).
fof(f1324,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f1323]) ).
fof(f1337,plain,
( subset(relation_dom(sK51_skl),relation_dom(sK51_skl))
| ~ relation(sK51_skl) ),
inference(paramodulation,[status(thm)],[f890,f792]) ).
fof(f1338,plain,
( subset(relation_dom(sK51_skl),relation_dom(identity_relation(relation_dom(sK51_skl))))
| ~ relation(sK51_skl)
| ~ relation(identity_relation(relation_dom(sK51_skl))) ),
inference(paramodulation,[status(thm)],[f890,f600]) ).
fof(f1339,plain,
! [X0] :
( relation_dom(relation_composition(identity_relation(X0),relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl))) = X0
| ~ subset(X0,relation_dom(sK51_skl))
| ~ relation(relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl)) ),
inference(paramodulation,[status(thm)],[f890,f816]) ).
fof(f1340,plain,
! [X0] :
( relation_rng(relation_composition(X0,relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl))) = relation_rng(relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl))
| ~ subset(relation_dom(sK51_skl),relation_rng(X0))
| ~ relation(X0)
| ~ relation(relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl)) ),
inference(paramodulation,[status(thm)],[f890,f612]) ).
fof(f1341,plain,
! [X0] :
( relation_dom(relation_composition(X0,relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl))) = relation_dom(X0)
| ~ subset(relation_rng(X0),relation_dom(sK51_skl))
| ~ relation(relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl))
| ~ relation(X0) ),
inference(paramodulation,[status(thm)],[f890,f606]) ).
fof(f1342,plain,
! [X0] :
( subset(relation_dom(relation_composition(relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl),X0)),relation_dom(sK51_skl))
| ~ relation(X0)
| ~ relation(relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl)) ),
inference(paramodulation,[status(thm)],[f890,f600]) ).
fof(f1343,definition,
( sQ41_spl
<=> subset(relation_dom(sK51_skl),relation_dom(sK51_skl)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1346,plain,
( sQ41_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1337,f905,f1343]) ).
fof(f1347,definition,
( sQ42_spl
<=> relation(identity_relation(relation_dom(sK51_skl))) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1349,plain,
( sQ42_spl
| ~ relation(identity_relation(relation_dom(sK51_skl))) ),
inference(component_clause,[status(thm)],[f1347]) ).
fof(f1350,definition,
( sQ43_spl
<=> subset(relation_dom(sK51_skl),relation_dom(identity_relation(relation_dom(sK51_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1353,plain,
( sQ43_spl
| ~ sQ7_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f1338,f1347,f905,f1350]) ).
fof(f1354,definition,
( sQ44_spl
<=> relation(relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1356,plain,
( sQ44_spl
| ~ relation(relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl)) ),
inference(component_clause,[status(thm)],[f1354]) ).
fof(f1357,definition,
! [X0] :
( sQ45_spl
<=> ( relation_dom(relation_composition(identity_relation(X0),relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl))) = X0
| ~ subset(X0,relation_dom(sK51_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1360,plain,
( sQ45_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f1339,f1354,f1357]) ).
fof(f1361,definition,
! [X0] :
( sQ46_spl
<=> ( relation_rng(relation_composition(X0,relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl))) = relation_rng(relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl))
| ~ subset(relation_dom(sK51_skl),relation_rng(X0))
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1364,plain,
( sQ46_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f1340,f1354,f1361]) ).
fof(f1365,definition,
! [X0] :
( sQ47_spl
<=> ( relation_dom(relation_composition(X0,relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl))) = relation_dom(X0)
| ~ subset(relation_rng(X0),relation_dom(sK51_skl))
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1368,plain,
( ~ sQ44_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f1341,f1365,f1354]) ).
fof(f1369,definition,
! [X0] :
( sQ48_spl
<=> ( subset(relation_dom(relation_composition(relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl),X0)),relation_dom(sK51_skl))
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1372,plain,
( sQ48_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f1342,f1354,f1369]) ).
fof(f1373,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1349,f375]) ).
fof(f1374,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f1373]) ).
fof(f1406,plain,
! [X0] :
( relation_rng(relation_composition(identity_relation(X0),relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl))) = relation_rng(relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl))
| ~ subset(relation_dom(sK51_skl),X0)
| ~ relation(relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl)) ),
inference(paramodulation,[status(thm)],[f890,f823]) ).
fof(f1410,definition,
! [X0] :
( sQ50_spl
<=> ( relation_rng(relation_composition(identity_relation(X0),relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl))) = relation_rng(relation_composition(identity_relation(relation_dom(sK51_skl)),sK51_skl))
| ~ subset(relation_dom(sK51_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1413,plain,
( sQ50_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f1406,f1354,f1410]) ).
fof(f1451,plain,
( sQ44_spl
| ~ relation(sK51_skl)
| ~ relation(identity_relation(relation_dom(sK51_skl))) ),
inference(resolution,[status(thm)],[f1356,f372]) ).
fof(f1459,plain,
( sQ44_spl
| ~ sQ7_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f1451,f1347,f905,f1354]) ).
fof(f1463,plain,
( ~ sQ9_spl
| in(sK52_skl,sK54_skl) ),
inference(resolution,[status(thm)],[f920,f773]) ).
fof(f1464,plain,
( ~ sQ9_spl
| sK52_skl = sK32_skl(sK53_skl,sK52_skl,relation_composition(identity_relation(sK54_skl),sK51_skl),sK51_skl,identity_relation(sK54_skl)) ),
inference(resolution,[status(thm)],[f920,f772]) ).
fof(f1468,plain,
( ~ sQ9_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f1463,f711,f919]) ).
fof(f1470,plain,
( ~ sQ8_spl
| ~ sQ9_spl
| in(ordered_pair(sK52_skl,sK53_skl),sK51_skl) ),
inference(backward_demodulation,[status(thm)],[f1464,f909]) ).
fof(f1481,plain,
( ~ sQ8_spl
| ~ sQ9_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1470,f715,f919,f908]) ).
fof(f1485,plain,
$false,
inference(sat_refutation,[status(thm)],[f714,f718,f719,f839,f841,f853,f911,f922,f925,f927,f993,f1025,f1029,f1033,f1037,f1047,f1051,f1055,f1059,f1105,f1107,f1109,f1111,f1125,f1318,f1322,f1324,f1346,f1353,f1360,f1364,f1368,f1372,f1374,f1413,f1459,f1468,f1481]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU191+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n001.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 21 06:02:29 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.40 % Drodi V4.1.1
% 0.16/0.77 % Refutation found
% 0.16/0.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.77 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.16/0.80 % Elapsed time: 0.410404 seconds
% 0.16/0.80 % CPU time: 2.650568 seconds
% 0.16/0.80 % Total memory used: 142.805 MB
% 0.16/0.80 % Net memory used: 139.448 MB
%------------------------------------------------------------------------------