%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT319+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 221.17s 33.20s
% Output : CNFRefutation 221.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 12
% Syntax : Number of formulae : 167 ( 26 unt; 0 def)
% Number of atoms : 671 ( 0 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 812 ( 308 ~; 385 |; 96 &)
% ( 8 <=>; 15 =>; 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 : 37 ( 0 sgn 13 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc2_lattices,axiom,
! [A] :
( l3_lattices(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) ) ) ),
file('theBenchmark.p',cc2_lattices) ).
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_2457,plain,
( v13_lattices(A)
| ~ v17_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc5_lattices]) ).
cnf(c_2458,plain,
( v14_lattices(A)
| ~ v17_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc5_lattices]) ).
cnf(c_2533,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_2543,plain,
( v16_lattices(A)
| ~ v17_lattices(A)
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d20_lattices]) ).
cnf(c_2544,plain,
( v11_lattices(A)
| ~ v17_lattices(A)
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d20_lattices]) ).
cnf(c_2545,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_3838,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_3841,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_3856,plain,
( v10_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v7_lattices(A)
| ~ v6_lattices(A)
| ~ v5_lattices(A)
| ~ v4_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc2_lattices]) ).
cnf(c_3981,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_3983,plain,
( v4_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_3984,plain,
( v5_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_3985,plain,
( v6_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_3986,plain,
( v7_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_3987,plain,
( v8_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_3988,plain,
( v9_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_4016,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_4017,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_4018,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_4019,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_4020,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_4022,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_4035,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
fof(nnf_1114,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_1114]) ).
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_4085,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t54_filter_2_neg]) ).
cnf(c_4086,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t54_filter_2_neg]) ).
cnf(c_4087,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t54_filter_2_neg]) ).
cnf(c_4090,negated_conjecture,
( v17_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(split_conjunct,[status(thm)],[sk_t54_filter_2_neg]) ).
cnf(c_4092,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_27024,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_4085,c_4092]) ).
cnf(c_27025,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_4086,c_27024]) ).
cnf(c_4093,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_4087,c_27025]) ).
cnf(c_5874,plain,
l3_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_4035,c_4087]) ).
cnf(c_5890,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_5874,c_4093]) ).
cnf(c_27026,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_4090,c_2544]) ).
cnf(c_7885,negated_conjecture,
( v11_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_5874,c_27026]) ).
cnf(c_27027,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_4090,c_2543]) ).
cnf(c_7886,negated_conjecture,
( v16_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_5874,c_27027]) ).
cnf(c_27028,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_4090,c_2458]) ).
cnf(c_7888,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_5874,c_27028]) ).
cnf(c_27029,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_4090,c_2457]) ).
cnf(c_7889,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_5874,c_27029]) ).
cnf(c_27030,negated_conjecture,
( ~ v3_struct_0(k1_lattice2(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3981,c_4087]) ).
cnf(c_18343,negated_conjecture,
~ v3_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_4085,c_27030]) ).
cnf(c_18358,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_18343,c_7889]) ).
cnf(c_18359,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_18343,c_7888]) ).
cnf(c_18361,negated_conjecture,
( v16_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_18343,c_7886]) ).
cnf(c_18362,negated_conjecture,
( v11_lattices(k1_lattice2(sK0))
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_18343,c_7885]) ).
cnf(c_18399,negated_conjecture,
( ~ v17_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| ~ v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_18343,c_5890]) ).
cnf(c_27031,negated_conjecture,
( v4_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3983,c_4086]) ).
cnf(c_27032,negated_conjecture,
( v4_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27031]) ).
cnf(c_19566,negated_conjecture,
v4_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_4087,c_27032]) ).
cnf(c_27033,negated_conjecture,
( v5_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3984,c_4086]) ).
cnf(c_27034,negated_conjecture,
( v5_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27033]) ).
cnf(c_19592,negated_conjecture,
v5_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_4087,c_27034]) ).
cnf(c_27035,negated_conjecture,
( v6_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3985,c_4086]) ).
cnf(c_27036,negated_conjecture,
( v6_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27035]) ).
cnf(c_19619,negated_conjecture,
v6_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_4087,c_27036]) ).
cnf(c_27037,negated_conjecture,
( v7_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3986,c_4086]) ).
cnf(c_27038,negated_conjecture,
( v7_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27037]) ).
cnf(c_19636,negated_conjecture,
v7_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_4087,c_27038]) ).
cnf(c_27039,negated_conjecture,
( v8_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3987,c_4086]) ).
cnf(c_27040,negated_conjecture,
( v8_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27039]) ).
cnf(c_19650,negated_conjecture,
v8_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_4087,c_27040]) ).
cnf(c_27041,negated_conjecture,
( v9_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3988,c_4086]) ).
cnf(c_27042,negated_conjecture,
( v9_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27041]) ).
cnf(c_19661,negated_conjecture,
v9_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_4087,c_27042]) ).
cnf(c_27043,plain,
( v10_lattices(k1_lattice2(sK0))
| ~ v9_lattices(k1_lattice2(sK0))
| ~ v8_lattices(k1_lattice2(sK0))
| ~ v6_lattices(k1_lattice2(sK0))
| ~ v5_lattices(k1_lattice2(sK0))
| ~ v4_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_19636,c_3856]) ).
cnf(c_27044,plain,
( v10_lattices(k1_lattice2(sK0))
| ~ v9_lattices(k1_lattice2(sK0))
| ~ v8_lattices(k1_lattice2(sK0))
| ~ v6_lattices(k1_lattice2(sK0))
| ~ v5_lattices(k1_lattice2(sK0))
| ~ v4_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_5874,c_27043]) ).
cnf(c_27045,plain,
( v10_lattices(k1_lattice2(sK0))
| ~ v9_lattices(k1_lattice2(sK0))
| ~ v8_lattices(k1_lattice2(sK0))
| ~ v6_lattices(k1_lattice2(sK0))
| ~ v5_lattices(k1_lattice2(sK0))
| ~ v4_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_18343,c_27044]) ).
cnf(c_27046,plain,
( v10_lattices(k1_lattice2(sK0))
| ~ v9_lattices(k1_lattice2(sK0))
| ~ v8_lattices(k1_lattice2(sK0))
| ~ v6_lattices(k1_lattice2(sK0))
| ~ v5_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_19566,c_27045]) ).
cnf(c_27047,plain,
( v10_lattices(k1_lattice2(sK0))
| ~ v9_lattices(k1_lattice2(sK0))
| ~ v8_lattices(k1_lattice2(sK0))
| ~ v6_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_19592,c_27046]) ).
cnf(c_27048,plain,
( v10_lattices(k1_lattice2(sK0))
| ~ v9_lattices(k1_lattice2(sK0))
| ~ v8_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_19619,c_27047]) ).
cnf(c_27049,plain,
( v10_lattices(k1_lattice2(sK0))
| ~ v9_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_19650,c_27048]) ).
cnf(c_19672,plain,
v10_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_19661,c_27049]) ).
cnf(c_19673,negated_conjecture,
( ~ v17_lattices(k1_lattice2(sK0))
| ~ v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_19672,c_18399]) ).
cnf(c_27050,plain,
( v14_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| v13_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_18358,c_2458]) ).
cnf(c_27051,negated_conjecture,
( v14_lattices(sK0)
| v3_struct_0(sK0)
| v13_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_4087,c_27050]) ).
cnf(c_24488,negated_conjecture,
( v14_lattices(sK0)
| v13_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_4085,c_27051]) ).
cnf(c_27052,plain,
( v13_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_18359,c_4017]) ).
cnf(c_27053,negated_conjecture,
( v13_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27052]) ).
cnf(c_27054,negated_conjecture,
( v13_lattices(sK0)
| ~ l3_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4086,c_27053]) ).
cnf(c_24495,negated_conjecture,
( v13_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4087,c_27054]) ).
cnf(c_27055,plain,
( v13_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| v13_lattices(sK0) ),
inference(resolve,[status(thm)],[c_24495,c_2457]) ).
cnf(c_27056,plain,
( v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| v13_lattices(sK0) ),
inference(copy,[status(thm)],[c_27055]) ).
cnf(c_27057,negated_conjecture,
( v3_struct_0(sK0)
| v13_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4087,c_27056]) ).
cnf(c_24509,negated_conjecture,
v13_lattices(sK0),
inference(resolve,[status(thm)],[c_4085,c_27057]) ).
cnf(c_27058,plain,
( v14_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_24509,c_4016]) ).
cnf(c_27059,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27058]) ).
cnf(c_27060,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4086,c_27059]) ).
cnf(c_24527,negated_conjecture,
v14_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_4087,c_27060]) ).
cnf(c_27061,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_24527,c_2533]) ).
cnf(c_27062,plain,
( ~ v13_lattices(k1_lattice2(sK0))
| v15_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_18343,c_27061]) ).
cnf(c_24539,plain,
( ~ v13_lattices(k1_lattice2(sK0))
| v15_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_5874,c_27062]) ).
cnf(c_27063,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_18361,c_3841]) ).
cnf(c_27064,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_4085,c_27063]) ).
cnf(c_27065,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_4086,c_27064]) ).
cnf(c_27066,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_4087,c_27065]) ).
cnf(c_27067,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_18343,c_27066]) ).
cnf(c_27068,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v15_lattices(k1_lattice2(sK0))
| v16_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_19672,c_27067]) ).
cnf(c_24549,negated_conjecture,
( ~ v15_lattices(k1_lattice2(sK0))
| v16_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_5874,c_27068]) ).
cnf(c_27069,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_18362,c_4022]) ).
cnf(c_27070,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_4085,c_27069]) ).
cnf(c_27071,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_4086,c_27070]) ).
cnf(c_27072,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_4087,c_27071]) ).
cnf(c_27073,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v11_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_18343,c_27072]) ).
cnf(c_27074,negated_conjecture,
( ~ l3_lattices(k1_lattice2(sK0))
| v11_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_19672,c_27073]) ).
cnf(c_24553,negated_conjecture,
( v11_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_5874,c_27074]) ).
cnf(c_27075,plain,
( v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| v13_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_24488,c_4018]) ).
cnf(c_27076,plain,
( ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| v13_lattices(k1_lattice2(sK0)) ),
inference(copy,[status(thm)],[c_27075]) ).
cnf(c_27077,negated_conjecture,
( ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v13_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_4085,c_27076]) ).
cnf(c_27078,negated_conjecture,
( ~ l3_lattices(sK0)
| v13_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_4086,c_27077]) ).
cnf(c_26731,negated_conjecture,
v13_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_4087,c_27078]) ).
cnf(c_26734,plain,
v15_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_26731,c_24539]) ).
cnf(c_26739,negated_conjecture,
( v16_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_26734,c_24549]) ).
cnf(c_27079,plain,
( v14_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_26731,c_4019]) ).
cnf(c_27080,negated_conjecture,
( v14_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27079]) ).
cnf(c_27081,negated_conjecture,
( v14_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4086,c_27080]) ).
cnf(c_26743,negated_conjecture,
v14_lattices(sK0),
inference(resolve,[status(thm)],[c_4087,c_27081]) ).
cnf(c_27082,plain,
( ~ v13_lattices(sK0)
| v15_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_26743,c_2533]) ).
cnf(c_27083,negated_conjecture,
( ~ v13_lattices(sK0)
| v15_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27082]) ).
cnf(c_27084,negated_conjecture,
( ~ v13_lattices(sK0)
| v15_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4087,c_27083]) ).
cnf(c_26760,negated_conjecture,
v15_lattices(sK0),
inference(resolve,[status(thm)],[c_24509,c_27084]) ).
cnf(c_27085,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_26739,c_2545]) ).
cnf(c_27086,plain,
( ~ v11_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0)
| v17_lattices(sK0) ),
inference(copy,[status(thm)],[c_27085]) ).
cnf(c_27087,negated_conjecture,
( ~ v11_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ l3_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27086]) ).
cnf(c_27088,negated_conjecture,
( ~ v11_lattices(sK0)
| ~ v15_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4087,c_27087]) ).
cnf(c_26969,negated_conjecture,
( ~ v11_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_26760,c_27088]) ).
cnf(c_27089,plain,
( v17_lattices(sK0)
| v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_26969,c_24553]) ).
cnf(c_26973,plain,
v17_lattices(sK0),
inference(copy,[status(thm)],[c_27089]) ).
cnf(c_26975,negated_conjecture,
~ v17_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_26973,c_19673]) ).
cnf(c_27090,plain,
( v11_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_26973,c_2544]) ).
cnf(c_27091,negated_conjecture,
( v11_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27090]) ).
cnf(c_27003,negated_conjecture,
v11_lattices(sK0),
inference(resolve,[status(thm)],[c_4087,c_27091]) ).
cnf(c_27092,plain,
( v16_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_26973,c_2543]) ).
cnf(c_27093,negated_conjecture,
( v16_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27092]) ).
cnf(c_27004,negated_conjecture,
v16_lattices(sK0),
inference(resolve,[status(thm)],[c_4087,c_27093]) ).
cnf(c_27094,plain,
( v11_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_27003,c_4020]) ).
cnf(c_27095,negated_conjecture,
( v11_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27094]) ).
cnf(c_27096,negated_conjecture,
( v11_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4086,c_27095]) ).
cnf(c_27010,negated_conjecture,
v11_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_4087,c_27096]) ).
cnf(c_27097,plain,
( v16_lattices(k1_lattice2(sK0))
| ~ v15_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_27004,c_3838]) ).
cnf(c_27098,negated_conjecture,
( v16_lattices(k1_lattice2(sK0))
| ~ v15_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4085,c_27097]) ).
cnf(c_27099,negated_conjecture,
( v16_lattices(k1_lattice2(sK0))
| ~ v15_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4086,c_27098]) ).
cnf(c_27100,negated_conjecture,
( v16_lattices(k1_lattice2(sK0))
| ~ v15_lattices(sK0) ),
inference(resolve,[status(thm)],[c_4087,c_27099]) ).
cnf(c_27013,negated_conjecture,
v16_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_26760,c_27100]) ).
cnf(c_27101,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_27013,c_2545]) ).
cnf(c_27102,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_18343,c_27101]) ).
cnf(c_27103,plain,
( ~ v11_lattices(k1_lattice2(sK0))
| ~ v15_lattices(k1_lattice2(sK0))
| v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_5874,c_27102]) ).
cnf(c_27104,negated_conjecture,
( ~ v11_lattices(k1_lattice2(sK0))
| ~ v15_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_26975,c_27103]) ).
cnf(c_27105,negated_conjecture,
~ v11_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_26734,c_27104]) ).
cnf(c_27023,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_27010,c_27105]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT319+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n001.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 25 20:55:49 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 27391 was started by sandbox on n001,
% 0.11/0.37 % Fri Sep 25 20:55:49 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 221.17/33.20
% 221.17/33.20 % SInE (scan): 843 to sos (tol 1.5x), 280 to usable (tol 2.0x), 33597 zapped, of 34720 axioms (depth 3).
% 221.17/33.20
% 221.17/33.20 % From the command line: assign(max_seconds, 300).
% 221.17/33.20
% 221.17/33.20 % given #500 (T,wt=4): 10331 l3_lattices(k1_lattice2(k1_lattice2(c5))). [resolve(10288,a,4035,a)].
% 221.17/33.20
% 221.17/33.20 % given #1000 (A,wt=131): 3969 v3_struct_0(A) | -v10_lattices(A) | -l3_lattices(A) | v1_xboole_0(B) | -m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) | m1_filter_0(B,A) | -r2_hidden(k4_lattices(A,f14(A,B),f15(A,B)),B) | r2_hidden(f16(A,B),B) # tptp_name(t9_filter_0) # sine_depth(2). [clausify(38)].
% 221.17/33.20
% 221.17/33.20 % given #1500 (T,wt=3): 22510 v15_lattices(k1_lattice2(c18)). [back_unit_del(22472),unit_del(b,22495)].
% 221.17/33.20
% 221.17/33.20 % given #2000 (W,wt=5): 22230 v1_funct_1(f184(f310(k1_lattice2(c19)))). [resolve(18722,a,1884,a)].
% 221.17/33.20
% 221.17/33.20 % SZS status Theorem for theBenchmark
% 221.17/33.20
% 221.17/33.20 % Proof 1 at 29.04 (+ 2.10) seconds.
% 221.17/33.20 % Length of proof is 81.
% 221.17/33.20 % Level of proof is 15.
% 221.17/33.20 % Maximum clause weight is 118.000.
% 221.17/33.20 % Given clauses 2205.
% 221.17/33.20
% 221.17/33.20 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------