%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET795+4 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:38 PM UTC 2026
% Result : Theorem 13.41s 2.18s
% Output : CNFRefutation 13.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 48
% Syntax : Number of formulae : 256 ( 25 unt; 37 def)
% Number of atoms : 830 ( 111 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 913 ( 339 ~; 385 |; 125 &)
% ( 53 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 45 ( 43 usr; 36 prp; 0-4 aty)
% Number of functors : 21 ( 21 usr; 5 con; 0-4 aty)
% Number of variables : 430 ( 403 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( subset(A,B)
<=> ! [X] :
( member(X,A)
=> member(X,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] : ~ member(X,empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [B,A,E] :
( member(B,difference(E,A))
<=> ( ~ member(B,A)
& member(B,E) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,A] :
( member(X,singleton(A))
<=> X = A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,A,B] :
( member(X,unordered_pair(A,B))
<=> ( X = B
| X = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,A] :
( member(X,sum(A))
<=> ? [Y] :
( member(X,Y)
& member(Y,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,A] :
( member(X,product(A))
<=> ! [Y] :
( member(Y,A)
=> member(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [R,E] :
( order(R,E)
<=> ( ! [X,Y,Z] :
( ( member(Z,E)
& member(Y,E)
& member(X,E) )
=> ( ( apply(R,Y,Z)
& apply(R,X,Y) )
=> apply(R,X,Z) ) )
& ! [X,Y] :
( ( member(Y,E)
& member(X,E) )
=> ( ( apply(R,Y,X)
& apply(R,X,Y) )
=> X = Y ) )
& ! [X] :
( member(X,E)
=> apply(R,X,X) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [R,E,M] :
( upper_bound(M,R,E)
<=> ! [X] :
( member(X,E)
=> apply(R,X,M) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A,X,R,E] :
( least_upper_bound(A,X,R,E)
<=> ( ! [M] :
( ( upper_bound(M,R,X)
& member(M,E) )
=> apply(R,A,M) )
& upper_bound(A,R,X)
& member(A,X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,conjecture,
! [R,E,A,B] :
( ( apply(R,A,B)
& member(B,E)
& member(A,E)
& order(R,E) )
=> least_upper_bound(B,unordered_pair(A,B),R,E) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
~ ! [R,E,A,B] :
( ( apply(R,A,B)
& member(B,E)
& member(A,E)
& order(R,E) )
=> least_upper_bound(B,unordered_pair(A,B),R,E) ),
inference(negated_conjecture,[status(cth)],[f22]) ).
fof(f24,plain,
! [A,B] :
( subset(A,B)
<=> ! [X] :
( member(X,B)
| ~ member(X,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f25,plain,
! [A,B] :
( ( ? [X] :
( ~ member(X,B)
& member(X,A) )
| subset(A,B) )
& ( ! [X] :
( member(X,B)
| ~ member(X,A) )
| ~ subset(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f24]) ).
fof(f26,plain,
( ! [A,B] :
( ? [X] :
( ~ member(X,B)
& member(X,A) )
| subset(A,B) )
& ! [A,B] :
( ! [X] :
( member(X,B)
| ~ member(X,A) )
| ~ subset(A,B) ) ),
inference(miniscoping,[status(thm)],[f25]) ).
fof(f27,plain,
( ! [A,B] :
( ( ~ member(sK0_skl(B,A),B)
& member(sK0_skl(B,A),A) )
| subset(A,B) )
& ! [A,B] :
( ! [X] :
( member(X,B)
| ~ member(X,A) )
| ~ subset(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X,sK0_skl(B,A))],[f26]) ).
fof(f28,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f29,plain,
! [X0,X1] :
( member(sK0_skl(X1,X0),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f50,plain,
! [X0] : ~ member(X0,empty_set),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f51,plain,
! [B,A,E] :
( ( member(B,A)
| ~ member(B,E)
| member(B,difference(E,A)) )
& ( ( ~ member(B,A)
& member(B,E) )
| ~ member(B,difference(E,A)) ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f52,plain,
( ! [B,A,E] :
( member(B,A)
| ~ member(B,E)
| member(B,difference(E,A)) )
& ! [B,A,E] :
( ( ~ member(B,A)
& member(B,E) )
| ~ member(B,difference(E,A)) ) ),
inference(miniscoping,[status(thm)],[f51]) ).
fof(f53,plain,
! [X0,X1,X2] :
( member(X0,X1)
| ~ member(X0,difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f54,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| ~ member(X0,difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f56,plain,
! [X,A] :
( ( X != A
| member(X,singleton(A)) )
& ( X = A
| ~ member(X,singleton(A)) ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f57,plain,
( ! [X,A] :
( X != A
| member(X,singleton(A)) )
& ! [X,A] :
( X = A
| ~ member(X,singleton(A)) ) ),
inference(miniscoping,[status(thm)],[f56]) ).
fof(f58,plain,
! [X0,X1] :
( X0 = X1
| ~ member(X0,singleton(X1)) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [X0,X1] :
( X0 != X1
| member(X0,singleton(X1)) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f60,plain,
! [X,A,B] :
( ( ( X != B
& X != A )
| member(X,unordered_pair(A,B)) )
& ( X = B
| X = A
| ~ member(X,unordered_pair(A,B)) ) ),
inference(NNF_transformation,[status(thm)],[f9]) ).
fof(f61,plain,
( ! [X,A,B] :
( ( X != B
& X != A )
| member(X,unordered_pair(A,B)) )
& ! [X,A,B] :
( X = B
| X = A
| ~ member(X,unordered_pair(A,B)) ) ),
inference(miniscoping,[status(thm)],[f60]) ).
fof(f62,plain,
! [X0,X1,X2] :
( X0 = X2
| X0 = X1
| ~ member(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
! [X0,X1,X2] :
( X0 != X1
| member(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f64,plain,
! [X0,X1,X2] :
( X0 != X2
| member(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f65,plain,
! [X,A] :
( ( ! [Y] :
( ~ member(X,Y)
| ~ member(Y,A) )
| member(X,sum(A)) )
& ( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,sum(A)) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f66,plain,
( ! [X,A] :
( ! [Y] :
( ~ member(X,Y)
| ~ member(Y,A) )
| member(X,sum(A)) )
& ! [X,A] :
( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,sum(A)) ) ),
inference(miniscoping,[status(thm)],[f65]) ).
fof(f67,plain,
( ! [X,A] :
( ! [Y] :
( ~ member(X,Y)
| ~ member(Y,A) )
| member(X,sum(A)) )
& ! [X,A] :
( ( member(X,sK1_skl(A,X))
& member(sK1_skl(A,X),A) )
| ~ member(X,sum(A)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Y,sK1_skl(A,X))],[f66]) ).
fof(f68,plain,
! [X0,X1] :
( member(sK1_skl(X1,X0),X1)
| ~ member(X0,sum(X1)) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f69,plain,
! [X0,X1] :
( member(X0,sK1_skl(X1,X0))
| ~ member(X0,sum(X1)) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f70,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| ~ member(X2,X1)
| member(X0,sum(X1)) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f71,plain,
! [X,A] :
( member(X,product(A))
<=> ! [Y] :
( member(X,Y)
| ~ member(Y,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f72,plain,
! [X,A] :
( ( ? [Y] :
( ~ member(X,Y)
& member(Y,A) )
| member(X,product(A)) )
& ( ! [Y] :
( member(X,Y)
| ~ member(Y,A) )
| ~ member(X,product(A)) ) ),
inference(NNF_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
( ! [X,A] :
( ? [Y] :
( ~ member(X,Y)
& member(Y,A) )
| member(X,product(A)) )
& ! [X,A] :
( ! [Y] :
( member(X,Y)
| ~ member(Y,A) )
| ~ member(X,product(A)) ) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f74,plain,
( ! [X,A] :
( ( ~ member(X,sK2_skl(A,X))
& member(sK2_skl(A,X),A) )
| member(X,product(A)) )
& ! [X,A] :
( ! [Y] :
( member(X,Y)
| ~ member(Y,A) )
| ~ member(X,product(A)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y,sK2_skl(A,X))],[f73]) ).
fof(f75,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X2,X1)
| ~ member(X0,product(X1)) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f76,plain,
! [X0,X1] :
( member(sK2_skl(X1,X0),X1)
| member(X0,product(X1)) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f78,plain,
! [R,E] :
( order(R,E)
<=> ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X,Y] :
( X = Y
| ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X] :
( apply(R,X,X)
| ~ member(X,E) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f79,definition,
! [R,E] :
( sP0_prd(E,R)
<=> ( ! [X,Y] :
( X = Y
| ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X] :
( apply(R,X,X)
| ~ member(X,E) ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f80,plain,
! [R,E] :
( order(R,E)
<=> ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& sP0_prd(E,R) ) ),
inference(formula_renaming,[status(thm)],[f78,f79]) ).
fof(f81,plain,
! [R,E] :
( ( ? [X,Y,Z] :
( ~ apply(R,X,Z)
& apply(R,Y,Z)
& apply(R,X,Y)
& member(Z,E)
& member(Y,E)
& member(X,E) )
| ~ sP0_prd(E,R)
| order(R,E) )
& ( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& sP0_prd(E,R) )
| ~ order(R,E) ) ),
inference(NNF_transformation,[status(thm)],[f80]) ).
fof(f82,plain,
( ! [R,E] :
( ? [X,Y,Z] :
( ~ apply(R,X,Z)
& apply(R,Y,Z)
& apply(R,X,Y)
& member(Z,E)
& member(Y,E)
& member(X,E) )
| ~ sP0_prd(E,R)
| order(R,E) )
& ! [R,E] :
( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& sP0_prd(E,R) )
| ~ order(R,E) ) ),
inference(miniscoping,[status(thm)],[f81]) ).
fof(f83,plain,
( ! [R,E] :
( ( ~ apply(R,sK3_skl(E,R),sK5_skl(E,R))
& apply(R,sK4_skl(E,R),sK5_skl(E,R))
& apply(R,sK3_skl(E,R),sK4_skl(E,R))
& member(sK5_skl(E,R),E)
& member(sK4_skl(E,R),E)
& member(sK3_skl(E,R),E) )
| ~ sP0_prd(E,R)
| order(R,E) )
& ! [R,E] :
( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& sP0_prd(E,R) )
| ~ order(R,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl]),skolemize(X,sK3_skl(E,R)),skolemize(Y,sK4_skl(E,R)),skolemize(Z,sK5_skl(E,R))],[f82]) ).
fof(f84,plain,
! [X0,X1] :
( sP0_prd(X1,X0)
| ~ order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f102,plain,
! [R,E,M] :
( upper_bound(M,R,E)
<=> ! [X] :
( apply(R,X,M)
| ~ member(X,E) ) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f103,plain,
! [R,E,M] :
( ( ? [X] :
( ~ apply(R,X,M)
& member(X,E) )
| upper_bound(M,R,E) )
& ( ! [X] :
( apply(R,X,M)
| ~ member(X,E) )
| ~ upper_bound(M,R,E) ) ),
inference(NNF_transformation,[status(thm)],[f102]) ).
fof(f104,plain,
( ! [R,E,M] :
( ? [X] :
( ~ apply(R,X,M)
& member(X,E) )
| upper_bound(M,R,E) )
& ! [R,E,M] :
( ! [X] :
( apply(R,X,M)
| ~ member(X,E) )
| ~ upper_bound(M,R,E) ) ),
inference(miniscoping,[status(thm)],[f103]) ).
fof(f105,plain,
( ! [R,E,M] :
( ( ~ apply(R,sK8_skl(M,E,R),M)
& member(sK8_skl(M,E,R),E) )
| upper_bound(M,R,E) )
& ! [R,E,M] :
( ! [X] :
( apply(R,X,M)
| ~ member(X,E) )
| ~ upper_bound(M,R,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X,sK8_skl(M,E,R))],[f104]) ).
fof(f106,plain,
! [X0,X1,X2,X3] :
( apply(X1,X3,X0)
| ~ member(X3,X2)
| ~ upper_bound(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f107,plain,
! [X0,X1,X2] :
( member(sK8_skl(X0,X2,X1),X2)
| upper_bound(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f108,plain,
! [X0,X1,X2] :
( ~ apply(X1,sK8_skl(X0,X2,X1),X0)
| upper_bound(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f150,plain,
! [A,X,R,E] :
( least_upper_bound(A,X,R,E)
<=> ( ! [M] :
( apply(R,A,M)
| ~ upper_bound(M,R,X)
| ~ member(M,E) )
& upper_bound(A,R,X)
& member(A,X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f151,plain,
! [A,X,R,E] :
( ( ? [M] :
( ~ apply(R,A,M)
& upper_bound(M,R,X)
& member(M,E) )
| ~ upper_bound(A,R,X)
| ~ member(A,X)
| least_upper_bound(A,X,R,E) )
& ( ( ! [M] :
( apply(R,A,M)
| ~ upper_bound(M,R,X)
| ~ member(M,E) )
& upper_bound(A,R,X)
& member(A,X) )
| ~ least_upper_bound(A,X,R,E) ) ),
inference(NNF_transformation,[status(thm)],[f150]) ).
fof(f152,plain,
( ! [A,X,R,E] :
( ? [M] :
( ~ apply(R,A,M)
& upper_bound(M,R,X)
& member(M,E) )
| ~ upper_bound(A,R,X)
| ~ member(A,X)
| least_upper_bound(A,X,R,E) )
& ! [A,X,R,E] :
( ( ! [M] :
( apply(R,A,M)
| ~ upper_bound(M,R,X)
| ~ member(M,E) )
& upper_bound(A,R,X)
& member(A,X) )
| ~ least_upper_bound(A,X,R,E) ) ),
inference(miniscoping,[status(thm)],[f151]) ).
fof(f153,plain,
( ! [A,X,R,E] :
( ( ~ apply(R,A,sK14_skl(E,R,X,A))
& upper_bound(sK14_skl(E,R,X,A),R,X)
& member(sK14_skl(E,R,X,A),E) )
| ~ upper_bound(A,R,X)
| ~ member(A,X)
| least_upper_bound(A,X,R,E) )
& ! [A,X,R,E] :
( ( ! [M] :
( apply(R,A,M)
| ~ upper_bound(M,R,X)
| ~ member(M,E) )
& upper_bound(A,R,X)
& member(A,X) )
| ~ least_upper_bound(A,X,R,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(M,sK14_skl(E,R,X,A))],[f152]) ).
fof(f158,plain,
! [X0,X1,X2,X3] :
( upper_bound(sK14_skl(X3,X2,X1,X0),X2,X1)
| ~ upper_bound(X0,X2,X1)
| ~ member(X0,X1)
| least_upper_bound(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f159,plain,
! [X0,X1,X2,X3] :
( ~ apply(X2,X0,sK14_skl(X3,X2,X1,X0))
| ~ upper_bound(X0,X2,X1)
| ~ member(X0,X1)
| least_upper_bound(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f170,plain,
? [R,E,A,B] :
( ~ least_upper_bound(B,unordered_pair(A,B),R,E)
& apply(R,A,B)
& member(B,E)
& member(A,E)
& order(R,E) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f171,plain,
( ~ least_upper_bound(sK19_skl,unordered_pair(sK18_skl,sK19_skl),sK16_skl,sK17_skl)
& apply(sK16_skl,sK18_skl,sK19_skl)
& member(sK19_skl,sK17_skl)
& member(sK18_skl,sK17_skl)
& order(sK16_skl,sK17_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl,sK19_skl]),skolemize(R,sK16_skl),skolemize(E,sK17_skl),skolemize(A,sK18_skl),skolemize(B,sK19_skl)],[f170]) ).
fof(f172,plain,
order(sK16_skl,sK17_skl),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f173,plain,
member(sK18_skl,sK17_skl),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f174,plain,
member(sK19_skl,sK17_skl),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f175,plain,
apply(sK16_skl,sK18_skl,sK19_skl),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f176,plain,
~ least_upper_bound(sK19_skl,unordered_pair(sK18_skl,sK19_skl),sK16_skl,sK17_skl),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f177,definition,
! [R,E,X] :
( sP1_prd(X,E,R)
<=> ( apply(R,X,X)
| ~ member(X,E) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f178,plain,
! [R,E] :
( sP0_prd(E,R)
<=> ( ! [X,Y] :
( X = Y
| ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X] : sP1_prd(X,E,R) ) ),
inference(formula_renaming,[status(thm)],[f79,f177]) ).
fof(f179,plain,
! [R,E] :
( ( ? [X,Y] :
( X != Y
& apply(R,Y,X)
& apply(R,X,Y)
& member(Y,E)
& member(X,E) )
| ? [X] : ~ sP1_prd(X,E,R)
| sP0_prd(E,R) )
& ( ( ! [X,Y] :
( X = Y
| ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X] : sP1_prd(X,E,R) )
| ~ sP0_prd(E,R) ) ),
inference(NNF_transformation,[status(thm)],[f178]) ).
fof(f180,plain,
( ! [R,E] :
( ? [X,Y] :
( X != Y
& apply(R,Y,X)
& apply(R,X,Y)
& member(Y,E)
& member(X,E) )
| ? [X] : ~ sP1_prd(X,E,R)
| sP0_prd(E,R) )
& ! [R,E] :
( ( ! [X,Y] :
( X = Y
| ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X] : sP1_prd(X,E,R) )
| ~ sP0_prd(E,R) ) ),
inference(miniscoping,[status(thm)],[f179]) ).
fof(f181,plain,
( ! [R,E] :
( ( sK21_skl(E,R) != sK22_skl(E,R)
& apply(R,sK22_skl(E,R),sK21_skl(E,R))
& apply(R,sK21_skl(E,R),sK22_skl(E,R))
& member(sK22_skl(E,R),E)
& member(sK21_skl(E,R),E) )
| ~ sP1_prd(sK20_skl(E,R),E,R)
| sP0_prd(E,R) )
& ! [R,E] :
( ( ! [X,Y] :
( X = Y
| ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X] : sP1_prd(X,E,R) )
| ~ sP0_prd(E,R) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl,sK22_skl]),skolemize(X,sK20_skl(E,R)),skolemize(X,sK21_skl(E,R)),skolemize(Y,sK22_skl(E,R))],[f180]) ).
fof(f182,plain,
! [X0,X1,X2] :
( sP1_prd(X2,X0,X1)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f189,plain,
! [R,E,X] :
( ( ( ~ apply(R,X,X)
& member(X,E) )
| sP1_prd(X,E,R) )
& ( apply(R,X,X)
| ~ member(X,E)
| ~ sP1_prd(X,E,R) ) ),
inference(NNF_transformation,[status(thm)],[f177]) ).
fof(f190,plain,
( ! [R,E,X] :
( ( ~ apply(R,X,X)
& member(X,E) )
| sP1_prd(X,E,R) )
& ! [R,E,X] :
( apply(R,X,X)
| ~ member(X,E)
| ~ sP1_prd(X,E,R) ) ),
inference(miniscoping,[status(thm)],[f189]) ).
fof(f191,plain,
! [X0,X1,X2] :
( apply(X2,X0,X0)
| ~ member(X0,X1)
| ~ sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f194,plain,
! [X0] : member(X0,singleton(X0)),
inference(destructive_equality_resolution,[status(thm)],[f59]) ).
fof(f195,plain,
! [X0,X1] : member(X0,unordered_pair(X0,X1)),
inference(destructive_equality_resolution,[status(thm)],[f63]) ).
fof(f196,plain,
! [X0,X1] : member(X0,unordered_pair(X1,X0)),
inference(destructive_equality_resolution,[status(thm)],[f64]) ).
fof(f202,plain,
! [X0,X1,X2] :
( member(X2,X0)
| ~ member(X2,X1)
| member(sK0_skl(X0,X1),X1) ),
inference(resolution,[status(thm)],[f29,f28]) ).
fof(f219,plain,
! [X0,X1,X2] :
( member(sK1_skl(X1,X2),X1)
| ~ member(X2,X0)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f70,f68]) ).
fof(f220,plain,
! [X0,X1,X2] :
( member(sK2_skl(X1,X2),X1)
| member(X2,X0)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f75,f76]) ).
fof(f232,plain,
! [X0,X1,X2] :
( sK0_skl(X2,singleton(X1)) = X1
| member(X0,X2)
| ~ member(X0,singleton(X1)) ),
inference(resolution,[status(thm)],[f202,f58]) ).
fof(f316,plain,
! [X0,X1,X2,X3] :
( sK1_skl(unordered_pair(X1,X2),X3) = X2
| sK1_skl(unordered_pair(X1,X2),X3) = X1
| ~ member(X3,X0)
| ~ member(X0,unordered_pair(X1,X2)) ),
inference(resolution,[status(thm)],[f219,f62]) ).
fof(f329,plain,
! [X0,X1,X2,X3] :
( sK2_skl(unordered_pair(X1,X2),X3) = X2
| sK2_skl(unordered_pair(X1,X2),X3) = X1
| member(X3,X0)
| ~ member(X0,unordered_pair(X1,X2)) ),
inference(resolution,[status(thm)],[f220,f62]) ).
fof(f345,plain,
! [X0,X1,X2] :
( sK1_skl(unordered_pair(X2,X1),X0) = X1
| sK1_skl(unordered_pair(X2,X1),X0) = X2
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f316,f196]) ).
fof(f346,plain,
! [X0,X1,X2] :
( sK1_skl(unordered_pair(X1,X2),X0) = X2
| sK1_skl(unordered_pair(X1,X2),X0) = X1
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f316,f195]) ).
fof(f353,plain,
! [X0] :
( sK1_skl(unordered_pair(X0,sK17_skl),sK19_skl) = sK17_skl
| sK1_skl(unordered_pair(X0,sK17_skl),sK19_skl) = X0 ),
inference(resolution,[status(thm)],[f345,f174]) ).
fof(f354,plain,
! [X0] :
( sK1_skl(unordered_pair(X0,sK17_skl),sK18_skl) = sK17_skl
| sK1_skl(unordered_pair(X0,sK17_skl),sK18_skl) = X0 ),
inference(resolution,[status(thm)],[f345,f173]) ).
fof(f363,plain,
! [X0,X1] :
( sK1_skl(unordered_pair(X0,singleton(X1)),X1) = singleton(X1)
| sK1_skl(unordered_pair(X0,singleton(X1)),X1) = X0 ),
inference(resolution,[status(thm)],[f345,f194]) ).
fof(f372,plain,
! [X0] :
( sK1_skl(unordered_pair(sK17_skl,X0),sK19_skl) = X0
| sK1_skl(unordered_pair(sK17_skl,X0),sK19_skl) = sK17_skl ),
inference(resolution,[status(thm)],[f346,f174]) ).
fof(f389,plain,
! [X0] :
( sK1_skl(unordered_pair(X0,sK17_skl),sK19_skl) = X0
| member(sK19_skl,sK17_skl)
| ~ member(sK19_skl,sum(unordered_pair(X0,sK17_skl))) ),
inference(paramodulation,[status(thm)],[f353,f69]) ).
fof(f390,plain,
! [X0] :
( sK1_skl(unordered_pair(X0,sK17_skl),sK19_skl) = X0
| sK17_skl != X0 ),
inference(equality_factoring,[status(thm)],[f353]) ).
fof(f391,definition,
! [X0] :
( sQ0_spl
<=> ( sK1_skl(unordered_pair(X0,sK17_skl),sK19_skl) = X0
| ~ member(sK19_skl,sum(unordered_pair(X0,sK17_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f394,definition,
( sQ1_spl
<=> member(sK19_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f397,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f389,f391,f394]) ).
fof(f398,plain,
sK1_skl(unordered_pair(sK17_skl,sK17_skl),sK19_skl) = sK17_skl,
inference(destructive_equality_resolution,[status(thm)],[f390]) ).
fof(f399,plain,
( sK1_skl(unordered_pair(sK17_skl,sK17_skl),sK19_skl) = sK17_skl
| sK17_skl = sK17_skl ),
inference(paramodulation,[status(thm)],[f353,f398]) ).
fof(f401,plain,
! [X0] :
( member(sK17_skl,unordered_pair(sK17_skl,sK17_skl))
| ~ member(sK19_skl,X0)
| ~ member(X0,unordered_pair(sK17_skl,sK17_skl)) ),
inference(paramodulation,[status(thm)],[f398,f219]) ).
fof(f402,plain,
( member(sK19_skl,sK17_skl)
| ~ member(sK19_skl,sum(unordered_pair(sK17_skl,sK17_skl))) ),
inference(paramodulation,[status(thm)],[f398,f69]) ).
fof(f403,definition,
( sQ2_spl
<=> sK17_skl = sK17_skl ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f406,definition,
( sQ3_spl
<=> sK1_skl(unordered_pair(sK17_skl,sK17_skl),sK19_skl) = sK17_skl ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f409,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f399,f403,f406]) ).
fof(f411,definition,
! [X0] :
( sQ4_spl
<=> ( ~ member(sK19_skl,X0)
| ~ member(X0,unordered_pair(sK17_skl,sK17_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f412,plain,
! [X0] :
( ~ sQ4_spl
| ~ member(sK19_skl,X0)
| ~ member(X0,unordered_pair(sK17_skl,sK17_skl)) ),
inference(component_clause,[status(thm)],[f411]) ).
fof(f414,definition,
( sQ5_spl
<=> member(sK17_skl,unordered_pair(sK17_skl,sK17_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f417,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f401,f411,f414]) ).
fof(f418,definition,
( sQ6_spl
<=> member(sK19_skl,sum(unordered_pair(sK17_skl,sK17_skl))) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f421,plain,
( sQ1_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f402,f418,f394]) ).
fof(f425,plain,
! [X0,X1,X2] :
( sK2_skl(unordered_pair(X2,X1),X0) = X1
| sK2_skl(unordered_pair(X2,X1),X0) = X2
| member(X0,X1) ),
inference(resolution,[status(thm)],[f329,f196]) ).
fof(f441,plain,
( ~ sQ4_spl
| ~ member(sK19_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f412,f196]) ).
fof(f446,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f441,f174]) ).
fof(f447,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f446]) ).
fof(f459,plain,
! [X0] :
( sK1_skl(unordered_pair(X0,sK17_skl),sK18_skl) = X0
| sK17_skl != X0 ),
inference(equality_factoring,[status(thm)],[f354]) ).
fof(f463,definition,
( sQ8_spl
<=> member(sK18_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f467,plain,
sK1_skl(unordered_pair(sK17_skl,sK17_skl),sK18_skl) = sK17_skl,
inference(destructive_equality_resolution,[status(thm)],[f459]) ).
fof(f468,plain,
( sK1_skl(unordered_pair(sK17_skl,sK17_skl),sK18_skl) = sK17_skl
| sK17_skl = sK17_skl ),
inference(paramodulation,[status(thm)],[f354,f467]) ).
fof(f471,plain,
( member(sK18_skl,sK17_skl)
| ~ member(sK18_skl,sum(unordered_pair(sK17_skl,sK17_skl))) ),
inference(paramodulation,[status(thm)],[f467,f69]) ).
fof(f472,definition,
( sQ9_spl
<=> sK1_skl(unordered_pair(sK17_skl,sK17_skl),sK18_skl) = sK17_skl ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f475,plain,
( sQ9_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f468,f403,f472]) ).
fof(f481,definition,
( sQ11_spl
<=> member(sK18_skl,sum(unordered_pair(sK17_skl,sK17_skl))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f483,plain,
( sQ11_spl
| ~ member(sK18_skl,sum(unordered_pair(sK17_skl,sK17_skl))) ),
inference(component_clause,[status(thm)],[f481]) ).
fof(f484,plain,
( sQ8_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f471,f481,f463]) ).
fof(f490,plain,
! [X0] :
( sK1_skl(unordered_pair(sK17_skl,X0),sK19_skl) = X0
| member(sK19_skl,sK17_skl)
| ~ member(sK19_skl,sum(unordered_pair(sK17_skl,X0))) ),
inference(paramodulation,[status(thm)],[f372,f69]) ).
fof(f496,definition,
! [X0] :
( sQ12_spl
<=> ( sK1_skl(unordered_pair(sK17_skl,X0),sK19_skl) = X0
| ~ member(sK19_skl,sum(unordered_pair(sK17_skl,X0))) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f499,plain,
( sQ1_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f490,f496,f394]) ).
fof(f512,plain,
! [X0,X1] :
( sK2_skl(unordered_pair(X0,empty_set),X1) = empty_set
| sK2_skl(unordered_pair(X0,empty_set),X1) = X0 ),
inference(resolution,[status(thm)],[f425,f50]) ).
fof(f523,plain,
! [X0,X1] :
( sK2_skl(unordered_pair(X0,empty_set),X1) = X0
| empty_set != X0 ),
inference(equality_factoring,[status(thm)],[f512]) ).
fof(f524,plain,
! [X0] : sK2_skl(unordered_pair(empty_set,empty_set),X0) = empty_set,
inference(destructive_equality_resolution,[status(thm)],[f523]) ).
fof(f527,plain,
! [X0,X1] :
( member(empty_set,unordered_pair(empty_set,empty_set))
| member(X1,X0)
| ~ member(X0,unordered_pair(empty_set,empty_set)) ),
inference(paramodulation,[status(thm)],[f524,f220]) ).
fof(f537,definition,
! [X0,X1] :
( sQ15_spl
<=> ( member(X1,X0)
| ~ member(X0,unordered_pair(empty_set,empty_set)) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f538,plain,
! [X0,X1] :
( ~ sQ15_spl
| member(X1,X0)
| ~ member(X0,unordered_pair(empty_set,empty_set)) ),
inference(component_clause,[status(thm)],[f537]) ).
fof(f540,definition,
( sQ16_spl
<=> member(empty_set,unordered_pair(empty_set,empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f543,plain,
( sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f527,f537,f540]) ).
fof(f547,plain,
! [X0] :
( ~ sQ15_spl
| member(X0,empty_set) ),
inference(resolution,[status(thm)],[f538,f196]) ).
fof(f555,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f547,f50]) ).
fof(f556,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f555]) ).
fof(f578,plain,
! [X0,X1] :
( sK0_skl(X1,singleton(X0)) = X0
| member(X0,X1) ),
inference(resolution,[status(thm)],[f232,f194]) ).
fof(f586,plain,
! [X0,X1] :
( member(sK1_skl(X0,X1),X0)
| sK0_skl(sum(X0),singleton(X1)) = X1 ),
inference(resolution,[status(thm)],[f578,f68]) ).
fof(f587,plain,
! [X0,X1,X2] :
( ~ member(X2,X1)
| sK0_skl(difference(X0,X1),singleton(X2)) = X2 ),
inference(resolution,[status(thm)],[f578,f54]) ).
fof(f588,plain,
! [X0,X1,X2] :
( member(X2,X0)
| sK0_skl(difference(X0,X1),singleton(X2)) = X2 ),
inference(resolution,[status(thm)],[f578,f53]) ).
fof(f614,plain,
! [X0] : sK0_skl(difference(X0,sK17_skl),singleton(sK19_skl)) = sK19_skl,
inference(resolution,[status(thm)],[f587,f174]) ).
fof(f615,plain,
! [X0] : sK0_skl(difference(X0,sK17_skl),singleton(sK18_skl)) = sK18_skl,
inference(resolution,[status(thm)],[f587,f173]) ).
fof(f634,definition,
( sQ17_spl
<=> member(sK19_skl,unordered_pair(sK18_skl,sK19_skl)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f636,plain,
( sQ17_spl
| ~ member(sK19_skl,unordered_pair(sK18_skl,sK19_skl)) ),
inference(component_clause,[status(thm)],[f634]) ).
fof(f637,definition,
( sQ18_spl
<=> upper_bound(sK19_skl,sK16_skl,unordered_pair(sK18_skl,sK19_skl)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f639,plain,
( sQ18_spl
| ~ upper_bound(sK19_skl,sK16_skl,unordered_pair(sK18_skl,sK19_skl)) ),
inference(component_clause,[status(thm)],[f637]) ).
fof(f644,plain,
! [X0,X1] :
( member(X0,difference(X1,sK17_skl))
| ~ member(X0,singleton(sK19_skl))
| member(sK19_skl,singleton(sK19_skl)) ),
inference(paramodulation,[status(thm)],[f614,f202]) ).
fof(f646,definition,
( sQ20_spl
<=> member(sK19_skl,singleton(sK19_skl)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f649,definition,
! [X0,X1] :
( sQ21_spl
<=> ( member(X0,difference(X1,sK17_skl))
| ~ member(X0,singleton(sK19_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f650,plain,
! [X0,X1] :
( ~ sQ21_spl
| member(X0,difference(X1,sK17_skl))
| ~ member(X0,singleton(sK19_skl)) ),
inference(component_clause,[status(thm)],[f649]) ).
fof(f652,plain,
( sQ21_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f644,f646,f649]) ).
fof(f674,plain,
! [X0] :
( ~ sQ21_spl
| ~ member(X0,sK17_skl)
| ~ member(X0,singleton(sK19_skl)) ),
inference(resolution,[status(thm)],[f650,f54]) ).
fof(f675,plain,
! [X0,X1] :
( ~ sQ21_spl
| member(X0,X1)
| ~ member(X0,singleton(sK19_skl)) ),
inference(resolution,[status(thm)],[f650,f53]) ).
fof(f679,plain,
! [X0] :
( ~ sQ21_spl
| ~ member(X0,singleton(sK19_skl)) ),
inference(backward_subsumption_resolution,[status(thm)],[f674,f675]) ).
fof(f703,plain,
( ~ sQ21_spl
| $false ),
inference(resolution,[status(thm)],[f679,f194]) ).
fof(f709,plain,
~ sQ21_spl,
inference(contradiction_clause,[status(thm)],[f703]) ).
fof(f734,plain,
! [X0,X1,X2,X3] :
( X3 = X1
| X3 = X0
| sK0_skl(difference(unordered_pair(X0,X1),X2),singleton(X3)) = X3 ),
inference(resolution,[status(thm)],[f588,f62]) ).
fof(f778,plain,
( ~ apply(sK16_skl,sK19_skl,sK14_skl(sK17_skl,sK16_skl,unordered_pair(sK18_skl,sK19_skl),sK19_skl))
| ~ upper_bound(sK19_skl,sK16_skl,unordered_pair(sK18_skl,sK19_skl))
| ~ member(sK19_skl,unordered_pair(sK18_skl,sK19_skl)) ),
inference(resolution,[status(thm)],[f159,f176]) ).
fof(f780,definition,
( sQ24_spl
<=> apply(sK16_skl,sK19_skl,sK14_skl(sK17_skl,sK16_skl,unordered_pair(sK18_skl,sK19_skl),sK19_skl)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f782,plain,
( sQ24_spl
| ~ apply(sK16_skl,sK19_skl,sK14_skl(sK17_skl,sK16_skl,unordered_pair(sK18_skl,sK19_skl),sK19_skl)) ),
inference(component_clause,[status(thm)],[f780]) ).
fof(f783,plain,
( ~ sQ24_spl
| ~ sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f778,f634,f637,f780]) ).
fof(f785,plain,
( sQ18_spl
| ~ apply(sK16_skl,sK8_skl(sK19_skl,unordered_pair(sK18_skl,sK19_skl),sK16_skl),sK19_skl) ),
inference(resolution,[status(thm)],[f639,f108]) ).
fof(f786,plain,
( sQ18_spl
| member(sK8_skl(sK19_skl,unordered_pair(sK18_skl,sK19_skl),sK16_skl),unordered_pair(sK18_skl,sK19_skl)) ),
inference(resolution,[status(thm)],[f639,f107]) ).
fof(f813,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f636,f196]) ).
fof(f814,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f813]) ).
fof(f825,plain,
! [X0,X1] :
( sK18_skl = X1
| sK18_skl = X0
| sK18_skl = sK18_skl ),
inference(paramodulation,[status(thm)],[f615,f734]) ).
fof(f834,definition,
( sQ29_spl
<=> sK18_skl = sK18_skl ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f837,definition,
! [X0] :
( sQ30_spl
<=> sK18_skl = X0 ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f838,plain,
! [X0] :
( ~ sQ30_spl
| sK18_skl = X0 ),
inference(component_clause,[status(thm)],[f837]) ).
fof(f840,plain,
( sQ30_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f825,f834,f837]) ).
fof(f861,plain,
( sQ18_spl
| sK8_skl(sK19_skl,unordered_pair(sK18_skl,sK19_skl),sK16_skl) = sK19_skl
| sK8_skl(sK19_skl,unordered_pair(sK18_skl,sK19_skl),sK16_skl) = sK18_skl ),
inference(resolution,[status(thm)],[f786,f62]) ).
fof(f865,definition,
( sQ33_spl
<=> sK8_skl(sK19_skl,unordered_pair(sK18_skl,sK19_skl),sK16_skl) = sK18_skl ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f866,plain,
( ~ sQ33_spl
| sK8_skl(sK19_skl,unordered_pair(sK18_skl,sK19_skl),sK16_skl) = sK18_skl ),
inference(component_clause,[status(thm)],[f865]) ).
fof(f867,plain,
( sQ33_spl
| sK8_skl(sK19_skl,unordered_pair(sK18_skl,sK19_skl),sK16_skl) != sK18_skl ),
inference(component_clause,[status(thm)],[f865]) ).
fof(f868,definition,
( sQ34_spl
<=> sK8_skl(sK19_skl,unordered_pair(sK18_skl,sK19_skl),sK16_skl) = sK19_skl ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f869,plain,
( ~ sQ34_spl
| sK8_skl(sK19_skl,unordered_pair(sK18_skl,sK19_skl),sK16_skl) = sK19_skl ),
inference(component_clause,[status(thm)],[f868]) ).
fof(f871,plain,
( sQ18_spl
| sQ34_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f861,f865,f868,f637]) ).
fof(f898,definition,
( sQ35_spl
<=> member(sK19_skl,unordered_pair(sK19_skl,sK19_skl)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f900,plain,
( sQ35_spl
| ~ member(sK19_skl,unordered_pair(sK19_skl,sK19_skl)) ),
inference(component_clause,[status(thm)],[f898]) ).
fof(f912,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f900,f196]) ).
fof(f913,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f912]) ).
fof(f914,plain,
( sQ33_spl
| ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f867,f838]) ).
fof(f915,plain,
( sQ33_spl
| ~ sQ30_spl ),
inference(contradiction_clause,[status(thm)],[f914]) ).
fof(f1010,plain,
! [X0] :
( sQ24_spl
| ~ member(sK19_skl,X0)
| ~ upper_bound(sK14_skl(sK17_skl,sK16_skl,unordered_pair(sK18_skl,sK19_skl),sK19_skl),sK16_skl,X0) ),
inference(resolution,[status(thm)],[f782,f106]) ).
fof(f1020,plain,
( sQ18_spl
| ~ sQ33_spl
| ~ apply(sK16_skl,sK18_skl,sK19_skl) ),
inference(forward_demodulation,[status(thm)],[f866,f785]) ).
fof(f1021,plain,
( sQ18_spl
| ~ sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1020,f175]) ).
fof(f1022,plain,
( sQ18_spl
| ~ sQ33_spl ),
inference(contradiction_clause,[status(thm)],[f1021]) ).
fof(f1024,plain,
( sQ18_spl
| ~ sQ34_spl
| ~ apply(sK16_skl,sK19_skl,sK19_skl) ),
inference(backward_demodulation,[status(thm)],[f869,f785]) ).
fof(f1061,plain,
! [X0] :
( sQ18_spl
| ~ sQ34_spl
| ~ member(sK19_skl,X0)
| ~ sP1_prd(sK19_skl,X0,sK16_skl) ),
inference(resolution,[status(thm)],[f1024,f191]) ).
fof(f1071,definition,
( sQ48_spl
<=> apply(sK16_skl,sK19_skl,sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1073,plain,
( sQ48_spl
| ~ apply(sK16_skl,sK19_skl,sK19_skl) ),
inference(component_clause,[status(thm)],[f1071]) ).
fof(f1104,plain,
! [X0] :
( sQ18_spl
| ~ sQ34_spl
| ~ sP0_prd(X0,sK16_skl)
| ~ member(sK19_skl,X0) ),
inference(resolution,[status(thm)],[f1061,f182]) ).
fof(f1105,definition,
! [X0] :
( sQ49_spl
<=> ~ member(sK19_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1106,plain,
! [X0] :
( ~ sQ49_spl
| ~ member(sK19_skl,X0) ),
inference(component_clause,[status(thm)],[f1105]) ).
fof(f1109,plain,
( ~ sQ49_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f174,f1106]) ).
fof(f1110,plain,
~ sQ49_spl,
inference(contradiction_clause,[status(thm)],[f1109]) ).
fof(f1126,plain,
! [X0] :
( sQ18_spl
| ~ sQ34_spl
| ~ order(sK16_skl,X0)
| ~ member(sK19_skl,X0) ),
inference(resolution,[status(thm)],[f1104,f84]) ).
fof(f1127,plain,
( sQ18_spl
| ~ sQ34_spl
| ~ member(sK19_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f1126,f172]) ).
fof(f1133,plain,
( sQ18_spl
| ~ sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1127,f174]) ).
fof(f1134,plain,
( sQ18_spl
| ~ sQ34_spl ),
inference(contradiction_clause,[status(thm)],[f1133]) ).
fof(f1242,plain,
( sK1_skl(unordered_pair(sK17_skl,singleton(sK19_skl)),sK19_skl) = singleton(sK19_skl)
| sK17_skl = singleton(sK19_skl)
| sK1_skl(unordered_pair(sK17_skl,singleton(sK19_skl)),sK19_skl) = sK17_skl ),
inference(paramodulation,[status(thm)],[f372,f363]) ).
fof(f1247,definition,
( sQ51_spl
<=> sK1_skl(unordered_pair(sK17_skl,singleton(sK19_skl)),sK19_skl) = sK17_skl ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1248,plain,
( ~ sQ51_spl
| sK1_skl(unordered_pair(sK17_skl,singleton(sK19_skl)),sK19_skl) = sK17_skl ),
inference(component_clause,[status(thm)],[f1247]) ).
fof(f1250,definition,
( sQ52_spl
<=> sK17_skl = singleton(sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1251,plain,
( ~ sQ52_spl
| sK17_skl = singleton(sK19_skl) ),
inference(component_clause,[status(thm)],[f1250]) ).
fof(f1253,definition,
( sQ53_spl
<=> sK1_skl(unordered_pair(sK17_skl,singleton(sK19_skl)),sK19_skl) = singleton(sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1254,plain,
( ~ sQ53_spl
| sK1_skl(unordered_pair(sK17_skl,singleton(sK19_skl)),sK19_skl) = singleton(sK19_skl) ),
inference(component_clause,[status(thm)],[f1253]) ).
fof(f1256,plain,
( sQ53_spl
| sQ52_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1242,f1247,f1250,f1253]) ).
fof(f1341,plain,
( ~ sQ53_spl
| sK1_skl(unordered_pair(sK17_skl,singleton(sK19_skl)),sK19_skl) = sK17_skl
| singleton(sK19_skl) = singleton(sK19_skl) ),
inference(paramodulation,[status(thm)],[f363,f1254]) ).
fof(f1344,plain,
! [X0] :
( ~ sQ53_spl
| member(singleton(sK19_skl),unordered_pair(sK17_skl,singleton(sK19_skl)))
| ~ member(sK19_skl,X0)
| ~ member(X0,unordered_pair(sK17_skl,singleton(sK19_skl))) ),
inference(paramodulation,[status(thm)],[f1254,f219]) ).
fof(f1347,definition,
( sQ54_spl
<=> singleton(sK19_skl) = singleton(sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1350,plain,
( ~ sQ53_spl
| sQ51_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f1341,f1347,f1247,f1253]) ).
fof(f1353,definition,
! [X0] :
( sQ55_spl
<=> ( ~ member(sK19_skl,X0)
| ~ member(X0,unordered_pair(sK17_skl,singleton(sK19_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1354,plain,
! [X0] :
( ~ sQ55_spl
| ~ member(sK19_skl,X0)
| ~ member(X0,unordered_pair(sK17_skl,singleton(sK19_skl))) ),
inference(component_clause,[status(thm)],[f1353]) ).
fof(f1356,definition,
( sQ56_spl
<=> member(singleton(sK19_skl),unordered_pair(sK17_skl,singleton(sK19_skl))) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1359,plain,
( ~ sQ53_spl
| sQ56_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1344,f1353,f1356,f1253]) ).
fof(f1360,definition,
( sQ57_spl
<=> member(sK19_skl,sum(unordered_pair(sK17_skl,singleton(sK19_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1362,plain,
( sQ57_spl
| ~ member(sK19_skl,sum(unordered_pair(sK17_skl,singleton(sK19_skl)))) ),
inference(component_clause,[status(thm)],[f1360]) ).
fof(f1364,plain,
( ~ sQ51_spl
| sK1_skl(unordered_pair(sK17_skl,singleton(sK19_skl)),sK19_skl) = singleton(sK19_skl)
| sK17_skl = sK17_skl ),
inference(paramodulation,[status(thm)],[f372,f1248]) ).
fof(f1368,plain,
! [X0] :
( ~ sQ51_spl
| member(sK17_skl,unordered_pair(sK17_skl,singleton(sK19_skl)))
| ~ member(sK19_skl,X0)
| ~ member(X0,unordered_pair(sK17_skl,singleton(sK19_skl))) ),
inference(paramodulation,[status(thm)],[f1248,f219]) ).
fof(f1369,plain,
( ~ sQ51_spl
| member(sK19_skl,sK17_skl)
| ~ member(sK19_skl,sum(unordered_pair(sK17_skl,singleton(sK19_skl)))) ),
inference(paramodulation,[status(thm)],[f1248,f69]) ).
fof(f1370,plain,
( ~ sQ51_spl
| sQ53_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1364,f403,f1253,f1247]) ).
fof(f1374,definition,
( sQ58_spl
<=> member(sK17_skl,unordered_pair(sK17_skl,singleton(sK19_skl))) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1377,plain,
( ~ sQ51_spl
| sQ58_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1368,f1353,f1374,f1247]) ).
fof(f1378,plain,
( ~ sQ51_spl
| sQ1_spl
| ~ sQ57_spl ),
inference(split_clause,[status(thm)],[f1369,f1360,f394,f1247]) ).
fof(f1381,plain,
! [X0] :
( ~ sQ55_spl
| ~ sQ52_spl
| ~ member(sK19_skl,X0)
| ~ member(X0,unordered_pair(sK17_skl,sK17_skl)) ),
inference(backward_demodulation,[status(thm)],[f1251,f1354]) ).
fof(f1384,plain,
( ~ sQ55_spl
| ~ sQ52_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f1381,f411,f1250,f1353]) ).
fof(f1456,plain,
! [X0] :
( sQ57_spl
| ~ member(sK19_skl,X0)
| ~ member(X0,unordered_pair(sK17_skl,singleton(sK19_skl))) ),
inference(resolution,[status(thm)],[f1362,f70]) ).
fof(f1466,plain,
( sQ57_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1456,f1353,f1360]) ).
fof(f1707,plain,
! [X0] :
( sQ11_spl
| ~ member(sK18_skl,X0)
| ~ member(X0,unordered_pair(sK17_skl,sK17_skl)) ),
inference(resolution,[status(thm)],[f483,f70]) ).
fof(f1761,plain,
( sQ11_spl
| ~ member(sK18_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f1707,f196]) ).
fof(f1772,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1761,f173]) ).
fof(f1773,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f1772]) ).
fof(f1891,plain,
! [X0] :
( sQ48_spl
| ~ member(sK19_skl,X0)
| ~ sP1_prd(sK19_skl,X0,sK16_skl) ),
inference(resolution,[status(thm)],[f1073,f191]) ).
fof(f1910,plain,
! [X0] :
( sQ48_spl
| ~ sP0_prd(X0,sK16_skl)
| ~ member(sK19_skl,X0) ),
inference(resolution,[status(thm)],[f1891,f182]) ).
fof(f1915,plain,
! [X0] :
( sQ48_spl
| ~ order(sK16_skl,X0)
| ~ member(sK19_skl,X0) ),
inference(resolution,[status(thm)],[f1910,f84]) ).
fof(f1916,plain,
( sQ48_spl
| ~ member(sK19_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f1915,f172]) ).
fof(f1922,plain,
( sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1916,f174]) ).
fof(f1923,plain,
sQ48_spl,
inference(contradiction_clause,[status(thm)],[f1922]) ).
fof(f2085,plain,
( ~ sQ53_spl
| member(singleton(sK19_skl),unordered_pair(sK17_skl,singleton(sK19_skl)))
| sK0_skl(sum(unordered_pair(sK17_skl,singleton(sK19_skl))),singleton(sK19_skl)) = sK19_skl ),
inference(paramodulation,[status(thm)],[f1254,f586]) ).
fof(f2091,definition,
( sQ78_spl
<=> sK0_skl(sum(unordered_pair(sK17_skl,singleton(sK19_skl))),singleton(sK19_skl)) = sK19_skl ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f2094,plain,
( ~ sQ53_spl
| sQ56_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f2085,f2091,f1356,f1253]) ).
fof(f2111,plain,
( ~ sQ51_spl
| member(sK17_skl,unordered_pair(sK17_skl,singleton(sK19_skl)))
| sK0_skl(sum(unordered_pair(sK17_skl,singleton(sK19_skl))),singleton(sK19_skl)) = sK19_skl ),
inference(paramodulation,[status(thm)],[f1248,f586]) ).
fof(f2118,plain,
( ~ sQ51_spl
| sQ58_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f2111,f2091,f1374,f1247]) ).
fof(f2168,plain,
( sQ24_spl
| ~ upper_bound(sK19_skl,sK16_skl,unordered_pair(sK18_skl,sK19_skl))
| ~ member(sK19_skl,unordered_pair(sK18_skl,sK19_skl))
| least_upper_bound(sK19_skl,unordered_pair(sK18_skl,sK19_skl),sK16_skl,sK17_skl)
| ~ member(sK19_skl,unordered_pair(sK18_skl,sK19_skl)) ),
inference(resolution,[status(thm)],[f1010,f158]) ).
fof(f2172,definition,
( sQ81_spl
<=> least_upper_bound(sK19_skl,unordered_pair(sK18_skl,sK19_skl),sK16_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f2173,plain,
( ~ sQ81_spl
| least_upper_bound(sK19_skl,unordered_pair(sK18_skl,sK19_skl),sK16_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f2172]) ).
fof(f2175,plain,
( sQ24_spl
| ~ sQ18_spl
| sQ81_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f2168,f634,f2172,f637,f780]) ).
fof(f2176,plain,
( ~ sQ81_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2173,f176]) ).
fof(f2177,plain,
~ sQ81_spl,
inference(contradiction_clause,[status(thm)],[f2176]) ).
fof(f2178,plain,
$false,
inference(sat_refutation,[status(thm)],[f397,f409,f417,f421,f447,f475,f484,f499,f543,f556,f652,f709,f783,f814,f840,f871,f913,f915,f1022,f1110,f1134,f1256,f1350,f1359,f1370,f1377,f1378,f1384,f1466,f1773,f1923,f2094,f2118,f2175,f2177]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET795+4 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n008.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 05:39:24 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.15/0.38 % Drodi V4.1.1
% 13.41/2.18 % Refutation found
% 13.41/2.18 % SZS status Theorem for theBenchmark: Theorem is valid
% 13.41/2.18 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 13.41/2.23 % Elapsed time: 1.844606 seconds
% 13.41/2.23 % CPU time: 14.297814 seconds
% 13.41/2.23 % Total memory used: 231.353 MB
% 13.41/2.23 % Net memory used: 209.530 MB
%------------------------------------------------------------------------------