%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT327+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 : n026.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:50 PM UTC 2026
% Result : Theorem 8.41s 1.94s
% Output : Proof 8.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 4
% Syntax : Number of formulae : 63 ( 8 unt; 0 def)
% Number of atoms : 322 ( 0 equ)
% Maximal formula atoms : 13 ( 5 avg)
% Number of connectives : 415 ( 156 ~; 192 |; 50 &)
% ( 1 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 13 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-3 aty)
% Number of variables : 74 ( 1 sgn 30 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f42,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ( r3_lattices(A,B,C)
=> ( r2_hidden(D,k22_filter_2(A,B,C))
<=> ( r3_lattices(A,D,C)
& r3_lattices(A,B,D) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t63_filter_2) ).
fof(f42_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( ( ~ r3_lattices(A,D,C)
| ~ r3_lattices(A,B,D)
| r2_hidden(D,k22_filter_2(A,B,C)) )
& ( ( r3_lattices(A,D,C)
& r3_lattices(A,B,D) )
| ~ r2_hidden(D,k22_filter_2(A,B,C)) ) )
| ~ r3_lattices(A,B,C)
| ~ m1_subset_1(D,u1_struct_0(A)) )
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [A,B,C,D] :
( ( ( ~ r3_lattices(A,D,C)
| ~ r3_lattices(A,B,D)
| r2_hidden(D,k22_filter_2(A,B,C)) )
& ( ( r3_lattices(A,D,C)
& r3_lattices(A,B,D) )
| ~ r2_hidden(D,k22_filter_2(A,B,C)) ) )
| ~ r3_lattices(A,B,C)
| ~ m1_subset_1(D,u1_struct_0(A))
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c66,plain,
( ~ r3_lattices(X0,X3,X2)
| ~ r3_lattices(X0,X1,X3)
| r2_hidden(X3,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p211,plain,
( ~ r3_lattices(X0,X2,X2)
| ~ r3_lattices(X0,X1,X2)
| r2_hidden(X2,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(factoring,[status(thm)],[c66]) ).
cnf(p369,plain,
( ~ r3_lattices(X0,X2,X2)
| r2_hidden(X2,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(factoring,[status(thm)],[p211]) ).
fof(f0,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r3_lattices(A,B,C)
=> ( r2_hidden(C,k22_filter_2(A,B,C))
& r2_hidden(B,k22_filter_2(A,B,C)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t64_filter_2) ).
fof(f0_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r3_lattices(A,B,C)
=> ( r2_hidden(C,k22_filter_2(A,B,C))
& r2_hidden(B,k22_filter_2(A,B,C)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ~ r2_hidden(C,k22_filter_2(A,B,C))
| ~ r2_hidden(B,k22_filter_2(A,B,C)) )
& r3_lattices(A,B,C)
& m1_subset_1(C,u1_struct_0(A)) )
& m1_subset_1(B,u1_struct_0(A)) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
( ( ~ r2_hidden(sk2,k22_filter_2(sk0,sk1,sk2))
| ~ r2_hidden(sk1,k22_filter_2(sk0,sk1,sk2)) )
& r3_lattices(sk0,sk1,sk2)
& m1_subset_1(sk2,u1_struct_0(sk0))
& m1_subset_1(sk1,u1_struct_0(sk0))
& l3_lattices(sk0)
& v10_lattices(sk0)
& ~ v3_struct_0(sk0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f0_nnf]) ).
cnf(c1,plain,
v10_lattices(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p824,plain,
( ~ r3_lattices(sk0,X1,X1)
| r2_hidden(X1,k22_filter_2(sk0,X0,X1))
| ~ r3_lattices(sk0,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sk0))
| ~ m1_subset_1(X0,u1_struct_0(sk0))
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p369,c1]) ).
cnf(c2,plain,
l3_lattices(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4503,plain,
( ~ r3_lattices(sk0,X1,X1)
| r2_hidden(X1,k22_filter_2(sk0,X0,X1))
| ~ r3_lattices(sk0,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sk0))
| ~ m1_subset_1(X0,u1_struct_0(sk0))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p824,c2]) ).
cnf(c3,plain,
m1_subset_1(sk1,u1_struct_0(sk0)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4703,plain,
( ~ r3_lattices(sk0,X0,X0)
| r2_hidden(X0,k22_filter_2(sk0,sk1,X0))
| ~ r3_lattices(sk0,sk1,X0)
| ~ m1_subset_1(X0,u1_struct_0(sk0))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p4503,c3]) ).
cnf(c4,plain,
m1_subset_1(sk2,u1_struct_0(sk0)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4741,plain,
( ~ r3_lattices(sk0,sk2,sk2)
| r2_hidden(sk2,k22_filter_2(sk0,sk1,sk2))
| ~ r3_lattices(sk0,sk1,sk2)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p4703,c4]) ).
cnf(c5,plain,
r3_lattices(sk0,sk1,sk2),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4779,plain,
( ~ r3_lattices(sk0,sk2,sk2)
| r2_hidden(sk2,k22_filter_2(sk0,sk1,sk2))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p4741,c5]) ).
fof(f31,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l3_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> r3_lattices(A,B,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r3_lattices) ).
fof(f31_nnf,plain,
! [A,B,C] :
( r3_lattices(A,B,B)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [A,B,C] :
( r3_lattices(A,B,B)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c44,plain,
( r3_lattices(X0,X1,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v9_lattices(X0)
| ~ v8_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p136,plain,
( r3_lattices(X0,X1,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v9_lattices(X0)
| ~ v8_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0) ),
inference(factoring,[status(thm)],[c44]) ).
fof(f39,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_lattices) ).
fof(f39_nnf,plain,
! [A] :
( ( v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) )
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [A] :
( ( v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) )
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c58,plain,
( v6_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p170,plain,
( v6_lattices(sk0)
| ~ v10_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c58,c2]) ).
cnf(p172,plain,
( v6_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p170,c1]) ).
cnf(p285,plain,
( v3_struct_0(sk0)
| r3_lattices(sk0,X0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sk0))
| ~ l3_lattices(sk0)
| ~ v9_lattices(sk0)
| ~ v8_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p136,p172]) ).
cnf(p287,plain,
( r3_lattices(sk0,X0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sk0))
| ~ l3_lattices(sk0)
| ~ v9_lattices(sk0)
| ~ v8_lattices(sk0)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p285]) ).
cnf(c60,plain,
( v8_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p184,plain,
( v8_lattices(sk0)
| ~ v10_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c60,c2]) ).
cnf(p186,plain,
( v8_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p184,c1]) ).
cnf(p288,plain,
( v3_struct_0(sk0)
| r3_lattices(sk0,X0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sk0))
| ~ l3_lattices(sk0)
| ~ v9_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p287,p186]) ).
cnf(p289,plain,
( r3_lattices(sk0,X0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sk0))
| ~ l3_lattices(sk0)
| ~ v9_lattices(sk0)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p288]) ).
cnf(c61,plain,
( v9_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p189,plain,
( v9_lattices(sk0)
| ~ v10_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c61,c2]) ).
cnf(p191,plain,
( v9_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p189,c1]) ).
cnf(p290,plain,
( v3_struct_0(sk0)
| r3_lattices(sk0,X0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sk0))
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p289,p191]) ).
cnf(p291,plain,
( r3_lattices(sk0,X0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sk0))
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p290]) ).
cnf(p292,plain,
( r3_lattices(sk0,X0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sk0))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p291,c2]) ).
cnf(p294,plain,
( r3_lattices(sk0,sk2,sk2)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p292,c4]) ).
cnf(p4780,plain,
( v3_struct_0(sk0)
| r2_hidden(sk2,k22_filter_2(sk0,sk1,sk2))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p4779,p294]) ).
cnf(p4781,plain,
( r2_hidden(sk2,k22_filter_2(sk0,sk1,sk2))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p4780]) ).
cnf(p210,plain,
( ~ r3_lattices(X0,X1,X2)
| ~ r3_lattices(X0,X1,X1)
| r2_hidden(X1,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(factoring,[status(thm)],[c66]) ).
cnf(p361,plain,
( ~ r3_lattices(X0,X1,X1)
| r2_hidden(X1,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(factoring,[status(thm)],[p210]) ).
cnf(p819,plain,
( ~ r3_lattices(sk0,X0,X0)
| r2_hidden(X0,k22_filter_2(sk0,X0,X1))
| ~ r3_lattices(sk0,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sk0))
| ~ m1_subset_1(X0,u1_struct_0(sk0))
| ~ l3_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p361,c1]) ).
cnf(p4464,plain,
( ~ r3_lattices(sk0,X0,X0)
| r2_hidden(X0,k22_filter_2(sk0,X0,X1))
| ~ r3_lattices(sk0,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sk0))
| ~ m1_subset_1(X0,u1_struct_0(sk0))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p819,c2]) ).
cnf(p4465,plain,
( ~ r3_lattices(sk0,sk1,sk1)
| r2_hidden(sk1,k22_filter_2(sk0,sk1,X0))
| ~ r3_lattices(sk0,sk1,X0)
| ~ m1_subset_1(X0,u1_struct_0(sk0))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p4464,c3]) ).
cnf(p4504,plain,
( ~ r3_lattices(sk0,sk1,sk1)
| r2_hidden(sk1,k22_filter_2(sk0,sk1,sk2))
| ~ r3_lattices(sk0,sk1,sk2)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p4465,c4]) ).
cnf(p4541,plain,
( ~ r3_lattices(sk0,sk1,sk1)
| r2_hidden(sk1,k22_filter_2(sk0,sk1,sk2))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p4504,c5]) ).
cnf(p293,plain,
( r3_lattices(sk0,sk1,sk1)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p292,c3]) ).
cnf(p4542,plain,
( v3_struct_0(sk0)
| r2_hidden(sk1,k22_filter_2(sk0,sk1,sk2))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p4541,p293]) ).
cnf(p4543,plain,
( r2_hidden(sk1,k22_filter_2(sk0,sk1,sk2))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p4542]) ).
cnf(c6,plain,
( ~ r2_hidden(sk2,k22_filter_2(sk0,sk1,sk2))
| ~ r2_hidden(sk1,k22_filter_2(sk0,sk1,sk2)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4583,plain,
( ~ r2_hidden(sk2,k22_filter_2(sk0,sk1,sk2))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p4543,c6]) ).
cnf(p4785,plain,
( v3_struct_0(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p4781,p4583]) ).
cnf(p4790,plain,
v3_struct_0(sk0),
inference(factoring,[status(thm)],[p4785]) ).
cnf(c0,plain,
~ v3_struct_0(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p4791,plain,
$false,
inference(resolution,[status(thm)],[p4790,c0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT327+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 21:10:09 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 8.41/1.94 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.41/1.94 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------