%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT346+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 : n012.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:20 AM UTC 2026
% Result : Theorem 2.72s 0.75s
% Output : CNFRefutation 2.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 11
% Syntax : Number of formulae : 75 ( 17 unt; 0 def)
% Number of atoms : 264 ( 0 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 299 ( 110 ~; 127 |; 47 &)
% ( 1 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 18 ( 17 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 1 con; 0-1 aty)
% Number of variables : 32 ( 0 sgn 14 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d5_lattice4,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l3_lattices(B)
& v10_lattices(B)
& ~ v3_struct_0(B) )
=> ( r1_filter_1(A,B)
<=> ? [C] :
( v3_lattice4(C,A,B)
& m1_lattice4(C,A,B) ) ) ) ),
file('theBenchmark.p',d5_lattice4) ).
fof(dt_k10_conlat_2,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> m1_lattice4(k10_conlat_2(A),k1_lattice2(k11_conlat_1(A)),k11_conlat_1(k7_conlat_2(A))) ),
file('theBenchmark.p',dt_k10_conlat_2) ).
fof(dt_k11_conlat_1,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( l3_lattices(k11_conlat_1(A))
& v3_lattices(k11_conlat_1(A))
& ~ v3_struct_0(k11_conlat_1(A)) ) ),
file('theBenchmark.p',dt_k11_conlat_1) ).
fof(dt_k1_lattice2,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('theBenchmark.p',dt_k1_lattice2) ).
fof(dt_k7_conlat_2,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( l2_conlat_1(k7_conlat_2(A))
& v4_conlat_1(k7_conlat_2(A))
& ~ v3_conlat_1(k7_conlat_2(A)) ) ),
file('theBenchmark.p',dt_k7_conlat_2) ).
fof(fc1_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc1_lattice2) ).
fof(fc5_conlat_1,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( v4_lattice3(k11_conlat_1(A))
& v10_lattices(k11_conlat_1(A))
& v9_lattices(k11_conlat_1(A))
& v8_lattices(k11_conlat_1(A))
& v7_lattices(k11_conlat_1(A))
& v6_lattices(k11_conlat_1(A))
& v5_lattices(k11_conlat_1(A))
& v4_lattices(k11_conlat_1(A))
& v3_lattices(k11_conlat_1(A))
& ~ v3_struct_0(k11_conlat_1(A)) ) ),
file('theBenchmark.p',fc5_conlat_1) ).
fof(fc6_lattice2,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('theBenchmark.p',fc6_lattice2) ).
fof(symmetry_r1_filter_1,axiom,
! [A,B] :
( ( l3_lattices(B)
& v10_lattices(B)
& ~ v3_struct_0(B)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( r1_filter_1(A,B)
=> r1_filter_1(B,A) ) ),
file('theBenchmark.p',symmetry_r1_filter_1) ).
fof(t21_conlat_2,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> v3_lattice4(k10_conlat_2(A),k1_lattice2(k11_conlat_1(A)),k11_conlat_1(k7_conlat_2(A))) ),
file('theBenchmark.p',t21_conlat_2) ).
fof(t22_conlat_2,conjecture,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> r1_filter_1(k11_conlat_1(k7_conlat_2(A)),k1_lattice2(k11_conlat_1(A))) ),
file('theBenchmark.p',t22_conlat_2) ).
fof(t22_conlat_2_neg,negated_conjecture,
~ ! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> r1_filter_1(k11_conlat_1(k7_conlat_2(A)),k1_lattice2(k11_conlat_1(A))) ),
inference(assume_negation,[status(cth)],[t22_conlat_2]) ).
cnf(c_151,plain,
( m1_lattice4(k10_conlat_2(A),k1_lattice2(k11_conlat_1(A)),k11_conlat_1(k7_conlat_2(A)))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k10_conlat_2]) ).
cnf(c_152,plain,
( ~ v3_lattice4(C,A,B)
| ~ m1_lattice4(C,A,B)
| r1_filter_1(A,B)
| ~ l3_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d5_lattice4]) ).
fof(nnf_101,plain,
? [A] :
( ~ r1_filter_1(k11_conlat_1(k7_conlat_2(A)),k1_lattice2(k11_conlat_1(A)))
& l2_conlat_1(A)
& ~ v3_conlat_1(A) ),
inference(fof_nnf,[status(thm)],[t22_conlat_2_neg]) ).
fof(sk_t22_conlat_2_neg,plain,
( ~ r1_filter_1(k11_conlat_1(k7_conlat_2(sK0)),k1_lattice2(k11_conlat_1(sK0)))
& l2_conlat_1(sK0)
& ~ v3_conlat_1(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(A,sK0)],[nnf_101]) ).
cnf(c_244,negated_conjecture,
~ r1_filter_1(k11_conlat_1(k7_conlat_2(sK0)),k1_lattice2(k11_conlat_1(sK0))),
inference(split_conjunct,[status(thm)],[sk_t22_conlat_2_neg]) ).
cnf(c_245,negated_conjecture,
l2_conlat_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t22_conlat_2_neg]) ).
cnf(c_246,negated_conjecture,
~ v3_conlat_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t22_conlat_2_neg]) ).
cnf(c_253,plain,
( v3_lattice4(k10_conlat_2(A),k1_lattice2(k11_conlat_1(A)),k11_conlat_1(k7_conlat_2(A)))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[t21_conlat_2]) ).
cnf(c_255,plain,
( r1_filter_1(B,A)
| ~ r1_filter_1(A,B)
| ~ l3_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[symmetry_r1_filter_1]) ).
cnf(c_303,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_311,plain,
( v10_lattices(k11_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[fc5_conlat_1]) ).
cnf(c_317,plain,
( ~ v3_struct_0(k11_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[fc5_conlat_1]) ).
cnf(c_326,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_335,plain,
( l2_conlat_1(k7_conlat_2(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k7_conlat_2]) ).
cnf(c_336,plain,
( ~ v3_conlat_1(k7_conlat_2(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k7_conlat_2]) ).
cnf(c_338,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_339,plain,
( l3_lattices(k11_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k11_conlat_1]) ).
cnf(c_376,plain,
( ~ l2_conlat_1(A)
| v3_conlat_1(A)
| ~ v3_lattice4(k10_conlat_2(A),k1_lattice2(k11_conlat_1(A)),k11_conlat_1(k7_conlat_2(A)))
| r1_filter_1(k1_lattice2(k11_conlat_1(A)),k11_conlat_1(k7_conlat_2(A)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(A)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(A)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(A)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(A)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(A)))
| v3_struct_0(k1_lattice2(k11_conlat_1(A))) ),
inference(resolve,[status(thm)],[c_152,c_151]) ).
cnf(c_5178,negated_conjecture,
( v3_lattice4(k10_conlat_2(sK0),k1_lattice2(k11_conlat_1(sK0)),k11_conlat_1(k7_conlat_2(sK0)))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_253,c_245]) ).
cnf(c_448,negated_conjecture,
v3_lattice4(k10_conlat_2(sK0),k1_lattice2(k11_conlat_1(sK0)),k11_conlat_1(k7_conlat_2(sK0))),
inference(resolve,[status(thm)],[c_246,c_5178]) ).
cnf(c_5179,negated_conjecture,
( v10_lattices(k11_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_311,c_245]) ).
cnf(c_527,negated_conjecture,
v10_lattices(k11_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_246,c_5179]) ).
cnf(c_5180,negated_conjecture,
( ~ v3_struct_0(k11_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_317,c_245]) ).
cnf(c_545,negated_conjecture,
~ v3_struct_0(k11_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_246,c_5180]) ).
cnf(c_5181,negated_conjecture,
( l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_335,c_245]) ).
cnf(c_594,negated_conjecture,
l2_conlat_1(k7_conlat_2(sK0)),
inference(resolve,[status(thm)],[c_246,c_5181]) ).
cnf(c_5182,negated_conjecture,
( l3_lattices(k11_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_339,c_245]) ).
cnf(c_605,negated_conjecture,
l3_lattices(k11_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_246,c_5182]) ).
cnf(c_5183,plain,
( ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0)
| r1_filter_1(k1_lattice2(k11_conlat_1(sK0)),k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK0)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK0)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK0))) ),
inference(resolve,[status(thm)],[c_448,c_376]) ).
cnf(c_5184,negated_conjecture,
( ~ l2_conlat_1(sK0)
| r1_filter_1(k1_lattice2(k11_conlat_1(sK0)),k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK0)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK0)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK0))) ),
inference(resolve,[status(thm)],[c_246,c_5183]) ).
cnf(c_848,negated_conjecture,
( r1_filter_1(k1_lattice2(k11_conlat_1(sK0)),k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK0)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK0)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK0))) ),
inference(resolve,[status(thm)],[c_245,c_5184]) ).
cnf(c_5185,plain,
( v10_lattices(k1_lattice2(k11_conlat_1(sK0)))
| ~ l3_lattices(k11_conlat_1(sK0))
| v3_struct_0(k11_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_527,c_303]) ).
cnf(c_5186,plain,
( v10_lattices(k1_lattice2(k11_conlat_1(sK0)))
| ~ l3_lattices(k11_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_545,c_5185]) ).
cnf(c_907,plain,
v10_lattices(k1_lattice2(k11_conlat_1(sK0))),
inference(resolve,[status(thm)],[c_605,c_5186]) ).
cnf(c_912,negated_conjecture,
( r1_filter_1(k1_lattice2(k11_conlat_1(sK0)),k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK0)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK0))) ),
inference(resolve,[status(thm)],[c_907,c_848]) ).
cnf(c_973,plain,
( l3_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| v3_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_594,c_339]) ).
cnf(c_975,plain,
( ~ v3_struct_0(k11_conlat_1(k7_conlat_2(sK0)))
| v3_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_594,c_317]) ).
cnf(c_981,plain,
( v10_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| v3_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_594,c_311]) ).
cnf(c_1055,plain,
l3_lattices(k1_lattice2(k11_conlat_1(sK0))),
inference(resolve,[status(thm)],[c_605,c_338]) ).
cnf(c_5187,plain,
( ~ v3_struct_0(k1_lattice2(k11_conlat_1(sK0)))
| v3_struct_0(k11_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_605,c_326]) ).
cnf(c_1057,plain,
~ v3_struct_0(k1_lattice2(k11_conlat_1(sK0))),
inference(resolve,[status(thm)],[c_545,c_5187]) ).
cnf(c_5188,negated_conjecture,
( r1_filter_1(k1_lattice2(k11_conlat_1(sK0)),k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK0))) ),
inference(resolve,[status(thm)],[c_1057,c_912]) ).
cnf(c_1063,negated_conjecture,
( r1_filter_1(k1_lattice2(k11_conlat_1(sK0)),k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_1055,c_5188]) ).
cnf(c_5189,plain,
( ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0)
| l3_lattices(k11_conlat_1(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_973,c_336]) ).
cnf(c_5190,negated_conjecture,
( ~ l2_conlat_1(sK0)
| l3_lattices(k11_conlat_1(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_246,c_5189]) ).
cnf(c_2574,negated_conjecture,
l3_lattices(k11_conlat_1(k7_conlat_2(sK0))),
inference(resolve,[status(thm)],[c_245,c_5190]) ).
cnf(c_2575,negated_conjecture,
( r1_filter_1(k1_lattice2(k11_conlat_1(sK0)),k11_conlat_1(k7_conlat_2(sK0)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_2574,c_1063]) ).
cnf(c_5191,plain,
( ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0)
| v10_lattices(k11_conlat_1(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_981,c_336]) ).
cnf(c_5192,negated_conjecture,
( ~ l2_conlat_1(sK0)
| v10_lattices(k11_conlat_1(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_246,c_5191]) ).
cnf(c_2630,negated_conjecture,
v10_lattices(k11_conlat_1(k7_conlat_2(sK0))),
inference(resolve,[status(thm)],[c_245,c_5192]) ).
cnf(c_2636,negated_conjecture,
( r1_filter_1(k1_lattice2(k11_conlat_1(sK0)),k11_conlat_1(k7_conlat_2(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_2630,c_2575]) ).
cnf(c_5193,plain,
( r1_filter_1(k11_conlat_1(k7_conlat_2(sK0)),k1_lattice2(k11_conlat_1(sK0)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK0)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK0)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_2636,c_255]) ).
cnf(c_5194,plain,
( r1_filter_1(k11_conlat_1(k7_conlat_2(sK0)),k1_lattice2(k11_conlat_1(sK0)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK0)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK0)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0))) ),
inference(copy,[status(thm)],[c_5193]) ).
cnf(c_5195,plain,
( r1_filter_1(k11_conlat_1(k7_conlat_2(sK0)),k1_lattice2(k11_conlat_1(sK0)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK0)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_1057,c_5194]) ).
cnf(c_5196,plain,
( r1_filter_1(k11_conlat_1(k7_conlat_2(sK0)),k1_lattice2(k11_conlat_1(sK0)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_907,c_5195]) ).
cnf(c_5197,plain,
( r1_filter_1(k11_conlat_1(k7_conlat_2(sK0)),k1_lattice2(k11_conlat_1(sK0)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| ~ v10_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_1055,c_5196]) ).
cnf(c_5198,plain,
( r1_filter_1(k11_conlat_1(k7_conlat_2(sK0)),k1_lattice2(k11_conlat_1(sK0)))
| ~ l3_lattices(k11_conlat_1(k7_conlat_2(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_2630,c_5197]) ).
cnf(c_5199,plain,
( r1_filter_1(k11_conlat_1(k7_conlat_2(sK0)),k1_lattice2(k11_conlat_1(sK0)))
| v3_struct_0(k11_conlat_1(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_2574,c_5198]) ).
cnf(c_5175,negated_conjecture,
v3_struct_0(k11_conlat_1(k7_conlat_2(sK0))),
inference(resolve,[status(thm)],[c_244,c_5199]) ).
cnf(c_5176,plain,
v3_conlat_1(k7_conlat_2(sK0)),
inference(resolve,[status(thm)],[c_5175,c_975]) ).
cnf(c_5200,plain,
( ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_5176,c_336]) ).
cnf(c_5201,negated_conjecture,
~ l2_conlat_1(sK0),
inference(resolve,[status(thm)],[c_246,c_5200]) ).
cnf(c_5177,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_245,c_5201]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LAT346+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.02/0.29 % Computer : n012.cluster.edu
% 0.02/0.29 % Model : x86_64 x86_64
% 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.29 % Memory : 8046.5625MB
% 0.02/0.29 % OS : Linux 6.8.0-71-generic
% 0.02/0.29 % CPULimit : 300
% 0.02/0.29 % WCLimit : 300
% 0.02/0.29 % DateTime : Fri Sep 25 21:07:35 UTC 2026
% 0.02/0.29 % CPUTime :
% 0.02/0.29 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.02/0.29 % Process 3022256 was started by sandbox2 on n012,
% 0.02/0.29 % Fri Sep 25 21:07:35 2026
% 0.02/0.29 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.02/0.31
% 0.02/0.31 % From the command line: assign(max_seconds, 300).
% 2.72/0.75
% 2.72/0.75 % given #500 (T,wt=19): 943 v1_relat_1(k4_relat_1(u2_lattices(c15))). [resolve(590,a,337,a)].
% 2.72/0.75
% 2.72/0.75 % given #1000 (T,wt=21): 3439 v1_funct_1(f2(k1_lattice2(c15),k11_conlat_1(c14))). [resolve(821,b,526,a),unit_del(a,544),unit_del(b,604)].
% 2.72/0.75
% 2.72/0.75 % SZS status Theorem for theBenchmark
% 2.72/0.75
% 2.72/0.75 % Proof 1 at 0.35 (+ 0.08) seconds.
% 2.72/0.75 % Length of proof is 48.
% 2.72/0.75 % Level of proof is 10.
% 2.72/0.75 % Maximum clause weight is 59.000.
% 2.72/0.75 % Given clauses 1477.
% 2.72/0.75
% 2.72/0.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------