%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT289+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:34 PM UTC 2026
% Result : Theorem 0.13s 0.50s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 25
% Syntax : Number of formulae : 116 ( 18 unt; 17 def)
% Number of atoms : 415 ( 13 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 489 ( 190 ~; 203 |; 62 &)
% ( 20 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 18 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-4 aty)
% Number of variables : 82 ( 79 !; 3 ?)
% 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))
=> ! [C] :
( m1_filter_0(C,A)
=> ~ ( r2_hidden(B,C)
& ~ r2_hidden(C,k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),B))
& v1_filter_0(C,A) ) ) ) ),
file('/export/starexec/sandbox/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))
=> ! [C] :
( m1_filter_0(C,A)
=> ~ ( r2_hidden(B,C)
& ~ r2_hidden(C,k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),B))
& v1_filter_0(C,A) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f35,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [A,B,C] :
~ ( v1_xboole_0(C)
& m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [A,B,C,D] :
( ( m1_subset_1(D,A)
& m1_relset_1(C,A,B)
& v1_funct_2(C,A,B)
& v1_funct_1(C)
& ~ v1_xboole_0(A) )
=> k8_funct_2(A,B,C,D) = k1_funct_1(C,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k9_lopclset(A) = k8_lopclset(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( m2_relset_1(k9_lopclset(A),u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)))
& v1_funct_2(k9_lopclset(A),u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)))
& v1_funct_1(k9_lopclset(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_0(B,A)
=> ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,axiom,
! [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))
=> ! [C] :
( m1_filter_0(C,A)
=> ( r2_hidden(C,k1_funct_1(k8_lopclset(A),B))
<=> ( r2_hidden(B,C)
& v1_filter_0(C,A) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,plain,
? [A] :
( ? [B] :
( ? [C] :
( r2_hidden(B,C)
& ~ r2_hidden(C,k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),B))
& v1_filter_0(C,A)
& m1_filter_0(C,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(f90,plain,
( r2_hidden(sK1_skl,sK2_skl)
& ~ r2_hidden(sK2_skl,k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),sK1_skl))
& v1_filter_0(sK2_skl,sK0_skl)
& m1_filter_0(sK2_skl,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,sK2_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl)],[f89]) ).
fof(f91,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f92,plain,
v10_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f93,plain,
v17_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f94,plain,
~ v3_realset2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f95,plain,
l3_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f96,plain,
m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f97,plain,
m1_filter_0(sK2_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f98,plain,
v1_filter_0(sK2_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f99,plain,
~ r2_hidden(sK2_skl,k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),sK1_skl)),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f100,plain,
r2_hidden(sK1_skl,sK2_skl),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f215,plain,
! [A,B,C] :
( ( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f35]) ).
fof(f216,plain,
( ! [A,B,C] :
( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ! [A,B,C] :
( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(miniscoping,[status(thm)],[f215]) ).
fof(f217,plain,
! [X0,X1,X2] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f291,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)],[f58]) ).
fof(f292,plain,
! [C] :
( ~ v1_xboole_0(C)
| ! [B] :
( ~ m1_subset_1(B,k1_zfmisc_1(C))
| ! [A] : ~ r2_hidden(A,B) ) ),
inference(miniscoping,[status(thm)],[f291]) ).
fof(f293,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)],[f292]) ).
fof(f321,plain,
! [A,B,C,D] :
( k8_funct_2(A,B,C,D) = k1_funct_1(C,D)
| ~ m1_subset_1(D,A)
| ~ m1_relset_1(C,A,B)
| ~ v1_funct_2(C,A,B)
| ~ v1_funct_1(C)
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f67]) ).
fof(f322,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X2,X1,X3) = k1_funct_1(X1,X3)
| ~ m1_subset_1(X3,X0)
| ~ m1_relset_1(X1,X0,X2)
| ~ v1_funct_2(X1,X0,X2)
| ~ v1_funct_1(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f321]) ).
fof(f323,plain,
! [A] :
( k9_lopclset(A) = k8_lopclset(A)
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f324,plain,
! [X0] :
( k9_lopclset(X0) = k8_lopclset(X0)
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f332,plain,
! [A] :
( ( m2_relset_1(k9_lopclset(A),u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)))
& v1_funct_2(k9_lopclset(A),u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)))
& v1_funct_1(k9_lopclset(A)) )
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f74]) ).
fof(f333,plain,
! [X0] :
( v1_funct_1(k9_lopclset(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f332]) ).
fof(f334,plain,
! [X0] :
( v1_funct_2(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f332]) ).
fof(f335,plain,
! [X0] :
( m2_relset_1(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f332]) ).
fof(f339,plain,
! [A] :
( ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(B) )
| ~ m1_filter_0(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f76]) ).
fof(f341,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f339]) ).
fof(f378,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( r2_hidden(C,k1_funct_1(k8_lopclset(A),B))
<=> ( r2_hidden(B,C)
& v1_filter_0(C,A) ) )
| ~ m1_filter_0(C,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)],[f88]) ).
fof(f379,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ r2_hidden(B,C)
| ~ v1_filter_0(C,A)
| r2_hidden(C,k1_funct_1(k8_lopclset(A),B)) )
& ( ( r2_hidden(B,C)
& v1_filter_0(C,A) )
| ~ r2_hidden(C,k1_funct_1(k8_lopclset(A),B)) ) )
| ~ m1_filter_0(C,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(NNF_transformation,[status(thm)],[f378]) ).
fof(f382,plain,
! [X0,X1,X2] :
( ~ r2_hidden(X1,X2)
| ~ v1_filter_0(X2,X0)
| r2_hidden(X2,k1_funct_1(k8_lopclset(X0),X1))
| ~ m1_filter_0(X2,X0)
| ~ 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)],[f379]) ).
fof(f411,definition,
( sQ5_spl
<=> v1_xboole_0(u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f412,plain,
( ~ sQ5_spl
| v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f411]) ).
fof(f418,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| ~ m1_subset_1(sK2_skl,k1_zfmisc_1(X0)) ),
inference(resolution,[status(thm)],[f293,f100]) ).
fof(f420,definition,
( sQ7_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f421,plain,
( ~ sQ7_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f420]) ).
fof(f423,definition,
( sQ8_spl
<=> v10_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f425,plain,
( sQ8_spl
| ~ v10_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f423]) ).
fof(f426,definition,
( sQ9_spl
<=> v17_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f428,plain,
( sQ9_spl
| ~ v17_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f426]) ).
fof(f429,definition,
( sQ10_spl
<=> v3_realset2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f430,plain,
( ~ sQ10_spl
| v3_realset2(sK0_skl) ),
inference(component_clause,[status(thm)],[f429]) ).
fof(f432,definition,
( sQ11_spl
<=> l3_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f434,plain,
( sQ11_spl
| ~ l3_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f432]) ).
fof(f438,definition,
( sQ13_spl
<=> m1_filter_0(sK2_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f440,plain,
( sQ13_spl
| ~ m1_filter_0(sK2_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f438]) ).
fof(f442,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f440,f97]) ).
fof(f443,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f442]) ).
fof(f469,plain,
( k9_lopclset(sK0_skl) = k8_lopclset(sK0_skl)
| v3_realset2(sK0_skl)
| ~ v17_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f324,f95]) ).
fof(f470,definition,
( sQ18_spl
<=> k9_lopclset(sK0_skl) = k8_lopclset(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f471,plain,
( ~ sQ18_spl
| k9_lopclset(sK0_skl) = k8_lopclset(sK0_skl) ),
inference(component_clause,[status(thm)],[f470]) ).
fof(f473,plain,
( sQ18_spl
| sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f469,f420,f423,f426,f429,f470]) ).
fof(f474,plain,
( ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f430,f94]) ).
fof(f475,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f474]) ).
fof(f476,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f428,f93]) ).
fof(f477,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f476]) ).
fof(f478,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f425,f92]) ).
fof(f479,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f478]) ).
fof(f480,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f421,f91]) ).
fof(f481,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f480]) ).
fof(f482,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f434,f95]) ).
fof(f483,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f482]) ).
fof(f532,plain,
( v1_funct_1(k9_lopclset(sK0_skl))
| v3_realset2(sK0_skl)
| ~ v17_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f333,f95]) ).
fof(f537,definition,
( sQ28_spl
<=> v1_funct_1(k9_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f540,plain,
( sQ28_spl
| sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f532,f420,f423,f426,f429,f537]) ).
fof(f542,plain,
( v1_funct_2(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)))
| v3_realset2(sK0_skl)
| ~ v17_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f334,f95]) ).
fof(f547,definition,
( sQ30_spl
<=> v1_funct_2(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f548,plain,
( ~ sQ30_spl
| v1_funct_2(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl))) ),
inference(component_clause,[status(thm)],[f547]) ).
fof(f550,plain,
( sQ30_spl
| sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f542,f420,f423,f426,f429,f547]) ).
fof(f552,plain,
( m2_relset_1(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)))
| v3_realset2(sK0_skl)
| ~ v17_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f335,f95]) ).
fof(f557,definition,
( sQ32_spl
<=> m2_relset_1(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f558,plain,
( ~ sQ32_spl
| m2_relset_1(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl))) ),
inference(component_clause,[status(thm)],[f557]) ).
fof(f560,plain,
( sQ32_spl
| sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f552,f420,f423,f426,f429,f557]) ).
fof(f727,plain,
( m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f341,f97]) ).
fof(f728,definition,
( sQ59_spl
<=> m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f729,plain,
( ~ sQ59_spl
| m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
inference(component_clause,[status(thm)],[f728]) ).
fof(f731,plain,
( sQ59_spl
| ~ sQ11_spl
| ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f727,f420,f423,f432,f728]) ).
fof(f867,plain,
! [X0] :
( ~ sQ30_spl
| k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),X0) = k1_funct_1(k9_lopclset(sK0_skl),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| ~ m1_relset_1(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)))
| ~ v1_funct_1(k9_lopclset(sK0_skl))
| v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f548,f322]) ).
fof(f868,definition,
( sQ83_spl
<=> m1_relset_1(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f870,plain,
( sQ83_spl
| ~ m1_relset_1(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl))) ),
inference(component_clause,[status(thm)],[f868]) ).
fof(f875,definition,
! [X0] :
( sQ85_spl
<=> ( k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),X0) = k1_funct_1(k9_lopclset(sK0_skl),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f876,plain,
! [X0] :
( ~ sQ85_spl
| k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),X0) = k1_funct_1(k9_lopclset(sK0_skl),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f875]) ).
fof(f878,plain,
( ~ sQ30_spl
| sQ85_spl
| ~ sQ83_spl
| ~ sQ28_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f867,f411,f537,f868,f875,f547]) ).
fof(f934,plain,
( ~ sQ59_spl
| ~ v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f729,f418]) ).
fof(f967,plain,
( ~ sQ59_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f934,f412]) ).
fof(f968,plain,
( ~ sQ59_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f967]) ).
fof(f1219,plain,
( ~ sQ32_spl
| m1_relset_1(k9_lopclset(sK0_skl),u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl))) ),
inference(resolution,[status(thm)],[f217,f558]) ).
fof(f1222,plain,
( ~ sQ32_spl
| sQ83_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1219,f870]) ).
fof(f1223,plain,
( ~ sQ32_spl
| sQ83_spl ),
inference(contradiction_clause,[status(thm)],[f1222]) ).
fof(f1343,plain,
( ~ sQ85_spl
| k8_funct_2(u1_struct_0(sK0_skl),k1_zfmisc_1(k7_lopclset(sK0_skl)),k9_lopclset(sK0_skl),sK1_skl) = k1_funct_1(k9_lopclset(sK0_skl),sK1_skl) ),
inference(resolution,[status(thm)],[f876,f96]) ).
fof(f1344,plain,
( ~ sQ85_spl
| ~ r2_hidden(sK2_skl,k1_funct_1(k9_lopclset(sK0_skl),sK1_skl)) ),
inference(backward_demodulation,[status(thm)],[f1343,f99]) ).
fof(f2502,plain,
! [X0] :
( ~ r2_hidden(sK1_skl,X0)
| ~ v1_filter_0(X0,sK0_skl)
| r2_hidden(X0,k1_funct_1(k8_lopclset(sK0_skl),sK1_skl))
| ~ m1_filter_0(X0,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)],[f382,f96]) ).
fof(f2503,definition,
! [X0] :
( sQ274_spl
<=> ( ~ r2_hidden(sK1_skl,X0)
| ~ v1_filter_0(X0,sK0_skl)
| r2_hidden(X0,k1_funct_1(k8_lopclset(sK0_skl),sK1_skl))
| ~ m1_filter_0(X0,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition]) ).
fof(f2504,plain,
! [X0] :
( ~ sQ274_spl
| ~ r2_hidden(sK1_skl,X0)
| ~ v1_filter_0(X0,sK0_skl)
| r2_hidden(X0,k1_funct_1(k8_lopclset(sK0_skl),sK1_skl))
| ~ m1_filter_0(X0,sK0_skl) ),
inference(component_clause,[status(thm)],[f2503]) ).
fof(f2506,plain,
( sQ274_spl
| ~ sQ11_spl
| sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f2502,f420,f423,f426,f429,f432,f2503]) ).
fof(f2507,plain,
! [X0] :
( ~ sQ274_spl
| ~ sQ18_spl
| ~ r2_hidden(sK1_skl,X0)
| ~ v1_filter_0(X0,sK0_skl)
| r2_hidden(X0,k1_funct_1(k9_lopclset(sK0_skl),sK1_skl))
| ~ m1_filter_0(X0,sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f471,f2504]) ).
fof(f2544,plain,
( ~ sQ274_spl
| ~ sQ18_spl
| ~ v1_filter_0(sK2_skl,sK0_skl)
| r2_hidden(sK2_skl,k1_funct_1(k9_lopclset(sK0_skl),sK1_skl))
| ~ m1_filter_0(sK2_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f2507,f100]) ).
fof(f2555,definition,
( sQ283_spl
<=> r2_hidden(sK2_skl,k1_funct_1(k9_lopclset(sK0_skl),sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition]) ).
fof(f2556,plain,
( ~ sQ283_spl
| r2_hidden(sK2_skl,k1_funct_1(k9_lopclset(sK0_skl),sK1_skl)) ),
inference(component_clause,[status(thm)],[f2555]) ).
fof(f2558,definition,
( sQ284_spl
<=> v1_filter_0(sK2_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition]) ).
fof(f2560,plain,
( sQ284_spl
| ~ v1_filter_0(sK2_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f2558]) ).
fof(f2561,plain,
( ~ sQ274_spl
| ~ sQ18_spl
| ~ sQ284_spl
| sQ283_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f2544,f438,f2555,f2558,f470,f2503]) ).
fof(f2570,plain,
( ~ sQ283_spl
| ~ sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2556,f1344]) ).
fof(f2571,plain,
( ~ sQ283_spl
| ~ sQ85_spl ),
inference(contradiction_clause,[status(thm)],[f2570]) ).
fof(f2572,plain,
( sQ284_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2560,f98]) ).
fof(f2573,plain,
sQ284_spl,
inference(contradiction_clause,[status(thm)],[f2572]) ).
fof(f2574,plain,
$false,
inference(sat_refutation,[status(thm)],[f443,f473,f475,f477,f479,f481,f483,f540,f550,f560,f731,f878,f968,f1223,f2506,f2561,f2571,f2573]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT289+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n001.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 23:32:13 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.50 % Refutation found
% 0.13/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.48/0.53 % Elapsed time: 0.167478 seconds
% 0.48/0.53 % CPU time: 1.024123 seconds
% 0.48/0.53 % Total memory used: 107.601 MB
% 0.48/0.53 % Net memory used: 106.648 MB
%------------------------------------------------------------------------------