%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU321+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 : n020.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:48 AM UTC 2026
% Result : Theorem 0.21s 5.57s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 10
% Syntax : Number of formulae : 59 ( 18 unt; 0 def)
% Number of atoms : 158 ( 13 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 155 ( 56 ~; 56 |; 26 &)
% ( 2 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 58 ( 2 sgn 28 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(rc5_struct_0,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ? [B] :
( ~ empty(B)
& element(B,powerset(the_carrier(A))) ) ),
file('theBenchmark.p',rc5_struct_0) ).
fof(t2_subset,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('theBenchmark.p',t2_subset) ).
fof(existence_m1_subset_1,axiom,
! [A] :
? [B] : element(B,A),
file('theBenchmark.p',existence_m1_subset_1) ).
fof(fc1_struct_0,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ~ empty(the_carrier(A)) ),
file('theBenchmark.p',fc1_struct_0) ).
fof(fc6_membered,axiom,
( v5_membered(empty_set)
& v4_membered(empty_set)
& v3_membered(empty_set)
& v2_membered(empty_set)
& v1_membered(empty_set)
& empty(empty_set) ),
file('theBenchmark.p',fc6_membered) ).
fof(t4_subset,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('theBenchmark.p',t4_subset) ).
fof(t7_boole,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('theBenchmark.p',t7_boole) ).
fof(t50_subset_1,axiom,
! [A] :
( A != empty_set
=> ! [B] :
( element(B,powerset(A))
=> ! [C] :
( element(C,A)
=> ( ~ in(C,B)
=> in(C,subset_complement(A,B)) ) ) ) ),
file('theBenchmark.p',t50_subset_1) ).
fof(t54_subset_1,axiom,
! [A,B,C] :
( element(C,powerset(A))
=> ~ ( in(B,C)
& in(B,subset_complement(A,C)) ) ),
file('theBenchmark.p',t54_subset_1) ).
fof(l40_tops_1,conjecture,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ! [C] :
( element(C,the_carrier(A))
=> ( in(C,subset_complement(the_carrier(A),B))
<=> ~ in(C,B) ) ) ) ),
file('theBenchmark.p',l40_tops_1) ).
fof(l40_tops_1_neg,negated_conjecture,
~ ! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ! [C] :
( element(C,the_carrier(A))
=> ( in(C,subset_complement(the_carrier(A),B))
<=> ~ in(C,B) ) ) ) ),
inference(assume_negation,[status(cth)],[l40_tops_1]) ).
cnf(c_46,plain,
( ~ empty(the_carrier(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[fc1_struct_0]) ).
fof(nnf_42,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( in(C,B)
| ~ in(C,subset_complement(the_carrier(A),B)) )
& ( ~ in(C,B)
| in(C,subset_complement(the_carrier(A),B)) )
& element(C,the_carrier(A)) )
& element(B,powerset(the_carrier(A))) )
& one_sorted_str(A)
& ~ empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[l40_tops_1_neg]) ).
fof(sk_l40_tops_1_neg,plain,
( ( in(sK2,sK3)
| ~ in(sK2,subset_complement(the_carrier(sK0),sK3)) )
& ( ~ in(sK2,sK3)
| in(sK2,subset_complement(the_carrier(sK0),sK3)) )
& element(sK2,the_carrier(sK0))
& element(sK3,powerset(the_carrier(sK0)))
& one_sorted_str(sK0)
& ~ empty_carrier(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK3,sK2]),skolemize(A,sK0),skolemize(B,sK3),skolemize(C,sK2)],[nnf_42]) ).
cnf(c_47,negated_conjecture,
one_sorted_str(sK0),
inference(split_conjunct,[status(thm)],[sk_l40_tops_1_neg]) ).
fof(nnf_2,plain,
! [A] :
( ? [B] :
( ~ empty(B)
& element(B,powerset(the_carrier(A))) )
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[rc5_struct_0]) ).
fof(sk_rc5_struct_0_sk,plain,
! [A] :
( ( ~ empty(sK1(A))
& element(sK1(A),powerset(the_carrier(A))) )
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(B,sK1(A))],[nnf_2]) ).
fof(sk_rc5_struct_0,plain,
( ! [VAR_0] :
( ~ empty(sK1(VAR_0))
| ~ one_sorted_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0] :
( element(sK1(VAR_0),powerset(the_carrier(VAR_0)))
| ~ one_sorted_str(VAR_0)
| empty_carrier(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_rc5_struct_0_sk]) ).
cnf(c_50,plain,
( ~ empty(sK1(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_rc5_struct_0]) ).
cnf(c_51,plain,
( element(sK1(A),powerset(the_carrier(A)))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_rc5_struct_0]) ).
cnf(c_53,negated_conjecture,
( in(sK2,sK3)
| ~ in(sK2,subset_complement(the_carrier(sK0),sK3)) ),
inference(split_conjunct,[status(thm)],[sk_l40_tops_1_neg]) ).
cnf(c_54,negated_conjecture,
( ~ in(sK2,sK3)
| in(sK2,subset_complement(the_carrier(sK0),sK3)) ),
inference(split_conjunct,[status(thm)],[sk_l40_tops_1_neg]) ).
cnf(c_55,negated_conjecture,
element(sK2,the_carrier(sK0)),
inference(split_conjunct,[status(thm)],[sk_l40_tops_1_neg]) ).
cnf(c_56,negated_conjecture,
element(sK3,powerset(the_carrier(sK0))),
inference(split_conjunct,[status(thm)],[sk_l40_tops_1_neg]) ).
cnf(c_57,negated_conjecture,
~ empty_carrier(sK0),
inference(split_conjunct,[status(thm)],[sk_l40_tops_1_neg]) ).
cnf(c_58,plain,
( ~ in(C,A)
| ~ in(C,subset_complement(B,A))
| ~ element(A,powerset(B)) ),
inference(clausify,[status(thm)],[t54_subset_1]) ).
cnf(c_59,plain,
( in(C,subset_complement(A,B))
| in(C,B)
| ~ element(C,A)
| ~ element(B,powerset(A))
| empty_set = A ),
inference(clausify,[status(thm)],[t50_subset_1]) ).
cnf(c_60,plain,
( ~ empty(B)
| ~ in(A,B) ),
inference(clausify,[status(thm)],[t7_boole]) ).
cnf(c_62,plain,
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(clausify,[status(thm)],[t4_subset]) ).
cnf(c_69,plain,
empty(empty_set),
inference(clausify,[status(thm)],[fc6_membered]) ).
fof(nnf_25,plain,
! [A] :
? [B] : element(B,A),
inference(fof_nnf,[status(thm)],[existence_m1_subset_1]) ).
fof(sk_existence_m1_subset_1,plain,
! [A] : element(sK4(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(B,sK4(A))],[nnf_25]) ).
cnf(c_72,plain,
element(sK4(A),A),
inference(split_conjunct,[status(thm)],[sk_existence_m1_subset_1]) ).
cnf(c_77,plain,
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(clausify,[status(thm)],[t2_subset]) ).
cnf(c_108,negated_conjecture,
( ~ empty(the_carrier(sK0))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_46,c_47]) ).
cnf(c_109,negated_conjecture,
~ empty(the_carrier(sK0)),
inference(resolve,[status(thm)],[c_57,c_108]) ).
cnf(c_116,negated_conjecture,
( ~ empty(sK1(sK0))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_50,c_47]) ).
cnf(c_117,negated_conjecture,
~ empty(sK1(sK0)),
inference(resolve,[status(thm)],[c_57,c_116]) ).
cnf(c_121,negated_conjecture,
( element(sK1(sK0),powerset(the_carrier(sK0)))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_51,c_47]) ).
cnf(c_122,negated_conjecture,
element(sK1(sK0),powerset(the_carrier(sK0))),
inference(resolve,[status(thm)],[c_57,c_121]) ).
cnf(c_856,negated_conjecture,
( in(A,subset_complement(the_carrier(sK0),sK3))
| in(A,sK3)
| ~ element(A,the_carrier(sK0))
| empty_set = the_carrier(sK0) ),
inference(resolve,[status(thm)],[c_59,c_56]) ).
cnf(c_126,negated_conjecture,
( in(A,subset_complement(the_carrier(sK0),sK3))
| in(A,sK3)
| ~ element(A,the_carrier(sK0))
| the_carrier(sK0) = empty_set ),
inference(copy,[status(thm)],[c_856]) ).
cnf(c_132,plain,
~ in(A,empty_set),
inference(resolve,[status(thm)],[c_69,c_60]) ).
cnf(c_146,plain,
( in(sK4(A),A)
| empty(A) ),
inference(resolve,[status(thm)],[c_77,c_72]) ).
cnf(c_258,plain,
( element(A,the_carrier(sK0))
| ~ in(A,sK1(sK0)) ),
inference(resolve,[status(thm)],[c_122,c_62]) ).
cnf(c_283,plain,
( in(sK2,subset_complement(the_carrier(sK0),sK3))
| in(sK2,sK3)
| the_carrier(sK0) = empty_set ),
inference(resolve,[status(thm)],[c_126,c_55]) ).
cnf(c_857,plain,
( empty(sK1(sK0))
| element(sK4(sK1(sK0)),the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_258,c_146]) ).
cnf(c_501,negated_conjecture,
element(sK4(sK1(sK0)),the_carrier(sK0)),
inference(resolve,[status(thm)],[c_117,c_857]) ).
cnf(c_858,plain,
( in(sK4(sK1(sK0)),the_carrier(sK0))
| empty(the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_501,c_77]) ).
cnf(c_548,negated_conjecture,
in(sK4(sK1(sK0)),the_carrier(sK0)),
inference(resolve,[status(thm)],[c_109,c_858]) ).
cnf(c_859,negated_conjecture,
( in(sK2,sK3)
| in(sK2,sK3)
| the_carrier(sK0) = empty_set ),
inference(resolve,[status(thm)],[c_283,c_53]) ).
cnf(c_782,negated_conjecture,
( in(sK2,sK3)
| the_carrier(sK0) = empty_set ),
inference(copy,[status(thm)],[c_859]) ).
cnf(c_791,plain,
( ~ in(sK2,subset_complement(A,sK3))
| ~ element(sK3,powerset(A))
| the_carrier(sK0) = empty_set ),
inference(resolve,[status(thm)],[c_782,c_58]) ).
cnf(c_792,plain,
( in(sK2,subset_complement(the_carrier(sK0),sK3))
| the_carrier(sK0) = empty_set ),
inference(resolve,[status(thm)],[c_782,c_54]) ).
cnf(c_860,plain,
( ~ element(sK3,powerset(the_carrier(sK0)))
| the_carrier(sK0) = empty_set
| the_carrier(sK0) = empty_set ),
inference(resolve,[status(thm)],[c_792,c_791]) ).
cnf(c_861,plain,
( ~ element(sK3,powerset(the_carrier(sK0)))
| the_carrier(sK0) = empty_set ),
inference(copy,[status(thm)],[c_860]) ).
cnf(c_816,negated_conjecture,
the_carrier(sK0) = empty_set,
inference(resolve,[status(thm)],[c_56,c_861]) ).
cnf(c_862,negated_conjecture,
in(sK4(sK1(sK0)),empty_set),
inference(paramod,[status(thm)],[c_816,c_548]) ).
cnf(c_855,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_132,c_862]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU321+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/5.44 % Computer : n020.cluster.edu
% 0.17/5.44 % Model : x86_64 x86_64
% 0.17/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.44 % Memory : 8046.5625MB
% 0.17/5.44 % OS : Linux 6.8.0-71-generic
% 0.17/5.44 % CPULimit : 300
% 0.17/5.44 % WCLimit : 300
% 0.17/5.44 % DateTime : Sat Sep 26 09:12:54 UTC 2026
% 0.17/5.44 % CPUTime :
% 0.17/5.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/5.44 % Process 1185407 was started by sandbox2 on n020,
% 0.17/5.44 % Sat Sep 26 09:12:54 2026
% 0.17/5.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/5.45
% 0.17/5.45 % From the command line: assign(max_seconds, 300).
% 0.21/5.57
% 0.21/5.57 % SZS status Theorem for theBenchmark
% 0.21/5.57
% 0.21/5.57 % Proof 1 at 0.08 (+ 0.03) seconds.
% 0.21/5.57 % Length of proof is 44.
% 0.21/5.57 % Level of proof is 7.
% 0.21/5.57 % Maximum clause weight is 32.000.
% 0.21/5.57 % Given clauses 442.
% 0.21/5.57
% 0.21/5.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------