%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT304+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 : n018.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 4.33s 1.02s
% Output : CNFRefutation 4.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 14
% Syntax : Number of formulae : 97 ( 22 unt; 0 def)
% Number of atoms : 328 ( 30 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 370 ( 139 ~; 146 |; 64 &)
% ( 5 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 1 con; 0-3 aty)
% Number of variables : 100 ( 99 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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(f2,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)],[f1]) ).
fof(f3,axiom,
! [A] :
( l3_lattices(A)
=> ( v3_lattices(A)
=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A] :
( l3_lattices(A)
=> k1_lattice2(A) = g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A] :
( l1_lattices(A)
=> ( m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u1_lattices(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
( l2_lattices(A)
=> ( m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u2_lattices(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,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(f51,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(f52,axiom,
! [A,B,C] :
( ( m1_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C)
& m1_relset_1(B,k2_zfmisc_1(A,A),A)
& v1_funct_2(B,k2_zfmisc_1(A,A),A)
& v1_funct_1(B) )
=> ! [D,E,F] :
( g3_lattices(A,B,C) = g3_lattices(D,E,F)
=> ( C = F
& B = E
& A = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,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(f67,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,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(f71,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(f79,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)],[f2]) ).
fof(f80,plain,
( ~ m2_filter_2(u1_struct_0(sK0_skl),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)],[f79]) ).
fof(f81,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f82,plain,
v10_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f83,plain,
l3_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f84,plain,
~ m2_filter_2(u1_struct_0(sK0_skl),sK0_skl),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f85,plain,
! [A] :
( A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))
| ~ v3_lattices(A)
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f86,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f109,plain,
! [A] :
( k1_lattice2(A) = g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A))
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f110,plain,
! [X0] :
( k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f114,plain,
! [A] :
( ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f115,plain,
! [X0] :
( v3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f116,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f121,plain,
! [A] :
( ( l2_lattices(A)
& l1_lattices(A) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f122,plain,
! [X0] :
( l1_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
! [X0] :
( l2_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f137,plain,
! [A] :
( ( m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u1_lattices(A)) )
| ~ l1_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f138,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f139,plain,
! [X0] :
( v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f140,plain,
! [X0] :
( m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f141,plain,
! [A] :
( ( m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u2_lattices(A)) )
| ~ l2_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f142,plain,
! [X0] :
( v1_funct_1(u2_lattices(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f143,plain,
! [X0] :
( v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f144,plain,
! [X0] :
( m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f171,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)],[f41]) ).
fof(f172,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f207,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)],[f51]) ).
fof(f216,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f217,plain,
! [A,B,C] :
( ! [D,E,F] :
( ( C = F
& B = E
& A = D )
| g3_lattices(A,B,C) != g3_lattices(D,E,F) )
| ~ m1_relset_1(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(C)
| ~ m1_relset_1(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f218,plain,
! [X0,X1,X2,X3,X4,X5] :
( X1 = X3
| g3_lattices(X1,X0,X2) != g3_lattices(X3,X4,X5)
| ~ m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f272,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)],[f66]) ).
fof(f273,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)],[f272]) ).
fof(f274,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)],[f273]) ).
fof(f276,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)],[f274]) ).
fof(f277,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)],[f67]) ).
fof(f278,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)],[f277]) ).
fof(f279,plain,
! [X0,X1,X2] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f283,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)],[f69]) ).
fof(f284,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)],[f283]) ).
fof(f287,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)],[f71]) ).
fof(f288,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)],[f287]) ).
fof(f289,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)],[f288]) ).
fof(f291,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)],[f289]) ).
fof(f360,plain,
k1_lattice2(sK0_skl) = g3_lattices(u1_struct_0(sK0_skl),u1_lattices(sK0_skl),u2_lattices(sK0_skl)),
inference(resolution,[status(thm)],[f110,f83]) ).
fof(f387,plain,
v3_lattices(k1_lattice2(sK0_skl)),
inference(resolution,[status(thm)],[f115,f83]) ).
fof(f388,plain,
( k1_lattice2(sK0_skl) = g3_lattices(u1_struct_0(k1_lattice2(sK0_skl)),u2_lattices(k1_lattice2(sK0_skl)),u1_lattices(k1_lattice2(sK0_skl)))
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f387,f86]) ).
fof(f401,plain,
l3_lattices(k1_lattice2(sK0_skl)),
inference(resolution,[status(thm)],[f116,f83]) ).
fof(f402,plain,
k1_lattice2(sK0_skl) = g3_lattices(u1_struct_0(k1_lattice2(sK0_skl)),u2_lattices(k1_lattice2(sK0_skl)),u1_lattices(k1_lattice2(sK0_skl))),
inference(backward_subsumption_resolution,[status(thm)],[f388,f401]) ).
fof(f423,plain,
l1_lattices(sK0_skl),
inference(resolution,[status(thm)],[f122,f83]) ).
fof(f446,plain,
l2_lattices(sK0_skl),
inference(resolution,[status(thm)],[f123,f83]) ).
fof(f479,plain,
v1_funct_1(u1_lattices(sK0_skl)),
inference(resolution,[status(thm)],[f138,f423]) ).
fof(f511,plain,
v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(resolution,[status(thm)],[f139,f423]) ).
fof(f520,plain,
m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(resolution,[status(thm)],[f140,f423]) ).
fof(f529,plain,
v1_funct_1(u2_lattices(sK0_skl)),
inference(resolution,[status(thm)],[f142,f446]) ).
fof(f557,plain,
v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(resolution,[status(thm)],[f143,f446]) ).
fof(f567,plain,
m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(resolution,[status(thm)],[f144,f446]) ).
fof(f1364,plain,
m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(resolution,[status(thm)],[f279,f567]) ).
fof(f1366,plain,
m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(resolution,[status(thm)],[f279,f520]) ).
fof(f1656,plain,
( v10_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f216,f83]) ).
fof(f1659,plain,
( v10_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1656,f81]) ).
fof(f1664,plain,
! [X0,X1,X2] :
( u1_struct_0(sK0_skl) = X0
| k1_lattice2(sK0_skl) != g3_lattices(X0,X1,X2)
| ~ m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_1(u2_lattices(sK0_skl))
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f360,f218]) ).
fof(f1675,plain,
! [X0,X1,X2] :
( u1_struct_0(sK0_skl) = X0
| k1_lattice2(sK0_skl) != g3_lattices(X0,X1,X2)
| ~ m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_1(u2_lattices(sK0_skl))
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1664,f479]) ).
fof(f1701,plain,
v10_lattices(k1_lattice2(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f1659,f82]) ).
fof(f1975,plain,
! [X0,X1,X2] :
( u1_struct_0(sK0_skl) = X0
| k1_lattice2(sK0_skl) != g3_lattices(X0,X1,X2)
| ~ m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_1(u2_lattices(sK0_skl))
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1675,f511]) ).
fof(f1976,plain,
( u1_struct_0(sK0_skl) = u1_struct_0(k1_lattice2(sK0_skl))
| ~ m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_1(u2_lattices(sK0_skl))
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f1975,f402]) ).
fof(f1983,plain,
( u1_struct_0(sK0_skl) = u1_struct_0(k1_lattice2(sK0_skl))
| ~ m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_1(u2_lattices(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1976,f1366]) ).
fof(f2023,plain,
( m1_filter_0(u1_struct_0(k1_lattice2(sK0_skl)),k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f284,f401]) ).
fof(f2029,plain,
( m1_filter_0(u1_struct_0(k1_lattice2(sK0_skl)),k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2023,f1701]) ).
fof(f2191,plain,
( m1_filter_2(u1_struct_0(k1_lattice2(sK0_skl)),k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f2029,f276]) ).
fof(f2194,plain,
( m1_filter_2(u1_struct_0(k1_lattice2(sK0_skl)),k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f2191]) ).
fof(f2195,plain,
( m1_filter_2(u1_struct_0(k1_lattice2(sK0_skl)),k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2194,f1701]) ).
fof(f3306,plain,
( u1_struct_0(sK0_skl) = u1_struct_0(k1_lattice2(sK0_skl))
| ~ m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1983,f529]) ).
fof(f3307,plain,
( u1_struct_0(sK0_skl) = u1_struct_0(k1_lattice2(sK0_skl))
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f3306,f1364]) ).
fof(f3308,plain,
u1_struct_0(sK0_skl) = u1_struct_0(k1_lattice2(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f3307,f557]) ).
fof(f3946,plain,
( m1_filter_2(u1_struct_0(sK0_skl),k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f3308,f2195]) ).
fof(f3947,plain,
( m1_filter_2(u1_struct_0(sK0_skl),k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3946,f401]) ).
fof(f3948,plain,
( m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f3947,f291]) ).
fof(f3952,plain,
( m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f3948,f172]) ).
fof(f3978,plain,
( m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f3952,f81]) ).
fof(f3979,plain,
( m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f3978,f83]) ).
fof(f3980,plain,
m2_filter_2(u1_struct_0(sK0_skl),sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f3979,f82]) ).
fof(f3985,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f3980,f84]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT304+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n018.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sun Sep 20 23:33:43 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.11/0.36 % Drodi V4.1.1
% 4.33/1.02 % Refutation found
% 4.33/1.02 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.33/1.02 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.33/1.04 % Elapsed time: 0.679268 seconds
% 4.33/1.04 % CPU time: 5.045503 seconds
% 4.33/1.04 % Total memory used: 162.726 MB
% 4.33/1.04 % Net memory used: 159.142 MB
%------------------------------------------------------------------------------