%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT287+2 : 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:01 AM UTC 2026
% Result : Theorem 194.74s 28.85s
% Output : CNFRefutation 194.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 17
% Syntax : Number of formulae : 98 ( 46 unt; 0 def)
% Number of atoms : 261 ( 37 equ)
% Maximal formula atoms : 33 ( 2 avg)
% Number of connectives : 256 ( 93 ~; 85 |; 61 &)
% ( 1 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-2 aty)
% Number of variables : 72 ( 2 sgn 34 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(rc1_xboole_0,axiom,
? [A] : v1_xboole_0(A),
file('theBenchmark.p',rc1_xboole_0) ).
fof(d5_xboole_0,axiom,
! [A] :
( v1_xboole_0(A)
<=> A = k1_xboole_0 ),
file('theBenchmark.p',d5_xboole_0) ).
fof(t4_subset_1,axiom,
! [A] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(A)),
file('theBenchmark.p',t4_subset_1) ).
fof(d5_subset_1,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(A))
=> k3_subset_1(A,B) = k4_xboole_0(A,B) ),
file('theBenchmark.p',d5_subset_1) ).
fof(involutiveness_k3_subset_1,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(A))
=> k3_subset_1(A,k3_subset_1(A,B)) = B ),
file('theBenchmark.p',involutiveness_k3_subset_1) ).
fof(t1_subset,axiom,
! [A,B] :
( r2_hidden(A,B)
=> m1_subset_1(A,B) ),
file('theBenchmark.p',t1_subset) ).
fof(d3_pre_topc,axiom,
! [A] :
( l1_struct_0(A)
=> k2_pre_topc(A) = u1_struct_0(A) ),
file('theBenchmark.p',d3_pre_topc) ).
fof(dt_l1_pre_topc,axiom,
! [A] :
( l1_pre_topc(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l1_pre_topc) ).
fof(t8_tops_1,axiom,
! [A] :
( l1_struct_0(A)
=> k3_subset_1(u1_struct_0(A),k2_pre_topc(A)) = k1_pre_topc(A) ),
file('theBenchmark.p',t8_tops_1) ).
fof(dt_k6_lopclset,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ( l3_lattices(k6_lopclset(A))
& v10_lattices(k6_lopclset(A))
& ~ v3_struct_0(k6_lopclset(A)) ) ),
file('theBenchmark.p',dt_k6_lopclset) ).
fof(t13_lopclset,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> u1_struct_0(k6_lopclset(A)) = k1_lopclset(A) ),
file('theBenchmark.p',t13_lopclset) ).
fof(t3_boole,axiom,
! [A] : k4_xboole_0(A,k1_xboole_0) = A,
file('theBenchmark.p',t3_boole) ).
fof(dt_l2_lattices,axiom,
! [A] :
( l2_lattices(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l2_lattices) ).
fof(dt_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(rc5_tops_1,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A) )
=> ? [B] :
( v3_tops_1(B,A)
& v2_tops_1(B,A)
& v5_membered(B)
& v4_membered(B)
& v3_membered(B)
& v2_membered(B)
& v1_membered(B)
& v4_pre_topc(B,A)
& v3_pre_topc(B,A)
& v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('theBenchmark.p',rc5_tops_1) ).
fof(t4_lopclset,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( ( v4_pre_topc(B,A)
& v3_pre_topc(B,A) )
=> r2_hidden(B,k1_lopclset(A)) ) ) ),
file('theBenchmark.p',t4_lopclset) ).
fof(t16_lopclset,conjecture,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k1_pre_topc(A),u1_struct_0(k6_lopclset(A))) ),
file('theBenchmark.p',t16_lopclset) ).
fof(t16_lopclset_neg,negated_conjecture,
~ ! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k1_pre_topc(A),u1_struct_0(k6_lopclset(A))) ),
inference(assume_negation,[status(cth)],[t16_lopclset]) ).
cnf(c_1430,plain,
k4_xboole_0(A,k1_xboole_0) = A,
inference(clausify,[status(thm)],[t3_boole]) ).
cnf(c_2993,plain,
( l1_struct_0(A)
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_l2_lattices]) ).
cnf(c_2996,plain,
( l2_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
fof(nnf_1185,plain,
! [A] :
( ? [B] :
( v3_tops_1(B,A)
& v2_tops_1(B,A)
& v5_membered(B)
& v4_membered(B)
& v3_membered(B)
& v2_membered(B)
& v1_membered(B)
& v4_pre_topc(B,A)
& v3_pre_topc(B,A)
& v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A) ),
inference(fof_nnf,[status(thm)],[rc5_tops_1]) ).
fof(sk_rc5_tops_1_sk,plain,
! [A] :
( ( v3_tops_1(sK0(A),A)
& v2_tops_1(sK0(A),A)
& v5_membered(sK0(A))
& v4_membered(sK0(A))
& v3_membered(sK0(A))
& v2_membered(sK0(A))
& v1_membered(sK0(A))
& v4_pre_topc(sK0(A),A)
& v3_pre_topc(sK0(A),A)
& v1_xboole_0(sK0(A))
& m1_subset_1(sK0(A),k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(B,sK0(A))],[nnf_1185]) ).
fof(sk_rc5_tops_1,plain,
( ! [VAR_0] :
( v3_tops_1(sK0(VAR_0),VAR_0)
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v2_tops_1(sK0(VAR_0),VAR_0)
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v5_membered(sK0(VAR_0))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v4_membered(sK0(VAR_0))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v3_membered(sK0(VAR_0))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v2_membered(sK0(VAR_0))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v1_membered(sK0(VAR_0))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v4_pre_topc(sK0(VAR_0),VAR_0)
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v3_pre_topc(sK0(VAR_0),VAR_0)
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v1_xboole_0(sK0(VAR_0))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( m1_subset_1(sK0(VAR_0),k1_zfmisc_1(u1_struct_0(VAR_0)))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_rc5_tops_1_sk]) ).
cnf(c_3065,plain,
( v1_xboole_0(sK0(A))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A) ),
inference(split_conjunct,[status(thm)],[sk_rc5_tops_1]) ).
cnf(c_3066,plain,
( v3_pre_topc(sK0(A),A)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A) ),
inference(split_conjunct,[status(thm)],[sk_rc5_tops_1]) ).
cnf(c_3067,plain,
( v4_pre_topc(sK0(A),A)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A) ),
inference(split_conjunct,[status(thm)],[sk_rc5_tops_1]) ).
cnf(c_3511,plain,
( r2_hidden(B,k1_lopclset(A))
| ~ v4_pre_topc(B,A)
| ~ v3_pre_topc(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t4_lopclset]) ).
fof(nnf_5,plain,
? [A] : v1_xboole_0(A),
inference(fof_nnf,[status(thm)],[rc1_xboole_0]) ).
fof(sk_rc1_xboole_0,plain,
v1_xboole_0(sK1),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(A,sK1)],[nnf_5]) ).
cnf(c_3525,plain,
v1_xboole_0(sK1),
inference(split_conjunct,[status(thm)],[sk_rc1_xboole_0]) ).
cnf(c_3543,plain,
( k1_xboole_0 = A
| ~ v1_xboole_0(A) ),
inference(clausify,[status(thm)],[d5_xboole_0]) ).
cnf(c_3688,plain,
m1_subset_1(k1_xboole_0,k1_zfmisc_1(A)),
inference(clausify,[status(thm)],[t4_subset_1]) ).
cnf(c_3697,plain,
( k3_subset_1(B,A) = k4_xboole_0(B,A)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[d5_subset_1]) ).
cnf(c_3698,plain,
( k4_xboole_0(B,A) = k3_subset_1(B,A)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(copy,[status(thm)],[c_3697]) ).
cnf(c_3733,plain,
( k3_subset_1(B,k3_subset_1(B,A)) = A
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[involutiveness_k3_subset_1]) ).
cnf(c_3737,plain,
( m1_subset_1(A,B)
| ~ r2_hidden(A,B) ),
inference(clausify,[status(thm)],[t1_subset]) ).
cnf(c_4089,plain,
( k2_pre_topc(A) = u1_struct_0(A)
| ~ l1_struct_0(A) ),
inference(clausify,[status(thm)],[d3_pre_topc]) ).
cnf(c_4090,plain,
( u1_struct_0(A) = k2_pre_topc(A)
| ~ l1_struct_0(A) ),
inference(copy,[status(thm)],[c_4089]) ).
cnf(c_4132,plain,
( l1_struct_0(A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[dt_l1_pre_topc]) ).
cnf(c_4167,plain,
( k1_pre_topc(A) = k3_subset_1(u1_struct_0(A),k2_pre_topc(A))
| ~ l1_struct_0(A) ),
inference(clausify,[status(thm)],[t8_tops_1]) ).
cnf(c_4168,plain,
( k3_subset_1(u1_struct_0(A),k2_pre_topc(A)) = k1_pre_topc(A)
| ~ l1_struct_0(A) ),
inference(copy,[status(thm)],[c_4167]) ).
cnf(c_4298,plain,
( l3_lattices(k6_lopclset(A))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k6_lopclset]) ).
cnf(c_4322,plain,
( k1_lopclset(A) = u1_struct_0(k6_lopclset(A))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t13_lopclset]) ).
cnf(c_4323,plain,
( u1_struct_0(k6_lopclset(A)) = k1_lopclset(A)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_4322]) ).
fof(nnf_1381,plain,
? [A] :
( ~ m1_subset_1(k1_pre_topc(A),u1_struct_0(k6_lopclset(A)))
& l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t16_lopclset_neg]) ).
fof(sk_t16_lopclset_neg,plain,
( ~ m1_subset_1(k1_pre_topc(sK2),u1_struct_0(k6_lopclset(sK2)))
& l1_pre_topc(sK2)
& v2_pre_topc(sK2)
& ~ v3_struct_0(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(A,sK2)],[nnf_1381]) ).
cnf(c_4326,negated_conjecture,
~ v3_struct_0(sK2),
inference(split_conjunct,[status(thm)],[sk_t16_lopclset_neg]) ).
cnf(c_4327,negated_conjecture,
v2_pre_topc(sK2),
inference(split_conjunct,[status(thm)],[sk_t16_lopclset_neg]) ).
cnf(c_4328,negated_conjecture,
l1_pre_topc(sK2),
inference(split_conjunct,[status(thm)],[sk_t16_lopclset_neg]) ).
cnf(c_4329,negated_conjecture,
~ m1_subset_1(k1_pre_topc(sK2),u1_struct_0(k6_lopclset(sK2))),
inference(split_conjunct,[status(thm)],[sk_t16_lopclset_neg]) ).
cnf(c_38487,negated_conjecture,
( v4_pre_topc(sK0(sK2),sK2)
| ~ l1_pre_topc(sK2) ),
inference(resolve,[status(thm)],[c_4327,c_3067]) ).
cnf(c_5004,negated_conjecture,
v4_pre_topc(sK0(sK2),sK2),
inference(resolve,[status(thm)],[c_4328,c_38487]) ).
cnf(c_38488,negated_conjecture,
( v3_pre_topc(sK0(sK2),sK2)
| ~ l1_pre_topc(sK2) ),
inference(resolve,[status(thm)],[c_4327,c_3066]) ).
cnf(c_5005,negated_conjecture,
v3_pre_topc(sK0(sK2),sK2),
inference(resolve,[status(thm)],[c_4328,c_38488]) ).
cnf(c_38489,negated_conjecture,
( v1_xboole_0(sK0(sK2))
| ~ l1_pre_topc(sK2) ),
inference(resolve,[status(thm)],[c_4327,c_3065]) ).
cnf(c_5006,negated_conjecture,
v1_xboole_0(sK0(sK2)),
inference(resolve,[status(thm)],[c_4328,c_38489]) ).
cnf(c_38490,plain,
k1_xboole_0 = sK0(sK2),
inference(resolve,[status(thm)],[c_3543,c_5006]) ).
cnf(c_10961,plain,
sK0(sK2) = k1_xboole_0,
inference(copy,[status(thm)],[c_38490]) ).
cnf(c_10963,plain,
k1_xboole_0 = sK1,
inference(resolve,[status(thm)],[c_3543,c_3525]) ).
cnf(c_38491,negated_conjecture,
v3_pre_topc(k1_xboole_0,sK2),
inference(paramod,[status(thm)],[c_10961,c_5005]) ).
cnf(c_11069,negated_conjecture,
v3_pre_topc(sK1,sK2),
inference(paramod,[status(thm)],[c_10963,c_38491]) ).
cnf(c_38492,negated_conjecture,
v4_pre_topc(k1_xboole_0,sK2),
inference(paramod,[status(thm)],[c_10961,c_5004]) ).
cnf(c_11070,negated_conjecture,
v4_pre_topc(sK1,sK2),
inference(paramod,[status(thm)],[c_10963,c_38492]) ).
cnf(c_12674,plain,
m1_subset_1(sK1,k1_zfmisc_1(A)),
inference(paramod,[status(thm)],[c_10963,c_3688]) ).
cnf(c_12855,plain,
k4_xboole_0(A,sK1) = A,
inference(paramod,[status(thm)],[c_10963,c_1430]) ).
cnf(c_38493,plain,
( r2_hidden(sK1,k1_lopclset(sK2))
| ~ v3_pre_topc(sK1,sK2)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_11070,c_3511]) ).
cnf(c_38494,negated_conjecture,
( r2_hidden(sK1,k1_lopclset(sK2))
| ~ v3_pre_topc(sK1,sK2)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2) ),
inference(resolve,[status(thm)],[c_4326,c_38493]) ).
cnf(c_38495,negated_conjecture,
( r2_hidden(sK1,k1_lopclset(sK2))
| ~ v3_pre_topc(sK1,sK2)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l1_pre_topc(sK2) ),
inference(resolve,[status(thm)],[c_4327,c_38494]) ).
cnf(c_38496,negated_conjecture,
( r2_hidden(sK1,k1_lopclset(sK2))
| ~ v3_pre_topc(sK1,sK2)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(resolve,[status(thm)],[c_4328,c_38495]) ).
cnf(c_38497,negated_conjecture,
( r2_hidden(sK1,k1_lopclset(sK2))
| ~ v3_pre_topc(sK1,sK2) ),
inference(resolve,[status(thm)],[c_12674,c_38496]) ).
cnf(c_16178,negated_conjecture,
r2_hidden(sK1,k1_lopclset(sK2)),
inference(resolve,[status(thm)],[c_11069,c_38497]) ).
cnf(c_38498,plain,
k4_xboole_0(A,sK1) = k3_subset_1(A,sK1),
inference(resolve,[status(thm)],[c_12674,c_3698]) ).
cnf(c_38499,plain,
A = k3_subset_1(A,sK1),
inference(paramod,[status(thm)],[c_12855,c_38498]) ).
cnf(c_19629,plain,
k3_subset_1(A,sK1) = A,
inference(copy,[status(thm)],[c_38499]) ).
cnf(c_38500,plain,
k3_subset_1(A,k3_subset_1(A,sK1)) = sK1,
inference(resolve,[status(thm)],[c_3733,c_12674]) ).
cnf(c_22587,plain,
k3_subset_1(A,A) = sK1,
inference(paramod,[status(thm)],[c_19629,c_38500]) ).
cnf(c_23658,plain,
m1_subset_1(sK1,k1_lopclset(sK2)),
inference(resolve,[status(thm)],[c_3737,c_16178]) ).
cnf(c_36076,plain,
l1_struct_0(sK2),
inference(resolve,[status(thm)],[c_4132,c_4328]) ).
cnf(c_36078,plain,
u1_struct_0(sK2) = k2_pre_topc(sK2),
inference(resolve,[status(thm)],[c_36076,c_4090]) ).
cnf(c_38501,plain,
k3_subset_1(u1_struct_0(sK2),k2_pre_topc(sK2)) = k1_pre_topc(sK2),
inference(resolve,[status(thm)],[c_4168,c_36076]) ).
cnf(c_38502,plain,
k3_subset_1(k2_pre_topc(sK2),k2_pre_topc(sK2)) = k1_pre_topc(sK2),
inference(paramod,[status(thm)],[c_36078,c_38501]) ).
cnf(c_38503,plain,
sK1 = k1_pre_topc(sK2),
inference(paramod,[status(thm)],[c_22587,c_38502]) ).
cnf(c_37730,plain,
k1_pre_topc(sK2) = sK1,
inference(copy,[status(thm)],[c_38503]) ).
cnf(c_37741,negated_conjecture,
~ m1_subset_1(sK1,u1_struct_0(k6_lopclset(sK2))),
inference(paramod,[status(thm)],[c_37730,c_4329]) ).
cnf(c_38504,negated_conjecture,
( l3_lattices(k6_lopclset(sK2))
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_4298,c_4327]) ).
cnf(c_38505,negated_conjecture,
( l3_lattices(k6_lopclset(sK2))
| ~ l1_pre_topc(sK2) ),
inference(resolve,[status(thm)],[c_4326,c_38504]) ).
cnf(c_38363,negated_conjecture,
l3_lattices(k6_lopclset(sK2)),
inference(resolve,[status(thm)],[c_4328,c_38505]) ).
cnf(c_38380,plain,
l2_lattices(k6_lopclset(sK2)),
inference(resolve,[status(thm)],[c_38363,c_2996]) ).
cnf(c_38393,plain,
l1_struct_0(k6_lopclset(sK2)),
inference(resolve,[status(thm)],[c_38380,c_2993]) ).
cnf(c_38395,plain,
u1_struct_0(k6_lopclset(sK2)) = k2_pre_topc(k6_lopclset(sK2)),
inference(resolve,[status(thm)],[c_38393,c_4090]) ).
cnf(c_38410,negated_conjecture,
~ m1_subset_1(sK1,k2_pre_topc(k6_lopclset(sK2))),
inference(paramod,[status(thm)],[c_38395,c_37741]) ).
cnf(c_38506,negated_conjecture,
( u1_struct_0(k6_lopclset(sK2)) = k1_lopclset(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_4323,c_4327]) ).
cnf(c_38507,negated_conjecture,
( k2_pre_topc(k6_lopclset(sK2)) = k1_lopclset(sK2)
| ~ l1_pre_topc(sK2)
| v3_struct_0(sK2) ),
inference(paramod,[status(thm)],[c_38395,c_38506]) ).
cnf(c_38508,negated_conjecture,
( k2_pre_topc(k6_lopclset(sK2)) = k1_lopclset(sK2)
| ~ l1_pre_topc(sK2) ),
inference(resolve,[status(thm)],[c_4326,c_38507]) ).
cnf(c_38485,negated_conjecture,
k2_pre_topc(k6_lopclset(sK2)) = k1_lopclset(sK2),
inference(resolve,[status(thm)],[c_4328,c_38508]) ).
cnf(c_38509,negated_conjecture,
~ m1_subset_1(sK1,k1_lopclset(sK2)),
inference(paramod,[status(thm)],[c_38485,c_38410]) ).
cnf(c_38486,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_23658,c_38509]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT287+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.41 % Computer : n019.cluster.edu
% 0.13/0.41 % Model : x86_64 x86_64
% 0.13/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.41 % Memory : 8046.5625MB
% 0.13/0.41 % OS : Linux 6.8.0-71-generic
% 0.13/0.41 % CPULimit : 300
% 0.13/0.41 % WCLimit : 300
% 0.13/0.41 % DateTime : Fri Sep 25 20:27:34 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.42 % Process 3600917 was started by sandbox2 on n019,
% 0.13/0.42 % Fri Sep 25 20:27:34 2026
% 0.13/0.42 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 194.74/28.85
% 194.74/28.85 % SInE (scan): 1108 to sos (tol 1.5x), 315 to usable (tol 2.0x), 5004 zapped, of 6427 axioms (depth 3).
% 194.74/28.85
% 194.74/28.85 % From the command line: assign(max_seconds, 300).
% 194.74/28.85
% 194.74/28.85 % given #500 (F,wt=44): 15608 -r2_hidden(A,k3_tarski(k2_tarski(k4_xboole_0(k2_zfmisc_1(k1_tarski(B),k1_tarski(C)),k1_tarski(k4_tarski(B,C))),k4_xboole_0(k2_zfmisc_1(k1_tarski(D),k1_tarski(C)),k1_tarski(k4_tarski(B,C)))))) | -r2_hidden(A,k3_tarski(k2_tarski(k2_zfmisc_1(k1_tarski(B),k1_tarski(C)),k2_zfmisc_1(k1_tarski(D),k1_tarski(C))))) | -r2_hidden(A,k1_tarski(k4_tarski(B,C))). [back_rewrite(13422),rewrite([15101(18)])].
% 194.74/28.85
% 194.74/28.85 % given #1000 (W,wt=3): 24099 v2_ordinal1(k1_ordinal1(c3)). [resolve(23949,a,2134,a)].
% 194.74/28.85
% 194.74/28.85 % given #1500 (F,wt=9): 28077 k4_xboole_0(k1_tarski(k1_card_1(c1)),k4_numbers) != k1_tarski(k1_card_1(c1)). [resolve(17747,a,1609,b)].
% 194.74/28.85
% 194.74/28.85 % given #2000 (T,wt=4): 25569 v1_funct_1(f269(k1_relat_1(c3))). [resolve(24298,a,2725,a)].
% 194.74/28.85
% 194.74/28.85 % given #2500 (F,wt=7): 34320 -r2_hidden(k1_numbers,c18) | -r2_hidden(k2_numbers,f4(k5_ordinal2)). [resolve(34305,a,25324,b)].
% 194.74/28.85
% 194.74/28.85 % given #3000 (T,wt=4): 30770 r1_tarski(f251(k1_numbers),k1_numbers). [resolve(3965,a,26835,a)].
% 194.74/28.85
% 194.74/28.85 % SZS status Theorem for theBenchmark
% 194.74/28.85
% 194.74/28.85 % Proof 1 at 24.88 (+ 2.50) seconds.
% 194.74/28.85 % Length of proof is 67.
% 194.74/28.85 % Level of proof is 9.
% 194.74/28.85 % Maximum clause weight is 111.000.
% 194.74/28.85 % Given clauses 3322.
% 194.74/28.85
% 194.74/28.85 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------