%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU238+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 : n014.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:27 PM UTC 2026
% Result : Theorem 73.79s 11.63s
% Output : Proof 73.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 9
% Syntax : Number of formulae : 78 ( 12 unt; 0 def)
% Number of atoms : 260 ( 26 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 293 ( 111 ~; 122 |; 41 &)
% ( 4 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-1 aty)
% Number of variables : 78 ( 0 sgn 48 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f52,axiom,
! [A] :
( ordinal(A)
=> ( being_limit_ordinal(A)
<=> ! [B] :
( ordinal(B)
=> ( in(B,A)
=> in(succ(B),A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t41_ordinal1) ).
fof(f52_nnf,plain,
! [A] :
( ( ( ? [B] :
( ~ in(succ(B),A)
& in(B,A)
& ordinal(B) )
| being_limit_ordinal(A) )
& ( ! [B] :
( in(succ(B),A)
| ~ in(B,A)
| ~ ordinal(B) )
| ~ being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
! [A,B] :
( ( ( ( ~ in(succ(sk13(A)),A)
& in(sk13(A),A)
& ordinal(sk13(A)) )
| being_limit_ordinal(A) )
& ( in(succ(B),A)
| ~ in(B,A)
| ~ ordinal(B)
| ~ being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk13])],[f52_nnf]) ).
cnf(c97,plain,
( ordinal(sk13(X0))
| being_limit_ordinal(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
fof(f53,conjecture,
! [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/sandbox2/benchmark/theBenchmark.p',t42_ordinal1) ).
fof(f53_neg,negated_conjecture,
~ ! [A] :
( ordinal(A)
=> ( ~ ( being_limit_ordinal(A)
& ? [B] :
( A = succ(B)
& ordinal(B) ) )
& ~ ( ! [B] :
( ordinal(B)
=> A != succ(B) )
& ~ being_limit_ordinal(A) ) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f53_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)],[f53_neg]) ).
fof(f53_sk,plain,
! [B] :
( ( ( being_limit_ordinal(sk14)
& sk14 = succ(sk15)
& ordinal(sk15) )
| ( ( sk14 != succ(B)
| ~ ordinal(B) )
& ~ being_limit_ordinal(sk14) ) )
& ordinal(sk14) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk14,sk15])],[f53_nnf]) ).
cnf(c100,plain,
ordinal(sk14),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(p436,plain,
( ordinal(sk13(sk14))
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[c97,c100]) ).
fof(f25,axiom,
! [A] :
( ordinal(A)
=> ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_ordinal1) ).
fof(f25_nnf,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c44,plain,
( ordinal(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p460,plain,
( ordinal(succ(sk13(sk14)))
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[p436,c44]) ).
fof(f42,axiom,
! [A,B] :
( ( ordinal(B)
& ordinal(A) )
=> ( ordinal_subset(A,B)
<=> subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r1_ordinal1) ).
fof(f42_nnf,plain,
! [A,B] :
( ( ( ~ subset(A,B)
| ordinal_subset(A,B) )
& ( subset(A,B)
| ~ ordinal_subset(A,B) ) )
| ~ ordinal(B)
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [A,B] :
( ( ( ~ subset(A,B)
| ordinal_subset(A,B) )
& ( subset(A,B)
| ~ ordinal_subset(A,B) ) )
| ~ ordinal(B)
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c83,plain,
( subset(X0,X1)
| ~ ordinal_subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p496,plain,
( subset(succ(sk13(sk14)),X0)
| ~ ordinal_subset(succ(sk13(sk14)),X0)
| ~ ordinal(X0)
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[p460,c83]) ).
cnf(p5517,plain,
( subset(succ(sk13(sk14)),sk14)
| ~ ordinal_subset(succ(sk13(sk14)),sk14)
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[p496,c100]) ).
fof(f50,axiom,
! [A] :
( ordinal(A)
=> ! [B] :
( ordinal(B)
=> ( in(A,B)
<=> ordinal_subset(succ(A),B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_ordinal1) ).
fof(f50_nnf,plain,
! [A] :
( ! [B] :
( ( ( ~ ordinal_subset(succ(A),B)
| in(A,B) )
& ( ordinal_subset(succ(A),B)
| ~ in(A,B) ) )
| ~ ordinal(B) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
! [A,B] :
( ( ( ~ ordinal_subset(succ(A),B)
| in(A,B) )
& ( ordinal_subset(succ(A),B)
| ~ in(A,B) ) )
| ~ ordinal(B)
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c92,plain,
( ordinal_subset(succ(X0),X1)
| ~ in(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(p466,plain,
( ordinal_subset(succ(sk13(sk14)),X0)
| ~ in(sk13(sk14),X0)
| ~ ordinal(X0)
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[p436,c92]) ).
cnf(p5128,plain,
( ordinal_subset(succ(sk13(sk14)),sk14)
| ~ in(sk13(sk14),sk14)
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[p466,c100]) ).
cnf(c98,plain,
( in(sk13(X0),X0)
| being_limit_ordinal(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p472,plain,
( in(sk13(sk14),sk14)
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[c98,c100]) ).
cnf(p5222,plain,
( being_limit_ordinal(sk14)
| ordinal_subset(succ(sk13(sk14)),sk14)
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[p5128,p472]) ).
cnf(p5223,plain,
( ordinal_subset(succ(sk13(sk14)),sk14)
| being_limit_ordinal(sk14) ),
inference(factoring,[status(thm)],[p5222]) ).
cnf(p6733,plain,
( being_limit_ordinal(sk14)
| subset(succ(sk13(sk14)),sk14)
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[p5517,p5223]) ).
cnf(p6734,plain,
( subset(succ(sk13(sk14)),sk14)
| being_limit_ordinal(sk14) ),
inference(factoring,[status(thm)],[p6733]) ).
fof(f11,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f11_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)],[f11]) ).
fof(f11_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)],[f11_nnf]) ).
cnf(c18,plain,
( X0 = X1
| ~ subset(X0,X1)
| proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p6791,plain,
( succ(sk13(sk14)) = sk14
| proper_subset(succ(sk13(sk14)),sk14)
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[p6734,c18]) ).
cnf(c42,plain,
( epsilon_transitive(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p458,plain,
( epsilon_transitive(succ(sk13(sk14)))
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[p436,c42]) ).
fof(f48,axiom,
! [A] :
( epsilon_transitive(A)
=> ! [B] :
( ordinal(B)
=> ( proper_subset(A,B)
=> in(A,B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_ordinal1) ).
fof(f48_nnf,plain,
! [A] :
( ! [B] :
( in(A,B)
| ~ proper_subset(A,B)
| ~ ordinal(B) )
| ~ epsilon_transitive(A) ),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
! [A,B] :
( in(A,B)
| ~ proper_subset(A,B)
| ~ ordinal(B)
| ~ epsilon_transitive(A) ),
inference(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c90,plain,
( in(X0,X1)
| ~ proper_subset(X0,X1)
| ~ ordinal(X1)
| ~ epsilon_transitive(X0) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(p471,plain,
( in(succ(sk13(sk14)),X0)
| ~ proper_subset(succ(sk13(sk14)),X0)
| ~ ordinal(X0)
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[p458,c90]) ).
cnf(p5271,plain,
( in(succ(sk13(sk14)),sk14)
| ~ proper_subset(succ(sk13(sk14)),sk14)
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[p471,c100]) ).
cnf(p7830,plain,
( in(succ(sk13(sk14)),sk14)
| being_limit_ordinal(sk14)
| succ(sk13(sk14)) = sk14
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[p6791,p5271]) ).
cnf(p17350,plain,
( in(succ(sk13(sk14)),sk14)
| succ(sk13(sk14)) = sk14
| being_limit_ordinal(sk14) ),
inference(factoring,[status(thm)],[p7830]) ).
cnf(c99,plain,
( ~ in(succ(sk13(X0)),X0)
| being_limit_ordinal(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p508,plain,
( ~ in(succ(sk13(sk14)),sk14)
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[c99,c100]) ).
cnf(p17354,plain,
( being_limit_ordinal(sk14)
| succ(sk13(sk14)) = sk14
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[p17350,p508]) ).
cnf(p17355,plain,
( succ(sk13(sk14)) = sk14
| being_limit_ordinal(sk14) ),
inference(factoring,[status(thm)],[p17354]) ).
cnf(c106,plain,
( being_limit_ordinal(sk14)
| sk14 != succ(X1)
| ~ ordinal(X1) ),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(p452,plain,
( being_limit_ordinal(sk14)
| sk14 != succ(sk13(sk14))
| being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[p436,c106]) ).
cnf(p816,plain,
( sk14 != succ(sk13(sk14))
| being_limit_ordinal(sk14) ),
inference(factoring,[status(thm)],[p452]) ).
cnf(p17356,plain,
( sk14 != sk14
| being_limit_ordinal(sk14)
| being_limit_ordinal(sk14) ),
inference(superposition,[status(thm)],[p17355,p816]) ).
cnf(p17566,plain,
( sk14 != sk14
| being_limit_ordinal(sk14) ),
inference(factoring,[status(thm)],[p17356]) ).
cnf(p17567,plain,
being_limit_ordinal(sk14),
inference(equality_resolution,[status(thm)],[p17566]) ).
cnf(c96,plain,
( in(succ(X1),X0)
| ~ in(X1,X0)
| ~ ordinal(X1)
| ~ being_limit_ordinal(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p419,plain,
( in(succ(X0),sk14)
| ~ in(X0,sk14)
| ~ ordinal(X0)
| ~ being_limit_ordinal(sk14) ),
inference(resolution,[status(thm)],[c96,c100]) ).
cnf(p17570,plain,
( in(succ(X0),sk14)
| ~ in(X0,sk14)
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[p17567,p419]) ).
cnf(c101,plain,
( ordinal(sk15)
| ~ being_limit_ordinal(sk14) ),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(p17568,plain,
ordinal(sk15),
inference(resolution,[status(thm)],[p17567,c101]) ).
cnf(p21064,plain,
( in(sk14,sk14)
| ~ in(sk15,sk14) ),
inference(resolution,[status(thm)],[p17570,p17568]) ).
cnf(c102,plain,
( sk14 = succ(sk15)
| ~ being_limit_ordinal(sk14) ),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(p17569,plain,
sk14 = succ(sk15),
inference(resolution,[status(thm)],[p17567,c102]) ).
fof(f45,axiom,
! [A] : in(A,succ(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_ordinal1) ).
fof(f45_nnf,plain,
! [A] : in(A,succ(A)),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [A] : in(A,succ(A)),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c87,plain,
in(X0,succ(X0)),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p17838,plain,
in(sk15,sk14),
inference(superposition,[status(thm)],[p17569,c87]) ).
cnf(p21076,plain,
in(sk14,sk14),
inference(resolution,[status(thm)],[p21064,p17838]) ).
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]) ).
cnf(p112,plain,
~ in(X0,X0),
inference(factoring,[status(thm)],[c0]) ).
cnf(p21079,plain,
$false,
inference(resolution,[status(thm)],[p21076,p112]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU238+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n014.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 13:21:34 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 73.79/11.63 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 73.79/11.63 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------