%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT288+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 01:02:33 PM UTC 2026
% Result : Theorem 59.42s 8.08s
% Output : CNFRefutation 59.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 86
% Syntax : Number of formulae : 395 ( 89 unt; 64 def)
% Number of atoms : 1043 ( 40 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 1088 ( 440 ~; 422 |; 140 &)
% ( 72 <=>; 13 =>; 0 <=; 1 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 99 ( 97 usr; 65 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 8 con; 0-3 aty)
% Number of variables : 259 ( 237 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> r1_tarski(a_2_0_lopclset(A,B),k7_lopclset(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> r1_tarski(a_2_0_lopclset(A,B),k7_lopclset(A)) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
! [A,B] :
( r2_hidden(A,B)
=> ~ r2_hidden(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [A,B] :
( r1_tarski(A,B)
<=> ! [C] :
( r2_hidden(C,A)
=> r2_hidden(C,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k7_lopclset(A) = a_1_1_lopclset(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
? [A] : l3_lattices(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [A] :
? [B] : m1_subset_1(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [A] :
( v4_finsub_1(k1_zfmisc_1(A))
& v3_finsub_1(k1_zfmisc_1(A))
& v1_finsub_1(k1_zfmisc_1(A))
& ~ v1_xboole_0(k1_zfmisc_1(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
( v5_membered(k1_xboole_0)
& v4_membered(k1_xboole_0)
& v3_membered(k1_xboole_0)
& v2_membered(k1_xboole_0)
& v1_membered(k1_xboole_0)
& v1_xboole_0(k1_xboole_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [A,B] :
( ( l3_lattices(B)
& ~ v3_realset2(B)
& v17_lattices(B)
& v10_lattices(B)
& ~ v3_struct_0(B) )
=> ( r2_hidden(A,a_1_1_lopclset(B))
<=> ? [C] :
( v1_filter_0(C,B)
& A = C
& m1_filter_0(C,B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(B))
& l3_lattices(B)
& ~ v3_realset2(B)
& v17_lattices(B)
& v10_lattices(B)
& ~ v3_struct_0(B) )
=> ( r2_hidden(A,a_2_0_lopclset(B,C))
<=> ? [D] :
( r2_hidden(C,D)
& v1_filter_0(D,B)
& A = D
& m1_filter_0(D,B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
? [A] :
( v1_finset_1(A)
& ~ v1_xboole_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
? [A] :
( ~ v3_realset2(A)
& v17_lattices(A)
& v16_lattices(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v12_lattices(A)
& v11_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
? [A] :
( v5_membered(A)
& v4_membered(A)
& v3_membered(A)
& v2_membered(A)
& v1_membered(A)
& ~ v1_xboole_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ? [B] :
( v1_finset_1(B)
& ~ v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,axiom,
? [A] :
( ~ v3_struct_0(A)
& l1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [A,B] : r1_tarski(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [A,B] :
( r2_hidden(A,B)
=> m1_subset_1(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( r2_hidden(A,B)
| v1_xboole_0(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A,B] :
( ! [C] :
( r2_hidden(C,A)
<=> r2_hidden(C,B) )
=> A = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [A,B,C] :
~ ( v1_xboole_0(C)
& m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [A,B] :
~ ( v1_xboole_0(B)
& r2_hidden(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,plain,
? [A] :
( ? [B] :
( ~ r1_tarski(a_2_0_lopclset(A,B),k7_lopclset(A))
& m1_subset_1(B,u1_struct_0(A)) )
& l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f72,plain,
( ~ r1_tarski(a_2_0_lopclset(sK0_skl,sK1_skl),k7_lopclset(sK0_skl))
& m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))
& l3_lattices(sK0_skl)
& ~ v3_realset2(sK0_skl)
& v17_lattices(sK0_skl)
& v10_lattices(sK0_skl)
& ~ v3_struct_0(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f71]) ).
fof(f73,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f74,plain,
v10_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f75,plain,
v17_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f76,plain,
~ v3_realset2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f77,plain,
l3_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f78,plain,
m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f79,plain,
~ r1_tarski(a_2_0_lopclset(sK0_skl,sK1_skl),k7_lopclset(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f80,plain,
! [A,B] :
( ~ r2_hidden(B,A)
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f81,plain,
! [X0,X1] :
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f183,plain,
! [A,B] :
( r1_tarski(A,B)
<=> ! [C] :
( r2_hidden(C,B)
| ~ r2_hidden(C,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f184,plain,
! [A,B] :
( ( ? [C] :
( ~ r2_hidden(C,B)
& r2_hidden(C,A) )
| r1_tarski(A,B) )
& ( ! [C] :
( r2_hidden(C,B)
| ~ r2_hidden(C,A) )
| ~ r1_tarski(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f183]) ).
fof(f185,plain,
( ! [A,B] :
( ? [C] :
( ~ r2_hidden(C,B)
& r2_hidden(C,A) )
| r1_tarski(A,B) )
& ! [A,B] :
( ! [C] :
( r2_hidden(C,B)
| ~ r2_hidden(C,A) )
| ~ r1_tarski(A,B) ) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f186,plain,
( ! [A,B] :
( ( ~ r2_hidden(sK2_skl(B,A),B)
& r2_hidden(sK2_skl(B,A),A) )
| r1_tarski(A,B) )
& ! [A,B] :
( ! [C] :
( r2_hidden(C,B)
| ~ r2_hidden(C,A) )
| ~ r1_tarski(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(C,sK2_skl(B,A))],[f185]) ).
fof(f187,plain,
! [X0,X1,X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0)
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f188,plain,
! [X0,X1] :
( r2_hidden(sK2_skl(X1,X0),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f189,plain,
! [X0,X1] :
( ~ r2_hidden(sK2_skl(X1,X0),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f190,plain,
! [A] :
( k7_lopclset(A) = a_1_1_lopclset(A)
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f191,plain,
! [X0] :
( k7_lopclset(X0) = a_1_1_lopclset(X0)
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f210,plain,
l3_lattices(sK6_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f45]) ).
fof(f211,plain,
l3_lattices(sK6_skl),
inference(cnf_transformation,[status(thm)],[f210]) ).
fof(f215,plain,
! [A] : m1_subset_1(sK8_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(B,sK8_skl(A))],[f47]) ).
fof(f216,plain,
! [X0] : m1_subset_1(sK8_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f217,plain,
( ! [A] : v4_finsub_1(k1_zfmisc_1(A))
& ! [A] : v3_finsub_1(k1_zfmisc_1(A))
& ! [A] : v1_finsub_1(k1_zfmisc_1(A))
& ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ),
inference(miniscoping,[status(thm)],[f48]) ).
fof(f218,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f226,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f232,plain,
! [A,B] :
( ( r2_hidden(A,a_1_1_lopclset(B))
<=> ? [C] :
( v1_filter_0(C,B)
& A = C
& m1_filter_0(C,B) ) )
| ~ l3_lattices(B)
| v3_realset2(B)
| ~ v17_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f233,plain,
! [A,B] :
( ( ( ! [C] :
( ~ v1_filter_0(C,B)
| A != C
| ~ m1_filter_0(C,B) )
| r2_hidden(A,a_1_1_lopclset(B)) )
& ( ? [C] :
( v1_filter_0(C,B)
& A = C
& m1_filter_0(C,B) )
| ~ r2_hidden(A,a_1_1_lopclset(B)) ) )
| ~ l3_lattices(B)
| v3_realset2(B)
| ~ v17_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) ),
inference(NNF_transformation,[status(thm)],[f232]) ).
fof(f234,plain,
! [B] :
( ( ! [A] :
( ! [C] :
( ~ v1_filter_0(C,B)
| A != C
| ~ m1_filter_0(C,B) )
| r2_hidden(A,a_1_1_lopclset(B)) )
& ! [A] :
( ? [C] :
( v1_filter_0(C,B)
& A = C
& m1_filter_0(C,B) )
| ~ r2_hidden(A,a_1_1_lopclset(B)) ) )
| ~ l3_lattices(B)
| v3_realset2(B)
| ~ v17_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) ),
inference(miniscoping,[status(thm)],[f233]) ).
fof(f235,plain,
! [B] :
( ( ! [A] :
( ! [C] :
( ~ v1_filter_0(C,B)
| A != C
| ~ m1_filter_0(C,B) )
| r2_hidden(A,a_1_1_lopclset(B)) )
& ! [A] :
( ( v1_filter_0(sK9_skl(A,B),B)
& A = sK9_skl(A,B)
& m1_filter_0(sK9_skl(A,B),B) )
| ~ r2_hidden(A,a_1_1_lopclset(B)) ) )
| ~ l3_lattices(B)
| v3_realset2(B)
| ~ v17_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(C,sK9_skl(A,B))],[f234]) ).
fof(f239,plain,
! [X0,X1,X2] :
( ~ v1_filter_0(X2,X0)
| X1 != X2
| ~ m1_filter_0(X2,X0)
| r2_hidden(X1,a_1_1_lopclset(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f240,plain,
! [A,B,C] :
( ( r2_hidden(A,a_2_0_lopclset(B,C))
<=> ? [D] :
( r2_hidden(C,D)
& v1_filter_0(D,B)
& A = D
& m1_filter_0(D,B) ) )
| ~ m1_subset_1(C,u1_struct_0(B))
| ~ l3_lattices(B)
| v3_realset2(B)
| ~ v17_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f241,plain,
! [A,B,C] :
( ( ( ! [D] :
( ~ r2_hidden(C,D)
| ~ v1_filter_0(D,B)
| A != D
| ~ m1_filter_0(D,B) )
| r2_hidden(A,a_2_0_lopclset(B,C)) )
& ( ? [D] :
( r2_hidden(C,D)
& v1_filter_0(D,B)
& A = D
& m1_filter_0(D,B) )
| ~ r2_hidden(A,a_2_0_lopclset(B,C)) ) )
| ~ m1_subset_1(C,u1_struct_0(B))
| ~ l3_lattices(B)
| v3_realset2(B)
| ~ v17_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) ),
inference(NNF_transformation,[status(thm)],[f240]) ).
fof(f242,plain,
! [B,C] :
( ( ! [A] :
( ! [D] :
( ~ r2_hidden(C,D)
| ~ v1_filter_0(D,B)
| A != D
| ~ m1_filter_0(D,B) )
| r2_hidden(A,a_2_0_lopclset(B,C)) )
& ! [A] :
( ? [D] :
( r2_hidden(C,D)
& v1_filter_0(D,B)
& A = D
& m1_filter_0(D,B) )
| ~ r2_hidden(A,a_2_0_lopclset(B,C)) ) )
| ~ m1_subset_1(C,u1_struct_0(B))
| ~ l3_lattices(B)
| v3_realset2(B)
| ~ v17_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) ),
inference(miniscoping,[status(thm)],[f241]) ).
fof(f243,plain,
! [B,C] :
( ( ! [A] :
( ! [D] :
( ~ r2_hidden(C,D)
| ~ v1_filter_0(D,B)
| A != D
| ~ m1_filter_0(D,B) )
| r2_hidden(A,a_2_0_lopclset(B,C)) )
& ! [A] :
( ( r2_hidden(C,sK10_skl(A,C,B))
& v1_filter_0(sK10_skl(A,C,B),B)
& A = sK10_skl(A,C,B)
& m1_filter_0(sK10_skl(A,C,B),B) )
| ~ r2_hidden(A,a_2_0_lopclset(B,C)) ) )
| ~ m1_subset_1(C,u1_struct_0(B))
| ~ l3_lattices(B)
| v3_realset2(B)
| ~ v17_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(D,sK10_skl(A,C,B))],[f242]) ).
fof(f244,plain,
! [X0,X1,X2] :
( m1_filter_0(sK10_skl(X2,X1,X0),X0)
| ~ r2_hidden(X2,a_2_0_lopclset(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f245,plain,
! [X0,X1,X2] :
( X2 = sK10_skl(X2,X1,X0)
| ~ r2_hidden(X2,a_2_0_lopclset(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f246,plain,
! [X0,X1,X2] :
( v1_filter_0(sK10_skl(X2,X1,X0),X0)
| ~ r2_hidden(X2,a_2_0_lopclset(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f249,plain,
( v1_finset_1(sK11_skl)
& ~ v1_xboole_0(sK11_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f54]) ).
fof(f250,plain,
~ v1_xboole_0(sK11_skl),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f252,plain,
( ~ v3_realset2(sK12_skl)
& v17_lattices(sK12_skl)
& v16_lattices(sK12_skl)
& v15_lattices(sK12_skl)
& v14_lattices(sK12_skl)
& v13_lattices(sK12_skl)
& v12_lattices(sK12_skl)
& v11_lattices(sK12_skl)
& v10_lattices(sK12_skl)
& v9_lattices(sK12_skl)
& v8_lattices(sK12_skl)
& v7_lattices(sK12_skl)
& v6_lattices(sK12_skl)
& v5_lattices(sK12_skl)
& v4_lattices(sK12_skl)
& ~ v3_struct_0(sK12_skl)
& l3_lattices(sK12_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f55]) ).
fof(f262,plain,
v11_lattices(sK12_skl),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f266,plain,
v15_lattices(sK12_skl),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f267,plain,
v16_lattices(sK12_skl),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f270,plain,
( v5_membered(sK13_skl)
& v4_membered(sK13_skl)
& v3_membered(sK13_skl)
& v2_membered(sK13_skl)
& v1_membered(sK13_skl)
& ~ v1_xboole_0(sK13_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f56]) ).
fof(f271,plain,
~ v1_xboole_0(sK13_skl),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f277,plain,
! [A] :
( ? [B] :
( v1_finset_1(B)
& ~ v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(A)) )
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f278,plain,
! [A] :
( ( v1_finset_1(sK14_skl(A))
& ~ v1_xboole_0(sK14_skl(A))
& m1_subset_1(sK14_skl(A),k1_zfmisc_1(A)) )
| v1_xboole_0(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(B,sK14_skl(A))],[f277]) ).
fof(f279,plain,
! [X0] :
( m1_subset_1(sK14_skl(X0),k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f280,plain,
! [X0] :
( ~ v1_xboole_0(sK14_skl(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f282,plain,
( ~ v3_struct_0(sK15_skl)
& l1_struct_0(sK15_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(A,sK15_skl)],[f58]) ).
fof(f283,plain,
l1_struct_0(sK15_skl),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f284,plain,
~ v3_struct_0(sK15_skl),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f294,plain,
! [A] : r1_tarski(A,A),
inference(miniscoping,[status(thm)],[f61]) ).
fof(f295,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f296,plain,
! [A,B] :
( m1_subset_1(A,B)
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f62]) ).
fof(f297,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f298,plain,
! [A,B] :
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f63]) ).
fof(f299,plain,
! [X0,X1] :
( r2_hidden(X0,X1)
| v1_xboole_0(X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f298]) ).
fof(f300,plain,
! [A,B] :
( A = B
| ? [C] :
( r2_hidden(C,A)
<~> r2_hidden(C,B) ) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f301,plain,
! [A,B] :
( A = B
| ? [C] :
( ( ~ r2_hidden(C,B)
| ~ r2_hidden(C,A) )
& ( r2_hidden(C,B)
| r2_hidden(C,A) ) ) ),
inference(NNF_transformation,[status(thm)],[f300]) ).
fof(f302,plain,
! [A,B] :
( A = B
| ( ( ~ r2_hidden(sK18_skl(B,A),B)
| ~ r2_hidden(sK18_skl(B,A),A) )
& ( r2_hidden(sK18_skl(B,A),B)
| r2_hidden(sK18_skl(B,A),A) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(C,sK18_skl(B,A))],[f301]) ).
fof(f303,plain,
! [X0,X1] :
( X1 = X0
| r2_hidden(sK18_skl(X0,X1),X0)
| r2_hidden(sK18_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f305,plain,
! [A,B] :
( ( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) )
& ( r1_tarski(A,B)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ) ),
inference(NNF_transformation,[status(thm)],[f65]) ).
fof(f306,plain,
( ! [A,B] :
( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) )
& ! [A,B] :
( r1_tarski(A,B)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ) ),
inference(miniscoping,[status(thm)],[f305]) ).
fof(f307,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[status(thm)],[f306]) ).
fof(f308,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[status(thm)],[f306]) ).
fof(f312,plain,
! [A,B,C] :
( ~ v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f67]) ).
fof(f313,plain,
! [C] :
( ~ v1_xboole_0(C)
| ! [B] :
( ~ m1_subset_1(B,k1_zfmisc_1(C))
| ! [A] : ~ r2_hidden(A,B) ) ),
inference(miniscoping,[status(thm)],[f312]) ).
fof(f314,plain,
! [X0,X1,X2] :
( ~ v1_xboole_0(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f313]) ).
fof(f317,plain,
! [A,B] :
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f69]) ).
fof(f318,plain,
! [B] :
( ~ v1_xboole_0(B)
| ! [A] : ~ r2_hidden(A,B) ),
inference(miniscoping,[status(thm)],[f317]) ).
fof(f319,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f323,plain,
! [X0,X1] :
( ~ v1_filter_0(X1,X0)
| ~ m1_filter_0(X1,X0)
| r2_hidden(X1,a_1_1_lopclset(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f239]) ).
fof(f325,plain,
( k7_lopclset(sK0_skl) = a_1_1_lopclset(sK0_skl)
| ~ l3_lattices(sK0_skl)
| v3_realset2(sK0_skl)
| ~ v17_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f191,f74]) ).
fof(f329,definition,
( sQ0_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f330,plain,
( ~ sQ0_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f329]) ).
fof(f332,definition,
( sQ1_spl
<=> v17_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f334,plain,
( sQ1_spl
| ~ v17_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f332]) ).
fof(f335,definition,
( sQ2_spl
<=> v3_realset2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f336,plain,
( ~ sQ2_spl
| v3_realset2(sK0_skl) ),
inference(component_clause,[status(thm)],[f335]) ).
fof(f338,definition,
( sQ3_spl
<=> l3_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f340,plain,
( sQ3_spl
| ~ l3_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f338]) ).
fof(f341,definition,
( sQ4_spl
<=> k7_lopclset(sK0_skl) = a_1_1_lopclset(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f342,plain,
( ~ sQ4_spl
| k7_lopclset(sK0_skl) = a_1_1_lopclset(sK0_skl) ),
inference(component_clause,[status(thm)],[f341]) ).
fof(f344,plain,
( sQ4_spl
| ~ sQ3_spl
| sQ2_spl
| ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f325,f329,f332,f335,f338,f341]) ).
fof(f345,definition,
( sQ5_spl
<=> v10_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f347,plain,
( sQ5_spl
| ~ v10_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f345]) ).
fof(f351,plain,
( ~ sQ4_spl
| ~ r1_tarski(a_2_0_lopclset(sK0_skl,sK1_skl),a_1_1_lopclset(sK0_skl)) ),
inference(backward_demodulation,[status(thm)],[f342,f79]) ).
fof(f357,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f330,f73]) ).
fof(f358,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f357]) ).
fof(f359,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f340,f77]) ).
fof(f360,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f359]) ).
fof(f361,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f336,f76]) ).
fof(f362,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f361]) ).
fof(f363,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f334,f75]) ).
fof(f364,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f363]) ).
fof(f365,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f347,f74]) ).
fof(f366,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f365]) ).
fof(f437,definition,
( sQ22_spl
<=> l3_lattices(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f439,plain,
( sQ22_spl
| ~ l3_lattices(sK6_skl) ),
inference(component_clause,[status(thm)],[f437]) ).
fof(f558,definition,
( sQ38_spl
<=> v15_lattices(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f560,plain,
( sQ38_spl
| ~ v15_lattices(sK12_skl) ),
inference(component_clause,[status(thm)],[f558]) ).
fof(f561,definition,
( sQ39_spl
<=> v16_lattices(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f563,plain,
( sQ39_spl
| ~ v16_lattices(sK12_skl) ),
inference(component_clause,[status(thm)],[f561]) ).
fof(f565,definition,
( sQ40_spl
<=> v11_lattices(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f567,plain,
( sQ40_spl
| ~ v11_lattices(sK12_skl) ),
inference(component_clause,[status(thm)],[f565]) ).
fof(f569,plain,
( ~ sQ4_spl
| r2_hidden(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),a_2_0_lopclset(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f188,f351]) ).
fof(f576,definition,
( sQ41_spl
<=> r2_hidden(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),a_2_0_lopclset(sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f578,plain,
( sQ41_spl
| ~ r2_hidden(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),a_2_0_lopclset(sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f576]) ).
fof(f615,plain,
! [X0] : r1_tarski(sK8_skl(k1_zfmisc_1(X0)),X0),
inference(resolution,[status(thm)],[f216,f307]) ).
fof(f639,plain,
! [X0] : ~ r2_hidden(X0,k1_xboole_0),
inference(resolution,[status(thm)],[f319,f226]) ).
fof(f644,plain,
! [X0,X1] :
( m1_filter_0(sK10_skl(X1,X0,sK0_skl),sK0_skl)
| ~ r2_hidden(X1,a_2_0_lopclset(sK0_skl,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v17_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f244,f76]) ).
fof(f649,definition,
! [X0,X1] :
( sQ51_spl
<=> ( m1_filter_0(sK10_skl(X1,X0,sK0_skl),sK0_skl)
| ~ r2_hidden(X1,a_2_0_lopclset(sK0_skl,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f650,plain,
! [X0,X1] :
( ~ sQ51_spl
| m1_filter_0(sK10_skl(X1,X0,sK0_skl),sK0_skl)
| ~ r2_hidden(X1,a_2_0_lopclset(sK0_skl,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f649]) ).
fof(f652,plain,
( sQ51_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ5_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f644,f329,f345,f332,f338,f649]) ).
fof(f654,plain,
! [X0,X1] :
( X1 = sK10_skl(X1,X0,sK0_skl)
| ~ r2_hidden(X1,a_2_0_lopclset(sK0_skl,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v17_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f245,f76]) ).
fof(f659,definition,
! [X0,X1] :
( sQ53_spl
<=> ( X1 = sK10_skl(X1,X0,sK0_skl)
| ~ r2_hidden(X1,a_2_0_lopclset(sK0_skl,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f660,plain,
! [X0,X1] :
( ~ sQ53_spl
| X1 = sK10_skl(X1,X0,sK0_skl)
| ~ r2_hidden(X1,a_2_0_lopclset(sK0_skl,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f659]) ).
fof(f662,plain,
( sQ53_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ5_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f654,f329,f345,f332,f338,f659]) ).
fof(f677,plain,
! [X0] :
( ~ sQ53_spl
| X0 = sK10_skl(X0,sK1_skl,sK0_skl)
| ~ r2_hidden(X0,a_2_0_lopclset(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f660,f78]) ).
fof(f690,plain,
( ~ sQ4_spl
| ~ sQ53_spl
| sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)) = sK10_skl(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f677,f569]) ).
fof(f711,plain,
! [X0] :
( r1_tarski(sK14_skl(X0),X0)
| v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f279,f307]) ).
fof(f735,plain,
! [X0,X1] :
( r2_hidden(X1,X0)
| ~ r2_hidden(X1,sK14_skl(X0))
| v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f711,f187]) ).
fof(f748,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| ~ r2_hidden(X0,k1_zfmisc_1(X1)) ),
inference(resolution,[status(thm)],[f297,f307]) ).
fof(f754,plain,
! [X0] :
( r2_hidden(sK8_skl(X0),X0)
| v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f299,f216]) ).
fof(f759,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| r2_hidden(X1,k1_zfmisc_1(X0))
| v1_xboole_0(k1_zfmisc_1(X0)) ),
inference(resolution,[status(thm)],[f299,f308]) ).
fof(f793,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| r2_hidden(X0,k1_zfmisc_1(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f759,f218]) ).
fof(f807,plain,
! [X0] :
( k1_xboole_0 = X0
| r2_hidden(sK18_skl(X0,k1_xboole_0),X0) ),
inference(resolution,[status(thm)],[f303,f639]) ).
fof(f820,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_xboole_0))
| ~ r2_hidden(X0,X1) ),
inference(resolution,[status(thm)],[f314,f226]) ).
fof(f861,plain,
! [X0,X1] :
( ~ r2_hidden(k1_zfmisc_1(X1),X0)
| ~ r1_tarski(X0,X1) ),
inference(resolution,[status(thm)],[f793,f81]) ).
fof(f942,definition,
( sQ89_spl
<=> m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f944,plain,
( sQ89_spl
| ~ m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f942]) ).
fof(f949,plain,
( sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f944,f78]) ).
fof(f950,plain,
sQ89_spl,
inference(contradiction_clause,[status(thm)],[f949]) ).
fof(f1081,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f560,f266]) ).
fof(f1082,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f1081]) ).
fof(f1083,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f439,f211]) ).
fof(f1084,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f1083]) ).
fof(f1137,plain,
! [X0,X1] :
( ~ r1_tarski(X1,k1_xboole_0)
| ~ r2_hidden(X0,X1) ),
inference(resolution,[status(thm)],[f820,f308]) ).
fof(f1151,plain,
! [X0] :
( v1_xboole_0(sK14_skl(X0))
| r2_hidden(sK8_skl(sK14_skl(X0)),X0)
| v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f735,f754]) ).
fof(f1153,plain,
! [X0] :
( r2_hidden(sK8_skl(sK14_skl(X0)),X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1151,f280]) ).
fof(f1241,definition,
( sQ115_spl
<=> r2_hidden(sK18_skl(k1_xboole_0,k1_xboole_0),k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1242,plain,
( ~ sQ115_spl
| r2_hidden(sK18_skl(k1_xboole_0,k1_xboole_0),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f1241]) ).
fof(f1382,plain,
! [X0,X1] :
( ~ r1_tarski(k1_zfmisc_1(X1),X0)
| ~ r1_tarski(k1_zfmisc_1(X0),X1) ),
inference(resolution,[status(thm)],[f861,f793]) ).
fof(f1515,definition,
( sQ147_spl
<=> l1_struct_0(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f1517,plain,
( sQ147_spl
| ~ l1_struct_0(sK15_skl) ),
inference(component_clause,[status(thm)],[f1515]) ).
fof(f1533,plain,
( sQ147_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1517,f283]) ).
fof(f1534,plain,
sQ147_spl,
inference(contradiction_clause,[status(thm)],[f1533]) ).
fof(f1846,plain,
! [X0] : ~ r2_hidden(X0,sK8_skl(k1_zfmisc_1(k1_xboole_0))),
inference(resolution,[status(thm)],[f1137,f615]) ).
fof(f1878,definition,
( sQ168_spl
<=> v1_xboole_0(k1_zfmisc_1(k1_xboole_0)) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f1879,plain,
( ~ sQ168_spl
| v1_xboole_0(k1_zfmisc_1(k1_xboole_0)) ),
inference(component_clause,[status(thm)],[f1878]) ).
fof(f1886,plain,
( ~ sQ168_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1879,f218]) ).
fof(f1887,plain,
~ sQ168_spl,
inference(contradiction_clause,[status(thm)],[f1886]) ).
fof(f1915,definition,
( sQ174_spl
<=> k1_xboole_0 = k1_zfmisc_1(k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f1916,plain,
( ~ sQ174_spl
| k1_xboole_0 = k1_zfmisc_1(k1_xboole_0) ),
inference(component_clause,[status(thm)],[f1915]) ).
fof(f2014,plain,
( ~ sQ174_spl
| ~ v1_xboole_0(k1_xboole_0) ),
inference(paramodulation,[status(thm)],[f1916,f218]) ).
fof(f2022,definition,
( sQ176_spl
<=> r2_hidden(sK1_skl,k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f2023,plain,
( ~ sQ176_spl
| r2_hidden(sK1_skl,k1_xboole_0) ),
inference(component_clause,[status(thm)],[f2022]) ).
fof(f2047,definition,
! [X0] :
( sQ181_spl
<=> ( r2_hidden(sK14_skl(k1_xboole_0),X0)
| r2_hidden(sK2_skl(X0,k1_zfmisc_1(k1_xboole_0)),k1_xboole_0) ) ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f2048,plain,
! [X0] :
( ~ sQ181_spl
| r2_hidden(sK14_skl(k1_xboole_0),X0)
| r2_hidden(sK2_skl(X0,k1_zfmisc_1(k1_xboole_0)),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f2047]) ).
fof(f2055,definition,
! [X0] :
( sQ183_spl
<=> ( r2_hidden(sK16_skl(k1_xboole_0),X0)
| r2_hidden(sK2_skl(X0,k1_zfmisc_1(k1_xboole_0)),k1_xboole_0) ) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f2056,plain,
! [X0] :
( ~ sQ183_spl
| r2_hidden(sK16_skl(k1_xboole_0),X0)
| r2_hidden(sK2_skl(X0,k1_zfmisc_1(k1_xboole_0)),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f2055]) ).
fof(f2075,definition,
( sQ185_spl
<=> r2_hidden(sK14_skl(k1_xboole_0),k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f2076,plain,
( ~ sQ185_spl
| r2_hidden(sK14_skl(k1_xboole_0),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f2075]) ).
fof(f2079,definition,
( sQ186_spl
<=> r2_hidden(sK16_skl(k1_xboole_0),k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f2080,plain,
( ~ sQ186_spl
| r2_hidden(sK16_skl(k1_xboole_0),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f2079]) ).
fof(f2093,plain,
( ~ sQ174_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2014,f226]) ).
fof(f2094,plain,
~ sQ174_spl,
inference(contradiction_clause,[status(thm)],[f2093]) ).
fof(f2095,plain,
( ~ sQ186_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2080,f639]) ).
fof(f2096,plain,
~ sQ186_spl,
inference(contradiction_clause,[status(thm)],[f2095]) ).
fof(f2097,plain,
( ~ sQ185_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2076,f639]) ).
fof(f2098,plain,
~ sQ185_spl,
inference(contradiction_clause,[status(thm)],[f2097]) ).
fof(f2099,plain,
! [X0] :
( ~ sQ183_spl
| r2_hidden(sK16_skl(k1_xboole_0),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2056,f639]) ).
fof(f2100,plain,
! [X0] :
( ~ sQ181_spl
| r2_hidden(sK14_skl(k1_xboole_0),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2048,f639]) ).
fof(f2101,plain,
( ~ sQ176_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2023,f639]) ).
fof(f2102,plain,
~ sQ176_spl,
inference(contradiction_clause,[status(thm)],[f2101]) ).
fof(f2145,plain,
( ~ sQ183_spl
| $false ),
inference(resolution,[status(thm)],[f2099,f639]) ).
fof(f2153,plain,
~ sQ183_spl,
inference(contradiction_clause,[status(thm)],[f2145]) ).
fof(f2165,plain,
( ~ sQ181_spl
| $false ),
inference(resolution,[status(thm)],[f2100,f639]) ).
fof(f2173,plain,
~ sQ181_spl,
inference(contradiction_clause,[status(thm)],[f2165]) ).
fof(f2179,definition,
( sQ189_spl
<=> r2_hidden(sK8_skl(k1_xboole_0),k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f2180,plain,
( ~ sQ189_spl
| r2_hidden(sK8_skl(k1_xboole_0),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f2179]) ).
fof(f2184,plain,
( ~ sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2180,f639]) ).
fof(f2185,plain,
~ sQ189_spl,
inference(contradiction_clause,[status(thm)],[f2184]) ).
fof(f2223,plain,
k1_xboole_0 = sK8_skl(k1_zfmisc_1(k1_xboole_0)),
inference(resolution,[status(thm)],[f1846,f807]) ).
fof(f2288,plain,
! [X0] :
( r1_tarski(sK8_skl(sK14_skl(k1_zfmisc_1(X0))),X0)
| v1_xboole_0(k1_zfmisc_1(X0)) ),
inference(resolution,[status(thm)],[f1153,f748]) ).
fof(f2306,plain,
! [X0] : r1_tarski(sK8_skl(sK14_skl(k1_zfmisc_1(X0))),X0),
inference(forward_subsumption_resolution,[status(thm)],[f2288,f218]) ).
fof(f2389,plain,
( ~ sQ4_spl
| ~ sQ53_spl
| ~ sQ51_spl
| m1_filter_0(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),sK0_skl)
| ~ r2_hidden(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),a_2_0_lopclset(sK0_skl,sK1_skl))
| ~ m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f690,f650]) ).
fof(f2390,plain,
( ~ sQ4_spl
| ~ sQ53_spl
| v1_filter_0(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),sK0_skl)
| ~ r2_hidden(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),a_2_0_lopclset(sK0_skl,sK1_skl))
| ~ m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))
| ~ l3_lattices(sK0_skl)
| v3_realset2(sK0_skl)
| ~ v17_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(paramodulation,[status(thm)],[f690,f246]) ).
fof(f2405,definition,
( sQ202_spl
<=> m1_filter_0(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f2408,plain,
( ~ sQ4_spl
| ~ sQ53_spl
| ~ sQ51_spl
| sQ202_spl
| ~ sQ41_spl
| ~ sQ89_spl ),
inference(split_clause,[status(thm)],[f2389,f942,f576,f2405,f649,f659,f341]) ).
fof(f2409,definition,
( sQ203_spl
<=> v1_filter_0(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f2410,plain,
( ~ sQ203_spl
| v1_filter_0(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),sK0_skl) ),
inference(component_clause,[status(thm)],[f2409]) ).
fof(f2412,plain,
( ~ sQ4_spl
| ~ sQ53_spl
| sQ203_spl
| ~ sQ41_spl
| ~ sQ89_spl
| ~ sQ3_spl
| sQ2_spl
| ~ sQ1_spl
| ~ sQ5_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2390,f329,f345,f332,f335,f338,f942,f576,f2409,f659,f341]) ).
fof(f2413,plain,
( sQ41_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f578,f569]) ).
fof(f2414,plain,
( sQ41_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f2413]) ).
fof(f2427,definition,
( sQ205_spl
<=> r2_hidden(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),a_1_1_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f2428,plain,
( ~ sQ205_spl
| r2_hidden(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),a_1_1_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2427]) ).
fof(f2536,definition,
( sQ216_spl
<=> m1_subset_1(sK8_skl(u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition]) ).
fof(f2538,plain,
( sQ216_spl
| ~ m1_subset_1(sK8_skl(u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2536]) ).
fof(f2564,plain,
( sQ216_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2538,f216]) ).
fof(f2565,plain,
sQ216_spl,
inference(contradiction_clause,[status(thm)],[f2564]) ).
fof(f2650,definition,
( sQ229_spl
<=> r2_hidden(sK8_skl(sK8_skl(k1_zfmisc_1(k1_xboole_0))),k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition]) ).
fof(f2651,plain,
( ~ sQ229_spl
| r2_hidden(sK8_skl(sK8_skl(k1_zfmisc_1(k1_xboole_0))),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f2650]) ).
fof(f2654,plain,
( ~ sQ229_spl
| r2_hidden(sK8_skl(k1_xboole_0),k1_xboole_0) ),
inference(forward_demodulation,[status(thm)],[f2223,f2651]) ).
fof(f2655,plain,
( ~ sQ229_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2654,f639]) ).
fof(f2656,plain,
~ sQ229_spl,
inference(contradiction_clause,[status(thm)],[f2655]) ).
fof(f2965,definition,
( sQ263_spl
<=> m1_subset_1(sK8_skl(u1_struct_0(sK12_skl)),u1_struct_0(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition]) ).
fof(f2967,plain,
( sQ263_spl
| ~ m1_subset_1(sK8_skl(u1_struct_0(sK12_skl)),u1_struct_0(sK12_skl)) ),
inference(component_clause,[status(thm)],[f2965]) ).
fof(f2974,plain,
( sQ263_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2967,f216]) ).
fof(f2975,plain,
sQ263_spl,
inference(contradiction_clause,[status(thm)],[f2974]) ).
fof(f3344,definition,
( sQ324_spl
<=> v3_struct_0(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ324_spl])],[split_symbol_definition]) ).
fof(f3345,plain,
( ~ sQ324_spl
| v3_struct_0(sK15_skl) ),
inference(component_clause,[status(thm)],[f3344]) ).
fof(f3372,definition,
( sQ331_spl
<=> m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition]) ).
fof(f3374,plain,
( sQ331_spl
| ~ m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK15_skl))) ),
inference(component_clause,[status(thm)],[f3372]) ).
fof(f3376,plain,
( ~ sQ324_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3345,f284]) ).
fof(f3377,plain,
~ sQ324_spl,
inference(contradiction_clause,[status(thm)],[f3376]) ).
fof(f3387,definition,
( sQ332_spl
<=> v1_xboole_0(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition]) ).
fof(f3388,plain,
( ~ sQ332_spl
| v1_xboole_0(sK11_skl) ),
inference(component_clause,[status(thm)],[f3387]) ).
fof(f3412,plain,
( ~ sQ332_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3388,f250]) ).
fof(f3413,plain,
~ sQ332_spl,
inference(contradiction_clause,[status(thm)],[f3412]) ).
fof(f3423,definition,
( sQ338_spl
<=> v1_xboole_0(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ338_spl])],[split_symbol_definition]) ).
fof(f3424,plain,
( ~ sQ338_spl
| v1_xboole_0(sK13_skl) ),
inference(component_clause,[status(thm)],[f3423]) ).
fof(f3448,plain,
( ~ sQ338_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3424,f271]) ).
fof(f3449,plain,
~ sQ338_spl,
inference(contradiction_clause,[status(thm)],[f3448]) ).
fof(f4050,definition,
! [X0] :
( sQ422_spl
<=> r2_hidden(sK18_skl(k1_xboole_0,k1_xboole_0),X0) ),
introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition]) ).
fof(f4051,plain,
! [X0] :
( ~ sQ422_spl
| r2_hidden(sK18_skl(k1_xboole_0,k1_xboole_0),X0) ),
inference(component_clause,[status(thm)],[f4050]) ).
fof(f4351,definition,
( sQ457_spl
<=> v1_xboole_0(k1_zfmisc_1(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ457_spl])],[split_symbol_definition]) ).
fof(f4352,plain,
( ~ sQ457_spl
| v1_xboole_0(k1_zfmisc_1(sK11_skl)) ),
inference(component_clause,[status(thm)],[f4351]) ).
fof(f4355,plain,
( ~ sQ457_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4352,f218]) ).
fof(f4356,plain,
~ sQ457_spl,
inference(contradiction_clause,[status(thm)],[f4355]) ).
fof(f4523,definition,
( sQ475_spl
<=> v1_xboole_0(k1_zfmisc_1(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ475_spl])],[split_symbol_definition]) ).
fof(f4524,plain,
( ~ sQ475_spl
| v1_xboole_0(k1_zfmisc_1(sK13_skl)) ),
inference(component_clause,[status(thm)],[f4523]) ).
fof(f4527,plain,
( ~ sQ475_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4524,f218]) ).
fof(f4528,plain,
~ sQ475_spl,
inference(contradiction_clause,[status(thm)],[f4527]) ).
fof(f4885,plain,
! [X0] : ~ r1_tarski(k1_zfmisc_1(k1_zfmisc_1(X0)),X0),
inference(resolution,[status(thm)],[f1382,f295]) ).
fof(f5454,plain,
( ~ sQ422_spl
| $false ),
inference(resolution,[status(thm)],[f4051,f639]) ).
fof(f5467,plain,
~ sQ422_spl,
inference(contradiction_clause,[status(thm)],[f5454]) ).
fof(f5625,definition,
! [X0] :
( sQ586_spl
<=> ( r2_hidden(sK8_skl(k1_xboole_0),X0)
| r2_hidden(sK2_skl(X0,k1_xboole_0),k1_xboole_0) ) ),
introduced(definition,[new_symbols(definition,[sQ586_spl])],[split_symbol_definition]) ).
fof(f5626,plain,
! [X0] :
( ~ sQ586_spl
| r2_hidden(sK8_skl(k1_xboole_0),X0)
| r2_hidden(sK2_skl(X0,k1_xboole_0),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f5625]) ).
fof(f5650,plain,
! [X0] :
( ~ sQ586_spl
| r2_hidden(sK8_skl(k1_xboole_0),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5626,f639]) ).
fof(f5743,definition,
! [X0] :
( sQ605_spl
<=> r2_hidden(sK8_skl(k1_xboole_0),X0) ),
introduced(definition,[new_symbols(definition,[sQ605_spl])],[split_symbol_definition]) ).
fof(f5744,plain,
! [X0] :
( ~ sQ605_spl
| r2_hidden(sK8_skl(k1_xboole_0),X0) ),
inference(component_clause,[status(thm)],[f5743]) ).
fof(f5824,plain,
( ~ sQ586_spl
| $false ),
inference(resolution,[status(thm)],[f5650,f639]) ).
fof(f5836,plain,
~ sQ586_spl,
inference(contradiction_clause,[status(thm)],[f5824]) ).
fof(f5873,definition,
! [X0] :
( sQ608_spl
<=> r2_hidden(sK8_skl(a_1_1_lopclset(sK12_skl)),X0) ),
introduced(definition,[new_symbols(definition,[sQ608_spl])],[split_symbol_definition]) ).
fof(f5874,plain,
! [X0] :
( ~ sQ608_spl
| r2_hidden(sK8_skl(a_1_1_lopclset(sK12_skl)),X0) ),
inference(component_clause,[status(thm)],[f5873]) ).
fof(f5878,definition,
! [X0] :
( sQ609_spl
<=> r2_hidden(sK18_skl(a_1_1_lopclset(sK12_skl),k1_xboole_0),X0) ),
introduced(definition,[new_symbols(definition,[sQ609_spl])],[split_symbol_definition]) ).
fof(f5879,plain,
! [X0] :
( ~ sQ609_spl
| r2_hidden(sK18_skl(a_1_1_lopclset(sK12_skl),k1_xboole_0),X0) ),
inference(component_clause,[status(thm)],[f5878]) ).
fof(f6017,plain,
( ~ sQ605_spl
| $false ),
inference(resolution,[status(thm)],[f5744,f639]) ).
fof(f6027,plain,
~ sQ605_spl,
inference(contradiction_clause,[status(thm)],[f6017]) ).
fof(f6329,plain,
( ~ sQ608_spl
| $false ),
inference(resolution,[status(thm)],[f5874,f639]) ).
fof(f6339,plain,
~ sQ608_spl,
inference(contradiction_clause,[status(thm)],[f6329]) ).
fof(f6662,definition,
( sQ688_spl
<=> v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK12_skl))) ),
introduced(definition,[new_symbols(definition,[sQ688_spl])],[split_symbol_definition]) ).
fof(f6663,plain,
( ~ sQ688_spl
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK12_skl))) ),
inference(component_clause,[status(thm)],[f6662]) ).
fof(f6666,plain,
( ~ sQ688_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6663,f218]) ).
fof(f6667,plain,
~ sQ688_spl,
inference(contradiction_clause,[status(thm)],[f6666]) ).
fof(f6756,definition,
( sQ695_spl
<=> v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK15_skl))) ),
introduced(definition,[new_symbols(definition,[sQ695_spl])],[split_symbol_definition]) ).
fof(f6757,plain,
( ~ sQ695_spl
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK15_skl))) ),
inference(component_clause,[status(thm)],[f6756]) ).
fof(f6760,plain,
( ~ sQ695_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6757,f218]) ).
fof(f6761,plain,
~ sQ695_spl,
inference(contradiction_clause,[status(thm)],[f6760]) ).
fof(f6870,definition,
( sQ706_spl
<=> v1_xboole_0(k1_zfmisc_1(a_1_1_lopclset(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ706_spl])],[split_symbol_definition]) ).
fof(f6871,plain,
( ~ sQ706_spl
| v1_xboole_0(k1_zfmisc_1(a_1_1_lopclset(sK0_skl))) ),
inference(component_clause,[status(thm)],[f6870]) ).
fof(f6875,plain,
( ~ sQ706_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6871,f218]) ).
fof(f6876,plain,
~ sQ706_spl,
inference(contradiction_clause,[status(thm)],[f6875]) ).
fof(f6899,definition,
( sQ709_spl
<=> v1_xboole_0(k1_zfmisc_1(sK7_skl(sK12_skl))) ),
introduced(definition,[new_symbols(definition,[sQ709_spl])],[split_symbol_definition]) ).
fof(f6900,plain,
( ~ sQ709_spl
| v1_xboole_0(k1_zfmisc_1(sK7_skl(sK12_skl))) ),
inference(component_clause,[status(thm)],[f6899]) ).
fof(f6903,plain,
( ~ sQ709_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6900,f218]) ).
fof(f6904,plain,
~ sQ709_spl,
inference(contradiction_clause,[status(thm)],[f6903]) ).
fof(f7026,definition,
( sQ721_spl
<=> v1_xboole_0(k1_zfmisc_1(sK7_skl(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ721_spl])],[split_symbol_definition]) ).
fof(f7027,plain,
( ~ sQ721_spl
| v1_xboole_0(k1_zfmisc_1(sK7_skl(sK0_skl))) ),
inference(component_clause,[status(thm)],[f7026]) ).
fof(f7030,plain,
( ~ sQ721_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7027,f218]) ).
fof(f7031,plain,
~ sQ721_spl,
inference(contradiction_clause,[status(thm)],[f7030]) ).
fof(f7083,definition,
( sQ728_spl
<=> v1_xboole_0(k1_zfmisc_1(a_1_1_lopclset(sK12_skl))) ),
introduced(definition,[new_symbols(definition,[sQ728_spl])],[split_symbol_definition]) ).
fof(f7084,plain,
( ~ sQ728_spl
| v1_xboole_0(k1_zfmisc_1(a_1_1_lopclset(sK12_skl))) ),
inference(component_clause,[status(thm)],[f7083]) ).
fof(f7088,plain,
( ~ sQ728_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7084,f218]) ).
fof(f7089,plain,
~ sQ728_spl,
inference(contradiction_clause,[status(thm)],[f7088]) ).
fof(f7114,definition,
( sQ731_spl
<=> v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(k1_xboole_0))) ),
introduced(definition,[new_symbols(definition,[sQ731_spl])],[split_symbol_definition]) ).
fof(f7115,plain,
( ~ sQ731_spl
| v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(k1_xboole_0))) ),
inference(component_clause,[status(thm)],[f7114]) ).
fof(f7125,plain,
( ~ sQ731_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7115,f218]) ).
fof(f7126,plain,
~ sQ731_spl,
inference(contradiction_clause,[status(thm)],[f7125]) ).
fof(f7775,definition,
( sQ784_spl
<=> k1_xboole_0 = k1_zfmisc_1(k1_zfmisc_1(k1_xboole_0)) ),
introduced(definition,[new_symbols(definition,[sQ784_spl])],[split_symbol_definition]) ).
fof(f7776,plain,
( ~ sQ784_spl
| k1_xboole_0 = k1_zfmisc_1(k1_zfmisc_1(k1_xboole_0)) ),
inference(component_clause,[status(thm)],[f7775]) ).
fof(f7834,plain,
( ~ sQ784_spl
| ~ r1_tarski(k1_xboole_0,k1_xboole_0) ),
inference(paramodulation,[status(thm)],[f7776,f4885]) ).
fof(f7947,plain,
( ~ sQ784_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7834,f295]) ).
fof(f7948,plain,
~ sQ784_spl,
inference(contradiction_clause,[status(thm)],[f7947]) ).
fof(f9279,plain,
( sQ331_spl
| ~ r1_tarski(k1_xboole_0,u1_struct_0(sK15_skl)) ),
inference(resolution,[status(thm)],[f3374,f308]) ).
fof(f10101,definition,
! [X0] :
( sQ982_spl
<=> r2_hidden(sK8_skl(sK8_skl(k1_xboole_0)),X0) ),
introduced(definition,[new_symbols(definition,[sQ982_spl])],[split_symbol_definition]) ).
fof(f10102,plain,
! [X0] :
( ~ sQ982_spl
| r2_hidden(sK8_skl(sK8_skl(k1_xboole_0)),X0) ),
inference(component_clause,[status(thm)],[f10101]) ).
fof(f10409,plain,
( ~ sQ982_spl
| $false ),
inference(resolution,[status(thm)],[f10102,f639]) ).
fof(f10426,plain,
~ sQ982_spl,
inference(contradiction_clause,[status(thm)],[f10409]) ).
fof(f10881,definition,
! [X0] :
( sQ1075_spl
<=> r2_hidden(sK8_skl(u1_struct_0(sK12_skl)),X0) ),
introduced(definition,[new_symbols(definition,[sQ1075_spl])],[split_symbol_definition]) ).
fof(f10882,plain,
! [X0] :
( ~ sQ1075_spl
| r2_hidden(sK8_skl(u1_struct_0(sK12_skl)),X0) ),
inference(component_clause,[status(thm)],[f10881]) ).
fof(f11150,plain,
( ~ sQ1075_spl
| $false ),
inference(resolution,[status(thm)],[f10882,f639]) ).
fof(f11167,plain,
~ sQ1075_spl,
inference(contradiction_clause,[status(thm)],[f11150]) ).
fof(f11531,plain,
( ~ sQ609_spl
| $false ),
inference(resolution,[status(thm)],[f5879,f639]) ).
fof(f11552,plain,
~ sQ609_spl,
inference(contradiction_clause,[status(thm)],[f11531]) ).
fof(f11619,definition,
( sQ1132_spl
<=> r2_hidden(sK8_skl(k1_zfmisc_1(k1_xboole_0)),k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ1132_spl])],[split_symbol_definition]) ).
fof(f11620,plain,
( ~ sQ1132_spl
| r2_hidden(sK8_skl(k1_zfmisc_1(k1_xboole_0)),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f11619]) ).
fof(f11623,definition,
! [X0] :
( sQ1133_spl
<=> ( r2_hidden(X0,k1_xboole_0)
| ~ r1_tarski(X0,k1_xboole_0) ) ),
introduced(definition,[new_symbols(definition,[sQ1133_spl])],[split_symbol_definition]) ).
fof(f11624,plain,
! [X0] :
( ~ sQ1133_spl
| r2_hidden(X0,k1_xboole_0)
| ~ r1_tarski(X0,k1_xboole_0) ),
inference(component_clause,[status(thm)],[f11623]) ).
fof(f11648,definition,
( sQ1137_spl
<=> r1_tarski(k1_zfmisc_1(k1_xboole_0),k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ1137_spl])],[split_symbol_definition]) ).
fof(f11649,plain,
( ~ sQ1137_spl
| r1_tarski(k1_zfmisc_1(k1_xboole_0),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f11648]) ).
fof(f11653,plain,
! [X0] :
( ~ sQ1133_spl
| ~ r1_tarski(X0,k1_xboole_0) ),
inference(forward_subsumption_resolution,[status(thm)],[f11624,f639]) ).
fof(f11659,plain,
( ~ sQ1132_spl
| r2_hidden(k1_xboole_0,k1_xboole_0) ),
inference(forward_demodulation,[status(thm)],[f2223,f11620]) ).
fof(f11660,plain,
( ~ sQ1132_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11659,f639]) ).
fof(f11661,plain,
~ sQ1132_spl,
inference(contradiction_clause,[status(thm)],[f11660]) ).
fof(f11750,plain,
( ~ sQ1133_spl
| $false ),
inference(resolution,[status(thm)],[f11653,f2306]) ).
fof(f11755,definition,
! [X0] :
( sQ1140_spl
<=> r2_hidden(sK14_skl(k1_xboole_0),X0) ),
introduced(definition,[new_symbols(definition,[sQ1140_spl])],[split_symbol_definition]) ).
fof(f11756,plain,
! [X0] :
( ~ sQ1140_spl
| r2_hidden(sK14_skl(k1_xboole_0),X0) ),
inference(component_clause,[status(thm)],[f11755]) ).
fof(f11759,definition,
! [X0] :
( sQ1141_spl
<=> r2_hidden(sK16_skl(k1_xboole_0),X0) ),
introduced(definition,[new_symbols(definition,[sQ1141_spl])],[split_symbol_definition]) ).
fof(f11760,plain,
! [X0] :
( ~ sQ1141_spl
| r2_hidden(sK16_skl(k1_xboole_0),X0) ),
inference(component_clause,[status(thm)],[f11759]) ).
fof(f11764,plain,
~ sQ1133_spl,
inference(contradiction_clause,[status(thm)],[f11750]) ).
fof(f11795,plain,
( ~ sQ1141_spl
| $false ),
inference(resolution,[status(thm)],[f11760,f639]) ).
fof(f11812,plain,
~ sQ1141_spl,
inference(contradiction_clause,[status(thm)],[f11795]) ).
fof(f11906,plain,
( ~ sQ1140_spl
| $false ),
inference(resolution,[status(thm)],[f11756,f639]) ).
fof(f11923,plain,
~ sQ1140_spl,
inference(contradiction_clause,[status(thm)],[f11906]) ).
fof(f11927,plain,
( ~ sQ1137_spl
| ~ r1_tarski(k1_zfmisc_1(k1_xboole_0),k1_xboole_0) ),
inference(resolution,[status(thm)],[f11649,f1382]) ).
fof(f11934,plain,
( ~ sQ1137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11927,f11649]) ).
fof(f11935,plain,
~ sQ1137_spl,
inference(contradiction_clause,[status(thm)],[f11934]) ).
fof(f12149,definition,
( sQ1161_spl
<=> v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(a_1_1_lopclset(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ1161_spl])],[split_symbol_definition]) ).
fof(f12150,plain,
( ~ sQ1161_spl
| v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(a_1_1_lopclset(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f12149]) ).
fof(f12157,plain,
( ~ sQ1161_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12150,f218]) ).
fof(f12158,plain,
~ sQ1161_spl,
inference(contradiction_clause,[status(thm)],[f12157]) ).
fof(f12633,definition,
! [X0] :
( sQ1184_spl
<=> ( r2_hidden(sK8_skl(u1_struct_0(sK0_skl)),X0)
| r2_hidden(sK2_skl(X0,sK10_skl(k1_xboole_0,sK8_skl(u1_struct_0(sK0_skl)),sK0_skl)),k1_xboole_0) ) ),
introduced(definition,[new_symbols(definition,[sQ1184_spl])],[split_symbol_definition]) ).
fof(f12634,plain,
! [X0] :
( ~ sQ1184_spl
| r2_hidden(sK8_skl(u1_struct_0(sK0_skl)),X0)
| r2_hidden(sK2_skl(X0,sK10_skl(k1_xboole_0,sK8_skl(u1_struct_0(sK0_skl)),sK0_skl)),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f12633]) ).
fof(f12645,definition,
( sQ1187_spl
<=> r2_hidden(sK8_skl(u1_struct_0(sK0_skl)),k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ1187_spl])],[split_symbol_definition]) ).
fof(f12646,plain,
( ~ sQ1187_spl
| r2_hidden(sK8_skl(u1_struct_0(sK0_skl)),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f12645]) ).
fof(f12663,plain,
( ~ sQ1187_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12646,f639]) ).
fof(f12664,plain,
~ sQ1187_spl,
inference(contradiction_clause,[status(thm)],[f12663]) ).
fof(f12665,plain,
! [X0] :
( ~ sQ1184_spl
| r2_hidden(sK8_skl(u1_struct_0(sK0_skl)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f12634,f639]) ).
fof(f12687,plain,
( sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f567,f262]) ).
fof(f12688,plain,
sQ40_spl,
inference(contradiction_clause,[status(thm)],[f12687]) ).
fof(f12689,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f563,f267]) ).
fof(f12690,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f12689]) ).
fof(f12717,plain,
( ~ sQ115_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1242,f639]) ).
fof(f12718,plain,
~ sQ115_spl,
inference(contradiction_clause,[status(thm)],[f12717]) ).
fof(f12750,definition,
( sQ1197_spl
<=> v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK6_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ1197_spl])],[split_symbol_definition]) ).
fof(f12751,plain,
( ~ sQ1197_spl
| v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK6_skl)))) ),
inference(component_clause,[status(thm)],[f12750]) ).
fof(f12757,plain,
( ~ sQ1197_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12751,f218]) ).
fof(f12758,plain,
~ sQ1197_spl,
inference(contradiction_clause,[status(thm)],[f12757]) ).
fof(f12864,definition,
! [X0] :
( sQ1206_spl
<=> r2_hidden(sK8_skl(a_1_1_lopclset(sK6_skl)),X0) ),
introduced(definition,[new_symbols(definition,[sQ1206_spl])],[split_symbol_definition]) ).
fof(f12865,plain,
! [X0] :
( ~ sQ1206_spl
| r2_hidden(sK8_skl(a_1_1_lopclset(sK6_skl)),X0) ),
inference(component_clause,[status(thm)],[f12864]) ).
fof(f12997,plain,
( ~ sQ1184_spl
| $false ),
inference(resolution,[status(thm)],[f12665,f639]) ).
fof(f13024,plain,
~ sQ1184_spl,
inference(contradiction_clause,[status(thm)],[f12997]) ).
fof(f13060,plain,
( ~ sQ1206_spl
| $false ),
inference(resolution,[status(thm)],[f12865,f639]) ).
fof(f13084,plain,
~ sQ1206_spl,
inference(contradiction_clause,[status(thm)],[f13060]) ).
fof(f13776,definition,
! [X0] :
( sQ1277_spl
<=> ( r2_hidden(sK8_skl(sK14_skl(k1_xboole_0)),X0)
| r2_hidden(sK2_skl(X0,sK14_skl(k1_xboole_0)),k1_xboole_0) ) ),
introduced(definition,[new_symbols(definition,[sQ1277_spl])],[split_symbol_definition]) ).
fof(f13777,plain,
! [X0] :
( ~ sQ1277_spl
| r2_hidden(sK8_skl(sK14_skl(k1_xboole_0)),X0)
| r2_hidden(sK2_skl(X0,sK14_skl(k1_xboole_0)),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f13776]) ).
fof(f13796,plain,
! [X0] :
( ~ sQ1277_spl
| r2_hidden(sK8_skl(sK14_skl(k1_xboole_0)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f13777,f639]) ).
fof(f13905,plain,
( ~ sQ1277_spl
| $false ),
inference(resolution,[status(thm)],[f13796,f639]) ).
fof(f13929,plain,
~ sQ1277_spl,
inference(contradiction_clause,[status(thm)],[f13905]) ).
fof(f13961,definition,
( sQ1290_spl
<=> r2_hidden(sK8_skl(sK14_skl(sK8_skl(k1_zfmisc_1(k1_xboole_0)))),k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ1290_spl])],[split_symbol_definition]) ).
fof(f13962,plain,
( ~ sQ1290_spl
| r2_hidden(sK8_skl(sK14_skl(sK8_skl(k1_zfmisc_1(k1_xboole_0)))),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f13961]) ).
fof(f13965,plain,
( ~ sQ1290_spl
| r2_hidden(sK8_skl(sK14_skl(k1_xboole_0)),k1_xboole_0) ),
inference(forward_demodulation,[status(thm)],[f2223,f13962]) ).
fof(f13966,plain,
( ~ sQ1290_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13965,f639]) ).
fof(f13967,plain,
~ sQ1290_spl,
inference(contradiction_clause,[status(thm)],[f13966]) ).
fof(f14031,definition,
( sQ1299_spl
<=> r2_hidden(sK8_skl(sK14_skl(k1_xboole_0)),k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ1299_spl])],[split_symbol_definition]) ).
fof(f14032,plain,
( ~ sQ1299_spl
| r2_hidden(sK8_skl(sK14_skl(k1_xboole_0)),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f14031]) ).
fof(f14048,plain,
( ~ sQ1299_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14032,f639]) ).
fof(f14049,plain,
~ sQ1299_spl,
inference(contradiction_clause,[status(thm)],[f14048]) ).
fof(f14172,plain,
( sQ331_spl
| r2_hidden(sK2_skl(u1_struct_0(sK15_skl),k1_xboole_0),k1_xboole_0) ),
inference(resolution,[status(thm)],[f9279,f188]) ).
fof(f14173,plain,
( sQ331_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14172,f639]) ).
fof(f14174,plain,
sQ331_spl,
inference(contradiction_clause,[status(thm)],[f14173]) ).
fof(f14380,plain,
( ~ sQ203_spl
| ~ m1_filter_0(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),sK0_skl)
| r2_hidden(sK2_skl(a_1_1_lopclset(sK0_skl),a_2_0_lopclset(sK0_skl,sK1_skl)),a_1_1_lopclset(sK0_skl))
| ~ l3_lattices(sK0_skl)
| v3_realset2(sK0_skl)
| ~ v17_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f2410,f323]) ).
fof(f14381,plain,
( ~ sQ203_spl
| ~ sQ202_spl
| sQ205_spl
| ~ sQ3_spl
| sQ2_spl
| ~ sQ1_spl
| ~ sQ5_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f14380,f329,f345,f332,f335,f338,f2427,f2405,f2409]) ).
fof(f14577,plain,
( ~ sQ205_spl
| r1_tarski(a_2_0_lopclset(sK0_skl,sK1_skl),a_1_1_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f2428,f189]) ).
fof(f14583,plain,
( ~ sQ205_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14577,f351]) ).
fof(f14584,plain,
( ~ sQ205_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f14583]) ).
fof(f14585,plain,
$false,
inference(sat_refutation,[status(thm)],[f344,f358,f360,f362,f364,f366,f652,f662,f950,f1082,f1084,f1534,f1887,f2094,f2096,f2098,f2102,f2153,f2173,f2185,f2408,f2412,f2414,f2565,f2656,f2975,f3377,f3413,f3449,f4356,f4528,f5467,f5836,f6027,f6339,f6667,f6761,f6876,f6904,f7031,f7089,f7126,f7948,f10426,f11167,f11552,f11661,f11764,f11812,f11923,f11935,f12158,f12664,f12688,f12690,f12718,f12758,f13024,f13084,f13929,f13967,f14049,f14174,f14381,f14584]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT288+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n020.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Sun Sep 20 23:28:02 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.48 % Drodi V4.1.1
% 59.42/8.08 % Refutation found
% 59.42/8.08 % SZS status Theorem for theBenchmark: Theorem is valid
% 59.42/8.08 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 16.03/8.18 % Elapsed time: 7.707088 seconds
% 16.03/8.18 % CPU time: 60.153886 seconds
% 16.03/8.18 % Total memory used: 257.429 MB
% 16.03/8.18 % Net memory used: 239.342 MB
%------------------------------------------------------------------------------