%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU363+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.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:51 PM UTC 2026
% Result : Theorem 163.61s 24.22s
% Output : Proof 163.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 9
% Syntax : Number of formulae : 70 ( 23 unt; 0 def)
% Number of atoms : 215 ( 14 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 222 ( 77 ~; 72 |; 46 &)
% ( 3 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 118 ( 2 sgn 75 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f33,axiom,
! [A,B] :
( relation(A)
=> relation_restriction_as_relation_of(A,B) = relation_restriction(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k1_toler_1) ).
fof(f33_nnf,plain,
! [A,B] :
( relation_restriction_as_relation_of(A,B) = relation_restriction(A,B)
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [A,B] :
( relation_restriction_as_relation_of(A,B) = relation_restriction(A,B)
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c40,plain,
( relation_restriction_as_relation_of(X0,X1) = relation_restriction(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
fof(f18,axiom,
! [A] :
( rel_str(A)
=> relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u1_orders_2) ).
fof(f18_nnf,plain,
! [A] :
( relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A))
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [A] :
( relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A))
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c20,plain,
( relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
fof(f43,conjecture,
! [A] :
( rel_str(A)
=> ! [B] :
( ( subrelstr(B,A)
& full_subrelstr(B,A) )
=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(B))
=> ( ( in(F,the_carrier(B))
& in(E,the_carrier(B))
& related(A,C,D)
& F = D
& E = C )
=> related(B,E,F) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t61_yellow_0) ).
fof(f43_neg,negated_conjecture,
~ ! [A] :
( rel_str(A)
=> ! [B] :
( ( subrelstr(B,A)
& full_subrelstr(B,A) )
=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(B))
=> ( ( in(F,the_carrier(B))
& in(E,the_carrier(B))
& related(A,C,D)
& F = D
& E = C )
=> related(B,E,F) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f43]) ).
fof(f43_nnf,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ? [F] :
( ~ related(B,E,F)
& in(F,the_carrier(B))
& in(E,the_carrier(B))
& related(A,C,D)
& F = D
& E = C
& element(F,the_carrier(B)) )
& element(E,the_carrier(B)) )
& element(D,the_carrier(A)) )
& element(C,the_carrier(A)) )
& subrelstr(B,A)
& full_subrelstr(B,A) )
& rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f43_neg]) ).
fof(f43_sk,plain,
( ~ related(sk12,sk15,sk16)
& in(sk16,the_carrier(sk12))
& in(sk15,the_carrier(sk12))
& related(sk11,sk13,sk14)
& sk16 = sk14
& sk15 = sk13
& element(sk16,the_carrier(sk12))
& element(sk15,the_carrier(sk12))
& element(sk14,the_carrier(sk11))
& element(sk13,the_carrier(sk11))
& subrelstr(sk12,sk11)
& full_subrelstr(sk12,sk11)
& rel_str(sk11) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk11,sk12,sk13,sk14,sk15,sk16])],[f43_nnf]) ).
cnf(c56,plain,
rel_str(sk11),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p118,plain,
relation_of2_as_subset(the_InternalRel(sk11),the_carrier(sk11),the_carrier(sk11)),
inference(resolution,[status(thm)],[c20,c56]) ).
fof(f17,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> element(C,powerset(cartesian_product2(A,B))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f17_nnf,plain,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
| ~ relation_of2_as_subset(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [C,A,B] :
( element(C,powerset(cartesian_product2(A,B)))
| ~ relation_of2_as_subset(C,A,B) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c19,plain,
( element(X2,powerset(cartesian_product2(X0,X1)))
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p124,plain,
element(the_InternalRel(sk11),powerset(cartesian_product2(the_carrier(sk11),the_carrier(sk11)))),
inference(resolution,[status(thm)],[p118,c19]) ).
fof(f2,axiom,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
=> relation(C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f2_nnf,plain,
! [A,B,C] :
( relation(C)
| ~ element(C,powerset(cartesian_product2(A,B))) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [C,A,B] :
( relation(C)
| ~ element(C,powerset(cartesian_product2(A,B))) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( relation(X2)
| ~ element(X2,powerset(cartesian_product2(X0,X1))) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p126,plain,
relation(the_InternalRel(sk11)),
inference(resolution,[status(thm)],[p124,c2]) ).
cnf(p274,plain,
relation_restriction_as_relation_of(the_InternalRel(sk11),X0) = relation_restriction(the_InternalRel(sk11),X0),
inference(resolution,[status(thm)],[c40,p126]) ).
fof(f37,axiom,
! [A,B,C] :
( relation(C)
=> ( in(A,relation_restriction(C,B))
<=> ( in(A,cartesian_product2(B,B))
& in(A,C) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t16_wellord1) ).
fof(f37_nnf,plain,
! [A,B,C] :
( ( ( ~ in(A,cartesian_product2(B,B))
| ~ in(A,C)
| in(A,relation_restriction(C,B)) )
& ( ( in(A,cartesian_product2(B,B))
& in(A,C) )
| ~ in(A,relation_restriction(C,B)) ) )
| ~ relation(C) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [C,A,B] :
( ( ( ~ in(A,cartesian_product2(B,B))
| ~ in(A,C)
| in(A,relation_restriction(C,B)) )
& ( ( in(A,cartesian_product2(B,B))
& in(A,C) )
| ~ in(A,relation_restriction(C,B)) ) )
| ~ relation(C) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c49,plain,
( ~ in(X0,cartesian_product2(X1,X1))
| ~ in(X0,X2)
| in(X0,relation_restriction(X2,X1))
| ~ relation(X2) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p415,plain,
( ~ in(X0,cartesian_product2(X1,X1))
| ~ in(X0,the_InternalRel(sk11))
| in(X0,relation_restriction(the_InternalRel(sk11),X1)) ),
inference(resolution,[status(thm)],[c49,p126]) ).
fof(f5,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( related(A,B,C)
<=> in(ordered_pair(B,C),the_InternalRel(A)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_orders_2) ).
fof(f5_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ in(ordered_pair(B,C),the_InternalRel(A))
| related(A,B,C) )
& ( in(ordered_pair(B,C),the_InternalRel(A))
| ~ related(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ element(B,the_carrier(A)) )
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,B,C] :
( ( ( ~ in(ordered_pair(B,C),the_InternalRel(A))
| related(A,B,C) )
& ( in(ordered_pair(B,C),the_InternalRel(A))
| ~ related(A,B,C) ) )
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c6,plain,
( in(ordered_pair(X1,X2),the_InternalRel(X0))
| ~ related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p84,plain,
( in(ordered_pair(X0,X1),the_InternalRel(sk11))
| ~ related(sk11,X0,X1)
| ~ element(X1,the_carrier(sk11))
| ~ element(X0,the_carrier(sk11)) ),
inference(resolution,[status(thm)],[c6,c56]) ).
cnf(c59,plain,
element(sk13,the_carrier(sk11)),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p93,plain,
( in(ordered_pair(sk13,X0),the_InternalRel(sk11))
| ~ related(sk11,sk13,X0)
| ~ element(X0,the_carrier(sk11)) ),
inference(resolution,[status(thm)],[p84,c59]) ).
cnf(c60,plain,
element(sk14,the_carrier(sk11)),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p97,plain,
( in(ordered_pair(sk13,sk14),the_InternalRel(sk11))
| ~ related(sk11,sk13,sk14) ),
inference(resolution,[status(thm)],[p93,c60]) ).
cnf(c65,plain,
related(sk11,sk13,sk14),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p98,plain,
in(ordered_pair(sk13,sk14),the_InternalRel(sk11)),
inference(resolution,[status(thm)],[p97,c65]) ).
cnf(p2297,plain,
( ~ in(ordered_pair(sk13,sk14),cartesian_product2(X0,X0))
| in(ordered_pair(sk13,sk14),relation_restriction(the_InternalRel(sk11),X0)) ),
inference(resolution,[status(thm)],[p415,p98]) ).
fof(f36,axiom,
! [A,B,C,D] :
( in(ordered_pair(A,B),cartesian_product2(C,D))
<=> ( in(B,D)
& in(A,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t106_zfmisc_1) ).
fof(f36_nnf,plain,
! [A,B,C,D] :
( ( ~ in(B,D)
| ~ in(A,C)
| in(ordered_pair(A,B),cartesian_product2(C,D)) )
& ( ( in(B,D)
& in(A,C) )
| ~ in(ordered_pair(A,B),cartesian_product2(C,D)) ) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [A,B,C,D] :
( ( ~ in(B,D)
| ~ in(A,C)
| in(ordered_pair(A,B),cartesian_product2(C,D)) )
& ( ( in(B,D)
& in(A,C) )
| ~ in(ordered_pair(A,B),cartesian_product2(C,D)) ) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c46,plain,
( ~ in(X1,X3)
| ~ in(X0,X2)
| in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(c66,plain,
in(sk15,the_carrier(sk12)),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p334,plain,
( ~ in(X0,X1)
| in(ordered_pair(sk13,X0),cartesian_product2(the_carrier(sk12),X1)) ),
inference(resolution,[status(thm)],[c46,c66]) ).
cnf(c67,plain,
in(sk16,the_carrier(sk12)),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p664,plain,
in(ordered_pair(sk13,sk14),cartesian_product2(the_carrier(sk12),the_carrier(sk12))),
inference(resolution,[status(thm)],[p334,c67]) ).
cnf(p7338,plain,
in(ordered_pair(sk13,sk14),relation_restriction(the_InternalRel(sk11),the_carrier(sk12))),
inference(resolution,[status(thm)],[p2297,p664]) ).
cnf(p7347,plain,
in(ordered_pair(sk13,sk14),the_InternalRel(sk12)),
inference(superposition,[status(thm)],[p274,p7338]) ).
fof(f16,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( subrelstr(B,A)
=> rel_str(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_yellow_0) ).
fof(f16_nnf,plain,
! [A] :
( ! [B] :
( rel_str(B)
| ~ subrelstr(B,A) )
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [A,B] :
( rel_str(B)
| ~ subrelstr(B,A)
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c18,plain,
( rel_str(X1)
| ~ subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p108,plain,
( rel_str(X0)
| ~ subrelstr(X0,sk11) ),
inference(resolution,[status(thm)],[c18,c56]) ).
cnf(c58,plain,
subrelstr(sk12,sk11),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p110,plain,
rel_str(sk12),
inference(resolution,[status(thm)],[p108,c58]) ).
cnf(c7,plain,
( ~ in(ordered_pair(X1,X2),the_InternalRel(X0))
| related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p114,plain,
( ~ in(ordered_pair(X0,X1),the_InternalRel(sk12))
| related(sk12,X0,X1)
| ~ element(X1,the_carrier(sk12))
| ~ element(X0,the_carrier(sk12)) ),
inference(resolution,[status(thm)],[p110,c7]) ).
cnf(c61,plain,
element(sk15,the_carrier(sk12)),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p647,plain,
( ~ in(ordered_pair(sk13,X0),the_InternalRel(sk12))
| related(sk12,sk13,X0)
| ~ element(X0,the_carrier(sk12)) ),
inference(resolution,[status(thm)],[p114,c61]) ).
cnf(c62,plain,
element(sk16,the_carrier(sk12)),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p4514,plain,
( ~ in(ordered_pair(sk13,sk14),the_InternalRel(sk12))
| related(sk12,sk13,sk14) ),
inference(resolution,[status(thm)],[p647,c62]) ).
cnf(p7380,plain,
related(sk12,sk13,sk14),
inference(resolution,[status(thm)],[p7347,p4514]) ).
cnf(c63,plain,
sk15 = sk13,
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(c68,plain,
~ related(sk12,sk15,sk16),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p85,plain,
~ related(sk12,sk13,sk14),
inference(superposition,[status(thm)],[c63,c68]) ).
cnf(p7387,plain,
$false,
inference(resolution,[status(thm)],[p7380,p85]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU363+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n009.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 13:50:59 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 163.61/24.22 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 163.61/24.22 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------