%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU325+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 : n017.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:44 PM UTC 2026
% Result : Theorem 79.47s 10.64s
% Output : Proof 79.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 50
% Syntax : Number of formulae : 298 ( 142 unt; 0 def)
% Number of atoms : 893 ( 216 equ)
% Maximal formula atoms : 49 ( 2 avg)
% Number of connectives : 1037 ( 442 ~; 260 |; 274 &)
% ( 11 <=>; 50 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 39 ( 37 usr; 1 prp; 0-3 aty)
% Number of functors : 50 ( 50 usr; 18 con; 0-4 aty)
% Number of variables : 473 ( 41 sgn 280 !; 40 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f214,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ~ empty(cast_as_carrier_subset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_pre_topc) ).
fof(f214_nnf,plain,
! [A] :
( ~ empty(cast_as_carrier_subset(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f214]) ).
fof(f214_sk,plain,
! [A] :
( ~ empty(cast_as_carrier_subset(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(skolemisation,[status(esa)],[f214_nnf]) ).
cnf(c643,plain,
( ~ empty(cast_as_carrier_subset(X0))
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f214_sk]) ).
cnf(t186,plain,
ifeq(one_sorted_str(X1),true,ifeq(empty(cast_as_carrier_subset(X1)),true,empty_carrier(X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c643]) ).
cnf(t486,plain,
ifeq(one_sorted_str(X1),true,ifeq(empty(cast_as_carrier_subset(X1)),true,empty_carrier(X1),true),true) = true,
inference(orient,[status(thm)],[t186]) ).
fof(f497,conjecture,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,powerset(powerset(the_carrier(A))))
=> ~ ( B = empty_set
& is_a_cover_of_carrier(A,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_tops_2) ).
fof(f497_neg,negated_conjecture,
~ ! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,powerset(powerset(the_carrier(A))))
=> ~ ( B = empty_set
& is_a_cover_of_carrier(A,B) ) ) ),
inference(negated_conjecture,[status(cth)],[f497]) ).
fof(f497_nnf,plain,
? [A] :
( ? [B] :
( B = empty_set
& is_a_cover_of_carrier(A,B)
& element(B,powerset(powerset(the_carrier(A)))) )
& one_sorted_str(A)
& ~ empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f497_neg]) ).
fof(f497_sk,plain,
( sk348 = empty_set
& is_a_cover_of_carrier(sk347,sk348)
& element(sk348,powerset(powerset(the_carrier(sk347))))
& one_sorted_str(sk347)
& ~ empty_carrier(sk347) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk347,sk348])],[f497_nnf]) ).
cnf(c2298,plain,
~ empty_carrier(sk347),
inference(cnf_transformation,[status(esa)],[f497_sk]) ).
cnf(t7,plain,
empty_carrier(sk347) = false,
inference(equality_encoding,[status(esa)],[c2298]) ).
cnf(t1535,plain,
empty_carrier(sk347) = false,
inference(orient,[status(thm)],[t7]) ).
cnf(t1537,plain,
true = ifeq(one_sorted_str(sk347),true,ifeq(empty(cast_as_carrier_subset(sk347)),true,false,true),true),
inference(cp,[status(thm)],[t486,t1535]) ).
cnf(c2299,plain,
one_sorted_str(sk347),
inference(cnf_transformation,[status(esa)],[f497_sk]) ).
cnf(t12,plain,
one_sorted_str(sk347) = true,
inference(equality_encoding,[status(esa)],[c2299]) ).
cnf(t1206,plain,
one_sorted_str(sk347) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t4560,plain,
true = ifeq(true,true,ifeq(empty(cast_as_carrier_subset(sk347)),true,false,true),true),
inference(step,[status(thm)],[t1537,t1206]) ).
cnf(t57,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t244,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t57]) ).
cnf(t4561,plain,
true = ifeq(empty(cast_as_carrier_subset(sk347)),true,false,true),
inference(step,[status(thm)],[t4560,t244]) ).
fof(f81,axiom,
! [A] :
( one_sorted_str(A)
=> cast_as_carrier_subset(A) = the_carrier(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f81_nnf,plain,
! [A] :
( cast_as_carrier_subset(A) = the_carrier(A)
| ~ one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f81]) ).
fof(f81_sk,plain,
! [A] :
( cast_as_carrier_subset(A) = the_carrier(A)
| ~ one_sorted_str(A) ),
inference(skolemisation,[status(esa)],[f81_nnf]) ).
cnf(c332,plain,
( cast_as_carrier_subset(X0) = the_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(esa)],[f81_sk]) ).
cnf(t128,plain,
ifeq(one_sorted_str(X1),true,cast_as_carrier_subset(X1),the_carrier(X1)) = the_carrier(X1),
inference(equality_encoding,[status(esa)],[c332]) ).
cnf(t1267,plain,
ifeq(one_sorted_str(X1),true,cast_as_carrier_subset(X1),the_carrier(X1)) = the_carrier(X1),
inference(orient,[status(thm)],[t128]) ).
cnf(t1268,plain,
the_carrier(sk347) = ifeq(true,true,cast_as_carrier_subset(sk347),the_carrier(sk347)),
inference(cp,[status(thm)],[t1267,t1206]) ).
cnf(t4393,plain,
the_carrier(sk347) = cast_as_carrier_subset(sk347),
inference(step,[status(thm)],[t1268,t244]) ).
cnf(t1637,plain,
cast_as_carrier_subset(sk347) = the_carrier(sk347),
inference(orient,[status(thm)],[t4393]) ).
fof(f112,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( element(B,powerset(powerset(the_carrier(A))))
=> ( is_a_cover_of_carrier(A,B)
<=> cast_as_carrier_subset(A) = union_of_subsets(the_carrier(A),B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_pre_topc) ).
fof(f112_nnf,plain,
! [A] :
( ! [B] :
( ( ( cast_as_carrier_subset(A) != union_of_subsets(the_carrier(A),B)
| is_a_cover_of_carrier(A,B) )
& ( cast_as_carrier_subset(A) = union_of_subsets(the_carrier(A),B)
| ~ is_a_cover_of_carrier(A,B) ) )
| ~ element(B,powerset(powerset(the_carrier(A)))) )
| ~ one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f112]) ).
fof(f112_sk,plain,
! [A,B] :
( ( ( cast_as_carrier_subset(A) != union_of_subsets(the_carrier(A),B)
| is_a_cover_of_carrier(A,B) )
& ( cast_as_carrier_subset(A) = union_of_subsets(the_carrier(A),B)
| ~ is_a_cover_of_carrier(A,B) ) )
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ one_sorted_str(A) ),
inference(skolemisation,[status(esa)],[f112_nnf]) ).
cnf(c480,plain,
( cast_as_carrier_subset(X0) = union_of_subsets(the_carrier(X0),X1)
| ~ is_a_cover_of_carrier(X0,X1)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(esa)],[f112_sk]) ).
cnf(t241,plain,
ifeq(one_sorted_str(X1),true,ifeq(element(X2,powerset(powerset(the_carrier(X1)))),true,ifeq(is_a_cover_of_carrier(X1,X2),true,cast_as_carrier_subset(X1),union_of_subsets(the_carrier(X1),X2)),union_of_subsets(the_carrier(X1),X2)),union_of_subsets(the_carrier(X1),X2)) = union_of_subsets(the_carrier(X1),X2),
inference(equality_encoding,[status(esa)],[c480]) ).
cnf(t1260,plain,
ifeq(one_sorted_str(X1),true,ifeq(element(X2,powerset(powerset(the_carrier(X1)))),true,ifeq(is_a_cover_of_carrier(X1,X2),true,cast_as_carrier_subset(X1),union_of_subsets(the_carrier(X1),X2)),union_of_subsets(the_carrier(X1),X2)),union_of_subsets(the_carrier(X1),X2)) = union_of_subsets(the_carrier(X1),X2),
inference(orient,[status(thm)],[t241]) ).
cnf(c2301,plain,
is_a_cover_of_carrier(sk347,sk348),
inference(cnf_transformation,[status(esa)],[f497_sk]) ).
cnf(t29,plain,
is_a_cover_of_carrier(sk347,sk348) = true,
inference(equality_encoding,[status(esa)],[c2301]) ).
cnf(t1214,plain,
is_a_cover_of_carrier(sk347,sk348) = true,
inference(orient,[status(thm)],[t29]) ).
cnf(t1266,plain,
union_of_subsets(the_carrier(sk347),sk348) = ifeq(one_sorted_str(sk347),true,ifeq(element(sk348,powerset(powerset(the_carrier(sk347)))),true,ifeq(true,true,cast_as_carrier_subset(sk347),union_of_subsets(the_carrier(sk347),sk348)),union_of_subsets(the_carrier(sk347),sk348)),union_of_subsets(the_carrier(sk347),sk348)),
inference(cp,[status(thm)],[t1260,t1214]) ).
fof(f312,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> union_of_subsets(A,B) = union(B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k5_setfam_1) ).
fof(f312_nnf,plain,
! [A,B] :
( union_of_subsets(A,B) = union(B)
| ~ element(B,powerset(powerset(A))) ),
inference(nnf_transformation,[status(thm)],[f312]) ).
fof(f312_sk,plain,
! [B,A] :
( union_of_subsets(A,B) = union(B)
| ~ element(B,powerset(powerset(A))) ),
inference(skolemisation,[status(esa)],[f312_nnf]) ).
cnf(c872,plain,
( union_of_subsets(X0,X1) = union(X1)
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[status(esa)],[f312_sk]) ).
cnf(t182,plain,
ifeq(element(X1,powerset(powerset(X2))),true,union_of_subsets(X2,X1),union(X1)) = union(X1),
inference(equality_encoding,[status(esa)],[c872]) ).
cnf(t1254,plain,
ifeq(element(X1,powerset(powerset(X2))),true,union_of_subsets(X2,X1),union(X1)) = union(X1),
inference(orient,[status(thm)],[t182]) ).
fof(f456,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f456_nnf,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(nnf_transformation,[status(thm)],[f456]) ).
fof(f456_sk,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(skolemisation,[status(esa)],[f456_nnf]) ).
cnf(c2215,plain,
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(esa)],[f456_sk]) ).
cnf(t159,plain,
ifeq(subset(X1,X2),true,element(X1,powerset(X2)),true) = true,
inference(equality_encoding,[status(esa)],[c2215]) ).
cnf(t384,plain,
ifeq(subset(X1,X2),true,element(X1,powerset(X2)),true) = true,
inference(orient,[status(thm)],[t159]) ).
fof(f434,lemma,
! [A] : subset(empty_set,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_xboole_1) ).
fof(f434_nnf,plain,
! [A] : subset(empty_set,A),
inference(nnf_transformation,[status(thm)],[f434]) ).
fof(f434_sk,plain,
! [A] : subset(empty_set,A),
inference(skolemisation,[status(esa)],[f434_nnf]) ).
cnf(c2175,plain,
subset(empty_set,X0),
inference(cnf_transformation,[status(esa)],[f434_sk]) ).
cnf(t44,plain,
subset(empty_set,X1) = true,
inference(equality_encoding,[status(esa)],[c2175]) ).
cnf(t768,plain,
subset(empty_set,X1) = true,
inference(orient,[status(thm)],[t44]) ).
cnf(c2302,plain,
sk348 = empty_set,
inference(cnf_transformation,[status(esa)],[f497_sk]) ).
cnf(t0,plain,
sk348 = empty_set,
inference(equality_encoding,[status(esa)],[c2302]) ).
cnf(t1287,plain,
empty_set = sk348,
inference(orient,[status(thm)],[t0]) ).
cnf(t4346,plain,
subset(sk348,X1) = true,
inference(step,[status(thm)],[t768,t1287]) ).
cnf(t1298,plain,
subset(sk348,X1) = true,
inference(rw,[status(thm)],[t4346]) ).
cnf(t1657,plain,
subset(sk348,X1) = true,
inference(orient,[status(thm)],[t1298]) ).
cnf(t1664,plain,
true = ifeq(true,true,element(sk348,powerset(X1)),true),
inference(cp,[status(thm)],[t384,t1657]) ).
cnf(t4421,plain,
true = element(sk348,powerset(X1)),
inference(step,[status(thm)],[t1664,t244]) ).
cnf(t2049,plain,
element(sk348,powerset(X1)) = true,
inference(orient,[status(thm)],[t4421]) ).
cnf(t2057,plain,
union(sk348) = ifeq(true,true,union_of_subsets(X1,sk348),union(sk348)),
inference(cp,[status(thm)],[t1254,t2049]) ).
cnf(t4422,plain,
union(sk348) = union_of_subsets(X1,sk348),
inference(step,[status(thm)],[t2057,t244]) ).
cnf(t2072,plain,
union_of_subsets(X1,sk348) = union(sk348),
inference(orient,[status(thm)],[t4422]) ).
cnf(t4433,plain,
union(sk348) = ifeq(one_sorted_str(sk347),true,ifeq(element(sk348,powerset(powerset(the_carrier(sk347)))),true,ifeq(true,true,cast_as_carrier_subset(sk347),union_of_subsets(the_carrier(sk347),sk348)),union_of_subsets(the_carrier(sk347),sk348)),union_of_subsets(the_carrier(sk347),sk348)),
inference(step,[status(thm)],[t1266,t2072]) ).
cnf(t4434,plain,
union(sk348) = ifeq(true,true,ifeq(element(sk348,powerset(powerset(the_carrier(sk347)))),true,ifeq(true,true,cast_as_carrier_subset(sk347),union_of_subsets(the_carrier(sk347),sk348)),union_of_subsets(the_carrier(sk347),sk348)),union_of_subsets(the_carrier(sk347),sk348)),
inference(step,[status(thm)],[t4433,t1206]) ).
cnf(t4435,plain,
union(sk348) = ifeq(element(sk348,powerset(powerset(the_carrier(sk347)))),true,ifeq(true,true,cast_as_carrier_subset(sk347),union_of_subsets(the_carrier(sk347),sk348)),union_of_subsets(the_carrier(sk347),sk348)),
inference(step,[status(thm)],[t4434,t244]) ).
cnf(c2300,plain,
element(sk348,powerset(powerset(the_carrier(sk347)))),
inference(cnf_transformation,[status(esa)],[f497_sk]) ).
cnf(t70,plain,
element(sk348,powerset(powerset(the_carrier(sk347)))) = true,
inference(equality_encoding,[status(esa)],[c2300]) ).
cnf(t950,plain,
element(sk348,powerset(powerset(the_carrier(sk347)))) = true,
inference(orient,[status(thm)],[t70]) ).
cnf(t4436,plain,
union(sk348) = ifeq(true,true,ifeq(true,true,cast_as_carrier_subset(sk347),union_of_subsets(the_carrier(sk347),sk348)),union_of_subsets(the_carrier(sk347),sk348)),
inference(step,[status(thm)],[t4435,t950]) ).
cnf(t4437,plain,
union(sk348) = ifeq(true,true,cast_as_carrier_subset(sk347),union_of_subsets(the_carrier(sk347),sk348)),
inference(step,[status(thm)],[t4436,t244]) ).
cnf(t4438,plain,
union(sk348) = cast_as_carrier_subset(sk347),
inference(step,[status(thm)],[t4437,t244]) ).
cnf(t4439,plain,
union(sk348) = the_carrier(sk347),
inference(step,[status(thm)],[t4438,t1637]) ).
cnf(t2183,plain,
the_carrier(sk347) = union(sk348),
inference(orient,[status(thm)],[t4439]) ).
cnf(t4440,plain,
cast_as_carrier_subset(sk347) = union(sk348),
inference(step,[status(thm)],[t1637,t2183]) ).
cnf(t2184,plain,
cast_as_carrier_subset(sk347) = union(sk348),
inference(orient,[status(thm)],[t4440]) ).
fof(f369,lemma,
! [A,B] :
( subset(A,B)
=> set_union2(A,B) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_xboole_1) ).
fof(f369_nnf,plain,
! [A,B] :
( set_union2(A,B) = B
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f369]) ).
fof(f369_sk,plain,
! [A,B] :
( set_union2(A,B) = B
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f369_nnf]) ).
cnf(c2075,plain,
( set_union2(X0,X1) = X1
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f369_sk]) ).
cnf(t135,plain,
ifeq(subset(X1,X2),true,set_union2(X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c2075]) ).
cnf(t249,plain,
ifeq(subset(X1,X2),true,set_union2(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t135]) ).
cnf(c2214,plain,
( subset(X0,X1)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(esa)],[f456_sk]) ).
cnf(t152,plain,
ifeq(element(X1,powerset(X2)),true,subset(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c2214]) ).
cnf(t432,plain,
ifeq(element(X1,powerset(X2)),true,subset(X1,X2),true) = true,
inference(orient,[status(thm)],[t152]) ).
fof(f159,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> element(union_of_subsets(A,B),powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_setfam_1) ).
fof(f159_nnf,plain,
! [A,B] :
( element(union_of_subsets(A,B),powerset(A))
| ~ element(B,powerset(powerset(A))) ),
inference(nnf_transformation,[status(thm)],[f159]) ).
fof(f159_sk,plain,
! [B,A] :
( element(union_of_subsets(A,B),powerset(A))
| ~ element(B,powerset(powerset(A))) ),
inference(skolemisation,[status(esa)],[f159_nnf]) ).
cnf(c552,plain,
( element(union_of_subsets(X0,X1),powerset(X0))
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[status(esa)],[f159_sk]) ).
cnf(t201,plain,
ifeq(element(X1,powerset(powerset(X2))),true,element(union_of_subsets(X2,X1),powerset(X2)),true) = true,
inference(equality_encoding,[status(esa)],[c552]) ).
cnf(t435,plain,
ifeq(element(X1,powerset(powerset(X2))),true,element(union_of_subsets(X2,X1),powerset(X2)),true) = true,
inference(orient,[status(thm)],[t201]) ).
cnf(t2073,plain,
true = ifeq(element(sk348,powerset(powerset(X1))),true,element(union(sk348),powerset(X1)),true),
inference(cp,[status(thm)],[t435,t2072]) ).
cnf(t4471,plain,
true = ifeq(true,true,element(union(sk348),powerset(X1)),true),
inference(step,[status(thm)],[t2073,t2049]) ).
cnf(t4472,plain,
true = element(union(sk348),powerset(X1)),
inference(step,[status(thm)],[t4471,t244]) ).
cnf(t2629,plain,
element(union(sk348),powerset(X1)) = true,
inference(orient,[status(thm)],[t4472]) ).
cnf(t2637,plain,
true = ifeq(true,true,subset(union(sk348),X1),true),
inference(cp,[status(thm)],[t432,t2629]) ).
cnf(t4473,plain,
true = subset(union(sk348),X1),
inference(step,[status(thm)],[t2637,t244]) ).
cnf(t2658,plain,
subset(union(sk348),X1) = true,
inference(orient,[status(thm)],[t4473]) ).
cnf(t2659,plain,
X1 = ifeq(true,true,set_union2(union(sk348),X1),X1),
inference(cp,[status(thm)],[t249,t2658]) ).
cnf(t4474,plain,
X1 = set_union2(union(sk348),X1),
inference(step,[status(thm)],[t2659,t244]) ).
cnf(t2677,plain,
set_union2(union(sk348),X1) = X1,
inference(orient,[status(thm)],[t4474]) ).
fof(f398,axiom,
! [A] : set_union2(A,empty_set) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_boole) ).
fof(f398_nnf,plain,
! [A] : set_union2(A,empty_set) = A,
inference(nnf_transformation,[status(thm)],[f398]) ).
fof(f398_sk,plain,
! [A] : set_union2(A,empty_set) = A,
inference(skolemisation,[status(esa)],[f398_nnf]) ).
cnf(c2117,plain,
set_union2(X0,empty_set) = X0,
inference(cnf_transformation,[status(esa)],[f398_sk]) ).
cnf(t41,plain,
set_union2(X1,empty_set) = X1,
inference(equality_encoding,[status(esa)],[c2117]) ).
cnf(t263,plain,
set_union2(X1,empty_set) = X1,
inference(orient,[status(thm)],[t41]) ).
cnf(t4348,plain,
set_union2(X1,sk348) = X1,
inference(step,[status(thm)],[t263,t1287]) ).
cnf(t1300,plain,
set_union2(X1,sk348) = X1,
inference(rw,[status(thm)],[t4348]) ).
cnf(t1740,plain,
set_union2(X1,sk348) = X1,
inference(orient,[status(thm)],[t1300]) ).
cnf(t2679,plain,
sk348 = union(sk348),
inference(cp,[status(thm)],[t2677,t1740]) ).
cnf(t2691,plain,
union(sk348) = sk348,
inference(orient,[status(thm)],[t2679]) ).
cnf(t4475,plain,
cast_as_carrier_subset(sk347) = sk348,
inference(step,[status(thm)],[t2184,t2691]) ).
cnf(t2692,plain,
cast_as_carrier_subset(sk347) = sk348,
inference(orient,[status(thm)],[t4475]) ).
cnf(t4562,plain,
true = ifeq(empty(sk348),true,false,true),
inference(step,[status(thm)],[t4561,t2692]) ).
fof(f194,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc12_relat_1) ).
fof(f194_nnf,plain,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
inference(nnf_transformation,[status(thm)],[f194]) ).
fof(f194_sk,plain,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
inference(skolemisation,[status(esa)],[f194_nnf]) ).
cnf(c594,plain,
empty(empty_set),
inference(cnf_transformation,[status(esa)],[f194_sk]) ).
cnf(t1,plain,
empty(empty_set) = true,
inference(equality_encoding,[status(esa)],[c594]) ).
cnf(t886,plain,
empty(empty_set) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t4345,plain,
empty(sk348) = true,
inference(step,[status(thm)],[t886,t1287]) ).
cnf(t1297,plain,
empty(sk348) = true,
inference(rw,[status(thm)],[t4345]) ).
cnf(t1624,plain,
empty(sk348) = true,
inference(orient,[status(thm)],[t1297]) ).
cnf(t4563,plain,
true = ifeq(true,true,false,true),
inference(step,[status(thm)],[t4562,t1624]) ).
cnf(t4564,plain,
true = false,
inference(step,[status(thm)],[t4563,t244]) ).
cnf(t4288,plain,
false = true,
inference(orient,[status(thm)],[t4564]) ).
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(f65,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(f65_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)],[f65]) ).
fof(f65_sk,plain,
! [A,C,B,D] :
( ( ( ( in(ordered_pair(sk37(A,B,C),B),A)
& sk37(A,B,C) != B
& ~ in(sk37(A,B,C),C) )
| ( ( ~ in(ordered_pair(sk37(A,B,C),B),A)
| sk37(A,B,C) = B )
& in(sk37(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,[sk37])],[f65_nnf]) ).
cnf(c245,plain,
( X3 != X1
| ~ in(X3,X2)
| X2 != fiber(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
fof(f67,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f67_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
! [A,B] :
( ( in(sk40(A),A)
| A = empty_set )
& ( ~ in(B,A)
| A != empty_set ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk40])],[f67_nnf]) ).
cnf(c263,plain,
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
fof(f94,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(f94_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)],[f94]) ).
fof(f94_sk,plain,
! [C,A,B,D] :
( ( ( ~ in(sk73(A,B,C),B)
& in(sk73(A,B,C),A)
& ~ in(sk73(A,B,C),C) )
| ( ( in(sk73(A,B,C),B)
| ~ in(sk73(A,B,C),A) )
& in(sk73(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,[sk73])],[f94_nnf]) ).
cnf(c395,plain,
( ~ in(X3,X1)
| ~ in(X3,X2)
| X2 != set_difference(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
fof(f116,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f116_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)],[f116]) ).
fof(f116_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)],[f116_nnf]) ).
cnf(c506,plain,
( X0 != X1
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f116_sk]) ).
fof(f197,axiom,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_finset_1) ).
fof(f197_nnf,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(nnf_transformation,[status(thm)],[f197]) ).
fof(f197_sk,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(skolemisation,[status(esa)],[f197_nnf]) ).
cnf(c600,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f197_sk]) ).
fof(f198,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(f198_nnf,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f198]) ).
fof(f198_sk,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(skolemisation,[status(esa)],[f198_nnf]) ).
cnf(c602,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f198_sk]) ).
fof(f200,axiom,
! [A] : ~ empty(succ(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_ordinal1) ).
fof(f200_nnf,plain,
! [A] : ~ empty(succ(A)),
inference(nnf_transformation,[status(thm)],[f200]) ).
fof(f200_sk,plain,
! [A] : ~ empty(succ(A)),
inference(skolemisation,[status(esa)],[f200_nnf]) ).
cnf(c608,plain,
~ empty(succ(X0)),
inference(cnf_transformation,[status(esa)],[f200_sk]) ).
fof(f201,axiom,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_ordinal2) ).
fof(f201_nnf,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(nnf_transformation,[status(thm)],[f201]) ).
fof(f201_sk,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(skolemisation,[status(esa)],[f201_nnf]) ).
cnf(c612,plain,
~ empty(omega),
inference(cnf_transformation,[status(esa)],[f201_sk]) ).
fof(f205,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f205_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f205]) ).
fof(f205_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f205_nnf]) ).
cnf(c621,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f205_sk]) ).
fof(f207,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f207_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f207]) ).
fof(f207_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f207_nnf]) ).
cnf(c623,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f207_sk]) ).
fof(f211,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(f211_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)],[f211]) ).
fof(f211_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)],[f211_nnf]) ).
cnf(c628,plain,
( ~ empty(succ(X0))
| ~ natural(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f211_sk]) ).
fof(f216,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f216_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f216]) ).
fof(f216_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f216_nnf]) ).
cnf(c645,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f216_sk]) ).
fof(f230,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(f230_nnf,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f230]) ).
fof(f230_sk,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f230_nnf]) ).
cnf(c682,plain,
( ~ empty(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f230_sk]) ).
fof(f232,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f232_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f232]) ).
fof(f232_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f232_nnf]) ).
cnf(c687,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f232_sk]) ).
fof(f258,axiom,
! [A,B] : ~ proper_subset(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f258_nnf,plain,
! [A,B] : ~ proper_subset(A,A),
inference(nnf_transformation,[status(thm)],[f258]) ).
fof(f258_sk,plain,
! [A] : ~ proper_subset(A,A),
inference(skolemisation,[status(esa)],[f258_nnf]) ).
cnf(c733,plain,
~ proper_subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f258_sk]) ).
fof(f260,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l1_zfmisc_1) ).
fof(f260_nnf,plain,
! [A] : singleton(A) != empty_set,
inference(nnf_transformation,[status(thm)],[f260]) ).
fof(f260_sk,plain,
! [A] : singleton(A) != empty_set,
inference(skolemisation,[status(esa)],[f260_nnf]) ).
cnf(c737,plain,
singleton(X0) != empty_set,
inference(cnf_transformation,[status(esa)],[f260_sk]) ).
fof(f262,lemma,
! [A,B] :
~ ( in(A,B)
& disjoint(singleton(A),B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l25_zfmisc_1) ).
fof(f262_nnf,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(nnf_transformation,[status(thm)],[f262]) ).
fof(f262_sk,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(skolemisation,[status(esa)],[f262_nnf]) ).
cnf(c739,plain,
( ~ in(X0,X1)
| ~ disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f262_sk]) ).
fof(f279,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(f279_nnf,plain,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f279]) ).
fof(f279_sk,plain,
( natural(sk117)
& ordinal(sk117)
& epsilon_connected(sk117)
& epsilon_transitive(sk117)
& ~ empty(sk117) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk117])],[f279_nnf]) ).
cnf(c778,plain,
~ empty(sk117),
inference(cnf_transformation,[status(esa)],[f279_sk]) ).
fof(f280,axiom,
? [A] :
( finite(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_finset_1) ).
fof(f280_nnf,plain,
? [A] :
( finite(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f280]) ).
fof(f280_sk,plain,
( finite(sk118)
& ~ empty(sk118) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk118])],[f280_nnf]) ).
cnf(c783,plain,
~ empty(sk118),
inference(cnf_transformation,[status(esa)],[f280_sk]) ).
fof(f283,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(f283_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)],[f283]) ).
fof(f283_sk,plain,
( v5_membered(sk121)
& v4_membered(sk121)
& v3_membered(sk121)
& v2_membered(sk121)
& v1_membered(sk121)
& ~ empty(sk121) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk121])],[f283_nnf]) ).
cnf(c791,plain,
~ empty(sk121),
inference(cnf_transformation,[status(esa)],[f283_sk]) ).
fof(f295,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f295_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f295]) ).
fof(f295_sk,plain,
( relation(sk133)
& ~ empty(sk133) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk133])],[f295_nnf]) ).
cnf(c838,plain,
~ empty(sk133),
inference(cnf_transformation,[status(esa)],[f295_sk]) ).
fof(f298,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f298_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f298]) ).
fof(f298_sk,plain,
~ empty(sk136),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk136])],[f298_nnf]) ).
cnf(c845,plain,
~ empty(sk136),
inference(cnf_transformation,[status(esa)],[f298_sk]) ).
fof(f301,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_ordinal1) ).
fof(f301_nnf,plain,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f301]) ).
fof(f301_sk,plain,
( ordinal(sk139)
& epsilon_connected(sk139)
& epsilon_transitive(sk139)
& ~ empty(sk139) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk139])],[f301_nnf]) ).
cnf(c852,plain,
~ empty(sk139),
inference(cnf_transformation,[status(esa)],[f301_sk]) ).
fof(f303,axiom,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_struct_0) ).
fof(f303_nnf,plain,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f303]) ).
fof(f303_sk,plain,
( ~ empty_carrier(sk141)
& one_sorted_str(sk141) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk141])],[f303_nnf]) ).
cnf(c859,plain,
~ empty_carrier(sk141),
inference(cnf_transformation,[status(esa)],[f303_sk]) ).
fof(f325,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(f325_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)],[f325]) ).
fof(f325_sk,plain,
! [B,E,G,I,K,L,N,P,D,R,T] :
( ( ( T = sk168(D,R)
| ~ subset(sk168(D,R),T)
| ~ in(T,R) )
& in(sk168(D,R),R) )
| R = empty_set
| ~ element(R,powerset(powerset(D)))
| ~ in(D,omega)
| ~ ordinal(D)
| ( ( ( sk167(P) != P
& subset(P,sk167(P))
& in(sk167(P),sk166) )
| ~ in(P,sk166) )
& sk166 != empty_set
& element(sk166,powerset(powerset(sk164)))
& in(sk164,omega)
& sk164 != empty_set
& ( ( ( N = sk165(K,L)
| ~ subset(sk165(K,L),N)
| ~ in(N,L) )
& in(sk165(K,L),L) )
| L = empty_set
| ~ element(L,powerset(powerset(K)))
| ~ in(K,omega)
| ~ in(K,sk164)
| ~ ordinal(K) )
& being_limit_ordinal(sk164)
& ordinal(sk164) )
| ( ( ( sk163(I) != I
& subset(I,sk163(I))
& in(sk163(I),sk162) )
| ~ in(I,sk162) )
& sk162 != empty_set
& element(sk162,powerset(powerset(succ(sk160))))
& in(succ(sk160),omega)
& ( ( ( G = sk161(E)
| ~ subset(sk161(E),G)
| ~ in(G,E) )
& in(sk161(E),E) )
| E = empty_set
| ~ element(E,powerset(powerset(sk160)))
| ~ in(sk160,omega) )
& ordinal(sk160) )
| ( ( ( sk159(B) != B
& subset(B,sk159(B))
& in(sk159(B),sk158) )
| ~ in(B,sk158) )
& sk158 != empty_set
& element(sk158,powerset(powerset(empty_set)))
& in(empty_set,omega) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk158,sk159,sk160,sk161,sk162,sk163,sk164,sk165,sk166,sk167,sk168])],[f325_nnf]) ).
cnf(c1003,plain,
( sk159(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])],[f325_sk]) ).
cnf(c1008,plain,
( sk158 != 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])],[f325_sk]) ).
cnf(c1017,plain,
( ~ subset(sk161(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])],[f325_sk]) ).
cnf(c1039,plain,
( sk163(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])],[f325_sk]) ).
cnf(c1044,plain,
( sk162 != 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])],[f325_sk]) ).
cnf(c1062,plain,
( ~ subset(sk165(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])],[f325_sk]) ).
cnf(c1093,plain,
( sk167(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])],[f325_sk]) ).
cnf(c1098,plain,
( sk166 != 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])],[f325_sk]) ).
cnf(c1107,plain,
( sk164 != 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])],[f325_sk]) ).
cnf(c1119,plain,
( ~ subset(sk168(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])],[f325_sk]) ).
fof(f455,lemma,
! [A,B,C] :
~ ( in(C,A)
& in(B,C)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_ordinal1) ).
fof(f455_nnf,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f455]) ).
fof(f455_sk,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f455_nnf]) ).
cnf(c2213,plain,
( ~ in(X2,X0)
| ~ in(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f455_sk]) ).
fof(f458,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(f458_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)],[f458]) ).
fof(f458_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,B)
| ~ in(C,A) )
& ( ( in(sk336(A,B),B)
& in(sk336(A,B),A) )
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk336])],[f458_nnf]) ).
cnf(c2219,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f458_sk]) ).
fof(f462,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(f462_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)],[f462]) ).
fof(f462_sk,plain,
! [A,B] :
( ( ( ~ being_limit_ordinal(A)
| A != succ(B)
| ~ ordinal(B) )
& ( ( A = succ(sk338(A))
& ordinal(sk338(A)) )
| being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk338])],[f462_nnf]) ).
cnf(c2228,plain,
( ~ being_limit_ordinal(X0)
| X0 != succ(X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f462_sk]) ).
fof(f484,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(f484_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)],[f484]) ).
fof(f484_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk342(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk342])],[f484_nnf]) ).
cnf(c2264,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f484_sk]) ).
fof(f490,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(f490_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f490]) ).
fof(f490_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f490_nnf]) ).
cnf(c2288,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f490_sk]) ).
fof(f496,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(f496_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f496]) ).
fof(f496_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f496_nnf]) ).
cnf(c2297,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f496_sk]) ).
fof(f501,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f501_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f501]) ).
fof(f501_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f501_nnf]) ).
cnf(c2308,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f501_sk]) ).
fof(f506,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f506_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)],[f506]) ).
fof(f506_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)],[f506_nnf]) ).
cnf(c2315,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f506_sk]) ).
fof(f517,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f517_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f517]) ).
fof(f517_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f517_nnf]) ).
cnf(c2333,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f517_sk]) ).
fof(f519,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(f519_nnf,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f519]) ).
fof(f519_sk,plain,
! [A,B,D] :
( ( ( ~ in(D,sk350(A,B))
| ~ in(D,B) )
& in(sk350(A,B),B) )
| ~ in(A,B) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk350])],[f519_nnf]) ).
cnf(c2337,plain,
( ~ in(X3,sk350(X0,X1))
| ~ in(X3,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f519_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c1,c129,c245,c263,c395,c506,c600,c602,c608,c612,c621,c623,c628,c645,c682,c687,c733,c737,c739,c778,c783,c791,c838,c845,c852,c859,c1003,c1008,c1017,c1039,c1044,c1062,c1093,c1098,c1107,c1119,c2213,c2219,c2228,c2264,c2288,c2297,c2298,c2308,c2315,c2333,c2337]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t4288]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU325+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.57 % Computer : n017.cluster.edu
% 0.08/0.57 % Model : x86_64 x86_64
% 0.08/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.57 % Memory : 8046.5625MB
% 0.08/0.57 % OS : Linux 6.8.0-71-generic
% 0.08/0.57 % CPULimit : 300
% 0.08/0.57 % WCLimit : 300
% 0.08/0.57 % DateTime : Thu Sep 24 13:37:32 UTC 2026
% 0.08/0.57 % CPUTime :
% 0.08/0.57 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 79.47/10.64 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 79.47/10.64 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------