%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU058+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:09 PM UTC 2026
% Result : Theorem 0.13s 0.64s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 31
% Syntax : Number of formulae : 172 ( 9 unt; 25 def)
% Number of atoms : 630 ( 62 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 799 ( 341 ~; 380 |; 42 &)
% ( 31 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 32 ( 30 usr; 26 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-3 aty)
% Number of variables : 192 ( 182 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B,C] :
( C = relation_inverse_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(apply(A,D),B)
& in(D,relation_dom(A)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B,C] :
( C = set_intersection2(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,conjecture,
! [A,B,C] :
( ( function(C)
& relation(C) )
=> relation_inverse_image(C,set_intersection2(A,B)) = set_intersection2(relation_inverse_image(C,A),relation_inverse_image(C,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,negated_conjecture,
~ ! [A,B,C] :
( ( function(C)
& relation(C) )
=> relation_inverse_image(C,set_intersection2(A,B)) = set_intersection2(relation_inverse_image(C,A),relation_inverse_image(C,B)) ),
inference(negated_conjecture,[status(cth)],[f28]) ).
fof(f32,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f41,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f50,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f51,plain,
! [A] :
( ! [B,C] :
( C = relation_inverse_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(apply(A,D),B)
& in(D,relation_dom(A)) ) ) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f52,plain,
! [A] :
( ! [B,C] :
( ( ? [D] :
( ( ( in(apply(A,D),B)
& in(D,relation_dom(A)) )
| in(D,C) )
& ( ~ in(apply(A,D),B)
| ~ in(D,relation_dom(A))
| ~ in(D,C) ) )
| C = relation_inverse_image(A,B) )
& ( ! [D] :
( ( ~ in(apply(A,D),B)
| ~ in(D,relation_dom(A))
| in(D,C) )
& ( ( in(apply(A,D),B)
& in(D,relation_dom(A)) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ function(A)
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f51]) ).
fof(f53,plain,
! [A] :
( ( ! [B,C] :
( ? [D] :
( ( ( in(apply(A,D),B)
& in(D,relation_dom(A)) )
| in(D,C) )
& ( ~ in(apply(A,D),B)
| ~ in(D,relation_dom(A))
| ~ in(D,C) ) )
| C = relation_inverse_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ~ in(apply(A,D),B)
| ~ in(D,relation_dom(A))
| in(D,C) )
& ! [D] :
( ( in(apply(A,D),B)
& in(D,relation_dom(A)) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ function(A)
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f52]) ).
fof(f54,plain,
! [A] :
( ( ! [B,C] :
( ( ( ( in(apply(A,sK0_skl(C,B,A)),B)
& in(sK0_skl(C,B,A),relation_dom(A)) )
| in(sK0_skl(C,B,A),C) )
& ( ~ in(apply(A,sK0_skl(C,B,A)),B)
| ~ in(sK0_skl(C,B,A),relation_dom(A))
| ~ in(sK0_skl(C,B,A),C) ) )
| C = relation_inverse_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ~ in(apply(A,D),B)
| ~ in(D,relation_dom(A))
| in(D,C) )
& ! [D] :
( ( in(apply(A,D),B)
& in(D,relation_dom(A)) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(D,sK0_skl(C,B,A))],[f53]) ).
fof(f55,plain,
! [X0,X1,X2,X3] :
( in(X3,relation_dom(X0))
| ~ in(X3,X1)
| X1 != relation_inverse_image(X0,X2)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f56,plain,
! [X0,X1,X2,X3] :
( in(apply(X0,X3),X2)
| ~ in(X3,X1)
| X1 != relation_inverse_image(X0,X2)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f57,plain,
! [X0,X1,X2,X3] :
( ~ in(apply(X0,X3),X2)
| ~ in(X3,relation_dom(X0))
| in(X3,X1)
| X1 != relation_inverse_image(X0,X2)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f58,plain,
! [X0,X1,X2] :
( ~ in(apply(X0,sK0_skl(X1,X2,X0)),X2)
| ~ in(sK0_skl(X1,X2,X0),relation_dom(X0))
| ~ in(sK0_skl(X1,X2,X0),X1)
| X1 = relation_inverse_image(X0,X2)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f59,plain,
! [X0,X1,X2] :
( in(sK0_skl(X1,X2,X0),relation_dom(X0))
| in(sK0_skl(X1,X2,X0),X1)
| X1 = relation_inverse_image(X0,X2)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f60,plain,
! [X0,X1,X2] :
( in(apply(X0,sK0_skl(X1,X2,X0)),X2)
| in(sK0_skl(X1,X2,X0),X1)
| X1 = relation_inverse_image(X0,X2)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f61,plain,
! [A,B,C] :
( ( ? [D] :
( ( ( in(D,B)
& in(D,A) )
| in(D,C) )
& ( ~ in(D,B)
| ~ in(D,A)
| ~ in(D,C) ) )
| C = set_intersection2(A,B) )
& ( ! [D] :
( ( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f62,plain,
( ! [A,B,C] :
( ? [D] :
( ( ( in(D,B)
& in(D,A) )
| in(D,C) )
& ( ~ in(D,B)
| ~ in(D,A)
| ~ in(D,C) ) )
| C = set_intersection2(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ! [D] :
( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(miniscoping,[status(thm)],[f61]) ).
fof(f63,plain,
( ! [A,B,C] :
( ( ( ( in(sK1_skl(C,B,A),B)
& in(sK1_skl(C,B,A),A) )
| in(sK1_skl(C,B,A),C) )
& ( ~ in(sK1_skl(C,B,A),B)
| ~ in(sK1_skl(C,B,A),A)
| ~ in(sK1_skl(C,B,A),C) ) )
| C = set_intersection2(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ! [D] :
( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(D,sK1_skl(C,B,A))],[f62]) ).
fof(f64,plain,
! [X0,X1,X2,X3] :
( in(X3,X1)
| ~ in(X3,X0)
| X0 != set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f65,plain,
! [X0,X1,X2,X3] :
( in(X3,X2)
| ~ in(X3,X0)
| X0 != set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f66,plain,
! [X0,X1,X2,X3] :
( ~ in(X3,X2)
| ~ in(X3,X1)
| in(X3,X0)
| X0 != set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f121,plain,
? [A,B,C] :
( relation_inverse_image(C,set_intersection2(A,B)) != set_intersection2(relation_inverse_image(C,A),relation_inverse_image(C,B))
& function(C)
& relation(C) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f122,plain,
? [C] :
( ? [A,B] : relation_inverse_image(C,set_intersection2(A,B)) != set_intersection2(relation_inverse_image(C,A),relation_inverse_image(C,B))
& function(C)
& relation(C) ),
inference(miniscoping,[status(thm)],[f121]) ).
fof(f123,plain,
( relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl)) != set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl))
& function(sK13_skl)
& relation(sK13_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(C,sK13_skl),skolemize(A,sK14_skl),skolemize(B,sK15_skl)],[f122]) ).
fof(f124,plain,
relation(sK13_skl),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f125,plain,
function(sK13_skl),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f126,plain,
relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl)) != set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f130,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f131,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f156,plain,
! [X0,X1,X2] :
( in(X1,relation_dom(X0))
| ~ in(X1,relation_inverse_image(X0,X2))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f55]) ).
fof(f157,plain,
! [X0,X1,X2] :
( in(apply(X0,X1),X2)
| ~ in(X1,relation_inverse_image(X0,X2))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f56]) ).
fof(f158,plain,
! [X0,X1,X2] :
( ~ in(apply(X0,X1),X2)
| ~ in(X1,relation_dom(X0))
| in(X1,relation_inverse_image(X0,X2))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f57]) ).
fof(f159,plain,
! [X0,X1,X2] :
( in(X0,X1)
| ~ in(X0,set_intersection2(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f64]) ).
fof(f160,plain,
! [X0,X1,X2] :
( in(X0,X2)
| ~ in(X0,set_intersection2(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f65]) ).
fof(f161,plain,
! [X0,X1,X2] :
( ~ in(X0,X2)
| ~ in(X0,X1)
| in(X0,set_intersection2(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f66]) ).
fof(f178,plain,
! [X0,X1,X2] :
( ~ in(X1,sK0_skl(X1,X2,X0))
| in(sK0_skl(X1,X2,X0),relation_dom(X0))
| X1 = relation_inverse_image(X0,X2)
| ~ function(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f59,f41]) ).
fof(f180,plain,
! [X0,X1,X2] :
( ~ in(X1,sK0_skl(X1,X2,X0))
| in(apply(X0,sK0_skl(X1,X2,X0)),X2)
| X1 = relation_inverse_image(X0,X2)
| ~ function(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f60,f41]) ).
fof(f195,plain,
! [X0,X1,X2] :
( ~ in(X1,X0)
| ~ in(X0,set_intersection2(X1,X2)) ),
inference(resolution,[status(thm)],[f159,f41]) ).
fof(f209,plain,
! [X0,X1,X2] :
( ~ in(X2,X0)
| ~ in(X0,set_intersection2(X1,X2)) ),
inference(resolution,[status(thm)],[f160,f41]) ).
fof(f224,plain,
! [X0,X1,X2,X3] :
( ~ in(X2,sK0_skl(X2,set_intersection2(X0,X3),X1))
| X2 = relation_inverse_image(X1,set_intersection2(X0,X3))
| ~ function(X1)
| ~ relation(X1)
| ~ in(X0,apply(X1,sK0_skl(X2,set_intersection2(X0,X3),X1))) ),
inference(resolution,[status(thm)],[f195,f180]) ).
fof(f229,plain,
! [X0,X1,X2,X3] :
( in(apply(X3,sK0_skl(set_intersection2(X0,X1),X2,X3)),X2)
| set_intersection2(X0,X1) = relation_inverse_image(X3,X2)
| ~ function(X3)
| ~ relation(X3)
| ~ in(X0,sK0_skl(set_intersection2(X0,X1),X2,X3)) ),
inference(resolution,[status(thm)],[f195,f60]) ).
fof(f230,plain,
! [X0,X1,X2,X3] :
( in(sK0_skl(set_intersection2(X0,X1),X2,X3),relation_dom(X3))
| set_intersection2(X0,X1) = relation_inverse_image(X3,X2)
| ~ function(X3)
| ~ relation(X3)
| ~ in(X0,sK0_skl(set_intersection2(X0,X1),X2,X3)) ),
inference(resolution,[status(thm)],[f195,f59]) ).
fof(f259,plain,
! [X0,X1,X2,X3] :
( in(apply(X3,sK0_skl(set_intersection2(X1,X0),X2,X3)),X2)
| set_intersection2(X0,X1) = relation_inverse_image(X3,X2)
| ~ function(X3)
| ~ relation(X3)
| ~ in(X0,sK0_skl(set_intersection2(X0,X1),X2,X3)) ),
inference(paramodulation,[status(thm)],[f50,f229]) ).
fof(f266,plain,
! [X0,X1,X2,X3] :
( in(sK0_skl(set_intersection2(X1,X0),X2,X3),relation_dom(X3))
| set_intersection2(X0,X1) = relation_inverse_image(X3,X2)
| ~ function(X3)
| ~ relation(X3)
| ~ in(X0,sK0_skl(set_intersection2(X0,X1),X2,X3)) ),
inference(paramodulation,[status(thm)],[f50,f230]) ).
fof(f376,plain,
! [X0,X1,X2,X3] :
( in(apply(X3,sK0_skl(set_intersection2(X1,X0),X2,X3)),X2)
| set_intersection2(X1,X0) = relation_inverse_image(X3,X2)
| ~ function(X3)
| ~ relation(X3)
| ~ in(X0,sK0_skl(set_intersection2(X1,X0),X2,X3)) ),
inference(resolution,[status(thm)],[f209,f60]) ).
fof(f377,plain,
! [X0,X1,X2,X3] :
( in(sK0_skl(set_intersection2(X1,X0),X2,X3),relation_dom(X3))
| set_intersection2(X1,X0) = relation_inverse_image(X3,X2)
| ~ function(X3)
| ~ relation(X3)
| ~ in(X0,sK0_skl(set_intersection2(X1,X0),X2,X3)) ),
inference(resolution,[status(thm)],[f209,f59]) ).
fof(f411,plain,
! [X0,X1,X2,X3] :
( in(apply(X3,sK0_skl(set_intersection2(X0,X1),X2,X3)),X2)
| set_intersection2(X1,X0) = relation_inverse_image(X3,X2)
| ~ function(X3)
| ~ relation(X3)
| ~ in(X0,sK0_skl(set_intersection2(X1,X0),X2,X3)) ),
inference(paramodulation,[status(thm)],[f50,f376]) ).
fof(f418,plain,
! [X0,X1,X2,X3] :
( in(sK0_skl(set_intersection2(X0,X1),X2,X3),relation_dom(X3))
| set_intersection2(X1,X0) = relation_inverse_image(X3,X2)
| ~ function(X3)
| ~ relation(X3)
| ~ in(X0,sK0_skl(set_intersection2(X1,X0),X2,X3)) ),
inference(paramodulation,[status(thm)],[f50,f377]) ).
fof(f499,definition,
( sQ1_spl
<=> relation(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f501,plain,
( sQ1_spl
| ~ relation(sK13_skl) ),
inference(component_clause,[status(thm)],[f499]) ).
fof(f502,definition,
( sQ2_spl
<=> function(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f504,plain,
( sQ2_spl
| ~ function(sK13_skl) ),
inference(component_clause,[status(thm)],[f502]) ).
fof(f505,definition,
( sQ3_spl
<=> in(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f574,plain,
( ~ in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),set_intersection2(sK14_skl,sK15_skl))
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_dom(sK13_skl))
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)))
| ~ function(sK13_skl)
| ~ relation(sK13_skl) ),
inference(resolution,[status(thm)],[f58,f126]) ).
fof(f575,definition,
( sQ4_spl
<=> in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f576,plain,
( ~ sQ4_spl
| in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl))) ),
inference(component_clause,[status(thm)],[f575]) ).
fof(f577,plain,
( sQ4_spl
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl))) ),
inference(component_clause,[status(thm)],[f575]) ).
fof(f578,definition,
( sQ5_spl
<=> in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_dom(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f580,plain,
( sQ5_spl
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_dom(sK13_skl)) ),
inference(component_clause,[status(thm)],[f578]) ).
fof(f581,definition,
( sQ6_spl
<=> in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),set_intersection2(sK14_skl,sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f582,plain,
( ~ sQ6_spl
| in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),set_intersection2(sK14_skl,sK15_skl)) ),
inference(component_clause,[status(thm)],[f581]) ).
fof(f583,plain,
( sQ6_spl
| ~ in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),set_intersection2(sK14_skl,sK15_skl)) ),
inference(component_clause,[status(thm)],[f581]) ).
fof(f584,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ2_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f574,f499,f502,f575,f578,f581]) ).
fof(f585,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f504,f125]) ).
fof(f586,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f585]) ).
fof(f587,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f501,f124]) ).
fof(f588,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f587]) ).
fof(f599,plain,
( sQ6_spl
| set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl)
| ~ in(relation_inverse_image(sK13_skl,sK14_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
inference(resolution,[status(thm)],[f583,f411]) ).
fof(f600,plain,
( sQ6_spl
| set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl)
| ~ in(relation_inverse_image(sK13_skl,sK15_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
inference(resolution,[status(thm)],[f583,f376]) ).
fof(f601,plain,
( sQ6_spl
| set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl)
| ~ in(relation_inverse_image(sK13_skl,sK15_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
inference(resolution,[status(thm)],[f583,f259]) ).
fof(f602,plain,
( sQ6_spl
| set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl)
| ~ in(relation_inverse_image(sK13_skl,sK14_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
inference(resolution,[status(thm)],[f583,f229]) ).
fof(f603,plain,
( sQ6_spl
| ~ in(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl))
| set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl) ),
inference(resolution,[status(thm)],[f583,f180]) ).
fof(f605,plain,
( sQ6_spl
| ~ in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),sK15_skl)
| ~ in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),sK14_skl) ),
inference(resolution,[status(thm)],[f583,f161]) ).
fof(f609,definition,
( sQ9_spl
<=> in(relation_inverse_image(sK13_skl,sK14_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f612,definition,
( sQ10_spl
<=> set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f613,plain,
( ~ sQ10_spl
| set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl)) ),
inference(component_clause,[status(thm)],[f612]) ).
fof(f614,plain,
( sQ10_spl
| set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)) != relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl)) ),
inference(component_clause,[status(thm)],[f612]) ).
fof(f615,plain,
( sQ6_spl
| sQ10_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f599,f609,f499,f502,f612,f581]) ).
fof(f616,definition,
( sQ11_spl
<=> in(relation_inverse_image(sK13_skl,sK15_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f619,definition,
( sQ12_spl
<=> set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f620,plain,
( ~ sQ12_spl
| set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl)) ),
inference(component_clause,[status(thm)],[f619]) ).
fof(f622,plain,
( sQ6_spl
| sQ12_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f600,f616,f499,f502,f619,f581]) ).
fof(f623,definition,
( sQ13_spl
<=> in(relation_inverse_image(sK13_skl,sK15_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f626,plain,
( sQ6_spl
| sQ10_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f601,f623,f499,f502,f612,f581]) ).
fof(f627,definition,
( sQ14_spl
<=> in(relation_inverse_image(sK13_skl,sK14_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f630,plain,
( sQ6_spl
| sQ12_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f602,f627,f499,f502,f619,f581]) ).
fof(f631,plain,
( sQ6_spl
| ~ sQ3_spl
| sQ12_spl
| ~ sQ2_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f603,f499,f502,f619,f505,f581]) ).
fof(f636,definition,
( sQ16_spl
<=> in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f637,plain,
( ~ sQ16_spl
| in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),sK14_skl) ),
inference(component_clause,[status(thm)],[f636]) ).
fof(f638,plain,
( sQ16_spl
| ~ in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),sK14_skl) ),
inference(component_clause,[status(thm)],[f636]) ).
fof(f639,definition,
( sQ17_spl
<=> in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f641,plain,
( sQ17_spl
| ~ in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),sK15_skl) ),
inference(component_clause,[status(thm)],[f639]) ).
fof(f642,plain,
( sQ6_spl
| ~ sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f605,f636,f639,f581]) ).
fof(f650,plain,
( ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f620,f126]) ).
fof(f651,plain,
~ sQ12_spl,
inference(contradiction_clause,[status(thm)],[f650]) ).
fof(f654,plain,
( sQ4_spl
| in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),set_intersection2(sK14_skl,sK15_skl))
| set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl) ),
inference(resolution,[status(thm)],[f577,f60]) ).
fof(f655,plain,
( sQ4_spl
| in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_dom(sK13_skl))
| set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl) ),
inference(resolution,[status(thm)],[f577,f59]) ).
fof(f656,plain,
( sQ4_spl
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_inverse_image(sK13_skl,sK15_skl))
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_inverse_image(sK13_skl,sK14_skl)) ),
inference(resolution,[status(thm)],[f577,f161]) ).
fof(f660,plain,
( sQ4_spl
| sQ6_spl
| sQ12_spl
| ~ sQ2_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f654,f499,f502,f619,f581,f575]) ).
fof(f661,plain,
( sQ4_spl
| sQ5_spl
| sQ12_spl
| ~ sQ2_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f655,f499,f502,f619,f578,f575]) ).
fof(f662,definition,
( sQ20_spl
<=> in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_inverse_image(sK13_skl,sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f664,plain,
( sQ20_spl
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_inverse_image(sK13_skl,sK14_skl)) ),
inference(component_clause,[status(thm)],[f662]) ).
fof(f665,definition,
( sQ21_spl
<=> in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_inverse_image(sK13_skl,sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f667,plain,
( sQ21_spl
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_inverse_image(sK13_skl,sK15_skl)) ),
inference(component_clause,[status(thm)],[f665]) ).
fof(f668,plain,
( sQ4_spl
| ~ sQ21_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f656,f662,f665,f575]) ).
fof(f682,plain,
( ~ sQ10_spl
| set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl)) ),
inference(paramodulation,[status(thm)],[f50,f613]) ).
fof(f724,plain,
( ~ sQ10_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f682,f619,f612]) ).
fof(f777,plain,
( sQ17_spl
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_inverse_image(sK13_skl,sK15_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl) ),
inference(resolution,[status(thm)],[f641,f157]) ).
fof(f778,plain,
! [X0] :
( sQ17_spl
| ~ in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),set_intersection2(X0,sK15_skl)) ),
inference(resolution,[status(thm)],[f641,f160]) ).
fof(f781,plain,
( sQ17_spl
| ~ sQ21_spl
| ~ sQ2_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f777,f499,f502,f665,f639]) ).
fof(f782,plain,
( ~ sQ6_spl
| sQ17_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f582,f778]) ).
fof(f790,plain,
( ~ sQ6_spl
| sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f782]) ).
fof(f795,plain,
( sQ16_spl
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_inverse_image(sK13_skl,sK14_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl) ),
inference(resolution,[status(thm)],[f638,f157]) ).
fof(f797,plain,
! [X0] :
( sQ16_spl
| ~ in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),set_intersection2(sK14_skl,X0)) ),
inference(resolution,[status(thm)],[f638,f159]) ).
fof(f799,plain,
( sQ16_spl
| ~ sQ20_spl
| ~ sQ2_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f795,f499,f502,f662,f636]) ).
fof(f800,plain,
( ~ sQ6_spl
| sQ16_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f582,f797]) ).
fof(f808,plain,
( ~ sQ6_spl
| sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f800]) ).
fof(f845,plain,
( sQ10_spl
| ~ in(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl)
| ~ in(sK14_skl,apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl))) ),
inference(resolution,[status(thm)],[f614,f224]) ).
fof(f846,plain,
( sQ10_spl
| ~ in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),set_intersection2(sK14_skl,sK15_skl))
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_dom(sK13_skl))
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)))
| ~ function(sK13_skl)
| ~ relation(sK13_skl) ),
inference(resolution,[status(thm)],[f614,f58]) ).
fof(f849,definition,
( sQ36_spl
<=> in(sK14_skl,apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl))) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f852,definition,
( sQ37_spl
<=> in(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f855,plain,
( sQ10_spl
| ~ sQ37_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ36_spl ),
inference(split_clause,[status(thm)],[f845,f849,f499,f502,f852,f612]) ).
fof(f856,definition,
( sQ38_spl
<=> in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f859,definition,
( sQ39_spl
<=> in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_dom(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f860,plain,
( ~ sQ39_spl
| in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_dom(sK13_skl)) ),
inference(component_clause,[status(thm)],[f859]) ).
fof(f861,plain,
( sQ39_spl
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_dom(sK13_skl)) ),
inference(component_clause,[status(thm)],[f859]) ).
fof(f862,definition,
( sQ40_spl
<=> in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),set_intersection2(sK14_skl,sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f865,plain,
( sQ10_spl
| ~ sQ40_spl
| ~ sQ39_spl
| ~ sQ38_spl
| ~ sQ2_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f846,f499,f502,f856,f859,f862,f612]) ).
fof(f880,plain,
( sQ39_spl
| ~ in(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl))
| set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl) ),
inference(resolution,[status(thm)],[f861,f178]) ).
fof(f891,plain,
( sQ39_spl
| ~ sQ37_spl
| sQ10_spl
| ~ sQ2_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f880,f499,f502,f612,f852,f859]) ).
fof(f905,plain,
( sQ20_spl
| ~ in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),sK14_skl)
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_dom(sK13_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl) ),
inference(resolution,[status(thm)],[f664,f158]) ).
fof(f907,plain,
! [X0] :
( sQ20_spl
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),X0)) ),
inference(resolution,[status(thm)],[f664,f159]) ).
fof(f909,plain,
( sQ20_spl
| ~ sQ16_spl
| ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f905,f499,f502,f578,f636,f662]) ).
fof(f919,plain,
( sQ5_spl
| set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl)
| ~ in(relation_inverse_image(sK13_skl,sK14_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
inference(resolution,[status(thm)],[f580,f418]) ).
fof(f920,plain,
( sQ5_spl
| set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl)
| ~ in(relation_inverse_image(sK13_skl,sK15_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
inference(resolution,[status(thm)],[f580,f377]) ).
fof(f921,plain,
( sQ5_spl
| set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl)
| ~ in(relation_inverse_image(sK13_skl,sK15_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
inference(resolution,[status(thm)],[f580,f266]) ).
fof(f922,plain,
( sQ5_spl
| set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl)
| ~ in(relation_inverse_image(sK13_skl,sK14_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
inference(resolution,[status(thm)],[f580,f230]) ).
fof(f923,plain,
( sQ5_spl
| ~ in(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl))
| set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)) = relation_inverse_image(sK13_skl,set_intersection2(sK14_skl,sK15_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl) ),
inference(resolution,[status(thm)],[f580,f178]) ).
fof(f924,plain,
! [X0] :
( sQ5_spl
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_inverse_image(sK13_skl,X0))
| ~ function(sK13_skl)
| ~ relation(sK13_skl) ),
inference(resolution,[status(thm)],[f580,f156]) ).
fof(f928,plain,
( sQ5_spl
| sQ10_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f919,f609,f499,f502,f612,f578]) ).
fof(f929,plain,
( sQ5_spl
| sQ12_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f920,f616,f499,f502,f619,f578]) ).
fof(f930,plain,
( sQ5_spl
| sQ10_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f921,f623,f499,f502,f612,f578]) ).
fof(f931,plain,
( sQ5_spl
| sQ12_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f922,f627,f499,f502,f619,f578]) ).
fof(f932,plain,
( sQ5_spl
| ~ sQ3_spl
| sQ12_spl
| ~ sQ2_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f923,f499,f502,f619,f505,f578]) ).
fof(f933,definition,
! [X0] :
( sQ48_spl
<=> ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_inverse_image(sK13_skl,X0)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f934,plain,
! [X0] :
( ~ sQ48_spl
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_inverse_image(sK13_skl,X0)) ),
inference(component_clause,[status(thm)],[f933]) ).
fof(f936,plain,
( sQ5_spl
| sQ48_spl
| ~ sQ2_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f924,f499,f502,f933,f578]) ).
fof(f984,plain,
! [X0,X1] :
( ~ sQ48_spl
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),set_intersection2(X0,relation_inverse_image(sK13_skl,X1))) ),
inference(resolution,[status(thm)],[f934,f160]) ).
fof(f987,definition,
! [X0] :
( sQ52_spl
<=> ~ in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),X0) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f988,plain,
! [X0] :
( ~ sQ52_spl
| ~ in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),X0) ),
inference(component_clause,[status(thm)],[f987]) ).
fof(f991,plain,
( ~ sQ4_spl
| ~ sQ48_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f576,f984]) ).
fof(f992,plain,
( ~ sQ4_spl
| ~ sQ48_spl ),
inference(contradiction_clause,[status(thm)],[f991]) ).
fof(f993,plain,
( ~ sQ16_spl
| ~ sQ52_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f637,f988]) ).
fof(f996,plain,
( ~ sQ16_spl
| ~ sQ52_spl ),
inference(contradiction_clause,[status(thm)],[f993]) ).
fof(f1067,plain,
( ~ sQ39_spl
| ~ in(relation_dom(sK13_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
inference(resolution,[status(thm)],[f860,f41]) ).
fof(f1120,plain,
( ~ sQ39_spl
| empty(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl))
| ~ element(relation_dom(sK13_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
inference(resolution,[status(thm)],[f1067,f131]) ).
fof(f1123,definition,
( sQ66_spl
<=> element(relation_dom(sK13_skl),sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1126,definition,
( sQ67_spl
<=> empty(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK15_skl),relation_inverse_image(sK13_skl,sK14_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1129,plain,
( ~ sQ39_spl
| sQ67_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f1120,f1123,f1126,f859]) ).
fof(f1184,plain,
( sQ21_spl
| ~ in(apply(sK13_skl,sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl)),sK15_skl)
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),relation_dom(sK13_skl))
| ~ function(sK13_skl)
| ~ relation(sK13_skl) ),
inference(resolution,[status(thm)],[f667,f158]) ).
fof(f1185,plain,
! [X0] :
( sQ21_spl
| ~ in(sK0_skl(set_intersection2(relation_inverse_image(sK13_skl,sK14_skl),relation_inverse_image(sK13_skl,sK15_skl)),set_intersection2(sK14_skl,sK15_skl),sK13_skl),set_intersection2(X0,relation_inverse_image(sK13_skl,sK15_skl))) ),
inference(resolution,[status(thm)],[f667,f160]) ).
fof(f1188,plain,
( sQ21_spl
| ~ sQ17_spl
| ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f1184,f499,f502,f578,f639,f665]) ).
fof(f1193,plain,
( ~ sQ4_spl
| sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f576,f1185]) ).
fof(f1194,plain,
( ~ sQ4_spl
| sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f1193]) ).
fof(f1195,plain,
( ~ sQ4_spl
| sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f576,f907]) ).
fof(f1196,plain,
( ~ sQ4_spl
| sQ20_spl ),
inference(contradiction_clause,[status(thm)],[f1195]) ).
fof(f1197,plain,
$false,
inference(sat_refutation,[status(thm)],[f584,f586,f588,f615,f622,f626,f630,f631,f642,f651,f660,f661,f668,f724,f781,f790,f799,f808,f855,f865,f891,f909,f928,f929,f930,f931,f932,f936,f992,f996,f1129,f1188,f1194,f1196]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU058+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n019.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.36 % DateTime : Mon Sep 21 05:48:34 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.64 % Refutation found
% 0.13/0.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.72/0.67 % Elapsed time: 0.298360 seconds
% 0.72/0.67 % CPU time: 1.949877 seconds
% 0.72/0.67 % Total memory used: 124.045 MB
% 0.72/0.67 % Net memory used: 121.057 MB
%------------------------------------------------------------------------------