%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU308+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n005.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:41 PM UTC 2026
% Result : Theorem 198.96s 31.29s
% Output : Proof 198.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 45
% Syntax : Number of formulae : 228 ( 92 unt; 0 def)
% Number of atoms : 714 ( 157 equ)
% Maximal formula atoms : 49 ( 3 avg)
% Number of connectives : 863 ( 377 ~; 203 |; 234 &)
% ( 8 <=>; 41 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 1 prp; 0-3 aty)
% Number of functors : 45 ( 45 usr; 18 con; 0-4 aty)
% Number of variables : 401 ( 25 sgn 251 !; 37 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f360,conjecture,
! [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(f360_neg,negated_conjecture,
~ ! [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) ) ),
inference(negated_conjecture,[status(cth)],[f360]) ).
fof(f360_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)],[f360_neg]) ).
fof(f360_sk,plain,
( subset_complement(the_carrier(sk295),sk296) != subset_difference(the_carrier(sk295),cast_as_carrier_subset(sk295),sk296)
& element(sk296,powerset(the_carrier(sk295)))
& one_sorted_str(sk295) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk295,sk296])],[f360_nnf]) ).
cnf(c1924,plain,
subset_complement(the_carrier(sk295),sk296) != subset_difference(the_carrier(sk295),cast_as_carrier_subset(sk295),sk296),
inference(cnf_transformation,[status(esa)],[f360_sk]) ).
cnf(t130,plain,
eq(subset_complement(the_carrier(sk295),sk296),subset_difference(the_carrier(sk295),cast_as_carrier_subset(sk295),sk296)) = false,
inference(equality_encoding,[status(esa)],[c1924]) ).
cnf(t828,plain,
eq(subset_complement(the_carrier(sk295),sk296),subset_difference(the_carrier(sk295),cast_as_carrier_subset(sk295),sk296)) = false,
inference(orient,[status(thm)],[t130]) ).
fof(f76,axiom,
! [A] :
( one_sorted_str(A)
=> cast_as_carrier_subset(A) = the_carrier(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f76_nnf,plain,
! [A] :
( cast_as_carrier_subset(A) = the_carrier(A)
| ~ one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f76]) ).
fof(f76_sk,plain,
! [A] :
( cast_as_carrier_subset(A) = the_carrier(A)
| ~ one_sorted_str(A) ),
inference(skolemisation,[status(esa)],[f76_nnf]) ).
cnf(c294,plain,
( cast_as_carrier_subset(X0) = the_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(esa)],[f76_sk]) ).
cnf(t111,plain,
ifeq(one_sorted_str(X1),true,cast_as_carrier_subset(X1),the_carrier(X1)) = the_carrier(X1),
inference(equality_encoding,[status(esa)],[c294]) ).
cnf(t667,plain,
ifeq(one_sorted_str(X1),true,cast_as_carrier_subset(X1),the_carrier(X1)) = the_carrier(X1),
inference(orient,[status(thm)],[t111]) ).
cnf(c1922,plain,
one_sorted_str(sk295),
inference(cnf_transformation,[status(esa)],[f360_sk]) ).
cnf(t15,plain,
one_sorted_str(sk295) = true,
inference(equality_encoding,[status(esa)],[c1922]) ).
cnf(t612,plain,
one_sorted_str(sk295) = true,
inference(orient,[status(thm)],[t15]) ).
cnf(t668,plain,
the_carrier(sk295) = ifeq(true,true,cast_as_carrier_subset(sk295),the_carrier(sk295)),
inference(cp,[status(thm)],[t667,t612]) ).
cnf(t78,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t177,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t78]) ).
cnf(t325667,plain,
the_carrier(sk295) = cast_as_carrier_subset(sk295),
inference(step,[status(thm)],[t668,t177]) ).
cnf(t858,plain,
cast_as_carrier_subset(sk295) = the_carrier(sk295),
inference(orient,[status(thm)],[t325667]) ).
cnf(t325668,plain,
eq(subset_complement(the_carrier(sk295),sk296),subset_difference(the_carrier(sk295),the_carrier(sk295),sk296)) = false,
inference(step,[status(thm)],[t828,t858]) ).
cnf(t861,plain,
eq(subset_complement(the_carrier(sk295),sk296),subset_difference(the_carrier(sk295),the_carrier(sk295),sk296)) = false,
inference(rw,[status(thm)],[t325668]) ).
fof(f290,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(f290_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)],[f290]) ).
fof(f290_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)],[f290_nnf]) ).
cnf(c804,plain,
( subset_difference(X0,X1,X2) = set_difference(X1,X2)
| ~ element(X2,powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f290_sk]) ).
cnf(t172,plain,
ifeq(element(X1,powerset(X2)),true,ifeq(element(X3,powerset(X2)),true,subset_difference(X2,X1,X3),set_difference(X1,X3)),set_difference(X1,X3)) = set_difference(X1,X3),
inference(equality_encoding,[status(esa)],[c804]) ).
cnf(t654,plain,
ifeq(element(X1,powerset(X2)),true,ifeq(element(X3,powerset(X2)),true,subset_difference(X2,X1,X3),set_difference(X1,X3)),set_difference(X1,X3)) = set_difference(X1,X3),
inference(orient,[status(thm)],[t172]) ).
cnf(c1923,plain,
element(sk296,powerset(the_carrier(sk295))),
inference(cnf_transformation,[status(esa)],[f360_sk]) ).
cnf(t77,plain,
element(sk296,powerset(the_carrier(sk295))) = true,
inference(equality_encoding,[status(esa)],[c1923]) ).
cnf(t501,plain,
element(sk296,powerset(the_carrier(sk295))) = true,
inference(orient,[status(thm)],[t77]) ).
cnf(t656,plain,
set_difference(X1,sk296) = ifeq(element(X1,powerset(the_carrier(sk295))),true,ifeq(true,true,subset_difference(the_carrier(sk295),X1,sk296),set_difference(X1,sk296)),set_difference(X1,sk296)),
inference(cp,[status(thm)],[t654,t501]) ).
cnf(t326752,plain,
set_difference(X1,sk296) = ifeq(element(X1,powerset(the_carrier(sk295))),true,subset_difference(the_carrier(sk295),X1,sk296),set_difference(X1,sk296)),
inference(step,[status(thm)],[t656,t177]) ).
cnf(t134788,plain,
ifeq(element(X1,powerset(the_carrier(sk295))),true,subset_difference(the_carrier(sk295),X1,sk296),set_difference(X1,sk296)) = set_difference(X1,sk296),
inference(orient,[status(thm)],[t326752]) ).
fof(f422,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f422_nnf,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(nnf_transformation,[status(thm)],[f422]) ).
fof(f422_sk,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(skolemisation,[status(esa)],[f422_nnf]) ).
cnf(c2026,plain,
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(esa)],[f422_sk]) ).
cnf(t124,plain,
ifeq(subset(X1,X2),true,element(X1,powerset(X2)),true) = true,
inference(equality_encoding,[status(esa)],[c2026]) ).
cnf(t251,plain,
ifeq(subset(X1,X2),true,element(X1,powerset(X2)),true) = true,
inference(orient,[status(thm)],[t124]) ).
fof(f295,axiom,
! [A,B] : subset(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f295_nnf,plain,
! [A,B] : subset(A,A),
inference(nnf_transformation,[status(thm)],[f295]) ).
fof(f295_sk,plain,
! [A] : subset(A,A),
inference(skolemisation,[status(esa)],[f295_nnf]) ).
cnf(c812,plain,
subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f295_sk]) ).
cnf(t61,plain,
subset(X1,X1) = true,
inference(equality_encoding,[status(esa)],[c812]) ).
cnf(t292,plain,
subset(X1,X1) = true,
inference(orient,[status(thm)],[t61]) ).
cnf(t296,plain,
true = ifeq(true,true,element(X1,powerset(X1)),true),
inference(cp,[status(thm)],[t251,t292]) ).
cnf(t325692,plain,
true = element(X1,powerset(X1)),
inference(step,[status(thm)],[t296,t177]) ).
cnf(t983,plain,
element(X1,powerset(X1)) = true,
inference(orient,[status(thm)],[t325692]) ).
cnf(t134789,plain,
set_difference(the_carrier(sk295),sk296) = ifeq(true,true,subset_difference(the_carrier(sk295),the_carrier(sk295),sk296),set_difference(the_carrier(sk295),sk296)),
inference(cp,[status(thm)],[t134788,t983]) ).
fof(f93,axiom,
! [A,B] :
( element(B,powerset(A))
=> subset_complement(A,B) = set_difference(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_subset_1) ).
fof(f93_nnf,plain,
! [A,B] :
( subset_complement(A,B) = set_difference(A,B)
| ~ element(B,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f93]) ).
fof(f93_sk,plain,
! [B,A] :
( subset_complement(A,B) = set_difference(A,B)
| ~ element(B,powerset(A)) ),
inference(skolemisation,[status(esa)],[f93_nnf]) ).
cnf(c388,plain,
( subset_complement(X0,X1) = set_difference(X0,X1)
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f93_sk]) ).
cnf(t147,plain,
ifeq(element(X1,powerset(X2)),true,subset_complement(X2,X1),set_difference(X2,X1)) = set_difference(X2,X1),
inference(equality_encoding,[status(esa)],[c388]) ).
cnf(t661,plain,
ifeq(element(X1,powerset(X2)),true,subset_complement(X2,X1),set_difference(X2,X1)) = set_difference(X2,X1),
inference(orient,[status(thm)],[t147]) ).
cnf(t662,plain,
set_difference(the_carrier(sk295),sk296) = ifeq(true,true,subset_complement(the_carrier(sk295),sk296),set_difference(the_carrier(sk295),sk296)),
inference(cp,[status(thm)],[t661,t501]) ).
cnf(t325706,plain,
set_difference(the_carrier(sk295),sk296) = subset_complement(the_carrier(sk295),sk296),
inference(step,[status(thm)],[t662,t177]) ).
cnf(t1161,plain,
set_difference(the_carrier(sk295),sk296) = subset_complement(the_carrier(sk295),sk296),
inference(orient,[status(thm)],[t325706]) ).
cnf(t326761,plain,
subset_complement(the_carrier(sk295),sk296) = ifeq(true,true,subset_difference(the_carrier(sk295),the_carrier(sk295),sk296),set_difference(the_carrier(sk295),sk296)),
inference(step,[status(thm)],[t134789,t1161]) ).
cnf(t326762,plain,
subset_complement(the_carrier(sk295),sk296) = subset_difference(the_carrier(sk295),the_carrier(sk295),sk296),
inference(step,[status(thm)],[t326761,t177]) ).
cnf(t134939,plain,
subset_difference(the_carrier(sk295),the_carrier(sk295),sk296) = subset_complement(the_carrier(sk295),sk296),
inference(orient,[status(thm)],[t326762]) ).
cnf(t327350,plain,
eq(subset_complement(the_carrier(sk295),sk296),subset_complement(the_carrier(sk295),sk296)) = false,
inference(step,[status(thm)],[t861,t134939]) ).
cnf(t49,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t531,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t49]) ).
cnf(t327351,plain,
true = false,
inference(step,[status(thm)],[t327350,t531]) ).
cnf(t325581,plain,
false = true,
inference(orient,[status(thm)],[t327351]) ).
fof(f0,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/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/sandbox2/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(f61,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/sandbox2/benchmark/theBenchmark.p',d1_wellord1) ).
fof(f61_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)],[f61]) ).
fof(f61_sk,plain,
! [A,C,B,D] :
( ( ( ( in(ordered_pair(sk31(A,B,C),B),A)
& sk31(A,B,C) != B
& ~ in(sk31(A,B,C),C) )
| ( ( ~ in(ordered_pair(sk31(A,B,C),B),A)
| sk31(A,B,C) = B )
& in(sk31(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,[sk31])],[f61_nnf]) ).
cnf(c208,plain,
( X3 != X1
| ~ in(X3,X2)
| X2 != fiber(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f61_sk]) ).
fof(f63,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f63_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f63]) ).
fof(f63_sk,plain,
! [A,B] :
( ( in(sk34(A),A)
| A = empty_set )
& ( ~ in(B,A)
| A != empty_set ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk34])],[f63_nnf]) ).
cnf(c226,plain,
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(esa)],[f63_sk]) ).
fof(f89,axiom,
! [A,B,C] :
( C = set_difference(A,B)
<=> ! [D] :
( in(D,C)
<=> ( ~ in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f89_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)],[f89]) ).
fof(f89_sk,plain,
! [C,A,B,D] :
( ( ( ~ in(sk67(A,B,C),B)
& in(sk67(A,B,C),A)
& ~ in(sk67(A,B,C),C) )
| ( ( in(sk67(A,B,C),B)
| ~ in(sk67(A,B,C),A) )
& in(sk67(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,[sk67])],[f89_nnf]) ).
cnf(c357,plain,
( ~ in(X3,X1)
| ~ in(X3,X2)
| X2 != set_difference(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f89_sk]) ).
fof(f108,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f108_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)],[f108]) ).
fof(f108_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)],[f108_nnf]) ).
cnf(c462,plain,
( X0 != X1
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f108_sk]) ).
fof(f183,axiom,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_finset_1) ).
fof(f183_nnf,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(nnf_transformation,[status(thm)],[f183]) ).
fof(f183_sk,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(skolemisation,[status(esa)],[f183_nnf]) ).
cnf(c550,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f183_sk]) ).
fof(f184,axiom,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_finsub_1) ).
fof(f184_nnf,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f184]) ).
fof(f184_sk,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(skolemisation,[status(esa)],[f184_nnf]) ).
cnf(c552,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f184_sk]) ).
fof(f186,axiom,
! [A] : ~ empty(succ(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_ordinal1) ).
fof(f186_nnf,plain,
! [A] : ~ empty(succ(A)),
inference(nnf_transformation,[status(thm)],[f186]) ).
fof(f186_sk,plain,
! [A] : ~ empty(succ(A)),
inference(skolemisation,[status(esa)],[f186_nnf]) ).
cnf(c558,plain,
~ empty(succ(X0)),
inference(cnf_transformation,[status(esa)],[f186_sk]) ).
fof(f187,axiom,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_ordinal2) ).
fof(f187_nnf,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(nnf_transformation,[status(thm)],[f187]) ).
fof(f187_sk,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(skolemisation,[status(esa)],[f187_nnf]) ).
cnf(c562,plain,
~ empty(omega),
inference(cnf_transformation,[status(esa)],[f187_sk]) ).
fof(f190,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f190_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f190]) ).
fof(f190_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f190_nnf]) ).
cnf(c565,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f190_sk]) ).
fof(f192,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f192_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f192]) ).
fof(f192_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f192_nnf]) ).
cnf(c567,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f192_sk]) ).
fof(f196,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/sandbox2/benchmark/theBenchmark.p',fc2_arytm_3) ).
fof(f196_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)],[f196]) ).
fof(f196_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)],[f196_nnf]) ).
cnf(c572,plain,
( ~ empty(succ(X0))
| ~ natural(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f196_sk]) ).
fof(f200,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f200_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f200]) ).
fof(f200_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f200_nnf]) ).
cnf(c588,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f200_sk]) ).
fof(f213,axiom,
! [A] :
( ordinal(A)
=> ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_ordinal1) ).
fof(f213_nnf,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f213]) ).
fof(f213_sk,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f213_nnf]) ).
cnf(c624,plain,
( ~ empty(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f213_sk]) ).
fof(f215,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f215_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f215]) ).
fof(f215_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f215_nnf]) ).
cnf(c629,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f215_sk]) ).
fof(f237,axiom,
! [A,B] : ~ proper_subset(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f237_nnf,plain,
! [A,B] : ~ proper_subset(A,A),
inference(nnf_transformation,[status(thm)],[f237]) ).
fof(f237_sk,plain,
! [A] : ~ proper_subset(A,A),
inference(skolemisation,[status(esa)],[f237_nnf]) ).
cnf(c671,plain,
~ proper_subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f237_sk]) ).
fof(f239,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_zfmisc_1) ).
fof(f239_nnf,plain,
! [A] : singleton(A) != empty_set,
inference(nnf_transformation,[status(thm)],[f239]) ).
fof(f239_sk,plain,
! [A] : singleton(A) != empty_set,
inference(skolemisation,[status(esa)],[f239_nnf]) ).
cnf(c675,plain,
singleton(X0) != empty_set,
inference(cnf_transformation,[status(esa)],[f239_sk]) ).
fof(f241,lemma,
! [A,B] :
~ ( in(A,B)
& disjoint(singleton(A),B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l25_zfmisc_1) ).
fof(f241_nnf,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(nnf_transformation,[status(thm)],[f241]) ).
fof(f241_sk,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(skolemisation,[status(esa)],[f241_nnf]) ).
cnf(c677,plain,
( ~ in(X0,X1)
| ~ disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f241_sk]) ).
fof(f257,axiom,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_arytm_3) ).
fof(f257_nnf,plain,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f257]) ).
fof(f257_sk,plain,
( natural(sk110)
& ordinal(sk110)
& epsilon_connected(sk110)
& epsilon_transitive(sk110)
& ~ empty(sk110) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk110])],[f257_nnf]) ).
cnf(c714,plain,
~ empty(sk110),
inference(cnf_transformation,[status(esa)],[f257_sk]) ).
fof(f258,axiom,
? [A] :
( finite(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_finset_1) ).
fof(f258_nnf,plain,
? [A] :
( finite(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f258]) ).
fof(f258_sk,plain,
( finite(sk111)
& ~ empty(sk111) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk111])],[f258_nnf]) ).
cnf(c719,plain,
~ empty(sk111),
inference(cnf_transformation,[status(esa)],[f258_sk]) ).
fof(f261,axiom,
? [A] :
( v5_membered(A)
& v4_membered(A)
& v3_membered(A)
& v2_membered(A)
& v1_membered(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_membered) ).
fof(f261_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)],[f261]) ).
fof(f261_sk,plain,
( v5_membered(sk114)
& v4_membered(sk114)
& v3_membered(sk114)
& v2_membered(sk114)
& v1_membered(sk114)
& ~ empty(sk114) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk114])],[f261_nnf]) ).
cnf(c727,plain,
~ empty(sk114),
inference(cnf_transformation,[status(esa)],[f261_sk]) ).
fof(f272,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f272_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f272]) ).
fof(f272_sk,plain,
( relation(sk125)
& ~ empty(sk125) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk125])],[f272_nnf]) ).
cnf(c772,plain,
~ empty(sk125),
inference(cnf_transformation,[status(esa)],[f272_sk]) ).
fof(f274,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f274_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f274]) ).
fof(f274_sk,plain,
~ empty(sk127),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk127])],[f274_nnf]) ).
cnf(c776,plain,
~ empty(sk127),
inference(cnf_transformation,[status(esa)],[f274_sk]) ).
fof(f277,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_ordinal1) ).
fof(f277_nnf,plain,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f277]) ).
fof(f277_sk,plain,
( ordinal(sk130)
& epsilon_connected(sk130)
& epsilon_transitive(sk130)
& ~ empty(sk130) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk130])],[f277_nnf]) ).
cnf(c783,plain,
~ empty(sk130),
inference(cnf_transformation,[status(esa)],[f277_sk]) ).
fof(f279,axiom,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_struct_0) ).
fof(f279_nnf,plain,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f279]) ).
fof(f279_sk,plain,
( ~ empty_carrier(sk132)
& one_sorted_str(sk132) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk132])],[f279_nnf]) ).
cnf(c790,plain,
~ empty_carrier(sk132),
inference(cnf_transformation,[status(esa)],[f279_sk]) ).
fof(f300,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/sandbox2/benchmark/theBenchmark.p',s1_ordinal2__e18_27__finset_1) ).
fof(f300_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)],[f300]) ).
fof(f300_sk,plain,
! [B,E,G,I,K,L,N,P,D,R,T] :
( ( ( T = sk158(D,R)
| ~ subset(sk158(D,R),T)
| ~ in(T,R) )
& in(sk158(D,R),R) )
| R = empty_set
| ~ element(R,powerset(powerset(D)))
| ~ in(D,omega)
| ~ ordinal(D)
| ( ( ( sk157(P) != P
& subset(P,sk157(P))
& in(sk157(P),sk156) )
| ~ in(P,sk156) )
& sk156 != empty_set
& element(sk156,powerset(powerset(sk154)))
& in(sk154,omega)
& sk154 != empty_set
& ( ( ( N = sk155(K,L)
| ~ subset(sk155(K,L),N)
| ~ in(N,L) )
& in(sk155(K,L),L) )
| L = empty_set
| ~ element(L,powerset(powerset(K)))
| ~ in(K,omega)
| ~ in(K,sk154)
| ~ ordinal(K) )
& being_limit_ordinal(sk154)
& ordinal(sk154) )
| ( ( ( sk153(I) != I
& subset(I,sk153(I))
& in(sk153(I),sk152) )
| ~ in(I,sk152) )
& sk152 != empty_set
& element(sk152,powerset(powerset(succ(sk150))))
& in(succ(sk150),omega)
& ( ( ( G = sk151(E)
| ~ subset(sk151(E),G)
| ~ in(G,E) )
& in(sk151(E),E) )
| E = empty_set
| ~ element(E,powerset(powerset(sk150)))
| ~ in(sk150,omega) )
& ordinal(sk150) )
| ( ( ( sk149(B) != B
& subset(B,sk149(B))
& in(sk149(B),sk148) )
| ~ in(B,sk148) )
& sk148 != empty_set
& element(sk148,powerset(powerset(empty_set)))
& in(empty_set,omega) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk148,sk149,sk150,sk151,sk152,sk153,sk154,sk155,sk156,sk157,sk158])],[f300_nnf]) ).
cnf(c932,plain,
( sk149(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])],[f300_sk]) ).
cnf(c937,plain,
( sk148 != 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])],[f300_sk]) ).
cnf(c946,plain,
( ~ subset(sk151(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])],[f300_sk]) ).
cnf(c968,plain,
( sk153(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])],[f300_sk]) ).
cnf(c973,plain,
( sk152 != 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])],[f300_sk]) ).
cnf(c991,plain,
( ~ subset(sk155(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])],[f300_sk]) ).
cnf(c1022,plain,
( sk157(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])],[f300_sk]) ).
cnf(c1027,plain,
( sk156 != 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])],[f300_sk]) ).
cnf(c1036,plain,
( sk154 != 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])],[f300_sk]) ).
cnf(c1048,plain,
( ~ subset(sk158(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])],[f300_sk]) ).
fof(f421,lemma,
! [A,B,C] :
~ ( in(C,A)
& in(B,C)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_ordinal1) ).
fof(f421_nnf,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f421]) ).
fof(f421_sk,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f421_nnf]) ).
cnf(c2024,plain,
( ~ in(X2,X0)
| ~ in(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f421_sk]) ).
fof(f424,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/sandbox2/benchmark/theBenchmark.p',t3_xboole_0) ).
fof(f424_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)],[f424]) ).
fof(f424_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,B)
| ~ in(C,A) )
& ( ( in(sk309(A,B),B)
& in(sk309(A,B),A) )
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk309])],[f424_nnf]) ).
cnf(c2030,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f424_sk]) ).
fof(f428,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/sandbox2/benchmark/theBenchmark.p',t42_ordinal1) ).
fof(f428_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)],[f428]) ).
fof(f428_sk,plain,
! [A,B] :
( ( ( ~ being_limit_ordinal(A)
| A != succ(B)
| ~ ordinal(B) )
& ( ( A = succ(sk311(A))
& ordinal(sk311(A)) )
| being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk311])],[f428_nnf]) ).
cnf(c2039,plain,
( ~ being_limit_ordinal(X0)
| X0 != succ(X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f428_sk]) ).
fof(f445,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/sandbox2/benchmark/theBenchmark.p',t4_xboole_0) ).
fof(f445_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)],[f445]) ).
fof(f445_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk312(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk312])],[f445_nnf]) ).
cnf(c2060,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f445_sk]) ).
fof(f449,lemma,
! [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(f449_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f449]) ).
fof(f449_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f449_nnf]) ).
cnf(c2081,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f449_sk]) ).
fof(f454,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f454_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f454]) ).
fof(f454_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f454_nnf]) ).
cnf(c2088,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f454_sk]) ).
fof(f458,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f458_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f458]) ).
fof(f458_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f458_nnf]) ).
cnf(c2094,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f458_sk]) ).
fof(f463,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f463_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)],[f463]) ).
fof(f463_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)],[f463_nnf]) ).
cnf(c2101,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f463_sk]) ).
fof(f474,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f474_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f474]) ).
fof(f474_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f474_nnf]) ).
cnf(c2119,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f474_sk]) ).
fof(f476,axiom,
! [A,B] :
~ ( ! [C] :
~ ( ! [D] :
~ ( in(D,C)
& in(D,B) )
& in(C,B) )
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_tarski) ).
fof(f476_nnf,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f476]) ).
fof(f476_sk,plain,
! [A,B,D] :
( ( ( ~ in(D,sk318(A,B))
| ~ in(D,B) )
& in(sk318(A,B),B) )
| ~ in(A,B) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk318])],[f476_nnf]) ).
cnf(c2123,plain,
( ~ in(X3,sk318(X0,X1))
| ~ in(X3,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f476_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c1,c208,c226,c357,c462,c550,c552,c558,c562,c565,c567,c572,c588,c624,c629,c671,c675,c677,c714,c719,c727,c772,c776,c783,c790,c932,c937,c946,c968,c973,c991,c1022,c1027,c1036,c1048,c1924,c2024,c2030,c2039,c2060,c2081,c2088,c2094,c2101,c2119,c2123]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t325581]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU308+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/5.37 % Computer : n005.cluster.edu
% 0.12/5.37 % Model : x86_64 x86_64
% 0.12/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.37 % Memory : 8046.5625MB
% 0.12/5.37 % OS : Linux 6.8.0-71-generic
% 0.12/5.37 % CPULimit : 300
% 0.12/5.37 % WCLimit : 300
% 0.12/5.37 % DateTime : Thu Sep 24 13:38:37 UTC 2026
% 0.12/5.37 % CPUTime :
% 0.12/5.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 198.96/31.29 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 198.96/31.29 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------