%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT313+1 : 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 : n014.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:10 AM UTC 2026
% Result : Theorem 0.48s 0.47s
% Output : CNFRefutation 0.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 13
% Syntax : Number of formulae : 84 ( 22 unt; 0 def)
% Number of atoms : 267 ( 29 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 307 ( 124 ~; 122 |; 39 &)
% ( 2 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% Number of variables : 70 ( 2 sgn 25 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d8_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k17_filter_2(A) = u1_struct_0(A) ),
file('theBenchmark.p',d8_filter_2) ).
fof(dt_l1_lattices,axiom,
! [A] :
( l1_lattices(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l1_lattices) ).
fof(dt_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(dt_m2_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) ) ) ),
file('theBenchmark.p',dt_m2_filter_2) ).
fof(dt_m2_lattice4,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_lattice4(B,A)
=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('theBenchmark.p',dt_m2_lattice4) ).
fof(fc1_struct_0,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('theBenchmark.p',fc1_struct_0) ).
fof(redefinition_r1_filter_2,axiom,
! [A,B,C] :
( ( m1_subset_1(C,k1_zfmisc_1(A))
& m1_subset_1(B,k1_zfmisc_1(A))
& ~ v1_xboole_0(A) )
=> ( r1_filter_2(A,B,C)
<=> B = C ) ),
file('theBenchmark.p',redefinition_r1_filter_2) ).
fof(reflexivity_r1_tarski,axiom,
! [A,B] : r1_tarski(A,A),
file('theBenchmark.p',reflexivity_r1_tarski) ).
fof(t38_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> r1_filter_2(u1_struct_0(A),k19_filter_2(A,B),B) ) ),
file('theBenchmark.p',t38_filter_2) ).
fof(t3_subset,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('theBenchmark.p',t3_subset) ).
fof(t42_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(B) )
=> ( ( r2_hidden(k6_lattices(A),B)
& v14_lattices(A) )
=> ( k19_filter_2(A,B) = u1_struct_0(A)
& r1_filter_2(u1_struct_0(A),k19_filter_2(A,B),k17_filter_2(A)) ) ) ) ),
file('theBenchmark.p',t42_filter_2) ).
fof(t7_boole,axiom,
! [A,B] :
~ ( v1_xboole_0(B)
& r2_hidden(A,B) ),
file('theBenchmark.p',t7_boole) ).
fof(t43_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( ( r2_hidden(k6_lattices(A),B)
& v14_lattices(A) )
=> ( B = u1_struct_0(A)
& r1_filter_2(u1_struct_0(A),B,k17_filter_2(A)) ) ) ) ),
file('theBenchmark.p',t43_filter_2) ).
fof(t43_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( ( r2_hidden(k6_lattices(A),B)
& v14_lattices(A) )
=> ( B = u1_struct_0(A)
& r1_filter_2(u1_struct_0(A),B,k17_filter_2(A)) ) ) ) ),
inference(assume_negation,[status(cth)],[t43_filter_2]) ).
cnf(c_57,plain,
( k17_filter_2(A) = u1_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d8_filter_2]) ).
cnf(c_61,plain,
( m2_lattice4(B,A)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m2_filter_2]) ).
cnf(c_62,plain,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ m2_lattice4(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m2_lattice4]) ).
cnf(c_67,plain,
( r1_filter_2(u1_struct_0(A),k19_filter_2(A,B),B)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t38_filter_2]) ).
cnf(c_68,plain,
( r1_filter_2(u1_struct_0(A),k19_filter_2(A,B),k17_filter_2(A))
| ~ r2_hidden(k6_lattices(A),B)
| ~ v14_lattices(A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t42_filter_2]) ).
cnf(c_69,plain,
( k19_filter_2(A,B) = u1_struct_0(A)
| ~ r2_hidden(k6_lattices(A),B)
| ~ v14_lattices(A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t42_filter_2]) ).
fof(nnf_49,plain,
? [A] :
( ? [B] :
( ( u1_struct_0(A) != B
| ~ r1_filter_2(u1_struct_0(A),B,k17_filter_2(A)) )
& r2_hidden(k6_lattices(A),B)
& v14_lattices(A)
& m2_filter_2(B,A) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t43_filter_2_neg]) ).
fof(sk_t43_filter_2_neg,plain,
( ( u1_struct_0(sK0) != sK1
| ~ r1_filter_2(u1_struct_0(sK0),sK1,k17_filter_2(sK0)) )
& r2_hidden(k6_lattices(sK0),sK1)
& v14_lattices(sK0)
& m2_filter_2(sK1,sK0)
& l3_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(A,sK0),skolemize(B,sK1)],[nnf_49]) ).
cnf(c_70,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t43_filter_2_neg]) ).
cnf(c_89,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_90,plain,
( l1_struct_0(A)
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_l1_lattices]) ).
cnf(c_93,plain,
( l1_struct_0(A)
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_89,c_90]) ).
cnf(c_97,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_struct_0]) ).
cnf(c_101,plain,
( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[t3_subset]) ).
cnf(c_103,plain,
r1_tarski(A,A),
inference(clausify,[status(thm)],[reflexivity_r1_tarski]) ).
cnf(c_104,plain,
m1_subset_1(A,k1_zfmisc_1(A)),
inference(resolve,[status(thm)],[c_101,c_103]) ).
cnf(c_136,negated_conjecture,
( k17_filter_2(sK0) = u1_struct_0(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_70,c_57]) ).
cnf(c_140,negated_conjecture,
( m2_lattice4(A,sK0)
| ~ m2_filter_2(A,sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_70,c_61]) ).
cnf(c_141,negated_conjecture,
( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_lattice4(A,sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_70,c_62]) ).
cnf(c_146,negated_conjecture,
( r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,A),A)
| ~ m2_filter_2(A,sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_70,c_67]) ).
cnf(c_147,negated_conjecture,
( r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,A),k17_filter_2(sK0))
| ~ r2_hidden(k6_lattices(sK0),A)
| ~ v14_lattices(sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(A)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_70,c_68]) ).
cnf(c_148,negated_conjecture,
( k19_filter_2(sK0,A) = u1_struct_0(sK0)
| ~ r2_hidden(k6_lattices(sK0),A)
| ~ v14_lattices(sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(A)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_70,c_69]) ).
cnf(c_149,negated_conjecture,
( u1_struct_0(sK0) != sK1
| ~ r1_filter_2(u1_struct_0(sK0),sK1,k17_filter_2(sK0)) ),
inference(split_conjunct,[status(thm)],[sk_t43_filter_2_neg]) ).
cnf(c_150,negated_conjecture,
( sK1 != u1_struct_0(sK0)
| ~ r1_filter_2(u1_struct_0(sK0),sK1,k17_filter_2(sK0)) ),
inference(copy,[status(thm)],[c_149]) ).
cnf(c_151,negated_conjecture,
r2_hidden(k6_lattices(sK0),sK1),
inference(split_conjunct,[status(thm)],[sk_t43_filter_2_neg]) ).
cnf(c_152,negated_conjecture,
v14_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t43_filter_2_neg]) ).
cnf(c_153,negated_conjecture,
m2_filter_2(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_t43_filter_2_neg]) ).
cnf(c_154,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t43_filter_2_neg]) ).
cnf(c_155,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t43_filter_2_neg]) ).
cnf(c_157,plain,
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(clausify,[status(thm)],[t7_boole]) ).
cnf(c_166,plain,
( C = B
| ~ r1_filter_2(A,B,C)
| ~ m1_subset_1(C,k1_zfmisc_1(A))
| ~ m1_subset_1(B,k1_zfmisc_1(A))
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[redefinition_r1_filter_2]) ).
cnf(c_191,plain,
( ~ l3_lattices(A)
| ~ v1_xboole_0(u1_struct_0(A))
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_97,c_93]) ).
cnf(c_478,negated_conjecture,
( k19_filter_2(sK0,A) = u1_struct_0(sK0)
| ~ r2_hidden(k6_lattices(sK0),A)
| ~ v14_lattices(sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(A)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_155,c_148]) ).
cnf(c_479,negated_conjecture,
( k19_filter_2(sK0,A) = u1_struct_0(sK0)
| ~ r2_hidden(k6_lattices(sK0),A)
| ~ v14_lattices(sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_154,c_478]) ).
cnf(c_199,negated_conjecture,
( k19_filter_2(sK0,A) = u1_struct_0(sK0)
| ~ r2_hidden(k6_lattices(sK0),A)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_152,c_479]) ).
cnf(c_480,negated_conjecture,
( r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,A),k17_filter_2(sK0))
| ~ r2_hidden(k6_lattices(sK0),A)
| ~ v14_lattices(sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(A)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_155,c_147]) ).
cnf(c_481,negated_conjecture,
( r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,A),k17_filter_2(sK0))
| ~ r2_hidden(k6_lattices(sK0),A)
| ~ v14_lattices(sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_154,c_480]) ).
cnf(c_200,negated_conjecture,
( r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,A),k17_filter_2(sK0))
| ~ r2_hidden(k6_lattices(sK0),A)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_152,c_481]) ).
cnf(c_482,negated_conjecture,
( r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,A),A)
| ~ m2_filter_2(A,sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_155,c_146]) ).
cnf(c_201,negated_conjecture,
( r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,A),A)
| ~ m2_filter_2(A,sK0) ),
inference(resolve,[status(thm)],[c_154,c_482]) ).
cnf(c_483,negated_conjecture,
( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_lattice4(A,sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_155,c_141]) ).
cnf(c_206,negated_conjecture,
( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_lattice4(A,sK0) ),
inference(resolve,[status(thm)],[c_154,c_483]) ).
cnf(c_484,negated_conjecture,
( m2_lattice4(A,sK0)
| ~ m2_filter_2(A,sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_155,c_140]) ).
cnf(c_207,negated_conjecture,
( m2_lattice4(A,sK0)
| ~ m2_filter_2(A,sK0) ),
inference(resolve,[status(thm)],[c_154,c_484]) ).
cnf(c_485,negated_conjecture,
( k17_filter_2(sK0) = u1_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_155,c_136]) ).
cnf(c_211,negated_conjecture,
k17_filter_2(sK0) = u1_struct_0(sK0),
inference(resolve,[status(thm)],[c_154,c_485]) ).
cnf(c_220,negated_conjecture,
( r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,A),u1_struct_0(sK0))
| ~ r2_hidden(k6_lattices(sK0),A)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(A) ),
inference(paramod,[status(thm)],[c_211,c_200]) ).
cnf(c_221,negated_conjecture,
( sK1 != u1_struct_0(sK0)
| ~ r1_filter_2(u1_struct_0(sK0),sK1,u1_struct_0(sK0)) ),
inference(paramod,[status(thm)],[c_211,c_150]) ).
cnf(c_222,plain,
~ v1_xboole_0(sK1),
inference(resolve,[status(thm)],[c_157,c_151]) ).
cnf(c_486,negated_conjecture,
( ~ l3_lattices(sK0)
| ~ v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_191,c_155]) ).
cnf(c_264,negated_conjecture,
~ v1_xboole_0(u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_486,c_154]) ).
cnf(c_487,negated_conjecture,
( k19_filter_2(sK0,sK1) = u1_struct_0(sK0)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(sK1) ),
inference(resolve,[status(thm)],[c_199,c_151]) ).
cnf(c_271,negated_conjecture,
( k19_filter_2(sK0,sK1) = u1_struct_0(sK0)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_222,c_487]) ).
cnf(c_272,plain,
r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,sK1),sK1),
inference(resolve,[status(thm)],[c_201,c_153]) ).
cnf(c_278,plain,
m2_lattice4(sK1,sK0),
inference(resolve,[status(thm)],[c_207,c_153]) ).
cnf(c_488,negated_conjecture,
( r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,sK1),u1_struct_0(sK0))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(sK1) ),
inference(resolve,[status(thm)],[c_220,c_151]) ).
cnf(c_300,negated_conjecture,
( r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,sK1),u1_struct_0(sK0))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_222,c_488]) ).
cnf(c_310,plain,
m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_278,c_206]) ).
cnf(c_311,negated_conjecture,
r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,sK1),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_310,c_300]) ).
cnf(c_312,negated_conjecture,
k19_filter_2(sK0,sK1) = u1_struct_0(sK0),
inference(resolve,[status(thm)],[c_310,c_271]) ).
cnf(c_313,negated_conjecture,
r1_filter_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0)),
inference(paramod,[status(thm)],[c_312,c_311]) ).
cnf(c_314,plain,
r1_filter_2(u1_struct_0(sK0),u1_struct_0(sK0),sK1),
inference(paramod,[status(thm)],[c_312,c_272]) ).
cnf(c_489,plain,
( sK1 = u1_struct_0(sK0)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_subset_1(u1_struct_0(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_314,c_166]) ).
cnf(c_490,plain,
( sK1 = u1_struct_0(sK0)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_subset_1(u1_struct_0(sK0),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_264,c_489]) ).
cnf(c_491,plain,
( sK1 = u1_struct_0(sK0)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_104,c_490]) ).
cnf(c_464,plain,
sK1 = u1_struct_0(sK0),
inference(resolve,[status(thm)],[c_310,c_491]) ).
cnf(c_492,negated_conjecture,
( sK1 != u1_struct_0(sK0)
| ~ r1_filter_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(paramod,[status(thm)],[c_464,c_221]) ).
cnf(c_493,negated_conjecture,
( u1_struct_0(sK0) != u1_struct_0(sK0)
| ~ r1_filter_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(paramod,[status(thm)],[c_464,c_492]) ).
cnf(c_494,negated_conjecture,
~ r1_filter_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0)),
inference(copy,[status(thm)],[c_493]) ).
cnf(c_477,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_313,c_494]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT313+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n014.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 20:45:17 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 1063668 was started by sandbox on n014,
% 0.10/0.37 % Fri Sep 25 20:45:17 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.39
% 0.10/0.39 % From the command line: assign(max_seconds, 300).
% 0.48/0.47
% 0.48/0.47 % SZS status Theorem for theBenchmark
% 0.48/0.47
% 0.48/0.47 % Proof 1 at 0.06 (+ 0.01) seconds.
% 0.48/0.47 % Length of proof is 64.
% 0.48/0.47 % Level of proof is 9.
% 0.48/0.47 % Maximum clause weight is 25.000.
% 0.48/0.47 % Given clauses 129.
% 0.48/0.47
% 0.48/0.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------