%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU235+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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 : Thu Sep 24 02:19:49 PM UTC 2026
% Result : Theorem 1.20s 0.72s
% Output : CNFRefutation 2.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 19
% Syntax : Number of formulae : 142 ( 18 unt; 0 def)
% Number of atoms : 476 ( 46 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 611 ( 277 ~; 248 |; 61 &)
% ( 5 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-1 aty)
% Number of variables : 225 ( 213 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [A] :
( ordinal(A)
=> ( epsilon_connected(A)
& epsilon_transitive(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] :
( empty(A)
=> ( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B] :
( ( ordinal(B)
& ordinal(A) )
=> ( ordinal_subset(B,A)
| ordinal_subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A] :
( epsilon_transitive(A)
<=> ! [B] :
( in(B,A)
=> subset(B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
( ordinal(empty_set)
& epsilon_connected(empty_set)
& epsilon_transitive(empty_set)
& empty(empty_set)
& one_to_one(empty_set)
& function(empty_set)
& relation_empty_yielding(empty_set)
& relation(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [A,B] :
( ( ordinal(B)
& ordinal(A) )
=> ( ordinal_subset(A,B)
<=> subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [A,B] :
( ordinal(B)
=> ( in(A,B)
=> ordinal(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [A] :
( ordinal(A)
=> ! [B] :
( ordinal(B)
=> ~ ( ~ in(B,A)
& A != B
& ~ in(A,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,conjecture,
! [A,B] :
( ordinal(B)
=> ~ ( ! [C] :
( ordinal(C)
=> ~ ( ! [D] :
( ordinal(D)
=> ( in(D,A)
=> ordinal_subset(C,D) ) )
& in(C,A) ) )
& A != empty_set
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,negated_conjecture,
~ ! [A,B] :
( ordinal(B)
=> ~ ( ! [C] :
( ordinal(C)
=> ~ ( ! [D] :
( ordinal(D)
=> ( in(D,A)
=> ordinal_subset(C,D) ) )
& in(C,A) ) )
& A != empty_set
& subset(A,B) ) ),
inference(negated_conjecture,[status(cth)],[f37]) ).
fof(f39,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A,B] :
~ ( ! [C] :
~ ( ! [D] :
~ ( in(D,C)
& in(D,B) )
& in(C,B) )
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,plain,
! [A] :
( ( epsilon_connected(A)
& epsilon_transitive(A) )
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f51,plain,
! [X0] :
( epsilon_transitive(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f61,plain,
! [A] :
( ( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f64,plain,
! [X0] :
( ordinal(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f65,plain,
! [A,B] :
( ordinal_subset(B,A)
| ordinal_subset(A,B)
| ~ ordinal(B)
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f66,plain,
! [X0,X1] :
( ordinal_subset(X1,X0)
| ordinal_subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
! [A] :
( epsilon_transitive(A)
<=> ! [B] :
( subset(B,A)
| ~ in(B,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f68,plain,
! [A] :
( ( ? [B] :
( ~ subset(B,A)
& in(B,A) )
| epsilon_transitive(A) )
& ( ! [B] :
( subset(B,A)
| ~ in(B,A) )
| ~ epsilon_transitive(A) ) ),
inference(NNF_transformation,[status(thm)],[f67]) ).
fof(f69,plain,
( ! [A] :
( ? [B] :
( ~ subset(B,A)
& in(B,A) )
| epsilon_transitive(A) )
& ! [A] :
( ! [B] :
( subset(B,A)
| ~ in(B,A) )
| ~ epsilon_transitive(A) ) ),
inference(miniscoping,[status(thm)],[f68]) ).
fof(f70,plain,
( ! [A] :
( ( ~ subset(sK0_skl(A),A)
& in(sK0_skl(A),A) )
| epsilon_transitive(A) )
& ! [A] :
( ! [B] :
( subset(B,A)
| ~ in(B,A) )
| ~ epsilon_transitive(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f69]) ).
fof(f71,plain,
! [X0,X1] :
( subset(X1,X0)
| ~ in(X1,X0)
| ~ epsilon_transitive(X0) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f74,plain,
! [A] : element(sK1_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B,sK1_skl(A))],[f13]) ).
fof(f75,plain,
! [X0] : element(sK1_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f76,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f87,plain,
ordinal(empty_set),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f97,plain,
( relation(sK4_skl)
& empty(sK4_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f20]) ).
fof(f98,plain,
empty(sK4_skl),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f135,plain,
! [A,B] :
( ( ordinal_subset(A,B)
<=> subset(A,B) )
| ~ ordinal(B)
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f136,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)],[f135]) ).
fof(f137,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ ordinal_subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f138,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| ordinal_subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f146,plain,
! [A,B] :
( ordinal(A)
| ~ in(A,B)
| ~ ordinal(B) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f147,plain,
! [B] :
( ! [A] :
( ordinal(A)
| ~ in(A,B) )
| ~ ordinal(B) ),
inference(miniscoping,[status(thm)],[f146]) ).
fof(f148,plain,
! [X0,X1] :
( ordinal(X1)
| ~ in(X1,X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f149,plain,
! [A] :
( ! [B] :
( in(B,A)
| A = B
| in(A,B)
| ~ ordinal(B) )
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f150,plain,
! [X0,X1] :
( in(X1,X0)
| X0 = X1
| in(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f151,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f152,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f153,plain,
? [A,B] :
( ! [C] :
( ? [D] :
( ~ ordinal_subset(C,D)
& in(D,A)
& ordinal(D) )
| ~ in(C,A)
| ~ ordinal(C) )
& A != empty_set
& subset(A,B)
& ordinal(B) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f154,plain,
? [B] :
( ? [A] :
( ! [C] :
( ? [D] :
( ~ ordinal_subset(C,D)
& in(D,A)
& ordinal(D) )
| ~ in(C,A)
| ~ ordinal(C) )
& A != empty_set
& subset(A,B) )
& ordinal(B) ),
inference(miniscoping,[status(thm)],[f153]) ).
fof(f155,plain,
( ! [C] :
( ( ~ ordinal_subset(C,sK16_skl(C))
& in(sK16_skl(C),sK15_skl)
& ordinal(sK16_skl(C)) )
| ~ in(C,sK15_skl)
| ~ ordinal(C) )
& sK15_skl != empty_set
& subset(sK15_skl,sK14_skl)
& ordinal(sK14_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl]),skolemize(B,sK14_skl),skolemize(A,sK15_skl),skolemize(D,sK16_skl(C))],[f154]) ).
fof(f156,plain,
ordinal(sK14_skl),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f157,plain,
subset(sK15_skl,sK14_skl),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f158,plain,
sK15_skl != empty_set,
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f159,plain,
! [X0] :
( ordinal(sK16_skl(X0))
| ~ in(X0,sK15_skl)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f160,plain,
! [X0] :
( in(sK16_skl(X0),sK15_skl)
| ~ in(X0,sK15_skl)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f161,plain,
! [X0] :
( ~ ordinal_subset(X0,sK16_skl(X0))
| ~ in(X0,sK15_skl)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f162,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(NNF_transformation,[status(thm)],[f39]) ).
fof(f163,plain,
( ! [A,B] :
( ~ subset(A,B)
| element(A,powerset(B)) )
& ! [A,B] :
( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(miniscoping,[status(thm)],[f162]) ).
fof(f165,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f166,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f167,plain,
! [A,C] :
( element(A,C)
| ! [B] :
( ~ element(B,powerset(C))
| ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f166]) ).
fof(f168,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f169,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f170,plain,
! [C] :
( ~ empty(C)
| ! [B] :
( ~ element(B,powerset(C))
| ! [A] : ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f169]) ).
fof(f171,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f172,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f173,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f174,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f175,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f174]) ).
fof(f176,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f177,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f178,plain,
! [B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f177]) ).
fof(f179,plain,
! [B] :
( ( ! [D] :
( ~ in(D,sK17_skl(B))
| ~ in(D,B) )
& in(sK17_skl(B),B) )
| ! [A] : ~ in(A,B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(C,sK17_skl(B))],[f178]) ).
fof(f180,plain,
! [X0,X1] :
( in(sK17_skl(X1),X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f181,plain,
! [X0,X1,X2] :
( ~ in(X2,sK17_skl(X1))
| ~ in(X2,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f187,plain,
! [X0] : ~ in(X0,empty_set),
inference(resolution,[status(thm)],[f176,f76]) ).
fof(f192,plain,
! [X0] :
( ~ in(X0,sK15_skl)
| ~ ordinal(X0)
| ~ subset(X0,sK16_skl(X0))
| ~ ordinal(sK16_skl(X0))
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f138,f161]) ).
fof(f193,plain,
! [X0] :
( ~ in(X0,sK15_skl)
| ~ subset(X0,sK16_skl(X0))
| ~ ordinal(sK16_skl(X0))
| ~ ordinal(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f192]) ).
fof(f194,plain,
! [X0] :
( ~ in(X0,sK15_skl)
| ~ subset(X0,sK16_skl(X0))
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f193,f159]) ).
fof(f199,plain,
! [X0] :
( empty_set = X0
| in(empty_set,X0)
| ~ ordinal(X0)
| ~ ordinal(empty_set) ),
inference(resolution,[status(thm)],[f150,f187]) ).
fof(f202,plain,
! [X0] :
( empty_set = X0
| in(empty_set,X0)
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f199,f87]) ).
fof(f249,plain,
! [X0] :
( in(sK1_skl(X0),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f152,f75]) ).
fof(f253,plain,
sK4_skl = empty_set,
inference(resolution,[status(thm)],[f98,f173]) ).
fof(f262,plain,
! [X0] :
( sK4_skl = X0
| in(empty_set,X0)
| ~ ordinal(X0) ),
inference(backward_demodulation,[status(thm)],[f253,f202]) ).
fof(f270,plain,
ordinal(sK4_skl),
inference(backward_demodulation,[status(thm)],[f253,f87]) ).
fof(f273,plain,
sK15_skl != sK4_skl,
inference(backward_demodulation,[status(thm)],[f253,f158]) ).
fof(f290,plain,
! [X0] :
( sK4_skl = X0
| in(sK4_skl,X0)
| ~ ordinal(X0) ),
inference(forward_demodulation,[status(thm)],[f253,f262]) ).
fof(f393,plain,
! [X0,X1,X2] :
( in(X0,X2)
| empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f168,f152]) ).
fof(f394,plain,
! [X0,X1,X2] :
( in(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f393,f171]) ).
fof(f396,plain,
! [X0] :
( ~ subset(sK17_skl(sK15_skl),sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f180,f194]) ).
fof(f398,plain,
! [X0] :
( ~ ordinal_subset(sK17_skl(sK15_skl),sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f396,f137]) ).
fof(f399,plain,
! [X0] :
( ~ in(sK17_skl(sK15_skl),sK16_skl(sK17_skl(sK15_skl)))
| ~ epsilon_transitive(sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f396,f71]) ).
fof(f400,plain,
! [X0] :
( ~ ordinal_subset(sK17_skl(sK15_skl),sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f398]) ).
fof(f402,plain,
! [X0] :
( ordinal_subset(sK16_skl(sK17_skl(sK15_skl)),sK17_skl(sK15_skl))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ ordinal(sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f400,f66]) ).
fof(f404,plain,
! [X0] :
( ordinal_subset(sK16_skl(sK17_skl(sK15_skl)),sK17_skl(sK15_skl))
| ~ ordinal(sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f402]) ).
fof(f405,plain,
! [X0] :
( sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl)
| in(sK16_skl(sK17_skl(sK15_skl)),sK17_skl(sK15_skl))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ ordinal(sK16_skl(sK17_skl(sK15_skl)))
| ~ epsilon_transitive(sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f399,f150]) ).
fof(f406,plain,
! [X0] :
( sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl)
| in(sK16_skl(sK17_skl(sK15_skl)),sK17_skl(sK15_skl))
| ~ ordinal(sK16_skl(sK17_skl(sK15_skl)))
| ~ epsilon_transitive(sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f405]) ).
fof(f407,plain,
! [X0] :
( sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl)
| in(sK16_skl(sK17_skl(sK15_skl)),sK17_skl(sK15_skl))
| ~ ordinal(sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f406,f51]) ).
fof(f431,plain,
! [X0,X1] :
( sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl)
| ~ ordinal(sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X1,sK15_skl)
| ~ in(sK16_skl(sK17_skl(sK15_skl)),sK15_skl)
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f181,f407]) ).
fof(f441,plain,
! [X0,X1] :
( ~ in(sK17_skl(sK15_skl),sK15_skl)
| ~ ordinal(sK17_skl(sK15_skl))
| sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl)
| ~ ordinal(sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X1,sK15_skl)
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f431,f160]) ).
fof(f443,plain,
! [X0,X1] :
( ~ in(sK17_skl(sK15_skl),sK15_skl)
| sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl)
| ~ ordinal(sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X1,sK15_skl)
| ~ in(X0,sK15_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f441]) ).
fof(f444,plain,
! [X0,X1] :
( ~ in(sK17_skl(sK15_skl),sK15_skl)
| sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl)
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X1,sK15_skl)
| ~ in(X0,sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f443,f159]) ).
fof(f446,plain,
! [X0,X1,X2] :
( ~ in(X2,sK15_skl)
| sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl)
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X1,sK15_skl)
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f444,f180]) ).
fof(f451,plain,
! [X0,X1,X2,X3] :
( ~ in(sK17_skl(sK15_skl),X3)
| ~ ordinal(X3)
| ~ in(X2,sK15_skl)
| sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl)
| ~ in(X1,sK15_skl)
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f446,f148]) ).
fof(f529,plain,
! [X0,X1,X2] :
( ~ subset(X1,X2)
| in(X0,X2)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f394,f165]) ).
fof(f607,plain,
! [X0] :
( in(X0,sK14_skl)
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f529,f157]) ).
fof(f611,plain,
! [X0] :
( ~ in(X0,sK15_skl)
| in(sK17_skl(sK15_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f607,f180]) ).
fof(f621,plain,
! [X0,X1,X2,X3] :
( ~ ordinal(sK14_skl)
| ~ in(X3,sK15_skl)
| sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl)
| ~ in(X2,sK15_skl)
| ~ in(X1,sK15_skl)
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f611,f451]) ).
fof(f624,plain,
! [X0,X1,X2,X3] :
( ~ in(X3,sK15_skl)
| sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl)
| ~ in(X2,sK15_skl)
| ~ in(X1,sK15_skl)
| ~ in(X0,sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f621,f156]) ).
fof(f698,plain,
! [X0] :
( empty(sK15_skl)
| sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl)
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f624,f249]) ).
fof(f721,plain,
! [X0] :
( sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl)
| ~ in(X0,sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f698,f176]) ).
fof(f727,plain,
( empty(sK15_skl)
| sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl) ),
inference(resolution,[status(thm)],[f721,f249]) ).
fof(f728,plain,
( sK4_skl = sK15_skl
| ~ ordinal(sK15_skl)
| sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl) ),
inference(resolution,[status(thm)],[f721,f290]) ).
fof(f731,plain,
( ~ ordinal(sK15_skl)
| sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f728,f273]) ).
fof(f734,plain,
( ~ empty(sK15_skl)
| sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl) ),
inference(resolution,[status(thm)],[f731,f64]) ).
fof(f737,plain,
! [X0] :
( ordinal_subset(sK17_skl(sK15_skl),sK17_skl(sK15_skl))
| ~ ordinal(sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(backward_demodulation,[status(thm)],[f744,f404]) ).
fof(f739,plain,
! [X0] :
( ~ ordinal_subset(sK17_skl(sK15_skl),sK17_skl(sK15_skl))
| ~ ordinal(sK16_skl(sK17_skl(sK15_skl)))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(backward_demodulation,[status(thm)],[f744,f400]) ).
fof(f744,plain,
sK16_skl(sK17_skl(sK15_skl)) = sK17_skl(sK15_skl),
inference(forward_subsumption_resolution,[status(thm)],[f734,f727]) ).
fof(f745,plain,
! [X0] :
( ordinal_subset(sK17_skl(sK15_skl),sK17_skl(sK15_skl))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(forward_demodulation,[status(thm)],[f744,f737]) ).
fof(f746,plain,
! [X0] :
( ordinal_subset(sK17_skl(sK15_skl),sK17_skl(sK15_skl))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f745]) ).
fof(f749,plain,
! [X0] :
( ~ ordinal_subset(sK17_skl(sK15_skl),sK17_skl(sK15_skl))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(forward_demodulation,[status(thm)],[f744,f739]) ).
fof(f750,plain,
! [X0] :
( ~ ordinal_subset(sK17_skl(sK15_skl),sK17_skl(sK15_skl))
| ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f749]) ).
fof(f751,plain,
! [X0] :
( ~ ordinal(sK17_skl(sK15_skl))
| ~ in(X0,sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f750,f746]) ).
fof(f816,plain,
! [X0,X1] :
( ~ in(sK17_skl(sK15_skl),X1)
| ~ ordinal(X1)
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f751,f148]) ).
fof(f819,plain,
! [X0,X1] :
( ~ in(X1,sK15_skl)
| ~ ordinal(sK14_skl)
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f816,f611]) ).
fof(f822,plain,
! [X0] :
( ~ in(X0,sK15_skl)
| ~ ordinal(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f160,f823]) ).
fof(f823,plain,
! [X0,X1] :
( ~ in(X1,sK15_skl)
| ~ in(X0,sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f819,f156]) ).
fof(f827,plain,
( sK4_skl = sK15_skl
| ~ ordinal(sK15_skl)
| ~ ordinal(sK4_skl) ),
inference(resolution,[status(thm)],[f822,f290]) ).
fof(f828,plain,
! [X0] :
( sK15_skl = X0
| in(sK15_skl,X0)
| ~ ordinal(X0)
| ~ ordinal(sK15_skl)
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f822,f150]) ).
fof(f829,plain,
( sK4_skl = sK15_skl
| ~ ordinal(sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f827,f270]) ).
fof(f830,plain,
! [X0] :
( sK15_skl = X0
| in(sK15_skl,X0)
| ~ ordinal(sK15_skl)
| ~ ordinal(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f828]) ).
fof(f832,plain,
! [X0] :
( ~ in(sK15_skl,X0)
| ~ ordinal(X0)
| sK4_skl = sK15_skl ),
inference(resolution,[status(thm)],[f829,f148]) ).
fof(f836,plain,
! [X0] :
( sK15_skl = X0
| ~ ordinal(sK15_skl)
| ~ ordinal(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f830,f837]) ).
fof(f837,plain,
! [X0] :
( ~ in(sK15_skl,X0)
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f832,f273]) ).
fof(f841,plain,
! [X0] :
( empty(sK15_skl)
| ~ in(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f823,f249]) ).
fof(f844,plain,
! [X0] : ~ in(X0,sK15_skl),
inference(forward_subsumption_resolution,[status(thm)],[f841,f176]) ).
fof(f846,plain,
empty(sK15_skl),
inference(resolution,[status(thm)],[f844,f249]) ).
fof(f859,plain,
! [X0] :
( ~ empty(sK15_skl)
| sK15_skl = X0
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f836,f64]) ).
fof(f860,plain,
! [X0] :
( sK15_skl = X0
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f859,f846]) ).
fof(f875,plain,
sK15_skl = sK4_skl,
inference(resolution,[status(thm)],[f860,f270]) ).
fof(f882,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f875,f273]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU235+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n008.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 06:02:39 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 1.20/0.72 % Refutation found
% 1.20/0.72 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.20/0.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.41/0.76 % Elapsed time: 0.387000 seconds
% 2.41/0.76 % CPU time: 2.773381 seconds
% 2.41/0.76 % Total memory used: 119.456 MB
% 2.41/0.76 % Net memory used: 115.626 MB
%------------------------------------------------------------------------------