%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU319+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 : n015.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:42 PM UTC 2026
% Result : Theorem 249.87s 37.65s
% Output : Proof 249.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 6
% Syntax : Number of formulae : 50 ( 12 unt; 0 def)
% Number of atoms : 124 ( 14 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 126 ( 52 ~; 49 |; 11 &)
% ( 3 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-3 aty)
% Number of variables : 48 ( 0 sgn 31 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f16,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> subset_complement(the_carrier(A),B) = subset_difference(the_carrier(A),cast_as_carrier_subset(A),B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_pre_topc) ).
fof(f16_nnf,plain,
! [A] :
( ! [B] :
( subset_complement(the_carrier(A),B) = subset_difference(the_carrier(A),cast_as_carrier_subset(A),B)
| ~ element(B,powerset(the_carrier(A))) )
| ~ one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [A,B] :
( subset_complement(the_carrier(A),B) = subset_difference(the_carrier(A),cast_as_carrier_subset(A),B)
| ~ element(B,powerset(the_carrier(A)))
| ~ one_sorted_str(A) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c17,plain,
( subset_complement(the_carrier(X0),X1) = subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
fof(f6,axiom,
! [A] :
( top_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f6_nnf,plain,
! [A] :
( one_sorted_str(A)
| ~ top_str(A) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A] :
( one_sorted_str(A)
| ~ top_str(A) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c7,plain,
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
fof(f17,conjecture,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( closed_subset(B,A)
<=> open_subset(subset_complement(the_carrier(A),B),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_tops_1) ).
fof(f17_neg,negated_conjecture,
~ ! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( closed_subset(B,A)
<=> open_subset(subset_complement(the_carrier(A),B),A) ) ) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f17_nnf,plain,
? [A] :
( ? [B] :
( ( ( open_subset(subset_complement(the_carrier(A),B),A)
& ~ closed_subset(B,A) )
| ( ~ open_subset(subset_complement(the_carrier(A),B),A)
& closed_subset(B,A) ) )
& element(B,powerset(the_carrier(A))) )
& top_str(A) ),
inference(nnf_transformation,[status(thm)],[f17_neg]) ).
fof(f17_sk,plain,
( ( ( open_subset(subset_complement(the_carrier(sk3),sk4),sk3)
& ~ closed_subset(sk4,sk3) )
| ( ~ open_subset(subset_complement(the_carrier(sk3),sk4),sk3)
& closed_subset(sk4,sk3) ) )
& element(sk4,powerset(the_carrier(sk3)))
& top_str(sk3) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk3,sk4])],[f17_nnf]) ).
cnf(c18,plain,
top_str(sk3),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p31,plain,
one_sorted_str(sk3),
inference(resolution,[status(thm)],[c7,c18]) ).
cnf(p84,plain,
( subset_complement(the_carrier(sk3),X0) = subset_difference(the_carrier(sk3),cast_as_carrier_subset(sk3),X0)
| ~ element(X0,powerset(the_carrier(sk3))) ),
inference(resolution,[status(thm)],[c17,p31]) ).
cnf(c19,plain,
element(sk4,powerset(the_carrier(sk3))),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p1983,plain,
subset_complement(the_carrier(sk3),sk4) = subset_difference(the_carrier(sk3),cast_as_carrier_subset(sk3),sk4),
inference(resolution,[status(thm)],[p84,c19]) ).
fof(f14,axiom,
! [A,B,C] :
( ( element(C,powerset(A))
& element(B,powerset(A)) )
=> subset_difference(A,B,C) = set_difference(B,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_subset_1) ).
fof(f14_nnf,plain,
! [A,B,C] :
( subset_difference(A,B,C) = set_difference(B,C)
| ~ element(C,powerset(A))
| ~ element(B,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [B,A,C] :
( subset_difference(A,B,C) = set_difference(B,C)
| ~ element(C,powerset(A))
| ~ element(B,powerset(A)) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c15,plain,
( subset_difference(X0,X1,X2) = set_difference(X1,X2)
| ~ element(X2,powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
fof(f2,axiom,
! [A] :
( one_sorted_str(A)
=> element(cast_as_carrier_subset(A),powerset(the_carrier(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_pre_topc) ).
fof(f2_nnf,plain,
! [A] :
( element(cast_as_carrier_subset(A),powerset(the_carrier(A)))
| ~ one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A] :
( element(cast_as_carrier_subset(A),powerset(the_carrier(A)))
| ~ one_sorted_str(A) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c3,plain,
( element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p34,plain,
element(cast_as_carrier_subset(sk3),powerset(the_carrier(sk3))),
inference(resolution,[status(thm)],[p31,c3]) ).
cnf(p69,plain,
( subset_difference(the_carrier(sk3),cast_as_carrier_subset(sk3),X0) = set_difference(cast_as_carrier_subset(sk3),X0)
| ~ element(X0,powerset(the_carrier(sk3))) ),
inference(resolution,[status(thm)],[c15,p34]) ).
cnf(p971,plain,
subset_difference(the_carrier(sk3),cast_as_carrier_subset(sk3),sk4) = set_difference(cast_as_carrier_subset(sk3),sk4),
inference(resolution,[status(thm)],[p69,c19]) ).
cnf(p5624,plain,
subset_complement(the_carrier(sk3),sk4) = set_difference(cast_as_carrier_subset(sk3),sk4),
inference(superposition,[status(thm)],[p1983,p971]) ).
cnf(p5626,plain,
set_difference(cast_as_carrier_subset(sk3),sk4) = subset_complement(the_carrier(sk3),sk4),
inference(superposition,[status(thm)],[p5624,p971]) ).
fof(f0,axiom,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( closed_subset(B,A)
<=> open_subset(subset_difference(the_carrier(A),cast_as_carrier_subset(A),B),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_pre_topc) ).
fof(f0_nnf,plain,
! [A] :
( ! [B] :
( ( ( ~ open_subset(subset_difference(the_carrier(A),cast_as_carrier_subset(A),B),A)
| closed_subset(B,A) )
& ( open_subset(subset_difference(the_carrier(A),cast_as_carrier_subset(A),B),A)
| ~ closed_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] :
( ( ( ~ open_subset(subset_difference(the_carrier(A),cast_as_carrier_subset(A),B),A)
| closed_subset(B,A) )
& ( open_subset(subset_difference(the_carrier(A),cast_as_carrier_subset(A),B),A)
| ~ closed_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( open_subset(subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1),X0)
| ~ closed_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p27,plain,
( open_subset(subset_difference(the_carrier(sk3),cast_as_carrier_subset(sk3),X0),sk3)
| ~ closed_subset(X0,sk3)
| ~ element(X0,powerset(the_carrier(sk3))) ),
inference(resolution,[status(thm)],[c18,c0]) ).
cnf(p131,plain,
( open_subset(subset_difference(the_carrier(sk3),cast_as_carrier_subset(sk3),sk4),sk3)
| ~ closed_subset(sk4,sk3) ),
inference(resolution,[status(thm)],[p27,c19]) ).
cnf(p972,plain,
( open_subset(set_difference(cast_as_carrier_subset(sk3),sk4),sk3)
| ~ closed_subset(sk4,sk3) ),
inference(demodulation,[status(thm)],[p971,p131]) ).
cnf(p5628,plain,
( open_subset(subset_complement(the_carrier(sk3),sk4),sk3)
| ~ closed_subset(sk4,sk3) ),
inference(demodulation,[status(thm)],[p5626,p972]) ).
cnf(c1,plain,
( ~ open_subset(subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1),X0)
| closed_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p29,plain,
( ~ open_subset(subset_difference(the_carrier(sk3),cast_as_carrier_subset(sk3),X0),sk3)
| closed_subset(X0,sk3)
| ~ element(X0,powerset(the_carrier(sk3))) ),
inference(resolution,[status(thm)],[c1,c18]) ).
cnf(p178,plain,
( ~ open_subset(subset_difference(the_carrier(sk3),cast_as_carrier_subset(sk3),sk4),sk3)
| closed_subset(sk4,sk3) ),
inference(resolution,[status(thm)],[p29,c19]) ).
cnf(p973,plain,
( ~ open_subset(set_difference(cast_as_carrier_subset(sk3),sk4),sk3)
| closed_subset(sk4,sk3) ),
inference(demodulation,[status(thm)],[p971,p178]) ).
cnf(p5625,plain,
( ~ open_subset(subset_complement(the_carrier(sk3),sk4),sk3)
| closed_subset(sk4,sk3) ),
inference(superposition,[status(thm)],[p5624,p973]) ).
cnf(c21,plain,
( open_subset(subset_complement(the_carrier(sk3),sk4),sk3)
| closed_subset(sk4,sk3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p5662,plain,
( closed_subset(sk4,sk3)
| closed_subset(sk4,sk3) ),
inference(resolution,[status(thm)],[p5625,c21]) ).
cnf(p5663,plain,
closed_subset(sk4,sk3),
inference(factoring,[status(thm)],[p5662]) ).
cnf(p5699,plain,
open_subset(subset_complement(the_carrier(sk3),sk4),sk3),
inference(resolution,[status(thm)],[p5628,p5663]) ).
cnf(c22,plain,
( ~ closed_subset(sk4,sk3)
| ~ open_subset(subset_complement(the_carrier(sk3),sk4),sk3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p5700,plain,
~ closed_subset(sk4,sk3),
inference(resolution,[status(thm)],[p5699,c22]) ).
cnf(p5701,plain,
$false,
inference(resolution,[status(thm)],[p5700,p5663]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU319+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n015.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 13:43:57 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 249.87/37.65 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 249.87/37.65 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------