%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT301+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.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 : Fri Sep 25 01:56:43 PM UTC 2026
% Result : Theorem 164.80s 29.26s
% Output : Proof 164.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 13
% Syntax : Number of formulae : 109 ( 9 unt; 0 def)
% Number of atoms : 473 ( 24 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 550 ( 186 ~; 261 |; 78 &)
% ( 2 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 2 con; 0-2 aty)
% Number of variables : 102 ( 0 sgn 61 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f85,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',t78_lattice2) ).
fof(f85_nnf,plain,
! [A] :
( k5_lattices(A) = k6_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v13_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f85]) ).
fof(f85_sk,plain,
! [A] :
( k5_lattices(A) = k6_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v13_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f85_nnf]) ).
cnf(c178,plain,
( 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(esa)],[f85_sk]) ).
fof(f0,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( v13_lattices(A)
=> r2_hidden(k5_lattices(A),B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t25_filter_2) ).
fof(f0_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( v13_lattices(A)
=> r2_hidden(k5_lattices(A),B) ) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A] :
( ? [B] :
( ~ r2_hidden(k5_lattices(A),B)
& v13_lattices(A)
& m2_filter_2(B,A) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
( ~ r2_hidden(k5_lattices(sk0),sk1)
& v13_lattices(sk0)
& m2_filter_2(sk1,sk0)
& l3_lattices(sk0)
& v10_lattices(sk0)
& ~ v3_struct_0(sk0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f0_nnf]) ).
cnf(c1,plain,
v10_lattices(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1883,plain,
( k5_lattices(sk0) = k6_lattices(k1_lattice2(sk0))
| ~ l3_lattices(sk0)
| ~ v13_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c178,c1]) ).
cnf(c4,plain,
v13_lattices(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4357,plain,
( k5_lattices(sk0) = k6_lattices(k1_lattice2(sk0))
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1883,c4]) ).
cnf(c2,plain,
l3_lattices(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4358,plain,
( k5_lattices(sk0) = k6_lattices(k1_lattice2(sk0))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p4357,c2]) ).
fof(f77,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_0(B,A)
=> ( ( l3_lattices(A)
& v14_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> r2_hidden(k6_lattices(A),B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_filter_0) ).
fof(f77_nnf,plain,
! [A] :
( ! [B] :
( r2_hidden(k6_lattices(A),B)
| ~ l3_lattices(A)
| ~ v14_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ m1_filter_0(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f77]) ).
fof(f77_sk,plain,
! [A,B] :
( r2_hidden(k6_lattices(A),B)
| ~ l3_lattices(A)
| ~ v14_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f77_nnf]) ).
cnf(c168,plain,
( r2_hidden(k6_lattices(X0),X1)
| ~ l3_lattices(X0)
| ~ v14_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(p1786,plain,
( r2_hidden(k6_lattices(X0),X1)
| ~ l3_lattices(X0)
| ~ v14_lattices(X0)
| ~ v10_lattices(X0)
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(factoring,[status(thm)],[c168]) ).
cnf(p10446,plain,
( r2_hidden(k6_lattices(X0),X1)
| ~ l3_lattices(X0)
| ~ v14_lattices(X0)
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(factoring,[status(thm)],[p1786]) ).
cnf(p10525,plain,
( r2_hidden(k6_lattices(X0),X1)
| ~ v14_lattices(X0)
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(factoring,[status(thm)],[p10446]) ).
fof(f57,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',fc6_lattice2) ).
fof(f57_nnf,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(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,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(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c110,plain,
( v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(p1474,plain,
( v10_lattices(k1_lattice2(sk0))
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c110,c1]) ).
cnf(p2130,plain,
( v10_lattices(k1_lattice2(sk0))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1474,c2]) ).
cnf(p10529,plain,
( v3_struct_0(sk0)
| r2_hidden(k6_lattices(k1_lattice2(sk0)),X0)
| ~ v14_lattices(k1_lattice2(sk0))
| ~ m1_filter_0(X0,k1_lattice2(sk0))
| ~ l3_lattices(k1_lattice2(sk0))
| v3_struct_0(k1_lattice2(sk0)) ),
inference(resolution,[status(thm)],[p10525,p2130]) ).
fof(f14,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f14_nnf,plain,
! [A] :
( ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) )
| ~ l3_lattices(A) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [A] :
( ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) )
| ~ l3_lattices(A) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c33,plain,
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p254,plain,
l3_lattices(k1_lattice2(sk0)),
inference(resolution,[status(thm)],[c33,c2]) ).
cnf(p11983,plain,
( v3_struct_0(sk0)
| r2_hidden(k6_lattices(k1_lattice2(sk0)),X0)
| ~ v14_lattices(k1_lattice2(sk0))
| ~ m1_filter_0(X0,k1_lattice2(sk0))
| v3_struct_0(k1_lattice2(sk0)) ),
inference(resolution,[status(thm)],[p10529,p254]) ).
fof(f74,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',redefinition_m1_filter_2) ).
fof(f74_nnf,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)],[f74]) ).
fof(f74_sk,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(skolemisation,[status(esa)],[f74_nnf]) ).
cnf(c163,plain,
( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
cnf(p2156,plain,
( m1_filter_0(X0,k1_lattice2(sk0))
| ~ m1_filter_2(X0,k1_lattice2(sk0))
| ~ l3_lattices(k1_lattice2(sk0))
| v3_struct_0(k1_lattice2(sk0))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p2130,c163]) ).
cnf(p7541,plain,
( m1_filter_0(X0,k1_lattice2(sk0))
| ~ m1_filter_2(X0,k1_lattice2(sk0))
| v3_struct_0(k1_lattice2(sk0))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p2156,p254]) ).
fof(f30,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_lattice4(B,A)
=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f30_nnf,plain,
! [A] :
( ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ m2_lattice4(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ m2_lattice4(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c53,plain,
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p642,plain,
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ m2_lattice4(X0,sk0)
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c53,c1]) ).
cnf(p4234,plain,
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ m2_lattice4(X0,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p642,c2]) ).
fof(f29,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f29_nnf,plain,
! [A] :
( ! [B] :
( ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) )
| ~ m2_filter_2(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [A,B] :
( ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) )
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c52,plain,
( m2_lattice4(X1,X0)
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p607,plain,
( m2_lattice4(X0,sk0)
| ~ m2_filter_2(X0,sk0)
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c52,c1]) ).
cnf(p3524,plain,
( m2_lattice4(X0,sk0)
| ~ m2_filter_2(X0,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p607,c2]) ).
cnf(c3,plain,
m2_filter_2(sk1,sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p3525,plain,
( m2_lattice4(sk1,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p3524,c3]) ).
cnf(p4237,plain,
( v3_struct_0(sk0)
| m1_subset_1(sk1,k1_zfmisc_1(u1_struct_0(sk0)))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p4234,p3525]) ).
cnf(p4239,plain,
( m1_subset_1(sk1,k1_zfmisc_1(u1_struct_0(sk0)))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p4237]) ).
fof(f11,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> k7_filter_2(A,B) = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d6_filter_2) ).
fof(f11_nnf,plain,
! [A] :
( ! [B] :
( k7_filter_2(A,B) = B
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A,B] :
( k7_filter_2(A,B) = B
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c28,plain,
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p374,plain,
( k7_filter_2(sk0,X0) = X0
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c28,c1]) ).
cnf(p2812,plain,
( k7_filter_2(sk0,X0) = X0
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p374,c2]) ).
cnf(p4244,plain,
( k7_filter_2(sk0,sk1) = sk1
| v3_struct_0(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p4239,p2812]) ).
cnf(p4246,plain,
( k7_filter_2(sk0,sk1) = sk1
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p4244]) ).
fof(f73,axiom,
! [A,B] :
( ( m2_filter_2(B,A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k15_filter_2(A,B) = k7_filter_2(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k15_filter_2) ).
fof(f73_nnf,plain,
! [A,B] :
( k15_filter_2(A,B) = k7_filter_2(A,B)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f73]) ).
fof(f73_sk,plain,
! [A,B] :
( k15_filter_2(A,B) = k7_filter_2(A,B)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f73_nnf]) ).
cnf(c162,plain,
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f73_sk]) ).
cnf(p1769,plain,
( k15_filter_2(sk0,X0) = k7_filter_2(sk0,X0)
| ~ m2_filter_2(X0,sk0)
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c162,c1]) ).
cnf(p5244,plain,
( k15_filter_2(sk0,X0) = k7_filter_2(sk0,X0)
| ~ m2_filter_2(X0,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1769,c2]) ).
cnf(p5245,plain,
( k15_filter_2(sk0,sk1) = k7_filter_2(sk0,sk1)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p5244,c3]) ).
cnf(p5248,plain,
( k15_filter_2(sk0,sk1) = sk1
| v3_struct_0(sk0)
| v3_struct_0(sk0) ),
inference(superposition,[status(thm)],[p4246,p5245]) ).
cnf(p5249,plain,
( k15_filter_2(sk0,sk1) = sk1
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5248]) ).
fof(f13,axiom,
! [A,B] :
( ( m2_filter_2(B,A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_filter_2(k15_filter_2(A,B),k1_lattice2(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k15_filter_2) ).
fof(f13_nnf,plain,
! [A,B] :
( m1_filter_2(k15_filter_2(A,B),k1_lattice2(A))
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [A,B] :
( m1_filter_2(k15_filter_2(A,B),k1_lattice2(A))
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c31,plain,
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p398,plain,
( m1_filter_2(k15_filter_2(sk0,X0),k1_lattice2(sk0))
| ~ m2_filter_2(X0,sk0)
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c31,c1]) ).
cnf(p3066,plain,
( m1_filter_2(k15_filter_2(sk0,X0),k1_lattice2(sk0))
| ~ m2_filter_2(X0,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p398,c2]) ).
cnf(p3559,plain,
( m1_filter_2(k15_filter_2(sk0,sk1),k1_lattice2(sk0))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p3066,c3]) ).
cnf(p5252,plain,
( m1_filter_2(sk1,k1_lattice2(sk0))
| v3_struct_0(sk0)
| v3_struct_0(sk0) ),
inference(superposition,[status(thm)],[p5249,p3559]) ).
cnf(p5254,plain,
( m1_filter_2(sk1,k1_lattice2(sk0))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5252]) ).
cnf(p7544,plain,
( v3_struct_0(sk0)
| m1_filter_0(sk1,k1_lattice2(sk0))
| v3_struct_0(k1_lattice2(sk0))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p7541,p5254]) ).
cnf(p7549,plain,
( m1_filter_0(sk1,k1_lattice2(sk0))
| v3_struct_0(k1_lattice2(sk0))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p7544]) ).
cnf(p11985,plain,
( v3_struct_0(k1_lattice2(sk0))
| v3_struct_0(sk0)
| v3_struct_0(sk0)
| r2_hidden(k6_lattices(k1_lattice2(sk0)),sk1)
| ~ v14_lattices(k1_lattice2(sk0))
| v3_struct_0(k1_lattice2(sk0)) ),
inference(resolution,[status(thm)],[p11983,p7549]) ).
cnf(p11992,plain,
( v3_struct_0(sk0)
| v3_struct_0(sk0)
| r2_hidden(k6_lattices(k1_lattice2(sk0)),sk1)
| ~ v14_lattices(k1_lattice2(sk0))
| v3_struct_0(k1_lattice2(sk0)) ),
inference(factoring,[status(thm)],[p11985]) ).
cnf(p11995,plain,
( v3_struct_0(sk0)
| r2_hidden(k6_lattices(k1_lattice2(sk0)),sk1)
| ~ v14_lattices(k1_lattice2(sk0))
| v3_struct_0(k1_lattice2(sk0)) ),
inference(factoring,[status(thm)],[p11992]) ).
fof(f83,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',t63_lattice2) ).
fof(f83_nnf,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)],[f83]) ).
fof(f83_sk,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(skolemisation,[status(esa)],[f83_nnf]) ).
cnf(c175,plain,
( v14_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(p1811,plain,
( v14_lattices(k1_lattice2(sk0))
| ~ v13_lattices(sk0)
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c175,c1]) ).
cnf(p3171,plain,
( v14_lattices(k1_lattice2(sk0))
| ~ v13_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1811,c2]) ).
cnf(p3172,plain,
( v14_lattices(k1_lattice2(sk0))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p3171,c4]) ).
cnf(p11996,plain,
( v3_struct_0(sk0)
| v3_struct_0(sk0)
| r2_hidden(k6_lattices(k1_lattice2(sk0)),sk1)
| v3_struct_0(k1_lattice2(sk0)) ),
inference(resolution,[status(thm)],[p11995,p3172]) ).
cnf(p11997,plain,
( v3_struct_0(sk0)
| r2_hidden(k6_lattices(k1_lattice2(sk0)),sk1)
| v3_struct_0(k1_lattice2(sk0)) ),
inference(factoring,[status(thm)],[p11996]) ).
cnf(p12002,plain,
( v3_struct_0(sk0)
| r2_hidden(k5_lattices(sk0),sk1)
| v3_struct_0(k1_lattice2(sk0))
| v3_struct_0(sk0) ),
inference(superposition,[status(thm)],[p4358,p11997]) ).
cnf(p12005,plain,
( r2_hidden(k5_lattices(sk0),sk1)
| v3_struct_0(k1_lattice2(sk0))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p12002]) ).
cnf(c5,plain,
~ r2_hidden(k5_lattices(sk0),sk1),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p12008,plain,
( v3_struct_0(k1_lattice2(sk0))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p12005,c5]) ).
fof(f47,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',fc1_lattice2) ).
fof(f47_nnf,plain,
! [A] :
( ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) )
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
! [A] :
( ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) )
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c74,plain,
( ~ v3_struct_0(k1_lattice2(X0))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p927,plain,
( ~ v3_struct_0(k1_lattice2(sk0))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c74,c2]) ).
cnf(p12009,plain,
( v3_struct_0(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p12008,p927]) ).
cnf(p12010,plain,
v3_struct_0(sk0),
inference(factoring,[status(thm)],[p12009]) ).
cnf(c0,plain,
~ v3_struct_0(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p12011,plain,
$false,
inference(resolution,[status(thm)],[p12010,c0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT301+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/5.37 % Computer : n017.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Wed Sep 23 20:51:36 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 164.80/29.26 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 164.80/29.26 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------