%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT292+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 : 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 : Fri Sep 25 01:56:40 PM UTC 2026
% Result : Theorem 26.02s 4.17s
% Output : Proof 26.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 5
% Syntax : Number of formulae : 57 ( 7 unt; 0 def)
% Number of atoms : 277 ( 7 equ)
% Maximal formula atoms : 9 ( 4 avg)
% Number of connectives : 319 ( 99 ~; 162 |; 52 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 1 con; 0-1 aty)
% Number of variables : 25 ( 0 sgn 16 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f106,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> r1_filter_1(A,k12_lopclset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t43_lopclset) ).
fof(f106_nnf,plain,
! [A] :
( r1_filter_1(A,k12_lopclset(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f106]) ).
fof(f106_sk,plain,
! [A] :
( r1_filter_1(A,k12_lopclset(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f106_nnf]) ).
cnf(c311,plain,
( r1_filter_1(X0,k12_lopclset(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f106_sk]) ).
fof(f0,conjecture,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ? [B] :
( r1_filter_1(A,k6_lopclset(B))
& l1_pre_topc(B)
& v2_pre_topc(B)
& ~ v3_struct_0(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t44_lopclset) ).
fof(f0_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ? [B] :
( r1_filter_1(A,k6_lopclset(B))
& l1_pre_topc(B)
& v2_pre_topc(B)
& ~ v3_struct_0(B) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A] :
( ! [B] :
( ~ r1_filter_1(A,k6_lopclset(B))
| ~ l1_pre_topc(B)
| ~ v2_pre_topc(B)
| v3_struct_0(B) )
& l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
! [B] :
( ( ~ r1_filter_1(sk0,k6_lopclset(B))
| ~ l1_pre_topc(B)
| ~ v2_pre_topc(B)
| v3_struct_0(B) )
& l3_lattices(sk0)
& ~ v3_realset2(sk0)
& v17_lattices(sk0)
& v10_lattices(sk0)
& ~ v3_struct_0(sk0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f0_nnf]) ).
cnf(c1,plain,
v10_lattices(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1474,plain,
( r1_filter_1(sk0,k12_lopclset(sk0))
| ~ l3_lattices(sk0)
| v3_realset2(sk0)
| ~ v17_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c311,c1]) ).
cnf(c2,plain,
v17_lattices(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1489,plain,
( r1_filter_1(sk0,k12_lopclset(sk0))
| ~ l3_lattices(sk0)
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1474,c2]) ).
cnf(c4,plain,
l3_lattices(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1490,plain,
( r1_filter_1(sk0,k12_lopclset(sk0))
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1489,c4]) ).
fof(f36,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k12_lopclset(A) = k6_lopclset(k11_lopclset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_lopclset) ).
fof(f36_nnf,plain,
! [A] :
( k12_lopclset(A) = k6_lopclset(k11_lopclset(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [A] :
( k12_lopclset(A) = k6_lopclset(k11_lopclset(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c96,plain,
( k12_lopclset(X0) = k6_lopclset(k11_lopclset(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p614,plain,
( k12_lopclset(sk0) = k6_lopclset(k11_lopclset(sk0))
| ~ l3_lattices(sk0)
| v3_realset2(sk0)
| ~ v17_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c96,c1]) ).
cnf(p621,plain,
( k12_lopclset(sk0) = k6_lopclset(k11_lopclset(sk0))
| ~ l3_lattices(sk0)
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p614,c2]) ).
cnf(p622,plain,
( k12_lopclset(sk0) = k6_lopclset(k11_lopclset(sk0))
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p621,c4]) ).
fof(f39,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( l1_pre_topc(k11_lopclset(A))
& v2_pre_topc(k11_lopclset(A))
& v1_pre_topc(k11_lopclset(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_lopclset) ).
fof(f39_nnf,plain,
! [A] :
( ( l1_pre_topc(k11_lopclset(A))
& v2_pre_topc(k11_lopclset(A))
& v1_pre_topc(k11_lopclset(A)) )
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [A] :
( ( l1_pre_topc(k11_lopclset(A))
& v2_pre_topc(k11_lopclset(A))
& v1_pre_topc(k11_lopclset(A)) )
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c103,plain,
( l1_pre_topc(k11_lopclset(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p720,plain,
( l1_pre_topc(k11_lopclset(sk0))
| ~ l3_lattices(sk0)
| v3_realset2(sk0)
| ~ v17_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c103,c1]) ).
cnf(p727,plain,
( l1_pre_topc(k11_lopclset(sk0))
| ~ l3_lattices(sk0)
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p720,c2]) ).
cnf(p728,plain,
( l1_pre_topc(k11_lopclset(sk0))
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p727,c4]) ).
cnf(c102,plain,
( v2_pre_topc(k11_lopclset(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p709,plain,
( v2_pre_topc(k11_lopclset(sk0))
| ~ l3_lattices(sk0)
| v3_realset2(sk0)
| ~ v17_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c102,c1]) ).
cnf(p716,plain,
( v2_pre_topc(k11_lopclset(sk0))
| ~ l3_lattices(sk0)
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p709,c2]) ).
cnf(p717,plain,
( v2_pre_topc(k11_lopclset(sk0))
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p716,c4]) ).
cnf(c5,plain,
( ~ r1_filter_1(sk0,k6_lopclset(X1))
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| v3_struct_0(X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p718,plain,
( ~ r1_filter_1(sk0,k6_lopclset(k11_lopclset(sk0)))
| ~ l1_pre_topc(k11_lopclset(sk0))
| v3_struct_0(k11_lopclset(sk0))
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p717,c5]) ).
cnf(p732,plain,
( ~ r1_filter_1(sk0,k6_lopclset(k11_lopclset(sk0)))
| v3_struct_0(k11_lopclset(sk0))
| v3_realset2(sk0)
| v3_struct_0(sk0)
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p728,p718]) ).
cnf(p1070,plain,
( ~ r1_filter_1(sk0,k6_lopclset(k11_lopclset(sk0)))
| v3_struct_0(k11_lopclset(sk0))
| v3_realset2(sk0)
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p732]) ).
cnf(p1080,plain,
( ~ r1_filter_1(sk0,k6_lopclset(k11_lopclset(sk0)))
| v3_struct_0(k11_lopclset(sk0))
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p1070]) ).
cnf(p1081,plain,
( ~ r1_filter_1(sk0,k12_lopclset(sk0))
| v3_struct_0(k11_lopclset(sk0))
| v3_realset2(sk0)
| v3_struct_0(sk0)
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(superposition,[status(thm)],[p622,p1080]) ).
cnf(p1082,plain,
( ~ r1_filter_1(sk0,k12_lopclset(sk0))
| v3_struct_0(k11_lopclset(sk0))
| v3_realset2(sk0)
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p1081]) ).
cnf(p1084,plain,
( ~ r1_filter_1(sk0,k12_lopclset(sk0))
| v3_struct_0(k11_lopclset(sk0))
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p1082]) ).
cnf(p1491,plain,
( v3_struct_0(k11_lopclset(sk0))
| v3_realset2(sk0)
| v3_struct_0(sk0)
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1490,p1084]) ).
cnf(p1492,plain,
( v3_struct_0(k11_lopclset(sk0))
| v3_realset2(sk0)
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p1491]) ).
cnf(p1498,plain,
( v3_struct_0(k11_lopclset(sk0))
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p1492]) ).
fof(f73,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v2_pre_topc(k11_lopclset(A))
& v1_pre_topc(k11_lopclset(A))
& ~ v3_struct_0(k11_lopclset(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_lopclset) ).
fof(f73_nnf,plain,
! [A] :
( ( v2_pre_topc(k11_lopclset(A))
& v1_pre_topc(k11_lopclset(A))
& ~ v3_struct_0(k11_lopclset(A)) )
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f73]) ).
fof(f73_sk,plain,
! [A] :
( ( v2_pre_topc(k11_lopclset(A))
& v1_pre_topc(k11_lopclset(A))
& ~ v3_struct_0(k11_lopclset(A)) )
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f73_nnf]) ).
cnf(c154,plain,
( ~ v3_struct_0(k11_lopclset(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f73_sk]) ).
cnf(p1053,plain,
( ~ v3_struct_0(k11_lopclset(sk0))
| ~ l3_lattices(sk0)
| v3_realset2(sk0)
| ~ v17_lattices(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c154,c1]) ).
cnf(p1062,plain,
( ~ v3_struct_0(k11_lopclset(sk0))
| ~ l3_lattices(sk0)
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1053,c2]) ).
cnf(p1063,plain,
( ~ v3_struct_0(k11_lopclset(sk0))
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1062,c4]) ).
cnf(p1499,plain,
( v3_realset2(sk0)
| v3_struct_0(sk0)
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1498,p1063]) ).
cnf(p1500,plain,
( v3_realset2(sk0)
| v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p1499]) ).
cnf(p1502,plain,
( v3_realset2(sk0)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p1500]) ).
cnf(c3,plain,
~ v3_realset2(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1504,plain,
v3_struct_0(sk0),
inference(resolution,[status(thm)],[p1502,c3]) ).
cnf(c0,plain,
~ v3_struct_0(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1505,plain,
$false,
inference(resolution,[status(thm)],[p1504,c0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT292+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.34 % Computer : n005.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 : Wed Sep 23 20:53:02 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 26.02/4.17 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.02/4.17 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------