%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET888+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:10:54 PM UTC 2026
% Result : Theorem 35.84s 4.96s
% Output : CNFRefutation 35.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 105
% Syntax : Number of formulae : 477 ( 58 unt; 98 def)
% Number of atoms : 1181 ( 145 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 1352 ( 648 ~; 563 |; 32 &)
% ( 105 <=>; 3 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 101 ( 99 usr; 99 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-3 aty)
% Number of variables : 320 ( 314 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] : symmetric_difference(A,B) = symmetric_difference(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,B,C] :
( C = unordered_pair(A,B)
<=> ! [D] :
( in(D,C)
<=> ( D = B
| D = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A,B,C] :
( in(A,symmetric_difference(B,C))
<=> ~ ( in(A,B)
<=> in(A,C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,conjecture,
! [A,B] :
( A != B
=> symmetric_difference(singleton(A),singleton(B)) = unordered_pair(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
~ ! [A,B] :
( A != B
=> symmetric_difference(singleton(A),singleton(B)) = unordered_pair(A,B) ),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f16,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f17,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f18,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f20,plain,
! [X0,X1] : symmetric_difference(X0,X1) = symmetric_difference(X1,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f21,plain,
! [A,B] :
( ( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ( ! [C] :
( ( C != A
| in(C,B) )
& ( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(NNF_transformation,[status(thm)],[f5]) ).
fof(f22,plain,
( ! [A,B] :
( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f23,plain,
( ! [A,B] :
( ( ( sK0_skl(B,A) = A
| in(sK0_skl(B,A),B) )
& ( sK0_skl(B,A) != A
| ~ in(sK0_skl(B,A),B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f22]) ).
fof(f24,plain,
! [X0,X1,X2] :
( X2 = X1
| ~ in(X2,X0)
| X0 != singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f25,plain,
! [X0,X1,X2] :
( X2 != X1
| in(X2,X0)
| X0 != singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f28,plain,
! [A,B,C] :
( ( ? [D] :
( ( D = B
| D = A
| in(D,C) )
& ( ( D != B
& D != A )
| ~ in(D,C) ) )
| C = unordered_pair(A,B) )
& ( ! [D] :
( ( ( D != B
& D != A )
| in(D,C) )
& ( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f29,plain,
( ! [A,B,C] :
( ? [D] :
( ( D = B
| D = A
| in(D,C) )
& ( ( D != B
& D != A )
| ~ in(D,C) ) )
| C = unordered_pair(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ( D != B
& D != A )
| in(D,C) )
& ! [D] :
( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(miniscoping,[status(thm)],[f28]) ).
fof(f30,plain,
( ! [A,B,C] :
( ( ( sK1_skl(C,B,A) = B
| sK1_skl(C,B,A) = A
| in(sK1_skl(C,B,A),C) )
& ( ( sK1_skl(C,B,A) != B
& sK1_skl(C,B,A) != A )
| ~ in(sK1_skl(C,B,A),C) ) )
| C = unordered_pair(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ( D != B
& D != A )
| in(D,C) )
& ! [D] :
( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(D,sK1_skl(C,B,A))],[f29]) ).
fof(f31,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| X3 = X1
| ~ in(X3,X0)
| X0 != unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f32,plain,
! [X0,X1,X2,X3] :
( X3 != X1
| in(X3,X0)
| X0 != unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f33,plain,
! [X0,X1,X2,X3] :
( X3 != X2
| in(X3,X0)
| X0 != unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f34,plain,
! [X0,X1,X2] :
( sK1_skl(X0,X2,X1) != X1
| ~ in(sK1_skl(X0,X2,X1),X0)
| X0 = unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f35,plain,
! [X0,X1,X2] :
( sK1_skl(X0,X2,X1) != X2
| ~ in(sK1_skl(X0,X2,X1),X0)
| X0 = unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f36,plain,
! [X0,X1,X2] :
( sK1_skl(X0,X2,X1) = X2
| sK1_skl(X0,X2,X1) = X1
| in(sK1_skl(X0,X2,X1),X0)
| X0 = unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f50,plain,
! [A,B,C] :
( in(A,symmetric_difference(B,C))
<=> ( in(A,B)
<~> in(A,C) ) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f51,plain,
! [A,B,C] :
( ( ( ( ~ in(A,C)
| in(A,B) )
& ( in(A,C)
| ~ in(A,B) ) )
| in(A,symmetric_difference(B,C)) )
& ( ( ( ~ in(A,C)
| ~ in(A,B) )
& ( in(A,C)
| in(A,B) ) )
| ~ in(A,symmetric_difference(B,C)) ) ),
inference(NNF_transformation,[status(thm)],[f50]) ).
fof(f52,plain,
( ! [A,B,C] :
( ( ( ~ in(A,C)
| in(A,B) )
& ( in(A,C)
| ~ in(A,B) ) )
| in(A,symmetric_difference(B,C)) )
& ! [A,B,C] :
( ( ( ~ in(A,C)
| ~ in(A,B) )
& ( in(A,C)
| in(A,B) ) )
| ~ in(A,symmetric_difference(B,C)) ) ),
inference(miniscoping,[status(thm)],[f51]) ).
fof(f53,plain,
! [X0,X1,X2] :
( in(X0,X2)
| in(X0,X1)
| ~ in(X0,symmetric_difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f54,plain,
! [X0,X1,X2] :
( ~ in(X0,X2)
| ~ in(X0,X1)
| ~ in(X0,symmetric_difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f55,plain,
! [X0,X1,X2] :
( in(X0,X2)
| ~ in(X0,X1)
| in(X0,symmetric_difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f56,plain,
! [X0,X1,X2] :
( ~ in(X0,X2)
| in(X0,X1)
| in(X0,symmetric_difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f57,plain,
? [A,B] :
( symmetric_difference(singleton(A),singleton(B)) != unordered_pair(A,B)
& A != B ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f58,plain,
( symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)) != unordered_pair(sK4_skl,sK5_skl)
& sK4_skl != sK5_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl]),skolemize(A,sK4_skl),skolemize(B,sK5_skl)],[f57]) ).
fof(f59,plain,
sK4_skl != sK5_skl,
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)) != unordered_pair(sK4_skl,sK5_skl),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f61,plain,
! [X0,X1] :
( X0 = X1
| ~ in(X0,singleton(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f24]) ).
fof(f62,plain,
! [X0] : in(X0,singleton(X0)),
inference(destructive_equality_resolution,[status(thm)],[f25]) ).
fof(f63,plain,
! [X0,X1,X2] :
( X0 = X2
| X0 = X1
| ~ in(X0,unordered_pair(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f31]) ).
fof(f64,plain,
! [X0,X1] : in(X0,unordered_pair(X0,X1)),
inference(destructive_equality_resolution,[status(thm)],[f32]) ).
fof(f65,plain,
! [X0,X1] : in(X0,unordered_pair(X1,X0)),
inference(destructive_equality_resolution,[status(thm)],[f33]) ).
fof(f76,plain,
! [X0,X1] : ~ in(unordered_pair(X0,X1),X0),
inference(resolution,[status(thm)],[f17,f64]) ).
fof(f84,plain,
~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl))),
inference(resolution,[status(thm)],[f61,f60]) ).
fof(f85,plain,
~ in(sK4_skl,singleton(sK5_skl)),
inference(resolution,[status(thm)],[f61,f59]) ).
fof(f86,plain,
~ in(unordered_pair(sK4_skl,sK5_skl),singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))),
inference(resolution,[status(thm)],[f61,f60]) ).
fof(f87,plain,
~ in(sK5_skl,singleton(sK4_skl)),
inference(resolution,[status(thm)],[f61,f59]) ).
fof(f88,plain,
! [X0] :
( symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)) = X0
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),unordered_pair(unordered_pair(sK4_skl,sK5_skl),X0)) ),
inference(resolution,[status(thm)],[f63,f60]) ).
fof(f89,plain,
! [X0] :
( sK4_skl = X0
| ~ in(sK4_skl,unordered_pair(sK5_skl,X0)) ),
inference(resolution,[status(thm)],[f63,f59]) ).
fof(f90,plain,
! [X0] :
( unordered_pair(sK4_skl,sK5_skl) = X0
| ~ in(unordered_pair(sK4_skl,sK5_skl),unordered_pair(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0)) ),
inference(resolution,[status(thm)],[f63,f60]) ).
fof(f91,plain,
! [X0] :
( sK5_skl = X0
| ~ in(sK5_skl,unordered_pair(sK4_skl,X0)) ),
inference(resolution,[status(thm)],[f63,f59]) ).
fof(f97,plain,
! [X0,X1] :
( in(X0,X1)
| ~ in(X0,symmetric_difference(X0,X1)) ),
inference(resolution,[status(thm)],[f53,f17]) ).
fof(f98,plain,
! [X0,X1,X2] :
( ~ in(X1,X0)
| in(X0,X2)
| ~ in(X0,symmetric_difference(X1,X2)) ),
inference(resolution,[status(thm)],[f53,f17]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ~ in(symmetric_difference(X1,X2),X0)
| in(X0,X2)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f55,f17]) ).
fof(f108,plain,
! [X0,X1,X2] :
( ~ in(symmetric_difference(X1,X2),X0)
| ~ in(X0,X2)
| in(X0,X1) ),
inference(resolution,[status(thm)],[f56,f17]) ).
fof(f115,plain,
! [X0,X1,X2] :
( ~ in(X0,sK1_skl(X0,X2,X1))
| sK1_skl(X0,X2,X1) = X2
| sK1_skl(X0,X2,X1) = X1
| X0 = unordered_pair(X1,X2) ),
inference(resolution,[status(thm)],[f36,f17]) ).
fof(f119,plain,
! [X0] :
( in(sK4_skl,X0)
| ~ in(sK4_skl,symmetric_difference(singleton(sK5_skl),X0)) ),
inference(resolution,[status(thm)],[f85,f53]) ).
fof(f120,plain,
! [X0] :
( in(sK5_skl,X0)
| ~ in(sK5_skl,symmetric_difference(singleton(sK4_skl),X0)) ),
inference(resolution,[status(thm)],[f87,f53]) ).
fof(f121,plain,
~ in(sK4_skl,unordered_pair(sK5_skl,sK5_skl)),
inference(resolution,[status(thm)],[f89,f59]) ).
fof(f122,plain,
! [X0] :
( in(sK4_skl,X0)
| ~ in(sK4_skl,symmetric_difference(unordered_pair(sK5_skl,sK5_skl),X0)) ),
inference(resolution,[status(thm)],[f121,f53]) ).
fof(f123,plain,
~ in(sK5_skl,unordered_pair(sK4_skl,sK4_skl)),
inference(resolution,[status(thm)],[f91,f59]) ).
fof(f124,plain,
! [X0] :
( in(sK5_skl,X0)
| ~ in(sK5_skl,symmetric_difference(unordered_pair(sK4_skl,sK4_skl),X0)) ),
inference(resolution,[status(thm)],[f123,f53]) ).
fof(f126,plain,
~ in(sK4_skl,symmetric_difference(singleton(sK5_skl),singleton(sK5_skl))),
inference(resolution,[status(thm)],[f119,f85]) ).
fof(f127,plain,
~ in(sK4_skl,symmetric_difference(singleton(sK5_skl),sK4_skl)),
inference(resolution,[status(thm)],[f119,f17]) ).
fof(f131,plain,
! [X0] :
( in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),X0)) ),
inference(resolution,[status(thm)],[f84,f53]) ).
fof(f132,plain,
! [X0] :
( in(unordered_pair(sK4_skl,sK5_skl),X0)
| ~ in(unordered_pair(sK4_skl,sK5_skl),symmetric_difference(singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))),X0)) ),
inference(resolution,[status(thm)],[f86,f53]) ).
fof(f133,plain,
~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl))),
inference(resolution,[status(thm)],[f88,f60]) ).
fof(f134,plain,
~ in(unordered_pair(sK4_skl,sK5_skl),unordered_pair(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))),
inference(resolution,[status(thm)],[f90,f60]) ).
fof(f137,plain,
~ in(sK5_skl,symmetric_difference(singleton(sK4_skl),sK5_skl)),
inference(resolution,[status(thm)],[f120,f17]) ).
fof(f141,plain,
~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl)))),
inference(resolution,[status(thm)],[f131,f84]) ).
fof(f142,plain,
~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))),
inference(resolution,[status(thm)],[f131,f17]) ).
fof(f143,plain,
! [X0] :
( ~ in(X0,symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),X0)) ),
inference(resolution,[status(thm)],[f131,f17]) ).
fof(f147,plain,
~ in(unordered_pair(sK4_skl,sK5_skl),symmetric_difference(singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))),unordered_pair(sK4_skl,sK5_skl))),
inference(resolution,[status(thm)],[f132,f17]) ).
fof(f148,plain,
! [X0] :
( ~ in(X0,unordered_pair(sK4_skl,sK5_skl))
| ~ in(unordered_pair(sK4_skl,sK5_skl),symmetric_difference(singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))),X0)) ),
inference(resolution,[status(thm)],[f132,f17]) ).
fof(f151,plain,
~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)))),
inference(resolution,[status(thm)],[f133,f131]) ).
fof(f152,plain,
! [X0] :
( in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)),X0)) ),
inference(resolution,[status(thm)],[f133,f53]) ).
fof(f154,plain,
( ~ in(sK4_skl,sK4_skl)
| in(sK4_skl,singleton(sK5_skl)) ),
inference(resolution,[status(thm)],[f127,f56]) ).
fof(f157,plain,
~ in(sK4_skl,symmetric_difference(sK4_skl,singleton(sK5_skl))),
inference(paramodulation,[status(thm)],[f20,f127]) ).
fof(f159,definition,
( sQ0_spl
<=> in(sK4_skl,singleton(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f160,plain,
( ~ sQ0_spl
| in(sK4_skl,singleton(sK5_skl)) ),
inference(component_clause,[status(thm)],[f159]) ).
fof(f162,definition,
( sQ1_spl
<=> in(sK4_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f164,plain,
( sQ1_spl
| ~ in(sK4_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f162]) ).
fof(f165,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f154,f159,f162]) ).
fof(f170,plain,
( ~ in(sK5_skl,sK5_skl)
| in(sK5_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f137,f56]) ).
fof(f173,plain,
~ in(sK5_skl,symmetric_difference(sK5_skl,singleton(sK4_skl))),
inference(paramodulation,[status(thm)],[f20,f137]) ).
fof(f175,definition,
( sQ2_spl
<=> in(sK5_skl,singleton(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f176,plain,
( ~ sQ2_spl
| in(sK5_skl,singleton(sK4_skl)) ),
inference(component_clause,[status(thm)],[f175]) ).
fof(f178,definition,
( sQ3_spl
<=> in(sK5_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f180,plain,
( sQ3_spl
| ~ in(sK5_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f178]) ).
fof(f181,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f170,f175,f178]) ).
fof(f183,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f160,f85]) ).
fof(f184,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f183]) ).
fof(f185,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f176,f87]) ).
fof(f186,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f185]) ).
fof(f219,definition,
( sQ4_spl
<=> in(sK4_skl,unordered_pair(sK5_skl,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f230,definition,
! [X0] :
( sQ5_spl
<=> ( ~ in(sK4_skl,X0)
| ~ in(X0,sK4_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f242,definition,
( sQ7_spl
<=> in(sK5_skl,unordered_pair(sK4_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f247,plain,
~ in(unordered_pair(sK4_skl,sK5_skl),symmetric_difference(singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))),unordered_pair(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))))),
inference(resolution,[status(thm)],[f134,f132]) ).
fof(f249,plain,
( sQ1_spl
| ~ in(sK4_skl,symmetric_difference(unordered_pair(sK5_skl,sK5_skl),sK4_skl)) ),
inference(resolution,[status(thm)],[f122,f164]) ).
fof(f258,plain,
! [X0] :
( ~ in(X0,sK4_skl)
| ~ in(sK4_skl,symmetric_difference(unordered_pair(sK5_skl,sK5_skl),X0)) ),
inference(resolution,[status(thm)],[f122,f17]) ).
fof(f261,plain,
( sQ3_spl
| ~ in(sK5_skl,symmetric_difference(unordered_pair(sK4_skl,sK4_skl),sK5_skl)) ),
inference(resolution,[status(thm)],[f124,f180]) ).
fof(f267,plain,
~ in(sK5_skl,symmetric_difference(unordered_pair(sK4_skl,sK4_skl),singleton(sK4_skl))),
inference(resolution,[status(thm)],[f124,f87]) ).
fof(f279,definition,
! [X0] :
( sQ8_spl
<=> ( ~ in(sK5_skl,X0)
| ~ in(X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f291,definition,
( sQ10_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f292,plain,
( ~ sQ10_spl
| in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl))) ),
inference(component_clause,[status(thm)],[f291]) ).
fof(f297,plain,
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))
| in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl))) ),
inference(resolution,[status(thm)],[f142,f56]) ).
fof(f300,definition,
( sQ11_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f303,plain,
( ~ sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f297,f291,f300]) ).
fof(f306,plain,
! [X0] :
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0)
| in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl)))
| ~ in(X0,symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))) ),
inference(resolution,[status(thm)],[f143,f56]) ).
fof(f311,definition,
! [X0] :
( sQ12_spl
<=> ( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0)
| ~ in(X0,symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f314,plain,
( sQ10_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f306,f311,f291]) ).
fof(f320,plain,
( ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f292,f84]) ).
fof(f321,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f320]) ).
fof(f326,definition,
( sQ14_spl
<=> in(unordered_pair(sK4_skl,sK5_skl),singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f327,plain,
( ~ sQ14_spl
| in(unordered_pair(sK4_skl,sK5_skl),singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))) ),
inference(component_clause,[status(thm)],[f326]) ).
fof(f332,plain,
( ~ in(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl))
| in(unordered_pair(sK4_skl,sK5_skl),singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))) ),
inference(resolution,[status(thm)],[f147,f56]) ).
fof(f337,definition,
( sQ15_spl
<=> in(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f340,plain,
( ~ sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f332,f326,f337]) ).
fof(f343,plain,
! [X0] :
( ~ in(unordered_pair(sK4_skl,sK5_skl),X0)
| in(unordered_pair(sK4_skl,sK5_skl),singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))))
| ~ in(X0,unordered_pair(sK4_skl,sK5_skl)) ),
inference(resolution,[status(thm)],[f148,f56]) ).
fof(f348,definition,
! [X0] :
( sQ16_spl
<=> ( ~ in(unordered_pair(sK4_skl,sK5_skl),X0)
| ~ in(X0,unordered_pair(sK4_skl,sK5_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f351,plain,
( sQ14_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f343,f348,f326]) ).
fof(f352,definition,
! [X0] :
( sQ17_spl
<=> ( in(unordered_pair(sK4_skl,sK5_skl),X0)
| ~ in(X0,unordered_pair(sK4_skl,sK5_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f353,plain,
! [X0] :
( ~ sQ17_spl
| in(unordered_pair(sK4_skl,sK5_skl),X0)
| ~ in(X0,unordered_pair(sK4_skl,sK5_skl)) ),
inference(component_clause,[status(thm)],[f352]) ).
fof(f356,plain,
! [X0] :
( ~ sQ17_spl
| ~ in(X0,unordered_pair(sK4_skl,sK5_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f353,f17]) ).
fof(f357,plain,
( ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f327,f86]) ).
fof(f358,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f357]) ).
fof(f360,plain,
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)))
| in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl))) ),
inference(resolution,[status(thm)],[f151,f56]) ).
fof(f363,definition,
( sQ18_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f366,plain,
( ~ sQ18_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f360,f291,f363]) ).
fof(f380,plain,
( sQ1_spl
| in(sK4_skl,sK4_skl)
| ~ in(sK4_skl,unordered_pair(sK5_skl,sK5_skl)) ),
inference(resolution,[status(thm)],[f249,f55]) ).
fof(f382,plain,
( sQ1_spl
| ~ in(sK4_skl,symmetric_difference(sK4_skl,unordered_pair(sK5_skl,sK5_skl))) ),
inference(paramodulation,[status(thm)],[f20,f249]) ).
fof(f385,plain,
( sQ1_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f380,f219,f162]) ).
fof(f387,plain,
( ~ in(unordered_pair(sK4_skl,sK5_skl),unordered_pair(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))))
| in(unordered_pair(sK4_skl,sK5_skl),singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))) ),
inference(resolution,[status(thm)],[f247,f56]) ).
fof(f390,definition,
( sQ19_spl
<=> in(unordered_pair(sK4_skl,sK5_skl),unordered_pair(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f393,plain,
( ~ sQ19_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f387,f326,f390]) ).
fof(f398,plain,
! [X0,X1] : ~ in(unordered_pair(X0,X1),X1),
inference(resolution,[status(thm)],[f65,f17]) ).
fof(f404,plain,
! [X0,X1] :
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(X0,X1)))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0) ),
inference(resolution,[status(thm)],[f54,f131]) ).
fof(f409,plain,
! [X0,X1,X2,X3] :
( sK1_skl(symmetric_difference(X0,X1),X2,X3) = X2
| sK1_skl(symmetric_difference(X0,X1),X2,X3) = X3
| symmetric_difference(X0,X1) = unordered_pair(X3,X2)
| ~ in(sK1_skl(symmetric_difference(X0,X1),X2,X3),X1)
| ~ in(sK1_skl(symmetric_difference(X0,X1),X2,X3),X0) ),
inference(resolution,[status(thm)],[f54,f36]) ).
fof(f413,plain,
! [X0,X1,X2,X3] :
( in(X0,X3)
| ~ in(X0,symmetric_difference(symmetric_difference(X1,X2),X3))
| ~ in(X0,X2)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f54,f53]) ).
fof(f416,plain,
~ in(unordered_pair(sK4_skl,sK5_skl),symmetric_difference(singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))),sK4_skl)),
inference(resolution,[status(thm)],[f76,f132]) ).
fof(f422,plain,
~ in(unordered_pair(sK4_skl,sK5_skl),symmetric_difference(singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))),sK5_skl)),
inference(resolution,[status(thm)],[f398,f132]) ).
fof(f433,plain,
( sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl) != sK4_skl
| ~ in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))) ),
inference(resolution,[status(thm)],[f34,f60]) ).
fof(f434,plain,
! [X0,X1,X2] :
( sK1_skl(X0,X1,X2) != X2
| ~ in(sK1_skl(X0,X1,X2),X0)
| X0 = unordered_pair(X1,X2) ),
inference(paramodulation,[status(thm)],[f18,f34]) ).
fof(f436,definition,
( sQ20_spl
<=> in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f438,plain,
( sQ20_spl
| ~ in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))) ),
inference(component_clause,[status(thm)],[f436]) ).
fof(f439,definition,
( sQ21_spl
<=> sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl) = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f440,plain,
( ~ sQ21_spl
| sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl) = sK4_skl ),
inference(component_clause,[status(thm)],[f439]) ).
fof(f441,plain,
( sQ21_spl
| sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl) != sK4_skl ),
inference(component_clause,[status(thm)],[f439]) ).
fof(f442,plain,
( ~ sQ21_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f433,f436,f439]) ).
fof(f443,plain,
( sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl) != sK5_skl
| ~ in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))) ),
inference(resolution,[status(thm)],[f35,f60]) ).
fof(f444,plain,
! [X0,X1,X2] :
( sK1_skl(X0,X1,X2) != X1
| ~ in(sK1_skl(X0,X1,X2),X0)
| X0 = unordered_pair(X1,X2) ),
inference(paramodulation,[status(thm)],[f18,f35]) ).
fof(f446,definition,
( sQ22_spl
<=> sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl) = sK5_skl ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f447,plain,
( ~ sQ22_spl
| sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl) = sK5_skl ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f448,plain,
( sQ22_spl
| sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl) != sK5_skl ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f449,plain,
( ~ sQ22_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f443,f436,f446]) ).
fof(f467,plain,
( sQ20_spl
| sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl) = sK5_skl
| sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl) = sK4_skl
| symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)) = unordered_pair(sK4_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f438,f36]) ).
fof(f468,plain,
( sQ20_spl
| ~ in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),singleton(sK5_skl))
| in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f438,f56]) ).
fof(f469,plain,
( sQ20_spl
| in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),singleton(sK5_skl))
| ~ in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f438,f55]) ).
fof(f471,definition,
( sQ23_spl
<=> symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)) = unordered_pair(sK4_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f472,plain,
( ~ sQ23_spl
| symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)) = unordered_pair(sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f471]) ).
fof(f474,plain,
( sQ20_spl
| sQ22_spl
| sQ21_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f467,f471,f439,f446,f436]) ).
fof(f475,definition,
( sQ24_spl
<=> in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),singleton(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f476,plain,
( ~ sQ24_spl
| in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),singleton(sK4_skl)) ),
inference(component_clause,[status(thm)],[f475]) ).
fof(f477,plain,
( sQ24_spl
| ~ in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),singleton(sK4_skl)) ),
inference(component_clause,[status(thm)],[f475]) ).
fof(f478,definition,
( sQ25_spl
<=> in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),singleton(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f479,plain,
( ~ sQ25_spl
| in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),singleton(sK5_skl)) ),
inference(component_clause,[status(thm)],[f478]) ).
fof(f480,plain,
( sQ25_spl
| ~ in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),singleton(sK5_skl)) ),
inference(component_clause,[status(thm)],[f478]) ).
fof(f481,plain,
( sQ20_spl
| ~ sQ25_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f468,f475,f478,f436]) ).
fof(f482,plain,
( sQ20_spl
| sQ25_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f469,f475,f478,f436]) ).
fof(f483,plain,
( ~ sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f472,f60]) ).
fof(f484,plain,
~ sQ23_spl,
inference(contradiction_clause,[status(thm)],[f483]) ).
fof(f486,plain,
( ~ sQ25_spl
| ~ sQ21_spl
| in(sK4_skl,singleton(sK5_skl)) ),
inference(backward_demodulation,[status(thm)],[f440,f479]) ).
fof(f489,plain,
( ~ sQ25_spl
| ~ sQ21_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f486,f159,f439,f478]) ).
fof(f494,plain,
( sQ3_spl
| in(sK5_skl,sK5_skl)
| ~ in(sK5_skl,unordered_pair(sK4_skl,sK4_skl)) ),
inference(resolution,[status(thm)],[f261,f55]) ).
fof(f499,plain,
( sQ3_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f494,f242,f178]) ).
fof(f560,definition,
( sQ26_spl
<=> in(sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl),singleton(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f563,definition,
( sQ27_spl
<=> in(sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl),singleton(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f566,definition,
( sQ28_spl
<=> symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)) = unordered_pair(sK4_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f567,plain,
( ~ sQ28_spl
| symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)) = unordered_pair(sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f566]) ).
fof(f568,plain,
( sQ28_spl
| symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)) != unordered_pair(sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f566]) ).
fof(f569,definition,
( sQ29_spl
<=> sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl) = sK5_skl ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f585,plain,
( sQ25_spl
| ~ sQ22_spl
| ~ in(sK5_skl,singleton(sK5_skl)) ),
inference(forward_demodulation,[status(thm)],[f447,f480]) ).
fof(f586,plain,
( sQ25_spl
| ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f585,f62]) ).
fof(f587,plain,
( sQ25_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f586]) ).
fof(f593,plain,
( ~ sQ24_spl
| ~ sQ22_spl
| in(sK5_skl,singleton(sK4_skl)) ),
inference(forward_demodulation,[status(thm)],[f447,f476]) ).
fof(f594,plain,
( ~ sQ24_spl
| ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f593,f87]) ).
fof(f595,plain,
( ~ sQ24_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f594]) ).
fof(f604,plain,
( sQ21_spl
| ~ in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f441,f61]) ).
fof(f612,plain,
( sQ22_spl
| ~ in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),singleton(sK5_skl)) ),
inference(resolution,[status(thm)],[f448,f61]) ).
fof(f632,definition,
( sQ31_spl
<=> in(sK4_skl,symmetric_difference(singleton(sK5_skl),sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f644,definition,
( sQ32_spl
<=> in(sK5_skl,symmetric_difference(singleton(sK4_skl),sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f654,definition,
( sQ33_spl
<=> in(sK4_skl,symmetric_difference(sK4_skl,singleton(sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f664,definition,
( sQ34_spl
<=> in(sK5_skl,symmetric_difference(sK5_skl,singleton(sK4_skl))) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f678,plain,
! [X0] :
( ~ in(sK4_skl,X0)
| in(sK4_skl,unordered_pair(sK5_skl,sK5_skl))
| ~ in(X0,sK4_skl) ),
inference(resolution,[status(thm)],[f258,f56]) ).
fof(f683,plain,
( sQ4_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f678,f230,f219]) ).
fof(f788,definition,
! [X0,X1] :
( sQ36_spl
<=> ( ~ in(unordered_pair(sK4_skl,sK5_skl),symmetric_difference(X0,X1))
| ~ in(unordered_pair(sK4_skl,sK5_skl),X1)
| ~ in(unordered_pair(sK4_skl,sK5_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f809,definition,
! [X0,X1] :
( sQ38_spl
<=> ( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(X0,X1))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f836,plain,
( ~ sQ17_spl
| $false ),
inference(resolution,[status(thm)],[f356,f65]) ).
fof(f839,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f836]) ).
fof(f857,plain,
~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl)))),
inference(resolution,[status(thm)],[f97,f84]) ).
fof(f863,plain,
~ in(sK5_skl,symmetric_difference(sK5_skl,symmetric_difference(sK5_skl,singleton(sK4_skl)))),
inference(resolution,[status(thm)],[f97,f173]) ).
fof(f868,plain,
~ in(sK5_skl,symmetric_difference(sK5_skl,symmetric_difference(singleton(sK4_skl),sK5_skl))),
inference(resolution,[status(thm)],[f97,f137]) ).
fof(f878,plain,
( sQ1_spl
| ~ in(sK4_skl,symmetric_difference(sK4_skl,symmetric_difference(unordered_pair(sK5_skl,sK5_skl),sK4_skl))) ),
inference(resolution,[status(thm)],[f97,f249]) ).
fof(f879,plain,
( sQ1_spl
| ~ in(sK4_skl,symmetric_difference(sK4_skl,symmetric_difference(sK4_skl,unordered_pair(sK5_skl,sK5_skl)))) ),
inference(resolution,[status(thm)],[f97,f382]) ).
fof(f880,plain,
~ in(sK4_skl,symmetric_difference(sK4_skl,symmetric_difference(sK4_skl,singleton(sK5_skl)))),
inference(resolution,[status(thm)],[f97,f157]) ).
fof(f884,plain,
~ in(sK4_skl,symmetric_difference(sK4_skl,symmetric_difference(singleton(sK5_skl),singleton(sK5_skl)))),
inference(resolution,[status(thm)],[f97,f126]) ).
fof(f885,plain,
~ in(sK4_skl,symmetric_difference(sK4_skl,symmetric_difference(singleton(sK5_skl),sK4_skl))),
inference(resolution,[status(thm)],[f97,f127]) ).
fof(f891,plain,
! [X0] : ~ in(X0,symmetric_difference(X0,X0)),
inference(resolution,[status(thm)],[f97,f17]) ).
fof(f927,plain,
! [X0] :
( ~ in(X0,sK5_skl)
| ~ in(sK5_skl,symmetric_difference(X0,unordered_pair(sK4_skl,sK4_skl))) ),
inference(resolution,[status(thm)],[f98,f123]) ).
fof(f959,plain,
~ in(sK5_skl,symmetric_difference(singleton(sK4_skl),symmetric_difference(sK5_skl,sK5_skl))),
inference(resolution,[status(thm)],[f891,f120]) ).
fof(f960,plain,
~ in(sK4_skl,symmetric_difference(unordered_pair(sK5_skl,sK5_skl),symmetric_difference(sK4_skl,sK4_skl))),
inference(resolution,[status(thm)],[f891,f122]) ).
fof(f993,plain,
! [X0] :
( ~ in(symmetric_difference(X0,singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))),unordered_pair(sK4_skl,sK5_skl))
| ~ in(unordered_pair(sK4_skl,sK5_skl),X0) ),
inference(resolution,[status(thm)],[f102,f86]) ).
fof(f1019,plain,
! [X0] :
( ~ in(symmetric_difference(X0,singleton(sK4_skl)),sK5_skl)
| ~ in(sK5_skl,X0) ),
inference(resolution,[status(thm)],[f102,f87]) ).
fof(f1034,plain,
! [X0] :
( ~ in(symmetric_difference(X0,singleton(sK5_skl)),sK4_skl)
| ~ in(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f102,f85]) ).
fof(f1112,plain,
! [X0,X1] :
( in(symmetric_difference(X0,singleton(sK4_skl)),X1)
| ~ in(symmetric_difference(X0,singleton(sK4_skl)),symmetric_difference(sK5_skl,X1))
| ~ in(sK5_skl,X0) ),
inference(resolution,[status(thm)],[f1019,f53]) ).
fof(f1113,plain,
! [X0] :
( ~ in(symmetric_difference(singleton(sK4_skl),X0),sK5_skl)
| ~ in(sK5_skl,X0) ),
inference(paramodulation,[status(thm)],[f20,f1019]) ).
fof(f1117,plain,
( ~ in(sK5_skl,symmetric_difference(sK5_skl,singleton(sK4_skl)))
| in(sK5_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f863,f56]) ).
fof(f1123,plain,
( ~ sQ34_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1117,f178,f664]) ).
fof(f1127,plain,
( ~ in(sK5_skl,symmetric_difference(singleton(sK4_skl),sK5_skl))
| in(sK5_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f868,f56]) ).
fof(f1135,plain,
( ~ sQ32_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1127,f178,f644]) ).
fof(f1139,plain,
( ~ in(sK4_skl,symmetric_difference(sK4_skl,singleton(sK5_skl)))
| in(sK4_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f880,f56]) ).
fof(f1145,plain,
( ~ sQ33_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f1139,f162,f654]) ).
fof(f1149,plain,
( ~ in(sK4_skl,symmetric_difference(singleton(sK5_skl),sK4_skl))
| in(sK4_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f885,f56]) ).
fof(f1157,plain,
( ~ sQ31_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f1149,f162,f632]) ).
fof(f1161,plain,
( ~ in(sK5_skl,symmetric_difference(sK5_skl,sK5_skl))
| in(sK5_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f959,f56]) ).
fof(f1167,definition,
( sQ40_spl
<=> in(sK5_skl,symmetric_difference(sK5_skl,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1170,plain,
( ~ sQ40_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1161,f175,f1167]) ).
fof(f1180,definition,
( sQ41_spl
<=> in(sK4_skl,symmetric_difference(sK4_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1185,plain,
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)),sK4_skl))
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f1034,f152]) ).
fof(f1186,plain,
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),sK4_skl))
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f1034,f131]) ).
fof(f1188,plain,
! [X0,X1] :
( ~ in(X1,symmetric_difference(X0,singleton(sK5_skl)))
| ~ in(symmetric_difference(X0,singleton(sK5_skl)),symmetric_difference(X1,sK4_skl))
| ~ in(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f1034,f98]) ).
fof(f1189,plain,
! [X0] :
( ~ in(symmetric_difference(X0,singleton(sK5_skl)),symmetric_difference(symmetric_difference(X0,singleton(sK5_skl)),sK4_skl))
| ~ in(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f1034,f97]) ).
fof(f1190,plain,
! [X0,X1] :
( in(symmetric_difference(X0,singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(X0,singleton(sK5_skl)),symmetric_difference(sK4_skl,X1))
| ~ in(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f1034,f53]) ).
fof(f1191,plain,
! [X0] :
( ~ in(symmetric_difference(singleton(sK5_skl),X0),sK4_skl)
| ~ in(sK4_skl,X0) ),
inference(paramodulation,[status(thm)],[f20,f1034]) ).
fof(f1193,definition,
( sQ42_spl
<=> in(sK4_skl,singleton(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1195,plain,
( sQ42_spl
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(component_clause,[status(thm)],[f1193]) ).
fof(f1196,definition,
( sQ43_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)),sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1199,plain,
( ~ sQ43_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f1185,f1193,f1196]) ).
fof(f1200,definition,
( sQ44_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1203,plain,
( ~ sQ44_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f1186,f1193,f1200]) ).
fof(f1204,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1195,f62]) ).
fof(f1205,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f1204]) ).
fof(f1206,plain,
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)),sK5_skl))
| ~ in(sK5_skl,singleton(sK5_skl)) ),
inference(resolution,[status(thm)],[f1113,f152]) ).
fof(f1207,plain,
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),sK5_skl))
| ~ in(sK5_skl,singleton(sK5_skl)) ),
inference(resolution,[status(thm)],[f1113,f131]) ).
fof(f1215,definition,
( sQ45_spl
<=> in(sK5_skl,singleton(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1217,plain,
( sQ45_spl
| ~ in(sK5_skl,singleton(sK5_skl)) ),
inference(component_clause,[status(thm)],[f1215]) ).
fof(f1218,definition,
( sQ46_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)),sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1221,plain,
( ~ sQ46_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f1206,f1215,f1218]) ).
fof(f1222,definition,
( sQ47_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1225,plain,
( ~ sQ47_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f1207,f1215,f1222]) ).
fof(f1230,plain,
( sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1217,f62]) ).
fof(f1231,plain,
sQ45_spl,
inference(contradiction_clause,[status(thm)],[f1230]) ).
fof(f1242,definition,
! [X0,X1] :
( sQ49_spl
<=> ( ~ in(sK5_skl,symmetric_difference(X0,X1))
| ~ in(sK5_skl,X1)
| ~ in(sK5_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1246,definition,
! [X0,X1] :
( sQ50_spl
<=> ( in(sK5_skl,symmetric_difference(X0,X1))
| ~ in(sK5_skl,X1)
| ~ in(sK5_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1247,plain,
! [X0,X1] :
( ~ sQ50_spl
| in(sK5_skl,symmetric_difference(X0,X1))
| ~ in(sK5_skl,X1)
| ~ in(sK5_skl,X0) ),
inference(component_clause,[status(thm)],[f1246]) ).
fof(f1250,plain,
! [X0,X1] :
( ~ sQ50_spl
| in(sK5_skl,symmetric_difference(X1,X0))
| ~ in(sK5_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1247,f56]) ).
fof(f1261,definition,
! [X0,X1] :
( sQ51_spl
<=> ( ~ in(sK4_skl,symmetric_difference(X0,X1))
| ~ in(sK4_skl,X1)
| ~ in(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1265,definition,
! [X0,X1] :
( sQ52_spl
<=> ( in(sK4_skl,symmetric_difference(X0,X1))
| ~ in(sK4_skl,X1)
| ~ in(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1266,plain,
! [X0,X1] :
( ~ sQ52_spl
| in(sK4_skl,symmetric_difference(X0,X1))
| ~ in(sK4_skl,X1)
| ~ in(sK4_skl,X0) ),
inference(component_clause,[status(thm)],[f1265]) ).
fof(f1269,plain,
! [X0,X1] :
( ~ sQ52_spl
| in(sK4_skl,symmetric_difference(X1,X0))
| ~ in(sK4_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1266,f56]) ).
fof(f1272,plain,
( ~ in(unordered_pair(sK4_skl,sK5_skl),sK4_skl)
| in(unordered_pair(sK4_skl,sK5_skl),singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))) ),
inference(resolution,[status(thm)],[f416,f56]) ).
fof(f1280,definition,
( sQ53_spl
<=> in(unordered_pair(sK4_skl,sK5_skl),sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1283,plain,
( ~ sQ53_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f1272,f326,f1280]) ).
fof(f1287,plain,
( ~ in(unordered_pair(sK4_skl,sK5_skl),sK5_skl)
| in(unordered_pair(sK4_skl,sK5_skl),singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))) ),
inference(resolution,[status(thm)],[f422,f56]) ).
fof(f1295,definition,
( sQ54_spl
<=> in(unordered_pair(sK4_skl,sK5_skl),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1298,plain,
( ~ sQ54_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f1287,f326,f1295]) ).
fof(f1308,definition,
( sQ55_spl
<=> sK5_skl = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1309,plain,
( ~ sQ55_spl
| sK5_skl = sK4_skl ),
inference(component_clause,[status(thm)],[f1308]) ).
fof(f1313,definition,
( sQ56_spl
<=> in(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1320,definition,
( sQ58_spl
<=> sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl) = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1322,plain,
( sQ58_spl
| sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl) != sK4_skl ),
inference(component_clause,[status(thm)],[f1320]) ).
fof(f1329,plain,
( sQ24_spl
| ~ sQ21_spl
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(backward_demodulation,[status(thm)],[f440,f477]) ).
fof(f1358,plain,
( sQ24_spl
| ~ sQ21_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f1329,f1193,f439,f475]) ).
fof(f1368,plain,
( ~ sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1309,f59]) ).
fof(f1369,plain,
~ sQ55_spl,
inference(contradiction_clause,[status(thm)],[f1368]) ).
fof(f1412,plain,
! [X0,X1] :
( ~ sQ52_spl
| ~ in(sK4_skl,X0)
| ~ in(sK4_skl,X1)
| ~ in(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f1269,f54]) ).
fof(f1421,definition,
! [X0] :
( sQ60_spl
<=> ( ~ in(sK4_skl,X0)
| ~ in(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1422,plain,
! [X0] :
( ~ sQ60_spl
| ~ in(sK4_skl,X0)
| ~ in(sK4_skl,X0) ),
inference(component_clause,[status(thm)],[f1421]) ).
fof(f1424,definition,
! [X1] :
( sQ61_spl
<=> ~ in(sK4_skl,X1) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1425,plain,
! [X0] :
( ~ sQ61_spl
| ~ in(sK4_skl,X0) ),
inference(component_clause,[status(thm)],[f1424]) ).
fof(f1427,plain,
( ~ sQ52_spl
| sQ61_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1412,f1421,f1424,f1265]) ).
fof(f1428,plain,
! [X0] :
( ~ sQ60_spl
| ~ in(sK4_skl,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1422]) ).
fof(f1431,plain,
( ~ sQ61_spl
| $false ),
inference(resolution,[status(thm)],[f1425,f65]) ).
fof(f1443,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f1431]) ).
fof(f1444,plain,
( ~ sQ60_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f1428,f1424,f1421]) ).
fof(f1493,plain,
! [X0,X1] :
( ~ sQ50_spl
| ~ in(sK5_skl,X0)
| ~ in(sK5_skl,X1)
| ~ in(sK5_skl,X0) ),
inference(resolution,[status(thm)],[f1250,f54]) ).
fof(f1502,definition,
! [X0] :
( sQ64_spl
<=> ( ~ in(sK5_skl,X0)
| ~ in(sK5_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1503,plain,
! [X0] :
( ~ sQ64_spl
| ~ in(sK5_skl,X0)
| ~ in(sK5_skl,X0) ),
inference(component_clause,[status(thm)],[f1502]) ).
fof(f1505,definition,
! [X1] :
( sQ65_spl
<=> ~ in(sK5_skl,X1) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1506,plain,
! [X0] :
( ~ sQ65_spl
| ~ in(sK5_skl,X0) ),
inference(component_clause,[status(thm)],[f1505]) ).
fof(f1508,plain,
( ~ sQ50_spl
| sQ65_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1493,f1502,f1505,f1246]) ).
fof(f1509,plain,
! [X0] :
( ~ sQ64_spl
| ~ in(sK5_skl,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1503]) ).
fof(f1512,plain,
( ~ sQ65_spl
| $false ),
inference(resolution,[status(thm)],[f1506,f65]) ).
fof(f1519,definition,
! [X0] :
( sQ66_spl
<=> in(sK5_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1520,plain,
! [X0] :
( ~ sQ66_spl
| in(sK5_skl,X0) ),
inference(component_clause,[status(thm)],[f1519]) ).
fof(f1524,plain,
~ sQ65_spl,
inference(contradiction_clause,[status(thm)],[f1512]) ).
fof(f1525,plain,
( ~ sQ64_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f1509,f1505,f1502]) ).
fof(f1545,plain,
! [X0] :
( sQ21_spl
| in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),X0)
| ~ in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),symmetric_difference(singleton(sK4_skl),X0)) ),
inference(resolution,[status(thm)],[f604,f53]) ).
fof(f1663,plain,
! [X0] :
( ~ in(symmetric_difference(unordered_pair(sK5_skl,sK5_skl),X0),sK4_skl)
| ~ in(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f108,f121]) ).
fof(f1688,plain,
! [X0,X1] :
( ~ in(unordered_pair(sK4_skl,sK5_skl),X0)
| ~ in(symmetric_difference(unordered_pair(sK4_skl,sK5_skl),X1),symmetric_difference(X0,singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))))
| ~ in(symmetric_difference(X0,singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))),X1) ),
inference(resolution,[status(thm)],[f108,f993]) ).
fof(f1719,plain,
! [X0,X1] :
( ~ in(sK5_skl,symmetric_difference(symmetric_difference(X0,X1),unordered_pair(sK4_skl,sK4_skl)))
| ~ in(sK5_skl,X1)
| ~ in(sK5_skl,X0) ),
inference(resolution,[status(thm)],[f413,f123]) ).
fof(f1720,plain,
! [X0,X1] :
( ~ in(sK5_skl,symmetric_difference(symmetric_difference(X0,X1),singleton(sK4_skl)))
| ~ in(sK5_skl,X1)
| ~ in(sK5_skl,X0) ),
inference(resolution,[status(thm)],[f413,f87]) ).
fof(f1724,plain,
! [X0,X1] :
( ~ in(sK4_skl,symmetric_difference(symmetric_difference(X0,X1),unordered_pair(sK5_skl,sK5_skl)))
| ~ in(sK4_skl,X1)
| ~ in(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f413,f121]) ).
fof(f1726,plain,
! [X0,X1] :
( ~ in(sK4_skl,symmetric_difference(symmetric_difference(X0,X1),singleton(sK5_skl)))
| ~ in(sK4_skl,X1)
| ~ in(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f413,f85]) ).
fof(f1734,plain,
! [X0,X1] :
( ~ in(unordered_pair(sK4_skl,sK5_skl),symmetric_difference(symmetric_difference(X0,X1),unordered_pair(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))))
| ~ in(unordered_pair(sK4_skl,sK5_skl),X1)
| ~ in(unordered_pair(sK4_skl,sK5_skl),X0) ),
inference(resolution,[status(thm)],[f413,f134]) ).
fof(f1739,plain,
! [X0,X1] :
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(symmetric_difference(X0,X1),symmetric_difference(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl)))))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0) ),
inference(resolution,[status(thm)],[f413,f857]) ).
fof(f1744,plain,
! [X0,X1] :
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(symmetric_difference(X0,X1),unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl))))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0) ),
inference(resolution,[status(thm)],[f413,f133]) ).
fof(f1747,plain,
! [X0,X1,X2] :
( ~ in(sK4_skl,X0)
| ~ in(symmetric_difference(X0,singleton(sK5_skl)),symmetric_difference(symmetric_difference(X1,X2),sK4_skl))
| ~ in(symmetric_difference(X0,singleton(sK5_skl)),X2)
| ~ in(symmetric_difference(X0,singleton(sK5_skl)),X1) ),
inference(resolution,[status(thm)],[f413,f1034]) ).
fof(f1833,plain,
! [X0,X1] :
( ~ in(sK5_skl,symmetric_difference(singleton(sK4_skl),symmetric_difference(symmetric_difference(X0,X1),singleton(sK4_skl))))
| ~ in(sK5_skl,X1)
| ~ in(sK5_skl,X0) ),
inference(resolution,[status(thm)],[f1720,f120]) ).
fof(f1933,plain,
! [X0,X1] :
( ~ in(sK4_skl,symmetric_difference(singleton(sK5_skl),symmetric_difference(symmetric_difference(X0,X1),singleton(sK5_skl))))
| ~ in(sK4_skl,X1)
| ~ in(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f1726,f119]) ).
fof(f1957,definition,
( sQ74_spl
<=> symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)) = unordered_pair(sK5_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1958,plain,
( ~ sQ74_spl
| symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)) = unordered_pair(sK5_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f1957]) ).
fof(f2007,plain,
( ~ sQ74_spl
| unordered_pair(sK5_skl,sK4_skl) != unordered_pair(sK4_skl,sK5_skl) ),
inference(backward_demodulation,[status(thm)],[f1958,f60]) ).
fof(f2251,plain,
( ~ sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2007,f18]) ).
fof(f2252,plain,
~ sQ74_spl,
inference(contradiction_clause,[status(thm)],[f2251]) ).
fof(f2331,plain,
( ~ sQ28_spl
| symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)) = unordered_pair(sK4_skl,sK5_skl) ),
inference(paramodulation,[status(thm)],[f20,f567]) ).
fof(f2349,plain,
( ~ sQ28_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f2331,f471,f566]) ).
fof(f2788,plain,
( sQ28_spl
| sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl) != sK4_skl
| ~ in(sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl),symmetric_difference(singleton(sK5_skl),singleton(sK4_skl))) ),
inference(resolution,[status(thm)],[f568,f444]) ).
fof(f2789,plain,
( sQ28_spl
| sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl) != sK5_skl
| ~ in(sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl),symmetric_difference(singleton(sK5_skl),singleton(sK4_skl))) ),
inference(resolution,[status(thm)],[f568,f434]) ).
fof(f2790,plain,
( sQ28_spl
| sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl) != sK5_skl
| ~ in(sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl),symmetric_difference(singleton(sK5_skl),singleton(sK4_skl))) ),
inference(resolution,[status(thm)],[f568,f35]) ).
fof(f2791,plain,
( sQ28_spl
| sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl) != sK4_skl
| ~ in(sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl),symmetric_difference(singleton(sK5_skl),singleton(sK4_skl))) ),
inference(resolution,[status(thm)],[f568,f34]) ).
fof(f2801,definition,
( sQ84_spl
<=> in(sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl),symmetric_difference(singleton(sK5_skl),singleton(sK4_skl))) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f2804,definition,
( sQ85_spl
<=> sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl) = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f2807,plain,
( sQ28_spl
| ~ sQ85_spl
| ~ sQ84_spl ),
inference(split_clause,[status(thm)],[f2788,f2801,f2804,f566]) ).
fof(f2808,definition,
( sQ86_spl
<=> sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl) = sK5_skl ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f2810,plain,
( sQ86_spl
| sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl) != sK5_skl ),
inference(component_clause,[status(thm)],[f2808]) ).
fof(f2811,plain,
( sQ28_spl
| ~ sQ86_spl
| ~ sQ84_spl ),
inference(split_clause,[status(thm)],[f2789,f2801,f2808,f566]) ).
fof(f2812,definition,
( sQ87_spl
<=> in(sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl),symmetric_difference(singleton(sK5_skl),singleton(sK4_skl))) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f2815,plain,
( sQ28_spl
| ~ sQ29_spl
| ~ sQ87_spl ),
inference(split_clause,[status(thm)],[f2790,f2812,f569,f566]) ).
fof(f2816,plain,
( sQ28_spl
| ~ sQ58_spl
| ~ sQ87_spl ),
inference(split_clause,[status(thm)],[f2791,f2812,f1320,f566]) ).
fof(f2917,definition,
( sQ88_spl
<=> in(sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl),singleton(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f2920,definition,
( sQ89_spl
<=> in(sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl),singleton(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f2923,definition,
( sQ90_spl
<=> symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)) = unordered_pair(sK5_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f2924,plain,
( ~ sQ90_spl
| symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)) = unordered_pair(sK5_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f2923]) ).
fof(f2932,plain,
( sQ28_spl
| ~ sQ90_spl
| unordered_pair(sK5_skl,sK4_skl) != unordered_pair(sK4_skl,sK5_skl) ),
inference(backward_demodulation,[status(thm)],[f2924,f568]) ).
fof(f2972,plain,
( sQ28_spl
| ~ sQ90_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2932,f18]) ).
fof(f2973,plain,
( sQ28_spl
| ~ sQ90_spl ),
inference(contradiction_clause,[status(thm)],[f2972]) ).
fof(f3069,plain,
( ~ in(sK4_skl,symmetric_difference(singleton(sK5_skl),singleton(sK5_skl)))
| in(sK4_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f884,f56]) ).
fof(f3077,definition,
( sQ92_spl
<=> in(sK4_skl,symmetric_difference(singleton(sK5_skl),singleton(sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f3080,plain,
( ~ sQ92_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f3069,f162,f3077]) ).
fof(f3084,plain,
( sQ1_spl
| ~ in(sK4_skl,symmetric_difference(sK4_skl,unordered_pair(sK5_skl,sK5_skl)))
| in(sK4_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f879,f56]) ).
fof(f3092,definition,
( sQ93_spl
<=> in(sK4_skl,symmetric_difference(sK4_skl,unordered_pair(sK5_skl,sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f3095,plain,
( ~ sQ93_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f3084,f162,f3092]) ).
fof(f3099,plain,
( sQ1_spl
| ~ in(sK4_skl,symmetric_difference(unordered_pair(sK5_skl,sK5_skl),sK4_skl))
| in(sK4_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f878,f56]) ).
fof(f3109,definition,
( sQ94_spl
<=> in(sK4_skl,symmetric_difference(unordered_pair(sK5_skl,sK5_skl),sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f3112,plain,
( ~ sQ94_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f3099,f162,f3109]) ).
fof(f3116,plain,
( ~ in(sK4_skl,symmetric_difference(sK4_skl,sK4_skl))
| in(sK4_skl,unordered_pair(sK5_skl,sK5_skl)) ),
inference(resolution,[status(thm)],[f960,f56]) ).
fof(f3124,plain,
( ~ sQ41_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f3116,f219,f1180]) ).
fof(f3206,plain,
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl))))
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f1190,f133]) ).
fof(f3207,plain,
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl)))))
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f1190,f857]) ).
fof(f3209,plain,
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,singleton(unordered_pair(sK4_skl,sK5_skl))))
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f1190,f84]) ).
fof(f3210,plain,
( ~ in(sK5_skl,singleton(sK5_skl))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,sK5_skl))
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f1190,f1113]) ).
fof(f3225,definition,
( sQ96_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f3228,plain,
( ~ sQ96_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f3206,f1193,f3225]) ).
fof(f3229,definition,
( sQ97_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f3232,plain,
( ~ sQ97_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f3207,f1193,f3229]) ).
fof(f3237,definition,
( sQ99_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,singleton(unordered_pair(sK4_skl,sK5_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f3240,plain,
( ~ sQ99_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f3209,f1193,f3237]) ).
fof(f3241,definition,
( sQ100_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f3243,plain,
( sQ100_spl
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,sK5_skl)) ),
inference(component_clause,[status(thm)],[f3241]) ).
fof(f3244,plain,
( ~ sQ45_spl
| ~ sQ100_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f3210,f1193,f3241,f1215]) ).
fof(f3250,plain,
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK4_skl)))
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f1189,f131]) ).
fof(f3266,definition,
( sQ102_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK4_skl))) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f3269,plain,
( ~ sQ102_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f3250,f1193,f3266]) ).
fof(f3271,plain,
! [X0] :
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(X0,sK4_skl)))
| ~ in(X0,symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f1188,f131]) ).
fof(f3286,definition,
! [X0] :
( sQ103_spl
<=> ( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(X0,sK4_skl)))
| ~ in(X0,symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f3289,plain,
( sQ103_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f3271,f1193,f3286]) ).
fof(f3321,plain,
! [X0] :
( in(sK5_skl,unordered_pair(sK4_skl,sK4_skl))
| ~ in(sK5_skl,X0)
| ~ in(X0,sK5_skl) ),
inference(resolution,[status(thm)],[f927,f55]) ).
fof(f3331,plain,
( sQ7_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f3321,f279,f242]) ).
fof(f3333,plain,
( ~ in(sK4_skl,singleton(sK4_skl))
| ~ in(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),symmetric_difference(sK5_skl,sK4_skl))
| ~ in(sK5_skl,singleton(sK5_skl)) ),
inference(resolution,[status(thm)],[f1112,f1191]) ).
fof(f3346,definition,
( sQ104_spl
<=> in(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),symmetric_difference(sK5_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f3348,plain,
( sQ104_spl
| ~ in(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),symmetric_difference(sK5_skl,sK4_skl)) ),
inference(component_clause,[status(thm)],[f3346]) ).
fof(f3349,plain,
( ~ sQ42_spl
| ~ sQ104_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f3333,f1215,f3346,f1193]) ).
fof(f3394,plain,
( ~ in(symmetric_difference(unordered_pair(sK5_skl,sK5_skl),singleton(sK4_skl)),symmetric_difference(sK5_skl,sK4_skl))
| ~ in(sK5_skl,unordered_pair(sK5_skl,sK5_skl))
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f1663,f1112]) ).
fof(f3405,definition,
( sQ105_spl
<=> in(sK5_skl,unordered_pair(sK5_skl,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f3407,plain,
( sQ105_spl
| ~ in(sK5_skl,unordered_pair(sK5_skl,sK5_skl)) ),
inference(component_clause,[status(thm)],[f3405]) ).
fof(f3408,definition,
( sQ106_spl
<=> in(symmetric_difference(unordered_pair(sK5_skl,sK5_skl),singleton(sK4_skl)),symmetric_difference(sK5_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f3411,plain,
( ~ sQ106_spl
| ~ sQ105_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f3394,f1193,f3405,f3408]) ).
fof(f3420,plain,
( sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3407,f65]) ).
fof(f3421,plain,
sQ105_spl,
inference(contradiction_clause,[status(thm)],[f3420]) ).
fof(f3679,plain,
! [X0,X1] :
( in(sK5_skl,unordered_pair(sK4_skl,sK4_skl))
| ~ in(sK5_skl,symmetric_difference(X0,X1))
| ~ in(sK5_skl,X1)
| ~ in(sK5_skl,X0) ),
inference(resolution,[status(thm)],[f1719,f55]) ).
fof(f3691,plain,
( sQ7_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f3679,f1242,f242]) ).
fof(f3695,plain,
! [X0,X1] :
( in(sK4_skl,unordered_pair(sK5_skl,sK5_skl))
| ~ in(sK4_skl,symmetric_difference(X0,X1))
| ~ in(sK4_skl,X1)
| ~ in(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f1724,f55]) ).
fof(f3707,plain,
( sQ4_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f3695,f1261,f219]) ).
fof(f3708,plain,
! [X0,X1] :
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(symmetric_difference(X0,X1),sK4_skl)))
| ~ in(sK4_skl,singleton(sK4_skl))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0) ),
inference(resolution,[status(thm)],[f1747,f131]) ).
fof(f3725,definition,
! [X0,X1] :
( sQ114_spl
<=> ( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(symmetric_difference(X0,X1),sK4_skl)))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f3728,plain,
( ~ sQ42_spl
| sQ114_spl ),
inference(split_clause,[status(thm)],[f3708,f3725,f1193]) ).
fof(f3732,plain,
! [X0,X1] :
( ~ in(sK5_skl,symmetric_difference(symmetric_difference(X0,X1),singleton(sK4_skl)))
| in(sK5_skl,singleton(sK4_skl))
| ~ in(sK5_skl,X1)
| ~ in(sK5_skl,X0) ),
inference(resolution,[status(thm)],[f1833,f56]) ).
fof(f3744,definition,
! [X0,X1] :
( sQ115_spl
<=> ( ~ in(sK5_skl,symmetric_difference(symmetric_difference(X0,X1),singleton(sK4_skl)))
| ~ in(sK5_skl,X1)
| ~ in(sK5_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f3747,plain,
( sQ2_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f3732,f3744,f175]) ).
fof(f3748,definition,
! [X0,X1] :
( sQ116_spl
<=> ( in(sK5_skl,symmetric_difference(symmetric_difference(X0,X1),singleton(sK4_skl)))
| ~ in(sK5_skl,X1)
| ~ in(sK5_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f3749,plain,
! [X0,X1] :
( ~ sQ116_spl
| in(sK5_skl,symmetric_difference(symmetric_difference(X0,X1),singleton(sK4_skl)))
| ~ in(sK5_skl,X1)
| ~ in(sK5_skl,X0) ),
inference(component_clause,[status(thm)],[f3748]) ).
fof(f3771,plain,
! [X0,X1] :
( ~ sQ116_spl
| ~ in(sK5_skl,X1)
| ~ in(sK5_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3749,f1720]) ).
fof(f3776,plain,
( ~ sQ116_spl
| $false ),
inference(resolution,[status(thm)],[f3771,f65]) ).
fof(f3809,plain,
~ sQ116_spl,
inference(contradiction_clause,[status(thm)],[f3776]) ).
fof(f3989,plain,
( ~ sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f267,f1520]) ).
fof(f3990,plain,
~ sQ66_spl,
inference(contradiction_clause,[status(thm)],[f3989]) ).
fof(f4100,plain,
! [X0,X1] :
( ~ in(sK4_skl,symmetric_difference(symmetric_difference(X0,X1),singleton(sK5_skl)))
| in(sK4_skl,singleton(sK5_skl))
| ~ in(sK4_skl,X1)
| ~ in(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f1933,f56]) ).
fof(f4112,definition,
! [X0,X1] :
( sQ117_spl
<=> ( ~ in(sK4_skl,symmetric_difference(symmetric_difference(X0,X1),singleton(sK5_skl)))
| ~ in(sK4_skl,X1)
| ~ in(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f4115,plain,
( sQ0_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f4100,f4112,f159]) ).
fof(f4116,definition,
! [X0,X1] :
( sQ118_spl
<=> ( in(sK4_skl,symmetric_difference(symmetric_difference(X0,X1),singleton(sK5_skl)))
| ~ in(sK4_skl,X1)
| ~ in(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f4117,plain,
! [X0,X1] :
( ~ sQ118_spl
| in(sK4_skl,symmetric_difference(symmetric_difference(X0,X1),singleton(sK5_skl)))
| ~ in(sK4_skl,X1)
| ~ in(sK4_skl,X0) ),
inference(component_clause,[status(thm)],[f4116]) ).
fof(f4121,plain,
! [X0] :
( ~ sQ118_spl
| ~ in(sK4_skl,symmetric_difference(singleton(sK5_skl),X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f119,f4145]) ).
fof(f4145,plain,
! [X0,X1] :
( ~ sQ118_spl
| ~ in(sK4_skl,X1)
| ~ in(sK4_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4117,f1726]) ).
fof(f4146,plain,
! [X0] :
( ~ sQ118_spl
| ~ in(sK4_skl,X0)
| in(sK4_skl,singleton(sK5_skl)) ),
inference(resolution,[status(thm)],[f4121,f56]) ).
fof(f4156,plain,
( ~ sQ118_spl
| sQ61_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f4146,f159,f1424,f4116]) ).
fof(f4365,plain,
! [X0,X1] :
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(X0,X1))))
| ~ in(sK4_skl,singleton(sK4_skl))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0) ),
inference(resolution,[status(thm)],[f404,f1190]) ).
fof(f4378,definition,
! [X0,X1] :
( sQ119_spl
<=> ( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(X0,X1))))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f4381,plain,
( ~ sQ42_spl
| sQ119_spl ),
inference(split_clause,[status(thm)],[f4365,f4378,f1193]) ).
fof(f4438,plain,
( ~ in(sK4_skl,singleton(sK4_skl))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK4_skl))) ),
inference(resolution,[status(thm)],[f152,f1189]) ).
fof(f4439,plain,
! [X0,X1] :
( ~ in(sK4_skl,singleton(sK4_skl))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(symmetric_difference(X0,X1),sK4_skl))) ),
inference(resolution,[status(thm)],[f152,f1747]) ).
fof(f4440,plain,
! [X0] :
( ~ in(X0,symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))
| ~ in(sK4_skl,singleton(sK4_skl))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(X0,sK4_skl))) ),
inference(resolution,[status(thm)],[f152,f1188]) ).
fof(f4452,definition,
( sQ120_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK4_skl))) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f4455,plain,
( ~ sQ42_spl
| ~ sQ120_spl ),
inference(split_clause,[status(thm)],[f4438,f4452,f1193]) ).
fof(f4456,definition,
! [X0,X1] :
( sQ121_spl
<=> ( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(symmetric_difference(X0,X1),sK4_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f4459,plain,
( ~ sQ42_spl
| sQ121_spl ),
inference(split_clause,[status(thm)],[f4439,f4456,f1193]) ).
fof(f4460,definition,
! [X0] :
( sQ122_spl
<=> ( ~ in(X0,symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(X0,sK4_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f4463,plain,
( ~ sQ42_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f4440,f4460,f1193]) ).
fof(f4467,plain,
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)))))
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f151,f1190]) ).
fof(f4476,definition,
( sQ123_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f4479,plain,
( ~ sQ123_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f4467,f1193,f4476]) ).
fof(f4514,plain,
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))))
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f142,f1190]) ).
fof(f4523,definition,
( sQ124_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f4526,plain,
( ~ sQ124_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f4514,f1193,f4523]) ).
fof(f4547,plain,
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl)))))
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f141,f1190]) ).
fof(f4556,definition,
( sQ125_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(singleton(unordered_pair(sK4_skl,sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f4559,plain,
( ~ sQ125_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f4547,f1193,f4556]) ).
fof(f4813,plain,
! [X0,X1] :
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(symmetric_difference(X0,X1),unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)))))
| ~ in(sK4_skl,singleton(sK4_skl))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0) ),
inference(resolution,[status(thm)],[f1744,f1190]) ).
fof(f4815,plain,
! [X0,X1] :
( in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(X0,X1))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0) ),
inference(resolution,[status(thm)],[f1744,f55]) ).
fof(f4826,definition,
! [X0,X1] :
( sQ126_spl
<=> ( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(symmetric_difference(X0,X1),unordered_pair(unordered_pair(sK4_skl,sK5_skl),unordered_pair(sK4_skl,sK5_skl)))))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f4829,plain,
( ~ sQ42_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f4813,f4826,f1193]) ).
fof(f4831,plain,
( sQ18_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f4815,f809,f363]) ).
fof(f4834,plain,
! [X0,X1] :
( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(symmetric_difference(X0,X1),symmetric_difference(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl))))))
| ~ in(sK4_skl,singleton(sK4_skl))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0) ),
inference(resolution,[status(thm)],[f1739,f1190]) ).
fof(f4849,definition,
! [X0,X1] :
( sQ127_spl
<=> ( ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(symmetric_difference(X0,X1),symmetric_difference(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),singleton(unordered_pair(sK4_skl,sK5_skl))))))
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X1)
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f4852,plain,
( ~ sQ42_spl
| sQ127_spl ),
inference(split_clause,[status(thm)],[f4834,f4849,f1193]) ).
fof(f4904,plain,
( sQ86_spl
| sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl) = sK4_skl
| symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)) = unordered_pair(sK5_skl,sK4_skl)
| ~ in(sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl),singleton(sK4_skl))
| ~ in(sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl),singleton(sK5_skl)) ),
inference(resolution,[status(thm)],[f2810,f409]) ).
fof(f4905,plain,
( sQ86_spl
| ~ in(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl))
| sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl) = sK4_skl
| symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)) = unordered_pair(sK5_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f2810,f115]) ).
fof(f4917,plain,
( sQ86_spl
| sQ85_spl
| sQ90_spl
| ~ sQ89_spl
| ~ sQ88_spl ),
inference(split_clause,[status(thm)],[f4904,f2917,f2920,f2923,f2804,f2808]) ).
fof(f4918,definition,
( sQ129_spl
<=> in(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f4921,plain,
( sQ86_spl
| ~ sQ129_spl
| sQ85_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f4905,f2923,f2804,f4918,f2808]) ).
fof(f4951,plain,
( sQ58_spl
| sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl) = sK5_skl
| symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)) = unordered_pair(sK4_skl,sK5_skl)
| ~ in(sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl),singleton(sK4_skl))
| ~ in(sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl),singleton(sK5_skl)) ),
inference(resolution,[status(thm)],[f1322,f409]) ).
fof(f4952,plain,
( sQ58_spl
| ~ in(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl))
| sK1_skl(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl,sK4_skl) = sK5_skl
| symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)) = unordered_pair(sK4_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f1322,f115]) ).
fof(f4964,plain,
( sQ58_spl
| sQ29_spl
| sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f4951,f560,f563,f566,f569,f1320]) ).
fof(f4965,plain,
( sQ58_spl
| ~ sQ56_spl
| sQ29_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f4952,f566,f569,f1313,f1320]) ).
fof(f4968,plain,
( sQ100_spl
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(sK4_skl,sK5_skl)))
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f3243,f1190]) ).
fof(f4969,plain,
( sQ100_spl
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl)
| in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK4_skl) ),
inference(resolution,[status(thm)],[f3243,f56]) ).
fof(f4977,definition,
( sQ130_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(sK4_skl,sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f4980,plain,
( sQ100_spl
| ~ sQ130_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f4968,f1193,f4977,f3241]) ).
fof(f4981,definition,
( sQ131_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f4982,plain,
( ~ sQ131_spl
| in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK4_skl) ),
inference(component_clause,[status(thm)],[f4981]) ).
fof(f4983,plain,
( sQ131_spl
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK4_skl) ),
inference(component_clause,[status(thm)],[f4981]) ).
fof(f4984,definition,
( sQ132_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f4987,plain,
( sQ100_spl
| ~ sQ132_spl
| sQ131_spl ),
inference(split_clause,[status(thm)],[f4969,f4981,f4984,f3241]) ).
fof(f4989,plain,
( ~ sQ131_spl
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f4982,f1034]) ).
fof(f4992,plain,
( ~ sQ131_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f4989,f1193,f4981]) ).
fof(f5045,plain,
! [X0,X1] :
( in(unordered_pair(sK4_skl,sK5_skl),unordered_pair(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))))
| ~ in(unordered_pair(sK4_skl,sK5_skl),symmetric_difference(X0,X1))
| ~ in(unordered_pair(sK4_skl,sK5_skl),X1)
| ~ in(unordered_pair(sK4_skl,sK5_skl),X0) ),
inference(resolution,[status(thm)],[f1734,f55]) ).
fof(f5057,plain,
( sQ19_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f5045,f788,f390]) ).
fof(f5093,plain,
! [X0] :
( ~ in(symmetric_difference(unordered_pair(sK4_skl,sK5_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(X0,singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))))))
| ~ in(sK4_skl,unordered_pair(sK4_skl,sK5_skl))
| ~ in(unordered_pair(sK4_skl,sK5_skl),X0)
| ~ in(symmetric_difference(X0,singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))),singleton(sK5_skl)) ),
inference(resolution,[status(thm)],[f1688,f1190]) ).
fof(f5107,definition,
! [X0] :
( sQ136_spl
<=> ( ~ in(symmetric_difference(unordered_pair(sK4_skl,sK5_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,symmetric_difference(X0,singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))))))
| ~ in(unordered_pair(sK4_skl,sK5_skl),X0)
| ~ in(symmetric_difference(X0,singleton(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)))),singleton(sK5_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f5110,definition,
( sQ137_spl
<=> in(sK4_skl,unordered_pair(sK4_skl,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f5112,plain,
( sQ137_spl
| ~ in(sK4_skl,unordered_pair(sK4_skl,sK5_skl)) ),
inference(component_clause,[status(thm)],[f5110]) ).
fof(f5113,plain,
( ~ sQ137_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f5093,f5107,f5110]) ).
fof(f5114,plain,
( sQ137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5112,f64]) ).
fof(f5115,plain,
sQ137_spl,
inference(contradiction_clause,[status(thm)],[f5114]) ).
fof(f5118,plain,
( sQ131_spl
| ~ in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,sK4_skl))
| ~ in(sK4_skl,singleton(sK4_skl)) ),
inference(resolution,[status(thm)],[f4983,f1190]) ).
fof(f5125,definition,
( sQ138_spl
<=> in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),symmetric_difference(sK4_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f5128,plain,
( sQ131_spl
| ~ sQ138_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f5118,f1193,f5125,f4981]) ).
fof(f5139,plain,
( sQ104_spl
| ~ in(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl)
| in(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl) ),
inference(resolution,[status(thm)],[f3348,f56]) ).
fof(f5151,definition,
( sQ139_spl
<=> in(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f5152,plain,
( ~ sQ139_spl
| in(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK5_skl) ),
inference(component_clause,[status(thm)],[f5151]) ).
fof(f5154,definition,
( sQ140_spl
<=> in(symmetric_difference(singleton(sK5_skl),singleton(sK4_skl)),sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f5157,plain,
( sQ104_spl
| ~ sQ140_spl
| sQ139_spl ),
inference(split_clause,[status(thm)],[f5139,f5151,f5154,f3346]) ).
fof(f5162,plain,
( ~ sQ139_spl
| in(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl) ),
inference(paramodulation,[status(thm)],[f20,f5152]) ).
fof(f5165,plain,
( ~ sQ139_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f5162,f4984,f5151]) ).
fof(f5445,plain,
( sQ22_spl
| sQ21_spl
| ~ in(sK1_skl(symmetric_difference(singleton(sK4_skl),singleton(sK5_skl)),sK5_skl,sK4_skl),symmetric_difference(singleton(sK4_skl),singleton(sK5_skl))) ),
inference(resolution,[status(thm)],[f1545,f612]) ).
fof(f5457,plain,
( sQ22_spl
| sQ21_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f5445,f436,f439,f446]) ).
fof(f5458,plain,
$false,
inference(sat_refutation,[status(thm)],[f165,f181,f184,f186,f303,f314,f321,f340,f351,f358,f366,f385,f393,f442,f449,f474,f481,f482,f484,f489,f499,f587,f595,f683,f839,f1123,f1135,f1145,f1157,f1170,f1199,f1203,f1205,f1221,f1225,f1231,f1283,f1298,f1358,f1369,f1427,f1443,f1444,f1508,f1524,f1525,f2252,f2349,f2807,f2811,f2815,f2816,f2973,f3080,f3095,f3112,f3124,f3228,f3232,f3240,f3244,f3269,f3289,f3331,f3349,f3411,f3421,f3691,f3707,f3728,f3747,f3809,f3990,f4115,f4156,f4381,f4455,f4459,f4463,f4479,f4526,f4559,f4829,f4831,f4852,f4917,f4921,f4964,f4965,f4980,f4987,f4992,f5057,f5113,f5115,f5128,f5157,f5165,f5457]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET888+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n013.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 21 05:42:21 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 35.84/4.96 % Refutation found
% 35.84/4.96 % SZS status Theorem for theBenchmark: Theorem is valid
% 35.84/4.96 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 35.84/5.00 % Elapsed time: 4.635197 seconds
% 35.84/5.00 % CPU time: 36.450653 seconds
% 35.84/5.00 % Total memory used: 297.889 MB
% 35.84/5.00 % Net memory used: 263.820 MB
%------------------------------------------------------------------------------