%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU056+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n007.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:50:53 PM UTC 2026
% Result : Theorem 74.97s 10.91s
% Output : Proof 74.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 19
% Syntax : Number of formulae : 151 ( 98 unt; 0 def)
% Number of atoms : 243 ( 99 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 169 ( 77 ~; 45 |; 36 &)
% ( 1 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-4 aty)
% Number of variables : 170 ( 7 sgn 77 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [A,B] :
( disjoint(A,B)
<=> set_intersection2(A,B) = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d7_xboole_0) ).
fof(f5_nnf,plain,
! [A,B] :
( ( set_intersection2(A,B) != empty_set
| disjoint(A,B) )
& ( set_intersection2(A,B) = empty_set
| ~ disjoint(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,B] :
( ( set_intersection2(A,B) != empty_set
| disjoint(A,B) )
& ( set_intersection2(A,B) = empty_set
| ~ disjoint(A,B) ) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c8,plain,
( set_intersection2(X0,X1) != empty_set
| disjoint(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t239,plain,
ifeq(set_intersection2(X1,X2),empty_set,disjoint(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t337,plain,
ifeq(set_intersection2(X1,X2),empty_set,disjoint(X1,X2),true) = true,
inference(orient,[status(thm)],[t239]) ).
fof(f36,axiom,
! [A,B] :
~ ( empty(B)
& A != B
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_boole) ).
fof(f36_nnf,plain,
! [A,B] :
( ~ empty(B)
| A = B
| ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [A,B] :
( ~ empty(B)
| A = B
| ~ empty(A) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c57,plain,
( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(hi48,axiom,
ifeq(empty(X0),true,ifeq(empty(X1),true,X0,X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c57]) ).
fof(f11,axiom,
( relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_relat_1) ).
fof(f11_nnf,plain,
( relation(empty_set)
& empty(empty_set) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
( relation(empty_set)
& empty(empty_set) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c16,plain,
empty(empty_set),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(hi12,axiom,
empty(empty_set) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
fof(f14,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_relat_1) ).
fof(f14_nnf,plain,
? [A] :
( relation(A)
& empty(A) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
( relation(sk2)
& empty(sk2) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2])],[f14_nnf]) ).
cnf(c21,plain,
empty(sk2),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(hi17,axiom,
empty(sk2) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t0,plain,
sk2 = empty_set,
inference(hyper_resolution,[status(thm)],[hi48,hi12,hi17]) ).
cnf(t876,plain,
empty_set = sk2,
inference(orient,[status(thm)],[t0]) ).
cnf(t15149,plain,
ifeq(set_intersection2(X1,X2),sk2,disjoint(X1,X2),true) = true,
inference(step,[status(thm)],[t337,t876]) ).
cnf(t951,plain,
ifeq(set_intersection2(X1,X2),sk2,disjoint(X1,X2),true) = true,
inference(rw,[status(thm)],[t15149]) ).
fof(f17,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_funct_1) ).
fof(f17_nnf,plain,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
( function(sk5)
& empty(sk5)
& relation(sk5) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5])],[f17_nnf]) ).
cnf(c27,plain,
empty(sk5),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(hi23,axiom,
empty(sk5) = true,
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(t3,plain,
sk5 = empty_set,
inference(hyper_resolution,[status(thm)],[hi48,hi12,hi23]) ).
cnf(t15150,plain,
sk5 = sk2,
inference(step,[status(thm)],[t3,t876]) ).
cnf(t952,plain,
sk2 = sk5,
inference(orient,[status(thm)],[t15150]) ).
cnf(t15754,plain,
ifeq(set_intersection2(X1,X2),sk5,disjoint(X1,X2),true) = true,
inference(step,[status(thm)],[t951,t952]) ).
cnf(t10665,plain,
ifeq(set_intersection2(X1,X2),sk5,disjoint(X1,X2),true) = true,
inference(orient,[status(thm)],[t15754]) ).
fof(f4,axiom,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(f4_nnf,plain,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c6,plain,
set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t219,plain,
set_intersection2(X1,X2) = set_intersection2(X2,X1),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t1005,plain,
set_intersection2(X1,X2) = set_intersection2(X2,X1),
inference(orient,[status(thm)],[t219]) ).
cnf(t10670,plain,
true = ifeq(set_intersection2(X1,X2),sk5,disjoint(X2,X1),true),
inference(cp,[status(thm)],[t10665,t1005]) ).
cnf(t14923,plain,
ifeq(set_intersection2(X1,X2),sk5,disjoint(X2,X1),true) = true,
inference(orient,[status(thm)],[t10670]) ).
fof(f26,conjecture,
! [A,B,C] :
( ( function(C)
& relation(C) )
=> ( ( one_to_one(C)
& disjoint(A,B) )
=> disjoint(relation_image(C,A),relation_image(C,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t125_funct_1) ).
fof(f26_neg,negated_conjecture,
~ ! [A,B,C] :
( ( function(C)
& relation(C) )
=> ( ( one_to_one(C)
& disjoint(A,B) )
=> disjoint(relation_image(C,A),relation_image(C,B)) ) ),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f26_nnf,plain,
? [A,B,C] :
( ~ disjoint(relation_image(C,A),relation_image(C,B))
& one_to_one(C)
& disjoint(A,B)
& function(C)
& relation(C) ),
inference(nnf_transformation,[status(thm)],[f26_neg]) ).
fof(f26_sk,plain,
( ~ disjoint(relation_image(sk13,sk11),relation_image(sk13,sk12))
& one_to_one(sk13)
& disjoint(sk11,sk12)
& function(sk13)
& relation(sk13) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk11,sk12,sk13])],[f26_nnf]) ).
cnf(c46,plain,
~ disjoint(relation_image(sk13,sk11),relation_image(sk13,sk12)),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(t226,plain,
disjoint(relation_image(sk13,sk11),relation_image(sk13,sk12)) = false,
inference(equality_encoding,[status(esa)],[c46]) ).
cnf(t1106,plain,
disjoint(relation_image(sk13,sk11),relation_image(sk13,sk12)) = false,
inference(orient,[status(thm)],[t226]) ).
cnf(t14927,plain,
true = ifeq(set_intersection2(relation_image(sk13,sk12),relation_image(sk13,sk11)),sk5,false,true),
inference(cp,[status(thm)],[t14923,t1106]) ).
fof(f25,axiom,
! [A,B,C] :
( ( function(C)
& relation(C) )
=> ( one_to_one(C)
=> relation_image(C,set_intersection2(A,B)) = set_intersection2(relation_image(C,A),relation_image(C,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t121_funct_1) ).
fof(f25_nnf,plain,
! [A,B,C] :
( relation_image(C,set_intersection2(A,B)) = set_intersection2(relation_image(C,A),relation_image(C,B))
| ~ one_to_one(C)
| ~ function(C)
| ~ relation(C) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [C,A,B] :
( relation_image(C,set_intersection2(A,B)) = set_intersection2(relation_image(C,A),relation_image(C,B))
| ~ one_to_one(C)
| ~ function(C)
| ~ relation(C) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c41,plain,
( relation_image(X2,set_intersection2(X0,X1)) = set_intersection2(relation_image(X2,X0),relation_image(X2,X1))
| ~ one_to_one(X2)
| ~ function(X2)
| ~ relation(X2) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(t255,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(one_to_one(X1),true,relation_image(X1,set_intersection2(X2,X3)),set_intersection2(relation_image(X1,X2),relation_image(X1,X3))),set_intersection2(relation_image(X1,X2),relation_image(X1,X3))),set_intersection2(relation_image(X1,X2),relation_image(X1,X3))) = set_intersection2(relation_image(X1,X2),relation_image(X1,X3)),
inference(equality_encoding,[status(esa)],[c41]) ).
cnf(t1024,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(one_to_one(X1),true,relation_image(X1,set_intersection2(X2,X3)),set_intersection2(relation_image(X1,X2),relation_image(X1,X3))),set_intersection2(relation_image(X1,X2),relation_image(X1,X3))),set_intersection2(relation_image(X1,X2),relation_image(X1,X3))) = set_intersection2(relation_image(X1,X2),relation_image(X1,X3)),
inference(orient,[status(thm)],[t255]) ).
fof(f8,axiom,
! [A,B] :
( ( relation(B)
& relation(A) )
=> relation(set_intersection2(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_relat_1) ).
fof(f8_nnf,plain,
! [A,B] :
( relation(set_intersection2(A,B))
| ~ relation(B)
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,B] :
( relation(set_intersection2(A,B))
| ~ relation(B)
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c13,plain,
( relation(set_intersection2(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(hi10,axiom,
ifeq(relation(X0),true,ifeq(relation(X1),true,relation(set_intersection2(X0,X1)),true),true) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(c42,plain,
relation(sk13),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(hi36,negated_conjecture,
relation(sk13) = true,
inference(equality_encoding,[status(esa)],[c42]) ).
cnf(t101,plain,
relation(set_intersection2(sk13,sk13)) = true,
inference(hyper_resolution,[status(thm)],[hi10,hi36,hi36]) ).
fof(f12,axiom,
! [A,B] : set_intersection2(A,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_k3_xboole_0) ).
fof(f12_nnf,plain,
! [A,B] : set_intersection2(A,A) = A,
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A] : set_intersection2(A,A) = A,
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c18,plain,
set_intersection2(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t67,plain,
set_intersection2(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t256,plain,
set_intersection2(X1,X1) = X1,
inference(orient,[status(thm)],[t67]) ).
cnf(t14994,plain,
relation(sk13) = true,
inference(step,[status(thm)],[t101,t256]) ).
cnf(t297,plain,
relation(sk13) = true,
inference(orient,[status(thm)],[t14994]) ).
cnf(t1041,plain,
set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2)) = ifeq(true,true,ifeq(function(sk13),true,ifeq(one_to_one(sk13),true,relation_image(sk13,set_intersection2(X1,X2)),set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2))),set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2))),set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2))),
inference(cp,[status(thm)],[t1024,t297]) ).
cnf(t153,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t257,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t153]) ).
cnf(t15358,plain,
set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2)) = ifeq(function(sk13),true,ifeq(one_to_one(sk13),true,relation_image(sk13,set_intersection2(X1,X2)),set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2))),set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2))),
inference(step,[status(thm)],[t1041,t257]) ).
cnf(c43,plain,
function(sk13),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(t16,plain,
function(sk13) = true,
inference(equality_encoding,[status(esa)],[c43]) ).
cnf(t764,plain,
function(sk13) = true,
inference(orient,[status(thm)],[t16]) ).
cnf(t15359,plain,
set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2)) = ifeq(true,true,ifeq(one_to_one(sk13),true,relation_image(sk13,set_intersection2(X1,X2)),set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2))),set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2))),
inference(step,[status(thm)],[t15358,t764]) ).
cnf(t15360,plain,
set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2)) = ifeq(one_to_one(sk13),true,relation_image(sk13,set_intersection2(X1,X2)),set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2))),
inference(step,[status(thm)],[t15359,t257]) ).
cnf(c45,plain,
one_to_one(sk13),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(t24,plain,
one_to_one(sk13) = true,
inference(equality_encoding,[status(esa)],[c45]) ).
cnf(t792,plain,
one_to_one(sk13) = true,
inference(orient,[status(thm)],[t24]) ).
cnf(t15361,plain,
set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2)) = ifeq(true,true,relation_image(sk13,set_intersection2(X1,X2)),set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2))),
inference(step,[status(thm)],[t15360,t792]) ).
cnf(t15362,plain,
set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2)) = relation_image(sk13,set_intersection2(X1,X2)),
inference(step,[status(thm)],[t15361,t257]) ).
cnf(t1941,plain,
set_intersection2(relation_image(sk13,X1),relation_image(sk13,X2)) = relation_image(sk13,set_intersection2(X1,X2)),
inference(orient,[status(thm)],[t15362]) ).
cnf(t16081,plain,
true = ifeq(relation_image(sk13,set_intersection2(sk12,sk11)),sk5,false,true),
inference(step,[status(thm)],[t14927,t1941]) ).
fof(f24,axiom,
! [A,B] :
( disjoint(A,B)
=> disjoint(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_r1_xboole_0) ).
fof(f24_nnf,plain,
! [A,B] :
( disjoint(B,A)
| ~ disjoint(A,B) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [A,B] :
( disjoint(B,A)
| ~ disjoint(A,B) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c40,plain,
( disjoint(X1,X0)
| ~ disjoint(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(hi34,axiom,
ifeq(disjoint(X0,X1),true,disjoint(X1,X0),true) = true,
inference(equality_encoding,[status(esa)],[c40]) ).
cnf(c44,plain,
disjoint(sk11,sk12),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(hi38,negated_conjecture,
disjoint(sk11,sk12) = true,
inference(equality_encoding,[status(esa)],[c44]) ).
cnf(h97,plain,
disjoint(sk12,sk11) = true,
inference(hyper_resolution,[status(thm)],[hi34,hi38]) ).
cnf(c7,plain,
( set_intersection2(X0,X1) = empty_set
| ~ disjoint(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(hi4,axiom,
ifeq(disjoint(X0,X1),true,set_intersection2(X0,X1),empty_set) = empty_set,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t72,plain,
set_intersection2(sk12,sk11) = empty_set,
inference(hyper_resolution,[status(thm)],[hi4,h97]) ).
cnf(t809,plain,
set_intersection2(sk12,sk11) = empty_set,
inference(orient,[status(thm)],[t72]) ).
cnf(t15009,plain,
set_intersection2(sk12,sk11) = sk2,
inference(step,[status(thm)],[t809,t876]) ).
cnf(t879,plain,
set_intersection2(sk12,sk11) = sk2,
inference(orient,[status(thm)],[t15009]) ).
cnf(t15153,plain,
set_intersection2(sk12,sk11) = sk5,
inference(step,[status(thm)],[t879,t952]) ).
cnf(t955,plain,
set_intersection2(sk12,sk11) = sk5,
inference(orient,[status(thm)],[t15153]) ).
cnf(t16082,plain,
true = ifeq(relation_image(sk13,sk5),sk5,false,true),
inference(step,[status(thm)],[t16081,t955]) ).
cnf(h82,plain,
relation(set_intersection2(sk13,sk13)) = true,
inference(hyper_resolution,[status(thm)],[hi10,hi36,hi36]) ).
fof(f27,axiom,
! [A] :
( relation(A)
=> relation_image(A,empty_set) = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t149_relat_1) ).
fof(f27_nnf,plain,
! [A] :
( relation_image(A,empty_set) = empty_set
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [A] :
( relation_image(A,empty_set) = empty_set
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c47,plain,
( relation_image(X0,empty_set) = empty_set
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(hi40,axiom,
ifeq(relation(X0),true,relation_image(X0,empty_set),empty_set) = empty_set,
inference(equality_encoding,[status(esa)],[c47]) ).
cnf(t173,plain,
relation_image(set_intersection2(sk13,sk13),empty_set) = empty_set,
inference(hyper_resolution,[status(thm)],[hi40,h82]) ).
cnf(t15002,plain,
relation_image(sk13,empty_set) = empty_set,
inference(step,[status(thm)],[t173,t256]) ).
cnf(t839,plain,
relation_image(sk13,empty_set) = empty_set,
inference(orient,[status(thm)],[t15002]) ).
cnf(t15019,plain,
relation_image(sk13,sk2) = empty_set,
inference(step,[status(thm)],[t839,t876]) ).
cnf(t15020,plain,
relation_image(sk13,sk2) = sk2,
inference(step,[status(thm)],[t15019,t876]) ).
cnf(t885,plain,
relation_image(sk13,sk2) = sk2,
inference(rw,[status(thm)],[t15020]) ).
cnf(t15184,plain,
relation_image(sk13,sk5) = sk2,
inference(step,[status(thm)],[t885,t952]) ).
cnf(t15185,plain,
relation_image(sk13,sk5) = sk5,
inference(step,[status(thm)],[t15184,t952]) ).
cnf(t1142,plain,
relation_image(sk13,sk5) = sk5,
inference(orient,[status(thm)],[t15185]) ).
cnf(t16083,plain,
true = ifeq(sk5,sk5,false,true),
inference(step,[status(thm)],[t16082,t1142]) ).
cnf(t16084,plain,
true = false,
inference(step,[status(thm)],[t16083,t257]) ).
cnf(t14929,plain,
false = true,
inference(orient,[status(thm)],[t16084]) ).
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(f9,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f9_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c14,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
fof(f18,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f18_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
( relation(sk6)
& ~ empty(sk6) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk6])],[f18_nnf]) ).
cnf(c29,plain,
~ empty(sk6),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
fof(f20,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f20_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
~ empty(sk8),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk8])],[f20_nnf]) ).
cnf(c33,plain,
~ empty(sk8),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
fof(f33,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f33_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c54,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
fof(f35,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f35_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c56,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c14,c29,c33,c46,c54,c56]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t14929]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU056+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 12:37:53 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 74.97/10.91 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 74.97/10.91 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------