%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU101+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/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 08:45:01 AM UTC 2026
% Result : Theorem 14.85s 4.44s
% Output : CNFRefutation 14.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 7
% Syntax : Number of formulae : 92 ( 10 unt; 0 def)
% Number of atoms : 323 ( 2 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 331 ( 100 ~; 181 |; 39 &)
% ( 5 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% Number of variables : 107 ( 0 sgn 49 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_finsub_1,axiom,
! [A] :
( preboolean(A)
=> ( diff_closed(A)
& cup_closed(A) ) ),
file('theBenchmark.p',cc1_finsub_1) ).
fof(cc2_finsub_1,axiom,
! [A] :
( ( diff_closed(A)
& cup_closed(A) )
=> preboolean(A) ),
file('theBenchmark.p',cc2_finsub_1) ).
fof(commutativity_k2_xboole_0,axiom,
! [A,B] : set_union2(A,B) = set_union2(B,A),
file('theBenchmark.p',commutativity_k2_xboole_0) ).
fof(d1_finsub_1,axiom,
! [A] :
( cup_closed(A)
<=> ! [B,C] :
( ( in(C,A)
& in(B,A) )
=> in(set_union2(B,C),A) ) ),
file('theBenchmark.p',d1_finsub_1) ).
fof(d3_finsub_1,axiom,
! [A] :
( diff_closed(A)
<=> ! [B,C] :
( ( in(C,A)
& in(B,A) )
=> in(set_difference(B,C),A) ) ),
file('theBenchmark.p',d3_finsub_1) ).
fof(d4_finsub_1,axiom,
! [A] :
( preboolean(A)
<=> ( diff_closed(A)
& cup_closed(A) ) ),
file('theBenchmark.p',d4_finsub_1) ).
fof(t10_finsub_1,conjecture,
! [A] :
( preboolean(A)
<=> ! [B,C] :
( ( in(C,A)
& in(B,A) )
=> ( in(set_difference(B,C),A)
& in(set_union2(B,C),A) ) ) ),
file('theBenchmark.p',t10_finsub_1) ).
fof(t10_finsub_1_neg,negated_conjecture,
~ ! [A] :
( preboolean(A)
<=> ! [B,C] :
( ( in(C,A)
& in(B,A) )
=> ( in(set_difference(B,C),A)
& in(set_union2(B,C),A) ) ) ),
inference(assume_negation,[status(cth)],[t10_finsub_1]) ).
cnf(c_39,plain,
( preboolean(A)
| ~ diff_closed(A)
| ~ cup_closed(A) ),
inference(clausify,[status(thm)],[cc2_finsub_1]) ).
cnf(c_40,plain,
( cup_closed(A)
| ~ preboolean(A) ),
inference(clausify,[status(thm)],[cc1_finsub_1]) ).
fof(nnf_7,plain,
! [A] :
( ( ? [B,C] :
( ~ in(set_union2(B,C),A)
& in(C,A)
& in(B,A) )
| cup_closed(A) )
& ( ! [X0,X1] :
( in(set_union2(X0,X1),A)
| ~ in(X1,A)
| ~ in(X0,A) )
| ~ cup_closed(A) ) ),
inference(fof_nnf,[status(thm)],[d1_finsub_1]) ).
fof(sk_d1_finsub_1_sk,plain,
! [A] :
( ( ( ~ in(set_union2(sK0(A),sK1(A)),A)
& in(sK1(A),A)
& in(sK0(A),A) )
| cup_closed(A) )
& ( ! [X0,X1] :
( in(set_union2(X0,X1),A)
| ~ in(X1,A)
| ~ in(X0,A) )
| ~ cup_closed(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(B,sK0(A)),skolemize(C,sK1(A))],[nnf_7]) ).
fof(sk_d1_finsub_1,plain,
( ! [VAR_0] :
( ~ in(set_union2(sK0(VAR_0),sK1(VAR_0)),VAR_0)
| cup_closed(VAR_0) )
& ! [VAR_0] :
( in(sK1(VAR_0),VAR_0)
| cup_closed(VAR_0) )
& ! [VAR_0] :
( in(sK0(VAR_0),VAR_0)
| cup_closed(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(set_union2(VAR_1,VAR_2),VAR_0)
| ~ in(VAR_2,VAR_0)
| ~ in(VAR_1,VAR_0)
| ~ cup_closed(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d1_finsub_1_sk]) ).
cnf(c_41,plain,
( in(set_union2(B,C),A)
| ~ in(C,A)
| ~ in(B,A)
| ~ cup_closed(A) ),
inference(split_conjunct,[status(thm)],[sk_d1_finsub_1]) ).
cnf(c_42,plain,
( in(sK0(A),A)
| cup_closed(A) ),
inference(split_conjunct,[status(thm)],[sk_d1_finsub_1]) ).
cnf(c_43,plain,
( in(sK1(A),A)
| cup_closed(A) ),
inference(split_conjunct,[status(thm)],[sk_d1_finsub_1]) ).
cnf(c_44,plain,
( ~ in(set_union2(sK0(A),sK1(A)),A)
| cup_closed(A) ),
inference(split_conjunct,[status(thm)],[sk_d1_finsub_1]) ).
cnf(c_49,plain,
( preboolean(A)
| ~ diff_closed(A)
| in(sK0(A),A) ),
inference(resolve,[status(thm)],[c_42,c_39]) ).
cnf(c_50,plain,
( preboolean(A)
| ~ diff_closed(A)
| in(sK1(A),A) ),
inference(resolve,[status(thm)],[c_43,c_39]) ).
cnf(c_51,plain,
( preboolean(A)
| ~ diff_closed(A)
| ~ in(set_union2(sK0(A),sK1(A)),A) ),
inference(resolve,[status(thm)],[c_44,c_39]) ).
cnf(c_52,plain,
( diff_closed(A)
| ~ preboolean(A) ),
inference(clausify,[status(thm)],[d4_finsub_1]) ).
fof(nnf_8,plain,
! [A] :
( ( ? [B,C] :
( ~ in(set_difference(B,C),A)
& in(C,A)
& in(B,A) )
| diff_closed(A) )
& ( ! [X0,X1] :
( in(set_difference(X0,X1),A)
| ~ in(X1,A)
| ~ in(X0,A) )
| ~ diff_closed(A) ) ),
inference(fof_nnf,[status(thm)],[d3_finsub_1]) ).
fof(sk_d3_finsub_1_sk,plain,
! [A] :
( ( ( ~ in(set_difference(sK2(A),sK3(A)),A)
& in(sK3(A),A)
& in(sK2(A),A) )
| diff_closed(A) )
& ( ! [X0,X1] :
( in(set_difference(X0,X1),A)
| ~ in(X1,A)
| ~ in(X0,A) )
| ~ diff_closed(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(B,sK2(A)),skolemize(C,sK3(A))],[nnf_8]) ).
fof(sk_d3_finsub_1,plain,
( ! [VAR_0] :
( ~ in(set_difference(sK2(VAR_0),sK3(VAR_0)),VAR_0)
| diff_closed(VAR_0) )
& ! [VAR_0] :
( in(sK3(VAR_0),VAR_0)
| diff_closed(VAR_0) )
& ! [VAR_0] :
( in(sK2(VAR_0),VAR_0)
| diff_closed(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(set_difference(VAR_1,VAR_2),VAR_0)
| ~ in(VAR_2,VAR_0)
| ~ in(VAR_1,VAR_0)
| ~ diff_closed(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d3_finsub_1_sk]) ).
cnf(c_53,plain,
( ~ in(set_difference(sK2(A),sK3(A)),A)
| diff_closed(A) ),
inference(split_conjunct,[status(thm)],[sk_d3_finsub_1]) ).
cnf(c_54,plain,
( in(sK3(A),A)
| diff_closed(A) ),
inference(split_conjunct,[status(thm)],[sk_d3_finsub_1]) ).
cnf(c_55,plain,
( in(sK2(A),A)
| diff_closed(A) ),
inference(split_conjunct,[status(thm)],[sk_d3_finsub_1]) ).
cnf(c_56,plain,
( in(set_difference(B,C),A)
| ~ in(C,A)
| ~ in(B,A)
| ~ diff_closed(A) ),
inference(split_conjunct,[status(thm)],[sk_d3_finsub_1]) ).
cnf(c_66,plain,
( ~ preboolean(B)
| in(set_union2(A,C),B)
| ~ in(C,B)
| ~ in(A,B) ),
inference(resolve,[status(thm)],[c_41,c_40]) ).
fof(nnf_38,plain,
? [A] :
( ( ? [B,C] :
( ( ~ in(set_difference(B,C),A)
| ~ in(set_union2(B,C),A) )
& in(C,A)
& in(B,A) )
| ~ preboolean(A) )
& ( ! [X0,X1] :
( ( in(set_difference(X0,X1),A)
& in(set_union2(X0,X1),A) )
| ~ in(X1,A)
| ~ in(X0,A) )
| preboolean(A) ) ),
inference(fof_nnf,[status(thm)],[t10_finsub_1_neg]) ).
fof(sk_t10_finsub_1_neg_sk,plain,
( ( ( ( ~ in(set_difference(sK5,sK6),sK4)
| ~ in(set_union2(sK5,sK6),sK4) )
& in(sK6,sK4)
& in(sK5,sK4) )
| ~ preboolean(sK4) )
& ( ! [X0,X1] :
( ( in(set_difference(X0,X1),sK4)
& in(set_union2(X0,X1),sK4) )
| ~ in(X1,sK4)
| ~ in(X0,sK4) )
| preboolean(sK4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(A,sK4),skolemize(B,sK5),skolemize(C,sK6)],[nnf_38]) ).
fof(sk_t10_finsub_1_neg,plain,
( ( ~ in(set_difference(sK5,sK6),sK4)
| ~ in(set_union2(sK5,sK6),sK4)
| ~ preboolean(sK4) )
& ( in(sK6,sK4)
| ~ preboolean(sK4) )
& ( in(sK5,sK4)
| ~ preboolean(sK4) )
& ! [VAR_0,VAR_1] :
( in(set_difference(VAR_0,VAR_1),sK4)
| ~ in(VAR_1,sK4)
| ~ in(VAR_0,sK4)
| preboolean(sK4) )
& ! [VAR_0,VAR_1] :
( in(set_union2(VAR_0,VAR_1),sK4)
| ~ in(VAR_1,sK4)
| ~ in(VAR_0,sK4)
| preboolean(sK4) ) ),
inference(cnf_transformation,[status(thm)],[sk_t10_finsub_1_neg_sk]) ).
cnf(c_67,negated_conjecture,
( ~ in(set_difference(sK5,sK6),sK4)
| ~ in(set_union2(sK5,sK6),sK4)
| ~ preboolean(sK4) ),
inference(split_conjunct,[status(thm)],[sk_t10_finsub_1_neg]) ).
cnf(c_68,negated_conjecture,
( in(sK6,sK4)
| ~ preboolean(sK4) ),
inference(split_conjunct,[status(thm)],[sk_t10_finsub_1_neg]) ).
cnf(c_69,negated_conjecture,
( in(sK5,sK4)
| ~ preboolean(sK4) ),
inference(split_conjunct,[status(thm)],[sk_t10_finsub_1_neg]) ).
cnf(c_70,negated_conjecture,
( in(set_difference(A,B),sK4)
| ~ in(B,sK4)
| ~ in(A,sK4)
| preboolean(sK4) ),
inference(split_conjunct,[status(thm)],[sk_t10_finsub_1_neg]) ).
cnf(c_71,negated_conjecture,
( in(set_union2(A,B),sK4)
| ~ in(B,sK4)
| ~ in(A,sK4)
| preboolean(sK4) ),
inference(split_conjunct,[status(thm)],[sk_t10_finsub_1_neg]) ).
cnf(c_109,plain,
set_union2(A,B) = set_union2(B,A),
inference(clausify,[status(thm)],[commutativity_k2_xboole_0]) ).
cnf(c_113,plain,
( preboolean(A)
| in(sK0(A),A)
| ~ in(set_difference(sK2(A),sK3(A)),A) ),
inference(resolve,[status(thm)],[c_53,c_49]) ).
cnf(c_114,plain,
( preboolean(A)
| in(sK1(A),A)
| ~ in(set_difference(sK2(A),sK3(A)),A) ),
inference(resolve,[status(thm)],[c_53,c_50]) ).
cnf(c_115,plain,
( preboolean(A)
| ~ in(set_union2(sK0(A),sK1(A)),A)
| ~ in(set_difference(sK2(A),sK3(A)),A) ),
inference(resolve,[status(thm)],[c_53,c_51]) ).
cnf(c_116,plain,
( preboolean(A)
| in(sK0(A),A)
| in(sK3(A),A) ),
inference(resolve,[status(thm)],[c_54,c_49]) ).
cnf(c_117,plain,
( preboolean(A)
| in(sK1(A),A)
| in(sK3(A),A) ),
inference(resolve,[status(thm)],[c_54,c_50]) ).
cnf(c_118,plain,
( preboolean(A)
| ~ in(set_union2(sK0(A),sK1(A)),A)
| in(sK3(A),A) ),
inference(resolve,[status(thm)],[c_54,c_51]) ).
cnf(c_119,plain,
( preboolean(A)
| in(sK0(A),A)
| in(sK2(A),A) ),
inference(resolve,[status(thm)],[c_55,c_49]) ).
cnf(c_120,plain,
( preboolean(A)
| in(sK1(A),A)
| in(sK2(A),A) ),
inference(resolve,[status(thm)],[c_55,c_50]) ).
cnf(c_121,plain,
( preboolean(A)
| ~ in(set_union2(sK0(A),sK1(A)),A)
| in(sK2(A),A) ),
inference(resolve,[status(thm)],[c_55,c_51]) ).
cnf(c_125,plain,
( ~ preboolean(B)
| in(set_difference(A,C),B)
| ~ in(C,B)
| ~ in(A,B) ),
inference(resolve,[status(thm)],[c_56,c_52]) ).
cnf(c_11462,negated_conjecture,
( in(set_difference(A,sK3(sK4)),sK4)
| ~ in(A,sK4)
| preboolean(sK4)
| preboolean(sK4)
| in(sK0(sK4),sK4) ),
inference(resolve,[status(thm)],[c_116,c_70]) ).
cnf(c_202,negated_conjecture,
( in(set_difference(A,sK3(sK4)),sK4)
| ~ in(A,sK4)
| preboolean(sK4)
| in(sK0(sK4),sK4) ),
inference(copy,[status(thm)],[c_11462]) ).
cnf(c_11463,negated_conjecture,
( in(set_difference(A,sK3(sK4)),sK4)
| ~ in(A,sK4)
| preboolean(sK4)
| preboolean(sK4)
| in(sK1(sK4),sK4) ),
inference(resolve,[status(thm)],[c_117,c_70]) ).
cnf(c_213,negated_conjecture,
( in(set_difference(A,sK3(sK4)),sK4)
| ~ in(A,sK4)
| preboolean(sK4)
| in(sK1(sK4),sK4) ),
inference(copy,[status(thm)],[c_11463]) ).
cnf(c_11464,plain,
( preboolean(sK4)
| in(sK0(sK4),sK4)
| in(set_difference(sK2(sK4),sK3(sK4)),sK4)
| preboolean(sK4)
| in(sK0(sK4),sK4) ),
inference(resolve,[status(thm)],[c_202,c_119]) ).
cnf(c_11465,plain,
( preboolean(sK4)
| in(set_difference(sK2(sK4),sK3(sK4)),sK4)
| preboolean(sK4)
| in(sK0(sK4),sK4) ),
inference(copy,[status(thm)],[c_11464]) ).
cnf(c_1553,plain,
( in(set_difference(sK2(sK4),sK3(sK4)),sK4)
| preboolean(sK4)
| in(sK0(sK4),sK4) ),
inference(copy,[status(thm)],[c_11465]) ).
cnf(c_11466,plain,
( preboolean(sK4)
| in(sK1(sK4),sK4)
| in(set_difference(sK2(sK4),sK3(sK4)),sK4)
| preboolean(sK4)
| in(sK1(sK4),sK4) ),
inference(resolve,[status(thm)],[c_213,c_120]) ).
cnf(c_11467,plain,
( preboolean(sK4)
| in(set_difference(sK2(sK4),sK3(sK4)),sK4)
| preboolean(sK4)
| in(sK1(sK4),sK4) ),
inference(copy,[status(thm)],[c_11466]) ).
cnf(c_2100,plain,
( in(set_difference(sK2(sK4),sK3(sK4)),sK4)
| preboolean(sK4)
| in(sK1(sK4),sK4) ),
inference(copy,[status(thm)],[c_11467]) ).
cnf(c_11468,plain,
( preboolean(sK4)
| in(sK0(sK4),sK4)
| preboolean(sK4)
| in(sK0(sK4),sK4) ),
inference(resolve,[status(thm)],[c_1553,c_113]) ).
cnf(c_11469,plain,
( preboolean(sK4)
| preboolean(sK4)
| in(sK0(sK4),sK4) ),
inference(copy,[status(thm)],[c_11468]) ).
cnf(c_8713,plain,
( preboolean(sK4)
| in(sK0(sK4),sK4) ),
inference(copy,[status(thm)],[c_11469]) ).
cnf(c_11470,negated_conjecture,
( in(set_union2(sK0(sK4),A),sK4)
| ~ in(A,sK4)
| preboolean(sK4)
| preboolean(sK4) ),
inference(resolve,[status(thm)],[c_8713,c_71]) ).
cnf(c_8743,negated_conjecture,
( in(set_union2(sK0(sK4),A),sK4)
| ~ in(A,sK4)
| preboolean(sK4) ),
inference(copy,[status(thm)],[c_11470]) ).
cnf(c_11471,plain,
( preboolean(sK4)
| in(sK1(sK4),sK4)
| preboolean(sK4)
| in(sK1(sK4),sK4) ),
inference(resolve,[status(thm)],[c_2100,c_114]) ).
cnf(c_11472,plain,
( preboolean(sK4)
| preboolean(sK4)
| in(sK1(sK4),sK4) ),
inference(copy,[status(thm)],[c_11471]) ).
cnf(c_9720,plain,
( preboolean(sK4)
| in(sK1(sK4),sK4) ),
inference(copy,[status(thm)],[c_11472]) ).
cnf(c_11473,plain,
( in(set_union2(sK0(sK4),sK1(sK4)),sK4)
| preboolean(sK4)
| preboolean(sK4) ),
inference(resolve,[status(thm)],[c_9720,c_8743]) ).
cnf(c_9723,plain,
( in(set_union2(sK0(sK4),sK1(sK4)),sK4)
| preboolean(sK4) ),
inference(copy,[status(thm)],[c_11473]) ).
cnf(c_11474,plain,
( preboolean(sK4)
| in(sK2(sK4),sK4)
| preboolean(sK4) ),
inference(resolve,[status(thm)],[c_9723,c_121]) ).
cnf(c_9896,plain,
( in(sK2(sK4),sK4)
| preboolean(sK4) ),
inference(copy,[status(thm)],[c_11474]) ).
cnf(c_11475,plain,
( preboolean(sK4)
| in(sK3(sK4),sK4)
| preboolean(sK4) ),
inference(resolve,[status(thm)],[c_9723,c_118]) ).
cnf(c_9897,plain,
( in(sK3(sK4),sK4)
| preboolean(sK4) ),
inference(copy,[status(thm)],[c_11475]) ).
cnf(c_11476,plain,
( preboolean(sK4)
| ~ in(set_difference(sK2(sK4),sK3(sK4)),sK4)
| preboolean(sK4) ),
inference(resolve,[status(thm)],[c_9723,c_115]) ).
cnf(c_9898,plain,
( ~ in(set_difference(sK2(sK4),sK3(sK4)),sK4)
| preboolean(sK4) ),
inference(copy,[status(thm)],[c_11476]) ).
cnf(c_11477,negated_conjecture,
( in(set_difference(sK2(sK4),A),sK4)
| ~ in(A,sK4)
| preboolean(sK4)
| preboolean(sK4) ),
inference(resolve,[status(thm)],[c_9896,c_70]) ).
cnf(c_9918,negated_conjecture,
( in(set_difference(sK2(sK4),A),sK4)
| ~ in(A,sK4)
| preboolean(sK4) ),
inference(copy,[status(thm)],[c_11477]) ).
cnf(c_11478,plain,
( preboolean(sK4)
| in(set_difference(sK2(sK4),sK3(sK4)),sK4)
| preboolean(sK4) ),
inference(resolve,[status(thm)],[c_9918,c_9897]) ).
cnf(c_11033,plain,
( in(set_difference(sK2(sK4),sK3(sK4)),sK4)
| preboolean(sK4) ),
inference(copy,[status(thm)],[c_11478]) ).
cnf(c_11479,plain,
( preboolean(sK4)
| preboolean(sK4) ),
inference(resolve,[status(thm)],[c_11033,c_9898]) ).
cnf(c_11052,plain,
preboolean(sK4),
inference(copy,[status(thm)],[c_11479]) ).
cnf(c_11053,negated_conjecture,
in(sK5,sK4),
inference(resolve,[status(thm)],[c_11052,c_69]) ).
cnf(c_11054,negated_conjecture,
in(sK6,sK4),
inference(resolve,[status(thm)],[c_11052,c_68]) ).
cnf(c_11055,negated_conjecture,
( ~ in(set_difference(sK5,sK6),sK4)
| ~ in(set_union2(sK5,sK6),sK4) ),
inference(resolve,[status(thm)],[c_11052,c_67]) ).
cnf(c_11480,negated_conjecture,
( ~ preboolean(sK4)
| in(set_difference(sK5,A),sK4)
| ~ in(A,sK4) ),
inference(resolve,[status(thm)],[c_11053,c_125]) ).
cnf(c_11082,negated_conjecture,
( in(set_difference(sK5,A),sK4)
| ~ in(A,sK4) ),
inference(resolve,[status(thm)],[c_11052,c_11480]) ).
cnf(c_11481,negated_conjecture,
( ~ preboolean(sK4)
| in(set_union2(A,sK5),sK4)
| ~ in(A,sK4) ),
inference(resolve,[status(thm)],[c_11053,c_66]) ).
cnf(c_11088,negated_conjecture,
( in(set_union2(A,sK5),sK4)
| ~ in(A,sK4) ),
inference(resolve,[status(thm)],[c_11052,c_11481]) ).
cnf(c_11381,plain,
in(set_difference(sK5,sK6),sK4),
inference(resolve,[status(thm)],[c_11082,c_11054]) ).
cnf(c_11387,negated_conjecture,
~ in(set_union2(sK5,sK6),sK4),
inference(resolve,[status(thm)],[c_11381,c_11055]) ).
cnf(c_11482,negated_conjecture,
in(set_union2(sK6,sK5),sK4),
inference(resolve,[status(thm)],[c_11088,c_11054]) ).
cnf(c_11483,negated_conjecture,
in(set_union2(sK5,sK6),sK4),
inference(paramod,[status(thm)],[c_109,c_11482]) ).
cnf(c_11461,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_11387,c_11483]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU101+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.42 % Computer : n005.cluster.edu
% 0.08/0.42 % Model : x86_64 x86_64
% 0.08/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.42 % Memory : 8046.5625MB
% 0.08/0.42 % OS : Linux 6.8.0-71-generic
% 0.08/0.42 % CPULimit : 300
% 0.08/0.42 % WCLimit : 300
% 0.08/0.42 % DateTime : Sat Sep 26 08:36:16 UTC 2026
% 0.08/0.42 % CPUTime :
% 0.08/0.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.42 % Process 1708986 was started by sandbox on n005,
% 0.08/0.42 % Sat Sep 26 08:36:16 2026
% 0.08/0.42 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.43
% 0.08/0.43 % From the command line: assign(max_seconds, 300).
% 14.85/4.44
% 14.85/4.44 % given #500 (T,wt=26): 721 finite(set_union2(c1,f5(powerset(c1)))). [resolve(489,a,168,a),rewrite([109(5)])].
% 14.85/4.44
% 14.85/4.44 % given #1000 (W,wt=22): 687 -in(c4,f9(f9(c4))). [ur(143,a,144,a,c,594,a)].
% 14.85/4.44
% 14.85/4.44 % SZS status Theorem for theBenchmark
% 14.85/4.44
% 14.85/4.44 % Proof 1 at 1.39 (+ 0.41) seconds.
% 14.85/4.44 % Length of proof is 60.
% 14.85/4.44 % Level of proof is 17.
% 14.85/4.44 % Maximum clause weight is 31.000.
% 14.85/4.44 % Given clauses 1402.
% 14.85/4.44
% 14.85/4.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------