%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU321+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n014.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 : Fri Sep 25 02:51:43 PM UTC 2026
% Result : Theorem 25.85s 4.36s
% Output : Proof 25.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 5
% Syntax : Number of formulae : 39 ( 7 unt; 0 def)
% Number of atoms : 128 ( 8 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 135 ( 46 ~; 44 |; 31 &)
% ( 2 <=>; 12 =>; 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 : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 39 ( 0 sgn 27 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f40,axiom,
! [A] :
( A != empty_set
=> ! [B] :
( element(B,powerset(A))
=> ! [C] :
( element(C,A)
=> ( ~ in(C,B)
=> in(C,subset_complement(A,B)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t50_subset_1) ).
fof(f40_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( in(C,subset_complement(A,B))
| in(C,B)
| ~ element(C,A) )
| ~ element(B,powerset(A)) )
| A = empty_set ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [A,B,C] :
( in(C,subset_complement(A,B))
| in(C,B)
| ~ element(C,A)
| ~ element(B,powerset(A))
| A = empty_set ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c84,plain,
( in(X2,subset_complement(X0,X1))
| in(X2,X1)
| ~ element(X2,X0)
| ~ element(X1,powerset(X0))
| X0 = empty_set ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
fof(f39,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('/export/starexec/sandbox2/benchmark/theBenchmark.p',l40_tops_1) ).
fof(f39_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(negated_conjecture,[status(cth)],[f39]) ).
fof(f39_nnf,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(nnf_transformation,[status(thm)],[f39_neg]) ).
fof(f39_sk,plain,
( ( ( ~ in(sk7,sk6)
& ~ in(sk7,subset_complement(the_carrier(sk5),sk6)) )
| ( in(sk7,sk6)
& in(sk7,subset_complement(the_carrier(sk5),sk6)) ) )
& element(sk7,the_carrier(sk5))
& element(sk6,powerset(the_carrier(sk5)))
& one_sorted_str(sk5)
& ~ empty_carrier(sk5) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5,sk6,sk7])],[f39_nnf]) ).
cnf(c78,plain,
element(sk6,powerset(the_carrier(sk5))),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p231,plain,
( in(X0,subset_complement(the_carrier(sk5),sk6))
| in(X0,sk6)
| ~ element(X0,the_carrier(sk5))
| the_carrier(sk5) = empty_set ),
inference(resolution,[status(thm)],[c84,c78]) ).
cnf(c79,plain,
element(sk7,the_carrier(sk5)),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p259,plain,
( in(sk7,subset_complement(the_carrier(sk5),sk6))
| in(sk7,sk6)
| the_carrier(sk5) = empty_set ),
inference(resolution,[status(thm)],[p231,c79]) ).
cnf(c82,plain,
( ~ in(sk7,subset_complement(the_carrier(sk5),sk6))
| in(sk7,sk6) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p261,plain,
( in(sk7,sk6)
| in(sk7,sk6)
| the_carrier(sk5) = empty_set ),
inference(resolution,[status(thm)],[p259,c82]) ).
cnf(p267,plain,
( in(sk7,sk6)
| the_carrier(sk5) = empty_set ),
inference(factoring,[status(thm)],[p261]) ).
fof(f32,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ~ empty(the_carrier(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f32_nnf,plain,
! [A] :
( ~ empty(the_carrier(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [A] :
( ~ empty(the_carrier(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c63,plain,
( ~ empty(the_carrier(X0))
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(c77,plain,
one_sorted_str(sk5),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p118,plain,
( ~ empty(the_carrier(sk5))
| empty_carrier(sk5) ),
inference(resolution,[status(thm)],[c63,c77]) ).
cnf(p275,plain,
( ~ empty(empty_set)
| empty_carrier(sk5)
| in(sk7,sk6) ),
inference(superposition,[status(thm)],[p267,p118]) ).
fof(f33,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('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_membered) ).
fof(f33_nnf,plain,
( v5_membered(empty_set)
& v4_membered(empty_set)
& v3_membered(empty_set)
& v2_membered(empty_set)
& v1_membered(empty_set)
& empty(empty_set) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
( v5_membered(empty_set)
& v4_membered(empty_set)
& v3_membered(empty_set)
& v2_membered(empty_set)
& v1_membered(empty_set)
& empty(empty_set) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c64,plain,
empty(empty_set),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p376,plain,
( empty_carrier(sk5)
| in(sk7,sk6) ),
inference(resolution,[status(thm)],[p275,c64]) ).
cnf(c81,plain,
( ~ in(sk7,sk6)
| in(sk7,subset_complement(the_carrier(sk5),sk6)) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p377,plain,
( in(sk7,subset_complement(the_carrier(sk5),sk6))
| empty_carrier(sk5) ),
inference(resolution,[status(thm)],[p376,c81]) ).
fof(f41,axiom,
! [A,B,C] :
( element(C,powerset(A))
=> ~ ( in(B,C)
& in(B,subset_complement(A,C)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t54_subset_1) ).
fof(f41_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c85,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p241,plain,
( ~ in(X0,sk6)
| ~ in(X0,subset_complement(the_carrier(sk5),sk6)) ),
inference(resolution,[status(thm)],[c85,c78]) ).
cnf(p533,plain,
( ~ in(sk7,sk6)
| empty_carrier(sk5) ),
inference(resolution,[status(thm)],[p377,p241]) ).
cnf(p536,plain,
( empty_carrier(sk5)
| empty_carrier(sk5) ),
inference(resolution,[status(thm)],[p533,p376]) ).
cnf(p538,plain,
empty_carrier(sk5),
inference(factoring,[status(thm)],[p536]) ).
cnf(c76,plain,
~ empty_carrier(sk5),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p540,plain,
$false,
inference(resolution,[status(thm)],[p538,c76]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU321+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n014.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 13:41:03 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 25.85/4.36 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 25.85/4.36 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------