%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT310+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n009.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:45 PM UTC 2026
% Result : Theorem 27.71s 4.03s
% Output : Proof 27.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 7
% Syntax : Number of formulae : 108 ( 15 unt; 0 def)
% Number of atoms : 540 ( 15 equ)
% Maximal formula atoms : 16 ( 5 avg)
% Number of connectives : 612 ( 180 ~; 354 |; 56 &)
% ( 1 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 111 ( 2 sgn 52 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(B) )
=> ! [C] :
( m2_filter_2(C,A)
=> ( C = k19_filter_2(A,B)
<=> ( ! [D] :
( m2_filter_2(D,A)
=> ( r1_tarski(B,D)
=> r1_tarski(C,D) ) )
& r1_tarski(B,C) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_filter_2) ).
fof(f5_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ? [D] :
( ~ r1_tarski(C,D)
& r1_tarski(B,D)
& m2_filter_2(D,A) )
| ~ r1_tarski(B,C)
| C = k19_filter_2(A,B) )
& ( ( ! [D] :
( r1_tarski(C,D)
| ~ r1_tarski(B,D)
| ~ m2_filter_2(D,A) )
& r1_tarski(B,C) )
| C != k19_filter_2(A,B) ) )
| ~ m2_filter_2(C,A) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,B,C,D] :
( ( ( ( ~ r1_tarski(C,sk4(A,B,C))
& r1_tarski(B,sk4(A,B,C))
& m2_filter_2(sk4(A,B,C),A) )
| ~ r1_tarski(B,C)
| C = k19_filter_2(A,B) )
& ( ( ( r1_tarski(C,D)
| ~ r1_tarski(B,D)
| ~ m2_filter_2(D,A) )
& r1_tarski(B,C) )
| C != k19_filter_2(A,B) ) )
| ~ m2_filter_2(C,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk4])],[f5_nnf]) ).
cnf(c23,plain,
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0)
| X2 != k19_filter_2(X0,X1)
| ~ m2_filter_2(X2,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
fof(f0,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(C) )
=> ! [D] :
( ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(D) )
=> ( r1_tarski(k19_filter_2(A,k19_filter_2(A,B)),k19_filter_2(A,B))
& ( r1_tarski(C,D)
=> r1_tarski(k19_filter_2(A,C),k19_filter_2(A,D)) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t39_filter_2) ).
fof(f0_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(C) )
=> ! [D] :
( ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(D) )
=> ( r1_tarski(k19_filter_2(A,k19_filter_2(A,B)),k19_filter_2(A,B))
& ( r1_tarski(C,D)
=> r1_tarski(k19_filter_2(A,C),k19_filter_2(A,D)) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ( ~ r1_tarski(k19_filter_2(A,k19_filter_2(A,B)),k19_filter_2(A,B))
| ( ~ r1_tarski(k19_filter_2(A,C),k19_filter_2(A,D))
& r1_tarski(C,D) ) )
& m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(D) )
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(C) )
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(B) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
( ( ~ r1_tarski(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),k19_filter_2(sk0,sk1))
| ( ~ r1_tarski(k19_filter_2(sk0,sk2),k19_filter_2(sk0,sk3))
& r1_tarski(sk2,sk3) ) )
& m1_subset_1(sk3,k1_zfmisc_1(u1_struct_0(sk0)))
& ~ v1_xboole_0(sk3)
& m1_subset_1(sk2,k1_zfmisc_1(u1_struct_0(sk0)))
& ~ v1_xboole_0(sk2)
& m1_subset_1(sk1,k1_zfmisc_1(u1_struct_0(sk0)))
& ~ v1_xboole_0(sk1)
& l3_lattices(sk0)
& v10_lattices(sk0)
& ~ v3_struct_0(sk0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3])],[f0_nnf]) ).
cnf(c1,plain,
v10_lattices(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p115,plain,
( r1_tarski(X1,X2)
| ~ r1_tarski(X0,X2)
| ~ m2_filter_2(X2,sk0)
| X1 != k19_filter_2(sk0,X0)
| ~ m2_filter_2(X1,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| v1_xboole_0(X0)
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c23,c1]) ).
cnf(c2,plain,
l3_lattices(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p421,plain,
( r1_tarski(X1,X2)
| ~ r1_tarski(X0,X2)
| ~ m2_filter_2(X2,sk0)
| X1 != k19_filter_2(sk0,X0)
| ~ m2_filter_2(X1,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| v1_xboole_0(X0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p115,c2]) ).
fof(f15,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/sandbox2/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f15_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)],[f15]) ).
fof(f15_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)],[f15_nnf]) ).
cnf(c38,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)],[f15_sk]) ).
cnf(p172,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)],[c38,c1]) ).
cnf(p207,plain,
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ m2_lattice4(X0,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p172,c2]) ).
fof(f14,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/sandbox2/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f14_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)],[f14]) ).
fof(f14_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)],[f14_nnf]) ).
cnf(c37,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)],[f14_sk]) ).
cnf(p169,plain,
( m2_lattice4(X0,sk0)
| ~ m2_filter_2(X0,sk0)
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c37,c1]) ).
cnf(p173,plain,
( m2_lattice4(X0,sk0)
| ~ m2_filter_2(X0,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p169,c2]) ).
fof(f6,axiom,
! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(B)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m2_filter_2(k19_filter_2(A,B),A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k19_filter_2) ).
fof(f6_nnf,plain,
! [A,B] :
( m2_filter_2(k19_filter_2(A,B),A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B] :
( m2_filter_2(k19_filter_2(A,B),A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c27,plain,
( m2_filter_2(k19_filter_2(X0,X1),X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p132,plain,
( m2_filter_2(k19_filter_2(sk0,X0),sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| v1_xboole_0(X0)
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c27,c1]) ).
cnf(p133,plain,
( m2_filter_2(k19_filter_2(sk0,X0),sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| v1_xboole_0(X0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p132,c2]) ).
cnf(c4,plain,
m1_subset_1(sk1,k1_zfmisc_1(u1_struct_0(sk0))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p134,plain,
( m2_filter_2(k19_filter_2(sk0,sk1),sk0)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p133,c4]) ).
cnf(p174,plain,
( v1_xboole_0(sk1)
| v3_struct_0(sk0)
| m2_lattice4(k19_filter_2(sk0,sk1),sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p173,p134]) ).
cnf(p177,plain,
( v1_xboole_0(sk1)
| m2_lattice4(k19_filter_2(sk0,sk1),sk0)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p174]) ).
cnf(p210,plain,
( v1_xboole_0(sk1)
| v3_struct_0(sk0)
| m1_subset_1(k19_filter_2(sk0,sk1),k1_zfmisc_1(u1_struct_0(sk0)))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p207,p177]) ).
cnf(p237,plain,
( v1_xboole_0(sk1)
| m1_subset_1(k19_filter_2(sk0,sk1),k1_zfmisc_1(u1_struct_0(sk0)))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p210]) ).
cnf(p1590,plain,
( v1_xboole_0(sk1)
| v3_struct_0(sk0)
| r1_tarski(X0,X1)
| ~ r1_tarski(k19_filter_2(sk0,sk1),X1)
| ~ m2_filter_2(X1,sk0)
| X0 != k19_filter_2(sk0,k19_filter_2(sk0,sk1))
| ~ m2_filter_2(X0,sk0)
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p421,p237]) ).
cnf(p4931,plain,
( v1_xboole_0(sk1)
| r1_tarski(X0,X1)
| ~ r1_tarski(k19_filter_2(sk0,sk1),X1)
| ~ m2_filter_2(X1,sk0)
| X0 != k19_filter_2(sk0,k19_filter_2(sk0,sk1))
| ~ m2_filter_2(X0,sk0)
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p1590]) ).
cnf(p4932,plain,
( v1_xboole_0(sk1)
| r1_tarski(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),X0)
| ~ r1_tarski(k19_filter_2(sk0,sk1),X0)
| ~ m2_filter_2(X0,sk0)
| ~ m2_filter_2(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),sk0)
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0) ),
inference(equality_resolution,[status(thm)],[p4931]) ).
cnf(p242,plain,
( m2_filter_2(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),sk0)
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p237,p133]) ).
cnf(p534,plain,
( m2_filter_2(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),sk0)
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p242]) ).
cnf(p4965,plain,
( v1_xboole_0(k19_filter_2(sk0,sk1))
| v1_xboole_0(sk1)
| v3_struct_0(sk0)
| v1_xboole_0(sk1)
| r1_tarski(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),X0)
| ~ r1_tarski(k19_filter_2(sk0,sk1),X0)
| ~ m2_filter_2(X0,sk0)
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p4932,p534]) ).
cnf(p5270,plain,
( v1_xboole_0(sk1)
| v3_struct_0(sk0)
| v1_xboole_0(sk1)
| r1_tarski(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),X0)
| ~ r1_tarski(k19_filter_2(sk0,sk1),X0)
| ~ m2_filter_2(X0,sk0)
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p4965]) ).
cnf(p5272,plain,
( v1_xboole_0(sk1)
| v1_xboole_0(sk1)
| r1_tarski(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),X0)
| ~ r1_tarski(k19_filter_2(sk0,sk1),X0)
| ~ m2_filter_2(X0,sk0)
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5270]) ).
cnf(p5275,plain,
( v1_xboole_0(sk1)
| r1_tarski(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),X0)
| ~ r1_tarski(k19_filter_2(sk0,sk1),X0)
| ~ m2_filter_2(X0,sk0)
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5272]) ).
cnf(p5276,plain,
( v1_xboole_0(sk1)
| v3_struct_0(sk0)
| v1_xboole_0(sk1)
| r1_tarski(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),k19_filter_2(sk0,sk1))
| ~ r1_tarski(k19_filter_2(sk0,sk1),k19_filter_2(sk0,sk1))
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p5275,p134]) ).
cnf(p5307,plain,
( v1_xboole_0(sk1)
| v1_xboole_0(sk1)
| r1_tarski(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),k19_filter_2(sk0,sk1))
| ~ r1_tarski(k19_filter_2(sk0,sk1),k19_filter_2(sk0,sk1))
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5276]) ).
cnf(p5309,plain,
( v1_xboole_0(sk1)
| r1_tarski(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),k19_filter_2(sk0,sk1))
| ~ r1_tarski(k19_filter_2(sk0,sk1),k19_filter_2(sk0,sk1))
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5307]) ).
fof(f34,axiom,
! [A,B] : r1_tarski(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f34_nnf,plain,
! [A,B] : r1_tarski(A,A),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [A] : r1_tarski(A,A),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c62,plain,
r1_tarski(X0,X0),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(p5310,plain,
( v1_xboole_0(sk1)
| r1_tarski(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),k19_filter_2(sk0,sk1))
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p5309,c62]) ).
cnf(c9,plain,
( ~ r1_tarski(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),k19_filter_2(sk0,sk1))
| r1_tarski(sk2,sk3) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p5311,plain,
( r1_tarski(sk2,sk3)
| v1_xboole_0(sk1)
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p5310,c9]) ).
cnf(c36,plain,
( ~ v1_xboole_0(X1)
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p154,plain,
( ~ v1_xboole_0(X0)
| ~ m2_filter_2(X0,sk0)
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c36,c1]) ).
cnf(p164,plain,
( ~ v1_xboole_0(X0)
| ~ m2_filter_2(X0,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p154,c2]) ).
cnf(p165,plain,
( v1_xboole_0(sk1)
| v3_struct_0(sk0)
| ~ v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p164,p134]) ).
cnf(p168,plain,
( v1_xboole_0(sk1)
| ~ v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p165]) ).
cnf(p5316,plain,
( v1_xboole_0(sk1)
| v3_struct_0(sk0)
| r1_tarski(sk2,sk3)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p5311,p168]) ).
cnf(p5320,plain,
( v1_xboole_0(sk1)
| r1_tarski(sk2,sk3)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5316]) ).
cnf(p5322,plain,
( r1_tarski(sk2,sk3)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5320]) ).
fof(f36,axiom,
! [A,B,C] :
( ( r1_tarski(B,C)
& r1_tarski(A,B) )
=> r1_tarski(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_xboole_1) ).
fof(f36_nnf,plain,
! [A,B,C] :
( r1_tarski(A,C)
| ~ r1_tarski(B,C)
| ~ r1_tarski(A,B) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [A,B,C] :
( r1_tarski(A,C)
| ~ r1_tarski(B,C)
| ~ r1_tarski(A,B) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c64,plain,
( r1_tarski(X0,X2)
| ~ r1_tarski(X1,X2)
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p5324,plain,
( r1_tarski(sk2,X0)
| ~ r1_tarski(sk3,X0)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p5322,c64]) ).
cnf(c8,plain,
m1_subset_1(sk3,k1_zfmisc_1(u1_struct_0(sk0))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p136,plain,
( m2_filter_2(k19_filter_2(sk0,sk3),sk0)
| v1_xboole_0(sk3)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p133,c8]) ).
cnf(c22,plain,
( r1_tarski(X1,X2)
| X2 != k19_filter_2(X0,X1)
| ~ m2_filter_2(X2,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p105,plain,
( r1_tarski(X0,X1)
| X1 != k19_filter_2(sk0,X0)
| ~ m2_filter_2(X1,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| v1_xboole_0(X0)
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c22,c1]) ).
cnf(p107,plain,
( r1_tarski(X0,X1)
| X1 != k19_filter_2(sk0,X0)
| ~ m2_filter_2(X1,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| v1_xboole_0(X0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p105,c2]) ).
cnf(p111,plain,
( r1_tarski(sk3,X0)
| X0 != k19_filter_2(sk0,sk3)
| ~ m2_filter_2(X0,sk0)
| v1_xboole_0(sk3)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p107,c8]) ).
cnf(p117,plain,
( r1_tarski(sk3,k19_filter_2(sk0,sk3))
| ~ m2_filter_2(k19_filter_2(sk0,sk3),sk0)
| v1_xboole_0(sk3)
| v3_struct_0(sk0) ),
inference(equality_resolution,[status(thm)],[p111]) ).
cnf(p158,plain,
( r1_tarski(sk3,k19_filter_2(sk0,sk3))
| v1_xboole_0(sk3)
| v3_struct_0(sk0)
| v1_xboole_0(sk3)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p136,p117]) ).
cnf(p414,plain,
( r1_tarski(sk3,k19_filter_2(sk0,sk3))
| v1_xboole_0(sk3)
| v1_xboole_0(sk3)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p158]) ).
cnf(p417,plain,
( r1_tarski(sk3,k19_filter_2(sk0,sk3))
| v1_xboole_0(sk3)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p414]) ).
cnf(p5327,plain,
( v1_xboole_0(sk3)
| v3_struct_0(sk0)
| r1_tarski(sk2,k19_filter_2(sk0,sk3))
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p5324,p417]) ).
cnf(p5333,plain,
( v1_xboole_0(sk3)
| r1_tarski(sk2,k19_filter_2(sk0,sk3))
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5327]) ).
cnf(c6,plain,
m1_subset_1(sk2,k1_zfmisc_1(u1_struct_0(sk0))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1583,plain,
( r1_tarski(X0,X1)
| ~ r1_tarski(sk2,X1)
| ~ m2_filter_2(X1,sk0)
| X0 != k19_filter_2(sk0,sk2)
| ~ m2_filter_2(X0,sk0)
| v1_xboole_0(sk2)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p421,c6]) ).
cnf(p1697,plain,
( r1_tarski(k19_filter_2(sk0,sk2),X0)
| ~ r1_tarski(sk2,X0)
| ~ m2_filter_2(X0,sk0)
| ~ m2_filter_2(k19_filter_2(sk0,sk2),sk0)
| v1_xboole_0(sk2)
| v3_struct_0(sk0) ),
inference(equality_resolution,[status(thm)],[p1583]) ).
cnf(p135,plain,
( m2_filter_2(k19_filter_2(sk0,sk2),sk0)
| v1_xboole_0(sk2)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p133,c6]) ).
cnf(p1722,plain,
( v1_xboole_0(sk2)
| v3_struct_0(sk0)
| r1_tarski(k19_filter_2(sk0,sk2),X0)
| ~ r1_tarski(sk2,X0)
| ~ m2_filter_2(X0,sk0)
| v1_xboole_0(sk2)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1697,p135]) ).
cnf(p1723,plain,
( v1_xboole_0(sk2)
| r1_tarski(k19_filter_2(sk0,sk2),X0)
| ~ r1_tarski(sk2,X0)
| ~ m2_filter_2(X0,sk0)
| v1_xboole_0(sk2)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p1722]) ).
cnf(p1725,plain,
( r1_tarski(k19_filter_2(sk0,sk2),X0)
| ~ r1_tarski(sk2,X0)
| ~ m2_filter_2(X0,sk0)
| v1_xboole_0(sk2)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p1723]) ).
cnf(p1728,plain,
( v1_xboole_0(sk3)
| v3_struct_0(sk0)
| r1_tarski(k19_filter_2(sk0,sk2),k19_filter_2(sk0,sk3))
| ~ r1_tarski(sk2,k19_filter_2(sk0,sk3))
| v1_xboole_0(sk2)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1725,p136]) ).
cnf(p1752,plain,
( v1_xboole_0(sk3)
| r1_tarski(k19_filter_2(sk0,sk2),k19_filter_2(sk0,sk3))
| ~ r1_tarski(sk2,k19_filter_2(sk0,sk3))
| v1_xboole_0(sk2)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p1728]) ).
cnf(p5338,plain,
( v1_xboole_0(sk3)
| r1_tarski(k19_filter_2(sk0,sk2),k19_filter_2(sk0,sk3))
| v1_xboole_0(sk2)
| v3_struct_0(sk0)
| v1_xboole_0(sk3)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p5333,p1752]) ).
cnf(p5353,plain,
( v1_xboole_0(sk3)
| r1_tarski(k19_filter_2(sk0,sk2),k19_filter_2(sk0,sk3))
| v1_xboole_0(sk2)
| v1_xboole_0(sk3)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5338]) ).
cnf(p5355,plain,
( r1_tarski(k19_filter_2(sk0,sk2),k19_filter_2(sk0,sk3))
| v1_xboole_0(sk2)
| v1_xboole_0(sk3)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5353]) ).
cnf(c10,plain,
( ~ r1_tarski(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),k19_filter_2(sk0,sk1))
| ~ r1_tarski(k19_filter_2(sk0,sk2),k19_filter_2(sk0,sk3)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p5356,plain,
( ~ r1_tarski(k19_filter_2(sk0,k19_filter_2(sk0,sk1)),k19_filter_2(sk0,sk1))
| v1_xboole_0(sk2)
| v1_xboole_0(sk3)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p5355,c10]) ).
cnf(p5361,plain,
( v1_xboole_0(sk1)
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v3_struct_0(sk0)
| v1_xboole_0(sk2)
| v1_xboole_0(sk3)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p5356,p5310]) ).
cnf(p5362,plain,
( v1_xboole_0(sk1)
| v1_xboole_0(k19_filter_2(sk0,sk1))
| v1_xboole_0(sk2)
| v1_xboole_0(sk3)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5361]) ).
cnf(p5364,plain,
( v1_xboole_0(k19_filter_2(sk0,sk1))
| v1_xboole_0(sk2)
| v1_xboole_0(sk3)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5362]) ).
cnf(p5367,plain,
( v1_xboole_0(sk1)
| v3_struct_0(sk0)
| v1_xboole_0(sk2)
| v1_xboole_0(sk3)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p5364,p168]) ).
cnf(p5371,plain,
( v1_xboole_0(sk1)
| v1_xboole_0(sk2)
| v1_xboole_0(sk3)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5367]) ).
cnf(p5373,plain,
( v1_xboole_0(sk2)
| v1_xboole_0(sk3)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p5371]) ).
cnf(c7,plain,
~ v1_xboole_0(sk3),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p5375,plain,
( v1_xboole_0(sk2)
| v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p5373,c7]) ).
cnf(c5,plain,
~ v1_xboole_0(sk2),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p5376,plain,
( v1_xboole_0(sk1)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p5375,c5]) ).
cnf(c3,plain,
~ v1_xboole_0(sk1),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p5377,plain,
v3_struct_0(sk0),
inference(resolution,[status(thm)],[p5376,c3]) ).
cnf(c0,plain,
~ v3_struct_0(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p5378,plain,
$false,
inference(resolution,[status(thm)],[p5377,c0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT310+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 20:59:58 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 27.71/4.03 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.71/4.03 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------