%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU411+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 : n008.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 08:46:14 AM UTC 2026
% Result : Theorem 22.09s 3.60s
% Output : CNFRefutation 22.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 19
% Syntax : Number of formulae : 105 ( 43 unt; 0 def)
% Number of atoms : 343 ( 49 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 370 ( 132 ~; 124 |; 90 &)
% ( 5 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-3 aty)
% Number of variables : 174 ( 23 sgn 69 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k3_xboole_0,axiom,
! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A),
file('theBenchmark.p',commutativity_k3_xboole_0) ).
fof(d19_waybel_0,axiom,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v12_waybel_0(B,A)
<=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ( ( r1_orders_2(A,D,C)
& r2_hidden(C,B) )
=> r2_hidden(D,B) ) ) ) ) ) ),
file('theBenchmark.p',d19_waybel_0) ).
fof(d1_xboole_0,axiom,
! [A] :
( A = k1_xboole_0
<=> ! [B] : ~ r2_hidden(B,A) ),
file('theBenchmark.p',d1_xboole_0) ).
fof(d3_xboole_0,axiom,
! [A,B,C] :
( C = k3_xboole_0(A,B)
<=> ! [D] :
( r2_hidden(D,C)
<=> ( r2_hidden(D,B)
& r2_hidden(D,A) ) ) ),
file('theBenchmark.p',d3_xboole_0) ).
fof(dt_k3_yellow_0,axiom,
! [A] :
( l1_orders_2(A)
=> m1_subset_1(k3_yellow_0(A),u1_struct_0(A)) ),
file('theBenchmark.p',dt_k3_yellow_0) ).
fof(dt_l1_orders_2,axiom,
! [A] :
( l1_orders_2(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l1_orders_2) ).
fof(existence_m1_subset_1,axiom,
! [A] :
? [B] : m1_subset_1(B,A),
file('theBenchmark.p',existence_m1_subset_1) ).
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(idempotence_k3_xboole_0,axiom,
! [A,B] : k3_xboole_0(A,A) = A,
file('theBenchmark.p',idempotence_k3_xboole_0) ).
fof(rc1_xboole_0,axiom,
? [A] : v1_xboole_0(A),
file('theBenchmark.p',rc1_xboole_0) ).
fof(reflexivity_r1_tarski,axiom,
! [A,B] : r1_tarski(A,A),
file('theBenchmark.p',reflexivity_r1_tarski) ).
fof(t2_boole,axiom,
! [A] : k3_xboole_0(A,k1_xboole_0) = k1_xboole_0,
file('theBenchmark.p',t2_boole) ).
fof(t2_subset,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( r2_hidden(A,B)
| v1_xboole_0(B) ) ),
file('theBenchmark.p',t2_subset) ).
fof(t3_subset,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('theBenchmark.p',t3_subset) ).
fof(t44_yellow_0,axiom,
! [A] :
( ( l1_orders_2(A)
& v1_yellow_0(A)
& v4_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> r1_orders_2(A,k3_yellow_0(A),B) ) ),
file('theBenchmark.p',t44_yellow_0) ).
fof(t4_subset,axiom,
! [A,B,C] :
( ( m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) )
=> m1_subset_1(A,C) ),
file('theBenchmark.p',t4_subset) ).
fof(t5_subset,axiom,
! [A,B,C] :
~ ( v1_xboole_0(C)
& m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) ),
file('theBenchmark.p',t5_subset) ).
fof(t6_boole,axiom,
! [A] :
( v1_xboole_0(A)
=> A = k1_xboole_0 ),
file('theBenchmark.p',t6_boole) ).
fof(t20_latsum_1,conjecture,
! [A] :
( ( l1_orders_2(A)
& v1_lattice3(A)
& v1_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v1_lattice3(B)
& v1_yellow_0(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& ~ v3_struct_0(B) )
=> ( ( m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B))) )
=> r2_hidden(k3_yellow_0(B),u1_struct_0(A)) ) ) ),
file('theBenchmark.p',t20_latsum_1) ).
fof(t20_latsum_1_neg,negated_conjecture,
~ ! [A] :
( ( l1_orders_2(A)
& v1_lattice3(A)
& v1_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v1_lattice3(B)
& v1_yellow_0(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& ~ v3_struct_0(B) )
=> ( ( m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B))) )
=> r2_hidden(k3_yellow_0(B),u1_struct_0(A)) ) ) ),
inference(assume_negation,[status(cth)],[t20_latsum_1]) ).
cnf(c_48,plain,
( r1_orders_2(A,k3_yellow_0(A),B)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_orders_2(A)
| ~ v1_yellow_0(A)
| ~ v4_orders_2(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t44_yellow_0]) ).
fof(nnf_38,plain,
? [A] :
( ? [B] :
( ~ r2_hidden(k3_yellow_0(B),u1_struct_0(A))
& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))
& l1_orders_2(B)
& v1_lattice3(B)
& v1_yellow_0(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& ~ v3_struct_0(B) )
& l1_orders_2(A)
& v1_lattice3(A)
& v1_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t20_latsum_1_neg]) ).
fof(sk_t20_latsum_1_neg,plain,
( ~ r2_hidden(k3_yellow_0(sK0),u1_struct_0(sK1))
& m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),k1_zfmisc_1(u1_struct_0(sK0)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),sK0)
& v1_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),sK0)
& ~ v1_xboole_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
& l1_orders_2(sK0)
& v1_lattice3(sK0)
& v1_yellow_0(sK0)
& v4_orders_2(sK0)
& v3_orders_2(sK0)
& v2_orders_2(sK0)
& ~ v3_struct_0(sK0)
& l1_orders_2(sK1)
& v1_lattice3(sK1)
& v1_yellow_0(sK1)
& v4_orders_2(sK1)
& v3_orders_2(sK1)
& v2_orders_2(sK1)
& ~ v3_struct_0(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0]),skolemize(A,sK1),skolemize(B,sK0)],[nnf_38]) ).
cnf(c_50,negated_conjecture,
v4_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t20_latsum_1_neg]) ).
cnf(c_52,plain,
( r2_hidden(D,B)
| ~ r1_orders_2(A,D,C)
| ~ r2_hidden(C,B)
| ~ m1_subset_1(D,u1_struct_0(A))
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ v12_waybel_0(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[d19_waybel_0]) ).
cnf(c_57,negated_conjecture,
v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),sK0),
inference(split_conjunct,[status(thm)],[sk_t20_latsum_1_neg]) ).
cnf(c_63,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_65,plain,
( l1_struct_0(A)
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[dt_l1_orders_2]) ).
cnf(c_66,plain,
( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[t3_subset]) ).
cnf(c_68,plain,
r1_tarski(A,A),
inference(clausify,[status(thm)],[reflexivity_r1_tarski]) ).
cnf(c_69,plain,
m1_subset_1(A,k1_zfmisc_1(A)),
inference(resolve,[status(thm)],[c_66,c_68]) ).
cnf(c_74,negated_conjecture,
( r2_hidden(B,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ r1_orders_2(sK0,B,A)
| ~ r2_hidden(A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_57,c_52]) ).
cnf(c_95,negated_conjecture,
~ r2_hidden(k3_yellow_0(sK0),u1_struct_0(sK1)),
inference(split_conjunct,[status(thm)],[sk_t20_latsum_1_neg]) ).
cnf(c_96,negated_conjecture,
m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),k1_zfmisc_1(u1_struct_0(sK0))),
inference(split_conjunct,[status(thm)],[sk_t20_latsum_1_neg]) ).
cnf(c_97,negated_conjecture,
~ v1_xboole_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),
inference(split_conjunct,[status(thm)],[sk_t20_latsum_1_neg]) ).
cnf(c_98,negated_conjecture,
l1_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t20_latsum_1_neg]) ).
cnf(c_99,negated_conjecture,
v1_yellow_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t20_latsum_1_neg]) ).
cnf(c_101,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t20_latsum_1_neg]) ).
cnf(c_108,plain,
( k1_xboole_0 = A
| ~ v1_xboole_0(A) ),
inference(clausify,[status(thm)],[t6_boole]) ).
cnf(c_109,plain,
( ~ v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(clausify,[status(thm)],[t5_subset]) ).
cnf(c_110,plain,
( m1_subset_1(A,C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(clausify,[status(thm)],[t4_subset]) ).
cnf(c_111,plain,
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(clausify,[status(thm)],[t2_subset]) ).
cnf(c_112,plain,
k3_xboole_0(A,k1_xboole_0) = k1_xboole_0,
inference(clausify,[status(thm)],[t2_boole]) ).
fof(nnf_19,plain,
? [A] : v1_xboole_0(A),
inference(fof_nnf,[status(thm)],[rc1_xboole_0]) ).
fof(sk_rc1_xboole_0,plain,
v1_xboole_0(sK2),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(A,sK2)],[nnf_19]) ).
cnf(c_117,plain,
v1_xboole_0(sK2),
inference(split_conjunct,[status(thm)],[sk_rc1_xboole_0]) ).
cnf(c_118,plain,
k3_xboole_0(A,A) = A,
inference(clausify,[status(thm)],[idempotence_k3_xboole_0]) ).
fof(nnf_16,plain,
! [A] :
? [B] : m1_subset_1(B,A),
inference(fof_nnf,[status(thm)],[existence_m1_subset_1]) ).
fof(sk_existence_m1_subset_1,plain,
! [A] : m1_subset_1(sK3(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(B,sK3(A))],[nnf_16]) ).
cnf(c_120,plain,
m1_subset_1(sK3(A),A),
inference(split_conjunct,[status(thm)],[sk_existence_m1_subset_1]) ).
cnf(c_122,plain,
( m1_subset_1(k3_yellow_0(A),u1_struct_0(A))
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[dt_k3_yellow_0]) ).
fof(nnf_5,plain,
! [A,B,C] :
( ( ? [D] :
( ( ~ r2_hidden(D,B)
| ~ r2_hidden(D,A)
| ~ r2_hidden(D,C) )
& ( ( r2_hidden(D,B)
& r2_hidden(D,A) )
| r2_hidden(D,C) ) )
| k3_xboole_0(A,B) = C )
& ( ! [X0] :
( ( ~ r2_hidden(X0,B)
| ~ r2_hidden(X0,A)
| r2_hidden(X0,C) )
& ( ( r2_hidden(X0,B)
& r2_hidden(X0,A) )
| ~ r2_hidden(X0,C) ) )
| k3_xboole_0(A,B) != C ) ),
inference(fof_nnf,[status(thm)],[d3_xboole_0]) ).
fof(sk_d3_xboole_0_sk,plain,
! [A,B,C] :
( ( ( ( ~ r2_hidden(sK4(A,B,C),B)
| ~ r2_hidden(sK4(A,B,C),A)
| ~ r2_hidden(sK4(A,B,C),C) )
& ( ( r2_hidden(sK4(A,B,C),B)
& r2_hidden(sK4(A,B,C),A) )
| r2_hidden(sK4(A,B,C),C) ) )
| k3_xboole_0(A,B) = C )
& ( ! [X0] :
( ( ~ r2_hidden(X0,B)
| ~ r2_hidden(X0,A)
| r2_hidden(X0,C) )
& ( ( r2_hidden(X0,B)
& r2_hidden(X0,A) )
| ~ r2_hidden(X0,C) ) )
| k3_xboole_0(A,B) != C ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(D,sK4(A,B,C))],[nnf_5]) ).
fof(sk_d3_xboole_0,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ r2_hidden(sK4(VAR_0,VAR_1,VAR_2),VAR_1)
| ~ r2_hidden(sK4(VAR_0,VAR_1,VAR_2),VAR_0)
| ~ r2_hidden(sK4(VAR_0,VAR_1,VAR_2),VAR_2)
| k3_xboole_0(VAR_0,VAR_1) = VAR_2 )
& ! [VAR_0,VAR_1,VAR_2] :
( r2_hidden(sK4(VAR_0,VAR_1,VAR_2),VAR_1)
| r2_hidden(sK4(VAR_0,VAR_1,VAR_2),VAR_2)
| k3_xboole_0(VAR_0,VAR_1) = VAR_2 )
& ! [VAR_0,VAR_1,VAR_2] :
( r2_hidden(sK4(VAR_0,VAR_1,VAR_2),VAR_0)
| r2_hidden(sK4(VAR_0,VAR_1,VAR_2),VAR_2)
| k3_xboole_0(VAR_0,VAR_1) = VAR_2 )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ r2_hidden(VAR_3,VAR_1)
| ~ r2_hidden(VAR_3,VAR_0)
| r2_hidden(VAR_3,VAR_2)
| k3_xboole_0(VAR_0,VAR_1) != VAR_2 )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( r2_hidden(VAR_3,VAR_1)
| ~ r2_hidden(VAR_3,VAR_2)
| k3_xboole_0(VAR_0,VAR_1) != VAR_2 )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( r2_hidden(VAR_3,VAR_0)
| ~ r2_hidden(VAR_3,VAR_2)
| k3_xboole_0(VAR_0,VAR_1) != VAR_2 ) ),
inference(cnf_transformation,[status(thm)],[sk_d3_xboole_0_sk]) ).
cnf(c_124,plain,
( r2_hidden(sK4(A,B,C),B)
| r2_hidden(sK4(A,B,C),C)
| k3_xboole_0(A,B) = C ),
inference(split_conjunct,[status(thm)],[sk_d3_xboole_0]) ).
cnf(c_125,plain,
( r2_hidden(sK4(A,B,C),A)
| r2_hidden(sK4(A,B,C),C)
| k3_xboole_0(A,B) = C ),
inference(split_conjunct,[status(thm)],[sk_d3_xboole_0]) ).
cnf(c_126,plain,
( ~ r2_hidden(D,B)
| ~ r2_hidden(D,A)
| r2_hidden(D,C)
| k3_xboole_0(A,B) != C ),
inference(split_conjunct,[status(thm)],[sk_d3_xboole_0]) ).
cnf(c_128,plain,
( r2_hidden(D,A)
| ~ r2_hidden(D,C)
| k3_xboole_0(A,B) != C ),
inference(split_conjunct,[status(thm)],[sk_d3_xboole_0]) ).
cnf(c_130,plain,
( ~ r2_hidden(B,A)
| k1_xboole_0 != A ),
inference(clausify,[status(thm)],[d1_xboole_0]) ).
cnf(c_131,plain,
k3_xboole_0(A,B) = k3_xboole_0(B,A),
inference(clausify,[status(thm)],[commutativity_k3_xboole_0]) ).
cnf(c_135,negated_conjecture,
( r1_orders_2(sK0,k3_yellow_0(sK0),A)
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l1_orders_2(sK0)
| ~ v1_yellow_0(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_48,c_50]) ).
cnf(c_7024,negated_conjecture,
( r1_orders_2(sK0,k3_yellow_0(sK0),A)
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l1_orders_2(sK0)
| ~ v1_yellow_0(sK0) ),
inference(resolve,[status(thm)],[c_101,c_135]) ).
cnf(c_7025,negated_conjecture,
( r1_orders_2(sK0,k3_yellow_0(sK0),A)
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_99,c_7024]) ).
cnf(c_136,negated_conjecture,
( r1_orders_2(sK0,k3_yellow_0(sK0),A)
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_98,c_7025]) ).
cnf(c_146,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| v3_struct_0(A)
| ~ l1_orders_2(A) ),
inference(resolve,[status(thm)],[c_65,c_63]) ).
cnf(c_7026,negated_conjecture,
( r2_hidden(B,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ r1_orders_2(sK0,B,A)
| ~ r2_hidden(A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_98,c_74]) ).
cnf(c_157,negated_conjecture,
( r2_hidden(B,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ r1_orders_2(sK0,B,A)
| ~ r2_hidden(A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_96,c_7026]) ).
cnf(c_7027,plain,
k1_xboole_0 = sK2,
inference(resolve,[status(thm)],[c_117,c_108]) ).
cnf(c_177,plain,
sK2 = k1_xboole_0,
inference(copy,[status(thm)],[c_7027]) ).
cnf(c_7028,plain,
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(resolve,[status(thm)],[c_109,c_69]) ).
cnf(c_7029,plain,
~ r2_hidden(A,sK2),
inference(resolve,[status(thm)],[c_7028,c_117]) ).
cnf(c_178,plain,
~ r2_hidden(A,k1_xboole_0),
inference(paramod,[status(thm)],[c_177,c_7029]) ).
cnf(c_179,plain,
( r2_hidden(sK3(A),A)
| v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_120,c_111]) ).
cnf(c_183,plain,
m1_subset_1(k3_yellow_0(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_122,c_98]) ).
cnf(c_210,plain,
( r2_hidden(sK4(D,B,E),E)
| k3_xboole_0(D,B) = E
| ~ r2_hidden(sK4(D,B,E),A)
| r2_hidden(sK4(D,B,E),C)
| k3_xboole_0(A,B) != C ),
inference(resolve,[status(thm)],[c_126,c_124]) ).
cnf(c_218,plain,
( k3_xboole_0(D,B) = C
| ~ r2_hidden(sK4(D,B,C),A)
| r2_hidden(sK4(D,B,C),C)
| k3_xboole_0(A,B) != C ),
inference(factor,[status(thm)],[c_210]) ).
cnf(c_7030,plain,
A = k3_xboole_0(A,A),
inference(copy,[status(thm)],[c_118]) ).
cnf(c_7031,plain,
( r2_hidden(A,B)
| ~ r2_hidden(A,k3_xboole_0(k3_xboole_0(B,C),k3_xboole_0(B,C))) ),
inference(resolve,[status(thm)],[c_128,c_7030]) ).
cnf(c_7032,negated_conjecture,
~ r2_hidden(k3_yellow_0(sK0),k3_xboole_0(k3_xboole_0(u1_struct_0(sK1),A),k3_xboole_0(u1_struct_0(sK1),A))),
inference(resolve,[status(thm)],[c_7031,c_95]) ).
cnf(c_233,negated_conjecture,
~ r2_hidden(k3_yellow_0(sK0),k3_xboole_0(u1_struct_0(sK1),A)),
inference(paramod,[status(thm)],[c_118,c_7032]) ).
cnf(c_251,plain,
k3_xboole_0(k1_xboole_0,A) = k1_xboole_0,
inference(paramod,[status(thm)],[c_131,c_112]) ).
cnf(c_7033,negated_conjecture,
( ~ v1_xboole_0(u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_146,c_98]) ).
cnf(c_263,negated_conjecture,
~ v1_xboole_0(u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_7033,c_101]) ).
cnf(c_7034,plain,
( r2_hidden(sK4(k1_xboole_0,A,B),B)
| k3_xboole_0(k1_xboole_0,A) = B ),
inference(resolve,[status(thm)],[c_178,c_125]) ).
cnf(c_326,plain,
( r2_hidden(sK4(k1_xboole_0,B,A),A)
| k1_xboole_0 = A ),
inference(paramod,[status(thm)],[c_251,c_7034]) ).
cnf(c_393,plain,
( k1_xboole_0 != A
| v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_179,c_130]) ).
cnf(c_7035,negated_conjecture,
k1_xboole_0 != k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_393,c_97]) ).
cnf(c_416,negated_conjecture,
k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)) != k1_xboole_0,
inference(copy,[status(thm)],[c_7035]) ).
cnf(c_639,plain,
( m1_subset_1(sK4(k1_xboole_0,C,A),B)
| ~ m1_subset_1(A,k1_zfmisc_1(B))
| k1_xboole_0 = A ),
inference(resolve,[status(thm)],[c_326,c_110]) ).
cnf(c_7036,negated_conjecture,
( m1_subset_1(sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),u1_struct_0(sK0))
| k1_xboole_0 = k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_639,c_96]) ).
cnf(c_7037,negated_conjecture,
( m1_subset_1(sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),u1_struct_0(sK0))
| k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)) = k1_xboole_0 ),
inference(copy,[status(thm)],[c_7036]) ).
cnf(c_6226,negated_conjecture,
m1_subset_1(sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_416,c_7037]) ).
cnf(c_6673,plain,
r1_orders_2(sK0,k3_yellow_0(sK0),sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))),
inference(resolve,[status(thm)],[c_6226,c_136]) ).
cnf(c_7038,plain,
( r2_hidden(sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_6226,c_111]) ).
cnf(c_6674,plain,
r2_hidden(sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_263,c_7038]) ).
cnf(c_7039,plain,
( k3_xboole_0(k1_xboole_0,A) = k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))
| r2_hidden(sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| k3_xboole_0(u1_struct_0(sK0),A) != k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_6674,c_218]) ).
cnf(c_7040,plain,
( k1_xboole_0 = k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))
| r2_hidden(sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| k3_xboole_0(u1_struct_0(sK0),A) != k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(paramod,[status(thm)],[c_251,c_7039]) ).
cnf(c_7041,plain,
( k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)) = k1_xboole_0
| r2_hidden(sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| k3_xboole_0(u1_struct_0(sK0),A) != k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_7040]) ).
cnf(c_6757,plain,
( r2_hidden(sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| k3_xboole_0(u1_struct_0(sK0),A) != k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_416,c_7041]) ).
cnf(c_7042,negated_conjecture,
( r2_hidden(k3_yellow_0(sK0),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ r2_hidden(sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ m1_subset_1(k3_yellow_0(sK0),u1_struct_0(sK0))
| ~ m1_subset_1(sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_6673,c_157]) ).
cnf(c_7043,negated_conjecture,
( r2_hidden(k3_yellow_0(sK0),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ r2_hidden(sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ m1_subset_1(k3_yellow_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_6226,c_7042]) ).
cnf(c_7044,negated_conjecture,
( r2_hidden(k3_yellow_0(sK0),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ r2_hidden(sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_183,c_7043]) ).
cnf(c_7012,negated_conjecture,
~ r2_hidden(sK4(k1_xboole_0,A,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_233,c_7044]) ).
cnf(c_7022,plain,
k3_xboole_0(u1_struct_0(sK0),A) != k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_7012,c_6757]) ).
cnf(c_7023,plain,
$false,
inference(resolve,[status(thm)],[c_7022,c_131]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU411+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.12/0.36 % Computer : n008.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.04/0.36 % WCLimit : 300
% 0.04/0.36 % DateTime : Sat Sep 26 09:30:27 UTC 2026
% 0.04/0.36 % CPUTime :
% 0.04/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.04/0.37 % Process 3334066 was started by sandbox on n008,
% 0.04/0.37 % Sat Sep 26 09:30:27 2026
% 0.04/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.04/0.38
% 0.04/0.38 % From the command line: assign(max_seconds, 300).
% 22.09/3.60
% 22.09/3.60 % given #500 (T,wt=6): 1940 v1_xboole_0(k3_xboole_0(A,B)) | -v1_xboole_0(B). [resolve(1860,b,107,a)].
% 22.09/3.60
% 22.09/3.60 % given #1000 (F,wt=8): 1241 k3_xboole_0(A,f3(f6(c7))) != u1_struct_0(c7). [ur(173,b,309,a,c,1216,a),flip(a)].
% 22.09/3.60
% 22.09/3.60 % SZS status Theorem for theBenchmark
% 22.09/3.60
% 22.09/3.60 % Proof 1 at 2.76 (+ 0.44) seconds.
% 22.09/3.60 % Length of proof is 74.
% 22.09/3.60 % Level of proof is 10.
% 22.09/3.60 % Maximum clause weight is 37.000.
% 22.09/3.60 % Given clauses 1042.
% 22.09/3.60
% 22.09/3.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------