%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU290+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 : n019.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:36 PM UTC 2026
% Result : Theorem 22.55s 3.75s
% Output : Proof 22.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 7
% Syntax : Number of formulae : 50 ( 13 unt; 0 def)
% Number of atoms : 182 ( 63 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 205 ( 73 ~; 76 |; 39 &)
% ( 5 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 5 con; 0-3 aty)
% Number of variables : 100 ( 2 sgn 65 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f44,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(f44_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)],[f44]) ).
fof(f44_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)],[f44_nnf]) ).
cnf(c84,plain,
( relation_of2(X2,X0,X1)
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
fof(f52,conjecture,
! [A,B,C,D] :
( ( relation_of2_as_subset(D,A,B)
& quasi_total(D,A,B)
& function(D) )
=> ( in(C,A)
=> ( in(apply(D,C),relation_rng(D))
| B = empty_set ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_funct_2) ).
fof(f52_neg,negated_conjecture,
~ ! [A,B,C,D] :
( ( relation_of2_as_subset(D,A,B)
& quasi_total(D,A,B)
& function(D) )
=> ( in(C,A)
=> ( in(apply(D,C),relation_rng(D))
| B = empty_set ) ) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f52_nnf,plain,
? [A,B,C,D] :
( ~ in(apply(D,C),relation_rng(D))
& B != empty_set
& in(C,A)
& relation_of2_as_subset(D,A,B)
& quasi_total(D,A,B)
& function(D) ),
inference(nnf_transformation,[status(thm)],[f52_neg]) ).
fof(f52_sk,plain,
( ~ in(apply(sk23,sk22),relation_rng(sk23))
& sk21 != empty_set
& in(sk22,sk20)
& relation_of2_as_subset(sk23,sk20,sk21)
& quasi_total(sk23,sk20,sk21)
& function(sk23) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk20,sk21,sk22,sk23])],[f52_nnf]) ).
cnf(c96,plain,
relation_of2_as_subset(sk23,sk20,sk21),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p530,plain,
relation_of2(sk23,sk20,sk21),
inference(resolution,[status(thm)],[c84,c96]) ).
fof(f43,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(f43_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)],[f43]) ).
fof(f43_sk,plain,
! [C,A,B] :
( relation_dom_as_subset(A,B,C) = relation_dom(C)
| ~ relation_of2(C,A,B) ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c83,plain,
( relation_dom_as_subset(X0,X1,X2) = relation_dom(X2)
| ~ relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p533,plain,
relation_dom_as_subset(sk20,sk21,sk23) = relation_dom(sk23),
inference(resolution,[status(thm)],[p530,c83]) ).
fof(f5,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(f5_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)],[f5]) ).
fof(f5_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)],[f5_nnf]) ).
cnf(c7,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)],[f5_sk]) ).
cnf(p114,plain,
( sk20 = relation_dom_as_subset(sk20,sk21,sk23)
| ~ quasi_total(sk23,sk20,sk21)
| sk21 = empty_set ),
inference(resolution,[status(thm)],[c7,c96]) ).
cnf(c95,plain,
quasi_total(sk23,sk20,sk21),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p115,plain,
( sk20 = relation_dom_as_subset(sk20,sk21,sk23)
| sk21 = empty_set ),
inference(resolution,[status(thm)],[p114,c95]) ).
cnf(p534,plain,
( sk20 = relation_dom(sk23)
| sk21 = empty_set ),
inference(demodulation,[status(thm)],[p533,p115]) ).
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(p369,plain,
element(sk23,powerset(cartesian_product2(sk20,sk21))),
inference(resolution,[status(thm)],[c31,c96]) ).
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(p371,plain,
relation(sk23),
inference(resolution,[status(thm)],[p369,c3]) ).
fof(f6,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_funct_1) ).
fof(f6_nnf,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) )
& ~ in(C,B) )
| ( ! [D] :
( C != apply(A,D)
| ~ in(D,relation_dom(A)) )
& in(C,B) ) )
| B = relation_rng(A) )
& ( ! [C] :
( ( ! [D] :
( C != apply(A,D)
| ~ in(D,relation_dom(A)) )
| in(C,B) )
& ( ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) )
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B,C,D] :
( ( ( ( sk1(A,B) = apply(A,sk2(A,B))
& in(sk2(A,B),relation_dom(A))
& ~ in(sk1(A,B),B) )
| ( ( sk1(A,B) != apply(A,D)
| ~ in(D,relation_dom(A)) )
& in(sk1(A,B),B) )
| B = relation_rng(A) )
& ( ( ( C != apply(A,D)
| ~ in(D,relation_dom(A))
| in(C,B) )
& ( ( C = apply(A,sk0(A,B,C))
& in(sk0(A,B,C),relation_dom(A)) )
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f6_nnf]) ).
cnf(c15,plain,
( X2 != apply(X0,X3)
| ~ in(X3,relation_dom(X0))
| in(X2,X1)
| X1 != relation_rng(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p375,plain,
( X1 != apply(sk23,X2)
| ~ in(X2,relation_dom(sk23))
| in(X1,X0)
| X0 != relation_rng(sk23)
| ~ function(sk23) ),
inference(resolution,[status(thm)],[p371,c15]) ).
cnf(p413,plain,
( X0 != apply(sk23,X1)
| ~ in(X1,relation_dom(sk23))
| in(X0,relation_rng(sk23))
| ~ function(sk23) ),
inference(equality_resolution,[status(thm)],[p375]) ).
cnf(p416,plain,
( ~ in(X0,relation_dom(sk23))
| in(apply(sk23,X0),relation_rng(sk23))
| ~ function(sk23) ),
inference(equality_resolution,[status(thm)],[p413]) ).
cnf(c94,plain,
function(sk23),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p418,plain,
( ~ in(X0,relation_dom(sk23))
| in(apply(sk23,X0),relation_rng(sk23)) ),
inference(resolution,[status(thm)],[p416,c94]) ).
cnf(p540,plain,
( ~ in(X0,sk20)
| in(apply(sk23,X0),relation_rng(sk23))
| sk21 = empty_set ),
inference(superposition,[status(thm)],[p534,p418]) ).
cnf(c97,plain,
in(sk22,sk20),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p574,plain,
( in(apply(sk23,sk22),relation_rng(sk23))
| sk21 = empty_set ),
inference(resolution,[status(thm)],[p540,c97]) ).
cnf(c99,plain,
~ in(apply(sk23,sk22),relation_rng(sk23)),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p580,plain,
sk21 = empty_set,
inference(resolution,[status(thm)],[p574,c99]) ).
cnf(c98,plain,
sk21 != empty_set,
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p583,plain,
empty_set != empty_set,
inference(demodulation,[status(thm)],[p580,c98]) ).
cnf(p592,plain,
$false,
inference(equality_resolution,[status(thm)],[p583]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU290+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.17/0.43 % Computer : n019.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Thu Sep 24 13:33:49 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 22.55/3.75 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.55/3.75 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------