%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU293+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.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:37 PM UTC 2026
% Result : Theorem 18.01s 29.64s
% Output : Proof 18.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 14
% Syntax : Number of formulae : 107 ( 16 unt; 0 def)
% Number of atoms : 348 ( 67 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 384 ( 143 ~; 163 |; 55 &)
% ( 7 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-3 aty)
% Number of variables : 182 ( 8 sgn 109 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f42,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f42_nnf,plain,
! [A,B,C] :
( ( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [C,A,B] :
( ( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c81,plain,
( relation_of2(X2,X0,X1)
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
fof(f47,conjecture,
! [A,B,C,D] :
( ( relation_of2_as_subset(D,A,B)
& quasi_total(D,A,B)
& function(D) )
=> ( B != empty_set
=> ! [E] :
( in(E,relation_inverse_image(D,C))
<=> ( in(apply(D,E),C)
& in(E,A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t46_funct_2) ).
fof(f47_neg,negated_conjecture,
~ ! [A,B,C,D] :
( ( relation_of2_as_subset(D,A,B)
& quasi_total(D,A,B)
& function(D) )
=> ( B != empty_set
=> ! [E] :
( in(E,relation_inverse_image(D,C))
<=> ( in(apply(D,E),C)
& in(E,A) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f47]) ).
fof(f47_nnf,plain,
? [A,B,C,D] :
( ? [E] :
( ( in(apply(D,E),C)
& in(E,A)
& ~ in(E,relation_inverse_image(D,C)) )
| ( ( ~ in(apply(D,E),C)
| ~ in(E,A) )
& in(E,relation_inverse_image(D,C)) ) )
& B != empty_set
& relation_of2_as_subset(D,A,B)
& quasi_total(D,A,B)
& function(D) ),
inference(nnf_transformation,[status(thm)],[f47_neg]) ).
fof(f47_sk,plain,
( ( ( in(apply(sk21,sk22),sk20)
& in(sk22,sk18)
& ~ in(sk22,relation_inverse_image(sk21,sk20)) )
| ( ( ~ in(apply(sk21,sk22),sk20)
| ~ in(sk22,sk18) )
& in(sk22,relation_inverse_image(sk21,sk20)) ) )
& sk19 != empty_set
& relation_of2_as_subset(sk21,sk18,sk19)
& quasi_total(sk21,sk18,sk19)
& function(sk21) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk18,sk19,sk20,sk21,sk22])],[f47_nnf]) ).
cnf(c90,plain,
relation_of2_as_subset(sk21,sk18,sk19),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p393,plain,
relation_of2(sk21,sk18,sk19),
inference(resolution,[status(thm)],[c81,c90]) ).
fof(f41,axiom,
! [A,B,C] :
( relation_of2(C,A,B)
=> relation_dom_as_subset(A,B,C) = relation_dom(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_relset_1) ).
fof(f41_nnf,plain,
! [A,B,C] :
( relation_dom_as_subset(A,B,C) = relation_dom(C)
| ~ relation_of2(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [C,A,B] :
( relation_dom_as_subset(A,B,C) = relation_dom(C)
| ~ relation_of2(C,A,B) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c80,plain,
( relation_dom_as_subset(X0,X1,X2) = relation_dom(X2)
| ~ relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p396,plain,
relation_dom_as_subset(sk18,sk19,sk21) = relation_dom(sk21),
inference(resolution,[status(thm)],[p393,c80]) ).
fof(f6,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> ( ( B = empty_set
=> ( ( quasi_total(C,A,B)
<=> C = empty_set )
| A = empty_set ) )
& ( ( B = empty_set
=> A = empty_set )
=> ( quasi_total(C,A,B)
<=> A = relation_dom_as_subset(A,B,C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_funct_2) ).
fof(f6_nnf,plain,
! [A,B,C] :
( ( ( ( ( C != empty_set
| quasi_total(C,A,B) )
& ( C = empty_set
| ~ quasi_total(C,A,B) ) )
| A = empty_set
| B != empty_set )
& ( ( ( A != relation_dom_as_subset(A,B,C)
| quasi_total(C,A,B) )
& ( A = relation_dom_as_subset(A,B,C)
| ~ quasi_total(C,A,B) ) )
| ( A != empty_set
& B = empty_set ) ) )
| ~ relation_of2_as_subset(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [C,A,B] :
( ( ( ( ( C != empty_set
| quasi_total(C,A,B) )
& ( C = empty_set
| ~ quasi_total(C,A,B) ) )
| A = empty_set
| B != empty_set )
& ( ( ( A != relation_dom_as_subset(A,B,C)
| quasi_total(C,A,B) )
& ( A = relation_dom_as_subset(A,B,C)
| ~ quasi_total(C,A,B) ) )
| ( A != empty_set
& B = empty_set ) ) )
| ~ relation_of2_as_subset(C,A,B) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c16,plain,
( X0 = relation_dom_as_subset(X0,X1,X2)
| ~ quasi_total(X2,X0,X1)
| X1 = empty_set
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p214,plain,
( sk18 = relation_dom_as_subset(sk18,sk19,sk21)
| ~ quasi_total(sk21,sk18,sk19)
| sk19 = empty_set ),
inference(resolution,[status(thm)],[c16,c90]) ).
cnf(c89,plain,
quasi_total(sk21,sk18,sk19),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p216,plain,
( sk18 = relation_dom_as_subset(sk18,sk19,sk21)
| sk19 = empty_set ),
inference(resolution,[status(thm)],[p214,c89]) ).
cnf(p397,plain,
( sk18 = relation_dom(sk21)
| sk19 = empty_set ),
inference(demodulation,[status(thm)],[p396,p216]) ).
fof(f16,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> element(C,powerset(cartesian_product2(A,B))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f16_nnf,plain,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
| ~ relation_of2_as_subset(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [C,A,B] :
( element(C,powerset(cartesian_product2(A,B)))
| ~ relation_of2_as_subset(C,A,B) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c31,plain,
( element(X2,powerset(cartesian_product2(X0,X1)))
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p313,plain,
element(sk21,powerset(cartesian_product2(sk18,sk19))),
inference(resolution,[status(thm)],[c31,c90]) ).
fof(f3,axiom,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
=> relation(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f3_nnf,plain,
! [A,B,C] :
( relation(C)
| ~ element(C,powerset(cartesian_product2(A,B))) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [C,A,B] :
( relation(C)
| ~ element(C,powerset(cartesian_product2(A,B))) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( relation(X2)
| ~ element(X2,powerset(cartesian_product2(X0,X1))) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p315,plain,
relation(sk21),
inference(resolution,[status(thm)],[p313,c3]) ).
fof(f5,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B,C] :
( C = relation_inverse_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(apply(A,D),B)
& in(D,relation_dom(A)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d13_funct_1) ).
fof(f5_nnf,plain,
! [A] :
( ! [B,C] :
( ( ? [D] :
( ( in(apply(A,D),B)
& in(D,relation_dom(A))
& ~ in(D,C) )
| ( ( ~ in(apply(A,D),B)
| ~ in(D,relation_dom(A)) )
& in(D,C) ) )
| C = relation_inverse_image(A,B) )
& ( ! [D] :
( ( ~ in(apply(A,D),B)
| ~ in(D,relation_dom(A))
| in(D,C) )
& ( ( in(apply(A,D),B)
& in(D,relation_dom(A)) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ function(A)
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,C,B,D] :
( ( ( ( in(apply(A,sk0(A,B,C)),B)
& in(sk0(A,B,C),relation_dom(A))
& ~ in(sk0(A,B,C),C) )
| ( ( ~ in(apply(A,sk0(A,B,C)),B)
| ~ in(sk0(A,B,C),relation_dom(A)) )
& in(sk0(A,B,C),C) )
| C = relation_inverse_image(A,B) )
& ( ( ( ~ in(apply(A,D),B)
| ~ in(D,relation_dom(A))
| in(D,C) )
& ( ( in(apply(A,D),B)
& in(D,relation_dom(A)) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f5_nnf]) ).
cnf(c9,plain,
( ~ in(apply(X0,X3),X1)
| ~ in(X3,relation_dom(X0))
| in(X3,X2)
| X2 != relation_inverse_image(X0,X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p319,plain,
( ~ in(apply(sk21,X2),X1)
| ~ in(X2,relation_dom(sk21))
| in(X2,X0)
| X0 != relation_inverse_image(sk21,X1)
| ~ function(sk21) ),
inference(resolution,[status(thm)],[p315,c9]) ).
cnf(p349,plain,
( ~ in(apply(sk21,X0),X1)
| ~ in(X0,relation_dom(sk21))
| in(X0,relation_inverse_image(sk21,X1))
| ~ function(sk21) ),
inference(equality_resolution,[status(thm)],[p319]) ).
cnf(c88,plain,
function(sk21),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p351,plain,
( ~ in(apply(sk21,X0),X1)
| ~ in(X0,relation_dom(sk21))
| in(X0,relation_inverse_image(sk21,X1)) ),
inference(resolution,[status(thm)],[p349,c88]) ).
cnf(p403,plain,
( ~ in(apply(sk21,X0),X1)
| ~ in(X0,sk18)
| in(X0,relation_inverse_image(sk21,X1))
| sk19 = empty_set ),
inference(superposition,[status(thm)],[p397,p351]) ).
fof(f48,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f48_nnf,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c98,plain,
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(c7,plain,
( in(X3,relation_dom(X0))
| ~ in(X3,X2)
| X2 != relation_inverse_image(X0,X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p317,plain,
( in(X2,relation_dom(sk21))
| ~ in(X2,X0)
| X0 != relation_inverse_image(sk21,X1)
| ~ function(sk21) ),
inference(resolution,[status(thm)],[p315,c7]) ).
cnf(p323,plain,
( in(X0,relation_dom(sk21))
| ~ in(X0,relation_inverse_image(sk21,X1))
| ~ function(sk21) ),
inference(equality_resolution,[status(thm)],[p317]) ).
cnf(p326,plain,
( in(X0,relation_dom(sk21))
| ~ in(X0,relation_inverse_image(sk21,X1)) ),
inference(resolution,[status(thm)],[p323,c88]) ).
cnf(c93,plain,
( in(sk22,sk18)
| in(sk22,relation_inverse_image(sk21,sk20)) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p327,plain,
( in(sk22,sk18)
| in(sk22,relation_dom(sk21)) ),
inference(resolution,[status(thm)],[p326,c93]) ).
cnf(p455,plain,
( in(sk22,sk18)
| element(sk22,X0)
| ~ element(relation_dom(sk21),powerset(X0)) ),
inference(resolution,[status(thm)],[c98,p327]) ).
fof(f13,axiom,
! [A,B,C] :
( relation_of2(C,A,B)
=> element(relation_dom_as_subset(A,B,C),powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_relset_1) ).
fof(f13_nnf,plain,
! [A,B,C] :
( element(relation_dom_as_subset(A,B,C),powerset(A))
| ~ relation_of2(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [C,A,B] :
( element(relation_dom_as_subset(A,B,C),powerset(A))
| ~ relation_of2(C,A,B) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c28,plain,
( element(relation_dom_as_subset(X0,X1,X2),powerset(X0))
| ~ relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p395,plain,
element(relation_dom_as_subset(sk18,sk19,sk21),powerset(sk18)),
inference(resolution,[status(thm)],[p393,c28]) ).
cnf(p399,plain,
element(relation_dom(sk21),powerset(sk18)),
inference(demodulation,[status(thm)],[p396,p395]) ).
cnf(p471,plain,
( in(sk22,sk18)
| element(sk22,sk18) ),
inference(resolution,[status(thm)],[p455,p399]) ).
fof(f45,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f45_nnf,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c85,plain,
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p472,plain,
( in(sk22,sk18)
| empty(sk18)
| in(sk22,sk18) ),
inference(resolution,[status(thm)],[p471,c85]) ).
cnf(p473,plain,
( empty(sk18)
| in(sk22,sk18) ),
inference(factoring,[status(thm)],[p472]) ).
cnf(p878,plain,
( empty(sk18)
| ~ in(apply(sk21,sk22),X0)
| in(sk22,relation_inverse_image(sk21,X0))
| sk19 = empty_set ),
inference(resolution,[status(thm)],[p403,p473]) ).
cnf(c94,plain,
( in(apply(sk21,sk22),sk20)
| in(sk22,relation_inverse_image(sk21,sk20)) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p885,plain,
( in(sk22,relation_inverse_image(sk21,sk20))
| empty(sk18)
| in(sk22,relation_inverse_image(sk21,sk20))
| sk19 = empty_set ),
inference(resolution,[status(thm)],[p878,c94]) ).
cnf(p886,plain,
( empty(sk18)
| in(sk22,relation_inverse_image(sk21,sk20))
| sk19 = empty_set ),
inference(factoring,[status(thm)],[p885]) ).
cnf(c8,plain,
( in(apply(X0,X3),X1)
| ~ in(X3,X2)
| X2 != relation_inverse_image(X0,X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p318,plain,
( in(apply(sk21,X2),X1)
| ~ in(X2,X0)
| X0 != relation_inverse_image(sk21,X1)
| ~ function(sk21) ),
inference(resolution,[status(thm)],[p315,c8]) ).
cnf(p337,plain,
( in(apply(sk21,X0),X1)
| ~ in(X0,relation_inverse_image(sk21,X1))
| ~ function(sk21) ),
inference(equality_resolution,[status(thm)],[p318]) ).
cnf(p339,plain,
( in(apply(sk21,X0),X1)
| ~ in(X0,relation_inverse_image(sk21,X1)) ),
inference(resolution,[status(thm)],[p337,c88]) ).
cnf(p899,plain,
( in(apply(sk21,sk22),sk20)
| empty(sk18)
| sk19 = empty_set ),
inference(resolution,[status(thm)],[p886,p339]) ).
cnf(c95,plain,
( ~ in(sk22,relation_inverse_image(sk21,sk20))
| ~ in(apply(sk21,sk22),sk20)
| ~ in(sk22,sk18) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p491,plain,
( ~ in(sk22,relation_inverse_image(sk21,sk20))
| ~ in(apply(sk21,sk22),sk20)
| empty(sk18) ),
inference(resolution,[status(thm)],[p473,c95]) ).
cnf(p915,plain,
( ~ in(sk22,relation_inverse_image(sk21,sk20))
| empty(sk18)
| empty(sk18)
| sk19 = empty_set ),
inference(resolution,[status(thm)],[p899,p491]) ).
cnf(p918,plain,
( ~ in(sk22,relation_inverse_image(sk21,sk20))
| empty(sk18)
| sk19 = empty_set ),
inference(factoring,[status(thm)],[p915]) ).
cnf(p919,plain,
( empty(sk18)
| sk19 = empty_set
| empty(sk18)
| sk19 = empty_set ),
inference(resolution,[status(thm)],[p918,p886]) ).
cnf(p920,plain,
( empty(sk18)
| empty(sk18)
| sk19 = empty_set ),
inference(factoring,[status(thm)],[p919]) ).
cnf(p922,plain,
( empty(sk18)
| sk19 = empty_set ),
inference(factoring,[status(thm)],[p920]) ).
cnf(c91,plain,
sk19 != empty_set,
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p923,plain,
empty(sk18),
inference(resolution,[status(thm)],[p922,c91]) ).
fof(f50,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
fof(f50_nnf,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c100,plain,
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(p928,plain,
sk18 = empty_set,
inference(resolution,[status(thm)],[p923,c100]) ).
fof(f49,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f49_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c99,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(p476,plain,
( in(sk22,sk18)
| ~ empty(X0)
| ~ element(relation_dom(sk21),powerset(X0)) ),
inference(resolution,[status(thm)],[c99,p327]) ).
cnf(p525,plain,
( in(sk22,sk18)
| ~ empty(sk18) ),
inference(resolution,[status(thm)],[p476,p399]) ).
cnf(p985,plain,
( in(sk22,empty_set)
| ~ empty(empty_set) ),
inference(demodulation,[status(thm)],[p928,p525]) ).
fof(f20,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc12_relat_1) ).
fof(f20_nnf,plain,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c35,plain,
empty(empty_set),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p1048,plain,
in(sk22,empty_set),
inference(resolution,[status(thm)],[p985,c35]) ).
fof(f51,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f51_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c101,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(p1053,plain,
~ empty(empty_set),
inference(resolution,[status(thm)],[p1048,c101]) ).
cnf(p1057,plain,
$false,
inference(resolution,[status(thm)],[p1053,c35]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU293+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/27.34 % CPULimit : 300
% 0.06/27.34 % WCLimit : 300
% 0.06/27.34 % DateTime : Thu Sep 24 13:34:35 UTC 2026
% 0.06/27.34 % CPUTime :
% 0.06/27.34 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 18.01/29.64 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.01/29.64 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------