%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU341+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n008.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:47 PM UTC 2026
% Result : Theorem 75.06s 10.01s
% Output : Proof 75.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 48
% Syntax : Number of formulae : 279 ( 127 unt; 0 def)
% Number of atoms : 940 ( 211 equ)
% Maximal formula atoms : 49 ( 3 avg)
% Number of connectives : 1138 ( 477 ~; 294 |; 295 &)
% ( 12 <=>; 60 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 4 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 41 ( 39 usr; 1 prp; 0-3 aty)
% Number of functors : 51 ( 51 usr; 19 con; 0-4 aty)
% Number of variables : 452 ( 23 sgn 285 !; 42 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f50,axiom,
! [A] :
( ( top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,powerset(the_carrier(A)))
=> ( point_neighbourhood(C,A,B)
<=> in(B,interior(A,C)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_connsp_2) ).
fof(f50_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ in(B,interior(A,C))
| point_neighbourhood(C,A,B) )
& ( in(B,interior(A,C))
| ~ point_neighbourhood(C,A,B) ) )
| ~ element(C,powerset(the_carrier(A))) )
| ~ element(B,the_carrier(A)) )
| ~ top_str(A)
| ~ topological_space(A)
| empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
! [A,B,C] :
( ( ( ~ in(B,interior(A,C))
| point_neighbourhood(C,A,B) )
& ( in(B,interior(A,C))
| ~ point_neighbourhood(C,A,B) ) )
| ~ element(C,powerset(the_carrier(A)))
| ~ element(B,the_carrier(A))
| ~ top_str(A)
| ~ topological_space(A)
| empty_carrier(A) ),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c168,plain,
( ~ in(X1,interior(X0,X2))
| point_neighbourhood(X2,X0,X1)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ element(X1,the_carrier(X0))
| ~ top_str(X0)
| ~ topological_space(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(t193,plain,
ifeq(topological_space(X1),true,ifeq(top_str(X1),true,ifeq(element(X2,the_carrier(X1)),true,ifeq(element(X3,powerset(the_carrier(X1))),true,ifeq(in(X2,interior(X1,X3)),true,or(empty_carrier(X1),point_neighbourhood(X3,X1,X2)),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c168]) ).
cnf(t366,plain,
ifeq(topological_space(X1),true,ifeq(top_str(X1),true,ifeq(element(X2,the_carrier(X1)),true,ifeq(element(X3,powerset(the_carrier(X1))),true,ifeq(in(X2,interior(X1,X3)),true,or(empty_carrier(X1),point_neighbourhood(X3,X1,X2)),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t193]) ).
fof(f530,conjecture,
! [A] :
( ( top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ! [C] :
( element(C,the_carrier(A))
=> ( ( in(C,B)
& open_subset(B,A) )
=> point_neighbourhood(B,A,C) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_connsp_2) ).
fof(f530_neg,negated_conjecture,
~ ! [A] :
( ( top_str(A)
& topological_space(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ! [C] :
( element(C,the_carrier(A))
=> ( ( in(C,B)
& open_subset(B,A) )
=> point_neighbourhood(B,A,C) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f530]) ).
fof(f530_nnf,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ point_neighbourhood(B,A,C)
& in(C,B)
& open_subset(B,A)
& element(C,the_carrier(A)) )
& element(B,powerset(the_carrier(A))) )
& top_str(A)
& topological_space(A)
& ~ empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f530_neg]) ).
fof(f530_sk,plain,
( ~ point_neighbourhood(sk424,sk423,sk425)
& in(sk425,sk424)
& open_subset(sk424,sk423)
& element(sk425,the_carrier(sk423))
& element(sk424,powerset(the_carrier(sk423)))
& top_str(sk423)
& topological_space(sk423)
& ~ empty_carrier(sk423) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk423,sk424,sk425])],[f530_nnf]) ).
cnf(c2788,plain,
~ point_neighbourhood(sk424,sk423,sk425),
inference(cnf_transformation,[status(esa)],[f530_sk]) ).
cnf(t58,plain,
point_neighbourhood(sk424,sk423,sk425) = false,
inference(equality_encoding,[status(esa)],[c2788]) ).
cnf(t1081,plain,
point_neighbourhood(sk424,sk423,sk425) = false,
inference(orient,[status(thm)],[t58]) ).
cnf(t1082,plain,
true = ifeq(topological_space(sk423),true,ifeq(top_str(sk423),true,ifeq(element(sk425,the_carrier(sk423)),true,ifeq(element(sk424,powerset(the_carrier(sk423))),true,ifeq(in(sk425,interior(sk423,sk424)),true,or(empty_carrier(sk423),false),true),true),true),true),true),
inference(cp,[status(thm)],[t366,t1081]) ).
cnf(c2782,plain,
topological_space(sk423),
inference(cnf_transformation,[status(esa)],[f530_sk]) ).
cnf(t20,plain,
topological_space(sk423) = true,
inference(equality_encoding,[status(esa)],[c2782]) ).
cnf(t910,plain,
topological_space(sk423) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(t21615,plain,
true = ifeq(true,true,ifeq(top_str(sk423),true,ifeq(element(sk425,the_carrier(sk423)),true,ifeq(element(sk424,powerset(the_carrier(sk423))),true,ifeq(in(sk425,interior(sk423,sk424)),true,or(empty_carrier(sk423),false),true),true),true),true),true),
inference(step,[status(thm)],[t1082,t910]) ).
cnf(t61,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t200,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t61]) ).
cnf(t21616,plain,
true = ifeq(top_str(sk423),true,ifeq(element(sk425,the_carrier(sk423)),true,ifeq(element(sk424,powerset(the_carrier(sk423))),true,ifeq(in(sk425,interior(sk423,sk424)),true,or(empty_carrier(sk423),false),true),true),true),true),
inference(step,[status(thm)],[t21615,t200]) ).
cnf(c2783,plain,
top_str(sk423),
inference(cnf_transformation,[status(esa)],[f530_sk]) ).
cnf(t19,plain,
top_str(sk423) = true,
inference(equality_encoding,[status(esa)],[c2783]) ).
cnf(t811,plain,
top_str(sk423) = true,
inference(orient,[status(thm)],[t19]) ).
cnf(t21617,plain,
true = ifeq(true,true,ifeq(element(sk425,the_carrier(sk423)),true,ifeq(element(sk424,powerset(the_carrier(sk423))),true,ifeq(in(sk425,interior(sk423,sk424)),true,or(empty_carrier(sk423),false),true),true),true),true),
inference(step,[status(thm)],[t21616,t811]) ).
cnf(t21618,plain,
true = ifeq(element(sk425,the_carrier(sk423)),true,ifeq(element(sk424,powerset(the_carrier(sk423))),true,ifeq(in(sk425,interior(sk423,sk424)),true,or(empty_carrier(sk423),false),true),true),true),
inference(step,[status(thm)],[t21617,t200]) ).
cnf(c2785,plain,
element(sk425,the_carrier(sk423)),
inference(cnf_transformation,[status(esa)],[f530_sk]) ).
cnf(t56,plain,
element(sk425,the_carrier(sk423)) = true,
inference(equality_encoding,[status(esa)],[c2785]) ).
cnf(t503,plain,
element(sk425,the_carrier(sk423)) = true,
inference(orient,[status(thm)],[t56]) ).
cnf(t21619,plain,
true = ifeq(true,true,ifeq(element(sk424,powerset(the_carrier(sk423))),true,ifeq(in(sk425,interior(sk423,sk424)),true,or(empty_carrier(sk423),false),true),true),true),
inference(step,[status(thm)],[t21618,t503]) ).
cnf(t21620,plain,
true = ifeq(element(sk424,powerset(the_carrier(sk423))),true,ifeq(in(sk425,interior(sk423,sk424)),true,or(empty_carrier(sk423),false),true),true),
inference(step,[status(thm)],[t21619,t200]) ).
cnf(c2784,plain,
element(sk424,powerset(the_carrier(sk423))),
inference(cnf_transformation,[status(esa)],[f530_sk]) ).
cnf(t60,plain,
element(sk424,powerset(the_carrier(sk423))) = true,
inference(equality_encoding,[status(esa)],[c2784]) ).
cnf(t456,plain,
element(sk424,powerset(the_carrier(sk423))) = true,
inference(orient,[status(thm)],[t60]) ).
cnf(t21621,plain,
true = ifeq(true,true,ifeq(in(sk425,interior(sk423,sk424)),true,or(empty_carrier(sk423),false),true),true),
inference(step,[status(thm)],[t21620,t456]) ).
cnf(t21622,plain,
true = ifeq(in(sk425,interior(sk423,sk424)),true,or(empty_carrier(sk423),false),true),
inference(step,[status(thm)],[t21621,t200]) ).
fof(f65,axiom,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> interior(A,B) = subset_complement(the_carrier(A),topstr_closure(A,subset_complement(the_carrier(A),B))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_tops_1) ).
fof(f65_nnf,plain,
! [A] :
( ! [B] :
( interior(A,B) = subset_complement(the_carrier(A),topstr_closure(A,subset_complement(the_carrier(A),B)))
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
! [A,B] :
( interior(A,B) = subset_complement(the_carrier(A),topstr_closure(A,subset_complement(the_carrier(A),B)))
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(skolemisation,[status(esa)],[f65_nnf]) ).
cnf(c246,plain,
( interior(X0,X1) = subset_complement(the_carrier(X0),topstr_closure(X0,subset_complement(the_carrier(X0),X1)))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
cnf(t192,plain,
ifeq(top_str(X1),true,ifeq(element(X2,powerset(the_carrier(X1))),true,interior(X1,X2),subset_complement(the_carrier(X1),topstr_closure(X1,subset_complement(the_carrier(X1),X2)))),subset_complement(the_carrier(X1),topstr_closure(X1,subset_complement(the_carrier(X1),X2)))) = subset_complement(the_carrier(X1),topstr_closure(X1,subset_complement(the_carrier(X1),X2))),
inference(equality_encoding,[status(esa)],[c246]) ).
cnf(t959,plain,
ifeq(top_str(X1),true,ifeq(element(X2,powerset(the_carrier(X1))),true,interior(X1,X2),subset_complement(the_carrier(X1),topstr_closure(X1,subset_complement(the_carrier(X1),X2)))),subset_complement(the_carrier(X1),topstr_closure(X1,subset_complement(the_carrier(X1),X2)))) = subset_complement(the_carrier(X1),topstr_closure(X1,subset_complement(the_carrier(X1),X2))),
inference(orient,[status(thm)],[t192]) ).
fof(f521,lemma,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( ( ( topstr_closure(A,B) = B
& topological_space(A) )
=> closed_subset(B,A) )
& ( closed_subset(B,A)
=> topstr_closure(A,B) = B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t52_pre_topc) ).
fof(f521_nnf,plain,
! [A] :
( ! [B] :
( ( ( closed_subset(B,A)
| topstr_closure(A,B) != B
| ~ topological_space(A) )
& ( topstr_closure(A,B) = B
| ~ closed_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(nnf_transformation,[status(thm)],[f521]) ).
fof(f521_sk,plain,
! [A,B] :
( ( ( closed_subset(B,A)
| topstr_closure(A,B) != B
| ~ topological_space(A) )
& ( topstr_closure(A,B) = B
| ~ closed_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(skolemisation,[status(esa)],[f521_nnf]) ).
cnf(c2751,plain,
( topstr_closure(X0,X1) = X1
| ~ closed_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f521_sk]) ).
cnf(t176,plain,
ifeq(top_str(X1),true,ifeq(element(X2,powerset(the_carrier(X1))),true,ifeq(closed_subset(X2,X1),true,topstr_closure(X1,X2),X2),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c2751]) ).
cnf(t209,plain,
ifeq(top_str(X1),true,ifeq(element(X2,powerset(the_carrier(X1))),true,ifeq(closed_subset(X2,X1),true,topstr_closure(X1,X2),X2),X2),X2) = X2,
inference(orient,[status(thm)],[t176]) ).
fof(f156,axiom,
! [A,B] :
( element(B,powerset(A))
=> element(subset_complement(A,B),powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_subset_1) ).
fof(f156_nnf,plain,
! [A,B] :
( element(subset_complement(A,B),powerset(A))
| ~ element(B,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f156]) ).
fof(f156_sk,plain,
! [B,A] :
( element(subset_complement(A,B),powerset(A))
| ~ element(B,powerset(A)) ),
inference(skolemisation,[status(esa)],[f156_nnf]) ).
cnf(c571,plain,
( element(subset_complement(X0,X1),powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f156_sk]) ).
cnf(t131,plain,
ifeq(element(X1,powerset(X2)),true,element(subset_complement(X2,X1),powerset(X2)),true) = true,
inference(equality_encoding,[status(esa)],[c571]) ).
cnf(t289,plain,
ifeq(element(X1,powerset(X2)),true,element(subset_complement(X2,X1),powerset(X2)),true) = true,
inference(orient,[status(thm)],[t131]) ).
cnf(t462,plain,
true = ifeq(true,true,element(subset_complement(the_carrier(sk423),sk424),powerset(the_carrier(sk423))),true),
inference(cp,[status(thm)],[t289,t456]) ).
cnf(t21026,plain,
true = element(subset_complement(the_carrier(sk423),sk424),powerset(the_carrier(sk423))),
inference(step,[status(thm)],[t462,t200]) ).
cnf(t5208,plain,
element(subset_complement(the_carrier(sk423),sk424),powerset(the_carrier(sk423))) = true,
inference(orient,[status(thm)],[t21026]) ).
cnf(t5219,plain,
subset_complement(the_carrier(sk423),sk424) = ifeq(top_str(sk423),true,ifeq(true,true,ifeq(closed_subset(subset_complement(the_carrier(sk423),sk424),sk423),true,topstr_closure(sk423,subset_complement(the_carrier(sk423),sk424)),subset_complement(the_carrier(sk423),sk424)),subset_complement(the_carrier(sk423),sk424)),subset_complement(the_carrier(sk423),sk424)),
inference(cp,[status(thm)],[t209,t5208]) ).
cnf(t21029,plain,
subset_complement(the_carrier(sk423),sk424) = ifeq(true,true,ifeq(true,true,ifeq(closed_subset(subset_complement(the_carrier(sk423),sk424),sk423),true,topstr_closure(sk423,subset_complement(the_carrier(sk423),sk424)),subset_complement(the_carrier(sk423),sk424)),subset_complement(the_carrier(sk423),sk424)),subset_complement(the_carrier(sk423),sk424)),
inference(step,[status(thm)],[t5219,t811]) ).
cnf(t21030,plain,
subset_complement(the_carrier(sk423),sk424) = ifeq(true,true,ifeq(closed_subset(subset_complement(the_carrier(sk423),sk424),sk423),true,topstr_closure(sk423,subset_complement(the_carrier(sk423),sk424)),subset_complement(the_carrier(sk423),sk424)),subset_complement(the_carrier(sk423),sk424)),
inference(step,[status(thm)],[t21029,t200]) ).
cnf(t21031,plain,
subset_complement(the_carrier(sk423),sk424) = ifeq(closed_subset(subset_complement(the_carrier(sk423),sk424),sk423),true,topstr_closure(sk423,subset_complement(the_carrier(sk423),sk424)),subset_complement(the_carrier(sk423),sk424)),
inference(step,[status(thm)],[t21030,t200]) ).
fof(f470,lemma,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( open_subset(B,A)
<=> closed_subset(subset_complement(the_carrier(A),B),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_tops_1) ).
fof(f470_nnf,plain,
! [A] :
( ! [B] :
( ( ( ~ closed_subset(subset_complement(the_carrier(A),B),A)
| open_subset(B,A) )
& ( closed_subset(subset_complement(the_carrier(A),B),A)
| ~ open_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(nnf_transformation,[status(thm)],[f470]) ).
fof(f470_sk,plain,
! [A,B] :
( ( ( ~ closed_subset(subset_complement(the_carrier(A),B),A)
| open_subset(B,A) )
& ( closed_subset(subset_complement(the_carrier(A),B),A)
| ~ open_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(skolemisation,[status(esa)],[f470_nnf]) ).
cnf(c2662,plain,
( closed_subset(subset_complement(the_carrier(X0),X1),X0)
| ~ open_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f470_sk]) ).
cnf(t184,plain,
ifeq(top_str(X1),true,ifeq(element(X2,powerset(the_carrier(X1))),true,ifeq(open_subset(X2,X1),true,closed_subset(subset_complement(the_carrier(X1),X2),X1),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c2662]) ).
cnf(t340,plain,
ifeq(top_str(X1),true,ifeq(element(X2,powerset(the_carrier(X1))),true,ifeq(open_subset(X2,X1),true,closed_subset(subset_complement(the_carrier(X1),X2),X1),true),true),true) = true,
inference(orient,[status(thm)],[t184]) ).
cnf(c2786,plain,
open_subset(sk424,sk423),
inference(cnf_transformation,[status(esa)],[f530_sk]) ).
cnf(t38,plain,
open_subset(sk424,sk423) = true,
inference(equality_encoding,[status(esa)],[c2786]) ).
cnf(t922,plain,
open_subset(sk424,sk423) = true,
inference(orient,[status(thm)],[t38]) ).
cnf(t924,plain,
true = ifeq(top_str(sk423),true,ifeq(element(sk424,powerset(the_carrier(sk423))),true,ifeq(true,true,closed_subset(subset_complement(the_carrier(sk423),sk424),sk423),true),true),true),
inference(cp,[status(thm)],[t340,t922]) ).
cnf(t20872,plain,
true = ifeq(true,true,ifeq(element(sk424,powerset(the_carrier(sk423))),true,ifeq(true,true,closed_subset(subset_complement(the_carrier(sk423),sk424),sk423),true),true),true),
inference(step,[status(thm)],[t924,t811]) ).
cnf(t20873,plain,
true = ifeq(element(sk424,powerset(the_carrier(sk423))),true,ifeq(true,true,closed_subset(subset_complement(the_carrier(sk423),sk424),sk423),true),true),
inference(step,[status(thm)],[t20872,t200]) ).
cnf(t20874,plain,
true = ifeq(true,true,ifeq(true,true,closed_subset(subset_complement(the_carrier(sk423),sk424),sk423),true),true),
inference(step,[status(thm)],[t20873,t456]) ).
cnf(t20875,plain,
true = ifeq(true,true,closed_subset(subset_complement(the_carrier(sk423),sk424),sk423),true),
inference(step,[status(thm)],[t20874,t200]) ).
cnf(t20876,plain,
true = closed_subset(subset_complement(the_carrier(sk423),sk424),sk423),
inference(step,[status(thm)],[t20875,t200]) ).
cnf(t2508,plain,
closed_subset(subset_complement(the_carrier(sk423),sk424),sk423) = true,
inference(orient,[status(thm)],[t20876]) ).
cnf(t21032,plain,
subset_complement(the_carrier(sk423),sk424) = ifeq(true,true,topstr_closure(sk423,subset_complement(the_carrier(sk423),sk424)),subset_complement(the_carrier(sk423),sk424)),
inference(step,[status(thm)],[t21031,t2508]) ).
cnf(t21033,plain,
subset_complement(the_carrier(sk423),sk424) = topstr_closure(sk423,subset_complement(the_carrier(sk423),sk424)),
inference(step,[status(thm)],[t21032,t200]) ).
cnf(t5267,plain,
topstr_closure(sk423,subset_complement(the_carrier(sk423),sk424)) = subset_complement(the_carrier(sk423),sk424),
inference(orient,[status(thm)],[t21033]) ).
cnf(t5268,plain,
subset_complement(the_carrier(sk423),topstr_closure(sk423,subset_complement(the_carrier(sk423),sk424))) = ifeq(top_str(sk423),true,ifeq(element(sk424,powerset(the_carrier(sk423))),true,interior(sk423,sk424),subset_complement(the_carrier(sk423),subset_complement(the_carrier(sk423),sk424))),subset_complement(the_carrier(sk423),topstr_closure(sk423,subset_complement(the_carrier(sk423),sk424)))),
inference(cp,[status(thm)],[t959,t5267]) ).
cnf(t21034,plain,
subset_complement(the_carrier(sk423),subset_complement(the_carrier(sk423),sk424)) = ifeq(top_str(sk423),true,ifeq(element(sk424,powerset(the_carrier(sk423))),true,interior(sk423,sk424),subset_complement(the_carrier(sk423),subset_complement(the_carrier(sk423),sk424))),subset_complement(the_carrier(sk423),topstr_closure(sk423,subset_complement(the_carrier(sk423),sk424)))),
inference(step,[status(thm)],[t5268,t5267]) ).
fof(f268,axiom,
! [A,B] :
( element(B,powerset(A))
=> subset_complement(A,subset_complement(A,B)) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',involutiveness_k3_subset_1) ).
fof(f268_nnf,plain,
! [A,B] :
( subset_complement(A,subset_complement(A,B)) = B
| ~ element(B,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f268]) ).
fof(f268_sk,plain,
! [B,A] :
( subset_complement(A,subset_complement(A,B)) = B
| ~ element(B,powerset(A)) ),
inference(skolemisation,[status(esa)],[f268_nnf]) ).
cnf(c765,plain,
( subset_complement(X0,subset_complement(X0,X1)) = X1
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f268_sk]) ).
cnf(t127,plain,
ifeq(element(X1,powerset(X2)),true,subset_complement(X2,subset_complement(X2,X1)),X1) = X1,
inference(equality_encoding,[status(esa)],[c765]) ).
cnf(t203,plain,
ifeq(element(X1,powerset(X2)),true,subset_complement(X2,subset_complement(X2,X1)),X1) = X1,
inference(orient,[status(thm)],[t127]) ).
cnf(t466,plain,
sk424 = ifeq(true,true,subset_complement(the_carrier(sk423),subset_complement(the_carrier(sk423),sk424)),sk424),
inference(cp,[status(thm)],[t203,t456]) ).
cnf(t20940,plain,
sk424 = subset_complement(the_carrier(sk423),subset_complement(the_carrier(sk423),sk424)),
inference(step,[status(thm)],[t466,t200]) ).
cnf(t3492,plain,
subset_complement(the_carrier(sk423),subset_complement(the_carrier(sk423),sk424)) = sk424,
inference(orient,[status(thm)],[t20940]) ).
cnf(t21035,plain,
sk424 = ifeq(top_str(sk423),true,ifeq(element(sk424,powerset(the_carrier(sk423))),true,interior(sk423,sk424),subset_complement(the_carrier(sk423),subset_complement(the_carrier(sk423),sk424))),subset_complement(the_carrier(sk423),topstr_closure(sk423,subset_complement(the_carrier(sk423),sk424)))),
inference(step,[status(thm)],[t21034,t3492]) ).
cnf(t21036,plain,
sk424 = ifeq(true,true,ifeq(element(sk424,powerset(the_carrier(sk423))),true,interior(sk423,sk424),subset_complement(the_carrier(sk423),subset_complement(the_carrier(sk423),sk424))),subset_complement(the_carrier(sk423),topstr_closure(sk423,subset_complement(the_carrier(sk423),sk424)))),
inference(step,[status(thm)],[t21035,t811]) ).
cnf(t21037,plain,
sk424 = ifeq(element(sk424,powerset(the_carrier(sk423))),true,interior(sk423,sk424),subset_complement(the_carrier(sk423),subset_complement(the_carrier(sk423),sk424))),
inference(step,[status(thm)],[t21036,t200]) ).
cnf(t21038,plain,
sk424 = ifeq(true,true,interior(sk423,sk424),subset_complement(the_carrier(sk423),subset_complement(the_carrier(sk423),sk424))),
inference(step,[status(thm)],[t21037,t456]) ).
cnf(t21039,plain,
sk424 = interior(sk423,sk424),
inference(step,[status(thm)],[t21038,t200]) ).
cnf(t5273,plain,
interior(sk423,sk424) = sk424,
inference(orient,[status(thm)],[t21039]) ).
cnf(t21623,plain,
true = ifeq(in(sk425,sk424),true,or(empty_carrier(sk423),false),true),
inference(step,[status(thm)],[t21622,t5273]) ).
cnf(c2787,plain,
in(sk425,sk424),
inference(cnf_transformation,[status(esa)],[f530_sk]) ).
cnf(t37,plain,
in(sk425,sk424) = true,
inference(equality_encoding,[status(esa)],[c2787]) ).
cnf(t377,plain,
in(sk425,sk424) = true,
inference(orient,[status(thm)],[t37]) ).
cnf(t21624,plain,
true = ifeq(true,true,or(empty_carrier(sk423),false),true),
inference(step,[status(thm)],[t21623,t377]) ).
cnf(t21625,plain,
true = or(empty_carrier(sk423),false),
inference(step,[status(thm)],[t21624,t200]) ).
cnf(t39,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t213,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t39]) ).
cnf(t21626,plain,
true = empty_carrier(sk423),
inference(step,[status(thm)],[t21625,t213]) ).
cnf(c2781,plain,
~ empty_carrier(sk423),
inference(cnf_transformation,[status(esa)],[f530_sk]) ).
cnf(t10,plain,
empty_carrier(sk423) = false,
inference(equality_encoding,[status(esa)],[c2781]) ).
cnf(t1075,plain,
empty_carrier(sk423) = false,
inference(orient,[status(thm)],[t10]) ).
cnf(t21627,plain,
true = false,
inference(step,[status(thm)],[t21626,t1075]) ).
cnf(t20432,plain,
false = true,
inference(orient,[status(thm)],[t21627]) ).
fof(f0,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f0_nnf,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f1,axiom,
! [A,B] :
( proper_subset(A,B)
=> ~ proper_subset(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_xboole_0) ).
fof(f1_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ proper_subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ proper_subset(A,B) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( ~ proper_subset(X1,X0)
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(f45,axiom,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ! [C] :
( element(C,powerset(the_carrier(A)))
=> ( C = topstr_closure(A,B)
<=> ! [D] :
( in(D,the_carrier(A))
=> ( in(D,C)
<=> ! [E] :
( element(E,powerset(the_carrier(A)))
=> ~ ( disjoint(B,E)
& in(D,E)
& open_subset(E,A) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d13_pre_topc) ).
fof(f45_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ? [D] :
( ( ( ! [E] :
( ~ disjoint(B,E)
| ~ in(D,E)
| ~ open_subset(E,A)
| ~ element(E,powerset(the_carrier(A))) )
& ~ in(D,C) )
| ( ? [E] :
( disjoint(B,E)
& in(D,E)
& open_subset(E,A)
& element(E,powerset(the_carrier(A))) )
& in(D,C) ) )
& in(D,the_carrier(A)) )
| C = topstr_closure(A,B) )
& ( ! [D] :
( ( ( ? [E] :
( disjoint(B,E)
& in(D,E)
& open_subset(E,A)
& element(E,powerset(the_carrier(A))) )
| in(D,C) )
& ( ! [E] :
( ~ disjoint(B,E)
| ~ in(D,E)
| ~ open_subset(E,A)
| ~ element(E,powerset(the_carrier(A))) )
| ~ in(D,C) ) )
| ~ in(D,the_carrier(A)) )
| C != topstr_closure(A,B) ) )
| ~ element(C,powerset(the_carrier(A))) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [A,B,C,D,E] :
( ( ( ( ( ( ( ~ disjoint(B,E)
| ~ in(sk11(A,B,C),E)
| ~ open_subset(E,A)
| ~ element(E,powerset(the_carrier(A))) )
& ~ in(sk11(A,B,C),C) )
| ( disjoint(B,sk12(A,B,C))
& in(sk11(A,B,C),sk12(A,B,C))
& open_subset(sk12(A,B,C),A)
& element(sk12(A,B,C),powerset(the_carrier(A)))
& in(sk11(A,B,C),C) ) )
& in(sk11(A,B,C),the_carrier(A)) )
| C = topstr_closure(A,B) )
& ( ( ( ( disjoint(B,sk10(A,B,C,D))
& in(D,sk10(A,B,C,D))
& open_subset(sk10(A,B,C,D),A)
& element(sk10(A,B,C,D),powerset(the_carrier(A))) )
| in(D,C) )
& ( ~ disjoint(B,E)
| ~ in(D,E)
| ~ open_subset(E,A)
| ~ element(E,powerset(the_carrier(A)))
| ~ in(D,C) ) )
| ~ in(D,the_carrier(A))
| C != topstr_closure(A,B) ) )
| ~ element(C,powerset(the_carrier(A)))
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk10,sk11,sk12])],[f45_nnf]) ).
cnf(c129,plain,
( ~ disjoint(X1,X4)
| ~ in(X3,X4)
| ~ open_subset(X4,X0)
| ~ element(X4,powerset(the_carrier(X0)))
| ~ in(X3,X2)
| ~ in(X3,the_carrier(X0))
| X2 != topstr_closure(X0,X1)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
fof(f67,axiom,
! [A] :
( relation(A)
=> ! [B,C] :
( C = fiber(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(ordered_pair(D,B),A)
& D != B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_wellord1) ).
fof(f67_nnf,plain,
! [A] :
( ! [B,C] :
( ( ? [D] :
( ( in(ordered_pair(D,B),A)
& D != B
& ~ in(D,C) )
| ( ( ~ in(ordered_pair(D,B),A)
| D = B )
& in(D,C) ) )
| C = fiber(A,B) )
& ( ! [D] :
( ( ~ in(ordered_pair(D,B),A)
| D = B
| in(D,C) )
& ( ( in(ordered_pair(D,B),A)
& D != B )
| ~ in(D,C) ) )
| C != fiber(A,B) ) )
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
! [A,C,B,D] :
( ( ( ( in(ordered_pair(sk38(A,B,C),B),A)
& sk38(A,B,C) != B
& ~ in(sk38(A,B,C),C) )
| ( ( ~ in(ordered_pair(sk38(A,B,C),B),A)
| sk38(A,B,C) = B )
& in(sk38(A,B,C),C) )
| C = fiber(A,B) )
& ( ( ( ~ in(ordered_pair(D,B),A)
| D = B
| in(D,C) )
& ( ( in(ordered_pair(D,B),A)
& D != B )
| ~ in(D,C) ) )
| C != fiber(A,B) ) )
| ~ relation(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk38])],[f67_nnf]) ).
cnf(c251,plain,
( X3 != X1
| ~ in(X3,X2)
| X2 != fiber(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
fof(f69,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f69_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f69]) ).
fof(f69_sk,plain,
! [A,B] :
( ( in(sk41(A),A)
| A = empty_set )
& ( ~ in(B,A)
| A != empty_set ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk41])],[f69_nnf]) ).
cnf(c269,plain,
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(esa)],[f69_sk]) ).
fof(f71,axiom,
! [A] :
( centered(A)
<=> ( ! [B] :
~ ( set_meet(B) = empty_set
& finite(B)
& subset(B,A)
& B != empty_set )
& A != empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_compts_1) ).
fof(f71_nnf,plain,
! [A] :
( ( ? [B] :
( set_meet(B) = empty_set
& finite(B)
& subset(B,A)
& B != empty_set )
| A = empty_set
| centered(A) )
& ( ( ! [B] :
( set_meet(B) != empty_set
| ~ finite(B)
| ~ subset(B,A)
| B = empty_set )
& A != empty_set )
| ~ centered(A) ) ),
inference(nnf_transformation,[status(thm)],[f71]) ).
fof(f71_sk,plain,
! [A,B] :
( ( ( set_meet(sk43(A)) = empty_set
& finite(sk43(A))
& subset(sk43(A),A)
& sk43(A) != empty_set )
| A = empty_set
| centered(A) )
& ( ( ( set_meet(B) != empty_set
| ~ finite(B)
| ~ subset(B,A)
| B = empty_set )
& A != empty_set )
| ~ centered(A) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk43])],[f71_nnf]) ).
cnf(c277,plain,
( X0 != empty_set
| ~ centered(X0) ),
inference(cnf_transformation,[status(esa)],[f71_sk]) ).
fof(f99,axiom,
! [A,B,C] :
( C = set_difference(A,B)
<=> ! [D] :
( in(D,C)
<=> ( ~ in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f99_nnf,plain,
! [A,B,C] :
( ( ? [D] :
( ( ~ in(D,B)
& in(D,A)
& ~ in(D,C) )
| ( ( in(D,B)
| ~ in(D,A) )
& in(D,C) ) )
| C = set_difference(A,B) )
& ( ! [D] :
( ( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f99]) ).
fof(f99_sk,plain,
! [C,A,B,D] :
( ( ( ~ in(sk78(A,B,C),B)
& in(sk78(A,B,C),A)
& ~ in(sk78(A,B,C),C) )
| ( ( in(sk78(A,B,C),B)
| ~ in(sk78(A,B,C),A) )
& in(sk78(A,B,C),C) )
| C = set_difference(A,B) )
& ( ( ( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk78])],[f99_nnf]) ).
cnf(c419,plain,
( ~ in(X3,X1)
| ~ in(X3,X2)
| X2 != set_difference(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f99_sk]) ).
fof(f123,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f123_nnf,plain,
! [A,B] :
( ( A = B
| ~ subset(A,B)
| proper_subset(A,B) )
& ( ( A != B
& subset(A,B) )
| ~ proper_subset(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f123]) ).
fof(f123_sk,plain,
! [A,B] :
( ( A = B
| ~ subset(A,B)
| proper_subset(A,B) )
& ( ( A != B
& subset(A,B) )
| ~ proper_subset(A,B) ) ),
inference(skolemisation,[status(esa)],[f123_nnf]) ).
cnf(c534,plain,
( X0 != X1
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f123_sk]) ).
fof(f210,axiom,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_finset_1) ).
fof(f210_nnf,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(nnf_transformation,[status(thm)],[f210]) ).
fof(f210_sk,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(skolemisation,[status(esa)],[f210_nnf]) ).
cnf(c635,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f210_sk]) ).
fof(f211,axiom,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_finsub_1) ).
fof(f211_nnf,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f211]) ).
fof(f211_sk,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(skolemisation,[status(esa)],[f211_nnf]) ).
cnf(c637,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f211_sk]) ).
fof(f213,axiom,
! [A] : ~ empty(succ(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_ordinal1) ).
fof(f213_nnf,plain,
! [A] : ~ empty(succ(A)),
inference(nnf_transformation,[status(thm)],[f213]) ).
fof(f213_sk,plain,
! [A] : ~ empty(succ(A)),
inference(skolemisation,[status(esa)],[f213_nnf]) ).
cnf(c643,plain,
~ empty(succ(X0)),
inference(cnf_transformation,[status(esa)],[f213_sk]) ).
fof(f214,axiom,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_ordinal2) ).
fof(f214_nnf,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(nnf_transformation,[status(thm)],[f214]) ).
fof(f214_sk,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(skolemisation,[status(esa)],[f214_nnf]) ).
cnf(c647,plain,
~ empty(omega),
inference(cnf_transformation,[status(esa)],[f214_sk]) ).
fof(f218,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f218_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f218]) ).
fof(f218_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f218_nnf]) ).
cnf(c656,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f218_sk]) ).
fof(f220,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f220_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f220]) ).
fof(f220_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f220_nnf]) ).
cnf(c658,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f220_sk]) ).
fof(f224,axiom,
! [A] :
( ( natural(A)
& ordinal(A) )
=> ( natural(succ(A))
& ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_arytm_3) ).
fof(f224_nnf,plain,
! [A] :
( ( natural(succ(A))
& ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ natural(A)
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f224]) ).
fof(f224_sk,plain,
! [A] :
( ( natural(succ(A))
& ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ natural(A)
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f224_nnf]) ).
cnf(c663,plain,
( ~ empty(succ(X0))
| ~ natural(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f224_sk]) ).
fof(f229,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f229_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f229]) ).
fof(f229_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f229_nnf]) ).
cnf(c680,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f229_sk]) ).
fof(f243,axiom,
! [A] :
( ordinal(A)
=> ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_ordinal1) ).
fof(f243_nnf,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f243]) ).
fof(f243_sk,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f243_nnf]) ).
cnf(c717,plain,
( ~ empty(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f243_sk]) ).
fof(f245,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f245_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f245]) ).
fof(f245_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f245_nnf]) ).
cnf(c722,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f245_sk]) ).
fof(f271,axiom,
! [A,B] : ~ proper_subset(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f271_nnf,plain,
! [A,B] : ~ proper_subset(A,A),
inference(nnf_transformation,[status(thm)],[f271]) ).
fof(f271_sk,plain,
! [A] : ~ proper_subset(A,A),
inference(skolemisation,[status(esa)],[f271_nnf]) ).
cnf(c768,plain,
~ proper_subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f271_sk]) ).
fof(f273,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l1_zfmisc_1) ).
fof(f273_nnf,plain,
! [A] : singleton(A) != empty_set,
inference(nnf_transformation,[status(thm)],[f273]) ).
fof(f273_sk,plain,
! [A] : singleton(A) != empty_set,
inference(skolemisation,[status(esa)],[f273_nnf]) ).
cnf(c772,plain,
singleton(X0) != empty_set,
inference(cnf_transformation,[status(esa)],[f273_sk]) ).
fof(f275,lemma,
! [A,B] :
~ ( in(A,B)
& disjoint(singleton(A),B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l25_zfmisc_1) ).
fof(f275_nnf,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(nnf_transformation,[status(thm)],[f275]) ).
fof(f275_sk,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(skolemisation,[status(esa)],[f275_nnf]) ).
cnf(c774,plain,
( ~ in(X0,X1)
| ~ disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f275_sk]) ).
fof(f292,axiom,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_arytm_3) ).
fof(f292_nnf,plain,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f292]) ).
fof(f292_sk,plain,
( natural(sk124)
& ordinal(sk124)
& epsilon_connected(sk124)
& epsilon_transitive(sk124)
& ~ empty(sk124) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk124])],[f292_nnf]) ).
cnf(c813,plain,
~ empty(sk124),
inference(cnf_transformation,[status(esa)],[f292_sk]) ).
fof(f293,axiom,
? [A] :
( finite(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_finset_1) ).
fof(f293_nnf,plain,
? [A] :
( finite(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f293]) ).
fof(f293_sk,plain,
( finite(sk125)
& ~ empty(sk125) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk125])],[f293_nnf]) ).
cnf(c818,plain,
~ empty(sk125),
inference(cnf_transformation,[status(esa)],[f293_sk]) ).
fof(f296,axiom,
? [A] :
( v5_membered(A)
& v4_membered(A)
& v3_membered(A)
& v2_membered(A)
& v1_membered(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_membered) ).
fof(f296_nnf,plain,
? [A] :
( v5_membered(A)
& v4_membered(A)
& v3_membered(A)
& v2_membered(A)
& v1_membered(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f296]) ).
fof(f296_sk,plain,
( v5_membered(sk128)
& v4_membered(sk128)
& v3_membered(sk128)
& v2_membered(sk128)
& v1_membered(sk128)
& ~ empty(sk128) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk128])],[f296_nnf]) ).
cnf(c826,plain,
~ empty(sk128),
inference(cnf_transformation,[status(esa)],[f296_sk]) ).
fof(f308,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f308_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f308]) ).
fof(f308_sk,plain,
( relation(sk140)
& ~ empty(sk140) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk140])],[f308_nnf]) ).
cnf(c873,plain,
~ empty(sk140),
inference(cnf_transformation,[status(esa)],[f308_sk]) ).
fof(f311,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f311_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f311]) ).
fof(f311_sk,plain,
~ empty(sk143),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk143])],[f311_nnf]) ).
cnf(c880,plain,
~ empty(sk143),
inference(cnf_transformation,[status(esa)],[f311_sk]) ).
fof(f314,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_ordinal1) ).
fof(f314_nnf,plain,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f314]) ).
fof(f314_sk,plain,
( ordinal(sk146)
& epsilon_connected(sk146)
& epsilon_transitive(sk146)
& ~ empty(sk146) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk146])],[f314_nnf]) ).
cnf(c887,plain,
~ empty(sk146),
inference(cnf_transformation,[status(esa)],[f314_sk]) ).
fof(f316,axiom,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_struct_0) ).
fof(f316_nnf,plain,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f316]) ).
fof(f316_sk,plain,
( ~ empty_carrier(sk148)
& one_sorted_str(sk148) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk148])],[f316_nnf]) ).
cnf(c894,plain,
~ empty_carrier(sk148),
inference(cnf_transformation,[status(esa)],[f316_sk]) ).
fof(f342,lemma,
( ( ! [D] :
( ordinal(D)
=> ( ( ! [K] :
( ordinal(K)
=> ( in(K,D)
=> ( in(K,omega)
=> ! [L] :
( element(L,powerset(powerset(K)))
=> ~ ( ! [M] :
~ ( ! [N] :
( ( subset(M,N)
& in(N,L) )
=> N = M )
& in(M,L) )
& L != empty_set ) ) ) ) )
& being_limit_ordinal(D) )
=> ( ( in(D,omega)
=> ! [O] :
( element(O,powerset(powerset(D)))
=> ~ ( ! [P] :
~ ( ! [Q] :
( ( subset(P,Q)
& in(Q,O) )
=> Q = P )
& in(P,O) )
& O != empty_set ) ) )
| D = empty_set ) ) )
& ! [D] :
( ordinal(D)
=> ( ( in(D,omega)
=> ! [E] :
( element(E,powerset(powerset(D)))
=> ~ ( ! [F] :
~ ( ! [G] :
( ( subset(F,G)
& in(G,E) )
=> G = F )
& in(F,E) )
& E != empty_set ) ) )
=> ( in(succ(D),omega)
=> ! [H] :
( element(H,powerset(powerset(succ(D))))
=> ~ ( ! [I] :
~ ( ! [J] :
( ( subset(I,J)
& in(J,H) )
=> J = I )
& in(I,H) )
& H != empty_set ) ) ) ) )
& ( in(empty_set,omega)
=> ! [A] :
( element(A,powerset(powerset(empty_set)))
=> ~ ( ! [B] :
~ ( ! [C] :
( ( subset(B,C)
& in(C,A) )
=> C = B )
& in(B,A) )
& A != empty_set ) ) ) )
=> ! [D] :
( ordinal(D)
=> ( in(D,omega)
=> ! [R] :
( element(R,powerset(powerset(D)))
=> ~ ( ! [S] :
~ ( ! [T] :
( ( subset(S,T)
& in(T,R) )
=> T = S )
& in(S,R) )
& R != empty_set ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_ordinal2__e18_27__finset_1) ).
fof(f342_nnf,plain,
( ! [D] :
( ! [R] :
( ? [S] :
( ! [T] :
( T = S
| ~ subset(S,T)
| ~ in(T,R) )
& in(S,R) )
| R = empty_set
| ~ element(R,powerset(powerset(D))) )
| ~ in(D,omega)
| ~ ordinal(D) )
| ? [D] :
( ? [O] :
( ! [P] :
( ? [Q] :
( Q != P
& subset(P,Q)
& in(Q,O) )
| ~ in(P,O) )
& O != empty_set
& element(O,powerset(powerset(D))) )
& in(D,omega)
& D != empty_set
& ! [K] :
( ! [L] :
( ? [M] :
( ! [N] :
( N = M
| ~ subset(M,N)
| ~ in(N,L) )
& in(M,L) )
| L = empty_set
| ~ element(L,powerset(powerset(K))) )
| ~ in(K,omega)
| ~ in(K,D)
| ~ ordinal(K) )
& being_limit_ordinal(D)
& ordinal(D) )
| ? [D] :
( ? [H] :
( ! [I] :
( ? [J] :
( J != I
& subset(I,J)
& in(J,H) )
| ~ in(I,H) )
& H != empty_set
& element(H,powerset(powerset(succ(D)))) )
& in(succ(D),omega)
& ( ! [E] :
( ? [F] :
( ! [G] :
( G = F
| ~ subset(F,G)
| ~ in(G,E) )
& in(F,E) )
| E = empty_set
| ~ element(E,powerset(powerset(D))) )
| ~ in(D,omega) )
& ordinal(D) )
| ( ? [A] :
( ! [B] :
( ? [C] :
( C != B
& subset(B,C)
& in(C,A) )
| ~ in(B,A) )
& A != empty_set
& element(A,powerset(powerset(empty_set))) )
& in(empty_set,omega) ) ),
inference(nnf_transformation,[status(thm)],[f342]) ).
fof(f342_sk,plain,
! [B,E,G,I,K,L,N,P,D,R,T] :
( ( ( T = sk187(D,R)
| ~ subset(sk187(D,R),T)
| ~ in(T,R) )
& in(sk187(D,R),R) )
| R = empty_set
| ~ element(R,powerset(powerset(D)))
| ~ in(D,omega)
| ~ ordinal(D)
| ( ( ( sk186(P) != P
& subset(P,sk186(P))
& in(sk186(P),sk185) )
| ~ in(P,sk185) )
& sk185 != empty_set
& element(sk185,powerset(powerset(sk183)))
& in(sk183,omega)
& sk183 != empty_set
& ( ( ( N = sk184(K,L)
| ~ subset(sk184(K,L),N)
| ~ in(N,L) )
& in(sk184(K,L),L) )
| L = empty_set
| ~ element(L,powerset(powerset(K)))
| ~ in(K,omega)
| ~ in(K,sk183)
| ~ ordinal(K) )
& being_limit_ordinal(sk183)
& ordinal(sk183) )
| ( ( ( sk182(I) != I
& subset(I,sk182(I))
& in(sk182(I),sk181) )
| ~ in(I,sk181) )
& sk181 != empty_set
& element(sk181,powerset(powerset(succ(sk179))))
& in(succ(sk179),omega)
& ( ( ( G = sk180(E)
| ~ subset(sk180(E),G)
| ~ in(G,E) )
& in(sk180(E),E) )
| E = empty_set
| ~ element(E,powerset(powerset(sk179)))
| ~ in(sk179,omega) )
& ordinal(sk179) )
| ( ( ( sk178(B) != B
& subset(B,sk178(B))
& in(sk178(B),sk177) )
| ~ in(B,sk177) )
& sk177 != empty_set
& element(sk177,powerset(powerset(empty_set)))
& in(empty_set,omega) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk177,sk178,sk179,sk180,sk181,sk182,sk183,sk184,sk185,sk186,sk187])],[f342_nnf]) ).
cnf(c1124,plain,
( sk178(X1) != X1
| ~ def1(X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f342_sk]) ).
cnf(c1129,plain,
( sk177 != empty_set
| ~ def3(X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f342_sk]) ).
cnf(c1138,plain,
( ~ subset(sk180(X4),X6)
| ~ in(X6,X4)
| ~ def6(X6,X4) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f342_sk]) ).
cnf(c1160,plain,
( sk182(X8) != X8
| ~ def13(X8) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f342_sk]) ).
cnf(c1165,plain,
( sk181 != empty_set
| ~ def15(X8) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f342_sk]) ).
cnf(c1183,plain,
( ~ subset(sk184(X10,X11),X13)
| ~ in(X13,X11)
| ~ def21(X13,X11,X10) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f342_sk]) ).
cnf(c1214,plain,
( sk186(X15) != X15
| ~ def31(X15) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f342_sk]) ).
cnf(c1219,plain,
( sk185 != empty_set
| ~ def33(X15) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f342_sk]) ).
cnf(c1228,plain,
( sk183 != empty_set
| ~ def36(X15) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f342_sk]) ).
cnf(c1240,plain,
( ~ subset(sk187(X3,X17),X19)
| ~ in(X19,X17)
| ~ def40(X19,X17,X3) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f342_sk]) ).
fof(f489,lemma,
! [A,B,C] :
~ ( in(C,A)
& in(B,C)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_ordinal1) ).
fof(f489_nnf,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f489]) ).
fof(f489_sk,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f489_nnf]) ).
cnf(c2697,plain,
( ~ in(X2,X0)
| ~ in(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f489_sk]) ).
fof(f492,lemma,
! [A,B] :
( ~ ( disjoint(A,B)
& ? [C] :
( in(C,B)
& in(C,A) ) )
& ~ ( ! [C] :
~ ( in(C,B)
& in(C,A) )
& ~ disjoint(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_xboole_0) ).
fof(f492_nnf,plain,
! [A,B] :
( ( ~ disjoint(A,B)
| ! [C] :
( ~ in(C,B)
| ~ in(C,A) ) )
& ( ? [C] :
( in(C,B)
& in(C,A) )
| disjoint(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f492]) ).
fof(f492_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,B)
| ~ in(C,A) )
& ( ( in(sk412(A,B),B)
& in(sk412(A,B),A) )
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk412])],[f492_nnf]) ).
cnf(c2703,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f492_sk]) ).
fof(f496,lemma,
! [A] :
( ordinal(A)
=> ( ~ ( being_limit_ordinal(A)
& ? [B] :
( A = succ(B)
& ordinal(B) ) )
& ~ ( ! [B] :
( ordinal(B)
=> A != succ(B) )
& ~ being_limit_ordinal(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t42_ordinal1) ).
fof(f496_nnf,plain,
! [A] :
( ( ( ~ being_limit_ordinal(A)
| ! [B] :
( A != succ(B)
| ~ ordinal(B) ) )
& ( ? [B] :
( A = succ(B)
& ordinal(B) )
| being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f496]) ).
fof(f496_sk,plain,
! [A,B] :
( ( ( ~ being_limit_ordinal(A)
| A != succ(B)
| ~ ordinal(B) )
& ( ( A = succ(sk414(A))
& ordinal(sk414(A)) )
| being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk414])],[f496_nnf]) ).
cnf(c2712,plain,
( ~ being_limit_ordinal(X0)
| X0 != succ(X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f496_sk]) ).
fof(f518,lemma,
! [A,B] :
( ~ ( disjoint(A,B)
& ? [C] : in(C,set_intersection2(A,B)) )
& ~ ( ! [C] : ~ in(C,set_intersection2(A,B))
& ~ disjoint(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_xboole_0) ).
fof(f518_nnf,plain,
! [A,B] :
( ( ~ disjoint(A,B)
| ! [C] : ~ in(C,set_intersection2(A,B)) )
& ( ? [C] : in(C,set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f518]) ).
fof(f518_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk418(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk418])],[f518_nnf]) ).
cnf(c2748,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f518_sk]) ).
fof(f524,lemma,
! [A,B,C] :
( element(C,powerset(A))
=> ~ ( in(B,C)
& in(B,subset_complement(A,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t54_subset_1) ).
fof(f524_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f524]) ).
fof(f524_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f524_nnf]) ).
cnf(c2772,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f524_sk]) ).
fof(f531,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(f531_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f531]) ).
fof(f531_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f531_nnf]) ).
cnf(c2789,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f531_sk]) ).
fof(f536,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f536_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f536]) ).
fof(f536_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f536_nnf]) ).
cnf(c2796,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f536_sk]) ).
fof(f541,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f541_nnf,plain,
! [A,B] :
( ( in(B,A)
| set_difference(A,singleton(B)) = A )
& ( ~ in(B,A)
| set_difference(A,singleton(B)) != A ) ),
inference(nnf_transformation,[status(thm)],[f541]) ).
fof(f541_sk,plain,
! [A,B] :
( ( in(B,A)
| set_difference(A,singleton(B)) = A )
& ( ~ in(B,A)
| set_difference(A,singleton(B)) != A ) ),
inference(skolemisation,[status(esa)],[f541_nnf]) ).
cnf(c2803,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f541_sk]) ).
fof(f552,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f552_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f552]) ).
fof(f552_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f552_nnf]) ).
cnf(c2821,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f552_sk]) ).
fof(f554,axiom,
! [A,B] :
~ ( ! [C] :
~ ( ! [D] :
~ ( in(D,C)
& in(D,B) )
& in(C,B) )
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_tarski) ).
fof(f554_nnf,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f554]) ).
fof(f554_sk,plain,
! [A,B,D] :
( ( ( ~ in(D,sk427(A,B))
| ~ in(D,B) )
& in(sk427(A,B),B) )
| ~ in(A,B) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk427])],[f554_nnf]) ).
cnf(c2825,plain,
( ~ in(X3,sk427(X0,X1))
| ~ in(X3,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f554_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c1,c129,c251,c269,c277,c419,c534,c635,c637,c643,c647,c656,c658,c663,c680,c717,c722,c768,c772,c774,c813,c818,c826,c873,c880,c887,c894,c1124,c1129,c1138,c1160,c1165,c1183,c1214,c1219,c1228,c1240,c2697,c2703,c2712,c2748,c2772,c2781,c2788,c2789,c2796,c2803,c2821,c2825]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t20432]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU341+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.40 % Computer : n008.cluster.edu
% 0.09/0.40 % Model : x86_64 x86_64
% 0.09/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.40 % Memory : 8046.5625MB
% 0.09/0.40 % OS : Linux 6.8.0-71-generic
% 0.09/0.40 % CPULimit : 300
% 0.09/0.40 % WCLimit : 300
% 0.09/0.40 % DateTime : Thu Sep 24 13:46:39 UTC 2026
% 0.09/0.40 % CPUTime :
% 0.09/0.40 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 75.06/10.01 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 75.06/10.01 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------