%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT304+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:02:38 PM UTC 2026
% Result : Theorem 280.16s 36.29s
% Output : CNFRefutation 282.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 45
% Syntax : Number of formulae : 177 ( 36 unt; 23 def)
% Number of atoms : 642 ( 40 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 640 ( 175 ~; 175 |; 251 &)
% ( 29 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 48 ( 46 usr; 24 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 13 con; 0-2 aty)
% Number of variables : 81 ( 67 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [A,B] :
( B = k1_tarski(A)
<=> ! [C] :
( r2_hidden(C,B)
<=> C = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f326,axiom,
k1_zfmisc_1(k1_xboole_0) = k1_tarski(k1_xboole_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2311,axiom,
? [A] :
( v3_lattices(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2317,axiom,
? [A] :
( v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2322,axiom,
? [A] :
( v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2323,axiom,
? [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_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2326,axiom,
? [A] :
( v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2327,axiom,
? [A] :
( v16_lattices(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2330,axiom,
? [A] :
( v17_lattices(A)
& v16_lattices(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_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_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2411,axiom,
? [A] : l3_lattices(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2436,axiom,
? [A] :
( v3_filter_0(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2455,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_filter_0(u1_struct_0(A),A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2456,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k1_filter_0(A) = u1_struct_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2564,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(f2569,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(f2570,axiom,
? [A] :
( v1_lattice2(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/sandbox/benchmark/theBenchmark.p') ).
fof(f2573,axiom,
? [A] :
( v1_lattice2(A)
& v3_filter_0(A)
& v13_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2597,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( u1_lattices(A) = u2_lattices(k1_lattice2(A))
& u2_lattices(A) = u1_lattices(k1_lattice2(A))
& u1_struct_0(A) = u1_struct_0(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2669,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2872,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(f2941,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(f2952,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m2_filter_2(u1_struct_0(A),A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2953,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m2_filter_2(u1_struct_0(A),A) ),
inference(negated_conjecture,[status(cth)],[f2952]) ).
fof(f2961,plain,
! [A,B] :
( ( ? [C] :
( ( C = A
| r2_hidden(C,B) )
& ( C != A
| ~ r2_hidden(C,B) ) )
| B = k1_tarski(A) )
& ( ! [C] :
( ( C != A
| r2_hidden(C,B) )
& ( C = A
| ~ r2_hidden(C,B) ) )
| B != k1_tarski(A) ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f2962,plain,
( ! [A,B] :
( ? [C] :
( ( C = A
| r2_hidden(C,B) )
& ( C != A
| ~ r2_hidden(C,B) ) )
| B = k1_tarski(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| r2_hidden(C,B) )
& ! [C] :
( C = A
| ~ r2_hidden(C,B) ) )
| B != k1_tarski(A) ) ),
inference(miniscoping,[status(thm)],[f2961]) ).
fof(f2963,plain,
( ! [A,B] :
( ( ( sK1_skl(B,A) = A
| r2_hidden(sK1_skl(B,A),B) )
& ( sK1_skl(B,A) != A
| ~ r2_hidden(sK1_skl(B,A),B) ) )
| B = k1_tarski(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| r2_hidden(C,B) )
& ! [C] :
( C = A
| ~ r2_hidden(C,B) ) )
| B != k1_tarski(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(C,sK1_skl(B,A))],[f2962]) ).
fof(f2965,plain,
! [X0,X1,X2] :
( X2 != X1
| r2_hidden(X2,X0)
| X0 != k1_tarski(X1) ),
inference(cnf_transformation,[status(thm)],[f2963]) ).
fof(f3566,plain,
k1_zfmisc_1(k1_xboole_0) = k1_tarski(k1_xboole_0),
inference(cnf_transformation,[status(thm)],[f326]) ).
fof(f9540,plain,
( v3_lattices(sK732_skl)
& l3_lattices(sK732_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK732_skl]),skolemize(A,sK732_skl)],[f2311]) ).
fof(f9541,plain,
l3_lattices(sK732_skl),
inference(cnf_transformation,[status(thm)],[f9540]) ).
fof(f9560,plain,
( v3_lattices(sK735_skl)
& ~ v3_struct_0(sK735_skl)
& l3_lattices(sK735_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK735_skl]),skolemize(A,sK735_skl)],[f2317]) ).
fof(f9561,plain,
l3_lattices(sK735_skl),
inference(cnf_transformation,[status(thm)],[f9560]) ).
fof(f9587,plain,
( v10_lattices(sK738_skl)
& v9_lattices(sK738_skl)
& v8_lattices(sK738_skl)
& v7_lattices(sK738_skl)
& v6_lattices(sK738_skl)
& v5_lattices(sK738_skl)
& v4_lattices(sK738_skl)
& v3_lattices(sK738_skl)
& ~ v3_struct_0(sK738_skl)
& l3_lattices(sK738_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK738_skl]),skolemize(A,sK738_skl)],[f2322]) ).
fof(f9597,plain,
v10_lattices(sK738_skl),
inference(cnf_transformation,[status(thm)],[f9587]) ).
fof(f9598,plain,
( v14_lattices(sK739_skl)
& v13_lattices(sK739_skl)
& v12_lattices(sK739_skl)
& v11_lattices(sK739_skl)
& v10_lattices(sK739_skl)
& v9_lattices(sK739_skl)
& v8_lattices(sK739_skl)
& v7_lattices(sK739_skl)
& v6_lattices(sK739_skl)
& v5_lattices(sK739_skl)
& v4_lattices(sK739_skl)
& v3_lattices(sK739_skl)
& ~ v3_struct_0(sK739_skl)
& l3_lattices(sK739_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK739_skl]),skolemize(A,sK739_skl)],[f2323]) ).
fof(f9608,plain,
v10_lattices(sK739_skl),
inference(cnf_transformation,[status(thm)],[f9598]) ).
fof(f9620,plain,
( v15_lattices(sK740_skl)
& v14_lattices(sK740_skl)
& v13_lattices(sK740_skl)
& v10_lattices(sK740_skl)
& v9_lattices(sK740_skl)
& v8_lattices(sK740_skl)
& v7_lattices(sK740_skl)
& v6_lattices(sK740_skl)
& v5_lattices(sK740_skl)
& v4_lattices(sK740_skl)
& v3_lattices(sK740_skl)
& ~ v3_struct_0(sK740_skl)
& l3_lattices(sK740_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK740_skl]),skolemize(A,sK740_skl)],[f2326]) ).
fof(f9630,plain,
v10_lattices(sK740_skl),
inference(cnf_transformation,[status(thm)],[f9620]) ).
fof(f9634,plain,
( v16_lattices(sK741_skl)
& v15_lattices(sK741_skl)
& v14_lattices(sK741_skl)
& v13_lattices(sK741_skl)
& v10_lattices(sK741_skl)
& v9_lattices(sK741_skl)
& v8_lattices(sK741_skl)
& v7_lattices(sK741_skl)
& v6_lattices(sK741_skl)
& v5_lattices(sK741_skl)
& v4_lattices(sK741_skl)
& v3_lattices(sK741_skl)
& ~ v3_struct_0(sK741_skl)
& l3_lattices(sK741_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK741_skl]),skolemize(A,sK741_skl)],[f2327]) ).
fof(f9644,plain,
v10_lattices(sK741_skl),
inference(cnf_transformation,[status(thm)],[f9634]) ).
fof(f9659,plain,
( v17_lattices(sK742_skl)
& v16_lattices(sK742_skl)
& v15_lattices(sK742_skl)
& v14_lattices(sK742_skl)
& v13_lattices(sK742_skl)
& v11_lattices(sK742_skl)
& v10_lattices(sK742_skl)
& v9_lattices(sK742_skl)
& v8_lattices(sK742_skl)
& v7_lattices(sK742_skl)
& v6_lattices(sK742_skl)
& v5_lattices(sK742_skl)
& v4_lattices(sK742_skl)
& v3_lattices(sK742_skl)
& ~ v3_struct_0(sK742_skl)
& l3_lattices(sK742_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK742_skl]),skolemize(A,sK742_skl)],[f2330]) ).
fof(f9669,plain,
v10_lattices(sK742_skl),
inference(cnf_transformation,[status(thm)],[f9659]) ).
fof(f9903,plain,
l3_lattices(sK782_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK782_skl]),skolemize(A,sK782_skl)],[f2411]) ).
fof(f9904,plain,
l3_lattices(sK782_skl),
inference(cnf_transformation,[status(thm)],[f9903]) ).
fof(f9967,plain,
( v3_filter_0(sK783_skl)
& v10_lattices(sK783_skl)
& v9_lattices(sK783_skl)
& v8_lattices(sK783_skl)
& v7_lattices(sK783_skl)
& v6_lattices(sK783_skl)
& v5_lattices(sK783_skl)
& v4_lattices(sK783_skl)
& v3_lattices(sK783_skl)
& ~ v3_struct_0(sK783_skl)
& l3_lattices(sK783_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK783_skl]),skolemize(A,sK783_skl)],[f2436]) ).
fof(f9977,plain,
v10_lattices(sK783_skl),
inference(cnf_transformation,[status(thm)],[f9967]) ).
fof(f10064,plain,
! [A] :
( m1_filter_0(u1_struct_0(A),A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2455]) ).
fof(f10065,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f10064]) ).
fof(f10066,plain,
! [A] :
( k1_filter_0(A) = u1_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2456]) ).
fof(f10067,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f10066]) ).
fof(f10408,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)],[f2564]) ).
fof(f10409,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f10408]) ).
fof(f10435,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)],[f2569]) ).
fof(f10444,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f10435]) ).
fof(f10445,plain,
( v1_lattice2(sK817_skl)
& v10_lattices(sK817_skl)
& v9_lattices(sK817_skl)
& v8_lattices(sK817_skl)
& v7_lattices(sK817_skl)
& v6_lattices(sK817_skl)
& v5_lattices(sK817_skl)
& v4_lattices(sK817_skl)
& ~ v3_struct_0(sK817_skl)
& l3_lattices(sK817_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK817_skl]),skolemize(A,sK817_skl)],[f2570]) ).
fof(f10454,plain,
v10_lattices(sK817_skl),
inference(cnf_transformation,[status(thm)],[f10445]) ).
fof(f10477,plain,
( v1_lattice2(sK818_skl)
& v3_filter_0(sK818_skl)
& v13_lattices(sK818_skl)
& v10_lattices(sK818_skl)
& v9_lattices(sK818_skl)
& v8_lattices(sK818_skl)
& v7_lattices(sK818_skl)
& v6_lattices(sK818_skl)
& v5_lattices(sK818_skl)
& v4_lattices(sK818_skl)
& v3_lattices(sK818_skl)
& ~ v3_struct_0(sK818_skl)
& l3_lattices(sK818_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK818_skl]),skolemize(A,sK818_skl)],[f2573]) ).
fof(f10487,plain,
v10_lattices(sK818_skl),
inference(cnf_transformation,[status(thm)],[f10477]) ).
fof(f10591,plain,
! [A] :
( ( u1_lattices(A) = u2_lattices(k1_lattice2(A))
& u2_lattices(A) = u1_lattices(k1_lattice2(A))
& u1_struct_0(A) = u1_struct_0(k1_lattice2(A)) )
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2597]) ).
fof(f10592,plain,
! [X0] :
( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f10591]) ).
fof(f10800,plain,
! [A] :
( ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2669]) ).
fof(f10802,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f10800]) ).
fof(f11272,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)],[f2872]) ).
fof(f11273,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)],[f11272]) ).
fof(f11274,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)],[f11273]) ).
fof(f11276,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)],[f11274]) ).
fof(f11468,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)],[f2941]) ).
fof(f11469,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)],[f11468]) ).
fof(f11470,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)],[f11469]) ).
fof(f11472,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)],[f11470]) ).
fof(f11511,plain,
? [A] :
( ~ m2_filter_2(u1_struct_0(A),A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2953]) ).
fof(f11512,plain,
( ~ m2_filter_2(u1_struct_0(sK899_skl),sK899_skl)
& l3_lattices(sK899_skl)
& v10_lattices(sK899_skl)
& ~ v3_struct_0(sK899_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK899_skl]),skolemize(A,sK899_skl)],[f11511]) ).
fof(f11513,plain,
~ v3_struct_0(sK899_skl),
inference(cnf_transformation,[status(thm)],[f11512]) ).
fof(f11514,plain,
v10_lattices(sK899_skl),
inference(cnf_transformation,[status(thm)],[f11512]) ).
fof(f11515,plain,
l3_lattices(sK899_skl),
inference(cnf_transformation,[status(thm)],[f11512]) ).
fof(f11516,plain,
~ m2_filter_2(u1_struct_0(sK899_skl),sK899_skl),
inference(cnf_transformation,[status(thm)],[f11512]) ).
fof(f13769,plain,
! [X0] : r2_hidden(X0,k1_tarski(X0)),
inference(destructive_equality_resolution,[status(thm)],[f2965]) ).
fof(f14837,definition,
( sQ410_spl
<=> l3_lattices(sK899_skl) ),
introduced(definition,[new_symbols(definition,[sQ410_spl])],[split_symbol_definition]) ).
fof(f14839,plain,
( sQ410_spl
| ~ l3_lattices(sK899_skl) ),
inference(component_clause,[status(thm)],[f14837]) ).
fof(f14840,definition,
( sQ411_spl
<=> v3_struct_0(sK899_skl) ),
introduced(definition,[new_symbols(definition,[sQ411_spl])],[split_symbol_definition]) ).
fof(f14841,plain,
( ~ sQ411_spl
| v3_struct_0(sK899_skl) ),
inference(component_clause,[status(thm)],[f14840]) ).
fof(f14847,plain,
( ~ sQ411_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14841,f11513]) ).
fof(f14848,plain,
~ sQ411_spl,
inference(contradiction_clause,[status(thm)],[f14847]) ).
fof(f14849,plain,
( sQ410_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14839,f11515]) ).
fof(f14850,plain,
sQ410_spl,
inference(contradiction_clause,[status(thm)],[f14849]) ).
fof(f15164,plain,
( u1_struct_0(sK899_skl) = u1_struct_0(k1_lattice2(sK899_skl))
| v3_struct_0(sK899_skl) ),
inference(resolution,[status(thm)],[f10592,f11515]) ).
fof(f15218,definition,
( sQ472_spl
<=> u1_struct_0(sK899_skl) = u1_struct_0(k1_lattice2(sK899_skl)) ),
introduced(definition,[new_symbols(definition,[sQ472_spl])],[split_symbol_definition]) ).
fof(f15219,plain,
( ~ sQ472_spl
| u1_struct_0(sK899_skl) = u1_struct_0(k1_lattice2(sK899_skl)) ),
inference(component_clause,[status(thm)],[f15218]) ).
fof(f15221,plain,
( sQ472_spl
| sQ411_spl ),
inference(split_clause,[status(thm)],[f15164,f14840,f15218]) ).
fof(f15261,definition,
( sQ474_spl
<=> v3_struct_0(k1_lattice2(sK899_skl)) ),
introduced(definition,[new_symbols(definition,[sQ474_spl])],[split_symbol_definition]) ).
fof(f15262,plain,
( ~ sQ474_spl
| v3_struct_0(k1_lattice2(sK899_skl)) ),
inference(component_clause,[status(thm)],[f15261]) ).
fof(f15264,definition,
( sQ475_spl
<=> v10_lattices(k1_lattice2(sK899_skl)) ),
introduced(definition,[new_symbols(definition,[sQ475_spl])],[split_symbol_definition]) ).
fof(f15265,plain,
( ~ sQ475_spl
| v10_lattices(k1_lattice2(sK899_skl)) ),
inference(component_clause,[status(thm)],[f15264]) ).
fof(f15266,plain,
( sQ475_spl
| ~ v10_lattices(k1_lattice2(sK899_skl)) ),
inference(component_clause,[status(thm)],[f15264]) ).
fof(f15267,definition,
( sQ476_spl
<=> l3_lattices(k1_lattice2(sK899_skl)) ),
introduced(definition,[new_symbols(definition,[sQ476_spl])],[split_symbol_definition]) ).
fof(f15269,plain,
( sQ476_spl
| ~ l3_lattices(k1_lattice2(sK899_skl)) ),
inference(component_clause,[status(thm)],[f15267]) ).
fof(f15300,plain,
( ~ sQ474_spl
| ~ l3_lattices(sK899_skl)
| v3_struct_0(sK899_skl) ),
inference(resolution,[status(thm)],[f15262,f10409]) ).
fof(f15301,plain,
( ~ sQ474_spl
| ~ sQ410_spl
| sQ411_spl ),
inference(split_clause,[status(thm)],[f15300,f14840,f14837,f15261]) ).
fof(f15302,plain,
( sQ476_spl
| ~ l3_lattices(sK899_skl) ),
inference(resolution,[status(thm)],[f15269,f10802]) ).
fof(f15303,plain,
( sQ476_spl
| ~ sQ410_spl ),
inference(split_clause,[status(thm)],[f15302,f14837,f15267]) ).
fof(f15361,plain,
( sQ475_spl
| ~ l3_lattices(sK899_skl)
| ~ v10_lattices(sK899_skl)
| v3_struct_0(sK899_skl) ),
inference(resolution,[status(thm)],[f15266,f10444]) ).
fof(f15362,definition,
( sQ494_spl
<=> v10_lattices(sK899_skl) ),
introduced(definition,[new_symbols(definition,[sQ494_spl])],[split_symbol_definition]) ).
fof(f15364,plain,
( sQ494_spl
| ~ v10_lattices(sK899_skl) ),
inference(component_clause,[status(thm)],[f15362]) ).
fof(f15365,plain,
( sQ475_spl
| ~ sQ410_spl
| ~ sQ494_spl
| sQ411_spl ),
inference(split_clause,[status(thm)],[f15361,f14840,f15362,f14837,f15264]) ).
fof(f15366,plain,
( sQ494_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15364,f11514]) ).
fof(f15367,plain,
sQ494_spl,
inference(contradiction_clause,[status(thm)],[f15366]) ).
fof(f15951,definition,
( sQ589_spl
<=> v10_lattices(sK738_skl) ),
introduced(definition,[new_symbols(definition,[sQ589_spl])],[split_symbol_definition]) ).
fof(f15953,plain,
( sQ589_spl
| ~ v10_lattices(sK738_skl) ),
inference(component_clause,[status(thm)],[f15951]) ).
fof(f15955,plain,
( sQ589_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15953,f9597]) ).
fof(f15956,plain,
sQ589_spl,
inference(contradiction_clause,[status(thm)],[f15955]) ).
fof(f16150,definition,
( sQ627_spl
<=> l3_lattices(sK732_skl) ),
introduced(definition,[new_symbols(definition,[sQ627_spl])],[split_symbol_definition]) ).
fof(f16152,plain,
( sQ627_spl
| ~ l3_lattices(sK732_skl) ),
inference(component_clause,[status(thm)],[f16150]) ).
fof(f16154,plain,
( sQ627_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16152,f9541]) ).
fof(f16155,plain,
sQ627_spl,
inference(contradiction_clause,[status(thm)],[f16154]) ).
fof(f16206,definition,
( sQ638_spl
<=> l3_lattices(sK735_skl) ),
introduced(definition,[new_symbols(definition,[sQ638_spl])],[split_symbol_definition]) ).
fof(f16208,plain,
( sQ638_spl
| ~ l3_lattices(sK735_skl) ),
inference(component_clause,[status(thm)],[f16206]) ).
fof(f16210,plain,
( sQ638_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16208,f9561]) ).
fof(f16211,plain,
sQ638_spl,
inference(contradiction_clause,[status(thm)],[f16210]) ).
fof(f16262,definition,
( sQ649_spl
<=> l3_lattices(sK782_skl) ),
introduced(definition,[new_symbols(definition,[sQ649_spl])],[split_symbol_definition]) ).
fof(f16264,plain,
( sQ649_spl
| ~ l3_lattices(sK782_skl) ),
inference(component_clause,[status(thm)],[f16262]) ).
fof(f16266,plain,
( sQ649_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16264,f9904]) ).
fof(f16267,plain,
sQ649_spl,
inference(contradiction_clause,[status(thm)],[f16266]) ).
fof(f16320,definition,
! [X0] :
( sQ656_spl
<=> ~ r2_hidden(X0,k1_zfmisc_1(k1_xboole_0)) ),
introduced(definition,[new_symbols(definition,[sQ656_spl])],[split_symbol_definition]) ).
fof(f16321,plain,
! [X0] :
( ~ sQ656_spl
| ~ r2_hidden(X0,k1_zfmisc_1(k1_xboole_0)) ),
inference(component_clause,[status(thm)],[f16320]) ).
fof(f16324,plain,
! [X0] :
( ~ sQ656_spl
| ~ r2_hidden(X0,k1_tarski(k1_xboole_0)) ),
inference(forward_demodulation,[status(thm)],[f3566,f16321]) ).
fof(f16343,plain,
( ~ sQ656_spl
| $false ),
inference(resolution,[status(thm)],[f16324,f13769]) ).
fof(f16344,plain,
~ sQ656_spl,
inference(contradiction_clause,[status(thm)],[f16343]) ).
fof(f16407,definition,
( sQ657_spl
<=> v10_lattices(sK739_skl) ),
introduced(definition,[new_symbols(definition,[sQ657_spl])],[split_symbol_definition]) ).
fof(f16409,plain,
( sQ657_spl
| ~ v10_lattices(sK739_skl) ),
inference(component_clause,[status(thm)],[f16407]) ).
fof(f16411,plain,
( sQ657_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16409,f9608]) ).
fof(f16412,plain,
sQ657_spl,
inference(contradiction_clause,[status(thm)],[f16411]) ).
fof(f16503,definition,
( sQ675_spl
<=> v10_lattices(sK740_skl) ),
introduced(definition,[new_symbols(definition,[sQ675_spl])],[split_symbol_definition]) ).
fof(f16505,plain,
( sQ675_spl
| ~ v10_lattices(sK740_skl) ),
inference(component_clause,[status(thm)],[f16503]) ).
fof(f16507,plain,
( sQ675_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16505,f9630]) ).
fof(f16508,plain,
sQ675_spl,
inference(contradiction_clause,[status(thm)],[f16507]) ).
fof(f16812,definition,
( sQ705_spl
<=> v10_lattices(sK741_skl) ),
introduced(definition,[new_symbols(definition,[sQ705_spl])],[split_symbol_definition]) ).
fof(f16814,plain,
( sQ705_spl
| ~ v10_lattices(sK741_skl) ),
inference(component_clause,[status(thm)],[f16812]) ).
fof(f16816,plain,
( sQ705_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16814,f9644]) ).
fof(f16817,plain,
sQ705_spl,
inference(contradiction_clause,[status(thm)],[f16816]) ).
fof(f16908,definition,
( sQ723_spl
<=> v10_lattices(sK742_skl) ),
introduced(definition,[new_symbols(definition,[sQ723_spl])],[split_symbol_definition]) ).
fof(f16910,plain,
( sQ723_spl
| ~ v10_lattices(sK742_skl) ),
inference(component_clause,[status(thm)],[f16908]) ).
fof(f16912,plain,
( sQ723_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16910,f9669]) ).
fof(f16913,plain,
sQ723_spl,
inference(contradiction_clause,[status(thm)],[f16912]) ).
fof(f17010,plain,
( ~ sQ475_spl
| m1_filter_0(u1_struct_0(k1_lattice2(sK899_skl)),k1_lattice2(sK899_skl))
| ~ l3_lattices(k1_lattice2(sK899_skl))
| v3_struct_0(k1_lattice2(sK899_skl)) ),
inference(resolution,[status(thm)],[f10065,f15265]) ).
fof(f17045,definition,
( sQ747_spl
<=> m1_filter_0(u1_struct_0(k1_lattice2(sK899_skl)),k1_lattice2(sK899_skl)) ),
introduced(definition,[new_symbols(definition,[sQ747_spl])],[split_symbol_definition]) ).
fof(f17046,plain,
( ~ sQ747_spl
| m1_filter_0(u1_struct_0(k1_lattice2(sK899_skl)),k1_lattice2(sK899_skl)) ),
inference(component_clause,[status(thm)],[f17045]) ).
fof(f17048,plain,
( ~ sQ475_spl
| sQ747_spl
| ~ sQ476_spl
| sQ474_spl ),
inference(split_clause,[status(thm)],[f17010,f15261,f15267,f17045,f15264]) ).
fof(f17087,plain,
( ~ sQ747_spl
| ~ sQ472_spl
| m1_filter_0(u1_struct_0(sK899_skl),k1_lattice2(sK899_skl)) ),
inference(forward_demodulation,[status(thm)],[f15219,f17046]) ).
fof(f17109,plain,
( k1_filter_0(sK899_skl) = u1_struct_0(sK899_skl)
| ~ l3_lattices(sK899_skl)
| v3_struct_0(sK899_skl) ),
inference(resolution,[status(thm)],[f10067,f11514]) ).
fof(f17171,definition,
( sQ772_spl
<=> k1_filter_0(sK899_skl) = u1_struct_0(sK899_skl) ),
introduced(definition,[new_symbols(definition,[sQ772_spl])],[split_symbol_definition]) ).
fof(f17172,plain,
( ~ sQ772_spl
| k1_filter_0(sK899_skl) = u1_struct_0(sK899_skl) ),
inference(component_clause,[status(thm)],[f17171]) ).
fof(f17174,plain,
( sQ772_spl
| ~ sQ410_spl
| sQ411_spl ),
inference(split_clause,[status(thm)],[f17109,f14840,f14837,f17171]) ).
fof(f17263,plain,
( ~ sQ747_spl
| ~ sQ472_spl
| ~ sQ772_spl
| m1_filter_0(k1_filter_0(sK899_skl),k1_lattice2(sK899_skl)) ),
inference(backward_demodulation,[status(thm)],[f17172,f17087]) ).
fof(f17275,plain,
( ~ sQ772_spl
| ~ m2_filter_2(k1_filter_0(sK899_skl),sK899_skl) ),
inference(backward_demodulation,[status(thm)],[f17172,f11516]) ).
fof(f17364,definition,
( sQ787_spl
<=> v10_lattices(sK783_skl) ),
introduced(definition,[new_symbols(definition,[sQ787_spl])],[split_symbol_definition]) ).
fof(f17366,plain,
( sQ787_spl
| ~ v10_lattices(sK783_skl) ),
inference(component_clause,[status(thm)],[f17364]) ).
fof(f17368,plain,
( sQ787_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17366,f9977]) ).
fof(f17369,plain,
sQ787_spl,
inference(contradiction_clause,[status(thm)],[f17368]) ).
fof(f17472,definition,
( sQ807_spl
<=> v10_lattices(sK817_skl) ),
introduced(definition,[new_symbols(definition,[sQ807_spl])],[split_symbol_definition]) ).
fof(f17474,plain,
( sQ807_spl
| ~ v10_lattices(sK817_skl) ),
inference(component_clause,[status(thm)],[f17472]) ).
fof(f17476,plain,
( sQ807_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17474,f10454]) ).
fof(f17477,plain,
sQ807_spl,
inference(contradiction_clause,[status(thm)],[f17476]) ).
fof(f17859,definition,
( sQ860_spl
<=> v10_lattices(sK818_skl) ),
introduced(definition,[new_symbols(definition,[sQ860_spl])],[split_symbol_definition]) ).
fof(f17861,plain,
( sQ860_spl
| ~ v10_lattices(sK818_skl) ),
inference(component_clause,[status(thm)],[f17859]) ).
fof(f17863,plain,
( sQ860_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17861,f10487]) ).
fof(f17864,plain,
sQ860_spl,
inference(contradiction_clause,[status(thm)],[f17863]) ).
fof(f18352,plain,
( ~ sQ747_spl
| ~ sQ472_spl
| ~ sQ772_spl
| m1_filter_2(k1_filter_0(sK899_skl),k1_lattice2(sK899_skl))
| ~ l3_lattices(k1_lattice2(sK899_skl))
| ~ v10_lattices(k1_lattice2(sK899_skl))
| v3_struct_0(k1_lattice2(sK899_skl)) ),
inference(resolution,[status(thm)],[f11276,f17263]) ).
fof(f18368,definition,
( sQ889_spl
<=> m1_filter_2(k1_filter_0(sK899_skl),k1_lattice2(sK899_skl)) ),
introduced(definition,[new_symbols(definition,[sQ889_spl])],[split_symbol_definition]) ).
fof(f18369,plain,
( ~ sQ889_spl
| m1_filter_2(k1_filter_0(sK899_skl),k1_lattice2(sK899_skl)) ),
inference(component_clause,[status(thm)],[f18368]) ).
fof(f18371,plain,
( ~ sQ747_spl
| ~ sQ472_spl
| ~ sQ772_spl
| sQ889_spl
| ~ sQ476_spl
| ~ sQ475_spl
| sQ474_spl ),
inference(split_clause,[status(thm)],[f18352,f15261,f15264,f15267,f18368,f17171,f15218,f17045]) ).
fof(f18935,plain,
( ~ sQ889_spl
| m2_filter_2(k1_filter_0(sK899_skl),sK899_skl)
| ~ l3_lattices(sK899_skl)
| ~ v10_lattices(sK899_skl)
| v3_struct_0(sK899_skl) ),
inference(resolution,[status(thm)],[f11472,f18369]) ).
fof(f18946,definition,
( sQ929_spl
<=> m2_filter_2(k1_filter_0(sK899_skl),sK899_skl) ),
introduced(definition,[new_symbols(definition,[sQ929_spl])],[split_symbol_definition]) ).
fof(f18947,plain,
( ~ sQ929_spl
| m2_filter_2(k1_filter_0(sK899_skl),sK899_skl) ),
inference(component_clause,[status(thm)],[f18946]) ).
fof(f18949,plain,
( ~ sQ889_spl
| sQ929_spl
| ~ sQ410_spl
| ~ sQ494_spl
| sQ411_spl ),
inference(split_clause,[status(thm)],[f18935,f14840,f15362,f14837,f18946,f18368]) ).
fof(f18951,plain,
( ~ sQ929_spl
| ~ sQ772_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18947,f17275]) ).
fof(f18952,plain,
( ~ sQ929_spl
| ~ sQ772_spl ),
inference(contradiction_clause,[status(thm)],[f18951]) ).
fof(f18953,plain,
$false,
inference(sat_refutation,[status(thm)],[f14848,f14850,f15221,f15301,f15303,f15365,f15367,f15956,f16155,f16211,f16267,f16344,f16412,f16508,f16817,f16913,f17048,f17174,f17369,f17477,f17864,f18371,f18949,f18952]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT304+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n005.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 20 23:31:34 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.31/0.62 % Drodi V4.1.1
% 280.16/36.29 % Refutation found
% 280.16/36.29 % SZS status Theorem for theBenchmark: Theorem is valid
% 280.16/36.29 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 102.35/36.47 % Elapsed time: 36.091513 seconds
% 102.35/36.47 % CPU time: 283.753874 seconds
% 102.35/36.47 % Total memory used: 981.222 MB
% 102.35/36.47 % Net memory used: 898.929 MB
%------------------------------------------------------------------------------