%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET801+4 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:39 PM UTC 2026
% Result : Theorem 42.77s 5.87s
% Output : CNFRefutation 42.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 110
% Syntax : Number of formulae : 603 ( 26 unt; 96 def)
% Number of atoms : 2091 ( 13 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 2602 (1114 ~;1192 |; 161 &)
% ( 119 <=>; 15 =>; 0 <=; 1 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 107 ( 105 usr; 95 prp; 0-4 aty)
% Number of functors : 24 ( 24 usr; 5 con; 0-4 aty)
% Number of variables : 1050 (1013 !; 37 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( subset(A,B)
<=> ! [X] :
( member(X,A)
=> member(X,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] :
( equal_set(A,B)
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,A,B] :
( member(X,intersection(A,B))
<=> ( member(X,B)
& member(X,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,A,B] :
( member(X,union(A,B))
<=> ( member(X,B)
| member(X,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] : ~ member(X,empty_set),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [B,A,E] :
( member(B,difference(E,A))
<=> ( ~ member(B,A)
& member(B,E) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,A] :
( member(X,sum(A))
<=> ? [Y] :
( member(X,Y)
& member(Y,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,A] :
( member(X,product(A))
<=> ! [Y] :
( member(Y,A)
=> member(X,Y) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [R,E] :
( total_order(R,E)
<=> ( ! [X,Y] :
( ( member(Y,E)
& member(X,E) )
=> ( apply(R,Y,X)
| apply(R,X,Y) ) )
& order(R,E) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [R,E,M] :
( greatest(M,R,E)
<=> ( ! [X] :
( member(X,E)
=> apply(R,X,M) )
& member(M,E) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f22,conjecture,
! [R,E] :
( order(R,E)
=> ! [X] :
( subset(X,E)
=> ! [M] :
( greatest(M,R,X)
<=> ( least_upper_bound(M,X,R,E)
& member(M,X) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
~ ! [R,E] :
( order(R,E)
=> ! [X] :
( subset(X,E)
=> ! [M] :
( greatest(M,R,X)
<=> ( least_upper_bound(M,X,R,E)
& member(M,X) ) ) ) ),
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(f30,plain,
! [X0,X1] :
( ~ member(sK0_skl(X1,X0),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f31,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| equal_set(A,B) )
& ( ( subset(B,A)
& subset(A,B) )
| ~ equal_set(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f2]) ).
fof(f32,plain,
( ! [A,B] :
( ~ subset(B,A)
| ~ subset(A,B)
| equal_set(A,B) )
& ! [A,B] :
( ( subset(B,A)
& subset(A,B) )
| ~ equal_set(A,B) ) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f33,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ equal_set(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f34,plain,
! [X0,X1] :
( subset(X1,X0)
| ~ equal_set(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f35,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| equal_set(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f40,plain,
! [X,A,B] :
( ( ~ member(X,B)
| ~ member(X,A)
| member(X,intersection(A,B)) )
& ( ( member(X,B)
& member(X,A) )
| ~ member(X,intersection(A,B)) ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f41,plain,
( ! [X,A,B] :
( ~ member(X,B)
| ~ member(X,A)
| member(X,intersection(A,B)) )
& ! [X,A,B] :
( ( member(X,B)
& member(X,A) )
| ~ member(X,intersection(A,B)) ) ),
inference(miniscoping,[status(thm)],[f40]) ).
fof(f42,plain,
! [X0,X1,X2] :
( member(X0,X1)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f43,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f44,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| ~ member(X0,X1)
| member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f45,plain,
! [X,A,B] :
( ( ( ~ member(X,B)
& ~ member(X,A) )
| member(X,union(A,B)) )
& ( member(X,B)
| member(X,A)
| ~ member(X,union(A,B)) ) ),
inference(NNF_transformation,[status(thm)],[f5]) ).
fof(f46,plain,
( ! [X,A,B] :
( ( ~ member(X,B)
& ~ member(X,A) )
| member(X,union(A,B)) )
& ! [X,A,B] :
( member(X,B)
| member(X,A)
| ~ member(X,union(A,B)) ) ),
inference(miniscoping,[status(thm)],[f45]) ).
fof(f47,plain,
! [X0,X1,X2] :
( member(X0,X2)
| member(X0,X1)
| ~ member(X0,union(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f48,plain,
! [X0,X1,X2] :
( ~ member(X0,X1)
| member(X0,union(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f49,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| member(X0,union(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
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(f55,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X0,X1)
| member(X0,difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
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(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(f85,plain,
! [X0,X1,X2,X3,X4] :
( apply(X0,X2,X4)
| ~ apply(X0,X3,X4)
| ~ apply(X0,X2,X3)
| ~ member(X4,X1)
| ~ member(X3,X1)
| ~ member(X2,X1)
| ~ order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f86,plain,
! [X0,X1] :
( member(sK3_skl(X1,X0),X1)
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f87,plain,
! [X0,X1] :
( member(sK4_skl(X1,X0),X1)
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f88,plain,
! [X0,X1] :
( member(sK5_skl(X1,X0),X1)
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f92,plain,
! [R,E] :
( total_order(R,E)
<=> ( ! [X,Y] :
( apply(R,Y,X)
| apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) )
& order(R,E) ) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f93,plain,
! [R,E] :
( ( ? [X,Y] :
( ~ apply(R,Y,X)
& ~ apply(R,X,Y)
& member(Y,E)
& member(X,E) )
| ~ order(R,E)
| total_order(R,E) )
& ( ( ! [X,Y] :
( apply(R,Y,X)
| apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) )
& order(R,E) )
| ~ total_order(R,E) ) ),
inference(NNF_transformation,[status(thm)],[f92]) ).
fof(f94,plain,
( ! [R,E] :
( ? [X,Y] :
( ~ apply(R,Y,X)
& ~ apply(R,X,Y)
& member(Y,E)
& member(X,E) )
| ~ order(R,E)
| total_order(R,E) )
& ! [R,E] :
( ( ! [X,Y] :
( apply(R,Y,X)
| apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) )
& order(R,E) )
| ~ total_order(R,E) ) ),
inference(miniscoping,[status(thm)],[f93]) ).
fof(f95,plain,
( ! [R,E] :
( ( ~ apply(R,sK7_skl(E,R),sK6_skl(E,R))
& ~ apply(R,sK6_skl(E,R),sK7_skl(E,R))
& member(sK7_skl(E,R),E)
& member(sK6_skl(E,R),E) )
| ~ order(R,E)
| total_order(R,E) )
& ! [R,E] :
( ( ! [X,Y] :
( apply(R,Y,X)
| apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) )
& order(R,E) )
| ~ total_order(R,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl]),skolemize(X,sK6_skl(E,R)),skolemize(Y,sK7_skl(E,R))],[f94]) ).
fof(f96,plain,
! [X0,X1] :
( order(X0,X1)
| ~ total_order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f97,plain,
! [X0,X1,X2,X3] :
( apply(X0,X3,X2)
| apply(X0,X2,X3)
| ~ member(X3,X1)
| ~ member(X2,X1)
| ~ total_order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f98,plain,
! [X0,X1] :
( member(sK6_skl(X1,X0),X1)
| ~ order(X0,X1)
| total_order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f99,plain,
! [X0,X1] :
( member(sK7_skl(X1,X0),X1)
| ~ order(X0,X1)
| total_order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f100,plain,
! [X0,X1] :
( ~ apply(X0,sK6_skl(X1,X0),sK7_skl(X1,X0))
| ~ order(X0,X1)
| total_order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f101,plain,
! [X0,X1] :
( ~ apply(X0,sK7_skl(X1,X0),sK6_skl(X1,X0))
| ~ order(X0,X1)
| total_order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
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(f116,plain,
! [R,E,M] :
( greatest(M,R,E)
<=> ( ! [X] :
( apply(R,X,M)
| ~ member(X,E) )
& member(M,E) ) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f117,plain,
! [R,E,M] :
( ( ? [X] :
( ~ apply(R,X,M)
& member(X,E) )
| ~ member(M,E)
| greatest(M,R,E) )
& ( ( ! [X] :
( apply(R,X,M)
| ~ member(X,E) )
& member(M,E) )
| ~ greatest(M,R,E) ) ),
inference(NNF_transformation,[status(thm)],[f116]) ).
fof(f118,plain,
( ! [R,E,M] :
( ? [X] :
( ~ apply(R,X,M)
& member(X,E) )
| ~ member(M,E)
| greatest(M,R,E) )
& ! [R,E,M] :
( ( ! [X] :
( apply(R,X,M)
| ~ member(X,E) )
& member(M,E) )
| ~ greatest(M,R,E) ) ),
inference(miniscoping,[status(thm)],[f117]) ).
fof(f119,plain,
( ! [R,E,M] :
( ( ~ apply(R,sK10_skl(M,E,R),M)
& member(sK10_skl(M,E,R),E) )
| ~ member(M,E)
| greatest(M,R,E) )
& ! [R,E,M] :
( ( ! [X] :
( apply(R,X,M)
| ~ member(X,E) )
& member(M,E) )
| ~ greatest(M,R,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X,sK10_skl(M,E,R))],[f118]) ).
fof(f120,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ greatest(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f121,plain,
! [X0,X1,X2,X3] :
( apply(X1,X3,X0)
| ~ member(X3,X2)
| ~ greatest(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f122,plain,
! [X0,X1,X2] :
( member(sK10_skl(X0,X2,X1),X2)
| ~ member(X0,X2)
| greatest(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f123,plain,
! [X0,X1,X2] :
( ~ apply(X1,sK10_skl(X0,X2,X1),X0)
| ~ member(X0,X2)
| greatest(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
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(f154,plain,
! [X0,X1,X2,X3] :
( member(X0,X1)
| ~ least_upper_bound(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f155,plain,
! [X0,X1,X2,X3] :
( upper_bound(X0,X2,X1)
| ~ least_upper_bound(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f156,plain,
! [X0,X1,X2,X3,X4] :
( apply(X2,X0,X4)
| ~ upper_bound(X4,X2,X1)
| ~ member(X4,X3)
| ~ least_upper_bound(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f157,plain,
! [X0,X1,X2,X3] :
( member(sK14_skl(X3,X2,X1,X0),X3)
| ~ upper_bound(X0,X2,X1)
| ~ member(X0,X1)
| least_upper_bound(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f153]) ).
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] :
( ? [X] :
( ? [M] :
( greatest(M,R,X)
<~> ( least_upper_bound(M,X,R,E)
& member(M,X) ) )
& subset(X,E) )
& order(R,E) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f171,plain,
? [R,E] :
( ? [X] :
( ? [M] :
( ( ~ least_upper_bound(M,X,R,E)
| ~ member(M,X)
| ~ greatest(M,R,X) )
& ( ( least_upper_bound(M,X,R,E)
& member(M,X) )
| greatest(M,R,X) ) )
& subset(X,E) )
& order(R,E) ),
inference(NNF_transformation,[status(thm)],[f170]) ).
fof(f172,plain,
( ( ~ least_upper_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)
| ~ member(sK19_skl,sK18_skl)
| ~ greatest(sK19_skl,sK16_skl,sK18_skl) )
& ( ( least_upper_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)
& member(sK19_skl,sK18_skl) )
| greatest(sK19_skl,sK16_skl,sK18_skl) )
& subset(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(X,sK18_skl),skolemize(M,sK19_skl)],[f171]) ).
fof(f173,plain,
order(sK16_skl,sK17_skl),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f174,plain,
subset(sK18_skl,sK17_skl),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f175,plain,
( member(sK19_skl,sK18_skl)
| greatest(sK19_skl,sK16_skl,sK18_skl) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f176,plain,
( least_upper_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)
| greatest(sK19_skl,sK16_skl,sK18_skl) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f177,plain,
( ~ least_upper_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)
| ~ member(sK19_skl,sK18_skl)
| ~ greatest(sK19_skl,sK16_skl,sK18_skl) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f178,definition,
! [R,E,X] :
( sP1_prd(X,E,R)
<=> ( apply(R,X,X)
| ~ member(X,E) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f179,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,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) )
& ( ( ! [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)],[f179]) ).
fof(f181,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)],[f180]) ).
fof(f182,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))],[f181]) ).
fof(f184,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ apply(X1,X3,X2)
| ~ apply(X1,X2,X3)
| ~ member(X3,X0)
| ~ member(X2,X0)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f186,plain,
! [X0,X1] :
( member(sK22_skl(X0,X1),X0)
| ~ sP1_prd(sK20_skl(X0,X1),X0,X1)
| sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f190,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)],[f178]) ).
fof(f191,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)],[f190]) ).
fof(f192,plain,
! [X0,X1,X2] :
( apply(X2,X0,X0)
| ~ member(X0,X1)
| ~ sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f193,plain,
! [X0,X1,X2] :
( member(X0,X1)
| sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f194,plain,
! [X0,X1,X2] :
( ~ apply(X2,X0,X0)
| sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f195,definition,
( sQ0_spl
<=> greatest(sK19_skl,sK16_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f196,plain,
( ~ sQ0_spl
| greatest(sK19_skl,sK16_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f195]) ).
fof(f197,plain,
( sQ0_spl
| ~ greatest(sK19_skl,sK16_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f195]) ).
fof(f198,definition,
( sQ1_spl
<=> member(sK19_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f199,plain,
( ~ sQ1_spl
| member(sK19_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f198]) ).
fof(f200,plain,
( sQ1_spl
| ~ member(sK19_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f198]) ).
fof(f201,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f175,f195,f198]) ).
fof(f202,definition,
( sQ2_spl
<=> least_upper_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f203,plain,
( ~ sQ2_spl
| least_upper_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f202]) ).
fof(f204,plain,
( sQ2_spl
| ~ least_upper_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f202]) ).
fof(f205,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f176,f195,f202]) ).
fof(f206,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f177,f195,f198,f202]) ).
fof(f210,plain,
sP0_prd(sK17_skl,sK16_skl),
inference(resolution,[status(thm)],[f84,f173]) ).
fof(f213,plain,
! [X0,X1,X2] :
( member(sK0_skl(X1,X0),X2)
| ~ subset(X0,X2)
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f29,f28]) ).
fof(f214,plain,
! [X0] :
( subset(X0,X0)
| subset(X0,X0) ),
inference(resolution,[status(thm)],[f30,f29]) ).
fof(f215,plain,
! [X0] : subset(X0,X0),
inference(duplicate_literals_removal,[status(thm)],[f214]) ).
fof(f216,plain,
( ~ sQ0_spl
| member(sK19_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f120,f196]) ).
fof(f217,plain,
( ~ sQ0_spl
| sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f216,f200]) ).
fof(f218,plain,
( ~ sQ0_spl
| sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f217]) ).
fof(f219,plain,
! [X0] :
( ~ sQ1_spl
| member(sK19_skl,X0)
| ~ subset(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f199,f28]) ).
fof(f221,plain,
( ~ subset(sK17_skl,sK18_skl)
| equal_set(sK17_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f35,f174]) ).
fof(f223,definition,
( sQ3_spl
<=> equal_set(sK17_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f224,plain,
( ~ sQ3_spl
| equal_set(sK17_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f223]) ).
fof(f226,definition,
( sQ4_spl
<=> subset(sK17_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f228,plain,
( sQ4_spl
| ~ subset(sK17_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f226]) ).
fof(f229,plain,
( ~ sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f221,f223,f226]) ).
fof(f236,plain,
( ~ sQ3_spl
| subset(sK17_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f224,f33]) ).
fof(f238,plain,
( ~ sQ3_spl
| ~ subset(sK18_skl,sK17_skl)
| equal_set(sK18_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f236,f35]) ).
fof(f239,definition,
( sQ5_spl
<=> equal_set(sK18_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f240,plain,
( ~ sQ5_spl
| equal_set(sK18_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f239]) ).
fof(f242,definition,
( sQ6_spl
<=> subset(sK18_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f244,plain,
( sQ6_spl
| ~ subset(sK18_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f242]) ).
fof(f245,plain,
( ~ sQ3_spl
| ~ sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f238,f239,f242,f223]) ).
fof(f246,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f244,f174]) ).
fof(f247,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f246]) ).
fof(f248,plain,
( ~ sQ2_spl
| upper_bound(sK19_skl,sK16_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f155,f203]) ).
fof(f249,plain,
! [X0] :
( ~ sQ2_spl
| apply(sK16_skl,sK19_skl,X0)
| ~ upper_bound(X0,sK16_skl,sK18_skl)
| ~ member(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f156,f203]) ).
fof(f252,plain,
( ~ sQ5_spl
| subset(sK17_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f240,f34]) ).
fof(f254,plain,
( ~ sQ5_spl
| sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f252,f228]) ).
fof(f255,plain,
( ~ sQ5_spl
| sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f254]) ).
fof(f258,plain,
! [X0,X1,X2] :
( subset(intersection(X1,X2),X0)
| member(sK0_skl(X0,intersection(X1,X2)),X1) ),
inference(resolution,[status(thm)],[f42,f29]) ).
fof(f259,plain,
! [X0,X1,X2] :
( subset(intersection(X1,X2),X0)
| member(sK0_skl(X0,intersection(X1,X2)),X2) ),
inference(resolution,[status(thm)],[f43,f29]) ).
fof(f263,plain,
! [X0,X1,X2,X3] :
( member(X0,X3)
| ~ subset(intersection(X1,X2),X3)
| ~ member(X0,X2)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f44,f28]) ).
fof(f264,plain,
( ~ sQ1_spl
| member(sK19_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f219,f174]) ).
fof(f273,plain,
! [X0,X1] :
( ~ subset(X0,empty_set)
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f213,f50]) ).
fof(f274,plain,
! [X0,X1,X2,X3] :
( member(sK0_skl(X1,X0),X3)
| ~ subset(X2,X3)
| ~ subset(X0,X2)
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f213,f28]) ).
fof(f275,plain,
! [X0] :
( ~ sQ1_spl
| member(sK19_skl,X0)
| ~ subset(sK17_skl,X0) ),
inference(resolution,[status(thm)],[f264,f28]) ).
fof(f278,plain,
! [X0,X1,X2] :
( subset(X2,union(X0,X1))
| ~ member(sK0_skl(union(X0,X1),X2),X0) ),
inference(resolution,[status(thm)],[f48,f30]) ).
fof(f281,plain,
! [X0,X1,X2] :
( subset(X2,union(X0,X1))
| ~ member(sK0_skl(union(X0,X1),X2),X1) ),
inference(resolution,[status(thm)],[f49,f30]) ).
fof(f285,definition,
( sQ7_spl
<=> member(sK19_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f288,definition,
( sQ8_spl
<=> apply(sK16_skl,sK19_skl,sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f289,plain,
( ~ sQ8_spl
| apply(sK16_skl,sK19_skl,sK19_skl) ),
inference(component_clause,[status(thm)],[f288]) ).
fof(f292,plain,
! [X0] :
( ~ sQ0_spl
| apply(sK16_skl,X0,sK19_skl)
| ~ member(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f196,f121]) ).
fof(f294,plain,
! [X0] : subset(empty_set,X0),
inference(resolution,[status(thm)],[f273,f215]) ).
fof(f298,plain,
! [X0,X1,X2] :
( subset(difference(X1,X2),X0)
| member(sK0_skl(X0,difference(X1,X2)),X1) ),
inference(resolution,[status(thm)],[f53,f29]) ).
fof(f300,plain,
! [X0,X1,X2] :
( subset(difference(X1,X2),X0)
| ~ member(sK0_skl(X0,difference(X1,X2)),X2) ),
inference(resolution,[status(thm)],[f54,f29]) ).
fof(f304,plain,
! [X0,X1,X2,X3] :
( member(X0,X3)
| ~ subset(difference(X1,X2),X3)
| member(X0,X2)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f55,f28]) ).
fof(f319,definition,
! [X0] :
( sQ10_spl
<=> sP1_prd(sK19_skl,X0,sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f320,plain,
! [X0] :
( ~ sQ10_spl
| sP1_prd(sK19_skl,X0,sK16_skl) ),
inference(component_clause,[status(thm)],[f319]) ).
fof(f338,plain,
! [X0] :
( ~ sQ10_spl
| apply(sK16_skl,sK19_skl,sK19_skl)
| ~ member(sK19_skl,X0) ),
inference(resolution,[status(thm)],[f192,f320]) ).
fof(f339,definition,
! [X0] :
( sQ11_spl
<=> ~ member(sK19_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f340,plain,
! [X0] :
( ~ sQ11_spl
| ~ member(sK19_skl,X0) ),
inference(component_clause,[status(thm)],[f339]) ).
fof(f342,plain,
( ~ sQ10_spl
| sQ8_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f338,f339,f288,f319]) ).
fof(f352,plain,
! [X0,X1,X2] :
( member(sK1_skl(X1,X0),X2)
| ~ subset(X1,X2)
| ~ member(X0,sum(X1)) ),
inference(resolution,[status(thm)],[f68,f28]) ).
fof(f371,plain,
! [X0,X1] :
( ~ subset(X1,empty_set)
| ~ member(X0,sum(X1)) ),
inference(resolution,[status(thm)],[f352,f50]) ).
fof(f377,plain,
! [X0,X1,X2] :
( ~ member(X2,X1)
| ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f371,f70]) ).
fof(f381,plain,
! [X0] :
( ~ sQ1_spl
| ~ member(X0,sK19_skl)
| ~ subset(sK17_skl,empty_set) ),
inference(resolution,[status(thm)],[f377,f264]) ).
fof(f382,plain,
! [X0] :
( ~ sQ1_spl
| ~ member(X0,sK19_skl)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f377,f199]) ).
fof(f406,plain,
! [X0,X1,X2,X3] :
( ~ subset(X2,X1)
| subset(X2,X3)
| ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f377,f213]) ).
fof(f407,plain,
! [X0,X1,X2] :
( subset(X1,X2)
| ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f377,f29]) ).
fof(f419,definition,
( sQ13_spl
<=> subset(sK17_skl,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f422,definition,
! [X0] :
( sQ14_spl
<=> ~ member(X0,sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f423,plain,
! [X0] :
( ~ sQ14_spl
| ~ member(X0,sK19_skl) ),
inference(component_clause,[status(thm)],[f422]) ).
fof(f425,plain,
( ~ sQ1_spl
| sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f381,f419,f422,f198]) ).
fof(f426,definition,
( sQ15_spl
<=> subset(sK18_skl,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f429,plain,
( ~ sQ1_spl
| sQ14_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f382,f426,f422,f198]) ).
fof(f434,plain,
! [X0,X1] :
( ~ sQ14_spl
| ~ subset(X1,sK19_skl)
| ~ member(X0,sum(X1)) ),
inference(resolution,[status(thm)],[f423,f352]) ).
fof(f442,plain,
! [X0] :
( ~ sQ2_spl
| apply(sK16_skl,X0,sK19_skl)
| ~ member(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f248,f106]) ).
fof(f456,plain,
! [X0,X1,X2] :
( member(sK2_skl(intersection(X1,X2),X0),X1)
| member(X0,product(intersection(X1,X2))) ),
inference(resolution,[status(thm)],[f76,f42]) ).
fof(f458,plain,
! [X0] : member(X0,product(empty_set)),
inference(resolution,[status(thm)],[f76,f50]) ).
fof(f461,plain,
! [X0,X1,X2] :
( member(sK2_skl(X1,X0),X2)
| ~ subset(X1,X2)
| member(X0,product(X1)) ),
inference(resolution,[status(thm)],[f76,f28]) ).
fof(f488,plain,
! [X0,X1,X2] :
( ~ sQ14_spl
| ~ member(X2,X1)
| ~ member(X1,X0)
| ~ subset(X0,sK19_skl) ),
inference(resolution,[status(thm)],[f434,f70]) ).
fof(f493,plain,
! [X0] :
( ~ sQ14_spl
| ~ sP0_prd(sK19_skl,X0)
| order(X0,sK19_skl) ),
inference(resolution,[status(thm)],[f86,f423]) ).
fof(f507,plain,
! [X0,X1,X2] :
( member(sK3_skl(X1,X0),X2)
| ~ subset(X1,X2)
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f86,f28]) ).
fof(f553,plain,
! [X0,X1] :
( ~ subset(X1,empty_set)
| member(X0,product(X1)) ),
inference(resolution,[status(thm)],[f461,f50]) ).
fof(f576,plain,
! [X0,X1,X2,X3] :
( ~ member(X2,X3)
| ~ subset(X3,empty_set)
| ~ subset(X1,X2)
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f507,f377]) ).
fof(f621,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ subset(X0,sK19_skl)
| subset(X0,X1)
| ~ subset(sK17_skl,empty_set) ),
inference(resolution,[status(thm)],[f406,f264]) ).
fof(f622,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ subset(X0,sK19_skl)
| subset(X0,X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f406,f199]) ).
fof(f635,definition,
! [X0,X1] :
( sQ17_spl
<=> ( ~ subset(X0,sK19_skl)
| subset(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f636,plain,
! [X0,X1] :
( ~ sQ17_spl
| ~ subset(X0,sK19_skl)
| subset(X0,X1) ),
inference(component_clause,[status(thm)],[f635]) ).
fof(f638,plain,
( ~ sQ1_spl
| sQ17_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f621,f419,f635,f198]) ).
fof(f639,plain,
( ~ sQ1_spl
| sQ17_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f622,f426,f635,f198]) ).
fof(f730,plain,
! [X0,X1,X2] :
( ~ member(X1,X2)
| ~ subset(X2,empty_set)
| ~ order(X0,X1)
| total_order(X0,X1) ),
inference(resolution,[status(thm)],[f98,f377]) ).
fof(f732,plain,
! [X0,X1,X2] :
( member(sK6_skl(X1,X0),X2)
| ~ subset(X1,X2)
| ~ order(X0,X1)
| total_order(X0,X1) ),
inference(resolution,[status(thm)],[f98,f28]) ).
fof(f749,plain,
! [X0,X1,X2] :
( member(sK7_skl(X1,X0),X2)
| ~ subset(X1,X2)
| ~ order(X0,X1)
| total_order(X0,X1) ),
inference(resolution,[status(thm)],[f99,f28]) ).
fof(f750,plain,
! [X0] :
( ~ member(sK17_skl,X0)
| ~ subset(X0,empty_set)
| total_order(sK16_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f730,f173]) ).
fof(f751,definition,
( sQ19_spl
<=> total_order(sK16_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f752,plain,
( ~ sQ19_spl
| total_order(sK16_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f751]) ).
fof(f754,definition,
! [X0] :
( sQ20_spl
<=> ( ~ member(sK17_skl,X0)
| ~ subset(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f757,plain,
( sQ20_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f750,f751,f754]) ).
fof(f766,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ member(sK18_skl,X1)
| ~ subset(X1,empty_set)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f576,f252]) ).
fof(f810,definition,
! [X0] :
( sQ24_spl
<=> ( ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f813,definition,
! [X1] :
( sQ25_spl
<=> ( ~ member(sK18_skl,X1)
| ~ subset(X1,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f816,plain,
( ~ sQ5_spl
| sQ25_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f766,f810,f813,f239]) ).
fof(f827,plain,
! [X0,X1,X2] :
( apply(X0,sK7_skl(X1,X0),sK6_skl(X1,X0))
| ~ member(sK6_skl(X1,X0),X2)
| ~ member(sK7_skl(X1,X0),X2)
| ~ total_order(X0,X2)
| ~ order(X0,X1)
| total_order(X0,X1) ),
inference(resolution,[status(thm)],[f100,f97]) ).
fof(f845,plain,
! [X0,X1,X2,X3] :
( ~ member(X2,X3)
| ~ subset(X3,empty_set)
| upper_bound(X0,X1,X2) ),
inference(resolution,[status(thm)],[f107,f377]) ).
fof(f847,plain,
! [X0,X1,X2,X3] :
( member(sK8_skl(X0,X2,X1),X3)
| ~ subset(X2,X3)
| upper_bound(X0,X1,X2) ),
inference(resolution,[status(thm)],[f107,f28]) ).
fof(f874,plain,
! [X0,X1] :
( ~ subset(X1,empty_set)
| ~ order(X0,X1)
| total_order(X0,X1) ),
inference(resolution,[status(thm)],[f732,f50]) ).
fof(f889,plain,
( ~ subset(sK17_skl,empty_set)
| total_order(sK16_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f874,f173]) ).
fof(f890,plain,
( ~ sQ13_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f889,f751,f419]) ).
fof(f891,plain,
! [X0] :
( ~ sQ0_spl
| ~ member(sK8_skl(sK19_skl,X0,sK16_skl),sK18_skl)
| upper_bound(sK19_skl,sK16_skl,X0) ),
inference(resolution,[status(thm)],[f108,f292]) ).
fof(f954,plain,
! [X0,X1,X2] :
( ~ subset(X2,empty_set)
| upper_bound(X0,X1,X2) ),
inference(resolution,[status(thm)],[f847,f50]) ).
fof(f965,plain,
! [X0,X1,X2,X3] :
( apply(X2,X1,X3)
| ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f954,f106]) ).
fof(f976,plain,
! [X0,X1,X2,X3,X4,X5] :
( apply(X2,X4,X5)
| ~ apply(X2,X4,X1)
| ~ member(X5,X3)
| ~ member(X1,X3)
| ~ member(X4,X3)
| ~ order(X2,X3)
| ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f965,f85]) ).
fof(f995,plain,
! [X0,X1,X2,X3] :
( member(sK10_skl(X0,X2,X1),X3)
| ~ subset(X2,X3)
| ~ member(X0,X2)
| greatest(X0,X1,X2) ),
inference(resolution,[status(thm)],[f122,f28]) ).
fof(f1067,plain,
! [X0] :
( ~ sQ2_spl
| ~ member(sK19_skl,X0)
| greatest(sK19_skl,sK16_skl,X0)
| ~ member(sK10_skl(sK19_skl,X0,sK16_skl),sK18_skl) ),
inference(resolution,[status(thm)],[f442,f123]) ).
fof(f1076,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ member(sK18_skl,X1)
| ~ subset(X1,empty_set)
| apply(sK16_skl,sK19_skl,X0)
| ~ member(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f249,f845]) ).
fof(f1078,definition,
! [X0] :
( sQ30_spl
<=> ( apply(sK16_skl,sK19_skl,X0)
| ~ member(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1079,plain,
! [X0] :
( ~ sQ30_spl
| apply(sK16_skl,sK19_skl,X0)
| ~ member(X0,sK17_skl) ),
inference(component_clause,[status(thm)],[f1078]) ).
fof(f1086,plain,
( ~ sQ2_spl
| sQ25_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f1076,f1078,f813,f202]) ).
fof(f1129,plain,
! [X0,X1,X2] :
( ~ subset(X2,empty_set)
| ~ member(X0,X2)
| greatest(X0,X1,X2) ),
inference(resolution,[status(thm)],[f995,f50]) ).
fof(f1209,plain,
! [X0,X1,X2] :
( ~ sQ8_spl
| apply(sK16_skl,sK19_skl,X2)
| ~ member(X2,X1)
| ~ member(sK19_skl,X1)
| ~ member(sK19_skl,X1)
| ~ order(sK16_skl,X1)
| ~ member(sK19_skl,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f976,f289]) ).
fof(f1218,definition,
! [X0] :
( sQ32_spl
<=> ( ~ member(sK19_skl,X0)
| ~ subset(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f1221,definition,
! [X1,X2] :
( sQ33_spl
<=> ( apply(sK16_skl,sK19_skl,X2)
| ~ member(X2,X1)
| ~ member(sK19_skl,X1)
| ~ member(sK19_skl,X1)
| ~ order(sK16_skl,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f1224,plain,
( ~ sQ8_spl
| sQ33_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f1209,f1218,f1221,f288]) ).
fof(f1231,plain,
( ~ sQ1_spl
| ~ sQ11_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f264,f340]) ).
fof(f1243,plain,
( ~ sQ1_spl
| ~ sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f1231]) ).
fof(f1247,plain,
( sQ0_spl
| ~ subset(sK18_skl,empty_set)
| ~ member(sK19_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f197,f1129]) ).
fof(f1248,plain,
( sQ0_spl
| ~ sQ15_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f1247,f198,f426,f195]) ).
fof(f1274,plain,
! [X0,X1,X2,X3] :
( ~ subset(X3,empty_set)
| ~ upper_bound(X0,X2,X1)
| ~ member(X0,X1)
| least_upper_bound(X0,X1,X2,sum(X3)) ),
inference(resolution,[status(thm)],[f157,f371]) ).
fof(f1291,plain,
! [X0,X1,X2,X3,X4] :
( apply(X2,X4,sK14_skl(X3,X2,X1,X0))
| ~ member(X4,X1)
| ~ upper_bound(X0,X2,X1)
| ~ member(X0,X1)
| least_upper_bound(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f158,f106]) ).
fof(f1343,plain,
! [X0] :
( ~ sQ30_spl
| sP1_prd(sK19_skl,X0,sK16_skl)
| ~ member(sK19_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f1079,f194]) ).
fof(f1345,plain,
( ~ sQ30_spl
| sQ10_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f1343,f285,f319,f1078]) ).
fof(f1379,plain,
! [X0,X1,X2,X3] :
( upper_bound(X0,X2,X1)
| ~ subset(X3,empty_set)
| ~ upper_bound(X0,X2,X1)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f1274,f155]) ).
fof(f1380,plain,
! [X0,X1,X2,X3] :
( member(X0,X1)
| ~ subset(X3,empty_set)
| ~ upper_bound(X0,X2,X1)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f1274,f154]) ).
fof(f1381,definition,
! [X0,X1,X2] :
( sQ35_spl
<=> ( upper_bound(X0,X2,X1)
| ~ upper_bound(X0,X2,X1)
| ~ member(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f1384,definition,
! [X3] :
( sQ36_spl
<=> ~ subset(X3,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1385,plain,
! [X0] :
( ~ sQ36_spl
| ~ subset(X0,empty_set) ),
inference(component_clause,[status(thm)],[f1384]) ).
fof(f1387,plain,
( sQ36_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f1379,f1381,f1384]) ).
fof(f1388,definition,
! [X0,X1,X2] :
( sQ37_spl
<=> ( member(X0,X1)
| ~ upper_bound(X0,X2,X1)
| ~ member(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1391,plain,
( sQ36_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f1380,f1388,f1384]) ).
fof(f1419,plain,
( ~ sQ36_spl
| $false ),
inference(resolution,[status(thm)],[f1385,f294]) ).
fof(f1421,plain,
~ sQ36_spl,
inference(contradiction_clause,[status(thm)],[f1419]) ).
fof(f1615,plain,
! [X0,X1,X2] :
( ~ sP0_prd(X1,X2)
| order(X2,X1)
| ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f377,f87]) ).
fof(f1616,plain,
! [X0,X1,X2,X3] :
( ~ subset(X3,X1)
| ~ sP0_prd(X3,X2)
| order(X2,X3)
| ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f377,f507]) ).
fof(f1622,plain,
! [X0,X1,X2,X3] :
( ~ subset(X2,X1)
| subset(X2,X3)
| ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f377,f213]) ).
fof(f1640,plain,
! [X0] :
( ~ sQ8_spl
| sK19_skl = sK19_skl
| ~ apply(sK16_skl,sK19_skl,sK19_skl)
| ~ member(sK19_skl,X0)
| ~ member(sK19_skl,X0)
| ~ sP0_prd(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f184,f289]) ).
fof(f1649,definition,
! [X0] :
( sQ38_spl
<=> ( ~ member(sK19_skl,X0)
| ~ member(sK19_skl,X0)
| ~ sP0_prd(X0,sK16_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1650,plain,
! [X0] :
( ~ sQ38_spl
| ~ member(sK19_skl,X0)
| ~ member(sK19_skl,X0)
| ~ sP0_prd(X0,sK16_skl) ),
inference(component_clause,[status(thm)],[f1649]) ).
fof(f1652,definition,
( sQ39_spl
<=> sK19_skl = sK19_skl ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1655,plain,
( sQ39_spl
| ~ sQ8_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f1640,f1649,f288,f1652]) ).
fof(f1658,plain,
! [X0] :
( ~ sQ38_spl
| ~ member(sK19_skl,X0)
| ~ sP0_prd(X0,sK16_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f1650]) ).
fof(f1662,plain,
( ~ sQ1_spl
| ~ sQ38_spl
| ~ sP0_prd(sK17_skl,sK16_skl) ),
inference(resolution,[status(thm)],[f1658,f264]) ).
fof(f1673,plain,
( ~ sQ1_spl
| ~ sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1662,f210]) ).
fof(f1674,plain,
( ~ sQ1_spl
| ~ sQ38_spl ),
inference(contradiction_clause,[status(thm)],[f1673]) ).
fof(f1834,plain,
! [X0,X1] :
( member(sK22_skl(X0,X1),X0)
| sP0_prd(X0,X1)
| member(sK20_skl(X0,X1),X0) ),
inference(resolution,[status(thm)],[f193,f186]) ).
fof(f1863,plain,
! [X0,X1,X2] :
( subset(X0,X1)
| ~ subset(X2,X1)
| ~ subset(X0,X2)
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f274,f30]) ).
fof(f1884,plain,
! [X0,X1,X2] :
( ~ subset(X2,X1)
| ~ subset(X0,X2)
| subset(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f1863]) ).
fof(f1892,plain,
! [X0] :
( ~ sQ5_spl
| ~ subset(X0,sK17_skl)
| subset(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f1884,f252]) ).
fof(f1893,plain,
! [X0] :
( ~ subset(X0,sK18_skl)
| subset(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f1884,f174]) ).
fof(f1908,plain,
! [X0,X1] :
( subset(intersection(X0,X1),X0)
| subset(intersection(X0,X1),X0) ),
inference(resolution,[status(thm)],[f258,f30]) ).
fof(f1925,plain,
! [X0,X1] : subset(intersection(X0,X1),X0),
inference(duplicate_literals_removal,[status(thm)],[f1908]) ).
fof(f1926,plain,
! [X0,X1] :
( subset(intersection(X0,X1),X1)
| subset(intersection(X0,X1),X1) ),
inference(resolution,[status(thm)],[f259,f30]) ).
fof(f1943,plain,
! [X0,X1] : subset(intersection(X0,X1),X1),
inference(duplicate_literals_removal,[status(thm)],[f1926]) ).
fof(f1945,plain,
( ~ sQ2_spl
| ~ member(sK19_skl,sK18_skl)
| greatest(sK19_skl,sK16_skl,sK18_skl)
| ~ member(sK19_skl,sK18_skl)
| greatest(sK19_skl,sK16_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f1067,f122]) ).
fof(f1947,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1945,f195,f198,f202]) ).
fof(f1959,plain,
! [X0] : subset(intersection(sK18_skl,X0),sK17_skl),
inference(resolution,[status(thm)],[f1925,f1893]) ).
fof(f1960,plain,
! [X0] :
( ~ sQ5_spl
| subset(intersection(sK17_skl,X0),sK18_skl) ),
inference(resolution,[status(thm)],[f1925,f1892]) ).
fof(f1971,plain,
! [X0] :
( ~ sQ5_spl
| subset(intersection(X0,sK17_skl),sK18_skl) ),
inference(resolution,[status(thm)],[f1943,f1892]) ).
fof(f2031,plain,
! [X0,X1,X2] :
( ~ subset(X0,X1)
| subset(X0,union(X1,X2))
| subset(X0,union(X1,X2)) ),
inference(resolution,[status(thm)],[f278,f213]) ).
fof(f2032,plain,
! [X0,X1] :
( subset(X0,union(X0,X1))
| subset(X0,union(X0,X1)) ),
inference(resolution,[status(thm)],[f278,f29]) ).
fof(f2043,plain,
! [X0,X1,X2] :
( ~ subset(X0,X1)
| subset(X0,union(X1,X2)) ),
inference(duplicate_literals_removal,[status(thm)],[f2031]) ).
fof(f2044,plain,
! [X0,X1] : subset(X0,union(X0,X1)),
inference(duplicate_literals_removal,[status(thm)],[f2032]) ).
fof(f2045,plain,
! [X0,X1] :
( member(X0,sK17_skl)
| ~ member(X0,X1)
| ~ member(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f1959,f263]) ).
fof(f2050,plain,
( ~ sQ0_spl
| upper_bound(sK19_skl,sK16_skl,sK18_skl)
| upper_bound(sK19_skl,sK16_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f891,f107]) ).
fof(f2052,definition,
( sQ41_spl
<=> upper_bound(sK19_skl,sK16_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f2055,plain,
( ~ sQ0_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f2050,f2052,f195]) ).
fof(f2096,plain,
! [X0] :
( ~ sQ1_spl
| member(sK19_skl,union(sK18_skl,X0)) ),
inference(resolution,[status(thm)],[f2044,f219]) ).
fof(f2100,plain,
! [X0,X1] :
( ~ sQ5_spl
| member(X0,sK18_skl)
| ~ member(X0,X1)
| ~ member(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f1960,f263]) ).
fof(f2112,plain,
! [X0,X1,X2] :
( ~ subset(X0,X2)
| subset(X0,union(X1,X2))
| subset(X0,union(X1,X2)) ),
inference(resolution,[status(thm)],[f281,f213]) ).
fof(f2113,plain,
! [X0,X1] :
( subset(X0,union(X1,X0))
| subset(X0,union(X1,X0)) ),
inference(resolution,[status(thm)],[f281,f29]) ).
fof(f2124,plain,
! [X0,X1,X2] :
( ~ subset(X0,X2)
| subset(X0,union(X1,X2)) ),
inference(duplicate_literals_removal,[status(thm)],[f2112]) ).
fof(f2125,plain,
! [X0,X1] : subset(X0,union(X1,X0)),
inference(duplicate_literals_removal,[status(thm)],[f2113]) ).
fof(f2130,plain,
! [X0,X1] :
( subset(difference(X0,X1),X0)
| subset(difference(X0,X1),X0) ),
inference(resolution,[status(thm)],[f298,f30]) ).
fof(f2151,plain,
! [X0,X1] : subset(difference(X0,X1),X0),
inference(duplicate_literals_removal,[status(thm)],[f2130]) ).
fof(f2154,plain,
! [X0,X1,X2] :
( ~ subset(difference(X0,X1),X1)
| subset(difference(X0,X1),X2)
| subset(difference(X0,X1),X2) ),
inference(resolution,[status(thm)],[f300,f213]) ).
fof(f2163,plain,
! [X0,X1,X2] :
( ~ subset(difference(X0,X1),X1)
| subset(difference(X0,X1),X2) ),
inference(duplicate_literals_removal,[status(thm)],[f2154]) ).
fof(f2193,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ subset(X1,sK19_skl)
| subset(X1,X2)
| ~ subset(union(sK18_skl,X0),empty_set) ),
inference(resolution,[status(thm)],[f2096,f406]) ).
fof(f2195,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ member(X1,sK19_skl)
| ~ subset(union(sK18_skl,X0),empty_set) ),
inference(resolution,[status(thm)],[f2096,f377]) ).
fof(f2198,definition,
! [X0] :
( sQ42_spl
<=> member(sK19_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f2199,plain,
! [X0] :
( ~ sQ42_spl
| member(sK19_skl,X0) ),
inference(component_clause,[status(thm)],[f2198]) ).
fof(f2202,definition,
! [X1] :
( sQ43_spl
<=> ~ subset(union(sK18_skl,X1),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f2206,plain,
( ~ sQ1_spl
| sQ17_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f2193,f2202,f635,f198]) ).
fof(f2207,plain,
( ~ sQ1_spl
| sQ14_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f2195,f2202,f422,f198]) ).
fof(f2233,plain,
! [X0] :
( ~ sQ1_spl
| member(sK19_skl,union(X0,sK18_skl)) ),
inference(resolution,[status(thm)],[f2125,f219]) ).
fof(f2241,plain,
! [X0] : subset(difference(sK18_skl,X0),sK17_skl),
inference(resolution,[status(thm)],[f2151,f1893]) ).
fof(f2242,plain,
! [X0] :
( ~ sQ5_spl
| subset(difference(sK17_skl,X0),sK18_skl) ),
inference(resolution,[status(thm)],[f2151,f1892]) ).
fof(f2333,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ subset(X1,sK19_skl)
| subset(X1,X2)
| ~ subset(union(X0,sK18_skl),empty_set) ),
inference(resolution,[status(thm)],[f2233,f406]) ).
fof(f2335,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ member(X1,sK19_skl)
| ~ subset(union(X0,sK18_skl),empty_set) ),
inference(resolution,[status(thm)],[f2233,f377]) ).
fof(f2339,definition,
! [X1] :
( sQ44_spl
<=> ~ subset(union(X1,sK18_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f2343,plain,
( ~ sQ1_spl
| sQ17_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f2333,f2339,f635,f198]) ).
fof(f2344,plain,
( ~ sQ1_spl
| sQ14_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f2335,f2339,f422,f198]) ).
fof(f2358,plain,
! [X0,X1] :
( member(X0,sK17_skl)
| member(X0,X1)
| ~ member(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f2241,f304]) ).
fof(f2409,plain,
! [X0,X1] :
( ~ sQ5_spl
| member(X0,sK18_skl)
| member(X0,X1)
| ~ member(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f2242,f304]) ).
fof(f2695,plain,
! [X0,X1] :
( ~ sQ1_spl
| member(sK19_skl,union(X0,X1))
| ~ subset(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f2043,f219]) ).
fof(f2782,plain,
! [X0,X1] :
( ~ sQ1_spl
| member(sK19_skl,X1)
| member(sK19_skl,X0)
| ~ subset(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f2695,f47]) ).
fof(f2784,plain,
! [X0,X1,X2,X3] :
( ~ sQ1_spl
| ~ subset(X2,sK19_skl)
| subset(X2,X3)
| ~ subset(union(X0,X1),empty_set)
| ~ subset(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f2695,f406]) ).
fof(f2786,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ member(X2,sK19_skl)
| ~ subset(union(X0,X1),empty_set)
| ~ subset(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f2695,f377]) ).
fof(f2789,definition,
! [X0] :
( sQ45_spl
<=> ( member(sK19_skl,X0)
| ~ subset(sK18_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f2792,plain,
( ~ sQ1_spl
| sQ42_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f2782,f2789,f2198,f198]) ).
fof(f2793,definition,
! [X0,X2] :
( sQ46_spl
<=> ( ~ subset(union(X0,X2),empty_set)
| ~ subset(sK18_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f2797,plain,
( ~ sQ1_spl
| sQ17_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f2784,f2793,f635,f198]) ).
fof(f2798,plain,
( ~ sQ1_spl
| sQ14_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f2786,f2793,f422,f198]) ).
fof(f2816,plain,
! [X0,X1] :
( ~ sQ14_spl
| ~ subset(X1,sK19_skl)
| ~ order(X0,X1)
| total_order(X0,X1) ),
inference(resolution,[status(thm)],[f423,f749]) ).
fof(f3297,plain,
! [X0,X1] :
( ~ sQ1_spl
| member(sK19_skl,union(X1,X0))
| ~ subset(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f2124,f219]) ).
fof(f3656,definition,
( sQ51_spl
<=> subset(sK17_skl,sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f3832,plain,
! [X0,X1] :
( ~ sQ14_spl
| ~ member(X0,X1)
| ~ subset(product(empty_set),sK19_skl) ),
inference(resolution,[status(thm)],[f458,f488]) ).
fof(f3838,plain,
! [X0,X1] :
( ~ member(X0,X1)
| ~ subset(product(empty_set),empty_set) ),
inference(resolution,[status(thm)],[f458,f377]) ).
fof(f3842,definition,
( sQ52_spl
<=> subset(product(empty_set),sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f3845,definition,
! [X0,X1] :
( sQ53_spl
<=> ~ member(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f3846,plain,
! [X0,X1] :
( ~ sQ53_spl
| ~ member(X0,X1) ),
inference(component_clause,[status(thm)],[f3845]) ).
fof(f3848,plain,
( ~ sQ14_spl
| sQ53_spl
| ~ sQ52_spl ),
inference(split_clause,[status(thm)],[f3832,f3842,f3845,f422]) ).
fof(f3852,definition,
( sQ55_spl
<=> subset(product(empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f3860,plain,
( sQ53_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f3838,f3852,f3845]) ).
fof(f3861,definition,
! [X0,X1] :
( sQ57_spl
<=> subset(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f3862,plain,
! [X0,X1] :
( ~ sQ57_spl
| subset(X0,X1) ),
inference(component_clause,[status(thm)],[f3861]) ).
fof(f3903,plain,
! [X0,X1,X2] :
( ~ sQ53_spl
| member(sK2_skl(intersection(X0,X1),X2),X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f456,f3846]) ).
fof(f3962,plain,
( ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3903,f3846]) ).
fof(f3963,plain,
~ sQ53_spl,
inference(contradiction_clause,[status(thm)],[f3962]) ).
fof(f4044,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ subset(sK18_skl,X1)
| ~ member(X2,sK19_skl)
| ~ subset(union(X0,X1),empty_set) ),
inference(resolution,[status(thm)],[f377,f3297]) ).
fof(f4085,definition,
! [X0,X1] :
( sQ58_spl
<=> ( ~ subset(sK18_skl,X1)
| ~ subset(union(X0,X1),empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f4088,plain,
( ~ sQ1_spl
| sQ14_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f4044,f4085,f422,f198]) ).
fof(f4134,plain,
! [X0] :
( ~ sQ1_spl
| member(sK19_skl,sK17_skl)
| ~ member(sK19_skl,X0) ),
inference(resolution,[status(thm)],[f2045,f199]) ).
fof(f4135,plain,
( ~ sQ1_spl
| sQ7_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f4134,f339,f285,f198]) ).
fof(f4152,plain,
! [X0] :
( ~ sQ5_spl
| subset(difference(sK17_skl,sK18_skl),X0) ),
inference(resolution,[status(thm)],[f2163,f2242]) ).
fof(f4153,plain,
! [X0] : subset(difference(sK18_skl,sK17_skl),X0),
inference(resolution,[status(thm)],[f2163,f2241]) ).
fof(f4229,plain,
! [X0] :
( member(X0,sK17_skl)
| ~ member(X0,sK18_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2358,f2045]) ).
fof(f4257,plain,
! [X0] :
( ~ sQ5_spl
| member(X0,sK18_skl)
| ~ member(X0,sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2409,f2100]) ).
fof(f4327,definition,
! [X0] :
( sQ61_spl
<=> ( ~ member(sK19_skl,X0)
| ~ subset(X0,sK18_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f4328,plain,
! [X0] :
( ~ sQ61_spl
| ~ member(sK19_skl,X0)
| ~ subset(X0,sK18_skl) ),
inference(component_clause,[status(thm)],[f4327]) ).
fof(f4628,plain,
! [X0,X1,X2,X3] :
( ~ sQ1_spl
| ~ subset(sK18_skl,X1)
| ~ subset(X2,sK19_skl)
| subset(X2,X3)
| ~ subset(union(X0,X1),empty_set) ),
inference(resolution,[status(thm)],[f1622,f3297]) ).
fof(f4648,plain,
( ~ sQ1_spl
| sQ17_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f4628,f4085,f635,f198]) ).
fof(f4761,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ member(sK18_skl,X2)
| ~ subset(X2,empty_set)
| ~ sP0_prd(difference(sK17_skl,X1),X0)
| order(X0,difference(sK17_skl,X1)) ),
inference(resolution,[status(thm)],[f576,f2242]) ).
fof(f4777,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ member(sK18_skl,X2)
| ~ subset(X2,empty_set)
| ~ sP0_prd(intersection(sK17_skl,X1),X0)
| order(X0,intersection(sK17_skl,X1)) ),
inference(resolution,[status(thm)],[f576,f1960]) ).
fof(f4779,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ member(sK18_skl,X2)
| ~ subset(X2,empty_set)
| ~ sP0_prd(intersection(X1,sK17_skl),X0)
| order(X0,intersection(X1,sK17_skl)) ),
inference(resolution,[status(thm)],[f576,f1971]) ).
fof(f4870,definition,
! [X0,X1] :
( sQ65_spl
<=> ( ~ sP0_prd(difference(sK17_skl,X1),X0)
| order(X0,difference(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f4873,plain,
( ~ sQ5_spl
| sQ25_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f4761,f4870,f813,f239]) ).
fof(f4902,definition,
! [X0,X1] :
( sQ73_spl
<=> ( ~ sP0_prd(intersection(sK17_skl,X1),X0)
| order(X0,intersection(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f4905,plain,
( ~ sQ5_spl
| sQ25_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f4777,f4902,f813,f239]) ).
fof(f4910,definition,
! [X0,X1] :
( sQ75_spl
<=> ( ~ sP0_prd(intersection(X1,sK17_skl),X0)
| order(X0,intersection(X1,sK17_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f4913,plain,
( ~ sQ5_spl
| sQ25_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f4779,f4910,f813,f239]) ).
fof(f5152,definition,
! [X0] :
( sQ80_spl
<=> ( ~ subset(sK17_skl,X0)
| ~ subset(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f5156,definition,
! [X0,X4] :
( sQ81_spl
<=> ( ~ subset(X4,X0)
| ~ subset(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f5157,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ subset(X1,X0)
| ~ subset(X0,empty_set) ),
inference(component_clause,[status(thm)],[f5156]) ).
fof(f5183,plain,
! [X0] :
( ~ sQ5_spl
| member(sK7_skl(sK17_skl,X0),sK18_skl)
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f99,f4257]) ).
fof(f5184,plain,
! [X0] :
( member(sK7_skl(sK18_skl,X0),sK17_skl)
| ~ order(X0,sK18_skl)
| total_order(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f99,f4229]) ).
fof(f5196,plain,
! [X0] :
( ~ sQ5_spl
| member(sK6_skl(sK17_skl,X0),sK18_skl)
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f98,f4257]) ).
fof(f5197,plain,
! [X0] :
( member(sK6_skl(sK18_skl,X0),sK17_skl)
| ~ order(X0,sK18_skl)
| total_order(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f98,f4229]) ).
fof(f5209,plain,
! [X0] :
( ~ sQ5_spl
| member(sK5_skl(sK17_skl,X0),sK18_skl)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f88,f4257]) ).
fof(f5217,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl)
| subset(sK7_skl(sK17_skl,X0),X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f407,f5183]) ).
fof(f5257,definition,
! [X0,X1] :
( sQ82_spl
<=> ( ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl)
| subset(sK7_skl(sK17_skl,X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f5260,plain,
( ~ sQ5_spl
| sQ82_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f5217,f426,f5257,f239]) ).
fof(f5269,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ order(X1,sK17_skl)
| total_order(X1,sK17_skl)
| ~ member(X0,sK7_skl(sK17_skl,X1))
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f377,f5183]) ).
fof(f5324,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ order(X1,sK17_skl)
| total_order(X1,sK17_skl)
| ~ member(sK18_skl,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f377,f5183]) ).
fof(f5365,definition,
! [X0,X1] :
( sQ83_spl
<=> ( ~ order(X1,sK17_skl)
| total_order(X1,sK17_skl)
| ~ member(X0,sK7_skl(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f5368,plain,
( ~ sQ5_spl
| sQ83_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f5269,f426,f5365,f239]) ).
fof(f5375,definition,
! [X1] :
( sQ84_spl
<=> ( ~ order(X1,sK17_skl)
| total_order(X1,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f5378,plain,
( ~ sQ5_spl
| sQ84_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f5324,f813,f5375,f239]) ).
fof(f5454,plain,
! [X0] :
( ~ sQ5_spl
| member(sK4_skl(sK17_skl,X0),sK18_skl)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f87,f4257]) ).
fof(f5470,plain,
! [X0] :
( ~ sQ5_spl
| member(sK3_skl(sK17_skl,X0),sK18_skl)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f86,f4257]) ).
fof(f5608,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ member(X1,sK6_skl(sK17_skl,X0))
| ~ subset(sK18_skl,empty_set)
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f5196,f377]) ).
fof(f5609,plain,
! [X0,X1] :
( ~ sQ5_spl
| subset(sK6_skl(sK17_skl,X0),X1)
| ~ subset(sK18_skl,empty_set)
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f5196,f407]) ).
fof(f5612,definition,
! [X0,X1] :
( sQ88_spl
<=> ( ~ member(X1,sK6_skl(sK17_skl,X0))
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f5615,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f5608,f5612,f426,f239]) ).
fof(f5616,definition,
! [X0,X1] :
( sQ89_spl
<=> ( subset(sK6_skl(sK17_skl,X0),X1)
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f5619,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f5609,f5616,f426,f239]) ).
fof(f5624,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ order(X2,sK17_skl)
| total_order(X2,sK17_skl)
| ~ subset(X0,sK6_skl(sK17_skl,X2))
| subset(X0,X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f1622,f5196]) ).
fof(f5628,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ order(X2,sK17_skl)
| total_order(X2,sK17_skl)
| ~ subset(X0,sK7_skl(sK17_skl,X2))
| subset(X0,X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f1622,f5183]) ).
fof(f5673,definition,
! [X0,X1,X2] :
( sQ90_spl
<=> ( ~ order(X2,sK17_skl)
| total_order(X2,sK17_skl)
| ~ subset(X0,sK6_skl(sK17_skl,X2))
| subset(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f5676,plain,
( ~ sQ5_spl
| sQ90_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f5624,f426,f5673,f239]) ).
fof(f5681,definition,
! [X0,X1,X2] :
( sQ92_spl
<=> ( ~ order(X2,sK17_skl)
| total_order(X2,sK17_skl)
| ~ subset(X0,sK7_skl(sK17_skl,X2))
| subset(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f5684,plain,
( ~ sQ5_spl
| sQ92_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f5628,f426,f5681,f239]) ).
fof(f5695,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ order(X1,sK17_skl)
| total_order(X1,sK17_skl)
| ~ sP0_prd(sK6_skl(sK17_skl,X1),X0)
| order(X0,sK6_skl(sK17_skl,X1))
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f1615,f5196]) ).
fof(f5699,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ order(X1,sK17_skl)
| total_order(X1,sK17_skl)
| ~ sP0_prd(sK7_skl(sK17_skl,X1),X0)
| order(X0,sK7_skl(sK17_skl,X1))
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f1615,f5183]) ).
fof(f5744,definition,
! [X0,X1] :
( sQ93_spl
<=> ( ~ order(X1,sK17_skl)
| total_order(X1,sK17_skl)
| ~ sP0_prd(sK6_skl(sK17_skl,X1),X0)
| order(X0,sK6_skl(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f5747,plain,
( ~ sQ5_spl
| sQ93_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f5695,f426,f5744,f239]) ).
fof(f5752,definition,
! [X0,X1] :
( sQ95_spl
<=> ( ~ order(X1,sK17_skl)
| total_order(X1,sK17_skl)
| ~ sP0_prd(sK7_skl(sK17_skl,X1),X0)
| order(X0,sK7_skl(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f5755,plain,
( ~ sQ5_spl
| sQ95_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f5699,f426,f5752,f239]) ).
fof(f5877,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ subset(sK17_skl,X1)
| member(sK19_skl,union(X0,X1)) ),
inference(resolution,[status(thm)],[f275,f2124]) ).
fof(f5878,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ subset(sK17_skl,X0)
| member(sK19_skl,union(X0,X1)) ),
inference(resolution,[status(thm)],[f275,f2043]) ).
fof(f5879,plain,
! [X0] :
( ~ sQ1_spl
| member(sK19_skl,union(X0,sK17_skl)) ),
inference(resolution,[status(thm)],[f275,f2125]) ).
fof(f5880,plain,
! [X0] :
( ~ sQ1_spl
| member(sK19_skl,union(sK17_skl,X0)) ),
inference(resolution,[status(thm)],[f275,f2044]) ).
fof(f5882,plain,
! [X0] :
( ~ sQ1_spl
| member(sK19_skl,sK17_skl)
| member(sK19_skl,X0) ),
inference(resolution,[status(thm)],[f5879,f47]) ).
fof(f5884,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ subset(X1,sK19_skl)
| subset(X1,X2)
| ~ subset(union(X0,sK17_skl),empty_set) ),
inference(resolution,[status(thm)],[f5879,f1622]) ).
fof(f5886,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ member(X1,sK19_skl)
| ~ subset(union(X0,sK17_skl),empty_set) ),
inference(resolution,[status(thm)],[f5879,f377]) ).
fof(f5889,plain,
( ~ sQ1_spl
| sQ7_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f5882,f2198,f285,f198]) ).
fof(f5890,definition,
! [X0] :
( sQ100_spl
<=> ~ subset(union(X0,sK17_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f5894,plain,
( ~ sQ1_spl
| sQ17_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f5884,f5890,f635,f198]) ).
fof(f5895,plain,
( ~ sQ1_spl
| sQ14_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f5886,f5890,f422,f198]) ).
fof(f5915,plain,
( ~ sQ42_spl
| $false ),
inference(resolution,[status(thm)],[f2199,f50]) ).
fof(f5932,plain,
~ sQ42_spl,
inference(contradiction_clause,[status(thm)],[f5915]) ).
fof(f5987,definition,
! [X0] :
( sQ102_spl
<=> ~ subset(union(sK17_skl,X0),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f5988,plain,
! [X0] :
( ~ sQ102_spl
| ~ subset(union(sK17_skl,X0),empty_set) ),
inference(component_clause,[status(thm)],[f5987]) ).
fof(f6110,plain,
! [X0,X1] :
( ~ sQ1_spl
| member(sK19_skl,X0)
| member(sK19_skl,X1)
| ~ subset(sK17_skl,X0) ),
inference(resolution,[status(thm)],[f5877,f47]) ).
fof(f6112,plain,
! [X0,X1,X2,X3] :
( ~ sQ1_spl
| ~ subset(X2,sK19_skl)
| subset(X2,X3)
| ~ subset(union(X1,X0),empty_set)
| ~ subset(sK17_skl,X0) ),
inference(resolution,[status(thm)],[f5877,f1622]) ).
fof(f6114,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ member(X2,sK19_skl)
| ~ subset(union(X1,X0),empty_set)
| ~ subset(sK17_skl,X0) ),
inference(resolution,[status(thm)],[f5877,f377]) ).
fof(f6117,definition,
! [X0] :
( sQ103_spl
<=> ( member(sK19_skl,X0)
| ~ subset(sK17_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f6120,plain,
( ~ sQ1_spl
| sQ42_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f6110,f6117,f2198,f198]) ).
fof(f6121,definition,
! [X0,X1] :
( sQ104_spl
<=> ( ~ subset(union(X1,X0),empty_set)
| ~ subset(sK17_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f6125,plain,
( ~ sQ1_spl
| sQ17_spl
| sQ104_spl ),
inference(split_clause,[status(thm)],[f6112,f6121,f635,f198]) ).
fof(f6126,plain,
( ~ sQ1_spl
| sQ14_spl
| sQ104_spl ),
inference(split_clause,[status(thm)],[f6114,f6121,f422,f198]) ).
fof(f6130,plain,
! [X0,X1,X2,X3] :
( ~ sQ1_spl
| ~ subset(X2,sK19_skl)
| subset(X2,X3)
| ~ subset(union(X0,X1),empty_set)
| ~ subset(sK17_skl,X0) ),
inference(resolution,[status(thm)],[f5878,f1622]) ).
fof(f6132,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ member(X2,sK19_skl)
| ~ subset(union(X0,X1),empty_set)
| ~ subset(sK17_skl,X0) ),
inference(resolution,[status(thm)],[f5878,f377]) ).
fof(f6136,definition,
! [X0,X1] :
( sQ105_spl
<=> ( ~ subset(union(X0,X1),empty_set)
| ~ subset(sK17_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f6140,plain,
( ~ sQ1_spl
| sQ17_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f6130,f6136,f635,f198]) ).
fof(f6141,plain,
( ~ sQ1_spl
| sQ14_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f6132,f6136,f422,f198]) ).
fof(f6227,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sP0_prd(sK5_skl(sK17_skl,X0),X1)
| order(X1,sK5_skl(sK17_skl,X0))
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f5209,f1615]) ).
fof(f6228,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ subset(X1,sK5_skl(sK17_skl,X0))
| subset(X1,X2)
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f5209,f1622]) ).
fof(f6230,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ member(X1,sK5_skl(sK17_skl,X0))
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f5209,f377]) ).
fof(f6231,plain,
! [X0,X1] :
( ~ sQ5_spl
| subset(sK5_skl(sK17_skl,X0),X1)
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f5209,f407]) ).
fof(f6233,definition,
! [X0,X1] :
( sQ106_spl
<=> ( ~ sP0_prd(sK5_skl(sK17_skl,X0),X1)
| order(X1,sK5_skl(sK17_skl,X0))
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f6236,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| sQ106_spl ),
inference(split_clause,[status(thm)],[f6227,f6233,f426,f239]) ).
fof(f6237,definition,
! [X0,X1,X2] :
( sQ107_spl
<=> ( ~ subset(X1,sK5_skl(sK17_skl,X0))
| subset(X1,X2)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f6240,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f6228,f6237,f426,f239]) ).
fof(f6242,definition,
! [X0,X1] :
( sQ108_spl
<=> ( ~ member(X1,sK5_skl(sK17_skl,X0))
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f6245,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| sQ108_spl ),
inference(split_clause,[status(thm)],[f6230,f6242,f426,f239]) ).
fof(f6246,definition,
! [X0,X1] :
( sQ109_spl
<=> ( subset(sK5_skl(sK17_skl,X0),X1)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f6249,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| sQ109_spl ),
inference(split_clause,[status(thm)],[f6231,f6246,f426,f239]) ).
fof(f6329,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sP0_prd(sK4_skl(sK17_skl,X0),X1)
| order(X1,sK4_skl(sK17_skl,X0))
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f5454,f1615]) ).
fof(f6330,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ subset(X1,sK4_skl(sK17_skl,X0))
| subset(X1,X2)
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f5454,f1622]) ).
fof(f6332,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ member(X1,sK4_skl(sK17_skl,X0))
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f5454,f377]) ).
fof(f6333,plain,
! [X0,X1] :
( ~ sQ5_spl
| subset(sK4_skl(sK17_skl,X0),X1)
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f5454,f407]) ).
fof(f6335,definition,
! [X0,X1] :
( sQ114_spl
<=> ( ~ sP0_prd(sK4_skl(sK17_skl,X0),X1)
| order(X1,sK4_skl(sK17_skl,X0))
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f6338,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| sQ114_spl ),
inference(split_clause,[status(thm)],[f6329,f6335,f426,f239]) ).
fof(f6339,definition,
! [X0,X1,X2] :
( sQ115_spl
<=> ( ~ subset(X1,sK4_skl(sK17_skl,X0))
| subset(X1,X2)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f6342,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f6330,f6339,f426,f239]) ).
fof(f6344,definition,
! [X0,X1] :
( sQ116_spl
<=> ( ~ member(X1,sK4_skl(sK17_skl,X0))
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f6347,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| sQ116_spl ),
inference(split_clause,[status(thm)],[f6332,f6344,f426,f239]) ).
fof(f6348,definition,
! [X0,X1] :
( sQ117_spl
<=> ( subset(sK4_skl(sK17_skl,X0),X1)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f6351,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f6333,f6348,f426,f239]) ).
fof(f6394,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sP0_prd(sK3_skl(sK17_skl,X0),X1)
| order(X1,sK3_skl(sK17_skl,X0))
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f5470,f1615]) ).
fof(f6395,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ subset(X1,sK3_skl(sK17_skl,X0))
| subset(X1,X2)
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f5470,f1622]) ).
fof(f6397,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ member(X1,sK3_skl(sK17_skl,X0))
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f5470,f377]) ).
fof(f6398,plain,
! [X0,X1] :
( ~ sQ5_spl
| subset(sK3_skl(sK17_skl,X0),X1)
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f5470,f407]) ).
fof(f6400,definition,
! [X0,X1] :
( sQ122_spl
<=> ( ~ sP0_prd(sK3_skl(sK17_skl,X0),X1)
| order(X1,sK3_skl(sK17_skl,X0))
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f6403,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f6394,f6400,f426,f239]) ).
fof(f6404,definition,
! [X0,X1,X2] :
( sQ123_spl
<=> ( ~ subset(X1,sK3_skl(sK17_skl,X0))
| subset(X1,X2)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f6407,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f6395,f6404,f426,f239]) ).
fof(f6409,definition,
! [X0,X1] :
( sQ124_spl
<=> ( ~ member(X1,sK3_skl(sK17_skl,X0))
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f6412,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| sQ124_spl ),
inference(split_clause,[status(thm)],[f6397,f6409,f426,f239]) ).
fof(f6413,definition,
! [X0,X1] :
( sQ125_spl
<=> ( subset(sK3_skl(sK17_skl,X0),X1)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f6416,plain,
( ~ sQ5_spl
| ~ sQ15_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f6398,f6413,f426,f239]) ).
fof(f6454,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X2)
| order(X2,sK17_skl)
| ~ subset(X1,sK3_skl(sK17_skl,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f1616,f5470]) ).
fof(f6462,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X2)
| order(X2,sK17_skl)
| ~ subset(X1,sK4_skl(sK17_skl,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f1616,f5454]) ).
fof(f6471,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X2)
| order(X2,sK17_skl)
| ~ subset(X1,sK5_skl(sK17_skl,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f1616,f5209]) ).
fof(f6475,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ order(X2,sK17_skl)
| total_order(X2,sK17_skl)
| ~ subset(X1,sK6_skl(sK17_skl,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f1616,f5196]) ).
fof(f6479,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ order(X2,sK17_skl)
| total_order(X2,sK17_skl)
| ~ subset(X1,sK7_skl(sK17_skl,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f1616,f5183]) ).
fof(f6532,definition,
! [X0,X1,X2] :
( sQ131_spl
<=> ( ~ sP0_prd(sK17_skl,X2)
| order(X2,sK17_skl)
| ~ subset(X1,sK3_skl(sK17_skl,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f6535,plain,
( ~ sQ5_spl
| sQ131_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f6454,f426,f6532,f239]) ).
fof(f6540,definition,
! [X0,X1,X2] :
( sQ133_spl
<=> ( ~ sP0_prd(sK17_skl,X2)
| order(X2,sK17_skl)
| ~ subset(X1,sK4_skl(sK17_skl,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f6543,plain,
( ~ sQ5_spl
| sQ133_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f6462,f426,f6540,f239]) ).
fof(f6548,definition,
! [X0,X1,X2] :
( sQ135_spl
<=> ( ~ sP0_prd(sK17_skl,X2)
| order(X2,sK17_skl)
| ~ subset(X1,sK5_skl(sK17_skl,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f6551,plain,
( ~ sQ5_spl
| sQ135_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f6471,f426,f6548,f239]) ).
fof(f6556,definition,
! [X0,X1,X2] :
( sQ137_spl
<=> ( ~ order(X2,sK17_skl)
| total_order(X2,sK17_skl)
| ~ subset(X1,sK6_skl(sK17_skl,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f6559,plain,
( ~ sQ5_spl
| sQ137_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f6475,f426,f6556,f239]) ).
fof(f6564,definition,
! [X0,X1,X2] :
( sQ139_spl
<=> ( ~ order(X2,sK17_skl)
| total_order(X2,sK17_skl)
| ~ subset(X1,sK7_skl(sK17_skl,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f6567,plain,
( ~ sQ5_spl
| sQ139_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f6479,f426,f6564,f239]) ).
fof(f6691,definition,
( sQ142_spl
<=> sP0_prd(sK17_skl,sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f6693,plain,
( sQ142_spl
| ~ sP0_prd(sK17_skl,sK16_skl) ),
inference(component_clause,[status(thm)],[f6691]) ).
fof(f6698,definition,
( sQ144_spl
<=> sP0_prd(sK18_skl,sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f6700,plain,
( sQ144_spl
| ~ sP0_prd(sK18_skl,sK16_skl) ),
inference(component_clause,[status(thm)],[f6698]) ).
fof(f6710,plain,
( sQ142_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6693,f210]) ).
fof(f6711,plain,
sQ142_spl,
inference(contradiction_clause,[status(thm)],[f6710]) ).
fof(f6937,plain,
! [X0] :
( ~ sQ17_spl
| subset(sK19_skl,X0) ),
inference(resolution,[status(thm)],[f636,f215]) ).
fof(f6959,plain,
! [X0] :
( ~ sQ81_spl
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f5157,f294]) ).
fof(f6961,plain,
( ~ sQ81_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f6959,f1384,f5156]) ).
fof(f7005,plain,
( ~ sQ1_spl
| ~ sQ61_spl
| ~ subset(sK18_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f4328,f199]) ).
fof(f7023,plain,
( ~ sQ1_spl
| ~ sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7005,f215]) ).
fof(f7024,plain,
( ~ sQ1_spl
| ~ sQ61_spl ),
inference(contradiction_clause,[status(thm)],[f7023]) ).
fof(f7816,plain,
! [X0,X1,X2] :
( ~ member(sK6_skl(X1,X0),X2)
| ~ member(sK7_skl(X1,X0),X2)
| ~ total_order(X0,X2)
| ~ order(X0,X1)
| total_order(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f827,f101]) ).
fof(f7822,plain,
! [X0] :
( ~ order(X0,sK18_skl)
| total_order(X0,sK18_skl)
| ~ member(sK6_skl(sK18_skl,X0),sK17_skl)
| ~ total_order(X0,sK17_skl)
| ~ order(X0,sK18_skl)
| total_order(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f7816,f5184]) ).
fof(f7823,plain,
! [X0] :
( ~ sQ5_spl
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl)
| ~ member(sK6_skl(sK17_skl,X0),sK18_skl)
| ~ total_order(X0,sK18_skl)
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f7816,f5183]) ).
fof(f7851,plain,
! [X0] :
( ~ member(sK6_skl(sK18_skl,X0),sK17_skl)
| ~ total_order(X0,sK17_skl)
| ~ order(X0,sK18_skl)
| total_order(X0,sK18_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f7822]) ).
fof(f7852,plain,
! [X0] :
( ~ total_order(X0,sK17_skl)
| ~ order(X0,sK18_skl)
| total_order(X0,sK18_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f7851,f5197]) ).
fof(f7853,plain,
! [X0] :
( ~ sQ5_spl
| ~ member(sK6_skl(sK17_skl,X0),sK18_skl)
| ~ total_order(X0,sK18_skl)
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f7823]) ).
fof(f7854,plain,
! [X0] :
( ~ sQ5_spl
| ~ total_order(X0,sK18_skl)
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f7853,f5196]) ).
fof(f7899,plain,
( ~ sQ19_spl
| ~ order(sK16_skl,sK18_skl)
| total_order(sK16_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f7852,f752]) ).
fof(f7900,definition,
( sQ167_spl
<=> total_order(sK16_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f7901,plain,
( ~ sQ167_spl
| total_order(sK16_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f7900]) ).
fof(f7903,definition,
( sQ168_spl
<=> order(sK16_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f7904,plain,
( ~ sQ168_spl
| order(sK16_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f7903]) ).
fof(f7905,plain,
( sQ168_spl
| ~ order(sK16_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f7903]) ).
fof(f7906,plain,
( ~ sQ19_spl
| ~ sQ168_spl
| sQ167_spl ),
inference(split_clause,[status(thm)],[f7899,f7900,f7903,f751]) ).
fof(f7952,plain,
( ~ sQ167_spl
| order(sK16_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f7901,f96]) ).
fof(f7953,plain,
( ~ sQ167_spl
| sQ168_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7952,f7905]) ).
fof(f7954,plain,
( ~ sQ167_spl
| sQ168_spl ),
inference(contradiction_clause,[status(thm)],[f7953]) ).
fof(f7955,plain,
! [X0] :
( ~ sQ168_spl
| ~ member(sK18_skl,X0)
| ~ subset(X0,empty_set)
| total_order(sK16_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f7904,f730]) ).
fof(f7956,plain,
( ~ sQ168_spl
| ~ subset(sK18_skl,empty_set)
| total_order(sK16_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f7904,f874]) ).
fof(f7957,plain,
( ~ sQ168_spl
| sP0_prd(sK18_skl,sK16_skl) ),
inference(resolution,[status(thm)],[f7904,f84]) ).
fof(f7958,plain,
( ~ sQ168_spl
| sQ25_spl
| sQ167_spl ),
inference(split_clause,[status(thm)],[f7955,f7900,f813,f7903]) ).
fof(f7959,plain,
( ~ sQ168_spl
| ~ sQ15_spl
| sQ167_spl ),
inference(split_clause,[status(thm)],[f7956,f7900,f426,f7903]) ).
fof(f7960,plain,
( ~ sQ168_spl
| sQ144_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7957,f6700]) ).
fof(f7961,plain,
( ~ sQ168_spl
| sQ144_spl ),
inference(contradiction_clause,[status(thm)],[f7960]) ).
fof(f8318,plain,
( ~ sQ167_spl
| ~ sQ5_spl
| ~ order(sK16_skl,sK17_skl)
| total_order(sK16_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f7854,f7901]) ).
fof(f8319,definition,
( sQ174_spl
<=> order(sK16_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f8321,plain,
( sQ174_spl
| ~ order(sK16_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f8319]) ).
fof(f8322,plain,
( ~ sQ167_spl
| ~ sQ5_spl
| ~ sQ174_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f8318,f751,f8319,f239,f7900]) ).
fof(f8323,plain,
( sQ174_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8321,f173]) ).
fof(f8324,plain,
sQ174_spl,
inference(contradiction_clause,[status(thm)],[f8323]) ).
fof(f8437,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f553,f75]) ).
fof(f8442,plain,
! [X0,X1,X2] :
( ~ member(X1,X2)
| ~ subset(product(X0),empty_set)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f553,f377]) ).
fof(f8447,plain,
! [X0,X1] :
( ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(forward_subsumption_resolution,[status(thm)],[f8437,f377]) ).
fof(f8448,definition,
! [X0] :
( sQ175_spl
<=> ( ~ subset(product(X0),empty_set)
| ~ subset(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f8452,plain,
( sQ53_spl
| sQ175_spl ),
inference(split_clause,[status(thm)],[f8442,f8448,f3845]) ).
fof(f8524,plain,
( ~ sQ102_spl
| ~ sQ57_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5988,f3862]) ).
fof(f8555,plain,
( ~ sQ102_spl
| ~ sQ57_spl ),
inference(contradiction_clause,[status(thm)],[f8524]) ).
fof(f8727,plain,
! [X0] :
( ~ sQ5_spl
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f8447,f5196]) ).
fof(f8769,plain,
( ~ sQ5_spl
| sQ84_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f8727,f426,f5375,f239]) ).
fof(f8837,plain,
! [X0,X1,X2] :
( ~ subset(X2,empty_set)
| ~ subset(X1,X2)
| ~ order(X0,X1)
| total_order(X0,X1) ),
inference(resolution,[status(thm)],[f732,f8447]) ).
fof(f9783,plain,
! [X0] :
( ~ subset(X0,empty_set)
| ~ subset(sK17_skl,X0)
| total_order(sK16_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f8837,f173]) ).
fof(f9784,plain,
( sQ80_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f9783,f751,f5152]) ).
fof(f10167,definition,
! [X3,X4] :
( sQ183_spl
<=> ( ~ subset(X3,empty_set)
| ~ member(X3,X4) ) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f10168,plain,
! [X0,X1] :
( ~ sQ183_spl
| ~ subset(X0,empty_set)
| ~ member(X0,X1) ),
inference(component_clause,[status(thm)],[f10167]) ).
fof(f10174,plain,
( ~ sQ1_spl
| ~ sQ183_spl
| ~ subset(sK19_skl,empty_set) ),
inference(resolution,[status(thm)],[f10168,f2096]) ).
fof(f10265,plain,
( ~ sQ1_spl
| ~ sQ183_spl
| ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10174,f6937]) ).
fof(f10266,plain,
( ~ sQ1_spl
| ~ sQ183_spl
| ~ sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f10265]) ).
fof(f10391,plain,
! [X0,X1,X2,X3] :
( ~ upper_bound(X0,X2,X1)
| ~ member(X0,X1)
| least_upper_bound(X0,X1,X2,X3)
| ~ member(X0,X1)
| ~ upper_bound(X0,X2,X1)
| ~ member(X0,X1)
| least_upper_bound(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f1291,f159]) ).
fof(f10396,plain,
! [X0,X1,X2,X3] :
( ~ upper_bound(X0,X2,X1)
| ~ member(X0,X1)
| least_upper_bound(X0,X1,X2,X3) ),
inference(duplicate_literals_removal,[status(thm)],[f10391]) ).
fof(f10403,definition,
! [X1] :
( sQ185_spl
<=> ~ subset(X1,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f10404,plain,
! [X0] :
( ~ sQ185_spl
| ~ subset(X0,sK18_skl) ),
inference(component_clause,[status(thm)],[f10403]) ).
fof(f10412,plain,
( ~ sQ5_spl
| ~ sQ185_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1960,f10404]) ).
fof(f10432,plain,
( ~ sQ5_spl
| ~ sQ185_spl ),
inference(contradiction_clause,[status(thm)],[f10412]) ).
fof(f10848,plain,
! [X0] :
( ~ sQ14_spl
| sP0_prd(sK19_skl,X0)
| member(sK20_skl(sK19_skl,X0),sK19_skl) ),
inference(resolution,[status(thm)],[f1834,f423]) ).
fof(f10864,plain,
! [X0,X1] :
( ~ subset(X0,empty_set)
| sP0_prd(X0,X1)
| member(sK20_skl(X0,X1),X0) ),
inference(resolution,[status(thm)],[f1834,f8447]) ).
fof(f10866,plain,
! [X0] :
( ~ sQ14_spl
| sP0_prd(sK19_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10848,f423]) ).
fof(f10868,plain,
! [X0,X1] :
( ~ subset(X0,empty_set)
| sP0_prd(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f10864,f8447]) ).
fof(f10895,definition,
! [X0] :
( sQ189_spl
<=> total_order(X0,sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f10898,definition,
! [X1] :
( sQ190_spl
<=> ( ~ subset(X1,empty_set)
| ~ subset(sK19_skl,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f10899,plain,
! [X0] :
( ~ sQ190_spl
| ~ subset(X0,empty_set)
| ~ subset(sK19_skl,X0) ),
inference(component_clause,[status(thm)],[f10898]) ).
fof(f10902,definition,
( sQ191_spl
<=> subset(sK19_skl,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f10904,plain,
( sQ191_spl
| ~ subset(sK19_skl,empty_set) ),
inference(component_clause,[status(thm)],[f10902]) ).
fof(f10906,plain,
( sQ191_spl
| ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10904,f6937]) ).
fof(f10907,plain,
( sQ191_spl
| ~ sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f10906]) ).
fof(f10908,plain,
! [X0] :
( ~ sQ190_spl
| ~ sQ17_spl
| ~ subset(X0,empty_set) ),
inference(forward_subsumption_resolution,[status(thm)],[f10899,f6937]) ).
fof(f10909,plain,
! [X0] :
( ~ sQ14_spl
| order(X0,sK19_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f493,f10866]) ).
fof(f10957,plain,
( ~ sQ17_spl
| ~ sQ190_spl
| $false ),
inference(resolution,[status(thm)],[f10908,f6937]) ).
fof(f10977,plain,
( ~ sQ17_spl
| ~ sQ190_spl ),
inference(contradiction_clause,[status(thm)],[f10957]) ).
fof(f11108,plain,
! [X0,X1] :
( ~ sP0_prd(X0,X1)
| order(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f8447,f86]) ).
fof(f11118,plain,
! [X0] :
( ~ sQ1_spl
| ~ subset(union(sK17_skl,X0),empty_set) ),
inference(resolution,[status(thm)],[f8447,f5880]) ).
fof(f11217,plain,
! [X0,X1] :
( order(X1,X0)
| ~ subset(X0,empty_set) ),
inference(forward_subsumption_resolution,[status(thm)],[f11108,f10868]) ).
fof(f11220,plain,
( ~ sQ1_spl
| sQ102_spl ),
inference(split_clause,[status(thm)],[f11118,f5987,f198]) ).
fof(f11295,plain,
! [X0] : order(X0,difference(sK18_skl,sK17_skl)),
inference(resolution,[status(thm)],[f11217,f4153]) ).
fof(f11296,plain,
! [X0] :
( ~ sQ5_spl
| order(X0,difference(sK17_skl,sK18_skl)) ),
inference(resolution,[status(thm)],[f11217,f4152]) ).
fof(f11301,plain,
! [X0] : order(X0,empty_set),
inference(resolution,[status(thm)],[f11217,f215]) ).
fof(f11980,plain,
( ~ sQ14_spl
| ~ subset(sK17_skl,sK19_skl)
| total_order(sK16_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f2816,f173]) ).
fof(f11983,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ14_spl
| ~ subset(difference(sK17_skl,sK18_skl),sK19_skl)
| total_order(X0,difference(sK17_skl,sK18_skl)) ),
inference(resolution,[status(thm)],[f2816,f11296]) ).
fof(f11984,plain,
! [X0] :
( ~ sQ14_spl
| ~ subset(difference(sK18_skl,sK17_skl),sK19_skl)
| total_order(X0,difference(sK18_skl,sK17_skl)) ),
inference(resolution,[status(thm)],[f2816,f11295]) ).
fof(f11989,plain,
! [X0] :
( ~ sQ14_spl
| ~ subset(empty_set,sK19_skl)
| total_order(X0,empty_set) ),
inference(resolution,[status(thm)],[f2816,f11301]) ).
fof(f11990,plain,
! [X0] :
( ~ sQ14_spl
| ~ subset(sK19_skl,sK19_skl)
| total_order(X0,sK19_skl) ),
inference(resolution,[status(thm)],[f2816,f10909]) ).
fof(f11991,plain,
( ~ sQ14_spl
| ~ sQ51_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f11980,f751,f3656,f422]) ).
fof(f11994,definition,
! [X0] :
( sQ192_spl
<=> total_order(X0,difference(sK17_skl,sK18_skl)) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f11997,definition,
( sQ193_spl
<=> subset(difference(sK17_skl,sK18_skl),sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f11999,plain,
( sQ193_spl
| ~ subset(difference(sK17_skl,sK18_skl),sK19_skl) ),
inference(component_clause,[status(thm)],[f11997]) ).
fof(f12000,plain,
( ~ sQ5_spl
| ~ sQ14_spl
| ~ sQ193_spl
| sQ192_spl ),
inference(split_clause,[status(thm)],[f11983,f11994,f11997,f422,f239]) ).
fof(f12001,definition,
! [X0] :
( sQ194_spl
<=> total_order(X0,difference(sK18_skl,sK17_skl)) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f12004,definition,
( sQ195_spl
<=> subset(difference(sK18_skl,sK17_skl),sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f12006,plain,
( sQ195_spl
| ~ subset(difference(sK18_skl,sK17_skl),sK19_skl) ),
inference(component_clause,[status(thm)],[f12004]) ).
fof(f12007,plain,
( ~ sQ14_spl
| ~ sQ195_spl
| sQ194_spl ),
inference(split_clause,[status(thm)],[f11984,f12001,f12004,f422]) ).
fof(f12012,definition,
! [X0] :
( sQ196_spl
<=> total_order(X0,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f12015,definition,
( sQ197_spl
<=> subset(empty_set,sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f12018,plain,
( ~ sQ14_spl
| ~ sQ197_spl
| sQ196_spl ),
inference(split_clause,[status(thm)],[f11989,f12012,f12015,f422]) ).
fof(f12019,definition,
( sQ198_spl
<=> subset(sK19_skl,sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f12021,plain,
( sQ198_spl
| ~ subset(sK19_skl,sK19_skl) ),
inference(component_clause,[status(thm)],[f12019]) ).
fof(f12022,plain,
( ~ sQ14_spl
| ~ sQ198_spl
| sQ189_spl ),
inference(split_clause,[status(thm)],[f11990,f10895,f12019,f422]) ).
fof(f12023,plain,
( sQ198_spl
| ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12021,f6937]) ).
fof(f12024,plain,
( sQ198_spl
| ~ sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f12023]) ).
fof(f12025,plain,
( sQ195_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12006,f4153]) ).
fof(f12026,plain,
sQ195_spl,
inference(contradiction_clause,[status(thm)],[f12025]) ).
fof(f12027,plain,
( sQ193_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11999,f4152]) ).
fof(f12028,plain,
( sQ193_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f12027]) ).
fof(f12600,plain,
( sQ2_spl
| ~ upper_bound(sK19_skl,sK16_skl,sK18_skl)
| ~ member(sK19_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f10396,f204]) ).
fof(f12604,plain,
( sQ2_spl
| ~ sQ41_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f12600,f198,f2052,f202]) ).
fof(f12605,plain,
$false,
inference(sat_refutation,[status(thm)],[f201,f205,f206,f218,f229,f245,f247,f255,f342,f425,f429,f638,f639,f757,f816,f890,f1086,f1224,f1243,f1248,f1345,f1387,f1391,f1421,f1655,f1674,f1947,f2055,f2206,f2207,f2343,f2344,f2792,f2797,f2798,f3848,f3860,f3963,f4088,f4135,f4648,f4873,f4905,f4913,f5260,f5368,f5378,f5615,f5619,f5676,f5684,f5747,f5755,f5889,f5894,f5895,f5932,f6120,f6125,f6126,f6140,f6141,f6236,f6240,f6245,f6249,f6338,f6342,f6347,f6351,f6403,f6407,f6412,f6416,f6535,f6543,f6551,f6559,f6567,f6711,f6961,f7024,f7906,f7954,f7958,f7959,f7961,f8322,f8324,f8452,f8555,f8769,f9784,f10266,f10432,f10907,f10977,f11220,f11991,f12000,f12007,f12018,f12022,f12024,f12026,f12028,f12604]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET801+4 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 05:36:50 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 42.77/5.87 % Refutation found
% 42.77/5.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 42.77/5.87 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.40/6.52 % Elapsed time: 6.142944 seconds
% 3.40/6.52 % CPU time: 44.222366 seconds
% 3.40/6.52 % Total memory used: 401.083 MB
% 3.40/6.52 % Net memory used: 340.590 MB
%------------------------------------------------------------------------------