%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT304+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 : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:50:07 AM UTC 2026
% Result : Theorem 9.77s 1.78s
% Output : CNFRefutation 9.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 14
% Syntax : Number of formulae : 88 ( 21 unt; 0 def)
% Number of atoms : 263 ( 33 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 295 ( 120 ~; 115 |; 41 &)
% ( 3 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 1 con; 0-3 aty)
% Number of variables : 94 ( 18 sgn 24 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(abstractness_v3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( v3_lattices(A)
=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ),
file('theBenchmark.p',abstractness_v3_lattices) ).
fof(d2_lattice2,axiom,
! [A] :
( l3_lattices(A)
=> k1_lattice2(A) = g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) ),
file('theBenchmark.p',d2_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(dt_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(dt_u1_lattices,axiom,
! [A] :
( l1_lattices(A)
=> ( m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u1_lattices(A)) ) ),
file('theBenchmark.p',dt_u1_lattices) ).
fof(dt_u2_lattices,axiom,
! [A] :
( l2_lattices(A)
=> ( m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u2_lattices(A)) ) ),
file('theBenchmark.p',dt_u2_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(free_g3_lattices,axiom,
! [A,B,C] :
( ( m1_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C)
& m1_relset_1(B,k2_zfmisc_1(A,A),A)
& v1_funct_2(B,k2_zfmisc_1(A,A),A)
& v1_funct_1(B) )
=> ! [D,E,F] :
( g3_lattices(A,B,C) = g3_lattices(D,E,F)
=> ( C = F
& B = E
& A = D ) ) ),
file('theBenchmark.p',free_g3_lattices) ).
fof(redefinition_m1_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_2(B,A)
<=> m1_filter_0(B,A) ) ),
file('theBenchmark.p',redefinition_m1_filter_2) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
fof(t15_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_filter_0(u1_struct_0(A),A) ),
file('theBenchmark.p',t15_filter_0) ).
fof(t21_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
<=> m1_filter_2(B,k1_lattice2(A)) ) ),
file('theBenchmark.p',t21_filter_2) ).
fof(t28_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m2_filter_2(u1_struct_0(A),A) ),
file('theBenchmark.p',t28_filter_2) ).
fof(t28_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m2_filter_2(u1_struct_0(A),A) ),
inference(assume_negation,[status(cth)],[t28_filter_2]) ).
cnf(c_78,plain,
( g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = A
| ~ v3_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[abstractness_v3_lattices]) ).
cnf(c_79,plain,
( v3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_106,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_108,plain,
( v1_funct_1(u1_lattices(A))
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_u1_lattices]) ).
cnf(c_109,plain,
( v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_u1_lattices]) ).
cnf(c_110,plain,
( m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_u1_lattices]) ).
cnf(c_132,plain,
( ~ m1_filter_0(B,A)
| m1_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_m1_filter_2]) ).
cnf(c_133,plain,
( m1_filter_0(u1_struct_0(A),A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t15_filter_0]) ).
cnf(c_139,plain,
( m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_u2_lattices]) ).
cnf(c_142,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_144,plain,
( ~ l3_lattices(A)
| m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ),
inference(resolve,[status(thm)],[c_110,c_106]) ).
cnf(c_151,plain,
( ~ l2_lattices(A)
| m1_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ),
inference(resolve,[status(thm)],[c_142,c_139]) ).
cnf(c_152,plain,
( v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_u2_lattices]) ).
cnf(c_153,plain,
( v1_funct_1(u2_lattices(A))
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_u2_lattices]) ).
cnf(c_154,plain,
( l2_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_170,plain,
( m1_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_154,c_151]) ).
cnf(c_172,plain,
( v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_154,c_152]) ).
cnf(c_173,plain,
( v1_funct_1(u2_lattices(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_154,c_153]) ).
cnf(c_204,plain,
( k1_lattice2(A) = g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[d2_lattice2]) ).
cnf(c_205,plain,
( g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) = k1_lattice2(A)
| ~ l3_lattices(A) ),
inference(copy,[status(thm)],[c_204]) ).
cnf(c_207,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_215,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_225,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_226,plain,
( D = B
| g3_lattices(D,E,F) != g3_lattices(B,A,C)
| ~ m1_relset_1(C,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(C,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(C)
| ~ m1_relset_1(A,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(A,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(A) ),
inference(clausify,[status(thm)],[free_g3_lattices]) ).
cnf(c_254,plain,
( ~ m1_filter_2(B,k1_lattice2(A))
| m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t21_filter_2]) ).
fof(nnf_76,plain,
? [A] :
( ~ m2_filter_2(u1_struct_0(A),A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t28_filter_2_neg]) ).
fof(sk_t28_filter_2_neg,plain,
( ~ m2_filter_2(u1_struct_0(sK0),sK0)
& l3_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(A,sK0)],[nnf_76]) ).
cnf(c_261,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t28_filter_2_neg]) ).
cnf(c_262,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t28_filter_2_neg]) ).
cnf(c_263,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t28_filter_2_neg]) ).
cnf(c_264,negated_conjecture,
~ m2_filter_2(u1_struct_0(sK0),sK0),
inference(split_conjunct,[status(thm)],[sk_t28_filter_2_neg]) ).
cnf(c_266,plain,
( g3_lattices(u1_struct_0(k1_lattice2(A)),u2_lattices(k1_lattice2(A)),u1_lattices(k1_lattice2(A))) = k1_lattice2(A)
| ~ l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_79,c_78]) ).
cnf(c_273,plain,
( ~ l3_lattices(A)
| v1_funct_1(u1_lattices(A)) ),
inference(resolve,[status(thm)],[c_108,c_106]) ).
cnf(c_274,plain,
( ~ l3_lattices(A)
| v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ),
inference(resolve,[status(thm)],[c_109,c_106]) ).
cnf(c_285,plain,
( m1_filter_2(u1_struct_0(A),A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_133,c_132]) ).
cnf(c_4622,plain,
( m1_filter_2(u1_struct_0(A),A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_285]) ).
cnf(c_4623,plain,
( m1_filter_2(u1_struct_0(A),A)
| ~ l3_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_4622]) ).
cnf(c_286,plain,
( m1_filter_2(u1_struct_0(A),A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_4623]) ).
cnf(c_292,plain,
( m1_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_144,c_142]) ).
cnf(c_4624,negated_conjecture,
( ~ m1_filter_2(A,k1_lattice2(sK0))
| m2_filter_2(A,sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_262,c_254]) ).
cnf(c_4625,negated_conjecture,
( ~ m1_filter_2(A,k1_lattice2(sK0))
| m2_filter_2(A,sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_261,c_4624]) ).
cnf(c_571,negated_conjecture,
( ~ m1_filter_2(A,k1_lattice2(sK0))
| m2_filter_2(A,sK0) ),
inference(resolve,[status(thm)],[c_263,c_4625]) ).
cnf(c_4626,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_262,c_225]) ).
cnf(c_4627,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_261,c_4626]) ).
cnf(c_574,negated_conjecture,
v10_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_263,c_4627]) ).
cnf(c_4628,negated_conjecture,
( ~ v3_struct_0(k1_lattice2(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_263,c_215]) ).
cnf(c_593,negated_conjecture,
~ v3_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_261,c_4628]) ).
cnf(c_594,plain,
l3_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_263,c_207]) ).
cnf(c_595,plain,
g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)) = k1_lattice2(sK0),
inference(resolve,[status(thm)],[c_263,c_205]) ).
cnf(c_596,plain,
v1_funct_1(u2_lattices(sK0)),
inference(resolve,[status(thm)],[c_263,c_173]) ).
cnf(c_597,plain,
v1_funct_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_263,c_172]) ).
cnf(c_599,plain,
m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_263,c_170]) ).
cnf(c_4629,negated_conjecture,
( g3_lattices(u1_struct_0(k1_lattice2(sK0)),u2_lattices(k1_lattice2(sK0)),u1_lattices(k1_lattice2(sK0))) = k1_lattice2(sK0)
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_266,c_263]) ).
cnf(c_614,negated_conjecture,
g3_lattices(u1_struct_0(k1_lattice2(sK0)),u2_lattices(k1_lattice2(sK0)),u1_lattices(k1_lattice2(sK0))) = k1_lattice2(sK0),
inference(resolve,[status(thm)],[c_594,c_4629]) ).
cnf(c_647,plain,
v1_funct_1(u1_lattices(sK0)),
inference(resolve,[status(thm)],[c_273,c_263]) ).
cnf(c_662,plain,
v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_274,c_263]) ).
cnf(c_746,plain,
m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_292,c_263]) ).
cnf(c_4630,plain,
( m1_filter_2(u1_struct_0(k1_lattice2(sK0)),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_574,c_286]) ).
cnf(c_4631,plain,
( m1_filter_2(u1_struct_0(k1_lattice2(sK0)),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_593,c_4630]) ).
cnf(c_1105,plain,
m1_filter_2(u1_struct_0(k1_lattice2(sK0)),k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_594,c_4631]) ).
cnf(c_3201,plain,
m2_filter_2(u1_struct_0(k1_lattice2(sK0)),sK0),
inference(resolve,[status(thm)],[c_1105,c_571]) ).
cnf(c_4632,plain,
( A = u1_struct_0(sK0)
| g3_lattices(A,B,C) != k1_lattice2(sK0)
| ~ m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(u2_lattices(sK0))
| ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(u1_lattices(sK0)) ),
inference(paramod,[status(thm)],[c_595,c_226]) ).
cnf(c_4633,plain,
( u1_struct_0(sK0) = A
| g3_lattices(A,B,C) != k1_lattice2(sK0)
| ~ m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(u2_lattices(sK0))
| ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(u1_lattices(sK0)) ),
inference(copy,[status(thm)],[c_4632]) ).
cnf(c_4634,plain,
( u1_struct_0(sK0) = A
| g3_lattices(A,B,C) != k1_lattice2(sK0)
| ~ m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(u2_lattices(sK0))
| ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_647,c_4633]) ).
cnf(c_4635,plain,
( u1_struct_0(sK0) = A
| g3_lattices(A,B,C) != k1_lattice2(sK0)
| ~ m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(u2_lattices(sK0))
| ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_662,c_4634]) ).
cnf(c_4636,plain,
( u1_struct_0(sK0) = A
| g3_lattices(A,B,C) != k1_lattice2(sK0)
| ~ m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(u2_lattices(sK0)) ),
inference(resolve,[status(thm)],[c_746,c_4635]) ).
cnf(c_4637,plain,
( u1_struct_0(sK0) = A
| g3_lattices(A,B,C) != k1_lattice2(sK0)
| ~ m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_596,c_4636]) ).
cnf(c_4638,plain,
( u1_struct_0(sK0) = A
| g3_lattices(A,B,C) != k1_lattice2(sK0)
| ~ m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_597,c_4637]) ).
cnf(c_3499,plain,
( u1_struct_0(sK0) = A
| g3_lattices(A,B,C) != k1_lattice2(sK0) ),
inference(resolve,[status(thm)],[c_599,c_4638]) ).
cnf(c_4639,plain,
u1_struct_0(sK0) = u1_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_3499,c_614]) ).
cnf(c_4619,plain,
u1_struct_0(k1_lattice2(sK0)) = u1_struct_0(sK0),
inference(copy,[status(thm)],[c_4639]) ).
cnf(c_4640,plain,
m2_filter_2(u1_struct_0(sK0),sK0),
inference(paramod,[status(thm)],[c_4619,c_3201]) ).
cnf(c_4621,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_264,c_4640]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT304+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n005.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Fri Sep 25 20:39:01 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.45 % Process 157833 was started by sandbox2 on n005,
% 0.18/0.45 % Fri Sep 25 20:39:01 2026
% 0.18/0.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/0.48
% 0.18/0.48 % From the command line: assign(max_seconds, 300).
% 9.77/1.78
% 9.77/1.78 % given #500 (T,wt=19): 2922 k1_lattice2(c12) != c13 | u1_struct_0(c13) = u1_struct_0(c12). [para(476(a,1),753(a,1))].
% 9.77/1.78
% 9.77/1.78 % SZS status Theorem for theBenchmark
% 9.77/1.78
% 9.77/1.78 % Proof 1 at 1.01 (+ 0.25) seconds.
% 9.77/1.78 % Length of proof is 66.
% 9.77/1.78 % Level of proof is 7.
% 9.77/1.78 % Maximum clause weight is 50.000.
% 9.77/1.78 % Given clauses 822.
% 9.77/1.78
% 9.77/1.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------