%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT319+3 : 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 : n019.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:12 AM UTC 2026
% Result : Theorem 101.56s 20.71s
% Output : CNFRefutation 101.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 11
% Syntax : Number of formulae : 145 ( 19 unt; 0 def)
% Number of atoms : 590 ( 0 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 697 ( 252 ~; 335 |; 89 &)
% ( 8 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 17 ( 16 usr; 1 prp; 0-1 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-1 aty)
% Number of variables : 30 ( 0 sgn 12 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
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(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(t63_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v13_lattices(A)
<=> v14_lattices(k1_lattice2(A)) ) ),
file('theBenchmark.p',t63_lattice2) ).
fof(t64_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v14_lattices(A)
<=> v13_lattices(k1_lattice2(A)) ) ),
file('theBenchmark.p',t64_lattice2) ).
fof(t65_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( ( l3_lattices(A)
& v11_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
<=> ( l3_lattices(k1_lattice2(A))
& v11_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ) ),
file('theBenchmark.p',t65_lattice2) ).
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(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(d15_lattices,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v15_lattices(A)
<=> ( v14_lattices(A)
& v13_lattices(A) ) ) ),
file('theBenchmark.p',d15_lattices) ).
fof(d20_lattices,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v17_lattices(A)
<=> ( v11_lattices(A)
& v16_lattices(A)
& v15_lattices(A) ) ) ),
file('theBenchmark.p',d20_lattices) ).
fof(t53_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( ( l3_lattices(A)
& v16_lattices(A)
& v15_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
<=> ( l3_lattices(k1_lattice2(A))
& v16_lattices(k1_lattice2(A))
& v15_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ) ),
file('theBenchmark.p',t53_filter_2) ).
fof(t54_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
<=> ( l3_lattices(k1_lattice2(A))
& v17_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ) ),
file('theBenchmark.p',t54_filter_2) ).
fof(t54_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
<=> ( l3_lattices(k1_lattice2(A))
& v17_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ) ),
inference(assume_negation,[status(cth)],[t54_filter_2]) ).
cnf(c_1484,plain,
( v13_lattices(A)
| ~ v17_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc5_lattices]) ).
cnf(c_1485,plain,
( v14_lattices(A)
| ~ v17_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc5_lattices]) ).
cnf(c_1555,plain,
( ~ v14_lattices(A)
| ~ v13_lattices(A)
| v15_lattices(A)
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d15_lattices]) ).
cnf(c_1565,plain,
( v16_lattices(A)
| ~ v17_lattices(A)
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d20_lattices]) ).
cnf(c_1566,plain,
( v11_lattices(A)
| ~ v17_lattices(A)
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d20_lattices]) ).
cnf(c_1567,plain,
( ~ v11_lattices(A)
| ~ v16_lattices(A)
| ~ v15_lattices(A)
| v17_lattices(A)
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d20_lattices]) ).
cnf(c_2434,plain,
( v16_lattices(k1_lattice2(A))
| ~ v16_lattices(A)
| ~ v15_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t53_filter_2]) ).
cnf(c_2437,plain,
( ~ l3_lattices(k1_lattice2(A))
| ~ v16_lattices(k1_lattice2(A))
| ~ v15_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A))
| v16_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t53_filter_2]) ).
cnf(c_2591,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_2599,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_2618,plain,
( v14_lattices(k1_lattice2(A))
| ~ v13_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t63_lattice2]) ).
cnf(c_2619,plain,
( ~ v14_lattices(k1_lattice2(A))
| v13_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t63_lattice2]) ).
cnf(c_2620,plain,
( v13_lattices(k1_lattice2(A))
| ~ v14_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t64_lattice2]) ).
cnf(c_2621,plain,
( ~ v13_lattices(k1_lattice2(A))
| v14_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t64_lattice2]) ).
cnf(c_2622,plain,
( v11_lattices(k1_lattice2(A))
| ~ v11_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t65_lattice2]) ).
cnf(c_2624,plain,
( ~ l3_lattices(k1_lattice2(A))
| ~ v11_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A))
| v11_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t65_lattice2]) ).
cnf(c_2632,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
fof(nnf_774,plain,
? [A] :
( ( ~ l3_lattices(k1_lattice2(A))
| ~ v17_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) )
& ( ( l3_lattices(k1_lattice2(A))
& v17_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) )
| ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t54_filter_2_neg]) ).
fof(sk_t54_filter_2_neg_sk,plain,
( ( ~ l3_lattices(k1_lattice2(sK0))
| ~ v17_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v17_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) )
& ( ( l3_lattices(k1_lattice2(sK0))
& v17_lattices(k1_lattice2(sK0))
& v10_lattices(k1_lattice2(sK0))
& ~ v3_struct_0(k1_lattice2(sK0)) )
| ( l3_lattices(sK0)
& v17_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ) )
& l3_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(A,sK0)],[nnf_774]) ).
fof(sk_t54_filter_2_neg,plain,
( ( ~ l3_lattices(k1_lattice2(sK0))
| ~ v17_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v17_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) )
& ( l3_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) )
& ( v17_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) )
& ( v10_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) )
& ( ~ v3_struct_0(k1_lattice2(sK0))
| v17_lattices(sK0) )
& l3_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(cnf_transformation,[status(thm)],[sk_t54_filter_2_neg_sk]) ).
cnf(c_2641,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t54_filter_2_neg]) ).
cnf(c_2642,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t54_filter_2_neg]) ).
cnf(c_2643,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t54_filter_2_neg]) ).
cnf(c_2646,negated_conjecture,
( v17_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(split_conjunct,[status(thm)],[sk_t54_filter_2_neg]) ).
cnf(c_2648,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v17_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v17_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(split_conjunct,[status(thm)],[sk_t54_filter_2_neg]) ).
cnf(c_18431,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v17_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v17_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2641,c_2648]) ).
cnf(c_18432,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v17_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2642,c_18431]) ).
cnf(c_2649,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v17_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2643,c_18432]) ).
cnf(c_6599,plain,
l3_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_2632,c_2643]) ).
cnf(c_6610,negated_conjecture,
( ~ v17_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_6599,c_2649]) ).
cnf(c_18433,negated_conjecture,
( v11_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2646,c_1566]) ).
cnf(c_18434,negated_conjecture,
( v11_lattices(sK0)
| ~ l3_lattices(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2641,c_18433]) ).
cnf(c_9075,negated_conjecture,
( v11_lattices(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2643,c_18434]) ).
cnf(c_18435,negated_conjecture,
( v16_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2646,c_1565]) ).
cnf(c_18436,negated_conjecture,
( v16_lattices(sK0)
| ~ l3_lattices(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2641,c_18435]) ).
cnf(c_9076,negated_conjecture,
( v16_lattices(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2643,c_18436]) ).
cnf(c_18437,negated_conjecture,
( v14_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2646,c_1485]) ).
cnf(c_18438,negated_conjecture,
( v14_lattices(sK0)
| v3_struct_0(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2643,c_18437]) ).
cnf(c_9078,negated_conjecture,
( v14_lattices(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2641,c_18438]) ).
cnf(c_18439,negated_conjecture,
( v13_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2646,c_1484]) ).
cnf(c_18440,negated_conjecture,
( v13_lattices(sK0)
| v3_struct_0(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2643,c_18439]) ).
cnf(c_9079,negated_conjecture,
( v13_lattices(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2641,c_18440]) ).
cnf(c_18441,negated_conjecture,
( v11_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2646,c_1566]) ).
cnf(c_9085,negated_conjecture,
( v11_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_6599,c_18441]) ).
cnf(c_18442,negated_conjecture,
( v16_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2646,c_1565]) ).
cnf(c_9086,negated_conjecture,
( v16_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_6599,c_18442]) ).
cnf(c_18443,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2646,c_1485]) ).
cnf(c_9088,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_6599,c_18443]) ).
cnf(c_18444,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2646,c_1484]) ).
cnf(c_9089,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_6599,c_18444]) ).
cnf(c_18445,negated_conjecture,
( ~ v3_struct_0(k1_lattice2(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_2591,c_2643]) ).
cnf(c_12840,negated_conjecture,
~ v3_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_2641,c_18445]) ).
cnf(c_12854,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_12840,c_9089]) ).
cnf(c_12855,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_12840,c_9088]) ).
cnf(c_12857,negated_conjecture,
( v16_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_12840,c_9086]) ).
cnf(c_12858,negated_conjecture,
( v11_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_12840,c_9085]) ).
cnf(c_12977,negated_conjecture,
( ~ v17_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| ~ v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_12840,c_6610]) ).
cnf(c_18446,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_2599,c_2642]) ).
cnf(c_18447,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2641,c_18446]) ).
cnf(c_13644,negated_conjecture,
v10_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_2643,c_18447]) ).
cnf(c_13653,negated_conjecture,
( ~ v17_lattices(k1_lattice2(sK0))
| ~ v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_13644,c_12977]) ).
cnf(c_18448,plain,
( v11_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_9075,c_2622]) ).
cnf(c_18449,negated_conjecture,
( v11_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2641,c_18448]) ).
cnf(c_18450,negated_conjecture,
( v11_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2642,c_18449]) ).
cnf(c_16294,negated_conjecture,
( v11_lattices(k1_lattice2(sK0))
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_2643,c_18450]) ).
cnf(c_16300,plain,
( ~ v17_lattices(sK0)
| v16_lattices(sK0) ),
inference(resolve,[status(thm)],[c_9076,c_13653]) ).
cnf(c_16336,plain,
( ~ v17_lattices(sK0)
| v14_lattices(sK0) ),
inference(resolve,[status(thm)],[c_9078,c_13653]) ).
cnf(c_16355,plain,
( ~ v17_lattices(sK0)
| v13_lattices(sK0) ),
inference(resolve,[status(thm)],[c_9079,c_13653]) ).
cnf(c_18451,plain,
( v14_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_12854,c_2621]) ).
cnf(c_18452,negated_conjecture,
( v14_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2641,c_18451]) ).
cnf(c_18453,negated_conjecture,
( v14_lattices(sK0)
| ~ l3_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2642,c_18452]) ).
cnf(c_18182,negated_conjecture,
( v14_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2643,c_18453]) ).
cnf(c_18454,plain,
( v14_lattices(sK0)
| v14_lattices(sK0) ),
inference(resolve,[status(thm)],[c_18182,c_16336]) ).
cnf(c_18191,plain,
v14_lattices(sK0),
inference(copy,[status(thm)],[c_18454]) ).
cnf(c_18455,plain,
( v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_18191,c_2620]) ).
cnf(c_18456,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2641,c_18455]) ).
cnf(c_18457,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2642,c_18456]) ).
cnf(c_18225,negated_conjecture,
v13_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_2643,c_18457]) ).
cnf(c_18458,plain,
( ~ v13_lattices(sK0)
| v15_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_18191,c_1555]) ).
cnf(c_18459,negated_conjecture,
( ~ v13_lattices(sK0)
| v15_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2641,c_18458]) ).
cnf(c_18231,negated_conjecture,
( ~ v13_lattices(sK0)
| v15_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2643,c_18459]) ).
cnf(c_18460,plain,
( v13_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_12855,c_2619]) ).
cnf(c_18461,negated_conjecture,
( v13_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2641,c_18460]) ).
cnf(c_18462,negated_conjecture,
( v13_lattices(sK0)
| ~ l3_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2642,c_18461]) ).
cnf(c_18250,negated_conjecture,
( v13_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2643,c_18462]) ).
cnf(c_18463,plain,
( v13_lattices(sK0)
| v13_lattices(sK0) ),
inference(resolve,[status(thm)],[c_18250,c_16355]) ).
cnf(c_18256,plain,
v13_lattices(sK0),
inference(copy,[status(thm)],[c_18463]) ).
cnf(c_18265,negated_conjecture,
v15_lattices(sK0),
inference(resolve,[status(thm)],[c_18256,c_18231]) ).
cnf(c_18464,plain,
( v14_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_18256,c_2618]) ).
cnf(c_18465,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2641,c_18464]) ).
cnf(c_18466,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2642,c_18465]) ).
cnf(c_18300,negated_conjecture,
v14_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_2643,c_18466]) ).
cnf(c_18467,plain,
( ~ v13_lattices(k1_lattice2(sK0))
| v15_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_18300,c_1555]) ).
cnf(c_18468,plain,
( ~ v13_lattices(k1_lattice2(sK0))
| v15_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_12840,c_18467]) ).
cnf(c_18469,plain,
( ~ v13_lattices(k1_lattice2(sK0))
| v15_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_6599,c_18468]) ).
cnf(c_18325,plain,
v15_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_18225,c_18469]) ).
cnf(c_18470,plain,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v15_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v16_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_12857,c_2437]) ).
cnf(c_18471,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v15_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v16_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2641,c_18470]) ).
cnf(c_18472,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v15_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v16_lattices(sK0)
| ~ l3_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2642,c_18471]) ).
cnf(c_18473,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v15_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v16_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2643,c_18472]) ).
cnf(c_18474,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v15_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v16_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_12840,c_18473]) ).
cnf(c_18475,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v15_lattices(k1_lattice2(sK0))
| v16_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_13644,c_18474]) ).
cnf(c_18476,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| v16_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_18325,c_18475]) ).
cnf(c_18334,negated_conjecture,
( v16_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_6599,c_18476]) ).
cnf(c_18477,plain,
( v16_lattices(sK0)
| v16_lattices(sK0) ),
inference(resolve,[status(thm)],[c_18334,c_16300]) ).
cnf(c_18339,plain,
v16_lattices(sK0),
inference(copy,[status(thm)],[c_18477]) ).
cnf(c_18478,plain,
( ~ v11_lattices(sK0)
| ~ v15_lattices(sK0)
| v17_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_18334,c_1567]) ).
cnf(c_18479,plain,
( ~ v11_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0)
| v17_lattices(sK0) ),
inference(copy,[status(thm)],[c_18478]) ).
cnf(c_18480,negated_conjecture,
( ~ v11_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ l3_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2641,c_18479]) ).
cnf(c_18481,negated_conjecture,
( ~ v11_lattices(sK0)
| ~ v15_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2643,c_18480]) ).
cnf(c_18342,negated_conjecture,
( ~ v11_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_18265,c_18481]) ).
cnf(c_18482,plain,
( v16_lattices(k1_lattice2(sK0))
| ~ v15_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_18339,c_2434]) ).
cnf(c_18483,negated_conjecture,
( v16_lattices(k1_lattice2(sK0))
| ~ v15_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2641,c_18482]) ).
cnf(c_18484,negated_conjecture,
( v16_lattices(k1_lattice2(sK0))
| ~ v15_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2642,c_18483]) ).
cnf(c_18485,negated_conjecture,
( v16_lattices(k1_lattice2(sK0))
| ~ v15_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2643,c_18484]) ).
cnf(c_18361,negated_conjecture,
v16_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_18265,c_18485]) ).
cnf(c_18486,plain,
( ~ v11_lattices(k1_lattice2(sK0))
| ~ v15_lattices(k1_lattice2(sK0))
| v17_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_18361,c_1567]) ).
cnf(c_18487,plain,
( ~ v11_lattices(k1_lattice2(sK0))
| ~ v15_lattices(k1_lattice2(sK0))
| v17_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_12840,c_18486]) ).
cnf(c_18488,plain,
( ~ v11_lattices(k1_lattice2(sK0))
| ~ v15_lattices(k1_lattice2(sK0))
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_6599,c_18487]) ).
cnf(c_18368,plain,
( ~ v11_lattices(k1_lattice2(sK0))
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_18325,c_18488]) ).
cnf(c_18489,plain,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v11_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_12858,c_2624]) ).
cnf(c_18490,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v11_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2641,c_18489]) ).
cnf(c_18491,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v11_lattices(sK0)
| ~ l3_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2642,c_18490]) ).
cnf(c_18492,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v11_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_2643,c_18491]) ).
cnf(c_18493,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v11_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_12840,c_18492]) ).
cnf(c_18494,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| v11_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_13644,c_18493]) ).
cnf(c_18375,negated_conjecture,
( v11_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_6599,c_18494]) ).
cnf(c_18495,plain,
( v17_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_18375,c_18342]) ).
cnf(c_18382,plain,
v17_lattices(sK0),
inference(copy,[status(thm)],[c_18495]) ).
cnf(c_18396,negated_conjecture,
~ v17_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_18382,c_13653]) ).
cnf(c_18423,negated_conjecture,
~ v11_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_18396,c_18368]) ).
cnf(c_18496,negated_conjecture,
v11_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_18396,c_16294]) ).
cnf(c_18430,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_18423,c_18496]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT319+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/5.79 % Computer : n019.cluster.edu
% 0.12/5.79 % Model : x86_64 x86_64
% 0.12/5.79 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.79 % Memory : 8046.5625MB
% 0.12/5.79 % OS : Linux 6.8.0-71-generic
% 0.12/5.80 % CPULimit : 300
% 0.12/5.80 % WCLimit : 300
% 0.12/5.80 % DateTime : Fri Sep 25 20:49:53 UTC 2026
% 0.15/5.80 % CPUTime :
% 0.15/5.80 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/5.80 % Process 3657533 was started by sandbox2 on n019,
% 0.15/5.80 % Fri Sep 25 20:49:53 2026
% 0.15/5.80 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 101.56/20.71
% 101.56/20.71 % SInE (scan): 551 to sos (tol 1.5x), 232 to usable (tol 2.0x), 12862 zapped, of 13645 axioms (depth 3).
% 101.56/20.71
% 101.56/20.71 % From the command line: assign(max_seconds, 300).
% 101.56/20.71
% 101.56/20.71 % given #500 (T,wt=13): 13466 v4_lattices(k1_lattice2(c27)). [resolve(2593,b,2317,a),unit_del(a,2310),unit_del(b,2309)].
% 101.56/20.71
% 101.56/20.71 % SZS status Theorem for theBenchmark
% 101.56/20.71
% 101.56/20.71 % Proof 1 at 13.43 (+ 0.91) seconds.
% 101.56/20.71 % Length of proof is 75.
% 101.56/20.71 % Level of proof is 15.
% 101.56/20.71 % Maximum clause weight is 30.000.
% 101.56/20.71 % Given clauses 959.
% 101.56/20.71
% 101.56/20.71 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------