%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT292+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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 : Sun Sep 27 07:50:03 AM UTC 2026
% Result : Theorem 4.54s 16.09s
% Output : CNFRefutation 4.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 8
% Syntax : Number of formulae : 88 ( 14 unt; 0 def)
% Number of atoms : 477 ( 7 equ)
% Maximal formula atoms : 16 ( 5 avg)
% Number of connectives : 651 ( 262 ~; 320 |; 57 &)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 1 con; 0-1 aty)
% Number of variables : 30 ( 0 sgn 11 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v14_lattices(A)
& v13_lattices(A)
& ~ v3_struct_0(A) )
=> ( v15_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('theBenchmark.p',cc3_lattices) ).
fof(cc5_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v17_lattices(A)
& ~ v3_struct_0(A) )
=> ( v16_lattices(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v11_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('theBenchmark.p',cc5_lattices) ).
fof(cc6_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v16_lattices(A)
& v15_lattices(A)
& v11_lattices(A)
& ~ v3_struct_0(A) )
=> ( v17_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('theBenchmark.p',cc6_lattices) ).
fof(d9_lopclset,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('theBenchmark.p',d9_lopclset) ).
fof(dt_k11_lopclset,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('theBenchmark.p',dt_k11_lopclset) ).
fof(fc4_lopclset,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('theBenchmark.p',fc4_lopclset) ).
fof(t43_lopclset,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('theBenchmark.p',t43_lopclset) ).
fof(t44_lopclset,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('theBenchmark.p',t44_lopclset) ).
fof(t44_lopclset_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(assume_negation,[status(cth)],[t44_lopclset]) ).
cnf(c_113,plain,
( v17_lattices(A)
| ~ v16_lattices(A)
| ~ v15_lattices(A)
| ~ v11_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc6_lattices]) ).
cnf(c_114,plain,
( v16_lattices(A)
| ~ v17_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc5_lattices]) ).
cnf(c_115,plain,
( v15_lattices(A)
| ~ v17_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc5_lattices]) ).
cnf(c_116,plain,
( v14_lattices(A)
| ~ v17_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc5_lattices]) ).
cnf(c_117,plain,
( v13_lattices(A)
| ~ v17_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc5_lattices]) ).
cnf(c_118,plain,
( v11_lattices(A)
| ~ v17_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc5_lattices]) ).
cnf(c_119,plain,
( 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(clausify,[status(thm)],[d9_lopclset]) ).
cnf(c_121,plain,
( v2_pre_topc(k11_lopclset(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k11_lopclset]) ).
cnf(c_122,plain,
( l1_pre_topc(k11_lopclset(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k11_lopclset]) ).
cnf(c_126,plain,
( ~ v3_struct_0(k11_lopclset(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc4_lopclset]) ).
cnf(c_131,plain,
( r1_filter_1(A,k12_lopclset(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t43_lopclset]) ).
fof(nnf_112,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(fof_nnf,[status(thm)],[t44_lopclset_neg]) ).
fof(sk_t44_lopclset_neg,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(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(A,sK0)],[nnf_112]) ).
cnf(c_132,negated_conjecture,
v17_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t44_lopclset_neg]) ).
cnf(c_133,negated_conjecture,
( ~ r1_filter_1(sK0,k6_lopclset(A))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_t44_lopclset_neg]) ).
cnf(c_134,plain,
( ~ v16_lattices(A)
| ~ v15_lattices(A)
| ~ v11_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| v2_pre_topc(k11_lopclset(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_121,c_113]) ).
cnf(c_189,plain,
( v15_lattices(A)
| ~ v14_lattices(A)
| ~ v13_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc3_lattices]) ).
cnf(c_199,negated_conjecture,
( v13_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_132,c_117]) ).
cnf(c_206,negated_conjecture,
( v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| v15_lattices(sK0)
| ~ v14_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_189,c_199]) ).
cnf(c_222,negated_conjecture,
( ~ v16_lattices(A)
| ~ v15_lattices(A)
| ~ v11_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(A)))
| ~ l1_pre_topc(k11_lopclset(A))
| v3_struct_0(k11_lopclset(A)) ),
inference(resolve,[status(thm)],[c_133,c_134]) ).
cnf(c_237,plain,
( ~ v16_lattices(A)
| ~ v15_lattices(A)
| ~ v11_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| r1_filter_1(A,k12_lopclset(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_131,c_113]) ).
cnf(c_238,negated_conjecture,
( v15_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_132,c_115]) ).
cnf(c_559,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t44_lopclset_neg]) ).
cnf(c_560,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t44_lopclset_neg]) ).
cnf(c_561,negated_conjecture,
~ v3_realset2(sK0),
inference(split_conjunct,[status(thm)],[sk_t44_lopclset_neg]) ).
cnf(c_562,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t44_lopclset_neg]) ).
cnf(c_599,negated_conjecture,
( ~ v3_struct_0(k11_lopclset(sK0))
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_132,c_126]) ).
cnf(c_928,negated_conjecture,
( ~ v3_struct_0(k11_lopclset(sK0))
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_559,c_599]) ).
cnf(c_929,negated_conjecture,
( ~ v3_struct_0(k11_lopclset(sK0))
| ~ l3_lattices(sK0)
| v3_realset2(sK0) ),
inference(resolve,[status(thm)],[c_560,c_928]) ).
cnf(c_930,negated_conjecture,
( ~ v3_struct_0(k11_lopclset(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_561,c_929]) ).
cnf(c_600,negated_conjecture,
~ v3_struct_0(k11_lopclset(sK0)),
inference(resolve,[status(thm)],[c_562,c_930]) ).
cnf(c_607,negated_conjecture,
( l1_pre_topc(k11_lopclset(sK0))
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_132,c_122]) ).
cnf(c_931,negated_conjecture,
( l1_pre_topc(k11_lopclset(sK0))
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_559,c_607]) ).
cnf(c_932,negated_conjecture,
( l1_pre_topc(k11_lopclset(sK0))
| ~ l3_lattices(sK0)
| v3_realset2(sK0) ),
inference(resolve,[status(thm)],[c_560,c_931]) ).
cnf(c_933,negated_conjecture,
( l1_pre_topc(k11_lopclset(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_561,c_932]) ).
cnf(c_608,negated_conjecture,
l1_pre_topc(k11_lopclset(sK0)),
inference(resolve,[status(thm)],[c_562,c_933]) ).
cnf(c_609,negated_conjecture,
( k12_lopclset(sK0) = k6_lopclset(k11_lopclset(sK0))
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_132,c_119]) ).
cnf(c_934,negated_conjecture,
( k12_lopclset(sK0) = k6_lopclset(k11_lopclset(sK0))
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_559,c_609]) ).
cnf(c_935,negated_conjecture,
( k12_lopclset(sK0) = k6_lopclset(k11_lopclset(sK0))
| ~ l3_lattices(sK0)
| v3_realset2(sK0) ),
inference(resolve,[status(thm)],[c_560,c_934]) ).
cnf(c_936,negated_conjecture,
( k12_lopclset(sK0) = k6_lopclset(k11_lopclset(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_561,c_935]) ).
cnf(c_610,negated_conjecture,
k12_lopclset(sK0) = k6_lopclset(k11_lopclset(sK0)),
inference(resolve,[status(thm)],[c_562,c_936]) ).
cnf(c_611,negated_conjecture,
( v16_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_132,c_114]) ).
cnf(c_937,negated_conjecture,
( v16_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_562,c_611]) ).
cnf(c_612,negated_conjecture,
v16_lattices(sK0),
inference(resolve,[status(thm)],[c_559,c_937]) ).
cnf(c_613,negated_conjecture,
( v14_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_132,c_116]) ).
cnf(c_938,negated_conjecture,
( v14_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_562,c_613]) ).
cnf(c_614,negated_conjecture,
v14_lattices(sK0),
inference(resolve,[status(thm)],[c_559,c_938]) ).
cnf(c_615,negated_conjecture,
( v11_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_132,c_118]) ).
cnf(c_939,negated_conjecture,
( v11_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_562,c_615]) ).
cnf(c_616,negated_conjecture,
v11_lattices(sK0),
inference(resolve,[status(thm)],[c_559,c_939]) ).
cnf(c_806,negated_conjecture,
( v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ v14_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0))
| v3_struct_0(k11_lopclset(sK0)) ),
inference(resolve,[status(thm)],[c_222,c_206]) ).
cnf(c_940,negated_conjecture,
( v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ v14_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0))
| v3_struct_0(k11_lopclset(sK0)) ),
inference(copy,[status(thm)],[c_806]) ).
cnf(c_941,negated_conjecture,
( v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ v14_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0))
| v3_struct_0(k11_lopclset(sK0)) ),
inference(copy,[status(thm)],[c_940]) ).
cnf(c_942,negated_conjecture,
( v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ v14_lattices(sK0)
| v3_struct_0(sK0)
| ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0))
| v3_struct_0(k11_lopclset(sK0)) ),
inference(copy,[status(thm)],[c_941]) ).
cnf(c_943,negated_conjecture,
( v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ v14_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0))
| v3_struct_0(k11_lopclset(sK0)) ),
inference(copy,[status(thm)],[c_942]) ).
cnf(c_944,negated_conjecture,
( v3_struct_0(sK0)
| ~ v14_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0))
| v3_struct_0(k11_lopclset(sK0)) ),
inference(copy,[status(thm)],[c_943]) ).
cnf(c_945,negated_conjecture,
( ~ v14_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0))
| v3_struct_0(k11_lopclset(sK0)) ),
inference(copy,[status(thm)],[c_944]) ).
cnf(c_946,negated_conjecture,
( ~ v14_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| ~ l1_pre_topc(k11_lopclset(sK0)) ),
inference(resolve,[status(thm)],[c_600,c_945]) ).
cnf(c_947,negated_conjecture,
( ~ v14_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0))) ),
inference(resolve,[status(thm)],[c_608,c_946]) ).
cnf(c_948,negated_conjecture,
( ~ v14_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0))) ),
inference(resolve,[status(thm)],[c_559,c_947]) ).
cnf(c_949,negated_conjecture,
( ~ v14_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0))) ),
inference(resolve,[status(thm)],[c_560,c_948]) ).
cnf(c_950,negated_conjecture,
( ~ v14_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0))) ),
inference(resolve,[status(thm)],[c_561,c_949]) ).
cnf(c_951,negated_conjecture,
( ~ v14_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0))) ),
inference(resolve,[status(thm)],[c_562,c_950]) ).
cnf(c_952,negated_conjecture,
( ~ v14_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0))) ),
inference(resolve,[status(thm)],[c_616,c_951]) ).
cnf(c_953,negated_conjecture,
( ~ v14_lattices(sK0)
| ~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0))) ),
inference(resolve,[status(thm)],[c_612,c_952]) ).
cnf(c_807,negated_conjecture,
~ r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0))),
inference(resolve,[status(thm)],[c_614,c_953]) ).
cnf(c_926,negated_conjecture,
( ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| r1_filter_1(sK0,k12_lopclset(sK0))
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_238,c_237]) ).
cnf(c_954,negated_conjecture,
( ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(paramod,[status(thm)],[c_610,c_926]) ).
cnf(c_955,negated_conjecture,
( ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(copy,[status(thm)],[c_954]) ).
cnf(c_956,negated_conjecture,
( ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(copy,[status(thm)],[c_955]) ).
cnf(c_957,negated_conjecture,
( ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| v3_struct_0(sK0)
| r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(copy,[status(thm)],[c_956]) ).
cnf(c_958,negated_conjecture,
( ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(copy,[status(thm)],[c_957]) ).
cnf(c_959,negated_conjecture,
( ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| v3_realset2(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_562,c_958]) ).
cnf(c_960,negated_conjecture,
( ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| v3_realset2(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_559,c_959]) ).
cnf(c_961,negated_conjecture,
( ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0)))
| v3_realset2(sK0) ),
inference(resolve,[status(thm)],[c_560,c_960]) ).
cnf(c_962,negated_conjecture,
( ~ v16_lattices(sK0)
| ~ v11_lattices(sK0)
| r1_filter_1(sK0,k6_lopclset(k11_lopclset(sK0))) ),
inference(resolve,[status(thm)],[c_561,c_961]) ).
cnf(c_963,negated_conjecture,
( ~ v16_lattices(sK0)
| ~ v11_lattices(sK0) ),
inference(resolve,[status(thm)],[c_807,c_962]) ).
cnf(c_964,negated_conjecture,
~ v16_lattices(sK0),
inference(resolve,[status(thm)],[c_616,c_963]) ).
cnf(c_927,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_612,c_964]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LAT292+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.04/15.45 % CPULimit : 300
% 0.04/15.45 % WCLimit : 300
% 0.04/15.45 % DateTime : Fri Sep 25 20:31:10 UTC 2026
% 0.04/15.45 % CPUTime :
% 0.04/15.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.04/15.45 % Process 2927475 was started by sandbox2 on n012,
% 0.04/15.45 % Fri Sep 25 20:31:10 2026
% 0.04/15.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.04/15.47
% 0.04/15.47 % From the command line: assign(max_seconds, 300).
% 4.54/16.09
% 4.54/16.09 % SZS status Theorem for theBenchmark
% 4.54/16.09
% 4.54/16.09 % Proof 1 at 0.60 (+ 0.01) seconds.
% 4.54/16.09 % Length of proof is 48.
% 4.54/16.09 % Level of proof is 6.
% 4.54/16.09 % Maximum clause weight is 12.000.
% 4.54/16.09 % Given clauses 0.
% 4.54/16.09
% 4.54/16.09 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------