%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT303+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 : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:02:38 PM UTC 2026
% Result : Theorem 0.22s 0.88s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 54
% Syntax : Number of formulae : 215 ( 41 unt; 32 def)
% Number of atoms : 596 ( 24 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 629 ( 248 ~; 258 |; 61 &)
% ( 39 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 55 ( 53 usr; 33 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-2 aty)
% Number of variables : 110 ( 106 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ( m2_filter_2(k6_domain_1(u1_struct_0(A),B),A)
=> v13_lattices(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ( m2_filter_2(k6_domain_1(u1_struct_0(A),B),A)
=> v13_lattices(A) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f14,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> k5_filter_2(A,B) = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A,B] :
( ( m1_subset_1(B,u1_struct_0(A))
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k5_filter_2(A,B),u1_struct_0(k1_lattice2(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [A] :
( l2_lattices(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
? [A] : l3_lattices(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A] :
? [B] : m1_subset_1(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [A] : ~ v1_xboole_0(k1_tarski(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,axiom,
! [A,B] :
( ( m1_subset_1(B,A)
& ~ v1_xboole_0(A) )
=> k6_domain_1(A,B) = k1_tarski(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f79,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_2(B,A)
<=> m1_filter_0(B,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,axiom,
! [A,B] : r1_tarski(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ( m1_filter_0(k6_domain_1(u1_struct_0(A),B),A)
=> v14_lattices(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
<=> m1_filter_2(B,k1_lattice2(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f89,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v13_lattices(A)
<=> v14_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f90,axiom,
! [A] :
( v1_xboole_0(A)
=> A = k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f93,plain,
? [A] :
( ? [B] :
( ~ v13_lattices(A)
& m2_filter_2(k6_domain_1(u1_struct_0(A),B),A)
& m1_subset_1(B,u1_struct_0(A)) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f94,plain,
( ~ v13_lattices(sK0_skl)
& m2_filter_2(k6_domain_1(u1_struct_0(sK0_skl),sK1_skl),sK0_skl)
& m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))
& l3_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)],[f93]) ).
fof(f95,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f96,plain,
v10_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f97,plain,
l3_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f98,plain,
m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f99,plain,
m2_filter_2(k6_domain_1(u1_struct_0(sK0_skl),sK1_skl),sK0_skl),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f100,plain,
~ v13_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f136,plain,
! [A] :
( ! [B] :
( k5_filter_2(A,B) = B
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f137,plain,
! [X0,X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f141,plain,
! [A] :
( ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f143,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f144,plain,
! [A,B] :
( m1_subset_1(k5_filter_2(A,B),u1_struct_0(k1_lattice2(A)))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f145,plain,
! [X0,X1] :
( m1_subset_1(k5_filter_2(X0,X1),u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f150,plain,
! [A] :
( l1_struct_0(A)
| ~ l2_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f151,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f152,plain,
! [A] :
( ( l2_lattices(A)
& l1_lattices(A) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f154,plain,
! [X0] :
( l2_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f182,plain,
l3_lattices(sK5_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f40]) ).
fof(f183,plain,
l3_lattices(sK5_skl),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f192,plain,
! [A] : m1_subset_1(sK9_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(B,sK9_skl(A))],[f44]) ).
fof(f193,plain,
! [X0] : m1_subset_1(sK9_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f202,plain,
! [A] :
( ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) )
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f203,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f205,plain,
! [A] :
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f206,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| ~ l1_struct_0(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f207,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f208,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f215,plain,
! [X0] : ~ v1_xboole_0(k1_tarski(X0)),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f243,plain,
! [A] :
( ( v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f60]) ).
fof(f252,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f328,plain,
! [A,B] :
( k6_domain_1(A,B) = k1_tarski(B)
| ~ m1_subset_1(B,A)
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f78]) ).
fof(f329,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f328]) ).
fof(f330,plain,
! [A] :
( ! [B] :
( m1_filter_2(B,A)
<=> m1_filter_0(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f79]) ).
fof(f331,plain,
! [A] :
( ! [B] :
( ( ~ m1_filter_0(B,A)
| m1_filter_2(B,A) )
& ( m1_filter_0(B,A)
| ~ m1_filter_2(B,A) ) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f330]) ).
fof(f332,plain,
! [A] :
( ( ! [B] :
( ~ m1_filter_0(B,A)
| m1_filter_2(B,A) )
& ! [B] :
( m1_filter_0(B,A)
| ~ m1_filter_2(B,A) ) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(miniscoping,[status(thm)],[f331]) ).
fof(f333,plain,
! [X0,X1] :
( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f332]) ).
fof(f339,plain,
! [A] : r1_tarski(A,A),
inference(miniscoping,[status(thm)],[f81]) ).
fof(f340,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[status(thm)],[f339]) ).
fof(f341,plain,
! [A] :
( ! [B] :
( v14_lattices(A)
| ~ m1_filter_0(k6_domain_1(u1_struct_0(A),B),A)
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f342,plain,
! [X0,X1] :
( v14_lattices(X0)
| ~ m1_filter_0(k6_domain_1(u1_struct_0(X0),X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f345,plain,
! [A] :
( ! [B] :
( m2_filter_2(B,A)
<=> m1_filter_2(B,k1_lattice2(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f346,plain,
! [A] :
( ! [B] :
( ( ~ m1_filter_2(B,k1_lattice2(A))
| m2_filter_2(B,A) )
& ( m1_filter_2(B,k1_lattice2(A))
| ~ m2_filter_2(B,A) ) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f345]) ).
fof(f347,plain,
! [A] :
( ( ! [B] :
( ~ m1_filter_2(B,k1_lattice2(A))
| m2_filter_2(B,A) )
& ! [B] :
( m1_filter_2(B,k1_lattice2(A))
| ~ m2_filter_2(B,A) ) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(miniscoping,[status(thm)],[f346]) ).
fof(f348,plain,
! [X0,X1] :
( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f352,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)],[f86]) ).
fof(f353,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)],[f352]) ).
fof(f355,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[status(thm)],[f353]) ).
fof(f362,plain,
! [A] :
( ( v13_lattices(A)
<=> v14_lattices(k1_lattice2(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f89]) ).
fof(f363,plain,
! [A] :
( ( ( ~ v14_lattices(k1_lattice2(A))
| v13_lattices(A) )
& ( v14_lattices(k1_lattice2(A))
| ~ v13_lattices(A) ) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f362]) ).
fof(f365,plain,
! [X0] :
( ~ v14_lattices(k1_lattice2(X0))
| v13_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f363]) ).
fof(f366,plain,
! [A] :
( A = k1_xboole_0
| ~ v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f90]) ).
fof(f367,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f377,definition,
( sQ0_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f378,plain,
( ~ sQ0_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f377]) ).
fof(f380,definition,
( sQ1_spl
<=> l3_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f382,plain,
( sQ1_spl
| ~ l3_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f380]) ).
fof(f387,definition,
( sQ3_spl
<=> v10_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f389,plain,
( sQ3_spl
| ~ v10_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f387]) ).
fof(f401,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f378,f95]) ).
fof(f402,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f401]) ).
fof(f403,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f382,f97]) ).
fof(f404,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f403]) ).
fof(f478,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f389,f96]) ).
fof(f479,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f478]) ).
fof(f702,definition,
( sQ55_spl
<=> v13_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f703,plain,
( ~ sQ55_spl
| v13_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f702]) ).
fof(f719,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| ~ m1_subset_1(X1,X0)
| X0 = k1_xboole_0 ),
inference(resolution,[status(thm)],[f367,f329]) ).
fof(f742,plain,
( k5_filter_2(sK0_skl,sK1_skl) = sK1_skl
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f137,f98]) ).
fof(f743,definition,
( sQ57_spl
<=> k5_filter_2(sK0_skl,sK1_skl) = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f744,plain,
( ~ sQ57_spl
| k5_filter_2(sK0_skl,sK1_skl) = sK1_skl ),
inference(component_clause,[status(thm)],[f743]) ).
fof(f746,plain,
( sQ57_spl
| ~ sQ1_spl
| ~ sQ3_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f742,f377,f387,f380,f743]) ).
fof(f889,definition,
( sQ86_spl
<=> k6_domain_1(u1_struct_0(sK0_skl),sK1_skl) = k1_tarski(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f890,plain,
( ~ sQ86_spl
| k6_domain_1(u1_struct_0(sK0_skl),sK1_skl) = k1_tarski(sK1_skl) ),
inference(component_clause,[status(thm)],[f889]) ).
fof(f972,plain,
( m1_subset_1(k5_filter_2(sK0_skl,sK1_skl),u1_struct_0(k1_lattice2(sK0_skl)))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f145,f98]) ).
fof(f974,definition,
( sQ94_spl
<=> m1_subset_1(k5_filter_2(sK0_skl,sK1_skl),u1_struct_0(k1_lattice2(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f975,plain,
( ~ sQ94_spl
| m1_subset_1(k5_filter_2(sK0_skl,sK1_skl),u1_struct_0(k1_lattice2(sK0_skl))) ),
inference(component_clause,[status(thm)],[f974]) ).
fof(f977,plain,
( sQ94_spl
| ~ sQ1_spl
| ~ sQ3_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f972,f377,f387,f380,f974]) ).
fof(f978,plain,
( ~ sQ94_spl
| ~ sQ57_spl
| m1_subset_1(sK1_skl,u1_struct_0(k1_lattice2(sK0_skl))) ),
inference(forward_demodulation,[status(thm)],[f744,f975]) ).
fof(f982,plain,
( ~ sQ94_spl
| ~ sQ57_spl
| k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl) = k1_tarski(sK1_skl)
| u1_struct_0(k1_lattice2(sK0_skl)) = k1_xboole_0 ),
inference(resolution,[status(thm)],[f978,f719]) ).
fof(f983,definition,
( sQ95_spl
<=> v3_struct_0(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f984,plain,
( ~ sQ95_spl
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f983]) ).
fof(f986,definition,
( sQ96_spl
<=> v10_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f989,definition,
( sQ97_spl
<=> l3_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f991,plain,
( sQ97_spl
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f989]) ).
fof(f1000,definition,
( sQ100_spl
<=> u1_struct_0(k1_lattice2(sK0_skl)) = k1_xboole_0 ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1001,plain,
( ~ sQ100_spl
| u1_struct_0(k1_lattice2(sK0_skl)) = k1_xboole_0 ),
inference(component_clause,[status(thm)],[f1000]) ).
fof(f1003,definition,
( sQ101_spl
<=> k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl) = k1_tarski(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1004,plain,
( ~ sQ101_spl
| k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl) = k1_tarski(sK1_skl) ),
inference(component_clause,[status(thm)],[f1003]) ).
fof(f1006,plain,
( ~ sQ94_spl
| ~ sQ57_spl
| sQ101_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f982,f1000,f1003,f743,f974]) ).
fof(f1007,plain,
( sQ97_spl
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f991,f143]) ).
fof(f1008,plain,
( sQ97_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f1007,f380,f989]) ).
fof(f1042,definition,
( sQ108_spl
<=> v14_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1043,plain,
( ~ sQ108_spl
| v14_lattices(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1042]) ).
fof(f1075,plain,
( ~ sQ86_spl
| m2_filter_2(k1_tarski(sK1_skl),sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f890,f99]) ).
fof(f1131,plain,
( ~ sQ95_spl
| ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f203,f984]) ).
fof(f1132,plain,
( ~ sQ95_spl
| ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1131,f377,f380,f983]) ).
fof(f1133,plain,
! [X0,X1] :
( k6_domain_1(u1_struct_0(X0),X1) = k1_tarski(X1)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_struct_0(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f206,f329]) ).
fof(f1134,plain,
( ~ sQ100_spl
| ~ v1_xboole_0(k1_xboole_0)
| ~ l1_struct_0(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f1001,f206]) ).
fof(f1135,definition,
( sQ116_spl
<=> l1_struct_0(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1137,plain,
( sQ116_spl
| ~ l1_struct_0(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1135]) ).
fof(f1138,definition,
( sQ117_spl
<=> v1_xboole_0(k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f1140,plain,
( sQ117_spl
| ~ v1_xboole_0(k1_xboole_0) ),
inference(component_clause,[status(thm)],[f1138]) ).
fof(f1141,plain,
( ~ sQ100_spl
| ~ sQ117_spl
| ~ sQ116_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f1134,f983,f1135,f1138,f1000]) ).
fof(f1142,plain,
( sQ116_spl
| ~ l2_lattices(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f1137,f151]) ).
fof(f1145,plain,
( sQ116_spl
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f1142,f154]) ).
fof(f1146,plain,
( sQ116_spl
| ~ sQ97_spl ),
inference(split_clause,[status(thm)],[f1145,f989,f1135]) ).
fof(f1281,plain,
( ~ sQ101_spl
| v14_lattices(k1_lattice2(sK0_skl))
| ~ m1_filter_0(k1_tarski(sK1_skl),k1_lattice2(sK0_skl))
| ~ m1_subset_1(sK1_skl,u1_struct_0(k1_lattice2(sK0_skl)))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f1004,f342]) ).
fof(f1284,definition,
( sQ127_spl
<=> m1_subset_1(sK1_skl,u1_struct_0(k1_lattice2(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1286,plain,
( sQ127_spl
| ~ m1_subset_1(sK1_skl,u1_struct_0(k1_lattice2(sK0_skl))) ),
inference(component_clause,[status(thm)],[f1284]) ).
fof(f1287,definition,
( sQ128_spl
<=> m1_filter_0(k1_tarski(sK1_skl),k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1290,plain,
( ~ sQ101_spl
| sQ108_spl
| ~ sQ128_spl
| ~ sQ127_spl
| ~ sQ97_spl
| ~ sQ96_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f1281,f983,f986,f989,f1284,f1287,f1042,f1003]) ).
fof(f1302,plain,
( sQ127_spl
| ~ sQ94_spl
| ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1286,f978]) ).
fof(f1303,plain,
( sQ127_spl
| ~ sQ94_spl
| ~ sQ57_spl ),
inference(contradiction_clause,[status(thm)],[f1302]) ).
fof(f1310,plain,
( sQ117_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1140,f208]) ).
fof(f1311,plain,
sQ117_spl,
inference(contradiction_clause,[status(thm)],[f1310]) ).
fof(f1476,plain,
( k6_domain_1(u1_struct_0(sK0_skl),sK1_skl) = k1_tarski(sK1_skl)
| ~ l1_struct_0(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1133,f98]) ).
fof(f1479,definition,
( sQ146_spl
<=> l1_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f1481,plain,
( sQ146_spl
| ~ l1_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f1479]) ).
fof(f1482,plain,
( sQ86_spl
| ~ sQ146_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1476,f377,f1479,f889]) ).
fof(f1496,plain,
( v10_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f252,f96]) ).
fof(f1505,plain,
( sQ96_spl
| ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1496,f377,f380,f986]) ).
fof(f1506,plain,
( ~ sQ108_spl
| v13_lattices(sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1043,f365]) ).
fof(f1507,plain,
( ~ sQ108_spl
| sQ55_spl
| ~ sQ1_spl
| ~ sQ3_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1506,f377,f387,f380,f702,f1042]) ).
fof(f1592,plain,
( ~ sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f703,f100]) ).
fof(f1593,plain,
~ sQ55_spl,
inference(contradiction_clause,[status(thm)],[f1592]) ).
fof(f2194,definition,
( sQ244_spl
<=> v1_xboole_0(k1_tarski(sK9_skl(sK16_skl))) ),
introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition]) ).
fof(f2195,plain,
( ~ sQ244_spl
| v1_xboole_0(k1_tarski(sK9_skl(sK16_skl))) ),
inference(component_clause,[status(thm)],[f2194]) ).
fof(f2197,definition,
( sQ245_spl
<=> v1_xboole_0(k1_zfmisc_1(sK16_skl)) ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f2198,plain,
( ~ sQ245_spl
| v1_xboole_0(k1_zfmisc_1(sK16_skl)) ),
inference(component_clause,[status(thm)],[f2197]) ).
fof(f2204,definition,
( sQ247_spl
<=> v1_xboole_0(k1_tarski(sK9_skl(sK20_skl))) ),
introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition]) ).
fof(f2205,plain,
( ~ sQ247_spl
| v1_xboole_0(k1_tarski(sK9_skl(sK20_skl))) ),
inference(component_clause,[status(thm)],[f2204]) ).
fof(f2207,definition,
( sQ248_spl
<=> v1_xboole_0(k1_zfmisc_1(sK20_skl)) ),
introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition]) ).
fof(f2208,plain,
( ~ sQ248_spl
| v1_xboole_0(k1_zfmisc_1(sK20_skl)) ),
inference(component_clause,[status(thm)],[f2207]) ).
fof(f2214,definition,
( sQ250_spl
<=> v1_xboole_0(k1_tarski(sK9_skl(sK22_skl))) ),
introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition]) ).
fof(f2215,plain,
( ~ sQ250_spl
| v1_xboole_0(k1_tarski(sK9_skl(sK22_skl))) ),
inference(component_clause,[status(thm)],[f2214]) ).
fof(f2217,definition,
( sQ251_spl
<=> v1_xboole_0(k1_zfmisc_1(sK22_skl)) ),
introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition]) ).
fof(f2218,plain,
( ~ sQ251_spl
| v1_xboole_0(k1_zfmisc_1(sK22_skl)) ),
inference(component_clause,[status(thm)],[f2217]) ).
fof(f2224,definition,
( sQ253_spl
<=> v1_xboole_0(k1_tarski(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition]) ).
fof(f2225,plain,
( ~ sQ253_spl
| v1_xboole_0(k1_tarski(sK1_skl)) ),
inference(component_clause,[status(thm)],[f2224]) ).
fof(f2227,definition,
( sQ254_spl
<=> v1_xboole_0(k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f2228,plain,
( ~ sQ254_spl
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f2227]) ).
fof(f2262,plain,
( ~ sQ253_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2225,f215]) ).
fof(f2263,plain,
~ sQ253_spl,
inference(contradiction_clause,[status(thm)],[f2262]) ).
fof(f2265,plain,
( ~ sQ254_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2228,f207]) ).
fof(f2266,plain,
~ sQ254_spl,
inference(contradiction_clause,[status(thm)],[f2265]) ).
fof(f2267,plain,
( ~ sQ251_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2218,f207]) ).
fof(f2268,plain,
~ sQ251_spl,
inference(contradiction_clause,[status(thm)],[f2267]) ).
fof(f2269,plain,
( ~ sQ250_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2215,f215]) ).
fof(f2270,plain,
~ sQ250_spl,
inference(contradiction_clause,[status(thm)],[f2269]) ).
fof(f2271,plain,
( ~ sQ248_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2208,f207]) ).
fof(f2272,plain,
~ sQ248_spl,
inference(contradiction_clause,[status(thm)],[f2271]) ).
fof(f2273,plain,
( ~ sQ247_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2205,f215]) ).
fof(f2274,plain,
~ sQ247_spl,
inference(contradiction_clause,[status(thm)],[f2273]) ).
fof(f2275,plain,
( ~ sQ245_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2198,f207]) ).
fof(f2276,plain,
~ sQ245_spl,
inference(contradiction_clause,[status(thm)],[f2275]) ).
fof(f2380,plain,
( sQ146_spl
| ~ l2_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f1481,f151]) ).
fof(f2382,plain,
( sQ146_spl
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f2380,f154]) ).
fof(f2383,plain,
( sQ146_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f2382,f380,f1479]) ).
fof(f2701,definition,
( sQ319_spl
<=> v1_xboole_0(k1_tarski(k1_xboole_0)) ),
introduced(definition,[new_symbols(definition,[sQ319_spl])],[split_symbol_definition]) ).
fof(f2702,plain,
( ~ sQ319_spl
| v1_xboole_0(k1_tarski(k1_xboole_0)) ),
inference(component_clause,[status(thm)],[f2701]) ).
fof(f2709,plain,
( ~ sQ319_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2702,f215]) ).
fof(f2710,plain,
~ sQ319_spl,
inference(contradiction_clause,[status(thm)],[f2709]) ).
fof(f2753,plain,
( ~ sQ244_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2195,f215]) ).
fof(f2754,plain,
~ sQ244_spl,
inference(contradiction_clause,[status(thm)],[f2753]) ).
fof(f2803,definition,
( sQ324_spl
<=> l3_lattices(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ324_spl])],[split_symbol_definition]) ).
fof(f2805,plain,
( sQ324_spl
| ~ l3_lattices(sK5_skl) ),
inference(component_clause,[status(thm)],[f2803]) ).
fof(f2807,plain,
( sQ324_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2805,f183]) ).
fof(f2808,plain,
sQ324_spl,
inference(contradiction_clause,[status(thm)],[f2807]) ).
fof(f3121,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m1_filter_0(X1,k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0)) ),
inference(resolution,[status(thm)],[f333,f348]) ).
fof(f3123,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m1_filter_0(X1,k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3121,f203]) ).
fof(f3256,definition,
( sQ390_spl
<=> m1_subset_1(sK9_skl(sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition]) ).
fof(f3258,plain,
( sQ390_spl
| ~ m1_subset_1(sK9_skl(sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f3256]) ).
fof(f3264,plain,
( sQ390_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3258,f193]) ).
fof(f3265,plain,
sQ390_spl,
inference(contradiction_clause,[status(thm)],[f3264]) ).
fof(f3443,definition,
( sQ417_spl
<=> v1_xboole_0(k1_tarski(sK9_skl(sK1_skl))) ),
introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition]) ).
fof(f3444,plain,
( ~ sQ417_spl
| v1_xboole_0(k1_tarski(sK9_skl(sK1_skl))) ),
inference(component_clause,[status(thm)],[f3443]) ).
fof(f3446,definition,
( sQ418_spl
<=> v1_xboole_0(k1_zfmisc_1(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ418_spl])],[split_symbol_definition]) ).
fof(f3447,plain,
( ~ sQ418_spl
| v1_xboole_0(k1_zfmisc_1(sK1_skl)) ),
inference(component_clause,[status(thm)],[f3446]) ).
fof(f3454,plain,
( ~ sQ418_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3447,f207]) ).
fof(f3455,plain,
~ sQ418_spl,
inference(contradiction_clause,[status(thm)],[f3454]) ).
fof(f3456,plain,
( ~ sQ417_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3444,f215]) ).
fof(f3457,plain,
~ sQ417_spl,
inference(contradiction_clause,[status(thm)],[f3456]) ).
fof(f3491,definition,
( sQ422_spl
<=> m1_subset_1(sK1_skl,k1_zfmisc_1(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition]) ).
fof(f3493,plain,
( sQ422_spl
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(sK1_skl)) ),
inference(component_clause,[status(thm)],[f3491]) ).
fof(f3525,plain,
( sQ422_spl
| ~ r1_tarski(sK1_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f3493,f355]) ).
fof(f3526,plain,
( sQ422_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3525,f340]) ).
fof(f3527,plain,
sQ422_spl,
inference(contradiction_clause,[status(thm)],[f3526]) ).
fof(f3528,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m1_filter_0(X1,k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3123,f252]) ).
fof(f3529,plain,
( ~ sQ86_spl
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| m1_filter_0(k1_tarski(sK1_skl),k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f3528,f1075]) ).
fof(f3534,plain,
( ~ sQ86_spl
| ~ sQ1_spl
| ~ sQ3_spl
| sQ0_spl
| sQ128_spl
| ~ sQ97_spl ),
inference(split_clause,[status(thm)],[f3529,f989,f1287,f377,f387,f380,f889]) ).
fof(f3549,plain,
$false,
inference(sat_refutation,[status(thm)],[f402,f404,f479,f746,f977,f1006,f1008,f1132,f1141,f1146,f1290,f1303,f1311,f1482,f1505,f1507,f1593,f2263,f2266,f2268,f2270,f2272,f2274,f2276,f2383,f2710,f2754,f2808,f3265,f3455,f3457,f3527,f3534]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT303+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.49 % Computer : n007.cluster.edu
% 0.18/0.49 % Model : x86_64 x86_64
% 0.18/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.49 % Memory : 8046.5625MB
% 0.18/0.49 % OS : Linux 6.8.0-71-generic
% 0.18/0.49 % CPULimit : 300
% 0.18/0.49 % WCLimit : 300
% 0.18/0.49 % DateTime : Sun Sep 20 23:28:50 UTC 2026
% 0.18/0.49 % CPUTime :
% 0.18/0.52 % Drodi V4.1.1
% 0.22/0.88 % Refutation found
% 0.22/0.88 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.22/0.88 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.36/0.94 % Elapsed time: 0.424956 seconds
% 0.36/0.94 % CPU time: 2.734860 seconds
% 0.36/0.94 % Total memory used: 127.853 MB
% 0.36/0.94 % Net memory used: 126.206 MB
%------------------------------------------------------------------------------