%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT302+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 : n008.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 22.80s 3.43s
% Output : CNFRefutation 22.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 15
% Syntax : Number of formulae : 106 ( 23 unt; 0 def)
% Number of atoms : 359 ( 17 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 399 ( 146 ~; 168 |; 60 &)
% ( 6 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 1 con; 0-2 aty)
% Number of variables : 75 ( 74 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v13_lattices(A)
=> m2_filter_2(k6_domain_1(u1_struct_0(A),k5_lattices(A)),A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v13_lattices(A)
=> m2_filter_2(k6_domain_1(u1_struct_0(A),k5_lattices(A)),A) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f15,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A] :
( ( l1_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k5_lattices(A),u1_struct_0(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A] :
( ( l2_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k6_lattices(A),u1_struct_0(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [A] :
( l1_lattices(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( ( l3_lattices(A)
& v14_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_filter_0(k6_domain_1(u1_struct_0(A),k6_lattices(A)),A) ) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f91,axiom,
! [A] :
( ( l3_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k5_lattices(A) = k6_lattices(k1_lattice2(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,plain,
? [A] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(A),k5_lattices(A)),A)
& v13_lattices(A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f95,plain,
( ~ m2_filter_2(k6_domain_1(u1_struct_0(sK0_skl),k5_lattices(sK0_skl)),sK0_skl)
& v13_lattices(sK0_skl)
& l3_lattices(sK0_skl)
& v10_lattices(sK0_skl)
& ~ v3_struct_0(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f94]) ).
fof(f96,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f97,plain,
v10_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f98,plain,
l3_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f99,plain,
v13_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f100,plain,
~ m2_filter_2(k6_domain_1(u1_struct_0(sK0_skl),k5_lattices(sK0_skl)),sK0_skl),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f139,plain,
! [A] :
( ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f141,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f142,plain,
! [A] :
( m1_subset_1(k5_lattices(A),u1_struct_0(A))
| ~ l1_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f143,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| ~ l1_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f146,plain,
! [A] :
( m1_subset_1(k6_lattices(A),u1_struct_0(A))
| ~ l2_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f147,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| ~ l2_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f148,plain,
! [A] :
( l1_struct_0(A)
| ~ l1_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f149,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f152,plain,
! [A] :
( ( l2_lattices(A)
& l1_lattices(A) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f153,plain,
! [X0] :
( l1_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f154,plain,
! [X0] :
( l2_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f152]) ).
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(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(f334,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(f341,plain,
! [A] :
( m1_filter_0(k6_domain_1(u1_struct_0(A),k6_lattices(A)),A)
| ~ l3_lattices(A)
| ~ v14_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f342,plain,
! [X0] :
( m1_filter_0(k6_domain_1(u1_struct_0(X0),k6_lattices(X0)),X0)
| ~ l3_lattices(X0)
| ~ v14_lattices(X0)
| ~ v10_lattices(X0)
| v3_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(f349,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(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(f364,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(f368,plain,
! [A] :
( k5_lattices(A) = k6_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v13_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f91]) ).
fof(f369,plain,
! [X0] :
( k5_lattices(X0) = k6_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v13_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f368]) ).
fof(f376,plain,
! [X0] :
( m1_filter_0(k6_domain_1(u1_struct_0(X0),k6_lattices(X0)),X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f342]) ).
fof(f379,plain,
! [X0] :
( ~ l1_lattices(X0)
| v3_struct_0(X0)
| k6_domain_1(u1_struct_0(X0),k5_lattices(X0)) = k1_tarski(k5_lattices(X0))
| v1_xboole_0(u1_struct_0(X0)) ),
inference(resolution,[status(thm)],[f329,f143]) ).
fof(f380,plain,
! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK0_skl))
| m2_filter_2(X0,sK0_skl)
| ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f349,f97]) ).
fof(f381,plain,
! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK0_skl))
| m2_filter_2(X0,sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f380,f96]) ).
fof(f382,plain,
( k5_lattices(sK0_skl) = k6_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v13_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f369,f97]) ).
fof(f383,plain,
( k5_lattices(sK0_skl) = k6_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v13_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f382,f96]) ).
fof(f439,plain,
( v10_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f252,f97]) ).
fof(f440,plain,
( v10_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f439,f96]) ).
fof(f457,plain,
v10_lattices(k1_lattice2(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f440,f98]) ).
fof(f475,plain,
! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK0_skl))
| m2_filter_2(X0,sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f381,f98]) ).
fof(f478,plain,
! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| m2_filter_2(X0,sK0_skl) ),
inference(resolution,[status(thm)],[f475,f334]) ).
fof(f480,plain,
! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| m2_filter_2(X0,sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f478,f457]) ).
fof(f488,plain,
( k5_lattices(sK0_skl) = k6_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f383,f99]) ).
fof(f489,plain,
k5_lattices(sK0_skl) = k6_lattices(k1_lattice2(sK0_skl)),
inference(resolution,[status(thm)],[f488,f98]) ).
fof(f545,plain,
( m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl)),k1_lattice2(sK0_skl))
| ~ v14_lattices(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)],[f489,f376]) ).
fof(f546,plain,
( m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl)),k1_lattice2(sK0_skl))
| ~ v14_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f545,f457]) ).
fof(f593,plain,
l3_lattices(k1_lattice2(sK0_skl)),
inference(resolution,[status(thm)],[f141,f98]) ).
fof(f687,plain,
( m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl)),k1_lattice2(sK0_skl))
| ~ v14_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(backward_subsumption_resolution,[status(thm)],[f546,f593]) ).
fof(f696,plain,
! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| m2_filter_2(X0,sK0_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f480,f593]) ).
fof(f726,plain,
l1_lattices(k1_lattice2(sK0_skl)),
inference(resolution,[status(thm)],[f153,f593]) ).
fof(f729,plain,
l1_lattices(sK0_skl),
inference(resolution,[status(thm)],[f153,f98]) ).
fof(f737,plain,
( ~ v13_lattices(sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl)),k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f687,f364]) ).
fof(f738,plain,
( ~ v13_lattices(sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl)),k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f737,f96]) ).
fof(f786,plain,
( ~ v13_lattices(sK0_skl)
| ~ l3_lattices(sK0_skl)
| m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl)),k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f738,f97]) ).
fof(f787,plain,
( ~ v13_lattices(sK0_skl)
| m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl)),k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f786,f98]) ).
fof(f789,plain,
( m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl)),k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f787,f99]) ).
fof(f930,plain,
l1_struct_0(sK0_skl),
inference(resolution,[status(thm)],[f729,f149]) ).
fof(f932,plain,
( v3_struct_0(sK0_skl)
| k6_domain_1(u1_struct_0(sK0_skl),k5_lattices(sK0_skl)) = k1_tarski(k5_lattices(sK0_skl))
| v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f729,f379]) ).
fof(f934,plain,
( k6_domain_1(u1_struct_0(sK0_skl),k5_lattices(sK0_skl)) = k1_tarski(k5_lattices(sK0_skl))
| v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f932,f96]) ).
fof(f937,plain,
l1_struct_0(k1_lattice2(sK0_skl)),
inference(resolution,[status(thm)],[f726,f149]) ).
fof(f958,plain,
l2_lattices(k1_lattice2(sK0_skl)),
inference(resolution,[status(thm)],[f154,f593]) ).
fof(f1177,plain,
( m1_subset_1(k6_lattices(k1_lattice2(sK0_skl)),u1_struct_0(k1_lattice2(sK0_skl)))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f958,f147]) ).
fof(f1179,plain,
( m1_subset_1(k5_lattices(sK0_skl),u1_struct_0(k1_lattice2(sK0_skl)))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f489,f1177]) ).
fof(f1231,plain,
( k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl)) = k1_tarski(k5_lattices(sK0_skl))
| v1_xboole_0(u1_struct_0(k1_lattice2(sK0_skl)))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f1179,f329]) ).
fof(f1698,plain,
( ~ v3_struct_0(k1_lattice2(sK0_skl))
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f203,f98]) ).
fof(f1702,plain,
~ v3_struct_0(k1_lattice2(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f1698,f96]) ).
fof(f2327,plain,
( k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl)) = k1_tarski(k5_lattices(sK0_skl))
| v1_xboole_0(u1_struct_0(k1_lattice2(sK0_skl))) ),
inference(backward_subsumption_resolution,[status(thm)],[f1231,f1702]) ).
fof(f2433,plain,
m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl)),k1_lattice2(sK0_skl)),
inference(backward_subsumption_resolution,[status(thm)],[f789,f1702]) ).
fof(f2439,plain,
! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK0_skl))
| m2_filter_2(X0,sK0_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f696,f1702]) ).
fof(f2554,plain,
( ~ v1_xboole_0(u1_struct_0(k1_lattice2(sK0_skl)))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f206,f937]) ).
fof(f2556,plain,
( ~ v1_xboole_0(u1_struct_0(sK0_skl))
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f206,f930]) ).
fof(f2560,plain,
~ v1_xboole_0(u1_struct_0(k1_lattice2(sK0_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f2554,f1702]) ).
fof(f2562,plain,
~ v1_xboole_0(u1_struct_0(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f2556,f96]) ).
fof(f3211,plain,
k6_domain_1(u1_struct_0(sK0_skl),k5_lattices(sK0_skl)) = k1_tarski(k5_lattices(sK0_skl)),
inference(backward_subsumption_resolution,[status(thm)],[f934,f2562]) ).
fof(f3256,plain,
~ m2_filter_2(k1_tarski(k5_lattices(sK0_skl)),sK0_skl),
inference(backward_demodulation,[status(thm)],[f3211,f100]) ).
fof(f5044,plain,
k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl)) = k1_tarski(k5_lattices(sK0_skl)),
inference(backward_subsumption_resolution,[status(thm)],[f2327,f2560]) ).
fof(f5114,plain,
m1_filter_0(k1_tarski(k5_lattices(sK0_skl)),k1_lattice2(sK0_skl)),
inference(backward_demodulation,[status(thm)],[f5044,f2433]) ).
fof(f5116,plain,
m2_filter_2(k1_tarski(k5_lattices(sK0_skl)),sK0_skl),
inference(resolution,[status(thm)],[f5114,f2439]) ).
fof(f5118,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f5116,f3256]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT302+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.36 % Computer : n008.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 23:31:54 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 22.80/3.43 % Refutation found
% 22.80/3.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 22.80/3.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 22.80/3.51 % Elapsed time: 3.127975 seconds
% 22.80/3.51 % CPU time: 24.199627 seconds
% 22.80/3.51 % Total memory used: 309.582 MB
% 22.80/3.51 % Net memory used: 295.294 MB
%------------------------------------------------------------------------------