%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU238+3 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n013.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 97.76s 18.09s
% Output : Proof 97.76s
% 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(f47,axiom,
! [A] :
( ordinal(A)
=> ( being_limit_ordinal(A)
<=> ! [B] :
( ordinal(B)
=> ( in(B,A)
=> in(succ(B),A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t41_ordinal1) ).
fof(f47_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)],[f47]) ).
fof(f47_sk,plain,
! [A,B] :
( ( ( ( ~ in(succ(sk14(A)),A)
& in(sk14(A),A)
& ordinal(sk14(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,[sk14])],[f47_nnf]) ).
cnf(c94,plain,
( ordinal(sk14(X0))
| being_limit_ordinal(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
fof(f48,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/sandbox/benchmark/theBenchmark.p',t42_ordinal1) ).
fof(f48_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)],[f48]) ).
fof(f48_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)],[f48_neg]) ).
fof(f48_sk,plain,
! [B] :
( ( ( being_limit_ordinal(sk15)
& sk15 = succ(sk16)
& ordinal(sk16) )
| ( ( sk15 != succ(B)
| ~ ordinal(B) )
& ~ being_limit_ordinal(sk15) ) )
& ordinal(sk15) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk15,sk16])],[f48_nnf]) ).
cnf(c97,plain,
ordinal(sk15),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(p457,plain,
( ordinal(sk14(sk15))
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[c94,c97]) ).
fof(f19,axiom,
! [A] :
( ordinal(A)
=> ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_ordinal1) ).
fof(f19_nnf,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c38,plain,
( ordinal(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p480,plain,
( ordinal(succ(sk14(sk15)))
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[p457,c38]) ).
fof(f37,axiom,
! [A,B] :
( ( ordinal(B)
& ordinal(A) )
=> ( ordinal_subset(A,B)
<=> subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_r1_ordinal1) ).
fof(f37_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)],[f37]) ).
fof(f37_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)],[f37_nnf]) ).
cnf(c80,plain,
( subset(X0,X1)
| ~ ordinal_subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p517,plain,
( subset(succ(sk14(sk15)),X0)
| ~ ordinal_subset(succ(sk14(sk15)),X0)
| ~ ordinal(X0)
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[p480,c80]) ).
cnf(p5548,plain,
( subset(succ(sk14(sk15)),sk15)
| ~ ordinal_subset(succ(sk14(sk15)),sk15)
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[p517,c97]) ).
fof(f45,axiom,
! [A] :
( ordinal(A)
=> ! [B] :
( ordinal(B)
=> ( in(A,B)
<=> ordinal_subset(succ(A),B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t33_ordinal1) ).
fof(f45_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)],[f45]) ).
fof(f45_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)],[f45_nnf]) ).
cnf(c89,plain,
( ordinal_subset(succ(X0),X1)
| ~ in(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p485,plain,
( ordinal_subset(succ(sk14(sk15)),X0)
| ~ in(sk14(sk15),X0)
| ~ ordinal(X0)
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[p457,c89]) ).
cnf(p5158,plain,
( ordinal_subset(succ(sk14(sk15)),sk15)
| ~ in(sk14(sk15),sk15)
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[p485,c97]) ).
cnf(c95,plain,
( in(sk14(X0),X0)
| being_limit_ordinal(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p494,plain,
( in(sk14(sk15),sk15)
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[c95,c97]) ).
cnf(p5250,plain,
( being_limit_ordinal(sk15)
| ordinal_subset(succ(sk14(sk15)),sk15)
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[p5158,p494]) ).
cnf(p5251,plain,
( ordinal_subset(succ(sk14(sk15)),sk15)
| being_limit_ordinal(sk15) ),
inference(factoring,[status(thm)],[p5250]) ).
cnf(p6763,plain,
( being_limit_ordinal(sk15)
| subset(succ(sk14(sk15)),sk15)
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[p5548,p5251]) ).
cnf(p6764,plain,
( subset(succ(sk14(sk15)),sk15)
| being_limit_ordinal(sk15) ),
inference(factoring,[status(thm)],[p6763]) ).
fof(f11,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox/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(p6821,plain,
( succ(sk14(sk15)) = sk15
| proper_subset(succ(sk14(sk15)),sk15)
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[p6764,c18]) ).
cnf(c36,plain,
( epsilon_transitive(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p478,plain,
( epsilon_transitive(succ(sk14(sk15)))
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[p457,c36]) ).
fof(f43,axiom,
! [A] :
( epsilon_transitive(A)
=> ! [B] :
( ordinal(B)
=> ( proper_subset(A,B)
=> in(A,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_ordinal1) ).
fof(f43_nnf,plain,
! [A] :
( ! [B] :
( in(A,B)
| ~ proper_subset(A,B)
| ~ ordinal(B) )
| ~ epsilon_transitive(A) ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [A,B] :
( in(A,B)
| ~ proper_subset(A,B)
| ~ ordinal(B)
| ~ epsilon_transitive(A) ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c87,plain,
( in(X0,X1)
| ~ proper_subset(X0,X1)
| ~ ordinal(X1)
| ~ epsilon_transitive(X0) ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p491,plain,
( in(succ(sk14(sk15)),X0)
| ~ proper_subset(succ(sk14(sk15)),X0)
| ~ ordinal(X0)
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[p478,c87]) ).
cnf(p5301,plain,
( in(succ(sk14(sk15)),sk15)
| ~ proper_subset(succ(sk14(sk15)),sk15)
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[p491,c97]) ).
cnf(p7737,plain,
( in(succ(sk14(sk15)),sk15)
| being_limit_ordinal(sk15)
| succ(sk14(sk15)) = sk15
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[p6821,p5301]) ).
cnf(p16987,plain,
( in(succ(sk14(sk15)),sk15)
| succ(sk14(sk15)) = sk15
| being_limit_ordinal(sk15) ),
inference(factoring,[status(thm)],[p7737]) ).
cnf(c96,plain,
( ~ in(succ(sk14(X0)),X0)
| being_limit_ordinal(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p531,plain,
( ~ in(succ(sk14(sk15)),sk15)
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[c96,c97]) ).
cnf(p16991,plain,
( being_limit_ordinal(sk15)
| succ(sk14(sk15)) = sk15
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[p16987,p531]) ).
cnf(p16992,plain,
( succ(sk14(sk15)) = sk15
| being_limit_ordinal(sk15) ),
inference(factoring,[status(thm)],[p16991]) ).
cnf(c103,plain,
( being_limit_ordinal(sk15)
| sk15 != succ(X1)
| ~ ordinal(X1) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(p472,plain,
( being_limit_ordinal(sk15)
| sk15 != succ(sk14(sk15))
| being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[p457,c103]) ).
cnf(p838,plain,
( sk15 != succ(sk14(sk15))
| being_limit_ordinal(sk15) ),
inference(factoring,[status(thm)],[p472]) ).
cnf(p16993,plain,
( sk15 != sk15
| being_limit_ordinal(sk15)
| being_limit_ordinal(sk15) ),
inference(superposition,[status(thm)],[p16992,p838]) ).
cnf(p17199,plain,
( sk15 != sk15
| being_limit_ordinal(sk15) ),
inference(factoring,[status(thm)],[p16993]) ).
cnf(p17200,plain,
being_limit_ordinal(sk15),
inference(equality_resolution,[status(thm)],[p17199]) ).
cnf(c93,plain,
( in(succ(X1),X0)
| ~ in(X1,X0)
| ~ ordinal(X1)
| ~ being_limit_ordinal(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p438,plain,
( in(succ(X0),sk15)
| ~ in(X0,sk15)
| ~ ordinal(X0)
| ~ being_limit_ordinal(sk15) ),
inference(resolution,[status(thm)],[c93,c97]) ).
cnf(p17203,plain,
( in(succ(X0),sk15)
| ~ in(X0,sk15)
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[p17200,p438]) ).
cnf(c98,plain,
( ordinal(sk16)
| ~ being_limit_ordinal(sk15) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(p17201,plain,
ordinal(sk16),
inference(resolution,[status(thm)],[p17200,c98]) ).
cnf(p19418,plain,
( in(sk15,sk15)
| ~ in(sk16,sk15) ),
inference(resolution,[status(thm)],[p17203,p17201]) ).
cnf(c99,plain,
( sk15 = succ(sk16)
| ~ being_limit_ordinal(sk15) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(p17202,plain,
sk15 = succ(sk16),
inference(resolution,[status(thm)],[p17200,c99]) ).
fof(f40,axiom,
! [A] : in(A,succ(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_ordinal1) ).
fof(f40_nnf,plain,
! [A] : in(A,succ(A)),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [A] : in(A,succ(A)),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c84,plain,
in(X0,succ(X0)),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p17528,plain,
in(sk16,sk15),
inference(superposition,[status(thm)],[p17202,c84]) ).
cnf(p19425,plain,
in(sk15,sk15),
inference(resolution,[status(thm)],[p19418,p17528]) ).
fof(f0,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/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(p109,plain,
~ in(X0,X0),
inference(factoring,[status(thm)],[c0]) ).
cnf(p19571,plain,
$false,
inference(resolution,[status(thm)],[p19425,p109]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU238+3 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/5.58 % Computer : n013.cluster.edu
% 0.08/5.58 % Model : x86_64 x86_64
% 0.08/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.58 % Memory : 8046.5625MB
% 0.08/5.58 % OS : Linux 6.8.0-71-generic
% 0.08/5.58 % CPULimit : 300
% 0.08/5.58 % WCLimit : 300
% 0.08/5.58 % DateTime : Thu Sep 24 13:21:13 UTC 2026
% 0.08/5.59 % CPUTime :
% 0.08/5.59 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 97.76/18.09 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 97.76/18.09 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------