%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT288+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 : 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:02 AM UTC 2026
% Result : Theorem 35.56s 5.62s
% Output : CNFRefutation 35.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 5
% Syntax : Number of formulae : 69 ( 17 unt; 0 def)
% Number of atoms : 348 ( 30 equ)
% Maximal formula atoms : 43 ( 5 avg)
% Number of connectives : 464 ( 185 ~; 212 |; 56 &)
% ( 3 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-3 aty)
% Number of variables : 116 ( 0 sgn 50 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d3_tarski,axiom,
! [A,B] :
( r1_tarski(A,B)
<=> ! [C] :
( r2_hidden(C,A)
=> r2_hidden(C,B) ) ),
file('theBenchmark.p',d3_tarski) ).
fof(d5_lopclset,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k7_lopclset(A) = a_1_1_lopclset(A) ),
file('theBenchmark.p',d5_lopclset) ).
fof(fraenkel_a_1_1_lopclset,axiom,
! [A,B] :
( ( l3_lattices(B)
& ~ v3_realset2(B)
& v17_lattices(B)
& v10_lattices(B)
& ~ v3_struct_0(B) )
=> ( r2_hidden(A,a_1_1_lopclset(B))
<=> ? [C] :
( v1_filter_0(C,B)
& A = C
& m1_filter_0(C,B) ) ) ),
file('theBenchmark.p',fraenkel_a_1_1_lopclset) ).
fof(fraenkel_a_2_0_lopclset,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(B))
& l3_lattices(B)
& ~ v3_realset2(B)
& v17_lattices(B)
& v10_lattices(B)
& ~ v3_struct_0(B) )
=> ( r2_hidden(A,a_2_0_lopclset(B,C))
<=> ? [D] :
( r2_hidden(C,D)
& v1_filter_0(D,B)
& A = D
& m1_filter_0(D,B) ) ) ),
file('theBenchmark.p',fraenkel_a_2_0_lopclset) ).
fof(t19_lopclset,conjecture,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> r1_tarski(a_2_0_lopclset(A,B),k7_lopclset(A)) ) ),
file('theBenchmark.p',t19_lopclset) ).
fof(t19_lopclset_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> r1_tarski(a_2_0_lopclset(A,B),k7_lopclset(A)) ) ),
inference(assume_negation,[status(cth)],[t19_lopclset]) ).
cnf(c_84,plain,
( a_1_1_lopclset(A) = k7_lopclset(A)
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d5_lopclset]) ).
cnf(c_93,plain,
( ~ v1_filter_0(C,A)
| C != B
| ~ m1_filter_0(C,A)
| r2_hidden(B,a_1_1_lopclset(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fraenkel_a_1_1_lopclset]) ).
fof(nnf_51,plain,
! [A,B,C] :
( ( ( ! [D] :
( ~ r2_hidden(C,D)
| ~ v1_filter_0(D,B)
| D != A
| ~ m1_filter_0(D,B) )
| r2_hidden(A,a_2_0_lopclset(B,C)) )
& ( ? [X0] :
( r2_hidden(C,X0)
& v1_filter_0(X0,B)
& X0 = A
& m1_filter_0(X0,B) )
| ~ r2_hidden(A,a_2_0_lopclset(B,C)) ) )
| ~ m1_subset_1(C,u1_struct_0(B))
| ~ l3_lattices(B)
| v3_realset2(B)
| ~ v17_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) ),
inference(fof_nnf,[status(thm)],[fraenkel_a_2_0_lopclset]) ).
fof(sk_fraenkel_a_2_0_lopclset_sk,plain,
! [A,B,C] :
( ( ( ! [D] :
( ~ r2_hidden(C,D)
| ~ v1_filter_0(D,B)
| D != A
| ~ m1_filter_0(D,B) )
| r2_hidden(A,a_2_0_lopclset(B,C)) )
& ( ( r2_hidden(C,sK0(A,B,C))
& v1_filter_0(sK0(A,B,C),B)
& sK0(A,B,C) = A
& m1_filter_0(sK0(A,B,C),B) )
| ~ r2_hidden(A,a_2_0_lopclset(B,C)) ) )
| ~ m1_subset_1(C,u1_struct_0(B))
| ~ l3_lattices(B)
| v3_realset2(B)
| ~ v17_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0(A,B,C))],[nnf_51]) ).
fof(sk_fraenkel_a_2_0_lopclset,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ r2_hidden(VAR_1,VAR_3)
| ~ v1_filter_0(VAR_3,VAR_0)
| VAR_3 != VAR_2
| ~ m1_filter_0(VAR_3,VAR_0)
| r2_hidden(VAR_2,a_2_0_lopclset(VAR_0,VAR_1))
| ~ m1_subset_1(VAR_1,u1_struct_0(VAR_0))
| ~ l3_lattices(VAR_0)
| v3_realset2(VAR_0)
| ~ v17_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( r2_hidden(VAR_1,sK0(VAR_2,VAR_0,VAR_1))
| ~ r2_hidden(VAR_2,a_2_0_lopclset(VAR_0,VAR_1))
| ~ m1_subset_1(VAR_1,u1_struct_0(VAR_0))
| ~ l3_lattices(VAR_0)
| v3_realset2(VAR_0)
| ~ v17_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( v1_filter_0(sK0(VAR_2,VAR_0,VAR_1),VAR_0)
| ~ r2_hidden(VAR_2,a_2_0_lopclset(VAR_0,VAR_1))
| ~ m1_subset_1(VAR_1,u1_struct_0(VAR_0))
| ~ l3_lattices(VAR_0)
| v3_realset2(VAR_0)
| ~ v17_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK0(VAR_2,VAR_0,VAR_1) = VAR_2
| ~ r2_hidden(VAR_2,a_2_0_lopclset(VAR_0,VAR_1))
| ~ m1_subset_1(VAR_1,u1_struct_0(VAR_0))
| ~ l3_lattices(VAR_0)
| v3_realset2(VAR_0)
| ~ v17_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( m1_filter_0(sK0(VAR_2,VAR_0,VAR_1),VAR_0)
| ~ r2_hidden(VAR_2,a_2_0_lopclset(VAR_0,VAR_1))
| ~ m1_subset_1(VAR_1,u1_struct_0(VAR_0))
| ~ l3_lattices(VAR_0)
| v3_realset2(VAR_0)
| ~ v17_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_fraenkel_a_2_0_lopclset_sk]) ).
cnf(c_94,plain,
( m1_filter_0(sK0(C,A,B),A)
| ~ r2_hidden(C,a_2_0_lopclset(A,B))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_fraenkel_a_2_0_lopclset]) ).
cnf(c_95,plain,
( sK0(C,A,B) = C
| ~ r2_hidden(C,a_2_0_lopclset(A,B))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_fraenkel_a_2_0_lopclset]) ).
cnf(c_96,plain,
( v1_filter_0(sK0(C,A,B),A)
| ~ r2_hidden(C,a_2_0_lopclset(A,B))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_fraenkel_a_2_0_lopclset]) ).
fof(nnf_69,plain,
? [A] :
( ? [B] :
( ~ r1_tarski(a_2_0_lopclset(A,B),k7_lopclset(A))
& m1_subset_1(B,u1_struct_0(A)) )
& l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t19_lopclset_neg]) ).
fof(sk_t19_lopclset_neg,plain,
( ~ r1_tarski(a_2_0_lopclset(sK1,sK3),k7_lopclset(sK1))
& m1_subset_1(sK3,u1_struct_0(sK1))
& l3_lattices(sK1)
& ~ v3_realset2(sK1)
& v17_lattices(sK1)
& v10_lattices(sK1)
& ~ v3_struct_0(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK3]),skolemize(A,sK1),skolemize(B,sK3)],[nnf_69]) ).
cnf(c_100,negated_conjecture,
v10_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t19_lopclset_neg]) ).
fof(nnf_28,plain,
! [A,B] :
( ( ? [C] :
( ~ r2_hidden(C,B)
& r2_hidden(C,A) )
| r1_tarski(A,B) )
& ( ! [X0] :
( r2_hidden(X0,B)
| ~ r2_hidden(X0,A) )
| ~ r1_tarski(A,B) ) ),
inference(fof_nnf,[status(thm)],[d3_tarski]) ).
fof(sk_d3_tarski_sk,plain,
! [A,B] :
( ( ( ~ r2_hidden(sK2(A,B),B)
& r2_hidden(sK2(A,B),A) )
| r1_tarski(A,B) )
& ( ! [X0] :
( r2_hidden(X0,B)
| ~ r2_hidden(X0,A) )
| ~ r1_tarski(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(C,sK2(A,B))],[nnf_28]) ).
fof(sk_d3_tarski,plain,
( ! [VAR_0,VAR_1] :
( ~ r2_hidden(sK2(VAR_0,VAR_1),VAR_1)
| r1_tarski(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( r2_hidden(sK2(VAR_0,VAR_1),VAR_0)
| r1_tarski(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( r2_hidden(VAR_2,VAR_1)
| ~ r2_hidden(VAR_2,VAR_0)
| ~ r1_tarski(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_d3_tarski_sk]) ).
cnf(c_274,plain,
( r2_hidden(sK2(A,B),A)
| r1_tarski(A,B) ),
inference(split_conjunct,[status(thm)],[sk_d3_tarski]) ).
cnf(c_275,plain,
( ~ r2_hidden(sK2(A,B),B)
| r1_tarski(A,B) ),
inference(split_conjunct,[status(thm)],[sk_d3_tarski]) ).
cnf(c_322,negated_conjecture,
~ v3_struct_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t19_lopclset_neg]) ).
cnf(c_323,negated_conjecture,
v17_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t19_lopclset_neg]) ).
cnf(c_324,negated_conjecture,
~ v3_realset2(sK1),
inference(split_conjunct,[status(thm)],[sk_t19_lopclset_neg]) ).
cnf(c_325,negated_conjecture,
l3_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t19_lopclset_neg]) ).
cnf(c_326,negated_conjecture,
m1_subset_1(sK3,u1_struct_0(sK1)),
inference(split_conjunct,[status(thm)],[sk_t19_lopclset_neg]) ).
cnf(c_327,negated_conjecture,
~ r1_tarski(a_2_0_lopclset(sK1,sK3),k7_lopclset(sK1)),
inference(split_conjunct,[status(thm)],[sk_t19_lopclset_neg]) ).
cnf(c_372,negated_conjecture,
( v1_filter_0(sK0(B,sK1,A),sK1)
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| v3_realset2(sK1)
| ~ v17_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_100,c_96]) ).
cnf(c_21487,negated_conjecture,
( v1_filter_0(sK0(B,sK1,A),sK1)
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| v3_realset2(sK1)
| ~ v17_lattices(sK1) ),
inference(resolve,[status(thm)],[c_322,c_372]) ).
cnf(c_21488,negated_conjecture,
( v1_filter_0(sK0(B,sK1,A),sK1)
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| v3_realset2(sK1) ),
inference(resolve,[status(thm)],[c_323,c_21487]) ).
cnf(c_21489,negated_conjecture,
( v1_filter_0(sK0(B,sK1,A),sK1)
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_324,c_21488]) ).
cnf(c_373,negated_conjecture,
( v1_filter_0(sK0(B,sK1,A),sK1)
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_325,c_21489]) ).
cnf(c_374,negated_conjecture,
( sK0(B,sK1,A) = B
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| v3_realset2(sK1)
| ~ v17_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_100,c_95]) ).
cnf(c_21490,negated_conjecture,
( sK0(B,sK1,A) = B
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| v3_realset2(sK1)
| ~ v17_lattices(sK1) ),
inference(resolve,[status(thm)],[c_322,c_374]) ).
cnf(c_21491,negated_conjecture,
( sK0(B,sK1,A) = B
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| v3_realset2(sK1) ),
inference(resolve,[status(thm)],[c_323,c_21490]) ).
cnf(c_21492,negated_conjecture,
( sK0(B,sK1,A) = B
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_324,c_21491]) ).
cnf(c_375,negated_conjecture,
( sK0(B,sK1,A) = B
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_325,c_21492]) ).
cnf(c_376,negated_conjecture,
( m1_filter_0(sK0(B,sK1,A),sK1)
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| v3_realset2(sK1)
| ~ v17_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_100,c_94]) ).
cnf(c_21493,negated_conjecture,
( m1_filter_0(sK0(B,sK1,A),sK1)
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| v3_realset2(sK1)
| ~ v17_lattices(sK1) ),
inference(resolve,[status(thm)],[c_322,c_376]) ).
cnf(c_21494,negated_conjecture,
( m1_filter_0(sK0(B,sK1,A),sK1)
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| v3_realset2(sK1) ),
inference(resolve,[status(thm)],[c_323,c_21493]) ).
cnf(c_21495,negated_conjecture,
( m1_filter_0(sK0(B,sK1,A),sK1)
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_324,c_21494]) ).
cnf(c_377,negated_conjecture,
( m1_filter_0(sK0(B,sK1,A),sK1)
| ~ r2_hidden(B,a_2_0_lopclset(sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_325,c_21495]) ).
cnf(c_378,negated_conjecture,
( ~ v1_filter_0(B,sK1)
| B != A
| ~ m1_filter_0(B,sK1)
| r2_hidden(A,a_1_1_lopclset(sK1))
| ~ l3_lattices(sK1)
| v3_realset2(sK1)
| ~ v17_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_100,c_93]) ).
cnf(c_21496,negated_conjecture,
( ~ v1_filter_0(B,sK1)
| B != A
| ~ m1_filter_0(B,sK1)
| r2_hidden(A,a_1_1_lopclset(sK1))
| ~ l3_lattices(sK1)
| v3_realset2(sK1)
| ~ v17_lattices(sK1) ),
inference(resolve,[status(thm)],[c_322,c_378]) ).
cnf(c_21497,negated_conjecture,
( ~ v1_filter_0(B,sK1)
| B != A
| ~ m1_filter_0(B,sK1)
| r2_hidden(A,a_1_1_lopclset(sK1))
| ~ l3_lattices(sK1)
| v3_realset2(sK1) ),
inference(resolve,[status(thm)],[c_323,c_21496]) ).
cnf(c_21498,negated_conjecture,
( ~ v1_filter_0(B,sK1)
| B != A
| ~ m1_filter_0(B,sK1)
| r2_hidden(A,a_1_1_lopclset(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_324,c_21497]) ).
cnf(c_379,negated_conjecture,
( ~ v1_filter_0(B,sK1)
| B != A
| ~ m1_filter_0(B,sK1)
| r2_hidden(A,a_1_1_lopclset(sK1)) ),
inference(resolve,[status(thm)],[c_325,c_21498]) ).
cnf(c_396,negated_conjecture,
( a_1_1_lopclset(sK1) = k7_lopclset(sK1)
| ~ l3_lattices(sK1)
| v3_realset2(sK1)
| ~ v17_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_100,c_84]) ).
cnf(c_21499,negated_conjecture,
( k7_lopclset(sK1) = a_1_1_lopclset(sK1)
| ~ l3_lattices(sK1)
| v3_realset2(sK1)
| ~ v17_lattices(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_396]) ).
cnf(c_21500,negated_conjecture,
( k7_lopclset(sK1) = a_1_1_lopclset(sK1)
| ~ l3_lattices(sK1)
| v3_realset2(sK1)
| ~ v17_lattices(sK1) ),
inference(resolve,[status(thm)],[c_322,c_21499]) ).
cnf(c_21501,negated_conjecture,
( k7_lopclset(sK1) = a_1_1_lopclset(sK1)
| ~ l3_lattices(sK1)
| v3_realset2(sK1) ),
inference(resolve,[status(thm)],[c_323,c_21500]) ).
cnf(c_21502,negated_conjecture,
( k7_lopclset(sK1) = a_1_1_lopclset(sK1)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_324,c_21501]) ).
cnf(c_397,negated_conjecture,
k7_lopclset(sK1) = a_1_1_lopclset(sK1),
inference(resolve,[status(thm)],[c_325,c_21502]) ).
cnf(c_435,negated_conjecture,
~ r1_tarski(a_2_0_lopclset(sK1,sK3),a_1_1_lopclset(sK1)),
inference(paramod,[status(thm)],[c_397,c_327]) ).
cnf(c_595,plain,
( v1_filter_0(sK0(A,sK1,sK3),sK1)
| ~ r2_hidden(A,a_2_0_lopclset(sK1,sK3)) ),
inference(resolve,[status(thm)],[c_373,c_326]) ).
cnf(c_599,plain,
( sK0(A,sK1,sK3) = A
| ~ r2_hidden(A,a_2_0_lopclset(sK1,sK3)) ),
inference(resolve,[status(thm)],[c_375,c_326]) ).
cnf(c_608,plain,
( ~ v1_filter_0(A,sK1)
| ~ m1_filter_0(A,sK1)
| r2_hidden(A,a_1_1_lopclset(sK1)) ),
inference(xxres,[status(thm)],[c_379]) ).
cnf(c_716,plain,
r2_hidden(sK2(a_2_0_lopclset(sK1,sK3),a_1_1_lopclset(sK1)),a_2_0_lopclset(sK1,sK3)),
inference(resolve,[status(thm)],[c_435,c_274]) ).
cnf(c_10880,plain,
sK0(sK2(a_2_0_lopclset(sK1,sK3),a_1_1_lopclset(sK1)),sK1,sK3) = sK2(a_2_0_lopclset(sK1,sK3),a_1_1_lopclset(sK1)),
inference(resolve,[status(thm)],[c_716,c_599]) ).
cnf(c_21503,plain,
v1_filter_0(sK0(sK2(a_2_0_lopclset(sK1,sK3),a_1_1_lopclset(sK1)),sK1,sK3),sK1),
inference(resolve,[status(thm)],[c_716,c_595]) ).
cnf(c_10881,plain,
v1_filter_0(sK2(a_2_0_lopclset(sK1,sK3),a_1_1_lopclset(sK1)),sK1),
inference(paramod,[status(thm)],[c_10880,c_21503]) ).
cnf(c_21504,negated_conjecture,
( m1_filter_0(sK0(sK2(a_2_0_lopclset(sK1,sK3),a_1_1_lopclset(sK1)),sK1,sK3),sK1)
| ~ m1_subset_1(sK3,u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_716,c_377]) ).
cnf(c_21505,negated_conjecture,
( m1_filter_0(sK2(a_2_0_lopclset(sK1,sK3),a_1_1_lopclset(sK1)),sK1)
| ~ m1_subset_1(sK3,u1_struct_0(sK1)) ),
inference(paramod,[status(thm)],[c_10880,c_21504]) ).
cnf(c_10887,negated_conjecture,
m1_filter_0(sK2(a_2_0_lopclset(sK1,sK3),a_1_1_lopclset(sK1)),sK1),
inference(resolve,[status(thm)],[c_326,c_21505]) ).
cnf(c_21506,plain,
( ~ m1_filter_0(sK2(a_2_0_lopclset(sK1,sK3),a_1_1_lopclset(sK1)),sK1)
| r2_hidden(sK2(a_2_0_lopclset(sK1,sK3),a_1_1_lopclset(sK1)),a_1_1_lopclset(sK1)) ),
inference(resolve,[status(thm)],[c_10881,c_608]) ).
cnf(c_16436,plain,
r2_hidden(sK2(a_2_0_lopclset(sK1,sK3),a_1_1_lopclset(sK1)),a_1_1_lopclset(sK1)),
inference(resolve,[status(thm)],[c_10887,c_21506]) ).
cnf(c_21507,plain,
r1_tarski(a_2_0_lopclset(sK1,sK3),a_1_1_lopclset(sK1)),
inference(resolve,[status(thm)],[c_16436,c_275]) ).
cnf(c_21486,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_435,c_21507]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT288+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.16/0.41 % Computer : n019.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Fri Sep 25 20:28:18 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.42 % Process 3603226 was started by sandbox2 on n019,
% 0.16/0.42 % Fri Sep 25 20:28:18 2026
% 0.16/0.42 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.16/0.45
% 0.16/0.45 % From the command line: assign(max_seconds, 300).
% 35.56/5.62
% 35.56/5.62 % given #500 (T,wt=20): 840 v1_xboole_0(A) | -r1_tarski(k1_zfmisc_1(A),B) | r2_hidden(f6(A),B). [resolve(521,a,273,b)].
% 35.56/5.62
% 35.56/5.62 % given #1000 (T,wt=22): 9048 v1_xboole_0(A) | r2_hidden(f1(A,B),A) | m1_subset_1(f1(B,k1_xboole_0),B). [resolve(4793,c,311,a)].
% 35.56/5.62
% 35.56/5.62 % given #1500 (T,wt=24): 11487 r2_hidden(f1(a_2_0_lopclset(c9,c10),c10),a_2_0_lopclset(c9,c10)). [resolve(10915,a,4850,c),unit_del(a,10890)].
% 35.56/5.62
% 35.56/5.62 % SZS status Theorem for theBenchmark
% 35.56/5.62
% 35.56/5.62 % Proof 1 at 3.85 (+ 1.20) seconds.
% 35.56/5.62 % Length of proof is 39.
% 35.56/5.62 % Level of proof is 9.
% 35.56/5.62 % Maximum clause weight is 36.000.
% 35.56/5.62 % Given clauses 1635.
% 35.56/5.62
% 35.56/5.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------