%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU383+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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:09 AM UTC 2026
% Result : Theorem 19.40s 3.20s
% Output : CNFRefutation 19.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 13
% Syntax : Number of formulae : 83 ( 18 unt; 0 def)
% Number of atoms : 268 ( 39 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 280 ( 95 ~; 113 |; 47 &)
% ( 6 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% Number of variables : 88 ( 1 sgn 37 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d20_waybel_0,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( upper_relstr_subset(B,A)
<=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ( ( related(A,C,D)
& in(C,B) )
=> in(D,B) ) ) ) ) ) ),
file('theBenchmark.p',d20_waybel_0) ).
fof(dt_k3_yellow_0,axiom,
! [A] :
( rel_str(A)
=> element(bottom_of_relstr(A),the_carrier(A)) ),
file('theBenchmark.p',dt_k3_yellow_0) ).
fof(dt_l1_orders_2,axiom,
! [A] :
( rel_str(A)
=> one_sorted_str(A) ),
file('theBenchmark.p',dt_l1_orders_2) ).
fof(fc1_struct_0,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ~ empty(the_carrier(A)) ),
file('theBenchmark.p',fc1_struct_0) ).
fof(reflexivity_r1_tarski,axiom,
! [A,B] : subset(A,A),
file('theBenchmark.p',reflexivity_r1_tarski) ).
fof(t1_subset,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('theBenchmark.p',t1_subset) ).
fof(t2_subset,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('theBenchmark.p',t2_subset) ).
fof(t2_tarski,axiom,
! [A,B] :
( ! [C] :
( in(C,A)
<=> in(C,B) )
=> A = B ),
file('theBenchmark.p',t2_tarski) ).
fof(t3_subset,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('theBenchmark.p',t3_subset) ).
fof(t44_yellow_0,axiom,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> related(A,bottom_of_relstr(A),B) ) ),
file('theBenchmark.p',t44_yellow_0) ).
fof(t4_subset,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('theBenchmark.p',t4_subset) ).
fof(t5_tex_2,axiom,
! [A,B] :
( element(B,powerset(A))
=> ( proper_element(B,powerset(A))
<=> B != A ) ),
file('theBenchmark.p',t5_tex_2) ).
fof(t8_waybel_7,conjecture,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
=> ( proper_element(B,powerset(the_carrier(A)))
<=> ~ in(bottom_of_relstr(A),B) ) ) ),
file('theBenchmark.p',t8_waybel_7) ).
fof(t8_waybel_7_neg,negated_conjecture,
~ ! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
=> ( proper_element(B,powerset(the_carrier(A)))
<=> ~ in(bottom_of_relstr(A),B) ) ) ),
inference(assume_negation,[status(cth)],[t8_waybel_7]) ).
cnf(c_46,plain,
( one_sorted_str(A)
| ~ rel_str(A) ),
inference(clausify,[status(thm)],[dt_l1_orders_2]) ).
cnf(c_47,plain,
( element(bottom_of_relstr(A),the_carrier(A))
| ~ rel_str(A) ),
inference(clausify,[status(thm)],[dt_k3_yellow_0]) ).
cnf(c_54,plain,
( in(D,B)
| ~ related(A,C,D)
| ~ in(C,B)
| ~ element(D,the_carrier(A))
| ~ element(C,the_carrier(A))
| ~ upper_relstr_subset(B,A)
| ~ element(B,powerset(the_carrier(A)))
| ~ rel_str(A) ),
inference(clausify,[status(thm)],[d20_waybel_0]) ).
cnf(c_63,plain,
( related(A,bottom_of_relstr(A),B)
| ~ element(B,the_carrier(A))
| ~ rel_str(A)
| ~ lower_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[t44_yellow_0]) ).
fof(nnf_44,plain,
? [A] :
( ? [B] :
( ( in(bottom_of_relstr(A),B)
| ~ proper_element(B,powerset(the_carrier(A))) )
& ( ~ in(bottom_of_relstr(A),B)
| proper_element(B,powerset(the_carrier(A))) )
& element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
& rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[t8_waybel_7_neg]) ).
fof(sk_t8_waybel_7_neg,plain,
( ( in(bottom_of_relstr(sK0),sK2)
| ~ proper_element(sK2,powerset(the_carrier(sK0))) )
& ( ~ in(bottom_of_relstr(sK0),sK2)
| proper_element(sK2,powerset(the_carrier(sK0))) )
& element(sK2,powerset(the_carrier(sK0)))
& upper_relstr_subset(sK2,sK0)
& filtered_subset(sK2,sK0)
& ~ empty(sK2)
& rel_str(sK0)
& lower_bounded_relstr(sK0)
& antisymmetric_relstr(sK0)
& transitive_relstr(sK0)
& reflexive_relstr(sK0)
& ~ empty_carrier(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK2]),skolemize(A,sK0),skolemize(B,sK2)],[nnf_44]) ).
cnf(c_64,negated_conjecture,
rel_str(sK0),
inference(split_conjunct,[status(thm)],[sk_t8_waybel_7_neg]) ).
cnf(c_67,negated_conjecture,
one_sorted_str(sK0),
inference(resolve,[status(thm)],[c_64,c_46]) ).
cnf(c_70,plain,
( ~ empty(the_carrier(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[fc1_struct_0]) ).
cnf(c_73,plain,
( ~ subset(A,B)
| element(A,powerset(B)) ),
inference(clausify,[status(thm)],[t3_subset]) ).
cnf(c_74,plain,
subset(A,A),
inference(clausify,[status(thm)],[reflexivity_r1_tarski]) ).
cnf(c_75,plain,
element(A,powerset(A)),
inference(resolve,[status(thm)],[c_74,c_73]) ).
cnf(c_79,negated_conjecture,
( ~ empty(the_carrier(sK0))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_70,c_67]) ).
cnf(c_109,plain,
( element(A,B)
| ~ in(A,B) ),
inference(clausify,[status(thm)],[t1_subset]) ).
cnf(c_110,plain,
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(clausify,[status(thm)],[t2_subset]) ).
fof(nnf_35,plain,
! [A,B] :
( B = A
| ? [C] :
( ( ~ in(C,B)
| ~ in(C,A) )
& ( in(C,B)
| in(C,A) ) ) ),
inference(fof_nnf,[status(thm)],[t2_tarski]) ).
fof(sk_t2_tarski_sk,plain,
! [A,B] :
( B = A
| ( ( ~ in(sK1(A,B),B)
| ~ in(sK1(A,B),A) )
& ( in(sK1(A,B),B)
| in(sK1(A,B),A) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(C,sK1(A,B))],[nnf_35]) ).
fof(sk_t2_tarski,plain,
( ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| ~ in(sK1(VAR_0,VAR_1),VAR_1)
| ~ in(sK1(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| in(sK1(VAR_0,VAR_1),VAR_1)
| in(sK1(VAR_0,VAR_1),VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_t2_tarski_sk]) ).
cnf(c_111,plain,
( B = A
| in(sK1(A,B),B)
| in(sK1(A,B),A) ),
inference(split_conjunct,[status(thm)],[sk_t2_tarski]) ).
cnf(c_112,plain,
( B = A
| ~ in(sK1(A,B),B)
| ~ in(sK1(A,B),A) ),
inference(split_conjunct,[status(thm)],[sk_t2_tarski]) ).
cnf(c_113,plain,
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(clausify,[status(thm)],[t4_subset]) ).
cnf(c_115,plain,
( A != B
| ~ proper_element(A,powerset(B))
| ~ element(A,powerset(B)) ),
inference(clausify,[status(thm)],[t5_tex_2]) ).
cnf(c_116,plain,
( A = B
| proper_element(A,powerset(B))
| ~ element(A,powerset(B)) ),
inference(clausify,[status(thm)],[t5_tex_2]) ).
cnf(c_120,negated_conjecture,
~ empty_carrier(sK0),
inference(split_conjunct,[status(thm)],[sk_t8_waybel_7_neg]) ).
cnf(c_123,negated_conjecture,
antisymmetric_relstr(sK0),
inference(split_conjunct,[status(thm)],[sk_t8_waybel_7_neg]) ).
cnf(c_124,negated_conjecture,
lower_bounded_relstr(sK0),
inference(split_conjunct,[status(thm)],[sk_t8_waybel_7_neg]) ).
cnf(c_126,negated_conjecture,
upper_relstr_subset(sK2,sK0),
inference(split_conjunct,[status(thm)],[sk_t8_waybel_7_neg]) ).
cnf(c_127,negated_conjecture,
element(sK2,powerset(the_carrier(sK0))),
inference(split_conjunct,[status(thm)],[sk_t8_waybel_7_neg]) ).
cnf(c_128,negated_conjecture,
( ~ in(bottom_of_relstr(sK0),sK2)
| proper_element(sK2,powerset(the_carrier(sK0))) ),
inference(split_conjunct,[status(thm)],[sk_t8_waybel_7_neg]) ).
cnf(c_129,negated_conjecture,
( in(bottom_of_relstr(sK0),sK2)
| ~ proper_element(sK2,powerset(the_carrier(sK0))) ),
inference(split_conjunct,[status(thm)],[sk_t8_waybel_7_neg]) ).
cnf(c_145,negated_conjecture,
( related(sK0,bottom_of_relstr(sK0),A)
| ~ element(A,the_carrier(sK0))
| ~ lower_bounded_relstr(sK0)
| ~ antisymmetric_relstr(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_64,c_63]) ).
cnf(c_7926,negated_conjecture,
( related(sK0,bottom_of_relstr(sK0),A)
| ~ element(A,the_carrier(sK0))
| ~ lower_bounded_relstr(sK0)
| ~ antisymmetric_relstr(sK0) ),
inference(resolve,[status(thm)],[c_120,c_145]) ).
cnf(c_7927,negated_conjecture,
( related(sK0,bottom_of_relstr(sK0),A)
| ~ element(A,the_carrier(sK0))
| ~ lower_bounded_relstr(sK0) ),
inference(resolve,[status(thm)],[c_123,c_7926]) ).
cnf(c_146,negated_conjecture,
( related(sK0,bottom_of_relstr(sK0),A)
| ~ element(A,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_124,c_7927]) ).
cnf(c_153,negated_conjecture,
element(bottom_of_relstr(sK0),the_carrier(sK0)),
inference(resolve,[status(thm)],[c_64,c_47]) ).
cnf(c_160,negated_conjecture,
( in(C,A)
| ~ related(sK0,B,C)
| ~ in(B,A)
| ~ element(C,the_carrier(sK0))
| ~ element(B,the_carrier(sK0))
| ~ upper_relstr_subset(A,sK0)
| ~ element(A,powerset(the_carrier(sK0))) ),
inference(resolve,[status(thm)],[c_64,c_54]) ).
cnf(c_171,negated_conjecture,
~ empty(the_carrier(sK0)),
inference(resolve,[status(thm)],[c_120,c_79]) ).
cnf(c_206,plain,
( element(sK1(A,B),A)
| B = A
| in(sK1(A,B),B) ),
inference(resolve,[status(thm)],[c_111,c_109]) ).
cnf(c_7928,plain,
( A != A
| ~ proper_element(A,powerset(A)) ),
inference(resolve,[status(thm)],[c_115,c_75]) ).
cnf(c_255,plain,
~ proper_element(A,powerset(A)),
inference(xxres,[status(thm)],[c_7928]) ).
cnf(c_7929,negated_conjecture,
( sK2 = the_carrier(sK0)
| proper_element(sK2,powerset(the_carrier(sK0))) ),
inference(resolve,[status(thm)],[c_127,c_116]) ).
cnf(c_273,negated_conjecture,
( the_carrier(sK0) = sK2
| proper_element(sK2,powerset(the_carrier(sK0))) ),
inference(copy,[status(thm)],[c_7929]) ).
cnf(c_7930,negated_conjecture,
( in(bottom_of_relstr(sK0),the_carrier(sK0))
| empty(the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_153,c_110]) ).
cnf(c_317,negated_conjecture,
in(bottom_of_relstr(sK0),the_carrier(sK0)),
inference(resolve,[status(thm)],[c_171,c_7930]) ).
cnf(c_7931,plain,
( element(sK1(C,A),C)
| A = C
| element(sK1(C,A),B)
| ~ element(A,powerset(B)) ),
inference(resolve,[status(thm)],[c_113,c_206]) ).
cnf(c_885,negated_conjecture,
( element(sK1(A,sK2),A)
| sK2 = A
| element(sK1(A,sK2),the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_7931,c_127]) ).
cnf(c_7932,plain,
( sK2 = the_carrier(sK0)
| element(sK1(the_carrier(sK0),sK2),the_carrier(sK0)) ),
inference(factor,[status(thm)],[c_885]) ).
cnf(c_898,plain,
( the_carrier(sK0) = sK2
| element(sK1(the_carrier(sK0),sK2),the_carrier(sK0)) ),
inference(copy,[status(thm)],[c_7932]) ).
cnf(c_1657,plain,
( in(bottom_of_relstr(sK0),sK2)
| the_carrier(sK0) = sK2 ),
inference(resolve,[status(thm)],[c_273,c_129]) ).
cnf(c_3545,plain,
( related(sK0,bottom_of_relstr(sK0),sK1(the_carrier(sK0),sK2))
| the_carrier(sK0) = sK2 ),
inference(resolve,[status(thm)],[c_898,c_146]) ).
cnf(c_7933,plain,
( in(sK1(the_carrier(sK0),sK2),the_carrier(sK0))
| empty(the_carrier(sK0))
| the_carrier(sK0) = sK2 ),
inference(resolve,[status(thm)],[c_898,c_110]) ).
cnf(c_3546,negated_conjecture,
( in(sK1(the_carrier(sK0),sK2),the_carrier(sK0))
| the_carrier(sK0) = sK2 ),
inference(resolve,[status(thm)],[c_171,c_7933]) ).
cnf(c_7934,plain,
( sK2 = the_carrier(sK0)
| ~ in(sK1(the_carrier(sK0),sK2),sK2)
| the_carrier(sK0) = sK2 ),
inference(resolve,[status(thm)],[c_3546,c_112]) ).
cnf(c_7935,plain,
( the_carrier(sK0) = sK2
| ~ in(sK1(the_carrier(sK0),sK2),sK2)
| the_carrier(sK0) = sK2 ),
inference(copy,[status(thm)],[c_7934]) ).
cnf(c_3719,plain,
( ~ in(sK1(the_carrier(sK0),sK2),sK2)
| the_carrier(sK0) = sK2 ),
inference(copy,[status(thm)],[c_7935]) ).
cnf(c_7936,negated_conjecture,
( in(B,sK2)
| ~ related(sK0,A,B)
| ~ in(A,sK2)
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0))
| ~ upper_relstr_subset(sK2,sK0) ),
inference(resolve,[status(thm)],[c_160,c_127]) ).
cnf(c_7937,negated_conjecture,
( in(B,sK2)
| ~ related(sK0,A,B)
| ~ in(A,sK2)
| ~ element(B,the_carrier(sK0))
| ~ element(A,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_7936,c_126]) ).
cnf(c_7938,negated_conjecture,
( in(A,sK2)
| ~ related(sK0,bottom_of_relstr(sK0),A)
| ~ in(bottom_of_relstr(sK0),sK2)
| ~ element(A,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_7937,c_153]) ).
cnf(c_7939,negated_conjecture,
( the_carrier(sK0) = sK2
| in(sK1(the_carrier(sK0),sK2),sK2)
| ~ related(sK0,bottom_of_relstr(sK0),sK1(the_carrier(sK0),sK2))
| ~ in(bottom_of_relstr(sK0),sK2) ),
inference(resolve,[status(thm)],[c_7938,c_898]) ).
cnf(c_7940,negated_conjecture,
( the_carrier(sK0) = sK2
| the_carrier(sK0) = sK2
| in(sK1(the_carrier(sK0),sK2),sK2)
| ~ related(sK0,bottom_of_relstr(sK0),sK1(the_carrier(sK0),sK2)) ),
inference(resolve,[status(thm)],[c_7939,c_1657]) ).
cnf(c_7941,negated_conjecture,
( the_carrier(sK0) = sK2
| the_carrier(sK0) = sK2
| the_carrier(sK0) = sK2
| in(sK1(the_carrier(sK0),sK2),sK2) ),
inference(resolve,[status(thm)],[c_7940,c_3545]) ).
cnf(c_7942,negated_conjecture,
( the_carrier(sK0) = sK2
| the_carrier(sK0) = sK2
| in(sK1(the_carrier(sK0),sK2),sK2) ),
inference(copy,[status(thm)],[c_7941]) ).
cnf(c_7190,negated_conjecture,
( the_carrier(sK0) = sK2
| in(sK1(the_carrier(sK0),sK2),sK2) ),
inference(copy,[status(thm)],[c_7942]) ).
cnf(c_7943,plain,
( the_carrier(sK0) = sK2
| the_carrier(sK0) = sK2 ),
inference(resolve,[status(thm)],[c_7190,c_3719]) ).
cnf(c_7191,plain,
the_carrier(sK0) = sK2,
inference(copy,[status(thm)],[c_7943]) ).
cnf(c_7907,negated_conjecture,
in(bottom_of_relstr(sK0),sK2),
inference(paramod,[status(thm)],[c_7191,c_317]) ).
cnf(c_7944,negated_conjecture,
( ~ in(bottom_of_relstr(sK0),sK2)
| proper_element(sK2,powerset(sK2)) ),
inference(paramod,[status(thm)],[c_7191,c_128]) ).
cnf(c_7945,negated_conjecture,
~ in(bottom_of_relstr(sK0),sK2),
inference(resolve,[status(thm)],[c_255,c_7944]) ).
cnf(c_7925,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_7907,c_7945]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU383+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 09:21:10 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 3408404 was started by sandbox2 on n007,
% 0.09/0.36 % Sat Sep 26 09:21:10 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.37
% 0.09/0.37 % From the command line: assign(max_seconds, 300).
% 19.40/3.20
% 19.40/3.20 % given #500 (T,wt=24): 2478 the_carrier(c7) = c8 | element(f3(f4(c7)),c8). [resolve(1665,a,109,a)].
% 19.40/3.20
% 19.40/3.20 % given #1000 (F,wt=26): 7014 -in(f5(f5(c5)),powerset(empty_set)). [ur(113,b,75,a,c,3664,a)].
% 19.40/3.20
% 19.40/3.20 % SZS status Theorem for theBenchmark
% 19.40/3.20
% 19.40/3.20 % Proof 1 at 2.35 (+ 0.33) seconds.
% 19.40/3.20 % Length of proof is 57.
% 19.40/3.20 % Level of proof is 9.
% 19.40/3.20 % Maximum clause weight is 41.000.
% 19.40/3.20 % Given clauses 1008.
% 19.40/3.20
% 19.40/3.20 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------