%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET802+4 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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 44.44s 6.04s
% Output : CNFRefutation 44.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 128
% Syntax : Number of formulae : 640 ( 34 unt; 114 def)
% Number of atoms : 2240 ( 15 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 2793 (1193 ~;1286 |; 161 &)
% ( 137 <=>; 15 =>; 0 <=; 1 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 125 ( 123 usr; 113 prp; 0-4 aty)
% Number of functors : 24 ( 24 usr; 5 con; 0-4 aty)
% Number of variables : 1179 (1142 !; 37 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( subset(A,B)
<=> ! [X] :
( member(X,A)
=> member(X,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] :
( equal_set(A,B)
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,A,B] :
( member(X,intersection(A,B))
<=> ( member(X,B)
& member(X,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,A,B] :
( member(X,union(A,B))
<=> ( member(X,B)
| member(X,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] : ~ member(X,empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [B,A,E] :
( member(B,difference(E,A))
<=> ( ~ member(B,A)
& member(B,E) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,A] :
( member(X,sum(A))
<=> ? [Y] :
( member(X,Y)
& member(Y,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,A] :
( member(X,product(A))
<=> ! [Y] :
( member(Y,A)
=> member(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [R,E] :
( order(R,E)
<=> ( ! [X,Y,Z] :
( ( member(Z,E)
& member(Y,E)
& member(X,E) )
=> ( ( apply(R,Y,Z)
& apply(R,X,Y) )
=> apply(R,X,Z) ) )
& ! [X,Y] :
( ( member(Y,E)
& member(X,E) )
=> ( ( apply(R,Y,X)
& apply(R,X,Y) )
=> X = Y ) )
& ! [X] :
( member(X,E)
=> apply(R,X,X) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [R,E,M] :
( lower_bound(M,R,E)
<=> ! [X] :
( member(X,E)
=> apply(R,M,X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [R,E,M] :
( least(M,R,E)
<=> ( ! [X] :
( member(X,E)
=> apply(R,M,X) )
& member(M,E) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A,X,R,E] :
( greatest_lower_bound(A,X,R,E)
<=> ( ! [M] :
( ( lower_bound(M,R,X)
& member(M,E) )
=> apply(R,M,A) )
& lower_bound(A,R,X)
& member(A,X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,conjecture,
! [R,E] :
( order(R,E)
=> ! [X] :
( subset(X,E)
=> ! [M] :
( least(M,R,X)
<=> ( greatest_lower_bound(M,X,R,E)
& member(M,X) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
~ ! [R,E] :
( order(R,E)
=> ! [X] :
( subset(X,E)
=> ! [M] :
( least(M,R,X)
<=> ( greatest_lower_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(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(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(f109,plain,
! [R,E,M] :
( lower_bound(M,R,E)
<=> ! [X] :
( apply(R,M,X)
| ~ member(X,E) ) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f110,plain,
! [R,E,M] :
( ( ? [X] :
( ~ apply(R,M,X)
& member(X,E) )
| lower_bound(M,R,E) )
& ( ! [X] :
( apply(R,M,X)
| ~ member(X,E) )
| ~ lower_bound(M,R,E) ) ),
inference(NNF_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
( ! [R,E,M] :
( ? [X] :
( ~ apply(R,M,X)
& member(X,E) )
| lower_bound(M,R,E) )
& ! [R,E,M] :
( ! [X] :
( apply(R,M,X)
| ~ member(X,E) )
| ~ lower_bound(M,R,E) ) ),
inference(miniscoping,[status(thm)],[f110]) ).
fof(f112,plain,
( ! [R,E,M] :
( ( ~ apply(R,M,sK9_skl(M,E,R))
& member(sK9_skl(M,E,R),E) )
| lower_bound(M,R,E) )
& ! [R,E,M] :
( ! [X] :
( apply(R,M,X)
| ~ member(X,E) )
| ~ lower_bound(M,R,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X,sK9_skl(M,E,R))],[f111]) ).
fof(f113,plain,
! [X0,X1,X2,X3] :
( apply(X1,X0,X3)
| ~ member(X3,X2)
| ~ lower_bound(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f114,plain,
! [X0,X1,X2] :
( member(sK9_skl(X0,X2,X1),X2)
| lower_bound(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f115,plain,
! [X0,X1,X2] :
( ~ apply(X1,X0,sK9_skl(X0,X2,X1))
| lower_bound(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f124,plain,
! [R,E,M] :
( least(M,R,E)
<=> ( ! [X] :
( apply(R,M,X)
| ~ member(X,E) )
& member(M,E) ) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f125,plain,
! [R,E,M] :
( ( ? [X] :
( ~ apply(R,M,X)
& member(X,E) )
| ~ member(M,E)
| least(M,R,E) )
& ( ( ! [X] :
( apply(R,M,X)
| ~ member(X,E) )
& member(M,E) )
| ~ least(M,R,E) ) ),
inference(NNF_transformation,[status(thm)],[f124]) ).
fof(f126,plain,
( ! [R,E,M] :
( ? [X] :
( ~ apply(R,M,X)
& member(X,E) )
| ~ member(M,E)
| least(M,R,E) )
& ! [R,E,M] :
( ( ! [X] :
( apply(R,M,X)
| ~ member(X,E) )
& member(M,E) )
| ~ least(M,R,E) ) ),
inference(miniscoping,[status(thm)],[f125]) ).
fof(f127,plain,
( ! [R,E,M] :
( ( ~ apply(R,M,sK11_skl(M,E,R))
& member(sK11_skl(M,E,R),E) )
| ~ member(M,E)
| least(M,R,E) )
& ! [R,E,M] :
( ( ! [X] :
( apply(R,M,X)
| ~ member(X,E) )
& member(M,E) )
| ~ least(M,R,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X,sK11_skl(M,E,R))],[f126]) ).
fof(f128,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ least(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f129,plain,
! [X0,X1,X2,X3] :
( apply(X1,X0,X3)
| ~ member(X3,X2)
| ~ least(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f130,plain,
! [X0,X1,X2] :
( member(sK11_skl(X0,X2,X1),X2)
| ~ member(X0,X2)
| least(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f131,plain,
! [X0,X1,X2] :
( ~ apply(X1,X0,sK11_skl(X0,X2,X1))
| ~ member(X0,X2)
| least(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f160,plain,
! [A,X,R,E] :
( greatest_lower_bound(A,X,R,E)
<=> ( ! [M] :
( apply(R,M,A)
| ~ lower_bound(M,R,X)
| ~ member(M,E) )
& lower_bound(A,R,X)
& member(A,X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f161,plain,
! [A,X,R,E] :
( ( ? [M] :
( ~ apply(R,M,A)
& lower_bound(M,R,X)
& member(M,E) )
| ~ lower_bound(A,R,X)
| ~ member(A,X)
| greatest_lower_bound(A,X,R,E) )
& ( ( ! [M] :
( apply(R,M,A)
| ~ lower_bound(M,R,X)
| ~ member(M,E) )
& lower_bound(A,R,X)
& member(A,X) )
| ~ greatest_lower_bound(A,X,R,E) ) ),
inference(NNF_transformation,[status(thm)],[f160]) ).
fof(f162,plain,
( ! [A,X,R,E] :
( ? [M] :
( ~ apply(R,M,A)
& lower_bound(M,R,X)
& member(M,E) )
| ~ lower_bound(A,R,X)
| ~ member(A,X)
| greatest_lower_bound(A,X,R,E) )
& ! [A,X,R,E] :
( ( ! [M] :
( apply(R,M,A)
| ~ lower_bound(M,R,X)
| ~ member(M,E) )
& lower_bound(A,R,X)
& member(A,X) )
| ~ greatest_lower_bound(A,X,R,E) ) ),
inference(miniscoping,[status(thm)],[f161]) ).
fof(f163,plain,
( ! [A,X,R,E] :
( ( ~ apply(R,sK15_skl(E,R,X,A),A)
& lower_bound(sK15_skl(E,R,X,A),R,X)
& member(sK15_skl(E,R,X,A),E) )
| ~ lower_bound(A,R,X)
| ~ member(A,X)
| greatest_lower_bound(A,X,R,E) )
& ! [A,X,R,E] :
( ( ! [M] :
( apply(R,M,A)
| ~ lower_bound(M,R,X)
| ~ member(M,E) )
& lower_bound(A,R,X)
& member(A,X) )
| ~ greatest_lower_bound(A,X,R,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(M,sK15_skl(E,R,X,A))],[f162]) ).
fof(f164,plain,
! [X0,X1,X2,X3] :
( member(X0,X1)
| ~ greatest_lower_bound(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f165,plain,
! [X0,X1,X2,X3] :
( lower_bound(X0,X2,X1)
| ~ greatest_lower_bound(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f166,plain,
! [X0,X1,X2,X3,X4] :
( apply(X2,X4,X0)
| ~ lower_bound(X4,X2,X1)
| ~ member(X4,X3)
| ~ greatest_lower_bound(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f167,plain,
! [X0,X1,X2,X3] :
( member(sK15_skl(X3,X2,X1,X0),X3)
| ~ lower_bound(X0,X2,X1)
| ~ member(X0,X1)
| greatest_lower_bound(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f168,plain,
! [X0,X1,X2,X3] :
( lower_bound(sK15_skl(X3,X2,X1,X0),X2,X1)
| ~ lower_bound(X0,X2,X1)
| ~ member(X0,X1)
| greatest_lower_bound(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f169,plain,
! [X0,X1,X2,X3] :
( ~ apply(X2,sK15_skl(X3,X2,X1,X0),X0)
| ~ lower_bound(X0,X2,X1)
| ~ member(X0,X1)
| greatest_lower_bound(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f170,plain,
? [R,E] :
( ? [X] :
( ? [M] :
( least(M,R,X)
<~> ( greatest_lower_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] :
( ( ~ greatest_lower_bound(M,X,R,E)
| ~ member(M,X)
| ~ least(M,R,X) )
& ( ( greatest_lower_bound(M,X,R,E)
& member(M,X) )
| least(M,R,X) ) )
& subset(X,E) )
& order(R,E) ),
inference(NNF_transformation,[status(thm)],[f170]) ).
fof(f172,plain,
( ( ~ greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)
| ~ member(sK19_skl,sK18_skl)
| ~ least(sK19_skl,sK16_skl,sK18_skl) )
& ( ( greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)
& member(sK19_skl,sK18_skl) )
| least(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)
| least(sK19_skl,sK16_skl,sK18_skl) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f176,plain,
( greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)
| least(sK19_skl,sK16_skl,sK18_skl) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f177,plain,
( ~ greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)
| ~ member(sK19_skl,sK18_skl)
| ~ least(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(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(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
<=> least(sK19_skl,sK16_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f196,plain,
( ~ sQ0_spl
| least(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
<=> greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f203,plain,
( ~ sQ2_spl
| greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f202]) ).
fof(f204,plain,
( sQ2_spl
| ~ greatest_lower_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)],[f128,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
| lower_bound(sK19_skl,sK16_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f165,f203]) ).
fof(f249,plain,
! [X0] :
( ~ sQ2_spl
| apply(sK16_skl,X0,sK19_skl)
| ~ lower_bound(X0,sK16_skl,sK18_skl)
| ~ member(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f166,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(f284,plain,
( ~ sQ2_spl
| apply(sK16_skl,sK19_skl,sK19_skl)
| ~ member(sK19_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f249,f248]) ).
fof(f285,definition,
( sQ7_spl
<=> member(sK19_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f287,plain,
( sQ7_spl
| ~ member(sK19_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f285]) ).
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(f291,plain,
( ~ sQ2_spl
| sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f284,f285,f288,f202]) ).
fof(f292,plain,
! [X0] :
( ~ sQ0_spl
| apply(sK16_skl,sK19_skl,X0)
| ~ member(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f196,f129]) ).
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] :
( ~ sQ0_spl
| ~ member(sK9_skl(sK19_skl,X0,sK16_skl),sK18_skl)
| lower_bound(sK19_skl,sK16_skl,X0) ),
inference(resolution,[status(thm)],[f115,f292]) ).
fof(f347,plain,
! [X0] : ~ member(X0,sum(empty_set)),
inference(resolution,[status(thm)],[f68,f50]) ).
fof(f348,plain,
! [X0,X1,X2] :
( member(sK1_skl(X1,X0),X2)
| ~ subset(X1,X2)
| ~ member(X0,sum(X1)) ),
inference(resolution,[status(thm)],[f68,f28]) ).
fof(f360,plain,
! [X0,X1] :
( ~ subset(X1,empty_set)
| ~ member(X0,sum(X1)) ),
inference(resolution,[status(thm)],[f348,f50]) ).
fof(f366,plain,
! [X0,X1,X2] :
( ~ member(X2,X1)
| ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f360,f70]) ).
fof(f370,plain,
! [X0] :
( ~ sQ1_spl
| ~ member(X0,sK19_skl)
| ~ subset(sK17_skl,empty_set) ),
inference(resolution,[status(thm)],[f366,f264]) ).
fof(f371,plain,
! [X0] :
( ~ sQ1_spl
| ~ member(X0,sK19_skl)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f366,f199]) ).
fof(f395,plain,
! [X0,X1,X2,X3] :
( ~ subset(X2,X1)
| subset(X2,X3)
| ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f366,f213]) ).
fof(f396,plain,
! [X0,X1,X2] :
( subset(X1,X2)
| ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f366,f29]) ).
fof(f408,definition,
( sQ11_spl
<=> subset(sK17_skl,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f411,definition,
! [X0] :
( sQ12_spl
<=> ~ member(X0,sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f412,plain,
! [X0] :
( ~ sQ12_spl
| ~ member(X0,sK19_skl) ),
inference(component_clause,[status(thm)],[f411]) ).
fof(f414,plain,
( ~ sQ1_spl
| sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f370,f408,f411,f198]) ).
fof(f415,definition,
( sQ13_spl
<=> subset(sK18_skl,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f418,plain,
( ~ sQ1_spl
| sQ12_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f371,f415,f411,f198]) ).
fof(f420,plain,
( sQ7_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f287,f264]) ).
fof(f421,plain,
( sQ7_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f420]) ).
fof(f425,plain,
! [X0,X1] :
( ~ sQ12_spl
| ~ subset(X1,sK19_skl)
| ~ member(X0,sum(X1)) ),
inference(resolution,[status(thm)],[f412,f348]) ).
fof(f433,plain,
! [X0] :
( ~ sQ2_spl
| apply(sK16_skl,sK19_skl,X0)
| ~ member(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f248,f113]) ).
fof(f447,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(f449,plain,
! [X0] : member(X0,product(empty_set)),
inference(resolution,[status(thm)],[f76,f50]) ).
fof(f452,plain,
! [X0,X1,X2] :
( member(sK2_skl(X1,X0),X2)
| ~ subset(X1,X2)
| member(X0,product(X1)) ),
inference(resolution,[status(thm)],[f76,f28]) ).
fof(f481,plain,
! [X0,X1,X2] :
( ~ sQ12_spl
| ~ member(X2,X1)
| ~ member(X1,X0)
| ~ subset(X0,sK19_skl) ),
inference(resolution,[status(thm)],[f425,f70]) ).
fof(f495,plain,
! [X0,X1,X2] :
( ~ member(X1,X2)
| ~ subset(X2,empty_set)
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f86,f366]) ).
fof(f497,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(f543,plain,
! [X0,X1] :
( ~ subset(X1,empty_set)
| member(X0,product(X1)) ),
inference(resolution,[status(thm)],[f452,f50]) ).
fof(f557,plain,
! [X0,X1,X2,X3] :
( ~ member(sK3_skl(X1,X0),X3)
| ~ subset(X1,difference(X2,X3))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f497,f54]) ).
fof(f566,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)],[f497,f366]) ).
fof(f569,plain,
! [X0,X1,X2,X3] :
( member(sK3_skl(X1,X0),X3)
| ~ subset(X2,X3)
| ~ subset(X1,X2)
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f497,f28]) ).
fof(f571,plain,
! [X0] :
( ~ sQ2_spl
| sP1_prd(sK19_skl,X0,sK16_skl)
| ~ member(sK19_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f433,f194]) ).
fof(f573,plain,
( ~ sQ2_spl
| sQ10_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f571,f198,f319,f202]) ).
fof(f578,plain,
! [X0] :
( ~ sQ0_spl
| lower_bound(sK19_skl,sK16_skl,X0)
| ~ member(sK9_skl(sK19_skl,X0,sK16_skl),sK18_skl) ),
inference(resolution,[status(thm)],[f292,f115]) ).
fof(f591,plain,
! [X0] :
( ~ sQ1_spl
| subset(sK19_skl,X0)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f396,f199]) ).
fof(f604,definition,
! [X0] :
( sQ14_spl
<=> subset(sK19_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f605,plain,
! [X0] :
( ~ sQ14_spl
| subset(sK19_skl,X0) ),
inference(component_clause,[status(thm)],[f604]) ).
fof(f608,plain,
( ~ sQ1_spl
| sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f591,f415,f604,f198]) ).
fof(f667,plain,
! [X0,X1,X2] :
( ~ member(X1,X2)
| ~ subset(X2,empty_set)
| ~ order(X0,X1)
| total_order(X0,X1) ),
inference(resolution,[status(thm)],[f98,f366]) ).
fof(f669,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(f685,plain,
! [X0] :
( ~ sQ10_spl
| apply(sK16_skl,sK19_skl,sK19_skl)
| ~ member(sK19_skl,X0) ),
inference(resolution,[status(thm)],[f320,f192]) ).
fof(f686,definition,
! [X0] :
( sQ15_spl
<=> ~ member(sK19_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f687,plain,
! [X0] :
( ~ sQ15_spl
| ~ member(sK19_skl,X0) ),
inference(component_clause,[status(thm)],[f686]) ).
fof(f689,plain,
( ~ sQ10_spl
| sQ8_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f685,f686,f288,f319]) ).
fof(f702,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(f736,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ subset(X0,sK19_skl)
| subset(X0,X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f395,f199]) ).
fof(f749,definition,
! [X0,X1] :
( sQ16_spl
<=> ( ~ subset(X0,sK19_skl)
| subset(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f753,plain,
( ~ sQ1_spl
| sQ16_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f736,f415,f749,f198]) ).
fof(f770,plain,
! [X0] :
( ~ sQ1_spl
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK19_skl,X0)
| order(X0,sK19_skl) ),
inference(resolution,[status(thm)],[f495,f199]) ).
fof(f783,definition,
! [X0] :
( sQ17_spl
<=> ( ~ sP0_prd(sK19_skl,X0)
| order(X0,sK19_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f787,plain,
( ~ sQ1_spl
| ~ sQ13_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f770,f783,f415,f198]) ).
fof(f799,plain,
! [X0] :
( ~ member(sK17_skl,X0)
| ~ subset(X0,empty_set)
| total_order(sK16_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f667,f173]) ).
fof(f800,definition,
( sQ18_spl
<=> total_order(sK16_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f801,plain,
( ~ sQ18_spl
| total_order(sK16_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f800]) ).
fof(f803,definition,
! [X0] :
( sQ19_spl
<=> ( ~ member(sK17_skl,X0)
| ~ subset(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f806,plain,
( sQ19_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f799,f800,f803]) ).
fof(f822,plain,
! [X0,X1,X2,X3] :
( ~ member(X2,X3)
| ~ subset(X3,empty_set)
| lower_bound(X0,X1,X2) ),
inference(resolution,[status(thm)],[f114,f366]) ).
fof(f824,plain,
! [X0,X1,X2,X3] :
( member(sK9_skl(X0,X2,X1),X3)
| ~ subset(X2,X3)
| lower_bound(X0,X1,X2) ),
inference(resolution,[status(thm)],[f114,f28]) ).
fof(f843,plain,
! [X0,X1] :
( ~ sQ2_spl
| apply(sK16_skl,X1,sK19_skl)
| ~ member(X1,sK17_skl)
| ~ member(sK18_skl,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f822,f249]) ).
fof(f845,definition,
! [X0] :
( sQ20_spl
<=> ( ~ member(sK18_skl,X0)
| ~ subset(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f848,definition,
! [X1] :
( sQ21_spl
<=> ( apply(sK16_skl,X1,sK19_skl)
| ~ member(X1,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f851,plain,
( ~ sQ2_spl
| sQ21_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f843,f845,f848,f202]) ).
fof(f865,plain,
! [X0,X1] :
( ~ subset(X1,empty_set)
| ~ order(X0,X1)
| total_order(X0,X1) ),
inference(resolution,[status(thm)],[f669,f50]) ).
fof(f882,plain,
( ~ subset(sK17_skl,empty_set)
| total_order(sK16_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f865,f173]) ).
fof(f883,plain,
( ~ sQ11_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f882,f800,f408]) ).
fof(f911,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)],[f566,f252]) ).
fof(f935,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ subset(sK18_skl,empty_set)
| ~ subset(X1,sK19_skl)
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f566,f199]) ).
fof(f949,definition,
! [X0] :
( sQ22_spl
<=> ( ~ sP0_prd(empty_set,X0)
| order(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f960,definition,
! [X0] :
( sQ25_spl
<=> ( ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f963,plain,
( ~ sQ5_spl
| sQ20_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f911,f960,f845,f239]) ).
fof(f969,definition,
! [X0,X1] :
( sQ27_spl
<=> ( ~ subset(X1,sK19_skl)
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f973,plain,
( ~ sQ1_spl
| ~ sQ13_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f935,f969,f415,f198]) ).
fof(f1048,plain,
( ~ sQ0_spl
| lower_bound(sK19_skl,sK16_skl,sK18_skl)
| lower_bound(sK19_skl,sK16_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f338,f114]) ).
fof(f1049,definition,
( sQ28_spl
<=> lower_bound(sK19_skl,sK16_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f1051,plain,
( sQ28_spl
| ~ lower_bound(sK19_skl,sK16_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f1049]) ).
fof(f1052,plain,
( ~ sQ0_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f1048,f1049,f195]) ).
fof(f1103,plain,
! [X0] :
( ~ sQ2_spl
| ~ member(sK19_skl,X0)
| least(sK19_skl,sK16_skl,X0)
| ~ member(sK11_skl(sK19_skl,X0,sK16_skl),sK18_skl) ),
inference(resolution,[status(thm)],[f433,f131]) ).
fof(f1185,plain,
! [X0] :
( ~ sQ0_spl
| ~ subset(X0,sK18_skl)
| lower_bound(sK19_skl,sK16_skl,X0)
| lower_bound(sK19_skl,sK16_skl,X0) ),
inference(resolution,[status(thm)],[f578,f824]) ).
fof(f1187,plain,
! [X0] :
( ~ sQ0_spl
| ~ subset(X0,sK18_skl)
| lower_bound(sK19_skl,sK16_skl,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1185]) ).
fof(f1189,plain,
! [X0,X1] :
( ~ sQ0_spl
| apply(sK16_skl,sK19_skl,X1)
| ~ member(X1,X0)
| ~ subset(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f1187,f113]) ).
fof(f1239,definition,
! [X0] :
( sQ29_spl
<=> ( ~ member(sK19_skl,X0)
| ~ subset(X0,sK18_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f1240,plain,
! [X0] :
( ~ sQ29_spl
| ~ member(sK19_skl,X0)
| ~ subset(X0,sK18_skl) ),
inference(component_clause,[status(thm)],[f1239]) ).
fof(f1249,plain,
! [X0,X1,X2,X3] :
( ~ subset(X3,empty_set)
| ~ lower_bound(X0,X2,X1)
| ~ member(X0,X1)
| greatest_lower_bound(X0,X1,X2,sum(X3)) ),
inference(resolution,[status(thm)],[f167,f360]) ).
fof(f1266,plain,
! [X0,X1,X2,X3,X4] :
( apply(X2,sK15_skl(X3,X2,X1,X0),X4)
| ~ member(X4,X1)
| ~ lower_bound(X0,X2,X1)
| ~ member(X0,X1)
| greatest_lower_bound(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f168,f113]) ).
fof(f1302,plain,
! [X0,X1,X2,X3] :
( lower_bound(X0,X2,X1)
| ~ subset(X3,empty_set)
| ~ lower_bound(X0,X2,X1)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f1249,f165]) ).
fof(f1303,plain,
! [X0,X1,X2,X3] :
( member(X0,X1)
| ~ subset(X3,empty_set)
| ~ lower_bound(X0,X2,X1)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f1249,f164]) ).
fof(f1304,definition,
! [X0,X1,X2] :
( sQ33_spl
<=> ( lower_bound(X0,X2,X1)
| ~ lower_bound(X0,X2,X1)
| ~ member(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f1307,definition,
! [X3] :
( sQ34_spl
<=> ~ subset(X3,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f1308,plain,
! [X0] :
( ~ sQ34_spl
| ~ subset(X0,empty_set) ),
inference(component_clause,[status(thm)],[f1307]) ).
fof(f1310,plain,
( sQ34_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f1302,f1304,f1307]) ).
fof(f1311,definition,
! [X0,X1,X2] :
( sQ35_spl
<=> ( member(X0,X1)
| ~ lower_bound(X0,X2,X1)
| ~ member(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f1314,plain,
( sQ34_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f1303,f1311,f1307]) ).
fof(f1343,plain,
( ~ sQ34_spl
| $false ),
inference(resolution,[status(thm)],[f1308,f294]) ).
fof(f1345,plain,
~ sQ34_spl,
inference(contradiction_clause,[status(thm)],[f1343]) ).
fof(f1371,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(f1373,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ member(X1,sK18_skl)
| X1 = sK19_skl
| ~ apply(sK16_skl,X1,sK19_skl)
| ~ member(sK19_skl,X0)
| ~ member(X1,X0)
| ~ sP0_prd(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f184,f292]) ).
fof(f1380,definition,
! [X0] :
( sQ36_spl
<=> ( ~ member(sK19_skl,X0)
| ~ member(sK19_skl,X0)
| ~ sP0_prd(X0,sK16_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1381,plain,
! [X0] :
( ~ sQ36_spl
| ~ member(sK19_skl,X0)
| ~ member(sK19_skl,X0)
| ~ sP0_prd(X0,sK16_skl) ),
inference(component_clause,[status(thm)],[f1380]) ).
fof(f1383,definition,
( sQ37_spl
<=> sK19_skl = sK19_skl ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1386,plain,
( sQ37_spl
| ~ sQ8_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f1371,f1380,f288,f1383]) ).
fof(f1455,plain,
( ~ sQ1_spl
| ~ sQ15_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f264,f687]) ).
fof(f1467,plain,
( ~ sQ1_spl
| ~ sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f1455]) ).
fof(f1468,plain,
! [X0] :
( ~ sQ36_spl
| ~ member(sK19_skl,X0)
| ~ sP0_prd(X0,sK16_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f1381]) ).
fof(f1486,plain,
( ~ sQ1_spl
| ~ sQ36_spl
| ~ sP0_prd(sK17_skl,sK16_skl) ),
inference(resolution,[status(thm)],[f1468,f264]) ).
fof(f1497,plain,
( ~ sQ1_spl
| ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1486,f210]) ).
fof(f1498,plain,
( ~ sQ1_spl
| ~ sQ36_spl ),
inference(contradiction_clause,[status(thm)],[f1497]) ).
fof(f1643,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)],[f366,f497]) ).
fof(f1757,plain,
! [X0,X1,X2] :
( subset(X0,X1)
| ~ subset(X2,X1)
| ~ subset(X0,X2)
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f274,f30]) ).
fof(f1776,plain,
! [X0,X1,X2] :
( ~ subset(X2,X1)
| ~ subset(X0,X2)
| subset(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f1757]) ).
fof(f1780,plain,
! [X0] :
( ~ sQ5_spl
| ~ subset(X0,sK17_skl)
| subset(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f1776,f252]) ).
fof(f1781,plain,
! [X0] :
( ~ subset(X0,sK18_skl)
| subset(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f1776,f174]) ).
fof(f1793,plain,
! [X0,X1] :
( subset(intersection(X0,X1),X0)
| subset(intersection(X0,X1),X0) ),
inference(resolution,[status(thm)],[f258,f30]) ).
fof(f1803,plain,
! [X0,X1] : subset(intersection(empty_set,X0),X1),
inference(resolution,[status(thm)],[f258,f50]) ).
fof(f1808,plain,
! [X0,X1] : subset(intersection(X0,X1),X0),
inference(duplicate_literals_removal,[status(thm)],[f1793]) ).
fof(f1809,plain,
! [X0,X1] :
( subset(intersection(X0,X1),X1)
| subset(intersection(X0,X1),X1) ),
inference(resolution,[status(thm)],[f259,f30]) ).
fof(f1819,plain,
! [X0,X1] : subset(intersection(X0,empty_set),X1),
inference(resolution,[status(thm)],[f259,f50]) ).
fof(f1824,plain,
! [X0,X1] : subset(intersection(X0,X1),X1),
inference(duplicate_literals_removal,[status(thm)],[f1809]) ).
fof(f1868,plain,
! [X0] : subset(intersection(sK18_skl,X0),sK17_skl),
inference(resolution,[status(thm)],[f1808,f1781]) ).
fof(f1869,plain,
! [X0] :
( ~ sQ5_spl
| subset(intersection(sK17_skl,X0),sK18_skl) ),
inference(resolution,[status(thm)],[f1808,f1780]) ).
fof(f1881,plain,
! [X0] :
( ~ sQ5_spl
| subset(intersection(X0,sK17_skl),sK18_skl) ),
inference(resolution,[status(thm)],[f1824,f1780]) ).
fof(f1923,plain,
! [X0,X1,X2] :
( ~ subset(X0,X1)
| subset(X0,union(X1,X2))
| subset(X0,union(X1,X2)) ),
inference(resolution,[status(thm)],[f278,f213]) ).
fof(f1924,plain,
! [X0,X1] :
( subset(X0,union(X0,X1))
| subset(X0,union(X0,X1)) ),
inference(resolution,[status(thm)],[f278,f29]) ).
fof(f1935,plain,
! [X0,X1,X2] :
( ~ subset(X0,X1)
| subset(X0,union(X1,X2)) ),
inference(duplicate_literals_removal,[status(thm)],[f1923]) ).
fof(f1936,plain,
! [X0,X1] : subset(X0,union(X0,X1)),
inference(duplicate_literals_removal,[status(thm)],[f1924]) ).
fof(f1941,plain,
! [X0,X1,X2] :
( ~ subset(X0,X2)
| subset(X0,union(X1,X2))
| subset(X0,union(X1,X2)) ),
inference(resolution,[status(thm)],[f281,f213]) ).
fof(f1942,plain,
! [X0,X1] :
( subset(X0,union(X1,X0))
| subset(X0,union(X1,X0)) ),
inference(resolution,[status(thm)],[f281,f29]) ).
fof(f1953,plain,
! [X0,X1,X2] :
( ~ subset(X0,X2)
| subset(X0,union(X1,X2)) ),
inference(duplicate_literals_removal,[status(thm)],[f1941]) ).
fof(f1954,plain,
! [X0,X1] : subset(X0,union(X1,X0)),
inference(duplicate_literals_removal,[status(thm)],[f1942]) ).
fof(f1955,plain,
! [X0,X1] :
( member(X0,sK17_skl)
| ~ member(X0,X1)
| ~ member(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f1868,f263]) ).
fof(f1959,plain,
! [X0,X1] :
( ~ sQ5_spl
| member(X0,sK18_skl)
| ~ member(X0,X1)
| ~ member(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f1869,f263]) ).
fof(f1993,plain,
! [X0] :
( ~ sQ1_spl
| member(sK19_skl,union(sK18_skl,X0)) ),
inference(resolution,[status(thm)],[f1936,f219]) ).
fof(f2007,plain,
! [X0] :
( ~ sQ1_spl
| member(sK19_skl,union(X0,sK18_skl)) ),
inference(resolution,[status(thm)],[f1954,f219]) ).
fof(f2025,plain,
! [X0,X1,X2] :
( subset(difference(X0,X1),union(X2,X0))
| subset(difference(X0,X1),union(X2,X0)) ),
inference(resolution,[status(thm)],[f298,f281]) ).
fof(f2026,plain,
! [X0,X1,X2] :
( subset(difference(X0,X1),union(X0,X2))
| subset(difference(X0,X1),union(X0,X2)) ),
inference(resolution,[status(thm)],[f298,f278]) ).
fof(f2029,plain,
! [X0,X1] :
( subset(difference(X0,X1),X0)
| subset(difference(X0,X1),X0) ),
inference(resolution,[status(thm)],[f298,f30]) ).
fof(f2044,plain,
! [X0,X1,X2] : subset(difference(X0,X1),union(X2,X0)),
inference(duplicate_literals_removal,[status(thm)],[f2025]) ).
fof(f2045,plain,
! [X0,X1,X2] : subset(difference(X0,X1),union(X0,X2)),
inference(duplicate_literals_removal,[status(thm)],[f2026]) ).
fof(f2048,plain,
! [X0,X1] : subset(difference(X0,X1),X0),
inference(duplicate_literals_removal,[status(thm)],[f2029]) ).
fof(f2049,plain,
! [X0,X1] :
( subset(difference(X0,X0),X1)
| subset(difference(X0,X0),X1) ),
inference(resolution,[status(thm)],[f300,f298]) ).
fof(f2051,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(f2058,plain,
! [X0,X1] : subset(difference(X0,X0),X1),
inference(duplicate_literals_removal,[status(thm)],[f2049]) ).
fof(f2060,plain,
! [X0,X1,X2] :
( ~ subset(difference(X0,X1),X1)
| subset(difference(X0,X1),X2) ),
inference(duplicate_literals_removal,[status(thm)],[f2051]) ).
fof(f2091,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ member(X1,sK19_skl)
| ~ subset(union(sK18_skl,X0),empty_set) ),
inference(resolution,[status(thm)],[f1993,f366]) ).
fof(f2094,definition,
! [X0] :
( sQ38_spl
<=> member(sK19_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f2095,plain,
! [X0] :
( ~ sQ38_spl
| member(sK19_skl,X0) ),
inference(component_clause,[status(thm)],[f2094]) ).
fof(f2098,definition,
! [X0] :
( sQ39_spl
<=> ~ subset(union(sK18_skl,X0),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f2101,plain,
( ~ sQ1_spl
| sQ12_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f2091,f2098,f411,f198]) ).
fof(f2313,plain,
! [X0] : subset(difference(sK18_skl,X0),sK17_skl),
inference(resolution,[status(thm)],[f2048,f1781]) ).
fof(f2314,plain,
! [X0] :
( ~ sQ5_spl
| subset(difference(sK17_skl,X0),sK18_skl) ),
inference(resolution,[status(thm)],[f2048,f1780]) ).
fof(f2317,plain,
! [X0,X1] : subset(difference(empty_set,X0),X1),
inference(resolution,[status(thm)],[f2048,f273]) ).
fof(f2489,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ member(X1,sK19_skl)
| ~ subset(union(X0,sK18_skl),empty_set) ),
inference(resolution,[status(thm)],[f2007,f366]) ).
fof(f2493,definition,
! [X0] :
( sQ40_spl
<=> ~ subset(union(X0,sK18_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f2496,plain,
( ~ sQ1_spl
| sQ12_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f2489,f2493,f411,f198]) ).
fof(f2607,plain,
! [X0,X1] :
( member(X0,sK17_skl)
| member(X0,X1)
| ~ member(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f2313,f304]) ).
fof(f2611,plain,
! [X0,X1] :
( ~ sQ5_spl
| member(X0,sK18_skl)
| member(X0,X1)
| ~ member(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f2314,f304]) ).
fof(f2676,plain,
! [X0] : subset(sum(empty_set),X0),
inference(resolution,[status(thm)],[f347,f29]) ).
fof(f3208,plain,
! [X0,X1] :
( ~ member(X0,X1)
| ~ subset(product(empty_set),empty_set) ),
inference(resolution,[status(thm)],[f449,f366]) ).
fof(f3212,definition,
( sQ41_spl
<=> subset(product(empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f3215,definition,
! [X0,X1] :
( sQ42_spl
<=> ~ member(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f3216,plain,
! [X0,X1] :
( ~ sQ42_spl
| ~ member(X0,X1) ),
inference(component_clause,[status(thm)],[f3215]) ).
fof(f3218,plain,
( sQ42_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f3208,f3212,f3215]) ).
fof(f3219,definition,
! [X0,X1] :
( sQ43_spl
<=> subset(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f3220,plain,
! [X0,X1] :
( ~ sQ43_spl
| subset(X0,X1) ),
inference(component_clause,[status(thm)],[f3219]) ).
fof(f3258,plain,
! [X0,X1] :
( ~ sQ1_spl
| member(sK19_skl,union(X0,X1))
| ~ subset(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f1935,f219]) ).
fof(f3357,plain,
! [X0,X1] :
( ~ sQ1_spl
| member(sK19_skl,union(X1,X0))
| ~ subset(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f1953,f219]) ).
fof(f3562,plain,
! [X0,X1] :
( ~ sQ12_spl
| ~ member(X0,X1)
| ~ subset(product(empty_set),sK19_skl) ),
inference(resolution,[status(thm)],[f481,f449]) ).
fof(f3678,definition,
( sQ48_spl
<=> subset(product(empty_set),sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f3681,plain,
( ~ sQ12_spl
| sQ42_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f3562,f3678,f3215,f411]) ).
fof(f3701,plain,
! [X0,X1,X2] :
( ~ sQ42_spl
| member(sK2_skl(intersection(X0,X1),X2),X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f447,f3216]) ).
fof(f3763,plain,
( ~ sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3701,f3216]) ).
fof(f3764,plain,
~ sQ42_spl,
inference(contradiction_clause,[status(thm)],[f3763]) ).
fof(f3844,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ subset(sK18_skl,X1)
| ~ member(X2,sK19_skl)
| ~ subset(union(X0,X1),empty_set) ),
inference(resolution,[status(thm)],[f366,f3357]) ).
fof(f3845,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ subset(sK18_skl,X0)
| ~ member(X2,sK19_skl)
| ~ subset(union(X0,X1),empty_set) ),
inference(resolution,[status(thm)],[f366,f3258]) ).
fof(f3885,definition,
! [X0,X1] :
( sQ49_spl
<=> ( ~ subset(sK18_skl,X1)
| ~ subset(union(X0,X1),empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f3888,plain,
( ~ sQ1_spl
| sQ12_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f3844,f3885,f411,f198]) ).
fof(f3889,definition,
! [X0,X1] :
( sQ50_spl
<=> ( ~ subset(sK18_skl,X0)
| ~ subset(union(X0,X1),empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f3892,plain,
( ~ sQ1_spl
| sQ12_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f3845,f3889,f411,f198]) ).
fof(f3914,definition,
! [X0] :
( sQ51_spl
<=> ( ~ member(sK19_skl,X0)
| ~ sP0_prd(X0,sK16_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f3915,plain,
! [X0] :
( ~ sQ51_spl
| ~ member(sK19_skl,X0)
| ~ sP0_prd(X0,sK16_skl) ),
inference(component_clause,[status(thm)],[f3914]) ).
fof(f3982,plain,
! [X0] :
( ~ sQ5_spl
| subset(difference(sK17_skl,sK18_skl),X0) ),
inference(resolution,[status(thm)],[f2060,f2314]) ).
fof(f3983,plain,
! [X0] : subset(difference(sK18_skl,sK17_skl),X0),
inference(resolution,[status(thm)],[f2060,f2313]) ).
fof(f3984,plain,
! [X0,X1,X2] : subset(difference(X0,union(X0,X1)),X2),
inference(resolution,[status(thm)],[f2060,f2045]) ).
fof(f3985,plain,
! [X0,X1,X2] : subset(difference(X0,union(X1,X0)),X2),
inference(resolution,[status(thm)],[f2060,f2044]) ).
fof(f4065,plain,
! [X0] :
( member(X0,sK17_skl)
| ~ member(X0,sK18_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2607,f1955]) ).
fof(f4075,plain,
! [X0] :
( ~ sQ5_spl
| member(X0,sK18_skl)
| ~ member(X0,sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2611,f1959]) ).
fof(f4117,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ member(sK19_skl,sK18_skl)
| sK19_skl = sK19_skl
| ~ member(sK19_skl,X1)
| ~ member(sK19_skl,X1)
| ~ sP0_prd(X1,sK16_skl)
| ~ member(sK19_skl,X0)
| ~ subset(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f1189,f1373]) ).
fof(f4130,plain,
( ~ sQ0_spl
| ~ sQ1_spl
| sQ37_spl
| sQ36_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f4117,f1239,f1380,f1383,f198,f195]) ).
fof(f4559,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ subset(sK18_skl,X1)
| member(sK19_skl,X1)
| member(sK19_skl,X0) ),
inference(resolution,[status(thm)],[f47,f3357]) ).
fof(f4571,definition,
! [X1] :
( sQ54_spl
<=> ( ~ subset(sK18_skl,X1)
| member(sK19_skl,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f4574,plain,
( ~ sQ1_spl
| sQ54_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f4559,f2094,f4571,f198]) ).
fof(f4592,plain,
( ~ sQ38_spl
| $false ),
inference(resolution,[status(thm)],[f2095,f50]) ).
fof(f4608,plain,
~ sQ38_spl,
inference(contradiction_clause,[status(thm)],[f4592]) ).
fof(f4875,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)],[f566,f2314]) ).
fof(f4891,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)],[f566,f1869]) ).
fof(f4893,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)],[f566,f1881]) ).
fof(f4980,definition,
! [X0] :
( sQ56_spl
<=> ( ~ sP0_prd(difference(sK17_skl,sK18_skl),X0)
| order(X0,difference(sK17_skl,sK18_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f4988,definition,
! [X0,X1] :
( sQ58_spl
<=> ( ~ sP0_prd(difference(sK17_skl,X1),X0)
| order(X0,difference(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f4991,plain,
( ~ sQ5_spl
| sQ20_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f4875,f4988,f845,f239]) ).
fof(f4992,definition,
! [X0] :
( sQ59_spl
<=> ( ~ sP0_prd(difference(sK18_skl,sK17_skl),X0)
| order(X0,difference(sK18_skl,sK17_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f5004,definition,
! [X0,X1,X2] :
( sQ62_spl
<=> ( ~ sP0_prd(difference(X1,union(X2,X1)),X0)
| order(X0,difference(X1,union(X2,X1))) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f5008,definition,
! [X0,X1,X2] :
( sQ63_spl
<=> ( ~ sP0_prd(difference(X1,union(X1,X2)),X0)
| order(X0,difference(X1,union(X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f5016,definition,
! [X0,X1] :
( sQ65_spl
<=> ( ~ sP0_prd(difference(X1,X1),X0)
| order(X0,difference(X1,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f5020,definition,
! [X0,X1] :
( sQ66_spl
<=> ( ~ sP0_prd(intersection(sK17_skl,X1),X0)
| order(X0,intersection(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f5023,plain,
( ~ sQ5_spl
| sQ20_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f4891,f5020,f845,f239]) ).
fof(f5028,definition,
! [X0,X1] :
( sQ68_spl
<=> ( ~ sP0_prd(intersection(X1,sK17_skl),X0)
| order(X0,intersection(X1,sK17_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f5031,plain,
( ~ sQ5_spl
| sQ20_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f4893,f5028,f845,f239]) ).
fof(f5036,definition,
! [X0,X1] :
( sQ70_spl
<=> ( ~ sP0_prd(intersection(X1,empty_set),X0)
| order(X0,intersection(X1,empty_set)) ) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f5120,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,f4075]) ).
fof(f5121,plain,
! [X0] :
( member(sK7_skl(sK18_skl,X0),sK17_skl)
| ~ order(X0,sK18_skl)
| total_order(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f99,f4065]) ).
fof(f5134,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,f4075]) ).
fof(f5135,plain,
! [X0] :
( member(sK6_skl(sK18_skl,X0),sK17_skl)
| ~ order(X0,sK18_skl)
| total_order(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f98,f4065]) ).
fof(f5148,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,f4075]) ).
fof(f5156,definition,
! [X0] :
( sQ73_spl
<=> ( ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f5157,plain,
! [X0] :
( ~ sQ73_spl
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl) ),
inference(component_clause,[status(thm)],[f5156]) ).
fof(f5237,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,f4075]) ).
fof(f5251,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,f4075]) ).
fof(f5324,definition,
! [X0] :
( sQ75_spl
<=> ( ~ subset(X0,empty_set)
| ~ subset(sK17_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f5460,definition,
( sQ76_spl
<=> subset(empty_set,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f5462,plain,
( sQ76_spl
| ~ subset(empty_set,empty_set) ),
inference(component_clause,[status(thm)],[f5460]) ).
fof(f5487,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl)
| subset(sK3_skl(sK17_skl,X0),X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f396,f5251]) ).
fof(f5491,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl)
| subset(sK4_skl(sK17_skl,X0),X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f396,f5237]) ).
fof(f5495,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl)
| subset(sK5_skl(sK17_skl,X0),X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f396,f5148]) ).
fof(f5499,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl)
| subset(sK6_skl(sK17_skl,X0),X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f396,f5134]) ).
fof(f5503,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)],[f396,f5120]) ).
fof(f5552,definition,
! [X0,X1] :
( sQ78_spl
<=> ( ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl)
| subset(sK3_skl(sK17_skl,X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f5555,plain,
( ~ sQ5_spl
| sQ78_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5487,f415,f5552,f239]) ).
fof(f5560,definition,
! [X0,X1] :
( sQ80_spl
<=> ( ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl)
| subset(sK4_skl(sK17_skl,X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f5563,plain,
( ~ sQ5_spl
| sQ80_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5491,f415,f5560,f239]) ).
fof(f5568,definition,
! [X0,X1] :
( sQ82_spl
<=> ( ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl)
| subset(sK5_skl(sK17_skl,X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f5571,plain,
( ~ sQ5_spl
| sQ82_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5495,f415,f5568,f239]) ).
fof(f5576,definition,
! [X0,X1] :
( sQ84_spl
<=> ( ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl)
| subset(sK6_skl(sK17_skl,X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f5579,plain,
( ~ sQ5_spl
| sQ84_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5499,f415,f5576,f239]) ).
fof(f5584,definition,
! [X0,X1] :
( sQ86_spl
<=> ( ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl)
| subset(sK7_skl(sK17_skl,X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f5587,plain,
( ~ sQ5_spl
| sQ86_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5503,f415,f5584,f239]) ).
fof(f5619,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X1)
| order(X1,sK17_skl)
| ~ member(X0,sK3_skl(sK17_skl,X1))
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f366,f5251]) ).
fof(f5624,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X1)
| order(X1,sK17_skl)
| ~ member(X0,sK4_skl(sK17_skl,X1))
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f366,f5237]) ).
fof(f5629,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X1)
| order(X1,sK17_skl)
| ~ member(X0,sK5_skl(sK17_skl,X1))
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f366,f5148]) ).
fof(f5634,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ order(X1,sK17_skl)
| total_order(X1,sK17_skl)
| ~ member(X0,sK6_skl(sK17_skl,X1))
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f366,f5134]) ).
fof(f5639,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)],[f366,f5120]) ).
fof(f5716,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)],[f366,f5134]) ).
fof(f5770,definition,
! [X0,X1] :
( sQ88_spl
<=> ( ~ sP0_prd(sK17_skl,X1)
| order(X1,sK17_skl)
| ~ member(X0,sK3_skl(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f5773,plain,
( ~ sQ5_spl
| sQ88_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5619,f415,f5770,f239]) ).
fof(f5778,definition,
! [X0,X1] :
( sQ90_spl
<=> ( ~ sP0_prd(sK17_skl,X1)
| order(X1,sK17_skl)
| ~ member(X0,sK4_skl(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f5781,plain,
( ~ sQ5_spl
| sQ90_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5624,f415,f5778,f239]) ).
fof(f5786,definition,
! [X0,X1] :
( sQ92_spl
<=> ( ~ sP0_prd(sK17_skl,X1)
| order(X1,sK17_skl)
| ~ member(X0,sK5_skl(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f5789,plain,
( ~ sQ5_spl
| sQ92_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5629,f415,f5786,f239]) ).
fof(f5794,definition,
! [X0,X1] :
( sQ94_spl
<=> ( ~ order(X1,sK17_skl)
| total_order(X1,sK17_skl)
| ~ member(X0,sK6_skl(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f5797,plain,
( ~ sQ5_spl
| sQ94_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5634,f415,f5794,f239]) ).
fof(f5802,definition,
! [X0,X1] :
( sQ96_spl
<=> ( ~ order(X1,sK17_skl)
| total_order(X1,sK17_skl)
| ~ member(X0,sK7_skl(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f5805,plain,
( ~ sQ5_spl
| sQ96_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5639,f415,f5802,f239]) ).
fof(f5820,plain,
( ~ sQ5_spl
| sQ73_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f5716,f845,f5156,f239]) ).
fof(f5958,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X2)
| order(X2,sK17_skl)
| ~ subset(X0,sK3_skl(sK17_skl,X2))
| subset(X0,X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f395,f5251]) ).
fof(f5965,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X2)
| order(X2,sK17_skl)
| ~ subset(X0,sK4_skl(sK17_skl,X2))
| subset(X0,X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f395,f5237]) ).
fof(f5969,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X2)
| order(X2,sK17_skl)
| ~ subset(X0,sK5_skl(sK17_skl,X2))
| subset(X0,X1)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f395,f5148]) ).
fof(f5973,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)],[f395,f5134]) ).
fof(f5977,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)],[f395,f5120]) ).
fof(f6026,definition,
! [X0,X1,X2] :
( sQ98_spl
<=> ( ~ sP0_prd(sK17_skl,X2)
| order(X2,sK17_skl)
| ~ subset(X0,sK3_skl(sK17_skl,X2))
| subset(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f6029,plain,
( ~ sQ5_spl
| sQ98_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5958,f415,f6026,f239]) ).
fof(f6034,definition,
! [X0,X1,X2] :
( sQ100_spl
<=> ( ~ sP0_prd(sK17_skl,X2)
| order(X2,sK17_skl)
| ~ subset(X0,sK4_skl(sK17_skl,X2))
| subset(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f6037,plain,
( ~ sQ5_spl
| sQ100_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5965,f415,f6034,f239]) ).
fof(f6042,definition,
! [X0,X1,X2] :
( sQ102_spl
<=> ( ~ sP0_prd(sK17_skl,X2)
| order(X2,sK17_skl)
| ~ subset(X0,sK5_skl(sK17_skl,X2))
| subset(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f6045,plain,
( ~ sQ5_spl
| sQ102_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5969,f415,f6042,f239]) ).
fof(f6050,definition,
! [X0,X1,X2] :
( sQ104_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,[sQ104_spl])],[split_symbol_definition]) ).
fof(f6053,plain,
( ~ sQ5_spl
| sQ104_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5973,f415,f6050,f239]) ).
fof(f6058,definition,
! [X0,X1,X2] :
( sQ106_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,[sQ106_spl])],[split_symbol_definition]) ).
fof(f6061,plain,
( ~ sQ5_spl
| sQ106_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f5977,f415,f6058,f239]) ).
fof(f6162,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X1)
| order(X1,sK17_skl)
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK3_skl(sK17_skl,X1),X0)
| order(X0,sK3_skl(sK17_skl,X1)) ),
inference(resolution,[status(thm)],[f495,f5251]) ).
fof(f6171,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X1)
| order(X1,sK17_skl)
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK4_skl(sK17_skl,X1),X0)
| order(X0,sK4_skl(sK17_skl,X1)) ),
inference(resolution,[status(thm)],[f495,f5237]) ).
fof(f6175,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X1)
| order(X1,sK17_skl)
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK5_skl(sK17_skl,X1),X0)
| order(X0,sK5_skl(sK17_skl,X1)) ),
inference(resolution,[status(thm)],[f495,f5148]) ).
fof(f6179,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ order(X1,sK17_skl)
| total_order(X1,sK17_skl)
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK6_skl(sK17_skl,X1),X0)
| order(X0,sK6_skl(sK17_skl,X1)) ),
inference(resolution,[status(thm)],[f495,f5134]) ).
fof(f6183,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ order(X1,sK17_skl)
| total_order(X1,sK17_skl)
| ~ subset(sK18_skl,empty_set)
| ~ sP0_prd(sK7_skl(sK17_skl,X1),X0)
| order(X0,sK7_skl(sK17_skl,X1)) ),
inference(resolution,[status(thm)],[f495,f5120]) ).
fof(f6232,definition,
! [X0,X1] :
( sQ108_spl
<=> ( ~ sP0_prd(sK17_skl,X1)
| order(X1,sK17_skl)
| ~ sP0_prd(sK3_skl(sK17_skl,X1),X0)
| order(X0,sK3_skl(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f6235,plain,
( ~ sQ5_spl
| ~ sQ13_spl
| sQ108_spl ),
inference(split_clause,[status(thm)],[f6162,f6232,f415,f239]) ).
fof(f6240,definition,
! [X0,X1] :
( sQ110_spl
<=> ( ~ sP0_prd(sK17_skl,X1)
| order(X1,sK17_skl)
| ~ sP0_prd(sK4_skl(sK17_skl,X1),X0)
| order(X0,sK4_skl(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f6243,plain,
( ~ sQ5_spl
| ~ sQ13_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f6171,f6240,f415,f239]) ).
fof(f6248,definition,
! [X0,X1] :
( sQ112_spl
<=> ( ~ sP0_prd(sK17_skl,X1)
| order(X1,sK17_skl)
| ~ sP0_prd(sK5_skl(sK17_skl,X1),X0)
| order(X0,sK5_skl(sK17_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f6251,plain,
( ~ sQ5_spl
| ~ sQ13_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f6175,f6248,f415,f239]) ).
fof(f6256,definition,
! [X0,X1] :
( sQ114_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,[sQ114_spl])],[split_symbol_definition]) ).
fof(f6259,plain,
( ~ sQ5_spl
| ~ sQ13_spl
| sQ114_spl ),
inference(split_clause,[status(thm)],[f6179,f6256,f415,f239]) ).
fof(f6264,definition,
! [X0,X1] :
( sQ116_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,[sQ116_spl])],[split_symbol_definition]) ).
fof(f6267,plain,
( ~ sQ5_spl
| ~ sQ13_spl
| sQ116_spl ),
inference(split_clause,[status(thm)],[f6183,f6264,f415,f239]) ).
fof(f6354,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)],[f1643,f5251]) ).
fof(f6365,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)],[f1643,f5237]) ).
fof(f6370,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)],[f1643,f5148]) ).
fof(f6374,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)],[f1643,f5134]) ).
fof(f6378,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)],[f1643,f5120]) ).
fof(f6427,definition,
! [X0,X1,X2] :
( sQ118_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,[sQ118_spl])],[split_symbol_definition]) ).
fof(f6430,plain,
( ~ sQ5_spl
| sQ118_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f6354,f415,f6427,f239]) ).
fof(f6435,definition,
! [X0,X1,X2] :
( sQ120_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,[sQ120_spl])],[split_symbol_definition]) ).
fof(f6438,plain,
( ~ sQ5_spl
| sQ120_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f6365,f415,f6435,f239]) ).
fof(f6443,definition,
! [X0,X1,X2] :
( sQ122_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,[sQ122_spl])],[split_symbol_definition]) ).
fof(f6446,plain,
( ~ sQ5_spl
| sQ122_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f6370,f415,f6443,f239]) ).
fof(f6451,definition,
! [X0,X1,X2] :
( sQ124_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,[sQ124_spl])],[split_symbol_definition]) ).
fof(f6454,plain,
( ~ sQ5_spl
| sQ124_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f6374,f415,f6451,f239]) ).
fof(f6459,definition,
! [X0,X1,X2] :
( sQ126_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,[sQ126_spl])],[split_symbol_definition]) ).
fof(f6462,plain,
( ~ sQ5_spl
| sQ126_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f6378,f415,f6459,f239]) ).
fof(f6754,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ subset(sK17_skl,X1)
| member(sK19_skl,union(X0,X1)) ),
inference(resolution,[status(thm)],[f275,f1953]) ).
fof(f6755,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ subset(sK17_skl,X0)
| member(sK19_skl,union(X0,X1)) ),
inference(resolution,[status(thm)],[f275,f1935]) ).
fof(f6756,plain,
! [X0] :
( ~ sQ1_spl
| member(sK19_skl,union(X0,sK17_skl)) ),
inference(resolution,[status(thm)],[f275,f1954]) ).
fof(f6757,plain,
! [X0] :
( ~ sQ1_spl
| member(sK19_skl,union(sK17_skl,X0)) ),
inference(resolution,[status(thm)],[f275,f1936]) ).
fof(f6764,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ member(X1,sK19_skl)
| ~ subset(union(X0,sK17_skl),empty_set) ),
inference(resolution,[status(thm)],[f6756,f366]) ).
fof(f6768,definition,
! [X0] :
( sQ133_spl
<=> ~ subset(union(X0,sK17_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f6774,plain,
( ~ sQ1_spl
| sQ12_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f6764,f6768,f411,f198]) ).
fof(f6781,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ member(X1,sK19_skl)
| ~ subset(union(sK17_skl,X0),empty_set) ),
inference(resolution,[status(thm)],[f6757,f366]) ).
fof(f6785,definition,
! [X0] :
( sQ134_spl
<=> ~ subset(union(sK17_skl,X0),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f6791,plain,
( ~ sQ1_spl
| sQ12_spl
| sQ134_spl ),
inference(split_clause,[status(thm)],[f6781,f6785,f411,f198]) ).
fof(f6793,plain,
! [X0,X1] :
( ~ sQ1_spl
| member(sK19_skl,X0)
| member(sK19_skl,X1)
| ~ subset(sK17_skl,X0) ),
inference(resolution,[status(thm)],[f6754,f47]) ).
fof(f6798,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ member(X2,sK19_skl)
| ~ subset(union(X1,X0),empty_set)
| ~ subset(sK17_skl,X0) ),
inference(resolution,[status(thm)],[f6754,f366]) ).
fof(f6801,definition,
! [X0] :
( sQ135_spl
<=> ( member(sK19_skl,X0)
| ~ subset(sK17_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f6804,plain,
( ~ sQ1_spl
| sQ38_spl
| sQ135_spl ),
inference(split_clause,[status(thm)],[f6793,f6801,f2094,f198]) ).
fof(f6805,definition,
! [X0,X1] :
( sQ136_spl
<=> ( ~ subset(union(X1,X0),empty_set)
| ~ subset(sK17_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f6811,plain,
( ~ sQ1_spl
| sQ12_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f6798,f6805,f411,f198]) ).
fof(f6818,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ member(X2,sK19_skl)
| ~ subset(union(X0,X1),empty_set)
| ~ subset(sK17_skl,X0) ),
inference(resolution,[status(thm)],[f6755,f366]) ).
fof(f6822,definition,
! [X0,X1] :
( sQ137_spl
<=> ( ~ subset(union(X0,X1),empty_set)
| ~ subset(sK17_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f6828,plain,
( ~ sQ1_spl
| sQ12_spl
| sQ137_spl ),
inference(split_clause,[status(thm)],[f6818,f6822,f411,f198]) ).
fof(f7091,definition,
! [X0,X1,X2] :
( sQ142_spl
<=> ( ~ subset(X0,X2)
| subset(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f7092,plain,
! [X0,X1,X2] :
( ~ sQ142_spl
| ~ subset(X0,X2)
| subset(X0,X1) ),
inference(component_clause,[status(thm)],[f7091]) ).
fof(f7223,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)],[f702,f101]) ).
fof(f7229,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)],[f7223,f5121]) ).
fof(f7230,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)],[f7223,f5120]) ).
fof(f7259,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)],[f7229]) ).
fof(f7260,plain,
! [X0] :
( ~ total_order(X0,sK17_skl)
| ~ order(X0,sK18_skl)
| total_order(X0,sK18_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f7259,f5135]) ).
fof(f7261,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)],[f7230]) ).
fof(f7262,plain,
! [X0] :
( ~ sQ5_spl
| ~ total_order(X0,sK18_skl)
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f7261,f5134]) ).
fof(f7461,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f543,f75]) ).
fof(f7468,plain,
! [X0,X1,X2] :
( ~ member(X1,X2)
| ~ subset(product(X0),empty_set)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f543,f366]) ).
fof(f7473,plain,
! [X0,X1] :
( ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(forward_subsumption_resolution,[status(thm)],[f7461,f366]) ).
fof(f7474,definition,
! [X0] :
( sQ143_spl
<=> ( ~ subset(product(X0),empty_set)
| ~ subset(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f7480,plain,
( sQ42_spl
| sQ143_spl ),
inference(split_clause,[status(thm)],[f7468,f7474,f3215]) ).
fof(f7509,plain,
! [X0] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f7473,f5251]) ).
fof(f7538,plain,
! [X0] :
( ~ sQ5_spl
| ~ order(X0,sK17_skl)
| total_order(X0,sK17_skl)
| ~ subset(sK18_skl,empty_set) ),
inference(resolution,[status(thm)],[f7473,f5134]) ).
fof(f7539,plain,
! [X0,X1,X2] :
( ~ subset(X2,X0)
| ~ order(X1,X2)
| total_order(X1,X2)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f7473,f669]) ).
fof(f7555,plain,
! [X0,X1,X2,X3] :
( ~ subset(X3,X0)
| lower_bound(X1,X2,X3)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f7473,f824]) ).
fof(f7603,plain,
( ~ sQ5_spl
| sQ25_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f7509,f415,f960,f239]) ).
fof(f7609,plain,
( ~ sQ5_spl
| sQ73_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f7538,f415,f5156,f239]) ).
fof(f7706,plain,
! [X0] :
( ~ subset(sK17_skl,X0)
| total_order(sK16_skl,sK17_skl)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f7539,f173]) ).
fof(f7707,plain,
( sQ18_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f7706,f5324,f800]) ).
fof(f7708,plain,
( ~ sQ18_spl
| ~ order(sK16_skl,sK18_skl)
| total_order(sK16_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f801,f7260]) ).
fof(f7710,definition,
( sQ144_spl
<=> total_order(sK16_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f7711,plain,
( ~ sQ144_spl
| total_order(sK16_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f7710]) ).
fof(f7713,definition,
( sQ145_spl
<=> order(sK16_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f7716,plain,
( ~ sQ18_spl
| ~ sQ145_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f7708,f7710,f7713,f800]) ).
fof(f7754,plain,
( ~ sQ5_spl
| ~ sQ144_spl
| ~ order(sK16_skl,sK17_skl)
| total_order(sK16_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f7711,f7262]) ).
fof(f7756,definition,
( sQ146_spl
<=> order(sK16_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f7758,plain,
( sQ146_spl
| ~ order(sK16_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f7756]) ).
fof(f7759,plain,
( ~ sQ5_spl
| ~ sQ144_spl
| ~ sQ146_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f7754,f800,f7756,f7710,f239]) ).
fof(f7836,definition,
! [X0,X4] :
( sQ148_spl
<=> ( ~ subset(X4,X0)
| ~ subset(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f7837,plain,
! [X0,X1] :
( ~ sQ148_spl
| ~ subset(X1,X0)
| ~ subset(X0,empty_set) ),
inference(component_clause,[status(thm)],[f7836]) ).
fof(f7842,plain,
( sQ146_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7758,f173]) ).
fof(f7843,plain,
sQ146_spl,
inference(contradiction_clause,[status(thm)],[f7842]) ).
fof(f7953,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl)
| ~ subset(sK17_skl,difference(X1,sK18_skl))
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f557,f5251]) ).
fof(f7984,definition,
! [X0] :
( sQ151_spl
<=> ( ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f7987,definition,
! [X1] :
( sQ152_spl
<=> ~ subset(sK17_skl,difference(X1,sK18_skl)) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f7990,plain,
( ~ sQ5_spl
| sQ152_spl
| sQ151_spl ),
inference(split_clause,[status(thm)],[f7953,f7984,f7987,f239]) ).
fof(f8385,plain,
! [X0,X1,X2,X3] :
( ~ subset(X3,empty_set)
| ~ subset(X2,X3)
| ~ subset(X1,X2)
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f569,f7473]) ).
fof(f8410,plain,
! [X0,X1,X2] :
( ~ subset(X2,empty_set)
| ~ subset(X1,X2)
| ~ sP0_prd(sum(empty_set),X0)
| order(X0,sum(empty_set)) ),
inference(resolution,[status(thm)],[f8385,f2676]) ).
fof(f8422,plain,
! [X0,X1,X2,X3] :
( ~ subset(X3,empty_set)
| ~ subset(X2,X3)
| ~ sP0_prd(difference(empty_set,X1),X0)
| order(X0,difference(empty_set,X1)) ),
inference(resolution,[status(thm)],[f8385,f2317]) ).
fof(f8424,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ subset(X2,empty_set)
| ~ subset(X1,X2)
| ~ sP0_prd(difference(sK17_skl,sK18_skl),X0)
| order(X0,difference(sK17_skl,sK18_skl)) ),
inference(resolution,[status(thm)],[f8385,f3982]) ).
fof(f8425,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ subset(X2,empty_set)
| ~ subset(sK18_skl,X2)
| ~ sP0_prd(difference(sK17_skl,X1),X0)
| order(X0,difference(sK17_skl,X1)) ),
inference(resolution,[status(thm)],[f8385,f2314]) ).
fof(f8427,plain,
! [X0,X1,X2] :
( ~ subset(X2,empty_set)
| ~ subset(X1,X2)
| ~ sP0_prd(difference(sK18_skl,sK17_skl),X0)
| order(X0,difference(sK18_skl,sK17_skl)) ),
inference(resolution,[status(thm)],[f8385,f3983]) ).
fof(f8430,plain,
! [X0,X1,X2,X3,X4] :
( ~ subset(X4,empty_set)
| ~ subset(X3,X4)
| ~ sP0_prd(difference(X1,union(X2,X1)),X0)
| order(X0,difference(X1,union(X2,X1))) ),
inference(resolution,[status(thm)],[f8385,f3985]) ).
fof(f8432,plain,
! [X0,X1,X2,X3,X4] :
( ~ subset(X4,empty_set)
| ~ subset(X3,X4)
| ~ sP0_prd(difference(X1,union(X1,X2)),X0)
| order(X0,difference(X1,union(X1,X2))) ),
inference(resolution,[status(thm)],[f8385,f3984]) ).
fof(f8436,plain,
! [X0,X1,X2,X3] :
( ~ subset(X3,empty_set)
| ~ subset(X2,X3)
| ~ sP0_prd(difference(X1,X1),X0)
| order(X0,difference(X1,X1)) ),
inference(resolution,[status(thm)],[f8385,f2058]) ).
fof(f8440,plain,
! [X0,X1,X2,X3] :
( ~ subset(X3,empty_set)
| ~ subset(X2,X3)
| ~ sP0_prd(intersection(empty_set,X1),X0)
| order(X0,intersection(empty_set,X1)) ),
inference(resolution,[status(thm)],[f8385,f1803]) ).
fof(f8441,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ subset(X2,empty_set)
| ~ subset(sK18_skl,X2)
| ~ sP0_prd(intersection(sK17_skl,X1),X0)
| order(X0,intersection(sK17_skl,X1)) ),
inference(resolution,[status(thm)],[f8385,f1869]) ).
fof(f8443,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ subset(X2,empty_set)
| ~ subset(sK18_skl,X2)
| ~ sP0_prd(intersection(X1,sK17_skl),X0)
| order(X0,intersection(X1,sK17_skl)) ),
inference(resolution,[status(thm)],[f8385,f1881]) ).
fof(f8446,plain,
! [X0,X1,X2,X3] :
( ~ subset(X3,empty_set)
| ~ subset(X2,X3)
| ~ sP0_prd(intersection(X1,empty_set),X0)
| order(X0,intersection(X1,empty_set)) ),
inference(resolution,[status(thm)],[f8385,f1819]) ).
fof(f8460,plain,
! [X0,X1,X2] :
( ~ subset(X2,empty_set)
| ~ subset(X1,X2)
| ~ sP0_prd(empty_set,X0)
| order(X0,empty_set) ),
inference(resolution,[status(thm)],[f8385,f294]) ).
fof(f8461,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ subset(X1,empty_set)
| ~ subset(sK18_skl,X1)
| ~ sP0_prd(sK17_skl,X0)
| order(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f8385,f252]) ).
fof(f8481,plain,
! [X0,X1,X2] :
( ~ subset(X2,empty_set)
| ~ subset(X1,sum(empty_set))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f8385,f2676]) ).
fof(f8487,plain,
! [X0,X1,X2,X3] :
( ~ subset(X3,empty_set)
| ~ subset(X1,difference(empty_set,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f8385,f2317]) ).
fof(f8488,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ subset(X2,empty_set)
| ~ subset(X1,difference(sK17_skl,sK18_skl))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f8385,f3982]) ).
fof(f8489,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ subset(sK18_skl,empty_set)
| ~ subset(X1,difference(sK17_skl,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f8385,f2314]) ).
fof(f8490,plain,
! [X0,X1,X2] :
( ~ subset(X2,empty_set)
| ~ subset(X1,difference(sK18_skl,sK17_skl))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f8385,f3983]) ).
fof(f8492,plain,
! [X0,X1,X2,X3,X4] :
( ~ subset(X4,empty_set)
| ~ subset(X1,difference(X2,union(X3,X2)))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f8385,f3985]) ).
fof(f8493,plain,
! [X0,X1,X2,X3,X4] :
( ~ subset(X4,empty_set)
| ~ subset(X1,difference(X2,union(X2,X3)))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f8385,f3984]) ).
fof(f8496,plain,
! [X0,X1,X2,X3] :
( ~ subset(X3,empty_set)
| ~ subset(X1,difference(X2,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f8385,f2058]) ).
fof(f8498,plain,
! [X0,X1,X2,X3] :
( ~ subset(X3,empty_set)
| ~ subset(X1,intersection(empty_set,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f8385,f1803]) ).
fof(f8499,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ subset(sK18_skl,empty_set)
| ~ subset(X1,intersection(sK17_skl,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f8385,f1869]) ).
fof(f8501,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ subset(sK18_skl,empty_set)
| ~ subset(X1,intersection(X2,sK17_skl))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f8385,f1881]) ).
fof(f8503,plain,
! [X0,X1,X2,X3] :
( ~ subset(X3,empty_set)
| ~ subset(X1,intersection(X2,empty_set))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f8385,f1819]) ).
fof(f8513,plain,
! [X0,X1,X2] :
( ~ subset(X2,empty_set)
| ~ subset(X1,empty_set)
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f8385,f294]) ).
fof(f8514,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ subset(sK18_skl,empty_set)
| ~ subset(X1,sK17_skl)
| ~ sP0_prd(X1,X0)
| order(X0,X1) ),
inference(resolution,[status(thm)],[f8385,f252]) ).
fof(f8554,definition,
! [X0] :
( sQ153_spl
<=> ( ~ sP0_prd(sum(empty_set),X0)
| order(X0,sum(empty_set)) ) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f8561,plain,
( sQ148_spl
| sQ153_spl ),
inference(split_clause,[status(thm)],[f8410,f8554,f7836]) ).
fof(f8566,definition,
! [X0,X1] :
( sQ155_spl
<=> ( ~ sP0_prd(difference(empty_set,X1),X0)
| order(X0,difference(empty_set,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f8569,plain,
( sQ148_spl
| sQ155_spl ),
inference(split_clause,[status(thm)],[f8422,f8566,f7836]) ).
fof(f8574,plain,
( ~ sQ5_spl
| sQ148_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f8424,f4980,f7836,f239]) ).
fof(f8575,definition,
! [X2] :
( sQ157_spl
<=> ( ~ subset(X2,empty_set)
| ~ subset(sK18_skl,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f8578,plain,
( ~ sQ5_spl
| sQ157_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f8425,f4988,f8575,f239]) ).
fof(f8583,plain,
( sQ148_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f8427,f4992,f7836]) ).
fof(f8585,plain,
( sQ148_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f8430,f5004,f7836]) ).
fof(f8586,plain,
( sQ148_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f8432,f5008,f7836]) ).
fof(f8587,plain,
( sQ148_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f8436,f5016,f7836]) ).
fof(f8589,definition,
! [X0,X1] :
( sQ159_spl
<=> ( ~ sP0_prd(intersection(empty_set,X1),X0)
| order(X0,intersection(empty_set,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f8592,plain,
( sQ148_spl
| sQ159_spl ),
inference(split_clause,[status(thm)],[f8440,f8589,f7836]) ).
fof(f8593,plain,
( ~ sQ5_spl
| sQ157_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f8441,f5020,f8575,f239]) ).
fof(f8595,plain,
( ~ sQ5_spl
| sQ157_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f8443,f5028,f8575,f239]) ).
fof(f8597,plain,
( sQ148_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f8446,f5036,f7836]) ).
fof(f8601,plain,
( sQ148_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f8460,f949,f7836]) ).
fof(f8602,plain,
( ~ sQ5_spl
| sQ157_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f8461,f960,f8575,f239]) ).
fof(f8612,definition,
! [X0,X1] :
( sQ162_spl
<=> ( ~ subset(X1,sum(empty_set))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f8615,plain,
( sQ34_spl
| sQ162_spl ),
inference(split_clause,[status(thm)],[f8481,f8612,f1307]) ).
fof(f8616,definition,
! [X0,X1,X2] :
( sQ163_spl
<=> ( ~ subset(X1,difference(empty_set,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f8619,plain,
( sQ34_spl
| sQ163_spl ),
inference(split_clause,[status(thm)],[f8487,f8616,f1307]) ).
fof(f8620,definition,
! [X0,X1] :
( sQ164_spl
<=> ( ~ subset(X1,difference(sK17_skl,sK18_skl))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f8623,plain,
( ~ sQ5_spl
| sQ34_spl
| sQ164_spl ),
inference(split_clause,[status(thm)],[f8488,f8620,f1307,f239]) ).
fof(f8624,definition,
! [X0,X1,X2] :
( sQ165_spl
<=> ( ~ subset(X1,difference(sK17_skl,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f8627,plain,
( ~ sQ5_spl
| ~ sQ13_spl
| sQ165_spl ),
inference(split_clause,[status(thm)],[f8489,f8624,f415,f239]) ).
fof(f8628,definition,
! [X0,X1] :
( sQ166_spl
<=> ( ~ subset(X1,difference(sK18_skl,sK17_skl))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f8631,plain,
( sQ34_spl
| sQ166_spl ),
inference(split_clause,[status(thm)],[f8490,f8628,f1307]) ).
fof(f8636,definition,
! [X0,X1,X2,X3] :
( sQ168_spl
<=> ( ~ subset(X1,difference(X2,union(X3,X2)))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f8639,plain,
( sQ34_spl
| sQ168_spl ),
inference(split_clause,[status(thm)],[f8492,f8636,f1307]) ).
fof(f8640,definition,
! [X0,X1,X2,X3] :
( sQ169_spl
<=> ( ~ subset(X1,difference(X2,union(X2,X3)))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f8643,plain,
( sQ34_spl
| sQ169_spl ),
inference(split_clause,[status(thm)],[f8493,f8640,f1307]) ).
fof(f8644,definition,
! [X0,X1,X2] :
( sQ170_spl
<=> ( ~ subset(X1,difference(X2,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f8647,plain,
( sQ34_spl
| sQ170_spl ),
inference(split_clause,[status(thm)],[f8496,f8644,f1307]) ).
fof(f8648,definition,
! [X0,X1,X2] :
( sQ171_spl
<=> ( ~ subset(X1,intersection(empty_set,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f8651,plain,
( sQ34_spl
| sQ171_spl ),
inference(split_clause,[status(thm)],[f8498,f8648,f1307]) ).
fof(f8652,definition,
! [X0,X1,X2] :
( sQ172_spl
<=> ( ~ subset(X1,intersection(sK17_skl,X2))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f8655,plain,
( ~ sQ5_spl
| ~ sQ13_spl
| sQ172_spl ),
inference(split_clause,[status(thm)],[f8499,f8652,f415,f239]) ).
fof(f8660,definition,
! [X0,X1,X2] :
( sQ174_spl
<=> ( ~ subset(X1,intersection(X2,sK17_skl))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f8663,plain,
( ~ sQ5_spl
| ~ sQ13_spl
| sQ174_spl ),
inference(split_clause,[status(thm)],[f8501,f8660,f415,f239]) ).
fof(f8668,definition,
! [X0,X1,X2] :
( sQ176_spl
<=> ( ~ subset(X1,intersection(X2,empty_set))
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f8671,plain,
( sQ34_spl
| sQ176_spl ),
inference(split_clause,[status(thm)],[f8503,f8668,f1307]) ).
fof(f8672,definition,
! [X0,X1] :
( sQ177_spl
<=> ( ~ subset(X1,empty_set)
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f8675,plain,
( sQ34_spl
| sQ177_spl ),
inference(split_clause,[status(thm)],[f8513,f8672,f1307]) ).
fof(f8676,definition,
! [X0,X1] :
( sQ178_spl
<=> ( ~ subset(X1,sK17_skl)
| ~ sP0_prd(X1,X0)
| order(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f8679,plain,
( ~ sQ5_spl
| ~ sQ13_spl
| sQ178_spl ),
inference(split_clause,[status(thm)],[f8514,f8676,f415,f239]) ).
fof(f8706,plain,
! [X0] :
( ~ sQ148_spl
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f7837,f294]) ).
fof(f8708,plain,
( ~ sQ148_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f8706,f1307,f7836]) ).
fof(f8710,plain,
( sQ76_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5462,f294]) ).
fof(f8711,plain,
sQ76_spl,
inference(contradiction_clause,[status(thm)],[f8710]) ).
fof(f8774,plain,
! [X0,X1] :
( ~ sQ43_spl
| ~ member(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f7473,f3220]) ).
fof(f8824,plain,
( ~ sQ43_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f8774,f3215,f3219]) ).
fof(f8960,plain,
! [X0,X1] :
( ~ sQ142_spl
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f7092,f215]) ).
fof(f8961,plain,
( ~ sQ142_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f8960,f3219,f7091]) ).
fof(f9309,plain,
( ~ sQ73_spl
| total_order(sK16_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f5157,f173]) ).
fof(f9310,plain,
( ~ sQ73_spl
| ~ order(sK16_skl,sK18_skl)
| total_order(sK16_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f9309,f7260]) ).
fof(f9312,plain,
( ~ sQ73_spl
| ~ sQ145_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f9310,f7710,f7713,f5156]) ).
fof(f9365,plain,
( ~ sQ1_spl
| ~ sQ29_spl
| ~ subset(sK18_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f1240,f199]) ).
fof(f9384,plain,
( ~ sQ1_spl
| ~ sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9365,f215]) ).
fof(f9385,plain,
( ~ sQ1_spl
| ~ sQ29_spl ),
inference(contradiction_clause,[status(thm)],[f9384]) ).
fof(f9815,plain,
( sQ28_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1051,f248]) ).
fof(f9816,plain,
( sQ28_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f9815]) ).
fof(f9931,plain,
! [X0,X1] :
( ~ sQ2_spl
| apply(sK16_skl,X1,sK19_skl)
| ~ member(X1,sK17_skl)
| ~ subset(sK18_skl,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f7555,f249]) ).
fof(f9933,plain,
( ~ sQ2_spl
| sQ21_spl
| sQ157_spl ),
inference(split_clause,[status(thm)],[f9931,f8575,f848,f202]) ).
fof(f10473,definition,
( sQ233_spl
<=> sP0_prd(sK17_skl,sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition]) ).
fof(f10475,plain,
( sQ233_spl
| ~ sP0_prd(sK17_skl,sK16_skl) ),
inference(component_clause,[status(thm)],[f10473]) ).
fof(f10725,plain,
( sQ233_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10475,f210]) ).
fof(f10726,plain,
sQ233_spl,
inference(contradiction_clause,[status(thm)],[f10725]) ).
fof(f11196,plain,
( ~ sQ1_spl
| ~ sQ51_spl
| ~ sP0_prd(sK17_skl,sK16_skl) ),
inference(resolution,[status(thm)],[f3915,f264]) ).
fof(f11216,plain,
( ~ sQ1_spl
| ~ sQ51_spl
| ~ sQ233_spl ),
inference(split_clause,[status(thm)],[f11196,f10473,f3914,f198]) ).
fof(f11303,definition,
! [X3,X4] :
( sQ295_spl
<=> ( ~ subset(X3,empty_set)
| ~ member(X3,X4) ) ),
introduced(definition,[new_symbols(definition,[sQ295_spl])],[split_symbol_definition]) ).
fof(f11304,plain,
! [X0,X1] :
( ~ sQ295_spl
| ~ subset(X0,empty_set)
| ~ member(X0,X1) ),
inference(component_clause,[status(thm)],[f11303]) ).
fof(f11396,plain,
( ~ sQ1_spl
| ~ sQ295_spl
| ~ subset(sK19_skl,empty_set) ),
inference(resolution,[status(thm)],[f11304,f6757]) ).
fof(f11472,plain,
( ~ sQ1_spl
| ~ sQ295_spl
| ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11396,f605]) ).
fof(f11473,plain,
( ~ sQ1_spl
| ~ sQ295_spl
| ~ sQ14_spl ),
inference(contradiction_clause,[status(thm)],[f11472]) ).
fof(f11502,plain,
! [X0,X1,X2,X3] :
( ~ lower_bound(X0,X2,X1)
| ~ member(X0,X1)
| greatest_lower_bound(X0,X1,X2,X3)
| ~ member(X0,X1)
| ~ lower_bound(X0,X2,X1)
| ~ member(X0,X1)
| greatest_lower_bound(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f1266,f169]) ).
fof(f11513,plain,
! [X0,X1,X2,X3] :
( ~ lower_bound(X0,X2,X1)
| ~ member(X0,X1)
| greatest_lower_bound(X0,X1,X2,X3) ),
inference(duplicate_literals_removal,[status(thm)],[f11502]) ).
fof(f11604,plain,
( ~ sQ2_spl
| ~ member(sK19_skl,sK18_skl)
| least(sK19_skl,sK16_skl,sK18_skl)
| ~ member(sK19_skl,sK18_skl)
| least(sK19_skl,sK16_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f1103,f130]) ).
fof(f11612,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f11604,f195,f198,f202]) ).
fof(f11616,plain,
( sQ2_spl
| ~ lower_bound(sK19_skl,sK16_skl,sK18_skl)
| ~ member(sK19_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f204,f11513]) ).
fof(f11617,plain,
( sQ2_spl
| ~ sQ28_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f11616,f198,f1049,f202]) ).
fof(f11618,plain,
$false,
inference(sat_refutation,[status(thm)],[f201,f205,f206,f218,f229,f245,f247,f255,f291,f414,f418,f421,f573,f608,f689,f753,f787,f806,f851,f883,f963,f973,f1052,f1310,f1314,f1345,f1386,f1467,f1498,f2101,f2496,f3218,f3681,f3764,f3888,f3892,f4130,f4574,f4608,f4991,f5023,f5031,f5555,f5563,f5571,f5579,f5587,f5773,f5781,f5789,f5797,f5805,f5820,f6029,f6037,f6045,f6053,f6061,f6235,f6243,f6251,f6259,f6267,f6430,f6438,f6446,f6454,f6462,f6774,f6791,f6804,f6811,f6828,f7480,f7603,f7609,f7707,f7716,f7759,f7843,f7990,f8561,f8569,f8574,f8578,f8583,f8585,f8586,f8587,f8592,f8593,f8595,f8597,f8601,f8602,f8615,f8619,f8623,f8627,f8631,f8639,f8643,f8647,f8651,f8655,f8663,f8671,f8675,f8679,f8708,f8711,f8824,f8961,f9312,f9385,f9816,f9933,f10726,f11216,f11473,f11612,f11617]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET802+4 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n005.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 05:38:49 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 44.44/6.04 % Refutation found
% 44.44/6.04 % SZS status Theorem for theBenchmark: Theorem is valid
% 44.44/6.04 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 44.44/6.09 % Elapsed time: 5.718196 seconds
% 44.44/6.09 % CPU time: 45.039481 seconds
% 44.44/6.09 % Total memory used: 400.458 MB
% 44.44/6.09 % Net memory used: 348.028 MB
%------------------------------------------------------------------------------